# HG changeset patch # User blanchet # Date 1452672577 -3600 # Node ID c25c62055180862572666846d6e2c3c67889183a # Parent adcaaf6c99104159515453058ab299ca5a3b217d generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes diff -r adcaaf6c9910 -r c25c62055180 src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Wed Jan 13 00:12:43 2016 +0100 +++ b/src/HOL/BNF_Fixpoint_Base.thy Wed Jan 13 09:09:37 2016 +0100 @@ -17,11 +17,8 @@ lemma conj_imp_eq_imp_imp: "(P \ Q \ PROP R) \ (P \ Q \ PROP R)" by standard simp_all -lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" - by auto - -lemma predicate2D_conj: "P \ Q \ R \ P x y \ R \ Q x y" - by auto +lemma predicate2D_conj: "P \ Q \ R \ R \ (P x y \ Q x y)" + by blast lemma eq_sym_Unity_conv: "(x = (() = ())) = x" by blast diff -r adcaaf6c9910 -r c25c62055180 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jan 13 00:12:43 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jan 13 09:09:37 2016 +0100 @@ -468,8 +468,6 @@ val name_of_set = name_of_const "set function" domain_type; -val mp_conj = @{thm mp_conj}; - val fundefcong_attrs = @{attributes [fundef_cong]}; val nitpicksimp_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; @@ -1322,13 +1320,13 @@ @{map 5} mk_preds_getterss_join cs cpss f_absTs abss cqgsss))) end; -fun postproc_co_induct lthy nn prop prop_conj = +fun postproc_co_induct ctxt nn prop prop_conj = Drule.zero_var_indexes #> `(conj_dests nn) #>> map (fn thm => Thm.permute_prems 0 ~1 (thm RS prop)) ##> (fn thm => Thm.permute_prems 0 (~ nn) (if nn = 1 then thm RS prop - else funpow nn (fn thm => unfold_thms lthy @{thms conj_assoc} (thm RS prop_conj)) thm)); + else funpow nn (fn thm => unfold_thms ctxt @{thms conj_assoc} (thm RS prop_conj)) thm)); fun mk_induct_attrs ctrss = let @@ -1338,7 +1336,7 @@ [induct_case_names_attr] end; -fun derive_rel_induct_thms_for_types lthy fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct +fun derive_rel_induct_thms_for_types lthy nn fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs = let val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); @@ -1375,8 +1373,7 @@ ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs) |> Thm.close_derivation; in - (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} - rel_induct0_thm, + (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm, mk_induct_attrs ctrAss) end; @@ -1549,7 +1546,6 @@ val coinduct_conclss = @{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; - 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)); @@ -1558,15 +1554,14 @@ Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls)))) coinduct_cases coinduct_conclss; - val common_coinduct_attrs = - common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; + val common_coinduct_attrs = coinduct_case_names_attr :: coinduct_case_concl_attrs; val coinduct_attrs = coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; in (coinduct_attrs, common_coinduct_attrs) end; -fun derive_rel_coinduct_thm_for_types lthy fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list) +fun derive_rel_coinduct_thms_for_types lthy nn fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list) abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct live_nesting_rel_eqs = let @@ -1635,8 +1630,7 @@ rel_pre_defs abs_inverses live_nesting_rel_eqs) |> Thm.close_derivation; in - (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} - rel_coinduct0_thm, + (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm, mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss) end; @@ -1846,7 +1840,8 @@ val dtor_coinducts = [dtor_coinduct, mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy] in - @{map 3} (postproc_co_induct lthy nn mp mp_conj ooo prove) dtor_coinducts goals varss + @{map 3} (postproc_co_induct lthy nn mp @{thm conj_commute[THEN iffD1]} ooo prove) + dtor_coinducts goals varss end; fun mk_maybe_not pos = not pos ? HOLogic.mk_not; @@ -2420,7 +2415,7 @@ else let val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) = - derive_rel_induct_thms_for_types lthy fpTs As Bs ctrss ctr_Tsss + derive_rel_induct_thms_for_types lthy nn fpTs As Bs ctrss ctr_Tsss (map #exhaust ctr_sugars) xtor_rel_co_induct ctr_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs; in @@ -2586,7 +2581,7 @@ let val ((rel_coinduct_thms, common_rel_coinduct_thm), (rel_coinduct_attrs, common_rel_coinduct_attrs)) = - derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses + derive_rel_coinduct_thms_for_types lthy nn fpTs ns As Bs mss ctr_sugars abs_inverses abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss xtor_rel_co_induct live_nesting_rel_eqs; in