--- a/LList.ML Tue Aug 16 09:57:51 1994 +0200
+++ b/LList.ML Thu Aug 18 11:30:27 1994 +0200
@@ -14,10 +14,14 @@
(** Simplification **)
-val llist_simps = [sum_case_Inl, sum_case_Inr];
-val llist_ss = univ_ss delsimps [Pair_eq]
- addcongs [split_weak_cong, sum_case_weak_cong]
- setloop (split_tac [expand_split, expand_sum_case]);
+val llist_ss = univ_ss addcongs [split_weak_cong, sum_case_weak_cong]
+ setloop split_tac [expand_split, expand_sum_case];
+
+(*For adding _eqI rules to a simpset; we must remove Pair_eq because
+ it may turn an instance of reflexivity into a conjunction!*)
+fun add_eqI ss = ss addsimps [range_eqI, image_eqI]
+ delsimps [Pair_eq];
+
(** the llist functional **)
@@ -76,14 +80,16 @@
by (simp_tac (univ_ss addsimps [In1_UN1, Scons_UN1_y]) 1);
val CONS_UN1 = result();
+(*UNUSED; obsolete?
goal Prod.thy "split(p, %x y.UN z.f(x,y,z)) = (UN z. split(p, %x y.f(x,y,z)))";
-by (simp_tac (pair_ss setloop (split_tac [expand_split])) 1);
+by (simp_tac (prod_ss setloop (split_tac [expand_split])) 1);
val split_UN1 = result();
-(* Does not seem to be used
+
goal Sum.thy "sum_case(s,f,%y.UN z.g(y,z)) = (UN z.sum_case(s,f,%y. g(y,z)))";
by (simp_tac (sum_ss setloop (split_tac [expand_sum_case])) 1);
val sum_case2_UN1 = result();
*)
+
val prems = goalw LList.thy [CONS_def]
"[| M<=M'; N<=N' |] ==> CONS(M,N) <= CONS(M',N')";
by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
@@ -96,8 +102,8 @@
(** The directions of the equality are proved separately **)
goalw LList.thy [LList_corec_def]
- "LList_corec(a,f) <= sum_case(f(a), %u.NIL, \
-\ %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
+ "LList_corec(a,f) <= sum_case(%u.NIL, \
+\ split(%z w. CONS(z, LList_corec(w,f))), f(a))";
by (rtac UN1_least 1);
by (res_inst_tac [("n","k")] natE 1);
by (ALLGOALS (asm_simp_tac corec_fun_ss));
@@ -105,7 +111,7 @@
val LList_corec_subset1 = result();
goalw LList.thy [LList_corec_def]
- "sum_case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, LList_corec(w,f)))) <= \
+ "sum_case(%u.NIL, split(%z w. CONS(z, LList_corec(w,f))), f(a)) <= \
\ LList_corec(a,f)";
by (simp_tac (corec_fun_ss addsimps [CONS_UN1]) 1);
by (safe_tac set_cs);
@@ -115,8 +121,8 @@
(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
goal LList.thy
- "LList_corec(a,f) = sum_case(f(a), %u. NIL, \
-\ %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
+ "LList_corec(a,f) = sum_case(%u. NIL, \
+\ split(%z w. CONS(z, LList_corec(w,f))), f(a))";
by (REPEAT (resolve_tac [equalityI, LList_corec_subset1,
LList_corec_subset2] 1));
val LList_corec = result();
@@ -124,7 +130,7 @@
(*definitional version of same*)
val [rew] = goal LList.thy
"[| !!x. h(x) == LList_corec(x,f) |] ==> \
-\ h(a) = sum_case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, h(w))))";
+\ h(a) = sum_case(%u.NIL, split(%z w. CONS(z, h(w))), f(a))";
by (rewtac rew);
by (rtac LList_corec 1);
val def_LList_corec = result();
@@ -136,29 +142,20 @@
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, range_eqI]) 1);
-(* 6.7 vs 3.4 !!!
-by (ASM_SIMP_TAC (llist_ss addsimps [List_Fun_NIL_I,List_Fun_CONS_I,
- CollectI, rangeI]) 1);
-*)
+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(f(z),Inl,%x.split(x,%v w.Inr(<Leaf(v),w>)))) : \
+ "LList_corec(a, %z.sum_case(Inl, split(%v w.Inr(<Leaf(v),w>)), f(z))) : \
\ 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);
-(*nested "sum_case"; requires an explicit split*)
-by (res_inst_tac [("s", "f(xa)")] sumE 1);
-by (asm_simp_tac (univ_ss addsimps [List_Fun_NIL_I]) 1);
-by (asm_simp_tac (univ_ss addsimps [List_Fun_CONS_I, range_eqI]
- setloop (split_tac [expand_split])) 1);
-(* FIXME: can the selection of the case split be automated?
-by (ASM_SIMP_TAC (llist_ss addsimps [List_Fun_CONS_I, rangeI]) 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);
val LList_corec_type2 = result();
(**** LList equality as a gfp; the bisimulation principle ****)
@@ -209,8 +206,7 @@
by (etac ssubst 1);
by (etac (LList_unfold RS equalityD1 RS subsetD RS usumE) 1);
by (rewtac LListD_Fun_def);
-by (ALLGOALS (fast_tac (set_cs addIs [diagI,dsum_In0I,dsum_In1I,dprodI]
- addSEs [uprodE])));
+by (ALLGOALS (fast_tac univ_cs));
val diag_subset_LListD = result();
goal LList.thy "LListD(diag(A)) = diag(LList(A))";
@@ -228,7 +224,7 @@
(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 (set_cs addSEs [Pair_inject]));
+by (safe_tac univ_cs);
val LList_equalityI = result();
(** Rules to prove the 2nd premise of LList_equalityI **)
@@ -257,8 +253,8 @@
(*abstract proof using a bisimulation*)
val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h1(w)))); \
-\ !!x. h2(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h2(w)))) |]\
+ "[| !!x. h1(x) = sum_case(%u.NIL, split(%z w. CONS(z,h1(w))), f(x)); \
+\ !!x. h2(x) = sum_case(%u.NIL, split(%z w. CONS(z,h2(w))), f(x)) |]\
\ ==> h1=h2";
by (rtac ext 1);
(*next step avoids an unknown (and flexflex pair) in simplification*)
@@ -268,15 +264,13 @@
by (safe_tac set_cs);
by (stac prem1 1);
by (stac prem2 1);
-by (simp_tac (llist_ss addsimps [LListD_Fun_NIL_I, range_eqI,
- CollectI RS LListD_Fun_CONS_I]) 1);
-(* 9.5 vs 9.2/4.1/4.3
-by (ASM_SIMP_TAC (llist_ss addsimps [LListD_Fun_NIL_I, rangeI,
- CollectI RS LListD_Fun_CONS_I]) 1);*)
+by (simp_tac (llist_ss addsimps [LListD_Fun_NIL_I,
+ CollectI RS LListD_Fun_CONS_I]
+ |> add_eqI) 1);
val LList_corec_unique = result();
val [prem] = goal LList.thy
- "[| !!x. h(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h(w)))) |] \
+ "[| !!x. h(x) = sum_case(%u.NIL, split(%z w. CONS(z,h(w))), f(x)) |] \
\ ==> h = (%x.LList_corec(x,f))";
by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
val equals_LList_corec = result();
@@ -294,8 +288,8 @@
val ntrunc_CONS = result();
val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h1(w)))); \
-\ !!x. h2(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h2(w)))) |]\
+ "[| !!x. h1(x) = sum_case(%u.NIL, split(%z w. CONS(z,h1(w))), f(x)); \
+\ !!x. h2(x) = sum_case(%u.NIL, split(%z w. CONS(z,h2(w))), f(x)) |]\
\ ==> h1=h2";
by (rtac (ntrunc_equality RS ext) 1);
by (res_inst_tac [("x", "x")] spec 1);
@@ -426,8 +420,8 @@
(****** Reasoning about LList(A) ******)
-val List_case_simps = [List_case_NIL, List_case_CONS];
-val List_case_ss = llist_ss addsimps List_case_simps;
+(*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
@@ -507,30 +501,25 @@
goalw LList.thy [Lappend_def] "Lappend(NIL,NIL) = NIL";
by (rtac (LList_corec RS trans) 1);
-(* takes 2.4(3.4 w NORM) vs 0.9 w/o NORM terms *)
by (simp_tac List_case_ss 1);
-(*by (SIMP_TAC List_case_ss 1);*)
val Lappend_NIL_NIL = result();
goalw LList.thy [Lappend_def]
"Lappend(NIL,CONS(N,N')) = CONS(N, Lappend(NIL,N'))";
by (rtac (LList_corec RS trans) 1);
-(* takes 5(7 w NORM) vs 2.1 w/o NORM terms *)
by (simp_tac List_case_ss 1);
-(*by (SIMP_TAC List_case_ss 1);*)
val Lappend_NIL_CONS = result();
goalw LList.thy [Lappend_def]
"Lappend(CONS(M,M'), N) = CONS(M, Lappend(M',N))";
by (rtac (LList_corec RS trans) 1);
-(* takes 4.9(6.7) vs 2.2 w/o NORM terms *)
by (simp_tac List_case_ss 1);
-(*by (SIMP_TAC List_case_ss 1);*)
val Lappend_CONS = result();
-val Lappend_ss = List_case_ss addsimps
- [NIL_LListI, Lappend_NIL_NIL, Lappend_NIL_CONS,
- Lappend_CONS, image_eqI, LListD_Fun_CONS_I];
+val Lappend_ss =
+ List_case_ss addsimps [NIL_LListI, 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);
@@ -553,15 +542,9 @@
by (safe_tac set_cs);
by (eres_inst_tac [("L", "u")] LListE 1);
by (eres_inst_tac [("L", "v")] LListE 1);
-(* 7/12 vs 7.8/13.3/8.2/13.4 *)
by (ALLGOALS
(asm_simp_tac Lappend_ss THEN'
fast_tac (set_cs addSIs [NIL_LListI,List_Fun_NIL_I,List_Fun_CONS_I]) ));
-(*
-by (REPEAT
- (ASM_SIMP_TAC Lappend_ss 1 THEN
- fast_tac (set_cs addSIs [NIL_LListI,List_Fun_NIL_I,List_Fun_CONS_I])1));
-*)
val Lappend_type = result();
(*strong co-induction: bisimulation and case analysis on one variable*)
@@ -587,12 +570,12 @@
Rep_LList, rangeI, inj_Leaf, Inv_f_f];
val Rep_LList_ss = llist_ss addsimps Rep_LList_simps;
-goalw LList.thy [llist_case_def,LNil_def] "llist_case(LNil, c, d) = c";
+goalw LList.thy [llist_case_def,LNil_def] "llist_case(c, d, LNil) = c";
by (simp_tac Rep_LList_ss 1);
val llist_case_LNil = result();
goalw LList.thy [llist_case_def,LCons_def]
- "llist_case(LCons(M,N), c, d) = d(M,N)";
+ "llist_case(c, d, LCons(M,N)) = d(M,N)";
by (simp_tac Rep_LList_ss 1);
val llist_case_LCons = result();
@@ -614,8 +597,8 @@
(** llist_corec: corecursion for 'a llist **)
goalw LList.thy [llist_corec_def,LNil_def,LCons_def]
- "llist_corec(a,f) = sum_case(f(a), %u. LNil, \
-\ %v. split(v, %z w. LCons(z, llist_corec(w,f))))";
+ "llist_corec(a,f) = sum_case(%u. LNil, \
+\ 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);
@@ -628,7 +611,7 @@
(*definitional version of same*)
val [rew] = goal LList.thy
"[| !!x. h(x) == llist_corec(x,f) |] ==> \
-\ h(a) = sum_case(f(a), %u.LNil, %v. split(v, %z w. LCons(z, h(w))))";
+\ h(a) = sum_case(%u.LNil, split(%z w. LCons(z, h(w))), f(a))";
by (rewtac rew);
by (rtac llist_corec 1);
val def_llist_corec = result();
@@ -648,13 +631,13 @@
goal LList.thy
"prod_fun(Rep_LList,Rep_LList) `` r <= \
\ Sigma(LList(range(Leaf)), %x.LList(range(Leaf)))";
-by (fast_tac (set_cs addSEs [prod_fun_imageE] addIs [SigmaI, Rep_LList]) 1);
+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";
-by (safe_tac (set_cs addSEs [prod_fun_imageE]));
+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);
@@ -664,10 +647,8 @@
"prod_fun(Rep_LList, Rep_LList) `` range(%x. <x, x>) = \
\ diag(LList(range(Leaf)))";
br equalityI 1;
-by (fast_tac (set_cs addIs [diagI, Rep_LList]
- addSEs [prod_fun_imageE, Pair_inject]) 1);
-by (fast_tac (set_cs addIs [prod_fun_imageI, rangeI]
- addSEs [diagE, 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!
@@ -730,9 +711,10 @@
val llist_fun_equalityI = result();
(*simpset for llist bisimulations*)
-val llistD_simps = [llist_case_LNil, llist_case_LCons, range_eqI,
+val llistD_simps = [llist_case_LNil, llist_case_LCons,
llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-val llistD_ss = llist_ss addsimps llistD_simps;
+(*Don't use llist_ss, as it does case splits!*)
+val llistD_ss = univ_ss addsimps llistD_simps |> add_eqI;
(*** The functional "lmap" ***)
@@ -837,25 +819,24 @@
"lappend(LNil,LCons(l,l')) = LCons(l, lappend(LNil,l'))";
by (rtac (llist_corec RS trans) 1);
by (simp_tac llistD_ss 1);
-(* 3.3(5.7) vs 1.3 !by (SIMP_TAC llistD_ss 1);*)
val lappend_LNil_LCons = result();
goalw LList.thy [lappend_def]
"lappend(LCons(l,l'), N) = LCons(l, lappend(l',N))";
by (rtac (llist_corec RS trans) 1);
by (simp_tac llistD_ss 1);
-(* 5(5.5) vs 1.3 !by (SIMP_TAC llistD_ss 1);*)
val lappend_LCons = result();
goal LList.thy "lappend(LNil,l) = l";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (llistD_ss addsimps [lappend_LNil_LNil,
- lappend_LNil_LCons])));
+by (ALLGOALS
+ (simp_tac (llistD_ss addsimps [lappend_LNil_LNil, lappend_LNil_LCons])));
val lappend_LNil = result();
goal LList.thy "lappend(l,LNil) = l";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac(llistD_ss addsimps [lappend_LNil_LNil,lappend_LCons])));
+by (ALLGOALS
+ (simp_tac (llistD_ss addsimps [lappend_LNil_LNil, lappend_LCons])));
val lappend_LNil2 = result();
(*The infinite first argument blocks the second*)
--- a/LList.thy Tue Aug 16 09:57:51 1994 +0200
+++ b/LList.thy Thu Aug 18 11:30:27 1994 +0200
@@ -20,7 +20,7 @@
llistD_Fun_def
"llistD_Fun(r) == \
\ {<LNil,LNil>} Un \
-\ (UN x. (%z.split(z, %l1 l2.<LCons(x,l1),LCons(x,l2)>))``r)"
+\ (UN x. (split(%l1 l2.<LCons(x,l1),LCons(x,l2)>))``r)"
*)
LList = Gfp + List +
@@ -45,7 +45,7 @@
LNil :: "'a llist"
LCons :: "['a, 'a llist] => 'a llist"
- llist_case :: "['a llist, 'b, ['a, 'a llist]=>'b] => 'b"
+ llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
LList_corec_fun :: "[nat, 'a=>unit+('b node set * 'a), 'a] => 'b node set"
LList_corec :: "['a, 'a => unit + ('b node set * 'a)] => 'b node set"
@@ -74,22 +74,21 @@
LCons_def "LCons(x,xs) == Abs_LList(CONS(Leaf(x), Rep_LList(xs)))"
llist_case_def
- "llist_case(l,c,d) == \
-\ List_case(Rep_LList(l), c, %x y. d(Inv(Leaf,x), Abs_LList(y)))"
+ "llist_case(c,d,l) == \
+\ List_case(c, %x y. d(Inv(Leaf,x), Abs_LList(y)), Rep_LList(l))"
LList_corec_fun_def
"LList_corec_fun(k,f) == \
\ nat_rec(k, %x. {}, \
-\ %j r x. sum_case(f(x), %u.NIL, \
-\ %v. split(v, %z w. CONS(z, r(w)))))"
+\ %j r x. sum_case(%u.NIL, split(%z w. CONS(z, r(w))), f(x)))"
LList_corec_def
"LList_corec(a,f) == UN k. LList_corec_fun(k,f,a)"
llist_corec_def
"llist_corec(a,f) == \
-\ Abs_LList(LList_corec(a, %z.sum_case(f(z), %x.Inl(x), \
-\ %y.split(y, %v w. Inr(<Leaf(v), w>)))))"
+\ Abs_LList(LList_corec(a, %z.sum_case(%x.Inl(x), \
+\ split(%v w. Inr(<Leaf(v), w>)), f(z))))"
llistD_Fun_def
"llistD_Fun(r) == \
@@ -100,12 +99,10 @@
Lconst_def "Lconst(M) == lfp(%N. CONS(M, N))"
Lmap_def
- "Lmap(f,M) == \
-\ LList_corec(M, %M. List_case(M, Inl(Unity), %x M'. Inr(<f(x), M'>)))"
+ "Lmap(f,M) == LList_corec(M, List_case(Inl(Unity), %x M'. Inr(<f(x), M'>)))"
lmap_def
- "lmap(f,l) == \
-\ llist_corec(l, %l. llist_case(l, Inl(Unity), %y z. Inr(<f(y), z>)))"
+ "lmap(f,l) == llist_corec(l, llist_case(Inl(Unity), %y z. Inr(<f(y), z>)))"
iterates_def "iterates(f,a) == llist_corec(a, %x. Inr(<x, f(x)>))"
@@ -116,16 +113,13 @@
*)
Lappend_def
- "Lappend(M,N) == LList_corec(<M,N>, %p. split(p, \
-\ %M N. List_case(M, List_case(N, Inl(Unity), \
-\ %N1 N2. Inr(<N1, <NIL,N2>>)), \
-\ %M1 M2. Inr(<M1, <M2,N>>))))"
+ "Lappend(M,N) == LList_corec(<M,N>, \
+\ split(List_case(List_case(Inl(Unity), %N1 N2. Inr(<N1, <NIL,N2>>)), \
+\ %M1 M2 N. Inr(<M1, <M2,N>>))))"
lappend_def
- "lappend(l,n) == llist_corec(<l,n>, %p. split(p, \
-\ %l n. llist_case(l, llist_case(n, Inl(Unity), \
-\ %n1 n2. Inr(<n1, <LNil,n2>>)), \
-\ %l1 l2. Inr(<l1, <l2,n>>))))"
-
+ "lappend(l,n) == llist_corec(<l,n>, \
+\ split(llist_case(llist_case(Inl(Unity), %n1 n2. Inr(<n1, <LNil,n2>>)), \
+\ %l1 l2 n. Inr(<l1, <l2,n>>))))"
end