# HG changeset patch
# User krauss
# Date 1230396555 -3600
# Node ID f1648e009dc111245ba28ff656f1e5e84a593924
# Parent  9304afad825ef9ddc2b4ee5571aa708f5bac72e1
removed duplicate sum_case used only by function package;
moved projections;
hide (open)

diff -r 9304afad825e -r f1648e009dc1 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Sat Dec 27 17:35:01 2008 +0100
+++ b/src/HOL/Datatype.thy	Sat Dec 27 17:49:15 2008 +0100
@@ -578,7 +578,13 @@
 lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
   by (unfold Sumr_def) (erule sum_case_inject)
 
-hide (open) const Suml Sumr
+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
 
 
 subsection {* The option datatype *}
diff -r 9304afad825e -r f1648e009dc1 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Sat Dec 27 17:35:01 2008 +0100
+++ b/src/HOL/Sum_Type.thy	Sat Dec 27 17:49:15 2008 +0100
@@ -120,29 +120,6 @@
 by (blast dest!: Inr_inject)
 
 
-subsection {* Projections *}
-
-definition 
-  "sum_case f g x =
-  (if (\<exists>!y. x = Inl y) 
-  then f (THE y. x = Inl y) 
-  else g (THE y. x = Inr y))"
-definition "Projl x = sum_case id undefined x"
-definition "Projr x = sum_case undefined id x"
-
-lemma sum_cases[simp]: 
-  "sum_case f g (Inl x) = f x"
-  "sum_case f g (Inr y) = g y"
-  unfolding sum_case_def
-  by auto
-
-lemma Projl_Inl[simp]: "Projl (Inl x) = x"
-  unfolding Projl_def by simp
-
-lemma Projr_Inr[simp]: "Projr (Inr x) = x"
-  unfolding Projr_def by simp
-
-
 subsection{*The Disjoint Sum of Sets*}
 
 (** Introduction rules for the injections **)
diff -r 9304afad825e -r f1648e009dc1 src/HOL/Tools/function_package/induction_scheme.ML
--- a/src/HOL/Tools/function_package/induction_scheme.ML	Sat Dec 27 17:35:01 2008 +0100
+++ b/src/HOL/Tools/function_package/induction_scheme.ML	Sat Dec 27 17:49:15 2008 +0100
@@ -55,7 +55,7 @@
 fun meta thm = thm RS eq_reflection
 
 val sum_prod_conv = MetaSimplifier.rewrite true 
-                    (map meta (@{thm split_conv} :: @{thms sum_cases}))
+                    (map meta (@{thm split_conv} :: @{thms sum.cases}))
 
 fun term_conv thy cv t = 
     cv (cterm_of thy t)
@@ -320,7 +320,7 @@
 
             val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
                      |> Goal.init
-                     |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum_cases}))
+                     |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
                          THEN CONVERSION ind_rulify 1)
                      |> Seq.hd
                      |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
diff -r 9304afad825e -r f1648e009dc1 src/HOL/Tools/function_package/scnp_reconstruct.ML
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Sat Dec 27 17:35:01 2008 +0100
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Sat Dec 27 17:49:15 2008 +0100
@@ -133,7 +133,7 @@
     THEN etac @{thm conjE} 1
     THEN etac @{thm ssubst} 1
     THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
-                     @ @{thms Sum_Type.sum_cases})
+                     @ @{thms sum.cases})
   end
 
 (* Sets *)
diff -r 9304afad825e -r f1648e009dc1 src/HOL/Tools/function_package/sum_tree.ML
--- a/src/HOL/Tools/function_package/sum_tree.ML	Sat Dec 27 17:35:01 2008 +0100
+++ b/src/HOL/Tools/function_package/sum_tree.ML	Sat Dec 27 17:49:15 2008 +0100
@@ -9,8 +9,8 @@
 struct
 
 (* Theory dependencies *)
-val proj_in_rules = [thm "Sum_Type.Projl_Inl", thm "Sum_Type.Projr_Inr"]
-val sumcase_split_ss = HOL_basic_ss addsimps (@{thm "Product_Type.split"} :: @{thms "Sum_Type.sum_cases"})
+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"})
 
 (* top-down access in balanced tree *)
 fun access_top_down {left, right, init} len i =
@@ -18,7 +18,7 @@
 
 (* Sum types *)
 fun mk_sumT LT RT = Type ("+", [LT, RT])
-fun mk_sumcase TL TR T l r = Const (@{const_name "Sum_Type.sum_case"}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
+fun mk_sumcase TL TR T l r = Const (@{const_name "sum.sum_case"}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
 
 val App = curry op $
 
@@ -32,8 +32,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 "Projl"}, T --> LT)) o proj)),
-      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name "Projr"}, T --> RT)) o proj))} n i
+      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
     |> snd
 
 fun mk_sumcases T fs =