diff -r d9527f97246e -r 89669c58e506 LList.ML --- a/LList.ML Thu Aug 25 10:47:33 1994 +0200 +++ b/LList.ML Thu Aug 25 11:01:45 1994 +0200 @@ -3,11 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -For llist.thy. - SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)? - -TOO LONG! needs splitting up *) open LList; @@ -23,55 +19,46 @@ delsimps [Pair_eq]; -(** the llist functional **) - -val LList_unfold = rewrite_rule [List_Fun_def] - (List_Fun_mono RS (LList_def RS def_gfp_Tarski)); +(*This justifies using llist in other recursive type definitions*) +goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)"; +by (rtac gfp_mono 1); +by (REPEAT (ares_tac basic_monos 1)); +val llist_mono = result(); -(*This justifies using LList in other recursive type definitions*) -goalw LList.thy [LList_def] "!!A B. A<=B ==> LList(A) <= LList(B)"; -by (rtac gfp_mono 1); -by (etac List_Fun_mono2 1); -val LList_mono = result(); -(*Elimination is case analysis, not induction.*) -val [major,prem1,prem2] = goalw LList.thy [NIL_def,CONS_def] - "[| L : LList(A); \ -\ L=NIL ==> P; \ -\ !!M N. [| M:A; N: LList(A); L=CONS(M,N) |] ==> P \ -\ |] ==> P"; -by (rtac (major RS (LList_unfold RS equalityD1 RS subsetD RS usumE)) 1); -by (etac uprodE 2); -by (rtac prem2 2); -by (rtac prem1 1); -by (REPEAT (ares_tac [refl] 1 - ORELSE eresolve_tac [singletonE,ssubst] 1)); -val LListE = result(); +goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))"; +let val rew = rewrite_rule [NIL_def, CONS_def] in +by (fast_tac (univ_cs addSIs (equalityI :: map rew llist.intrs) + addEs [rew llist.elim]) 1) +end; +val llist_unfold = result(); -(*** Type checking by co-induction, using List_Fun ***) - -val prems = goalw LList.thy [LList_def] - "[| M : X; X <= List_Fun(A, X Un LList(A)) |] ==> M : LList(A)"; -by (REPEAT (resolve_tac (prems@[List_Fun_mono RS coinduct]) 1)); -val LList_coinduct = result(); - -(** Rules to prove the 2nd premise of LList_coinduct **) +(*** Type checking by coinduction, using list_Fun + THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! +***) -goalw LList.thy [List_Fun_def,NIL_def] "NIL: List_Fun(A,X)"; -by (resolve_tac [singletonI RS usum_In0I] 1); -val List_Fun_NIL_I = result(); +goalw LList.thy [list_Fun_def] + "!!M. [| M : X; X <= list_Fun(A, X Un llist(A)) |] ==> M : llist(A)"; +be llist.coinduct 1; +be (subsetD RS CollectD) 1; +ba 1; +val llist_coinduct = result(); -goalw LList.thy [List_Fun_def,CONS_def] - "!!M N. [| M: A; N: X |] ==> CONS(M,N) : List_Fun(A,X)"; -by (REPEAT (ares_tac [uprodI RS usum_In1I] 1)); -val List_Fun_CONS_I = result(); +goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun(A,X)"; +by (fast_tac set_cs 1); +val list_Fun_NIL_I = result(); + +goalw LList.thy [list_Fun_def,CONS_def] + "!!M N. [| M: A; N: X |] ==> CONS(M,N) : list_Fun(A,X)"; +by (fast_tac set_cs 1); +val list_Fun_CONS_I = result(); (*Utilise the "strong" part, i.e. gfp(f)*) -goalw LList.thy [LList_def] - "!!M N. M: LList(A) ==> M : List_Fun(A, X Un LList(A))"; -by (etac (List_Fun_mono RS gfp_fun_UnI2) 1); -val List_Fun_LList_I = result(); +goalw LList.thy (llist.defs @ [list_Fun_def]) + "!!M N. M: llist(A) ==> M : list_Fun(A, X Un llist(A))"; +by (etac (llist.mono RS gfp_fun_UnI2) 1); +val list_Fun_llist_I = result(); (*** LList_corec satisfies the desired recurion equation ***) @@ -137,119 +124,140 @@ (*A typical use of co-induction to show membership in the gfp. Bisimulation is range(%x. LList_corec(x,f)) *) -goal LList.thy "LList_corec(a,f) : LList({u.True})"; -by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] LList_coinduct 1); +goal LList.thy "LList_corec(a,f) : llist({u.True})"; +by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] llist_coinduct 1); by (rtac rangeI 1); by (safe_tac set_cs); by (stac LList_corec 1); -by (simp_tac (llist_ss addsimps [List_Fun_NIL_I,List_Fun_CONS_I, CollectI] +by (simp_tac (llist_ss addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI] |> add_eqI) 1); val LList_corec_type = result(); (*Lemma for the proof of llist_corec*) goal LList.thy "LList_corec(a, %z.sum_case(Inl, split(%v w.Inr()), f(z))) : \ -\ LList(range(Leaf))"; -by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] LList_coinduct 1); +\ llist(range(Leaf))"; +by (res_inst_tac [("X", "range(%x.LList_corec(x,?g))")] llist_coinduct 1); by (rtac rangeI 1); by (safe_tac set_cs); by (stac LList_corec 1); -by (asm_simp_tac (llist_ss addsimps [List_Fun_NIL_I, Pair_eq]) 1); -by (fast_tac (set_cs addSIs [List_Fun_CONS_I]) 1); +by (asm_simp_tac (llist_ss addsimps [list_Fun_NIL_I]) 1); +by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1); val LList_corec_type2 = result(); -(**** LList equality as a gfp; the bisimulation principle ****) + +(**** llist equality as a gfp; the bisimulation principle ****) -goalw LList.thy [LListD_Fun_def] "mono(LListD_Fun(r))"; -by (REPEAT (ares_tac [monoI, subset_refl, dsum_mono, dprod_mono] 1)); -val LListD_Fun_mono = result(); - -val LListD_unfold = rewrite_rule [LListD_Fun_def] - (LListD_Fun_mono RS (LListD_def RS def_gfp_Tarski)); +(*This theorem is actually used, unlike the many similar ones in ZF*) +goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))"; +let val rew = rewrite_rule [NIL_def, CONS_def] in +by (fast_tac (univ_cs addSIs (equalityI :: map rew LListD.intrs) + addEs [rew LListD.elim]) 1) +end; +val LListD_unfold = result(); goal LList.thy "!M N. : LListD(diag(A)) --> ntrunc(k,M) = ntrunc(k,N)"; by (res_inst_tac [("n", "k")] less_induct 1); by (safe_tac set_cs); -by (etac (LListD_unfold RS equalityD1 RS subsetD RS dsumE) 1); -by (safe_tac (set_cs addSEs [Pair_inject, dprodE, diagE])); +by (etac LListD.elim 1); +by (safe_tac (prod_cs addSEs [diagE])); by (res_inst_tac [("n", "n")] natE 1); by (asm_simp_tac (univ_ss addsimps [ntrunc_0]) 1); -by (res_inst_tac [("n", "xb")] natE 1); -by (asm_simp_tac (univ_ss addsimps [ntrunc_one_In1]) 1); -by (asm_simp_tac (univ_ss addsimps [ntrunc_In1, ntrunc_Scons]) 1); +by (rename_tac "n'" 1); +by (res_inst_tac [("n", "n'")] natE 1); +by (asm_simp_tac (univ_ss addsimps [CONS_def, ntrunc_one_In1]) 1); +by (asm_simp_tac (univ_ss addsimps [CONS_def, ntrunc_In1, ntrunc_Scons]) 1); val LListD_implies_ntrunc_equality = result(); -goalw LList.thy [LList_def,List_Fun_def] "fst``LListD(diag(A)) <= LList(A)"; +(*The domain of the LListD relation*) +goalw LList.thy (llist.defs @ [NIL_def, CONS_def]) + "fst``LListD(diag(A)) <= llist(A)"; by (rtac gfp_upperbound 1); +(*avoids unfolding LListD on the rhs*) by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1); by (simp_tac fst_image_ss 1); +by (fast_tac univ_cs 1); val fst_image_LListD = result(); (*This inclusion justifies the use of coinduction to show M=N*) -goal LList.thy "LListD(diag(A)) <= diag(LList(A))"; +goal LList.thy "LListD(diag(A)) <= diag(llist(A))"; by (rtac subsetI 1); by (res_inst_tac [("p","x")] PairE 1); by (safe_tac HOL_cs); -by (res_inst_tac [("s","xa")] subst 1); +by (rtac diag_eqI 1); by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS ntrunc_equality) 1); by (assume_tac 1); -by (rtac diagI 1); by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1); val LListD_subset_diag = result(); -(*This converse inclusion helps to strengthen LList_equalityI*) -goalw LList.thy [LListD_def] "diag(LList(A)) <= LListD(diag(A))"; -by (rtac gfp_upperbound 1); +(** Coinduction, using LListD_Fun + THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! + **) + +goalw LList.thy [LListD_Fun_def] + "!!M. [| M : X; X <= LListD_Fun(r, X Un LListD(r)) |] ==> M : LListD(r)"; +be LListD.coinduct 1; +be (subsetD RS CollectD) 1; +ba 1; +val LListD_coinduct = result(); + +goalw LList.thy [LListD_Fun_def,NIL_def] " : LListD_Fun(r,s)"; +by (fast_tac set_cs 1); +val LListD_Fun_NIL_I = result(); + +goalw LList.thy [LListD_Fun_def,CONS_def] + "!!x. [| x:A; :s |] ==> : LListD_Fun(diag(A),s)"; +by (fast_tac univ_cs 1); +val LListD_Fun_CONS_I = result(); + +(*Utilise the "strong" part, i.e. gfp(f)*) +goalw LList.thy (LListD.defs @ [LListD_Fun_def]) + "!!M N. M: LListD(r) ==> M : LListD_Fun(r, X Un LListD(r))"; +by (etac (LListD.mono RS gfp_fun_UnI2) 1); +val LListD_Fun_LListD_I = result(); + + +(*This converse inclusion helps to strengthen llist_equalityI*) +goal LList.thy "diag(llist(A)) <= LListD(diag(A))"; by (rtac subsetI 1); -by (etac diagE 1); -by (etac ssubst 1); -by (etac (LList_unfold RS equalityD1 RS subsetD RS usumE) 1); -by (rewtac LListD_Fun_def); -by (ALLGOALS (fast_tac univ_cs)); +by (etac LListD_coinduct 1); +by (rtac subsetI 1); +by (eresolve_tac [diagE] 1); +by (eresolve_tac [ssubst] 1); +by (eresolve_tac [llist.elim] 1); +by (ALLGOALS + (asm_simp_tac (llist_ss addsimps [diagI, LListD_Fun_NIL_I, + LListD_Fun_CONS_I]))); val diag_subset_LListD = result(); -goal LList.thy "LListD(diag(A)) = diag(LList(A))"; +goal LList.thy "LListD(diag(A)) = diag(llist(A))"; by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, diag_subset_LListD] 1)); val LListD_eq_diag = result(); +goal LList.thy + "!!M N. M: llist(A) ==> : LListD_Fun(diag(A), X Un diag(llist(A)))"; +by (rtac (LListD_eq_diag RS subst) 1); +br LListD_Fun_LListD_I 1; +by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag, diagI]) 1); +val LListD_Fun_diag_I = result(); + + (** To show two LLists are equal, exhibit a bisimulation! [also admits true equality] Replace "A" by some particular set, like {x.True}??? *) goal LList.thy - "!!r. [| : r; r <= LListD_Fun(diag(A), r Un diag(LList(A))) \ + "!!r. [| : r; r <= LListD_Fun(diag(A), r Un diag(llist(A))) \ \ |] ==> M=N"; -by (rtac (rewrite_rule [LListD_def] - (LListD_subset_diag RS subsetD RS diagE)) 1); -by (etac (LListD_Fun_mono RS coinduct) 1); -by (etac (rewrite_rule [LListD_def] LListD_eq_diag RS ssubst) 1); -by (safe_tac univ_cs); -val LList_equalityI = result(); - -(** Rules to prove the 2nd premise of LList_equalityI **) - -goalw LList.thy [LListD_Fun_def,NIL_def] " : LListD_Fun(r,s)"; -by (rtac (singletonI RS diagI RS dsum_In0I) 1); -val LListD_Fun_NIL_I = result(); - -val prems = goalw LList.thy [LListD_Fun_def,CONS_def] - "[| x:A; :s |] ==> : LListD_Fun(diag(A),s)"; -by (rtac (dprodI RS dsum_In1I) 1); -by (REPEAT (resolve_tac (diagI::prems) 1)); -val LListD_Fun_CONS_I = result(); - -(*Utilise the "strong" part, i.e. gfp(f)*) -goal LList.thy - "!!M N. M: LList(A) ==> : LListD_Fun(diag(A), X Un diag(LList(A)))"; -br (rewrite_rule [LListD_def] LListD_eq_diag RS subst) 1; -br (LListD_Fun_mono RS gfp_fun_UnI2) 1; -br (rewrite_rule [LListD_def] LListD_eq_diag RS ssubst) 1; -be diagI 1; -val LListD_Fun_diag_I = result(); +by (rtac (LListD_subset_diag RS subsetD RS diagE) 1); +by (etac LListD_coinduct 1); +by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag]) 1); +by (safe_tac prod_cs); +val llist_equalityI = result(); -(*** Finality of LList(A): Uniqueness of functions defined by corecursion ***) +(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***) (*abstract proof using a bisimulation*) val [prem1,prem2] = goal LList.thy @@ -259,7 +267,7 @@ by (rtac ext 1); (*next step avoids an unknown (and flexflex pair) in simplification*) by (res_inst_tac [("A", "{u.True}"), - ("r", "range(%u. )")] LList_equalityI 1); + ("r", "range(%u. )")] llist_equalityI 1); by (rtac rangeI 1); by (safe_tac set_cs); by (stac prem1 1); @@ -317,11 +325,11 @@ (*A typical use of co-induction to show membership in the gfp. The containing set is simply the singleton {Lconst(M)}. *) -goal LList.thy "!!M A. M:A ==> Lconst(M): LList(A)"; -by (rtac (singletonI RS LList_coinduct) 1); +goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)"; +by (rtac (singletonI RS llist_coinduct) 1); by (safe_tac set_cs); by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1); -by (REPEAT (ares_tac [List_Fun_CONS_I, singletonI, UnI1] 1)); +by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1)); val Lconst_type = result(); goal LList.thy "Lconst(M) = LList_corec(M, %x.Inr())"; @@ -338,39 +346,23 @@ val gfp_Lconst_eq_LList_corec = result(); -(** Introduction rules for LList constructors **) - -(* c : {Numb(0)} <+> A <*> LList(A) ==> c : LList(A) *) -val LListI = LList_unfold RS equalityD2 RS subsetD; - -(*This justifies the type definition: LList(A) is nonempty.*) -goalw LList.thy [NIL_def] "NIL: LList(A)"; -by (rtac (singletonI RS usum_In0I RS LListI) 1); -val NIL_LListI = result(); - -val prems = goalw LList.thy [CONS_def] - "[| M: A; N: LList(A) |] ==> CONS(M,N) : LList(A)"; -by (rtac (uprodI RS usum_In1I RS LListI) 1); -by (REPEAT (resolve_tac prems 1)); -val CONS_LListI = result(); - (*** Isomorphisms ***) -goal LList.thy "inj(Rep_LList)"; +goal LList.thy "inj(Rep_llist)"; by (rtac inj_inverseI 1); -by (rtac Rep_LList_inverse 1); -val inj_Rep_LList = result(); +by (rtac Rep_llist_inverse 1); +val inj_Rep_llist = result(); -goal LList.thy "inj_onto(Abs_LList,LList(range(Leaf)))"; +goal LList.thy "inj_onto(Abs_llist,llist(range(Leaf)))"; by (rtac inj_onto_inverseI 1); -by (etac Abs_LList_inverse 1); -val inj_onto_Abs_LList = result(); +by (etac Abs_llist_inverse 1); +val inj_onto_Abs_llist = result(); (** Distinctness of constructors **) goalw LList.thy [LNil_def,LCons_def] "~ LCons(x,xs) = LNil"; -by (rtac (CONS_not_NIL RS (inj_onto_Abs_LList RS inj_onto_contraD)) 1); -by (REPEAT (resolve_tac [rangeI, NIL_LListI, CONS_LListI, Rep_LList] 1)); +by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1); +by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1)); val LCons_not_LNil = result(); val LNil_not_LCons = standard (LCons_not_LNil RS not_sym); @@ -381,15 +373,15 @@ (** llist constructors **) goalw LList.thy [LNil_def] - "Rep_LList(LNil) = NIL"; -by (rtac (NIL_LListI RS Abs_LList_inverse) 1); -val Rep_LList_LNil = result(); + "Rep_llist(LNil) = NIL"; +by (rtac (llist.NIL_I RS Abs_llist_inverse) 1); +val Rep_llist_LNil = result(); goalw LList.thy [LCons_def] - "Rep_LList(LCons(x,l)) = CONS(Leaf(x),Rep_LList(l))"; -by (REPEAT (resolve_tac [CONS_LListI RS Abs_LList_inverse, - rangeI, Rep_LList] 1)); -val Rep_LList_LCons = result(); + "Rep_llist(LCons(x,l)) = CONS(Leaf(x),Rep_llist(l))"; +by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse, + rangeI, Rep_llist] 1)); +val Rep_llist_LCons = result(); (** Injectiveness of CONS and LCons **) @@ -401,49 +393,49 @@ (*For reasoning about abstract llist constructors*) -val LList_cs = set_cs addIs [Rep_LList, NIL_LListI, CONS_LListI] +val llist_cs = set_cs addIs [Rep_llist]@llist.intrs addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject] - addSDs [inj_onto_Abs_LList RS inj_ontoD, - inj_Rep_LList RS injD, Leaf_inject]; + addSDs [inj_onto_Abs_llist RS inj_ontoD, + inj_Rep_llist RS injD, Leaf_inject]; goalw LList.thy [LCons_def] "(LCons(x,xs)=LCons(y,ys)) = (x=y & xs=ys)"; -by (fast_tac LList_cs 1); +by (fast_tac llist_cs 1); val LCons_LCons_eq = result(); val LCons_inject = standard (LCons_LCons_eq RS iffD1 RS conjE); -val [major] = goal LList.thy "CONS(M,N): LList(A) ==> M: A & N: LList(A)"; -by (rtac (major RS LListE) 1); +val [major] = goal LList.thy "CONS(M,N): llist(A) ==> M: A & N: llist(A)"; +by (rtac (major RS llist.elim) 1); by (etac CONS_neq_NIL 1); -by (fast_tac LList_cs 1); +by (fast_tac llist_cs 1); val CONS_D = result(); -(****** Reasoning about LList(A) ******) +(****** Reasoning about llist(A) ******) (*Don't use llist_ss, as it does case splits!*) val List_case_ss = univ_ss addsimps [List_case_NIL, List_case_CONS]; (*A special case of list_equality for functions over lazy lists*) -val [MList,gMList,NILcase,CONScase] = goal LList.thy - "[| M: LList(A); g(NIL): LList(A); \ +val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy + "[| M: llist(A); g(NIL): llist(A); \ \ f(NIL)=g(NIL); \ -\ !!x l. [| x:A; l: LList(A) |] ==> \ +\ !!x l. [| x:A; l: llist(A) |] ==> \ \ : \ -\ LListD_Fun(diag(A), (%u.)``LList(A) Un \ -\ diag(LList(A))) \ +\ LListD_Fun(diag(A), (%u.)``llist(A) Un \ +\ diag(llist(A))) \ \ |] ==> f(M) = g(M)"; -by (rtac LList_equalityI 1); -br (MList RS imageI) 1; +by (rtac llist_equalityI 1); +br (Mlist RS imageI) 1; by (rtac subsetI 1); by (etac imageE 1); by (etac ssubst 1); -by (etac LListE 1); +by (etac llist.elim 1); by (etac ssubst 1); by (stac NILcase 1); -br (gMList RS LListD_Fun_diag_I) 1; +br (gMlist RS LListD_Fun_diag_I) 1; by (etac ssubst 1); by (REPEAT (ares_tac [CONScase] 1)); -val LList_fun_equalityI = result(); +val llist_fun_equalityI = result(); (*** The functional "Lmap" ***) @@ -460,17 +452,17 @@ (*Another type-checking proof by coinduction*) val [major,minor] = goal LList.thy - "[| M: LList(A); !!x. x:A ==> f(x):B |] ==> Lmap(f,M): LList(B)"; -by (rtac (major RS imageI RS LList_coinduct) 1); + "[| M: llist(A); !!x. x:A ==> f(x):B |] ==> Lmap(f,M): llist(B)"; +by (rtac (major RS imageI RS llist_coinduct) 1); by (safe_tac set_cs); -by (etac LListE 1); +by (etac llist.elim 1); by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); -by (REPEAT (ares_tac [List_Fun_NIL_I, List_Fun_CONS_I, +by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, minor, imageI, UnI1] 1)); val Lmap_type = result(); (*This type checking rule synthesises a sufficiently large set for f*) -val [major] = goal LList.thy "M: LList(A) ==> Lmap(f,M): LList(f``A)"; +val [major] = goal LList.thy "M: llist(A) ==> Lmap(f,M): llist(f``A)"; by (rtac (major RS Lmap_type) 1); by (etac imageI 1); val Lmap_type2 = result(); @@ -478,19 +470,19 @@ (** Two easy results about Lmap **) val [prem] = goalw LList.thy [o_def] - "M: LList(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))"; -by (rtac (prem RS imageI RS LList_equalityI) 1); + "M: llist(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))"; +by (rtac (prem RS imageI RS llist_equalityI) 1); by (safe_tac set_cs); -by (etac LListE 1); +by (etac llist.elim 1); by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1, rangeI RS LListD_Fun_CONS_I] 1)); val Lmap_compose = result(); -val [prem] = goal LList.thy "M: LList(A) ==> Lmap(%x.x, M) = M"; -by (rtac (prem RS imageI RS LList_equalityI) 1); +val [prem] = goal LList.thy "M: llist(A) ==> Lmap(%x.x, M) = M"; +by (rtac (prem RS imageI RS llist_equalityI) 1); by (safe_tac set_cs); -by (etac LListE 1); +by (etac llist.elim 1); by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1, rangeI RS LListD_Fun_CONS_I] 1)); @@ -517,17 +509,17 @@ val Lappend_CONS = result(); val Lappend_ss = - List_case_ss addsimps [NIL_LListI, Lappend_NIL_NIL, Lappend_NIL_CONS, + List_case_ss addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS, Lappend_CONS, LListD_Fun_CONS_I] |> add_eqI; -goal LList.thy "!!M. M: LList(A) ==> Lappend(NIL,M) = M"; -by (etac LList_fun_equalityI 1); +goal LList.thy "!!M. M: llist(A) ==> Lappend(NIL,M) = M"; +by (etac llist_fun_equalityI 1); by (ALLGOALS (asm_simp_tac Lappend_ss)); val Lappend_NIL = result(); -goal LList.thy "!!M. M: LList(A) ==> Lappend(M,NIL) = M"; -by (etac LList_fun_equalityI 1); +goal LList.thy "!!M. M: llist(A) ==> Lappend(M,NIL) = M"; +by (etac llist_fun_equalityI 1); by (ALLGOALS (asm_simp_tac Lappend_ss)); val Lappend_NIL2 = result(); @@ -535,62 +527,63 @@ (*weak co-induction: bisimulation and case analysis on both variables*) goal LList.thy - "!!M N. [| M: LList(A); N: LList(A) |] ==> Lappend(M,N): LList(A)"; + "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend(M,N): llist(A)"; by (res_inst_tac - [("X", "UN u:LList(A). UN v: LList(A). {Lappend(u,v)}")] LList_coinduct 1); + [("X", "UN u:llist(A). UN v: llist(A). {Lappend(u,v)}")] llist_coinduct 1); by (fast_tac set_cs 1); by (safe_tac set_cs); -by (eres_inst_tac [("L", "u")] LListE 1); -by (eres_inst_tac [("L", "v")] LListE 1); +by (eres_inst_tac [("a", "u")] llist.elim 1); +by (eres_inst_tac [("a", "v")] llist.elim 1); by (ALLGOALS (asm_simp_tac Lappend_ss THEN' - fast_tac (set_cs addSIs [NIL_LListI,List_Fun_NIL_I,List_Fun_CONS_I]) )); + fast_tac (set_cs addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I]))); val Lappend_type = result(); (*strong co-induction: bisimulation and case analysis on one variable*) goal LList.thy - "!!M N. [| M: LList(A); N: LList(A) |] ==> Lappend(M,N): LList(A)"; -by (res_inst_tac [("X", "(%u.Lappend(u,N))``LList(A)")] LList_coinduct 1); + "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend(M,N): llist(A)"; +by (res_inst_tac [("X", "(%u.Lappend(u,N))``llist(A)")] llist_coinduct 1); be imageI 1; br subsetI 1; be imageE 1; -by (eres_inst_tac [("L", "u")] LListE 1); -by (asm_simp_tac (Lappend_ss addsimps [Lappend_NIL, List_Fun_LList_I]) 1); +by (eres_inst_tac [("a", "u")] llist.elim 1); +by (asm_simp_tac (Lappend_ss addsimps [Lappend_NIL, list_Fun_llist_I]) 1); by (asm_simp_tac Lappend_ss 1); -by (fast_tac (set_cs addSIs [List_Fun_CONS_I]) 1); +by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1); val Lappend_type = result(); (**** Lazy lists as the type 'a llist -- strongly typed versions of above ****) (** llist_case: case analysis for 'a llist **) -val Rep_LList_simps = +val Rep_llist_simps = [List_case_NIL, List_case_CONS, - Abs_LList_inverse, Rep_LList_inverse, NIL_LListI, CONS_LListI, - Rep_LList, rangeI, inj_Leaf, Inv_f_f]; -val Rep_LList_ss = llist_ss addsimps Rep_LList_simps; + Abs_llist_inverse, Rep_llist_inverse, + Rep_llist, rangeI, inj_Leaf, Inv_f_f] + @ llist.intrs; +val Rep_llist_ss = llist_ss addsimps Rep_llist_simps; goalw LList.thy [llist_case_def,LNil_def] "llist_case(c, d, LNil) = c"; -by (simp_tac Rep_LList_ss 1); +by (simp_tac Rep_llist_ss 1); val llist_case_LNil = result(); goalw LList.thy [llist_case_def,LCons_def] "llist_case(c, d, LCons(M,N)) = d(M,N)"; -by (simp_tac Rep_LList_ss 1); +by (simp_tac Rep_llist_ss 1); val llist_case_LCons = result(); (*Elimination is case analysis, not induction.*) val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def] "[| l=LNil ==> P; !!x l'. l=LCons(x,l') ==> P \ \ |] ==> P"; -by (rtac (Rep_LList RS LListE) 1); -by (rtac (inj_Rep_LList RS injD RS prem1) 1); -by (stac Rep_LList_LNil 1); +by (rtac (Rep_llist RS llist.elim) 1); +by (rtac (inj_Rep_llist RS injD RS prem1) 1); +by (stac Rep_llist_LNil 1); by (assume_tac 1); by (etac rangeE 1); -by (rtac (inj_Rep_LList RS injD RS prem2) 1); -by (asm_simp_tac (HOL_ss addsimps [Rep_LList_LCons]) 1); -by (etac (Abs_LList_inverse RS ssubst) 1); +by (rtac (inj_Rep_llist RS injD RS prem2) 1); +by (asm_simp_tac (HOL_ss addsimps [Rep_llist_LCons]) 1); +by (etac (Abs_llist_inverse RS ssubst) 1); by (rtac refl 1); val llistE = result(); @@ -601,11 +594,11 @@ \ split(%z w. LCons(z, llist_corec(w,f))), f(a))"; by (stac LList_corec 1); by (res_inst_tac [("s","f(a)")] sumE 1); -by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_LList_inverse]) 1); +by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1); by (res_inst_tac [("p","y")] PairE 1); -by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_LList_inverse]) 1); +by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1); (*FIXME: correct case splits usd to be found automatically: -by (ASM_SIMP_TAC(llist_ss addsimps [LList_corec_type2,Abs_LList_inverse]) 1);*) +by (ASM_SIMP_TAC(llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1);*) val llist_corec = result(); (*definitional version of same*) @@ -620,53 +613,53 @@ (*** Deriving llist_equalityI -- llist equality is a bisimulation ***) -val prems = goalw LList.thy [LListD_Fun_def] - "r <= Sigma(LList(A), %x.LList(A)) ==> \ -\ LListD_Fun(diag(A),r) <= Sigma(LList(A), %x.LList(A))"; -by (stac LList_unfold 1); -by (cut_facts_tac prems 1); +goalw LList.thy [LListD_Fun_def] + "!!r A. r <= Sigma(llist(A), %x.llist(A)) ==> \ +\ LListD_Fun(diag(A),r) <= Sigma(llist(A), %x.llist(A))"; +by (stac llist_unfold 1); +by (simp_tac (HOL_ss addsimps [NIL_def, CONS_def]) 1); by (fast_tac univ_cs 1); -val LListD_Fun_subset_Sigma_LList = result(); +val LListD_Fun_subset_Sigma_llist = result(); goal LList.thy - "prod_fun(Rep_LList,Rep_LList) `` r <= \ -\ Sigma(LList(range(Leaf)), %x.LList(range(Leaf)))"; -by (fast_tac (prod_cs addIs [Rep_LList]) 1); -val subset_Sigma_LList = result(); + "prod_fun(Rep_llist,Rep_llist) `` r <= \ +\ Sigma(llist(range(Leaf)), %x.llist(range(Leaf)))"; +by (fast_tac (prod_cs addIs [Rep_llist]) 1); +val subset_Sigma_llist = result(); val [prem] = goal LList.thy - "r <= Sigma(LList(range(Leaf)), %x.LList(range(Leaf))) ==> \ -\ prod_fun(Rep_LList o Abs_LList, Rep_LList o Abs_LList) `` r <= r"; + "r <= Sigma(llist(range(Leaf)), %x.llist(range(Leaf))) ==> \ +\ prod_fun(Rep_llist o Abs_llist, Rep_llist o Abs_llist) `` r <= r"; by (safe_tac prod_cs); by (rtac (prem RS subsetD RS SigmaE2) 1); by (assume_tac 1); -by (asm_simp_tac (HOL_ss addsimps [o_def,prod_fun,Abs_LList_inverse]) 1); +by (asm_simp_tac (HOL_ss addsimps [o_def,prod_fun,Abs_llist_inverse]) 1); val prod_fun_lemma = result(); goal LList.thy - "prod_fun(Rep_LList, Rep_LList) `` range(%x. ) = \ -\ diag(LList(range(Leaf)))"; + "prod_fun(Rep_llist, Rep_llist) `` range(%x. ) = \ +\ diag(llist(range(Leaf)))"; br equalityI 1; -by (fast_tac (univ_cs addIs [Rep_LList]) 1); -by (fast_tac (univ_cs addSEs [Abs_LList_inverse RS subst]) 1); +by (fast_tac (univ_cs addIs [Rep_llist]) 1); +by (fast_tac (univ_cs addSEs [Abs_llist_inverse RS subst]) 1); val prod_fun_range_eq_diag = result(); (** To show two llists are equal, exhibit a bisimulation! [also admits true equality] **) val [prem1,prem2] = goalw LList.thy [llistD_Fun_def] "[| : r; r <= llistD_Fun(r Un range(%x.)) |] ==> l1=l2"; -by (rtac (inj_Rep_LList RS injD) 1); -by (res_inst_tac [("r", "prod_fun(Rep_LList,Rep_LList)``r"), +by (rtac (inj_Rep_llist RS injD) 1); +by (res_inst_tac [("r", "prod_fun(Rep_llist,Rep_llist)``r"), ("A", "range(Leaf)")] - LList_equalityI 1); + llist_equalityI 1); by (rtac (prem1 RS prod_fun_imageI) 1); by (rtac (prem2 RS image_mono RS subset_trans) 1); by (rtac (image_compose RS subst) 1); by (rtac (prod_fun_compose RS subst) 1); by (rtac (image_Un RS ssubst) 1); by (stac prod_fun_range_eq_diag 1); -by (rtac (LListD_Fun_subset_Sigma_LList RS prod_fun_lemma) 1); -by (rtac (subset_Sigma_LList RS Un_least) 1); +by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1); +by (rtac (subset_Sigma_llist RS Un_least) 1); by (rtac diag_subset_Sigma 1); val llist_equalityI = result(); @@ -684,11 +677,11 @@ (*Utilise the "strong" part, i.e. gfp(f)*) goalw LList.thy [llistD_Fun_def] "!!l. : llistD_Fun(r Un range(%x.))"; -br (Rep_LList_inverse RS subst) 1; +br (Rep_llist_inverse RS subst) 1; br prod_fun_imageI 1; by (rtac (image_Un RS ssubst) 1); by (stac prod_fun_range_eq_diag 1); -br (Rep_LList RS LListD_Fun_diag_I) 1; +br (Rep_llist RS LListD_Fun_diag_I) 1; val llistD_Fun_range_I = result(); (*A special case of list_equality for functions over lazy lists*)