(* Title: ZF/ex/LList.thy ID: $Id: LList.thy,v 1.11 2005/06/17 14:15:11 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Codatatype definition of Lazy Lists Equality for llist(A) as a greatest fixed point Functions for Lazy Lists STILL NEEDS: co_recursion for defining lconst, flip, etc. a typing rule for it, based on some notion of "productivity..." *) theory LList imports Main begin consts llist :: "i=>i"; codatatype "llist(A)" = LNil | LCons ("a ∈ A", "l ∈ llist(A)") (*Coinductive definition of equality*) consts lleq :: "i=>i" (*Previously used <*> in the domain and variant pairs as elements. But standard pairs work just as well. To use variant pairs, must change prefix a q/Q to the Sigma, Pair and converse rules.*) coinductive domains "lleq(A)" <= "llist(A) * llist(A)" intros LNil: "<LNil, LNil> ∈ lleq(A)" LCons: "[| a ∈ A; <l,l'> ∈ lleq(A) |] ==> <LCons(a,l), LCons(a,l')> ∈ lleq(A)" type_intros llist.intros (*Lazy list functions; flip is not definitional!*) consts lconst :: "i => i" flip :: "i => i" defs lconst_def: "lconst(a) == lfp(univ(a), %l. LCons(a,l))" axioms flip_LNil: "flip(LNil) = LNil" flip_LCons: "[| x ∈ bool; l ∈ llist(bool) |] ==> flip(LCons(x,l)) = LCons(not(x), flip(l))" (*These commands cause classical reasoning to regard the subset relation as primitive, not reducing it to membership*) declare subsetI [rule del] subsetCE [rule del] declare subset_refl [intro!] cons_subsetI [intro!] subset_consI [intro!] Union_least [intro!] UN_least [intro!] Un_least [intro!] Inter_greatest [intro!] Int_greatest [intro!] RepFun_subset [intro!] Un_upper1 [intro!] Un_upper2 [intro!] Int_lower1 [intro!] Int_lower2 [intro!] (*An elimination rule, for type-checking*) inductive_cases LConsE: "LCons(a,l) ∈ llist(A)" (*Proving freeness results*) lemma LCons_iff: "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'" by auto lemma LNil_LCons_iff: "~ LNil=LCons(a,l)" by auto (* lemma llist_unfold: "llist(A) = {0} <+> (A <*> llist(A))"; let open llist val rew = rewrite_rule con_defs in by (fast_tac (claset() addSIs (subsetI ::map rew intros) addEs [rew elim]) 1) end done *) (*** Lemmas to justify using "llist" in other recursive type definitions ***) lemma llist_mono: "A ⊆ B ==> llist(A) ⊆ llist(B)" apply (unfold llist.defs ) apply (rule gfp_mono) apply (rule llist.bnd_mono) apply (assumption | rule quniv_mono basic_monos)+ done (** Closure of quniv(A) under llist -- why so complex? Its a gfp... **) declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!] QPair_subset_univ [intro!] empty_subsetI [intro!] one_in_quniv [THEN qunivD, intro!] declare qunivD [dest!] declare Ord_in_Ord [elim!] lemma llist_quniv_lemma [rule_format]: "Ord(i) ==> ∀l ∈ llist(quniv(A)). l Int Vset(i) ⊆ univ(eclose(A))" apply (erule trans_induct) apply (rule ballI) apply (erule llist.cases) apply (simp_all add: QInl_def QInr_def llist.con_defs) (*LCons case: I simply can't get rid of the deepen_tac*) apply (tactic "deepen_tac (claset() addIs [Ord_trans] addIs [Int_lower1 RS subset_trans]) 2 1") done lemma llist_quniv: "llist(quniv(A)) ⊆ quniv(A)" apply (rule qunivI [THEN subsetI]) apply (rule Int_Vset_subset) apply (assumption | rule llist_quniv_lemma)+ done lemmas llist_subset_quniv = subset_trans [OF llist_mono llist_quniv] (*** Lazy List Equality: lleq ***) declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!] QPair_mono [intro!] declare Ord_in_Ord [elim!] (*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*) lemma lleq_Int_Vset_subset [rule_format]: "Ord(i) ==> ∀l l'. <l,l'> ∈ lleq(A) --> l Int Vset(i) ⊆ l'" apply (erule trans_induct) apply (intro allI impI) apply (erule lleq.cases) apply (unfold QInr_def llist.con_defs, safe) apply (fast elim!: Ord_trans bspec [elim_format]) done (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) lemma lleq_symmetric: "<l,l'> ∈ lleq(A) ==> <l',l> ∈ lleq(A)" apply (erule lleq.coinduct [OF converseI]) apply (rule lleq.dom_subset [THEN converse_type], safe) apply (erule lleq.cases, blast+) done lemma lleq_implies_equal: "<l,l'> ∈ lleq(A) ==> l=l'" apply (rule equalityI) apply (assumption | rule lleq_Int_Vset_subset [THEN Int_Vset_subset] | erule lleq_symmetric)+ done lemma equal_llist_implies_leq: "[| l=l'; l ∈ llist(A) |] ==> <l,l'> ∈ lleq(A)" apply (rule_tac X = "{<l,l>. l ∈ llist (A) }" in lleq.coinduct) apply blast apply safe apply (erule_tac a=l in llist.cases, fast+) done (*** Lazy List Functions ***) (*Examples of coinduction for type-checking and to prove llist equations*) (*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***) lemma lconst_fun_bnd_mono: "bnd_mono(univ(a), %l. LCons(a,l))" apply (unfold llist.con_defs ) apply (rule bnd_monoI) apply (blast intro: A_subset_univ QInr_subset_univ) apply (blast intro: subset_refl QInr_mono QPair_mono) done (* lconst(a) = LCons(a,lconst(a)) *) lemmas lconst = def_lfp_unfold [OF lconst_def lconst_fun_bnd_mono] lemmas lconst_subset = lconst_def [THEN def_lfp_subset] lemmas member_subset_Union_eclose = arg_into_eclose [THEN Union_upper] lemma lconst_in_quniv: "a ∈ A ==> lconst(a) ∈ quniv(A)" apply (rule lconst_subset [THEN subset_trans, THEN qunivI]) apply (erule arg_into_eclose [THEN eclose_subset, THEN univ_mono]) done lemma lconst_type: "a ∈ A ==> lconst(a): llist(A)" apply (rule singletonI [THEN llist.coinduct]) apply (erule lconst_in_quniv [THEN singleton_subsetI]) apply (fast intro!: lconst) done (*** flip --- equations merely assumed; certain consequences proved ***) declare flip_LNil [simp] flip_LCons [simp] not_type [simp] lemma bool_Int_subset_univ: "b ∈ bool ==> b Int X ⊆ univ(eclose(A))" by (fast intro: Int_lower1 [THEN subset_trans] elim!: boolE) declare not_type [intro!] declare bool_Int_subset_univ [intro] (*Reasoning borrowed from lleq.ML; a similar proof works for all "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*) lemma flip_llist_quniv_lemma [rule_format]: "Ord(i) ==> ∀l ∈ llist(bool). flip(l) Int Vset(i) ⊆ univ(eclose(bool))" apply (erule trans_induct) apply (rule ballI) apply (erule llist.cases, simp_all) apply (simp_all add: QInl_def QInr_def llist.con_defs) (*LCons case: I simply can't get rid of the deepen_tac*) apply (tactic "deepen_tac (claset() addIs [Ord_trans] addIs [Int_lower1 RS subset_trans]) 2 1") done lemma flip_in_quniv: "l ∈ llist(bool) ==> flip(l) ∈ quniv(bool)" by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+) lemma flip_type: "l ∈ llist(bool) ==> flip(l): llist(bool)" apply (rule_tac X = "{flip (l) . l ∈ llist (bool) }" in llist.coinduct) apply blast apply (fast intro!: flip_in_quniv) apply (erule RepFunE) apply (erule_tac a=la in llist.cases, auto) done lemma flip_flip: "l ∈ llist(bool) ==> flip(flip(l)) = l" apply (rule_tac X1 = "{<flip (flip (l)),l> . l ∈ llist (bool) }" in lleq.coinduct [THEN lleq_implies_equal]) apply blast apply (fast intro!: flip_type) apply (erule RepFunE) apply (erule_tac a=la in llist.cases) apply (simp_all add: flip_type not_not) done end
lemmas LConsE:
[| LCons(a, l) ∈ llist(A); [| a ∈ A; l ∈ llist(A) |] ==> Q |] ==> Q
lemma LCons_iff:
LCons(a, l) = LCons(a', l') <-> a = a' ∧ l = l'
lemma LNil_LCons_iff:
LNil ≠ LCons(a, l)
lemma llist_mono:
A ⊆ B ==> llist(A) ⊆ llist(B)
lemma llist_quniv_lemma:
[| Ord(i); l ∈ llist(quniv(A)) |] ==> l ∩ Vset(i) ⊆ univ(eclose(A))
lemma llist_quniv:
llist(quniv(A)) ⊆ quniv(A)
lemmas llist_subset_quniv:
A2 ⊆ quniv(A1) ==> llist(A2) ⊆ quniv(A1)
lemmas llist_subset_quniv:
A2 ⊆ quniv(A1) ==> llist(A2) ⊆ quniv(A1)
lemma lleq_Int_Vset_subset:
[| Ord(i); 〈l, l'〉 ∈ lleq(A) |] ==> l ∩ Vset(i) ⊆ l'
lemma lleq_symmetric:
〈l, l'〉 ∈ lleq(A) ==> 〈l', l〉 ∈ lleq(A)
lemma lleq_implies_equal:
〈l, l'〉 ∈ lleq(A) ==> l = l'
lemma equal_llist_implies_leq:
[| l = l'; l ∈ llist(A) |] ==> 〈l, l'〉 ∈ lleq(A)
lemma lconst_fun_bnd_mono:
bnd_mono(univ(a), %l. LCons(a, l))
lemmas lconst:
lconst(a1) = LCons(a1, lconst(a1))
lemmas lconst:
lconst(a1) = LCons(a1, lconst(a1))
lemmas lconst_subset:
lconst(a1) ⊆ univ(a1)
lemmas lconst_subset:
lconst(a1) ⊆ univ(a1)
lemmas member_subset_Union_eclose:
B ∈ A1 ==> B ⊆ \<Union>eclose(A1)
lemmas member_subset_Union_eclose:
B ∈ A1 ==> B ⊆ \<Union>eclose(A1)
lemma lconst_in_quniv:
a ∈ A ==> lconst(a) ∈ quniv(A)
lemma lconst_type:
a ∈ A ==> lconst(a) ∈ llist(A)
lemma bool_Int_subset_univ:
b ∈ bool ==> b ∩ X ⊆ univ(eclose(A))
lemma flip_llist_quniv_lemma:
[| Ord(i); l ∈ llist(bool) |] ==> flip(l) ∩ Vset(i) ⊆ univ(eclose(bool))
lemma flip_in_quniv:
l ∈ llist(bool) ==> flip(l) ∈ quniv(bool)
lemma flip_type:
l ∈ llist(bool) ==> flip(l) ∈ llist(bool)
lemma flip_flip:
l ∈ llist(bool) ==> flip(flip(l)) = l