src/HOL/Sum_Type.thy
changeset 55393 ce5cebfaedda
parent 53010 ec5e6f69bd65
child 55403 677569668824
--- a/src/HOL/Sum_Type.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Sum_Type.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -85,6 +85,12 @@
   with assms show P by (auto simp add: sum_def Inl_def Inr_def)
 qed
 
+wrap_free_constructors [Inl, Inr] sum_case [isl] [[projl], [projr]]
+by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
+
+-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+setup {* Sign.mandatory_path "old" *}
+
 rep_datatype Inl Inr
 proof -
   fix P
@@ -93,6 +99,24 @@
   then show "P s" by (auto intro: sumE [of s])
 qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
 
+setup {* Sign.parent_path *}
+
+-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+setup {* Sign.mandatory_path "sum" *}
+
+declare
+  old.sum.inject[iff del]
+  old.sum.distinct(1)[simp del, induct_simp del]
+  old.sum.cases[simp del]
+
+lemmas induct = old.sum.induct
+lemmas inducts = old.sum.inducts
+lemmas recs = old.sum.recs
+lemmas cases = sum.case
+lemmas simps = sum.inject sum.distinct sum.case old.sum.recs
+
+setup {* Sign.parent_path *}
+
 primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
@@ -150,17 +174,6 @@
   qed
 qed
 
-lemma sum_case_weak_cong:
-  "s = t \<Longrightarrow> sum_case f g s = sum_case f g t"
-  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
-  by simp
-
-primrec Projl :: "'a + 'b \<Rightarrow> 'a" where
-  Projl_Inl: "Projl (Inl x) = x"
-
-primrec Projr :: "'a + 'b \<Rightarrow> 'b" where
-  Projr_Inr: "Projr (Inr x) = x"
-
 primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   "Suml f (Inl x) = f x"
 
@@ -224,9 +237,6 @@
   } then show ?thesis by auto
 qed
 
-hide_const (open) Suml Sumr Projl Projr
-
-hide_const (open) sum
+hide_const (open) Suml Sumr sum
 
 end
-