# HG changeset patch
# User haftmann
# Date 1259144218 -3600
# Node ID 03f2ab6a4ea60ad9777229795d5ca8e2958977d6
# Parent  53993394ac19a8e0bad14a6a960ed47f5dc210b5
centralized sum type matter in Sum_Type.thy

diff -r 53993394ac19 -r 03f2ab6a4ea6 src/HOL/Sum_Type.thy
--- 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
 {*
diff -r 53993394ac19 -r 03f2ab6a4ea6 src/HOL/Tools/Function/sum_tree.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 =