--- a/LList.ML Mon Jan 24 16:03:03 1994 +0100
+++ b/LList.ML Wed Jan 26 17:53:27 1994 +0100
@@ -14,11 +14,11 @@
(** Simplification **)
-val llist_simps = [case_Inl, case_Inr];
+val llist_simps = [sum_case_Inl, sum_case_Inr];
val llist_ss = univ_ss delsimps [Pair_eq]
addsimps llist_simps
- addcongs [split_weak_cong, case_weak_cong]
- setloop (split_tac [expand_split, expand_case]);
+ addcongs [split_weak_cong, sum_case_weak_cong]
+ setloop (split_tac [expand_split, expand_sum_case]);
(** the llist functional **)
@@ -80,11 +80,11 @@
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);
val split_UN1 = result();
-
-goal Sum.thy "case(s, f, %y. UN z.g(y,z)) = (UN z. case(s, f, %y. g(y,z)))";
-by (simp_tac (sum_ss setloop (split_tac [expand_case])) 1);
-val case2_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));
@@ -97,7 +97,7 @@
(** The directions of the equality are proved separately **)
goalw LList.thy [LList_corec_def]
- "LList_corec(a,f) <= case(f(a), %u.NIL, \
+ "LList_corec(a,f) <= sum_case(f(a), %u.NIL, \
\ %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
by (rtac UN1_least 1);
by (res_inst_tac [("n","k")] natE 1);
@@ -106,7 +106,7 @@
val LList_corec_subset1 = result();
goalw LList.thy [LList_corec_def]
- "case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, LList_corec(w,f)))) <= \
+ "sum_case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, LList_corec(w,f)))) <= \
\ LList_corec(a,f)";
by (simp_tac (corec_fun_ss addsimps [CONS_UN1]) 1);
by (safe_tac set_cs);
@@ -116,7 +116,7 @@
(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
goal LList.thy
- "LList_corec(a,f) = case(f(a), %u. NIL, \
+ "LList_corec(a,f) = sum_case(f(a), %u. NIL, \
\ %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
by (REPEAT (resolve_tac [equalityI, LList_corec_subset1,
LList_corec_subset2] 1));
@@ -125,7 +125,7 @@
(*definitional version of same*)
val [rew] = goal LList.thy
"[| !!x. h(x) == LList_corec(x,f) |] ==> \
-\ h(a) = case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, h(w))))";
+\ h(a) = sum_case(f(a), %u.NIL, %v. split(v, %z w. CONS(z, h(w))))";
by (rewtac rew);
by (rtac LList_corec 1);
val def_LList_corec = result();
@@ -147,13 +147,13 @@
(*Lemma for the proof of llist_corec*)
goal LList.thy
- "LList_corec(a, %z. case(f(z),Inl,%x. split(x,%v w. Inr(<Leaf(v),w>)))) : \
-\ LList(range(Leaf))";
+ "LList_corec(a, %z.sum_case(f(z),Inl,%x.split(x,%v w.Inr(<Leaf(v),w>)))) : \
+\ 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 "case"; requires an explicit split*)
+(*nested "sum_case"; requires an explicit split*)
by (res_inst_tac [("s", "f(xa)")] sumE 1);
by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_NIL_I])) 1);
by (asm_simp_tac (univ_ss addsimps (llist_simps@[List_Fun_CONS_I, range_eqI])
@@ -258,8 +258,8 @@
(*abstract proof using a bisimulation*)
val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h1(w)))); \
-\ !!x. h2(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h2(w)))) |] \
+ "[| !!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)))) |]\
\ ==> h1=h2";
by (rtac ext 1);
(*next step avoids an unknown (and flexflex pair) in simplification*)
@@ -277,7 +277,7 @@
val LList_corec_unique = result();
val [prem] = goal LList.thy
- "[| !!x. h(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h(w)))) |] \
+ "[| !!x. h(x) = sum_case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h(w)))) |] \
\ ==> h = (%x.LList_corec(x,f))";
by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
val equals_LList_corec = result();
@@ -295,8 +295,8 @@
val ntrunc_CONS = result();
val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h1(w)))); \
-\ !!x. h2(x) = case(f(x), %u.NIL, %v. split(v, %z w. CONS(z,h2(w)))) |] \
+ "[| !!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)))) |]\
\ ==> h1=h2";
by (rtac (ntrunc_equality RS ext) 1);
by (res_inst_tac [("x", "x")] spec 1);
@@ -304,7 +304,7 @@
by (rtac allI 1);
by (stac prem1 1);
by (stac prem2 1);
-by (simp_tac (sum_ss setloop (split_tac [expand_split,expand_case])) 1);
+by (simp_tac (sum_ss setloop (split_tac [expand_split,expand_sum_case])) 1);
by (strip_tac 1);
by (res_inst_tac [("n", "n")] natE 1);
by (res_inst_tac [("n", "xc")] natE 2);
@@ -616,7 +616,7 @@
(** llist_corec: corecursion for 'a llist **)
goalw LList.thy [llist_corec_def,LNil_def,LCons_def]
- "llist_corec(a,f) = case(f(a), %u. LNil, \
+ "llist_corec(a,f) = sum_case(f(a), %u. LNil, \
\ %v. split(v, %z w. LCons(z, llist_corec(w,f))))";
by (stac LList_corec 1);
by (res_inst_tac [("s","f(a)")] sumE 1);
@@ -630,7 +630,7 @@
(*definitional version of same*)
val [rew] = goal LList.thy
"[| !!x. h(x) == llist_corec(x,f) |] ==> \
-\ h(a) = case(f(a), %u.LNil, %v. split(v, %z w. LCons(z, h(w))))";
+\ h(a) = sum_case(f(a), %u.LNil, %v. split(v, %z w. LCons(z, h(w))))";
by (rewtac rew);
by (rtac llist_corec 1);
val def_llist_corec = result();