# HG changeset patch
# User nipkow
# Date 759603207 -3600
# Node ID 7ef6ba42914bb15c5631224b0980f392ffe8dd46
# Parent  65a546c2b8ed20981cd71840fff42f3ed9e8d7f7
sum: renamed case to sum_case
hol: added general case-of syntax

diff -r 65a546c2b8ed -r 7ef6ba42914b HOL.thy
--- a/HOL.thy	Mon Jan 24 16:03:03 1994 +0100
+++ b/HOL.thy	Wed Jan 26 17:53:27 1994 +0100
@@ -20,6 +20,7 @@
 types
   bool 0
   letbinds, letbind 0
+  case_syn,cases_syn 0
 
 arities
   fun :: (term, term) term
@@ -49,6 +50,13 @@
   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   "_Let"        :: "[letbinds, 'a] => 'a"            ("(let (_)/ in (_))" 10)
 
+  (* Case expressions *)
+
+  "@case"            :: "['a, cases_syn] => 'b"		("(case _ of/ _)" 10)
+  "@case1"           :: "['a, 'b] => case_syn"		("(2_ =>/ _)" 10)
+  ""                 :: "case_syn => cases_syn"		("_")
+  "@case2"           :: "[case_syn,cases_syn] => cases_syn"	("_/ | _")
+
   (* Alternative Quantifiers *)
 
   "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
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();
diff -r 65a546c2b8ed -r 7ef6ba42914b LList.thy
--- a/LList.thy	Mon Jan 24 16:03:03 1994 +0100
+++ b/LList.thy	Wed Jan 26 17:53:27 1994 +0100
@@ -75,7 +75,7 @@
   LList_corec_fun_def
     "LList_corec_fun(k,f) == \
 \     nat_rec(k, %x. {}, 			\
-\	        %j r x. case(f(x), %u.NIL, 	\
+\	        %j r x. sum_case(f(x), %u.NIL, 	\
 \			   %v. split(v, %z w. CONS(z, r(w)))))"
 
   LList_corec_def
@@ -83,7 +83,7 @@
 
   llist_corec_def
    "llist_corec(a,f) == \
-\       Abs_LList(LList_corec(a, %z.case(f(z), %x.Inl(x), \
+\       Abs_LList(LList_corec(a, %z.sum_case(f(z), %x.Inl(x), \
 \                                    %y.split(y, %v w. Inr(<Leaf(v), w>)))))"
 
   llistD_Fun_def
diff -r 65a546c2b8ed -r 7ef6ba42914b Sum.ML
--- a/Sum.ML	Mon Jan 24 16:03:03 1994 +0100
+++ b/Sum.ML	Wed Jan 26 17:53:27 1994 +0100
@@ -85,17 +85,17 @@
 br refl 1;
 val Inr_inj = result();
 
-(** case -- the selection operator for sums **)
+(** sum_case -- the selection operator for sums **)
 
-goalw Sum.thy [case_def] "case(Inl(x), f, g) = f(x)";
+goalw Sum.thy [sum_case_def] "sum_case(Inl(x), f, g) = f(x)";
 by (fast_tac (set_cs addIs [select_equality] 
 		     addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
-val case_Inl = result();
+val sum_case_Inl = result();
 
-goalw Sum.thy [case_def] "case(Inr(x), f, g) = g(x)";
+goalw Sum.thy [sum_case_def] "sum_case(Inr(x), f, g) = g(x)";
 by (fast_tac (set_cs addIs [select_equality] 
 		     addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
-val case_Inr = result();
+val sum_case_Inr = result();
 
 (** Exhaustion rule for sums -- a degenerate form of induction **)
 
@@ -109,26 +109,26 @@
 		    rtac (Rep_Sum_inverse RS sym)]));
 val sumE = result();
 
-goal Sum.thy "case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)";
+goal Sum.thy "sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)";
 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
-	    etac ssubst, rtac case_Inl,
-	    etac ssubst, rtac case_Inr]);
+	    etac ssubst, rtac sum_case_Inl,
+	    etac ssubst, rtac sum_case_Inr]);
 val surjective_sum = result();
 
-goal Sum.thy "R(case(s,f,g)) = \
+goal Sum.thy "R(sum_case(s,f,g)) = \
 \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
 by (rtac sumE 1);
 by (etac ssubst 1);
-by (stac case_Inl 1);
+by (stac sum_case_Inl 1);
 by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
 by (etac ssubst 1);
-by (stac case_Inr 1);
+by (stac sum_case_Inr 1);
 by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
-val expand_case = result();
+val expand_sum_case = result();
 
-val sum_ss = pair_ss addsimps [case_Inl, case_Inr];
+val sum_ss = pair_ss addsimps [sum_case_Inl, sum_case_Inr];
 
 (*Prevents simplification of f and g: much faster*)
-val case_weak_cong = prove_goal Sum.thy
-  "s=t ==> case(s,f,g) = case(t,f,g)"
+val sum_case_weak_cong = prove_goal Sum.thy
+  "s=t ==> sum_case(s,f,g) = sum_case(t,f,g)"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
diff -r 65a546c2b8ed -r 7ef6ba42914b Sum.thy
--- a/Sum.thy	Mon Jan 24 16:03:03 1994 +0100
+++ b/Sum.thy	Wed Jan 26 17:53:27 1994 +0100
@@ -17,7 +17,7 @@
    Abs_Sum	:: "(['a,'b,bool] => bool) => 'a+'b"
    Inl		:: "'a => 'a+'b"
    Inr		:: "'b => 'a+'b"
-   case		:: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+   sum_case	:: "['a+'b, 'a=>'c,'b=>'c] =>'c"
 rules
   Inl_Rep_def	"Inl_Rep == (%a. %x y p. x=a & p)"
   Inr_Rep_def	"Inr_Rep == (%b. %x y p. y=b & ~p)"
@@ -29,6 +29,6 @@
     (*defining the abstract constants*)
   Inl_def  		"Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def 		"Inr == (%b. Abs_Sum(Inr_Rep(b)))"
-  case_def	"case == (%p f g. @z.  (!x. p=Inl(x) --> z=f(x))\
-\                                    & (!y. p=Inr(y) --> z=g(y)))"
+  sum_case_def	"sum_case == (%p f g. @z.  (!x. p=Inl(x) --> z=f(x))\
+\                                        & (!y. p=Inr(y) --> z=g(y)))"
 end
diff -r 65a546c2b8ed -r 7ef6ba42914b hol.thy
--- a/hol.thy	Mon Jan 24 16:03:03 1994 +0100
+++ b/hol.thy	Wed Jan 26 17:53:27 1994 +0100
@@ -20,6 +20,7 @@
 types
   bool 0
   letbinds, letbind 0
+  case_syn,cases_syn 0
 
 arities
   fun :: (term, term) term
@@ -49,6 +50,13 @@
   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   "_Let"        :: "[letbinds, 'a] => 'a"            ("(let (_)/ in (_))" 10)
 
+  (* Case expressions *)
+
+  "@case"            :: "['a, cases_syn] => 'b"		("(case _ of/ _)" 10)
+  "@case1"           :: "['a, 'b] => case_syn"		("(2_ =>/ _)" 10)
+  ""                 :: "case_syn => cases_syn"		("_")
+  "@case2"           :: "[case_syn,cases_syn] => cases_syn"	("_/ | _")
+
   (* Alternative Quantifiers *)
 
   "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
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();
diff -r 65a546c2b8ed -r 7ef6ba42914b llist.thy
--- a/llist.thy	Mon Jan 24 16:03:03 1994 +0100
+++ b/llist.thy	Wed Jan 26 17:53:27 1994 +0100
@@ -75,7 +75,7 @@
   LList_corec_fun_def
     "LList_corec_fun(k,f) == \
 \     nat_rec(k, %x. {}, 			\
-\	        %j r x. case(f(x), %u.NIL, 	\
+\	        %j r x. sum_case(f(x), %u.NIL, 	\
 \			   %v. split(v, %z w. CONS(z, r(w)))))"
 
   LList_corec_def
@@ -83,7 +83,7 @@
 
   llist_corec_def
    "llist_corec(a,f) == \
-\       Abs_LList(LList_corec(a, %z.case(f(z), %x.Inl(x), \
+\       Abs_LList(LList_corec(a, %z.sum_case(f(z), %x.Inl(x), \
 \                                    %y.split(y, %v w. Inr(<Leaf(v), w>)))))"
 
   llistD_Fun_def
diff -r 65a546c2b8ed -r 7ef6ba42914b sum.ML
--- a/sum.ML	Mon Jan 24 16:03:03 1994 +0100
+++ b/sum.ML	Wed Jan 26 17:53:27 1994 +0100
@@ -85,17 +85,17 @@
 br refl 1;
 val Inr_inj = result();
 
-(** case -- the selection operator for sums **)
+(** sum_case -- the selection operator for sums **)
 
-goalw Sum.thy [case_def] "case(Inl(x), f, g) = f(x)";
+goalw Sum.thy [sum_case_def] "sum_case(Inl(x), f, g) = f(x)";
 by (fast_tac (set_cs addIs [select_equality] 
 		     addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
-val case_Inl = result();
+val sum_case_Inl = result();
 
-goalw Sum.thy [case_def] "case(Inr(x), f, g) = g(x)";
+goalw Sum.thy [sum_case_def] "sum_case(Inr(x), f, g) = g(x)";
 by (fast_tac (set_cs addIs [select_equality] 
 		     addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
-val case_Inr = result();
+val sum_case_Inr = result();
 
 (** Exhaustion rule for sums -- a degenerate form of induction **)
 
@@ -109,26 +109,26 @@
 		    rtac (Rep_Sum_inverse RS sym)]));
 val sumE = result();
 
-goal Sum.thy "case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)";
+goal Sum.thy "sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)";
 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
-	    etac ssubst, rtac case_Inl,
-	    etac ssubst, rtac case_Inr]);
+	    etac ssubst, rtac sum_case_Inl,
+	    etac ssubst, rtac sum_case_Inr]);
 val surjective_sum = result();
 
-goal Sum.thy "R(case(s,f,g)) = \
+goal Sum.thy "R(sum_case(s,f,g)) = \
 \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
 by (rtac sumE 1);
 by (etac ssubst 1);
-by (stac case_Inl 1);
+by (stac sum_case_Inl 1);
 by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
 by (etac ssubst 1);
-by (stac case_Inr 1);
+by (stac sum_case_Inr 1);
 by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
-val expand_case = result();
+val expand_sum_case = result();
 
-val sum_ss = pair_ss addsimps [case_Inl, case_Inr];
+val sum_ss = pair_ss addsimps [sum_case_Inl, sum_case_Inr];
 
 (*Prevents simplification of f and g: much faster*)
-val case_weak_cong = prove_goal Sum.thy
-  "s=t ==> case(s,f,g) = case(t,f,g)"
+val sum_case_weak_cong = prove_goal Sum.thy
+  "s=t ==> sum_case(s,f,g) = sum_case(t,f,g)"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
diff -r 65a546c2b8ed -r 7ef6ba42914b sum.thy
--- a/sum.thy	Mon Jan 24 16:03:03 1994 +0100
+++ b/sum.thy	Wed Jan 26 17:53:27 1994 +0100
@@ -17,7 +17,7 @@
    Abs_Sum	:: "(['a,'b,bool] => bool) => 'a+'b"
    Inl		:: "'a => 'a+'b"
    Inr		:: "'b => 'a+'b"
-   case		:: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+   sum_case	:: "['a+'b, 'a=>'c,'b=>'c] =>'c"
 rules
   Inl_Rep_def	"Inl_Rep == (%a. %x y p. x=a & p)"
   Inr_Rep_def	"Inr_Rep == (%b. %x y p. y=b & ~p)"
@@ -29,6 +29,6 @@
     (*defining the abstract constants*)
   Inl_def  		"Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def 		"Inr == (%b. Abs_Sum(Inr_Rep(b)))"
-  case_def	"case == (%p f g. @z.  (!x. p=Inl(x) --> z=f(x))\
-\                                    & (!y. p=Inr(y) --> z=g(y)))"
+  sum_case_def	"sum_case == (%p f g. @z.  (!x. p=Inl(x) --> z=f(x))\
+\                                        & (!y. p=Inr(y) --> z=g(y)))"
 end