# HG changeset patch # User blanchet # Date 1402939090 -7200 # Node ID 8747af0d101291313d77dcd09ff0e068a7ae28ed # Parent 3a448982a74a0547c56787e4bcbc0da0daa54a58 fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses) diff -r 3a448982a74a -r 8747af0d1012 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jun 16 17:52:33 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jun 16 19:18:10 2014 +0200 @@ -26,7 +26,7 @@ val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms type gfp_sugar_thms = - ((thm list * thm) list * Args.src list) + ((thm list * thm) list * (Args.src list * Args.src list)) * (thm list list * Args.src list) * (thm list list * Args.src list) * (thm list list * Args.src list) @@ -280,17 +280,17 @@ morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; type gfp_sugar_thms = - ((thm list * thm) list * Args.src list) + ((thm list * thm) list * (Args.src list * Args.src list)) * (thm list list * Args.src list) * (thm list list * Args.src list) * (thm list list * Args.src list) * (thm list list list * Args.src list); -fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs), +fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair), (corecss, corec_attrs), (disc_corecss, disc_corec_attrs), (disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) = ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, - coinduct_attrs), + coinduct_attrs_pair), (map (map (Morphism.thm phi)) corecss, corec_attrs), (map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs), (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs), @@ -688,18 +688,20 @@ |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; - fun postproc nn thm = - Thm.permute_prems 0 nn - (if nn = 1 then thm RS mp else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm) - |> Drule.zero_var_indexes - |> `(conj_dests nn); + val postproc = + Drule.zero_var_indexes + #> `(conj_dests nn) + #>> map (fn thm => Thm.permute_prems 0 nn (thm RS mp)) + ##> (fn thm => Thm.permute_prems 0 nn + (if nn = 1 then thm RS mp + else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)); val rel_eqs = map rel_eq_of_bnf pre_bnfs; val rel_monos = map rel_mono_of_bnf pre_bnfs; val dtor_coinducts = [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy] in - map2 (postproc nn oo prove) dtor_coinducts goals + map2 (postproc oo prove) dtor_coinducts goals end; fun mk_coinduct_concls ms discs ctrs = @@ -809,16 +811,21 @@ val sel_corec_thmsss = mk_sel_corec_thms corec_thmss; - val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn)); + val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn)); + val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); + val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases)); val coinduct_case_concl_attrs = map2 (fn casex => fn concls => Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls)))) coinduct_cases coinduct_conclss; - val coinduct_case_attrs = + + val common_coinduct_attrs = + common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; + val coinduct_attrs = coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; in - ((coinduct_thms_pairs, coinduct_case_attrs), + ((coinduct_thms_pairs, (coinduct_attrs, common_coinduct_attrs)), (corec_thmss, code_nitpicksimp_attrs), (disc_corec_thmss, []), (disc_corec_iff_thmss, simp_attrs), @@ -1176,7 +1183,7 @@ ||>> mk_TFrees (live_of_bnf fp_bnf) ||>> mk_TFrees (live_of_bnf fp_bnf); val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf; - val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf; + val Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf; val fTs = map2 (curry op -->) As Bs; val ((fs, ta), names_lthy) = names_lthy |> mk_Frees "f" fTs @@ -1466,7 +1473,7 @@ (corecs, corec_defs)), lthy) = let val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)], - coinduct_attrs), + (coinduct_attrs, common_coinduct_attrs)), (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs), (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) = derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct @@ -1487,8 +1494,8 @@ val common_notes = (if nn > 1 then - [(coinductN, [coinduct_thm], coinduct_attrs), - (strong_coinductN, [strong_coinduct_thm], coinduct_attrs)] + [(coinductN, [coinduct_thm], common_coinduct_attrs), + (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)] else []) |> massage_simple_notes fp_common_name; diff -r 3a448982a74a -r 8747af0d1012 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jun 16 17:52:33 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jun 16 19:18:10 2014 +0200 @@ -262,17 +262,16 @@ val name_of_ctr = name_of_const "constructor"; val notN = "not_"; -val eqN = "eq_"; -val neqN = "neq_"; +val isN = "is_"; fun name_of_disc t = (case head_of t of Abs (_, _, @{const Not} $ (t' $ Bound 0)) => Long_Name.map_base_name (prefix notN) (name_of_disc t') | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') => - Long_Name.map_base_name (prefix eqN) (name_of_disc t') + Long_Name.map_base_name (prefix isN) (name_of_disc t') | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) => - Long_Name.map_base_name (prefix neqN) (name_of_disc t') + Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t') | t' => name_of_const "destructor" t'); val base_name_of_ctr = Long_Name.base_name o name_of_ctr; diff -r 3a448982a74a -r 8747af0d1012 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Mon Jun 16 17:52:33 2014 +0200 +++ b/src/HOL/Transfer.thy Mon Jun 16 19:18:10 2014 +0200 @@ -246,7 +246,7 @@ using assms by (auto simp add: eq_onp_def) lemma Ball_Collect: "Ball A P = (A \ (Collect P))" -by (metis mem_Collect_eq subset_eq) +by auto ML_file "Tools/Transfer/transfer.ML" setup Transfer.setup