se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
authorblanchet
Wed Feb 12 08:35:56 2014 +0100 (2014-02-12)
changeset 55393ce5cebfaedda
parent 55392 20f282bb8371
child 55394 d5ebe055b599
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
* * *
cleaner simp/iff sets
src/HOL/Import/HOL_Light_Maps.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/Function/sum_tree.ML
     1.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -212,12 +212,12 @@
     1.4    "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
     1.5    by (intro allI, rule_tac x="sum_case Inl' Inr'" in exI) auto
     1.6  
     1.7 -lemma OUTL[import_const "OUTL" : "Sum_Type.Projl"]:
     1.8 -  "Sum_Type.Projl (Inl x) = x"
     1.9 +lemma OUTL[import_const "OUTL" : "Sum_Type.projl"]:
    1.10 +  "Sum_Type.projl (Inl x) = x"
    1.11    by simp
    1.12  
    1.13 -lemma OUTR[import_const "OUTR" : "Sum_Type.Projr"]:
    1.14 -  "Sum_Type.Projr (Inr y) = y"
    1.15 +lemma OUTR[import_const "OUTR" : "Sum_Type.projr"]:
    1.16 +  "Sum_Type.projr (Inr y) = y"
    1.17    by simp
    1.18  
    1.19  import_type_map list : List.list
     2.1 --- a/src/HOL/Product_Type.thy	Wed Feb 12 08:35:56 2014 +0100
     2.2 +++ b/src/HOL/Product_Type.thy	Wed Feb 12 08:35:56 2014 +0100
     2.3 @@ -12,8 +12,29 @@
     2.4  
     2.5  subsection {* @{typ bool} is a datatype *}
     2.6  
     2.7 +wrap_free_constructors [True, False] bool_case [=]
     2.8 +by auto
     2.9 +
    2.10 +-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    2.11 +setup {* Sign.mandatory_path "old" *}
    2.12 +
    2.13  rep_datatype True False by (auto intro: bool_induct)
    2.14  
    2.15 +setup {* Sign.parent_path *}
    2.16 +
    2.17 +-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    2.18 +setup {* Sign.mandatory_path "bool" *}
    2.19 +
    2.20 +declare old.bool.cases[simp del]
    2.21 +
    2.22 +lemmas induct = old.bool.induct
    2.23 +lemmas inducts = old.bool.inducts
    2.24 +lemmas recs = old.bool.recs
    2.25 +lemmas cases = bool.case
    2.26 +lemmas simps = bool.distinct bool.case old.bool.recs
    2.27 +
    2.28 +setup {* Sign.parent_path *}
    2.29 +
    2.30  declare case_split [cases type: bool]
    2.31    -- "prefer plain propositional version"
    2.32  
    2.33 @@ -61,8 +82,29 @@
    2.34      else SOME (mk_meta_eq @{thm unit_eq})
    2.35  *}
    2.36  
    2.37 +wrap_free_constructors ["()"] unit_case
    2.38 +by auto
    2.39 +
    2.40 +-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    2.41 +setup {* Sign.mandatory_path "old" *}
    2.42 +
    2.43  rep_datatype "()" by simp
    2.44  
    2.45 +setup {* Sign.parent_path *}
    2.46 +
    2.47 +-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    2.48 +setup {* Sign.mandatory_path "unit" *}
    2.49 +
    2.50 +declare old.unit.cases[simp del]
    2.51 +
    2.52 +lemmas induct = old.unit.induct
    2.53 +lemmas inducts = old.unit.inducts
    2.54 +lemmas recs = old.unit.recs
    2.55 +lemmas cases = unit.case
    2.56 +lemmas simps = unit.case old.unit.recs
    2.57 +
    2.58 +setup {* Sign.parent_path *}
    2.59 +
    2.60  lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
    2.61    by simp
    2.62  
    2.63 @@ -139,10 +181,14 @@
    2.64  definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
    2.65    "Pair a b = Abs_prod (Pair_Rep a b)"
    2.66  
    2.67 -rep_datatype Pair proof -
    2.68 -  fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
    2.69 -  assume "\<And>a b. P (Pair a b)"
    2.70 -  then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    2.71 +lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
    2.72 +  by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    2.73 +
    2.74 +wrap_free_constructors [Pair] prod_case [] [[fst, snd]]
    2.75 +proof -
    2.76 +  fix P :: bool and p :: "'a \<times> 'b"
    2.77 +  show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
    2.78 +    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    2.79  next
    2.80    fix a c :: 'a and b d :: 'b
    2.81    have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
    2.82 @@ -153,8 +199,38 @@
    2.83      by (simp add: Pair_def Abs_prod_inject)
    2.84  qed
    2.85  
    2.86 -declare prod.simps(2) [nitpick_simp del]
    2.87 +-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    2.88 +setup {* Sign.mandatory_path "old" *}
    2.89 +
    2.90 +rep_datatype Pair
    2.91 +proof -
    2.92 +  fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
    2.93 +  assume "\<And>a b. P (Pair a b)"
    2.94 +  then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    2.95 +next
    2.96 +  fix a c :: 'a and b d :: 'b
    2.97 +  show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
    2.98 +    by (rule prod.inject)
    2.99 +qed
   2.100 +
   2.101 +setup {* Sign.parent_path *}
   2.102  
   2.103 +-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
   2.104 +setup {* Sign.mandatory_path "prod" *}
   2.105 +
   2.106 +declare
   2.107 +  old.prod.inject[iff del]
   2.108 +  old.prod.cases[simp del]
   2.109 +
   2.110 +lemmas induct = old.prod.induct
   2.111 +lemmas inducts = old.prod.inducts
   2.112 +lemmas recs = old.prod.recs
   2.113 +lemmas cases = prod.case
   2.114 +lemmas simps = prod.inject prod.case old.prod.recs
   2.115 +
   2.116 +setup {* Sign.parent_path *}
   2.117 +
   2.118 +declare prod.case [nitpick_simp del]
   2.119  declare prod.weak_case_cong [cong del]
   2.120  
   2.121  
   2.122 @@ -312,18 +388,6 @@
   2.123  lemma surj_pair [simp]: "EX x y. p = (x, y)"
   2.124    by (cases p) simp
   2.125  
   2.126 -definition fst :: "'a \<times> 'b \<Rightarrow> 'a" where
   2.127 -  "fst p = (case p of (a, b) \<Rightarrow> a)"
   2.128 -
   2.129 -definition snd :: "'a \<times> 'b \<Rightarrow> 'b" where
   2.130 -  "snd p = (case p of (a, b) \<Rightarrow> b)"
   2.131 -
   2.132 -lemma fst_conv [simp, code]: "fst (a, b) = a"
   2.133 -  unfolding fst_def by simp
   2.134 -
   2.135 -lemma snd_conv [simp, code]: "snd (a, b) = b"
   2.136 -  unfolding snd_def by simp
   2.137 -
   2.138  code_printing
   2.139    constant fst \<rightharpoonup> (Haskell) "fst"
   2.140  | constant snd \<rightharpoonup> (Haskell) "snd"
   2.141 @@ -337,10 +401,7 @@
   2.142  lemma snd_eqD: "snd (x, y) = a ==> y = a"
   2.143    by simp
   2.144  
   2.145 -lemma pair_collapse [simp]: "(fst p, snd p) = p"
   2.146 -  by (cases p) simp
   2.147 -
   2.148 -lemmas surjective_pairing = pair_collapse [symmetric]
   2.149 +lemmas surjective_pairing = prod.collapse [symmetric]
   2.150  
   2.151  lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
   2.152    by (cases s, cases t) simp
   2.153 @@ -1179,9 +1240,10 @@
   2.154    by (fact prod.exhaust)
   2.155  
   2.156  lemmas Pair_eq = prod.inject
   2.157 -
   2.158 -lemmas split = split_conv  -- {* for backwards compatibility *}
   2.159 -
   2.160 +lemmas fst_conv = prod.sel(1)
   2.161 +lemmas snd_conv = prod.sel(2)
   2.162 +lemmas pair_collapse = prod.collapse
   2.163 +lemmas split = split_conv
   2.164  lemmas Pair_fst_snd_eq = prod_eq_iff
   2.165  
   2.166  hide_const (open) prod
     3.1 --- a/src/HOL/Sum_Type.thy	Wed Feb 12 08:35:56 2014 +0100
     3.2 +++ b/src/HOL/Sum_Type.thy	Wed Feb 12 08:35:56 2014 +0100
     3.3 @@ -85,6 +85,12 @@
     3.4    with assms show P by (auto simp add: sum_def Inl_def Inr_def)
     3.5  qed
     3.6  
     3.7 +wrap_free_constructors [Inl, Inr] sum_case [isl] [[projl], [projr]]
     3.8 +by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
     3.9 +
    3.10 +-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    3.11 +setup {* Sign.mandatory_path "old" *}
    3.12 +
    3.13  rep_datatype Inl Inr
    3.14  proof -
    3.15    fix P
    3.16 @@ -93,6 +99,24 @@
    3.17    then show "P s" by (auto intro: sumE [of s])
    3.18  qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
    3.19  
    3.20 +setup {* Sign.parent_path *}
    3.21 +
    3.22 +-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    3.23 +setup {* Sign.mandatory_path "sum" *}
    3.24 +
    3.25 +declare
    3.26 +  old.sum.inject[iff del]
    3.27 +  old.sum.distinct(1)[simp del, induct_simp del]
    3.28 +  old.sum.cases[simp del]
    3.29 +
    3.30 +lemmas induct = old.sum.induct
    3.31 +lemmas inducts = old.sum.inducts
    3.32 +lemmas recs = old.sum.recs
    3.33 +lemmas cases = sum.case
    3.34 +lemmas simps = sum.inject sum.distinct sum.case old.sum.recs
    3.35 +
    3.36 +setup {* Sign.parent_path *}
    3.37 +
    3.38  primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
    3.39    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    3.40  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    3.41 @@ -150,17 +174,6 @@
    3.42    qed
    3.43  qed
    3.44  
    3.45 -lemma sum_case_weak_cong:
    3.46 -  "s = t \<Longrightarrow> sum_case f g s = sum_case f g t"
    3.47 -  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    3.48 -  by simp
    3.49 -
    3.50 -primrec Projl :: "'a + 'b \<Rightarrow> 'a" where
    3.51 -  Projl_Inl: "Projl (Inl x) = x"
    3.52 -
    3.53 -primrec Projr :: "'a + 'b \<Rightarrow> 'b" where
    3.54 -  Projr_Inr: "Projr (Inr x) = x"
    3.55 -
    3.56  primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
    3.57    "Suml f (Inl x) = f x"
    3.58  
    3.59 @@ -224,9 +237,6 @@
    3.60    } then show ?thesis by auto
    3.61  qed
    3.62  
    3.63 -hide_const (open) Suml Sumr Projl Projr
    3.64 -
    3.65 -hide_const (open) sum
    3.66 +hide_const (open) Suml Sumr sum
    3.67  
    3.68  end
    3.69 -
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:56 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:56 2014 +0100
     4.3 @@ -1432,7 +1432,7 @@
     4.4          map (fn i => map (fn i' =>
     4.5            split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
     4.6              else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
     4.7 -              (2, @{thm sum_case_weak_cong} RS iffD1) RS
     4.8 +              (2, @{thm sum.weak_case_cong} RS iffD1) RS
     4.9                (mk_sum_casesN n i' RS iffD1))) ks) ks
    4.10        end;
    4.11  
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 12 08:35:56 2014 +0100
     5.3 @@ -112,7 +112,7 @@
     5.4    @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
     5.5  val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
     5.6  val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
     5.7 -val sum_case_weak_cong = @{thm sum_case_weak_cong};
     5.8 +val sum_weak_case_cong = @{thm sum.weak_case_cong};
     5.9  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
    5.10  val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
    5.11  val rev_bspec = Drule.rotate_prems 1 bspec;
    5.12 @@ -512,7 +512,7 @@
    5.13          CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
    5.14            CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
    5.15              rtac (@{thm append_Cons} RS arg_cong RS trans),
    5.16 -            rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),
    5.17 +            rtac (rv_Cons RS trans), etac (sum_weak_case_cong RS arg_cong RS trans),
    5.18              rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
    5.19            ks])
    5.20          rv_Conss)
    5.21 @@ -684,7 +684,7 @@
    5.22                rtac exI, rtac conjI,
    5.23                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
    5.24                else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
    5.25 -                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
    5.26 +                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
    5.27                EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
    5.28                  EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
    5.29                    rtac trans_fun_cong_image_id_id_apply,
    5.30 @@ -708,7 +708,7 @@
    5.31                rtac exI, rtac conjI,
    5.32                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
    5.33                else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
    5.34 -                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
    5.35 +                etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
    5.36                EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
    5.37                  EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
    5.38                    rtac trans_fun_cong_image_id_id_apply,
    5.39 @@ -756,14 +756,13 @@
    5.40      fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
    5.41        ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
    5.42        EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
    5.43 -        rtac (@{thm if_P} RS
    5.44 -          (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
    5.45 +        rtac (@{thm if_P} RS (if n = 1 then map_arg_cong else sum_weak_case_cong) RS trans),
    5.46          rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
    5.47          rtac Lev_0, rtac @{thm singletonI},
    5.48          CONVERSION (Conv.top_conv
    5.49            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
    5.50          if n = 1 then K all_tac
    5.51 -        else (rtac (sum_case_weak_cong RS trans) THEN'
    5.52 +        else (rtac (sum_weak_case_cong RS trans) THEN'
    5.53            rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
    5.54          rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
    5.55          EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
    5.56 @@ -801,7 +800,7 @@
    5.57              CONVERSION (Conv.top_conv
    5.58                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
    5.59              if n = 1 then K all_tac
    5.60 -            else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
    5.61 +            else rtac sum_weak_case_cong THEN' rtac (mk_sum_casesN n i' RS trans),
    5.62              SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
    5.63              rtac refl])
    5.64          ks to_sbd_injs from_to_sbds)];
     6.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Wed Feb 12 08:35:56 2014 +0100
     6.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Wed Feb 12 08:35:56 2014 +0100
     6.3 @@ -50,9 +50,9 @@
     6.4    access_top_down
     6.5    { init = (ST, I : term -> term),
     6.6      left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
     6.7 -      (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
     6.8 +      (LT, App (Const (@{const_name Sum_Type.projl}, T --> LT)) o proj)),
     6.9      right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
    6.10 -      (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
    6.11 +      (RT, App (Const (@{const_name Sum_Type.projr}, T --> RT)) o proj))} n i
    6.12    |> snd
    6.13  
    6.14  fun mk_sumcases T fs =