fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
authorblanchet
Mon Jun 16 19:18:10 2014 +0200 (2014-06-16)
changeset 572608747af0d1012
parent 57259 3a448982a74a
child 57261 49c1db0313e6
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jun 16 17:52:33 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jun 16 19:18:10 2014 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
     1.5  
     1.6    type gfp_sugar_thms =
     1.7 -    ((thm list * thm) list * Args.src list)
     1.8 +    ((thm list * thm) list * (Args.src list * Args.src list))
     1.9      * (thm list list * Args.src list)
    1.10      * (thm list list * Args.src list)
    1.11      * (thm list list * Args.src list)
    1.12 @@ -280,17 +280,17 @@
    1.13    morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
    1.14  
    1.15  type gfp_sugar_thms =
    1.16 -  ((thm list * thm) list * Args.src list)
    1.17 +  ((thm list * thm) list * (Args.src list * Args.src list))
    1.18    * (thm list list * Args.src list)
    1.19    * (thm list list * Args.src list)
    1.20    * (thm list list * Args.src list)
    1.21    * (thm list list list * Args.src list);
    1.22  
    1.23 -fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs),
    1.24 +fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
    1.25      (corecss, corec_attrs), (disc_corecss, disc_corec_attrs),
    1.26      (disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) =
    1.27    ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
    1.28 -    coinduct_attrs),
    1.29 +    coinduct_attrs_pair),
    1.30     (map (map (Morphism.thm phi)) corecss, corec_attrs),
    1.31     (map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs),
    1.32     (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
    1.33 @@ -688,18 +688,20 @@
    1.34            |> singleton (Proof_Context.export names_lthy lthy)
    1.35            |> Thm.close_derivation;
    1.36  
    1.37 -        fun postproc nn thm =
    1.38 -          Thm.permute_prems 0 nn
    1.39 -            (if nn = 1 then thm RS mp else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
    1.40 -          |> Drule.zero_var_indexes
    1.41 -          |> `(conj_dests nn);
    1.42 +        val postproc =
    1.43 +          Drule.zero_var_indexes
    1.44 +          #> `(conj_dests nn)
    1.45 +          #>> map (fn thm => Thm.permute_prems 0 nn (thm RS mp))
    1.46 +          ##> (fn thm => Thm.permute_prems 0 nn
    1.47 +            (if nn = 1 then thm RS mp
    1.48 +             else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm));
    1.49  
    1.50          val rel_eqs = map rel_eq_of_bnf pre_bnfs;
    1.51          val rel_monos = map rel_mono_of_bnf pre_bnfs;
    1.52          val dtor_coinducts =
    1.53            [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
    1.54        in
    1.55 -        map2 (postproc nn oo prove) dtor_coinducts goals
    1.56 +        map2 (postproc oo prove) dtor_coinducts goals
    1.57        end;
    1.58  
    1.59      fun mk_coinduct_concls ms discs ctrs =
    1.60 @@ -809,16 +811,21 @@
    1.61  
    1.62      val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
    1.63  
    1.64 -    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
    1.65 +    val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
    1.66 +    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
    1.67 +
    1.68      val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
    1.69      val coinduct_case_concl_attrs =
    1.70        map2 (fn casex => fn concls =>
    1.71            Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
    1.72          coinduct_cases coinduct_conclss;
    1.73 -    val coinduct_case_attrs =
    1.74 +
    1.75 +    val common_coinduct_attrs =
    1.76 +      common_coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    1.77 +    val coinduct_attrs =
    1.78        coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    1.79    in
    1.80 -    ((coinduct_thms_pairs, coinduct_case_attrs),
    1.81 +    ((coinduct_thms_pairs, (coinduct_attrs, common_coinduct_attrs)),
    1.82       (corec_thmss, code_nitpicksimp_attrs),
    1.83       (disc_corec_thmss, []),
    1.84       (disc_corec_iff_thmss, simp_attrs),
    1.85 @@ -1176,7 +1183,7 @@
    1.86                      ||>> mk_TFrees (live_of_bnf fp_bnf)
    1.87                      ||>> mk_TFrees (live_of_bnf fp_bnf);
    1.88                    val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf;
    1.89 -                  val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
    1.90 +                  val Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
    1.91                    val fTs = map2 (curry op -->) As Bs;
    1.92                    val ((fs, ta), names_lthy) = names_lthy
    1.93                      |> mk_Frees "f" fTs
    1.94 @@ -1466,7 +1473,7 @@
    1.95            (corecs, corec_defs)), lthy) =
    1.96        let
    1.97          val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
    1.98 -              coinduct_attrs),
    1.99 +              (coinduct_attrs, common_coinduct_attrs)),
   1.100               (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
   1.101               (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
   1.102            derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
   1.103 @@ -1487,8 +1494,8 @@
   1.104  
   1.105          val common_notes =
   1.106            (if nn > 1 then
   1.107 -             [(coinductN, [coinduct_thm], coinduct_attrs),
   1.108 -              (strong_coinductN, [strong_coinduct_thm], coinduct_attrs)]
   1.109 +             [(coinductN, [coinduct_thm], common_coinduct_attrs),
   1.110 +              (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
   1.111             else
   1.112               [])
   1.113            |> massage_simple_notes fp_common_name;
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jun 16 17:52:33 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jun 16 19:18:10 2014 +0200
     2.3 @@ -262,17 +262,16 @@
     2.4  val name_of_ctr = name_of_const "constructor";
     2.5  
     2.6  val notN = "not_";
     2.7 -val eqN = "eq_";
     2.8 -val neqN = "neq_";
     2.9 +val isN = "is_";
    2.10  
    2.11  fun name_of_disc t =
    2.12    (case head_of t of
    2.13      Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
    2.14      Long_Name.map_base_name (prefix notN) (name_of_disc t')
    2.15    | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
    2.16 -    Long_Name.map_base_name (prefix eqN) (name_of_disc t')
    2.17 +    Long_Name.map_base_name (prefix isN) (name_of_disc t')
    2.18    | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
    2.19 -    Long_Name.map_base_name (prefix neqN) (name_of_disc t')
    2.20 +    Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t')
    2.21    | t' => name_of_const "destructor" t');
    2.22  
    2.23  val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
     3.1 --- a/src/HOL/Transfer.thy	Mon Jun 16 17:52:33 2014 +0200
     3.2 +++ b/src/HOL/Transfer.thy	Mon Jun 16 19:18:10 2014 +0200
     3.3 @@ -246,7 +246,7 @@
     3.4  using assms by (auto simp add: eq_onp_def)
     3.5  
     3.6  lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
     3.7 -by (metis mem_Collect_eq subset_eq)
     3.8 +by auto
     3.9  
    3.10  ML_file "Tools/Transfer/transfer.ML"
    3.11  setup Transfer.setup