generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
authorblanchet
Wed Jan 13 09:09:37 2016 +0100 (2016-01-13 ago)
changeset 62158c25c62055180
parent 62157 adcaaf6c9910
child 62159 56d35d0fda5b
generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Wed Jan 13 00:12:43 2016 +0100
     1.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Wed Jan 13 09:09:37 2016 +0100
     1.3 @@ -17,11 +17,8 @@
     1.4  lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
     1.5    by standard simp_all
     1.6  
     1.7 -lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
     1.8 -  by auto
     1.9 -
    1.10 -lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
    1.11 -  by auto
    1.12 +lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> R \<and> (P x y \<longrightarrow> Q x y)"
    1.13 +  by blast
    1.14  
    1.15  lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
    1.16    by blast
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jan 13 00:12:43 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jan 13 09:09:37 2016 +0100
     2.3 @@ -468,8 +468,6 @@
     2.4  
     2.5  val name_of_set = name_of_const "set function" domain_type;
     2.6  
     2.7 -val mp_conj = @{thm mp_conj};
     2.8 -
     2.9  val fundefcong_attrs = @{attributes [fundef_cong]};
    2.10  val nitpicksimp_attrs = @{attributes [nitpick_simp]};
    2.11  val simp_attrs = @{attributes [simp]};
    2.12 @@ -1322,13 +1320,13 @@
    2.13           @{map 5} mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
    2.14    end;
    2.15  
    2.16 -fun postproc_co_induct lthy nn prop prop_conj =
    2.17 +fun postproc_co_induct ctxt nn prop prop_conj =
    2.18    Drule.zero_var_indexes
    2.19    #> `(conj_dests nn)
    2.20    #>> map (fn thm => Thm.permute_prems 0 ~1 (thm RS prop))
    2.21    ##> (fn thm => Thm.permute_prems 0 (~ nn)
    2.22      (if nn = 1 then thm RS prop
    2.23 -     else funpow nn (fn thm => unfold_thms lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
    2.24 +     else funpow nn (fn thm => unfold_thms ctxt @{thms conj_assoc} (thm RS prop_conj)) thm));
    2.25  
    2.26  fun mk_induct_attrs ctrss =
    2.27    let
    2.28 @@ -1338,7 +1336,7 @@
    2.29      [induct_case_names_attr]
    2.30    end;
    2.31  
    2.32 -fun derive_rel_induct_thms_for_types lthy fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct
    2.33 +fun derive_rel_induct_thms_for_types lthy nn fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct
    2.34      ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
    2.35    let
    2.36      val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
    2.37 @@ -1375,8 +1373,7 @@
    2.38            ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
    2.39        |> Thm.close_derivation;
    2.40    in
    2.41 -    (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
    2.42 -       rel_induct0_thm,
    2.43 +    (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm,
    2.44       mk_induct_attrs ctrAss)
    2.45    end;
    2.46  
    2.47 @@ -1549,7 +1546,6 @@
    2.48      val coinduct_conclss =
    2.49        @{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
    2.50  
    2.51 -    val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
    2.52      val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
    2.53  
    2.54      val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
    2.55 @@ -1558,15 +1554,14 @@
    2.56            Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
    2.57          coinduct_cases coinduct_conclss;
    2.58  
    2.59 -    val common_coinduct_attrs =
    2.60 -      common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    2.61 +    val common_coinduct_attrs = coinduct_case_names_attr :: coinduct_case_concl_attrs;
    2.62      val coinduct_attrs =
    2.63        coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    2.64    in
    2.65      (coinduct_attrs, common_coinduct_attrs)
    2.66    end;
    2.67  
    2.68 -fun derive_rel_coinduct_thm_for_types lthy fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list)
    2.69 +fun derive_rel_coinduct_thms_for_types lthy nn fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list)
    2.70      abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct
    2.71      live_nesting_rel_eqs =
    2.72    let
    2.73 @@ -1635,8 +1630,7 @@
    2.74            rel_pre_defs abs_inverses live_nesting_rel_eqs)
    2.75        |> Thm.close_derivation;
    2.76    in
    2.77 -    (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
    2.78 -       rel_coinduct0_thm,
    2.79 +    (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
    2.80       mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
    2.81    end;
    2.82  
    2.83 @@ -1846,7 +1840,8 @@
    2.84          val dtor_coinducts =
    2.85            [dtor_coinduct, mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
    2.86        in
    2.87 -        @{map 3} (postproc_co_induct lthy nn mp mp_conj ooo prove) dtor_coinducts goals varss
    2.88 +        @{map 3} (postproc_co_induct lthy nn mp @{thm conj_commute[THEN iffD1]} ooo prove)
    2.89 +          dtor_coinducts goals varss
    2.90        end;
    2.91  
    2.92      fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
    2.93 @@ -2420,7 +2415,7 @@
    2.94            else
    2.95              let
    2.96                val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) =
    2.97 -                derive_rel_induct_thms_for_types lthy fpTs As Bs ctrss ctr_Tsss
    2.98 +                derive_rel_induct_thms_for_types lthy nn fpTs As Bs ctrss ctr_Tsss
    2.99                    (map #exhaust ctr_sugars) xtor_rel_co_induct ctr_defss ctor_injects
   2.100                    pre_rel_defs abs_inverses live_nesting_rel_eqs;
   2.101              in
   2.102 @@ -2586,7 +2581,7 @@
   2.103              let
   2.104                val ((rel_coinduct_thms, common_rel_coinduct_thm),
   2.105                     (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
   2.106 -                derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
   2.107 +                derive_rel_coinduct_thms_for_types lthy nn fpTs ns As Bs mss ctr_sugars abs_inverses
   2.108                    abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss xtor_rel_co_induct
   2.109                    live_nesting_rel_eqs;
   2.110              in