diff -r 65a546c2b8ed -r 7ef6ba42914b llist.ML
--- 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();