set up things for (co)induction sugar
authorblanchet
Wed Sep 12 17:26:05 2012 +0200 (2012-09-12)
changeset 49337538687a77075
parent 49336 a2e6473145e4
child 49338 4a922800531d
set up things for (co)induction sugar
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
src/HOL/Codatatype/Tools/bnf_util.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 17:26:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 17:26:05 2012 +0200
     1.3 @@ -10,16 +10,16 @@
     1.4    val datatyp: bool ->
     1.5      (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
     1.6        BNF_Def.BNF list -> local_theory ->
     1.7 -      (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
     1.8 -         thm list) * local_theory) ->
     1.9 +      (term list * term list * term list * term list * thm * thm list * thm list * thm list *
    1.10 +         thm list * thm list) * local_theory) ->
    1.11      bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
    1.12        (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
    1.13      local_theory -> local_theory
    1.14    val parse_datatype_cmd: bool ->
    1.15      (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
    1.16        BNF_Def.BNF list -> local_theory ->
    1.17 -      (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
    1.18 -         thm list) * local_theory) ->
    1.19 +      (term list * term list * term list * term list * thm * thm list * thm list * thm list *
    1.20 +         thm list * thm list) * local_theory) ->
    1.21      (local_theory -> local_theory) parser
    1.22  end;
    1.23  
    1.24 @@ -33,10 +33,12 @@
    1.25  open BNF_FP_Sugar_Tactics
    1.26  
    1.27  val caseN = "case";
    1.28 +val coinductsN = "coinducts";
    1.29  val coitersN = "coiters";
    1.30  val corecsN = "corecs";
    1.31  val disc_coitersN = "disc_coiters";
    1.32  val disc_corecsN = "disc_corecs";
    1.33 +val inductsN = "inducts";
    1.34  val itersN = "iters";
    1.35  val recsN = "recs";
    1.36  val sel_coitersN = "sel_coiters";
    1.37 @@ -131,6 +133,8 @@
    1.38          unsorted_As);
    1.39  
    1.40      val fp_bs = map type_binding_of specs;
    1.41 +    val fp_common_name = mk_common_name fp_bs;
    1.42 +
    1.43      val fake_Ts = map mk_fake_T fp_bs;
    1.44  
    1.45      val mixfixes = map mixfix_of specs;
    1.46 @@ -179,7 +183,7 @@
    1.47      val fp_eqs =
    1.48        map dest_TFree Bs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsBs;
    1.49  
    1.50 -    val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
    1.51 +    val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, fp_induct, unf_flds, fld_unfs, fld_injects,
    1.52          fp_iter_thms, fp_rec_thms), lthy)) =
    1.53        fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
    1.54  
    1.55 @@ -517,15 +521,22 @@
    1.56          val args = map build_arg TUs;
    1.57        in Term.list_comb (mapx, args) end;
    1.58  
    1.59 -    fun derive_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs,
    1.60 -        rec_defs), lthy) =
    1.61 +    fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _,
    1.62 +        iter_defs, rec_defs), lthy) =
    1.63        let
    1.64 -        val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
    1.65 -        val giters = map (lists_bmoc gss) iters;
    1.66 -        val hrecs = map (lists_bmoc hss) recs;
    1.67 +        val (induct_thms, induct_thm) =
    1.68 +          let
    1.69 +            val induct_thm = fp_induct;
    1.70 +          in
    1.71 +            `(conj_dests N) induct_thm
    1.72 +          end;
    1.73  
    1.74          val (iter_thmss, rec_thmss) =
    1.75            let
    1.76 +            val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
    1.77 +            val giters = map (lists_bmoc gss) iters;
    1.78 +            val hrecs = map (lists_bmoc hss) recs;
    1.79 +
    1.80              fun mk_goal_iter_like fss fiter_like xctr f xs fxs =
    1.81                fold_rev (fold_rev Logic.all) (xs :: fss)
    1.82                  (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
    1.83 @@ -567,6 +578,12 @@
    1.84                 goal_recss rec_tacss)
    1.85            end;
    1.86  
    1.87 +        val common_notes =
    1.88 +          [(inductN, [induct_thm], []), (*### attribs *)
    1.89 +           (inductsN, induct_thms, [])] (*### attribs *)
    1.90 +          |> map (fn (thmN, thms, attrs) =>
    1.91 +              ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
    1.92 +
    1.93          val notes =
    1.94            [(itersN, iter_thmss, simp_attrs),
    1.95             (recsN, rec_thmss, Code.add_default_eqn_attrib :: simp_attrs)]
    1.96 @@ -575,19 +592,25 @@
    1.97                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
    1.98                  [(thms, [])])) fp_bs thmss);
    1.99        in
   1.100 -        lthy |> Local_Theory.notes notes |> snd
   1.101 +        lthy |> Local_Theory.notes (common_notes @ notes) |> snd
   1.102        end;
   1.103  
   1.104 -    fun derive_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _, ctr_defss,
   1.105 -        discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
   1.106 +    fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _,
   1.107 +        ctr_defss, discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
   1.108        let
   1.109 -        val z = the_single zs;
   1.110 -
   1.111 -        val gcoiters = map (lists_bmoc pgss) coiters;
   1.112 -        val hcorecs = map (lists_bmoc phss) corecs;
   1.113 +        val (coinduct_thms, coinduct_thm) =
   1.114 +          let
   1.115 +            val coinduct_thm = fp_induct;
   1.116 +          in
   1.117 +            `(conj_dests N) coinduct_thm
   1.118 +          end;
   1.119  
   1.120          val (coiter_thmss, corec_thmss) =
   1.121            let
   1.122 +            val z = the_single zs;
   1.123 +            val gcoiters = map (lists_bmoc pgss) coiters;
   1.124 +            val hcorecs = map (lists_bmoc phss) corecs;
   1.125 +
   1.126              fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
   1.127  
   1.128              fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' =
   1.129 @@ -684,7 +707,8 @@
   1.130          fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
   1.131          ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
   1.132        |>> split_list |> wrap_types_and_define_iter_likes
   1.133 -      |> (if lfp then derive_iter_rec_thms_for_types else derive_coiter_corec_thms_for_types);
   1.134 +      |> (if lfp then derive_induct_iter_rec_thms_for_types
   1.135 +          else derive_coinduct_coiter_corec_thms_for_types);
   1.136  
   1.137      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
   1.138        (if lfp then "" else "co") ^ "datatype"));
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 17:26:05 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 17:26:05 2012 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4    val mk_set_minimalN: int -> string
     2.5    val mk_set_inductN: int -> string
     2.6  
     2.7 -  val mk_bundle_name: binding list -> string
     2.8 +  val mk_common_name: binding list -> string
     2.9  
    2.10    val split_conj_thm: thm -> thm list
    2.11    val split_conj_prems: int -> thm -> thm
    2.12 @@ -214,7 +214,7 @@
    2.13  val set_inclN = "set_incl"
    2.14  val set_set_inclN = "set_set_incl"
    2.15  
    2.16 -val mk_bundle_name = space_implode "_" o map Binding.name_of;
    2.17 +val mk_common_name = space_implode "_" o map Binding.name_of;
    2.18  
    2.19  fun mk_predT T = T --> HOLogic.boolT;
    2.20  
    2.21 @@ -347,7 +347,7 @@
    2.22  
    2.23  fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
    2.24    let
    2.25 -    val name = mk_bundle_name bs;
    2.26 +    val name = mk_common_name bs;
    2.27      fun qualify i bind =
    2.28        let val namei = if i > 0 then name ^ string_of_int i else name;
    2.29        in
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 17:26:05 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 17:26:05 2012 +0200
     3.3 @@ -11,8 +11,8 @@
     3.4  sig
     3.5    val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
     3.6      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     3.7 -    (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
     3.8 -      thm list) * local_theory
     3.9 +    (term list * term list * term list * term list * thm * thm list * thm list * thm list *
    3.10 +      thm list * thm list) * local_theory
    3.11  end;
    3.12  
    3.13  structure BNF_GFP : BNF_GFP =
    3.14 @@ -64,7 +64,7 @@
    3.15      val ks = 1 upto n;
    3.16      val m = live - n (*passive, if 0 don't generate a new bnf*);
    3.17      val ls = 1 upto m;
    3.18 -    val b = Binding.name (mk_bundle_name bs);
    3.19 +    val b = Binding.name (mk_common_name bs);
    3.20  
    3.21      (* TODO: check if m, n etc are sane *)
    3.22  
    3.23 @@ -2974,8 +2974,8 @@
    3.24              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    3.25            bs thmss)
    3.26    in
    3.27 -    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, fld_coiter_thms,
    3.28 -      fld_corec_thms),
    3.29 +    ((unfs, flds, coiters, corecs, unf_coinduct_thm, unf_fld_thms, fld_unf_thms, fld_inject_thms,
    3.30 +      fld_coiter_thms, fld_corec_thms),
    3.31       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    3.32    end;
    3.33  
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 17:26:05 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 17:26:05 2012 +0200
     4.3 @@ -10,8 +10,8 @@
     4.4  sig
     4.5    val bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
     4.6      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     4.7 -    (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
     4.8 -      thm list) * local_theory
     4.9 +    (term list * term list * term list * term list * thm * thm list * thm list * thm list *
    4.10 +      thm list * thm list) * local_theory
    4.11  end;
    4.12  
    4.13  structure BNF_LFP : BNF_LFP =
    4.14 @@ -33,7 +33,7 @@
    4.15      val n = length bnfs; (*active*)
    4.16      val ks = 1 upto n;
    4.17      val m = live - n; (*passive, if 0 don't generate a new bnf*)
    4.18 -    val b = Binding.name (mk_bundle_name bs);
    4.19 +    val b = Binding.name (mk_common_name bs);
    4.20  
    4.21      (* TODO: check if m, n etc are sane *)
    4.22  
    4.23 @@ -1810,7 +1810,8 @@
    4.24              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    4.25            bs thmss)
    4.26    in
    4.27 -    ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms, iter_thms, rec_thms),
    4.28 +    ((unfs, flds, iters, recs, fld_induct_thm, unf_fld_thms, fld_unf_thms, fld_inject_thms,
    4.29 +      iter_thms, rec_thms),
    4.30       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    4.31    end;
    4.32  
     5.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Wed Sep 12 17:26:05 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Wed Sep 12 17:26:05 2012 +0200
     5.3 @@ -106,6 +106,7 @@
     5.4    val mk_Un_upper: int -> int -> thm
     5.5    val mk_conjIN: int -> thm
     5.6    val mk_conjunctN: int -> int -> thm
     5.7 +  val conj_dests: int -> thm -> thm list
     5.8    val mk_disjIN: int -> int -> thm
     5.9    val mk_nthI: int -> int -> thm
    5.10    val mk_nth_conv: int -> int -> thm
    5.11 @@ -513,6 +514,8 @@
    5.12    | mk_conjunctN 2 2 = conjunct2
    5.13    | mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1));
    5.14  
    5.15 +fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n);
    5.16 +
    5.17  fun mk_conjIN 1 = @{thm TrueE[OF TrueI]}
    5.18    | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI);
    5.19