# HG changeset patch # User blanchet # Date 1392190556 -3600 # Node ID ce5cebfaeddab3f3a0ba679e0ab85e1bf2eb2153 # Parent 20f282bb83718e4fcb1aae7577a8ae0f3c16c86c se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets diff -r 20f282bb8371 -r ce5cebfaedda src/HOL/Import/HOL_Light_Maps.thy --- 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 @@ "\Inl' Inr'. \fn. (\a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \ (\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 diff -r 20f282bb8371 -r ce5cebfaedda src/HOL/Product_Type.thy --- 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 \ 'b \ 'a \ 'b" where "Pair a b = Abs_prod (Pair_Rep a b)" -rep_datatype Pair proof - - fix P :: "'a \ 'b \ bool" and p - assume "\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: "(\a b. P (Pair a b)) \ 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 \ 'b" + show "(\x1 x2. p = Pair x1 x2 \ P) \ 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 \ a = c \ 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 \ 'b \ bool" and p + assume "\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 \ a = c \ 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 \ 'b \ 'a" where - "fst p = (case p of (a, b) \ a)" - -definition snd :: "'a \ 'b \ 'b" where - "snd p = (case p of (a, b) \ 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 \ (Haskell) "fst" | constant snd \ (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 \ fst s = fst t \ 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 diff -r 20f282bb8371 -r ce5cebfaedda src/HOL/Sum_Type.thy --- 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 \ 'c) \ ('b \ 'd) \ 'a + 'b \ '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 \ 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 \ 'a" where - Projl_Inl: "Projl (Inl x) = x" - -primrec Projr :: "'a + 'b \ 'b" where - Projr_Inr: "Projr (Inr x) = x" - primrec Suml :: "('a \ 'c) \ 'a + 'b \ '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 - diff -r 20f282bb8371 -r ce5cebfaedda src/HOL/Tools/BNF/bnf_gfp.ML --- 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; diff -r 20f282bb8371 -r ce5cebfaedda src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- 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)]; diff -r 20f282bb8371 -r ce5cebfaedda src/HOL/Tools/Function/sum_tree.ML --- 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 =