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]);