Renamed sum_case to basic_sum_case and removed translations for sum_case
to avoid conflicts with the constant sum_case introduced in Datatype.thy.
--- a/src/HOL/Sum.ML Wed Aug 18 16:05:27 1999 +0200
+++ b/src/HOL/Sum.ML Wed Aug 18 16:11:14 1999 +0200
@@ -116,11 +116,11 @@
(** sum_case -- the selection operator for sums **)
-Goalw [sum_case_def] "sum_case f g (Inl x) = f(x)";
+Goalw [sum_case_def] "basic_sum_case f g (Inl x) = f(x)";
by (Blast_tac 1);
qed "sum_case_Inl";
-Goalw [sum_case_def] "sum_case f g (Inr x) = g(x)";
+Goalw [sum_case_def] "basic_sum_case f g (Inr x) = g(x)";
by (Blast_tac 1);
qed "sum_case_Inr";
@@ -143,31 +143,31 @@
by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
qed "sum_induct";
-Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
+Goal "basic_sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
by (EVERY1 [res_inst_tac [("s","s")] sumE,
etac ssubst, rtac sum_case_Inl,
etac ssubst, rtac sum_case_Inr]);
qed "surjective_sum";
-Goal "R(sum_case f g s) = \
+Goal "R(basic_sum_case f g s) = \
\ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
by (res_inst_tac [("s","s")] sumE 1);
by Auto_tac;
qed "split_sum_case";
-Goal "P (sum_case f g s) = \
+Goal "P (basic_sum_case f g s) = \
\ (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
by (stac split_sum_case 1);
by (Blast_tac 1);
qed "split_sum_case_asm";
(*Prevents simplification of f and g: much faster*)
-Goal "s=t ==> sum_case f g s = sum_case f g t";
+Goal "s=t ==> basic_sum_case f g s = basic_sum_case f g t";
by (etac arg_cong 1);
qed "sum_case_weak_cong";
val [p1,p2] = Goal
- "[| sum_case f1 f2 = sum_case g1 g2; \
+ "[| basic_sum_case f1 f2 = basic_sum_case g1 g2; \
\ [| f1 = g1; f2 = g2 |] ==> P |] \
\ ==> P";
by (rtac p2 1);
--- a/src/HOL/Sum.thy Wed Aug 18 16:05:27 1999 +0200
+++ b/src/HOL/Sum.thy Wed Aug 18 16:11:14 1999 +0200
@@ -27,23 +27,20 @@
(* abstract constants and syntax *)
consts
- Inl :: "'a => 'a + 'b"
- Inr :: "'b => 'a + 'b"
- sum_case :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c"
+ Inl :: "'a => 'a + 'b"
+ Inr :: "'b => 'a + 'b"
+ basic_sum_case :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c"
(*disjoint sum for sets; the operator + is overloaded with wrong type!*)
Plus :: "['a set, 'b set] => ('a + 'b) set" (infixr 65)
Part :: ['a set, 'b => 'a] => 'a set
-translations
- "case p of Inl x => a | Inr y => b" == "sum_case (%x. a) (%y. b) p"
-
local
defs
Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
- sum_case_def "sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x))
+ sum_case_def "basic_sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x))
& (!y. p=Inr(y) --> z=g(y))"
sum_def "A Plus B == (Inl``A) Un (Inr``B)"