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