--- a/src/HOL/Sum_Type.thy Wed Nov 25 11:16:57 2009 +0100
+++ b/src/HOL/Sum_Type.thy Wed Nov 25 11:16:58 2009 +0100
@@ -7,7 +7,7 @@
header{*The Disjoint Sum of Two Types*}
theory Sum_Type
-imports Typedef Fun
+imports Typedef Inductive Fun
begin
text{*The representations of the two injections*}
@@ -191,6 +191,74 @@
lemma Part_Collect: "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"
by blast
+subsection {* Representing sums *}
+
+rep_datatype (sum) Inl Inr
+proof -
+ fix P
+ fix s :: "'a + 'b"
+ assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
+ then show "P s" by (auto intro: sumE [of s])
+qed simp_all
+
+lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
+ by (rule ext) (simp split: sum.split)
+
+lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
+ apply (rule_tac s = s in sumE)
+ apply (erule ssubst)
+ apply (rule sum.cases(1))
+ apply (erule ssubst)
+ apply (rule sum.cases(2))
+ done
+
+lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
+ -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
+ by simp
+
+lemma sum_case_inject:
+ "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
+proof -
+ assume a: "sum_case f1 f2 = sum_case g1 g2"
+ assume r: "f1 = g1 ==> f2 = g2 ==> P"
+ show P
+ apply (rule r)
+ apply (rule ext)
+ apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
+ apply (rule ext)
+ apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
+ done
+qed
+
+constdefs
+ Suml :: "('a => 'c) => 'a + 'b => 'c"
+ "Suml == (%f. sum_case f undefined)"
+
+ Sumr :: "('b => 'c) => 'a + 'b => 'c"
+ "Sumr == sum_case undefined"
+
+lemma [code]:
+ "Suml f (Inl x) = f x"
+ by (simp add: Suml_def)
+
+lemma [code]:
+ "Sumr f (Inr x) = f x"
+ by (simp add: Sumr_def)
+
+lemma Suml_inject: "Suml f = Suml g ==> f = g"
+ by (unfold Suml_def) (erule sum_case_inject)
+
+lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
+ by (unfold Sumr_def) (erule sum_case_inject)
+
+primrec Projl :: "'a + 'b => 'a"
+where Projl_Inl: "Projl (Inl x) = x"
+
+primrec Projr :: "'a + 'b => 'b"
+where Projr_Inr: "Projr (Inr x) = x"
+
+hide (open) const Suml Sumr Projl Projr
+
ML
{*
--- a/src/HOL/Tools/Function/sum_tree.ML Wed Nov 25 11:16:57 2009 +0100
+++ b/src/HOL/Tools/Function/sum_tree.ML Wed Nov 25 11:16:58 2009 +0100
@@ -8,8 +8,8 @@
struct
(* Theory dependencies *)
-val proj_in_rules = [@{thm "Datatype.Projl_Inl"}, @{thm "Datatype.Projr_Inr"}]
-val sumcase_split_ss = HOL_basic_ss addsimps (@{thm "Product_Type.split"} :: @{thms "sum.cases"})
+val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
+val sumcase_split_ss = HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
(* top-down access in balanced tree *)
fun access_top_down {left, right, init} len i =
@@ -31,8 +31,8 @@
fun mk_proj ST n i =
access_top_down
{ init = (ST, I : term -> term),
- left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Datatype.Projl}, T --> LT)) o proj)),
- right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Datatype.Projr}, T --> RT)) o proj))} n i
+ left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
+ right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
|> snd
fun mk_sumcases T fs =