diff -r c00df7765656 -r 5c900a821a7c src/ZF/ex/LList.thy --- a/src/ZF/ex/LList.thy Sat Feb 02 13:26:51 2002 +0100 +++ b/src/ZF/ex/LList.thy Mon Feb 04 13:16:54 2002 +0100 @@ -14,43 +14,242 @@ a typing rule for it, based on some notion of "productivity..." *) -LList = Main + +theory LList = Main: consts - llist :: i=>i + llist :: "i=>i"; codatatype - "llist(A)" = LNil | LCons ("a \\ A", "l \\ llist(A)") + "llist(A)" = LNil | LCons ("a \ A", "l \ llist(A)") (*Coinductive definition of equality*) consts - lleq :: i=>i + 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)" - intrs - LNil " \\ lleq(A)" - LCons "[| a \\ A; : lleq(A) |] ==> : lleq(A)" - type_intrs "llist.intrs" + intros + LNil: " \ lleq(A)" + LCons: "[| a \ A; \ lleq(A) |] + ==> \ lleq(A)" + type_intros llist.intros (*Lazy list functions; flip is not definitional!*) consts - lconst :: i => i - flip :: i => i + lconst :: "i => i" + flip :: "i => i" defs - lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))" + 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'. \ 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) +apply safe +apply (fast elim!: Ord_trans bspec [elim_format]) +done -rules - flip_LNil "flip(LNil) = LNil" +(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) +lemma lleq_symmetric: " \ lleq(A) ==> \ lleq(A)" +apply (erule lleq.coinduct [OF converseI]) +apply (rule lleq.dom_subset [THEN converse_type]) +apply safe +apply (erule lleq.cases) +apply blast+ +done + +lemma lleq_implies_equal: " \ 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) |] ==> \ lleq(A)" +apply (rule_tac X = "{. l \ llist (A) }" in lleq.coinduct) +apply blast +apply safe +apply (erule_tac a="l" in llist.cases) +apply 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 - flip_LCons "[| x \\ bool; l \\ llist(bool) |] ==> - flip(LCons(x,l)) = LCons(not(x), flip(l))" +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) +apply (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)" +apply (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI]) +apply assumption+ +done + +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) +apply auto +done + +lemma flip_flip: "l \ llist(bool) ==> flip(flip(l)) = l" +apply (rule_tac X1 = "{ . 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