se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
* * *
cleaner simp/iff sets

--- a/src/HOL/Import/HOL_Light_Maps.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -212,12 +212,12 @@
   "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
   by (intro allI, rule_tac x="sum_case Inl' Inr'" in exI) auto
 
-lemma OUTL[import_const "OUTL" : "Sum_Type.Projl"]:
-  "Sum_Type.Projl (Inl x) = x"
+lemma OUTL[import_const "OUTL" : "Sum_Type.projl"]:
+  "Sum_Type.projl (Inl x) = x"
   by simp
 
-lemma OUTR[import_const "OUTR" : "Sum_Type.Projr"]:
-  "Sum_Type.Projr (Inr y) = y"
+lemma OUTR[import_const "OUTR" : "Sum_Type.projr"]:
+  "Sum_Type.projr (Inr y) = y"
   by simp
 
 import_type_map list : List.list

--- a/src/HOL/Product_Type.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Product_Type.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -12,8 +12,29 @@
 
 subsection {* @{typ bool} is a datatype *}
 
+wrap_free_constructors [True, False] bool_case [=]
+by auto
+
+-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+setup {* Sign.mandatory_path "old" *}
+
 rep_datatype True False by (auto intro: bool_induct)
 
+setup {* Sign.parent_path *}
+
+-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+setup {* Sign.mandatory_path "bool" *}
+
+declare old.bool.cases[simp del]
+
+lemmas induct = old.bool.induct
+lemmas inducts = old.bool.inducts
+lemmas recs = old.bool.recs
+lemmas cases = bool.case
+lemmas simps = bool.distinct bool.case old.bool.recs
+
+setup {* Sign.parent_path *}
+
 declare case_split [cases type: bool]
   -- "prefer plain propositional version"
 
@@ -61,8 +82,29 @@
     else SOME (mk_meta_eq @{thm unit_eq})
 *}
 
+wrap_free_constructors ["()"] unit_case
+by auto
+
+-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+setup {* Sign.mandatory_path "old" *}
+
 rep_datatype "()" by simp
 
+setup {* Sign.parent_path *}
+
+-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+setup {* Sign.mandatory_path "unit" *}
+
+declare old.unit.cases[simp del]
+
+lemmas induct = old.unit.induct
+lemmas inducts = old.unit.inducts
+lemmas recs = old.unit.recs
+lemmas cases = unit.case
+lemmas simps = unit.case old.unit.recs
+
+setup {* Sign.parent_path *}
+
 lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
   by simp
 
@@ -139,10 +181,14 @@
 definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
   "Pair a b = Abs_prod (Pair_Rep a b)"
 
-rep_datatype Pair proof -
-  fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
-  assume "\<And>a b. P (Pair a b)"
-  then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
+lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
+  by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
+
+wrap_free_constructors [Pair] prod_case [] [[fst, snd]]
+proof -
+  fix P :: bool and p :: "'a \<times> 'b"
+  show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
+    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
 next
   fix a c :: 'a and b d :: 'b
   have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
@@ -153,8 +199,38 @@
     by (simp add: Pair_def Abs_prod_inject)
 qed
 
-declare prod.simps(2) [nitpick_simp del]
+-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+setup {* Sign.mandatory_path "old" *}
+
+rep_datatype Pair
+proof -
+  fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
+  assume "\<And>a b. P (Pair a b)"
+  then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
+next
+  fix a c :: 'a and b d :: 'b
+  show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
+    by (rule prod.inject)
+qed
+
+setup {* Sign.parent_path *}
 
+-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+setup {* Sign.mandatory_path "prod" *}
+
+declare
+  old.prod.inject[iff del]
+  old.prod.cases[simp del]
+
+lemmas induct = old.prod.induct
+lemmas inducts = old.prod.inducts
+lemmas recs = old.prod.recs
+lemmas cases = prod.case
+lemmas simps = prod.inject prod.case old.prod.recs
+
+setup {* Sign.parent_path *}
+
+declare prod.case [nitpick_simp del]
 declare prod.weak_case_cong [cong del]
 
 
@@ -312,18 +388,6 @@
 lemma surj_pair [simp]: "EX x y. p = (x, y)"
   by (cases p) simp
 
-definition fst :: "'a \<times> 'b \<Rightarrow> 'a" where
-  "fst p = (case p of (a, b) \<Rightarrow> a)"
-
-definition snd :: "'a \<times> 'b \<Rightarrow> 'b" where
-  "snd p = (case p of (a, b) \<Rightarrow> b)"
-
-lemma fst_conv [simp, code]: "fst (a, b) = a"
-  unfolding fst_def by simp
-
-lemma snd_conv [simp, code]: "snd (a, b) = b"
-  unfolding snd_def by simp
-
 code_printing
   constant fst \<rightharpoonup> (Haskell) "fst"
 | constant snd \<rightharpoonup> (Haskell) "snd"
@@ -337,10 +401,7 @@
 lemma snd_eqD: "snd (x, y) = a ==> y = a"
   by simp
 
-lemma pair_collapse [simp]: "(fst p, snd p) = p"
-  by (cases p) simp
-
-lemmas surjective_pairing = pair_collapse [symmetric]
+lemmas surjective_pairing = prod.collapse [symmetric]
 
 lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
   by (cases s, cases t) simp
@@ -1179,9 +1240,10 @@
   by (fact prod.exhaust)
 
 lemmas Pair_eq = prod.inject
-
-lemmas split = split_conv  -- {* for backwards compatibility *}
-
+lemmas fst_conv = prod.sel(1)
+lemmas snd_conv = prod.sel(2)
+lemmas pair_collapse = prod.collapse
+lemmas split = split_conv
 lemmas Pair_fst_snd_eq = prod_eq_iff
 
 hide_const (open) prod

--- 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
-

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -1432,7 +1432,7 @@
         map (fn i => map (fn i' =>
           split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
             else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
-              (2, @{thm sum_case_weak_cong} RS iffD1) RS
+              (2, @{thm sum.weak_case_cong} RS iffD1) RS
               (mk_sum_casesN n i' RS iffD1))) ks) ks
       end;
 

--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -112,7 +112,7 @@
   @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
 val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
-val sum_case_weak_cong = @{thm sum_case_weak_cong};
+val sum_weak_case_cong = @{thm sum.weak_case_cong};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
 val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
 val rev_bspec = Drule.rotate_prems 1 bspec;
@@ -512,7 +512,7 @@
         CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
           CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
             rtac (@{thm append_Cons} RS arg_cong RS trans),
-            rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),
+            rtac (rv_Cons RS trans), etac (sum_weak_case_cong RS arg_cong RS trans),
             rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
           ks])
         rv_Conss)
@@ -684,7 +684,7 @@
               rtac exI, rtac conjI,
               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
               else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
-                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
+                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
               EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
                 EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
                   rtac trans_fun_cong_image_id_id_apply,
@@ -708,7 +708,7 @@
               rtac exI, rtac conjI,
               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
               else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
-                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
+                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
               EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
                 EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
                   rtac trans_fun_cong_image_id_id_apply,
@@ -756,14 +756,13 @@
     fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
       ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
       EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
-        rtac (@{thm if_P} RS
-          (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
+        rtac (@{thm if_P} RS (if n = 1 then map_arg_cong else sum_weak_case_cong) RS trans),
         rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
         rtac Lev_0, rtac @{thm singletonI},
         CONVERSION (Conv.top_conv
           (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
         if n = 1 then K all_tac
-        else (rtac (sum_case_weak_cong RS trans) THEN'
+        else (rtac (sum_weak_case_cong RS trans) THEN'
           rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
         rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
         EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
@@ -801,7 +800,7 @@
             CONVERSION (Conv.top_conv
               (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
             if n = 1 then K all_tac
-            else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
+            else rtac sum_weak_case_cong THEN' rtac (mk_sum_casesN n i' RS trans),
             SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
             rtac refl])
         ks to_sbd_injs from_to_sbds)];

--- a/src/HOL/Tools/Function/sum_tree.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Function/sum_tree.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -50,9 +50,9 @@
   access_top_down
   { init = (ST, I : term -> term),
     left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
-      (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
+      (LT, App (Const (@{const_name Sum_Type.projl}, T --> LT)) o proj)),
     right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
-      (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
+      (RT, App (Const (@{const_name Sum_Type.projr}, T --> RT)) o proj))} n i
   |> snd
 
 fun mk_sumcases T fs =