enriched data structure with necessary theorems
authorblanchet
Mon Sep 09 13:47:58 2013 +0200 (2013-09-09)
changeset 53475185ad6cf6576
parent 53474 077a2758ceb4
child 53476 eb3865c3ee58
enriched data structure with necessary theorems
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Sun Sep 08 19:25:06 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
     1.3 @@ -23,7 +23,11 @@
     1.4       split_asm: thm,
     1.5       disc_thmss: thm list list,
     1.6       discIs: thm list,
     1.7 -     sel_thmss: thm list list};
     1.8 +     sel_thmss: thm list list,
     1.9 +     disc_exhausts: thm list,
    1.10 +     collapses: thm list,
    1.11 +     expands: thm list,
    1.12 +     case_convs: thm list};
    1.13  
    1.14    val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
    1.15  
    1.16 @@ -68,10 +72,15 @@
    1.17     split_asm: thm,
    1.18     disc_thmss: thm list list,
    1.19     discIs: thm list,
    1.20 -   sel_thmss: thm list list};
    1.21 +   sel_thmss: thm list list,
    1.22 +   disc_exhausts: thm list,
    1.23 +   collapses: thm list,
    1.24 +   expands: thm list,
    1.25 +   case_convs: thm list};
    1.26  
    1.27  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    1.28 -    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss} =
    1.29 +    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    1.30 +    disc_exhausts, collapses, expands, case_convs} =
    1.31    {ctrs = map (Morphism.term phi) ctrs,
    1.32     casex = Morphism.term phi casex,
    1.33     discs = map (Morphism.term phi) discs,
    1.34 @@ -87,7 +96,11 @@
    1.35     split_asm = Morphism.thm phi split_asm,
    1.36     disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    1.37     discIs = map (Morphism.thm phi) discIs,
    1.38 -   sel_thmss = map (map (Morphism.thm phi)) sel_thmss};
    1.39 +   sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
    1.40 +   disc_exhausts = map (Morphism.thm phi) disc_exhausts,
    1.41 +   collapses = map (Morphism.thm phi) collapses,
    1.42 +   expands = map (Morphism.thm phi) expands,
    1.43 +   case_convs = map (Morphism.thm phi) case_convs};
    1.44  
    1.45  val rep_compat_prefix = "new";
    1.46  
    1.47 @@ -762,7 +775,8 @@
    1.48            nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
    1.49            case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
    1.50            split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
    1.51 -          discIs = discI_thms, sel_thmss = sel_thmss},
    1.52 +          discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
    1.53 +          collapses = collapse_thms, expands = expand_thms, case_convs = case_conv_thms},
    1.54           lthy
    1.55           |> not rep_compat ?
    1.56              (Local_Theory.declaration {syntax = false, pervasive = true}
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Sep 08 19:25:06 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
     2.3 @@ -19,7 +19,9 @@
     2.4       ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
     2.5       co_iterss: term list list,
     2.6       co_inducts: thm list,
     2.7 -     co_iter_thmsss: thm list list list};
     2.8 +     co_iter_thmsss: thm list list list,
     2.9 +     disc_co_itersss: thm list list list,
    2.10 +     sel_co_iterssss: thm list list list list};
    2.11  
    2.12    val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
    2.13    val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
    2.14 @@ -80,7 +82,7 @@
    2.15      * (thm list list * thm list list * Args.src list)
    2.16      * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    2.17      * (thm list list * thm list list * Args.src list)
    2.18 -    * (thm list list * thm list list * Args.src list)
    2.19 +    * (thm list list list * thm list list list * Args.src list)
    2.20  
    2.21    val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    2.22        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    2.23 @@ -119,7 +121,9 @@
    2.24     ctr_sugars: ctr_sugar list,
    2.25     co_iterss: term list list,
    2.26     co_inducts: thm list,
    2.27 -   co_iter_thmsss: thm list list list};
    2.28 +   co_iter_thmsss: thm list list list,
    2.29 +   disc_co_itersss: thm list list list,
    2.30 +   sel_co_iterssss: thm list list list list};
    2.31  
    2.32  fun of_fp_sugar f (fp_sugar as {index, ...}) = nth (f fp_sugar) index;
    2.33  
    2.34 @@ -128,7 +132,7 @@
    2.35    T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
    2.36  
    2.37  fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
    2.38 -    ctr_sugars, co_iterss, co_inducts, co_iter_thmsss} =
    2.39 +    ctr_sugars, co_iterss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
    2.40    {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    2.41      nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    2.42     fp_res = morph_fp_result phi fp_res,
    2.43 @@ -136,7 +140,9 @@
    2.44     ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    2.45     co_iterss = map (map (Morphism.term phi)) co_iterss,
    2.46     co_inducts = map (Morphism.thm phi) co_inducts,
    2.47 -   co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss};
    2.48 +   co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
    2.49 +   disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
    2.50 +   sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
    2.51  
    2.52  structure Data = Generic_Data
    2.53  (
    2.54 @@ -161,13 +167,14 @@
    2.55      (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
    2.56  
    2.57  fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
    2.58 -    ctr_sugars co_iterss co_inducts co_iter_thmsss lthy =
    2.59 +    ctr_sugars co_iterss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
    2.60    (0, lthy)
    2.61    |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
    2.62      register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs,
    2.63          nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res,
    2.64          ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss,
    2.65 -        co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss}
    2.66 +        co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
    2.67 +        sel_co_iterssss = sel_co_iterssss}
    2.68        lthy)) Ts
    2.69    |> snd;
    2.70  
    2.71 @@ -999,10 +1006,10 @@
    2.72        end;
    2.73  
    2.74      fun mk_sel_coiter_thms coiter_thmss =
    2.75 -      map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss |> map flat;
    2.76 +      map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss;
    2.77  
    2.78 -    val sel_unfold_thmss = mk_sel_coiter_thms unfold_thmss;
    2.79 -    val sel_corec_thmss = mk_sel_coiter_thms corec_thmss;
    2.80 +    val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss;
    2.81 +    val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss;
    2.82  
    2.83      val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
    2.84      val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
    2.85 @@ -1018,7 +1025,7 @@
    2.86       (safe_unfold_thmss, safe_corec_thmss),
    2.87       (disc_unfold_thmss, disc_corec_thmss, simp_attrs),
    2.88       (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
    2.89 -     (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
    2.90 +     (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
    2.91    end;
    2.92  
    2.93  fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
    2.94 @@ -1435,7 +1442,7 @@
    2.95          lthy
    2.96          |> Local_Theory.notes (common_notes @ notes) |> snd
    2.97          |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
    2.98 -          iterss [induct_thm] (transpose [fold_thmss, rec_thmss])
    2.99 +          iterss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
   2.100        end;
   2.101  
   2.102      fun derive_and_note_coinduct_coiters_thms_for_types
   2.103 @@ -1448,11 +1455,14 @@
   2.104               (safe_unfold_thmss, safe_corec_thmss),
   2.105               (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
   2.106               (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
   2.107 -             (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
   2.108 +             (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
   2.109            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
   2.110              dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
   2.111              ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
   2.112  
   2.113 +        val sel_unfold_thmss = map flat sel_unfold_thmsss;
   2.114 +        val sel_corec_thmss = map flat sel_corec_thmsss;
   2.115 +
   2.116          val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
   2.117  
   2.118          fun flat_coiter_thms coiters disc_coiters sel_coiters =
   2.119 @@ -1495,7 +1505,8 @@
   2.120          |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
   2.121          |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
   2.122            ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm]
   2.123 -          (transpose [unfold_thmss, corec_thmss])
   2.124 +          (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
   2.125 +          (transpose [sel_unfold_thmsss, sel_corec_thmsss])
   2.126        end;
   2.127  
   2.128      val lthy'' = lthy'
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Sun Sep 08 19:25:06 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
     3.3 @@ -145,19 +145,23 @@
     3.4  
     3.5        val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
     3.6  
     3.7 -      val (co_inducts, un_fold_thmss, co_rec_thmss) =
     3.8 +      val (co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
     3.9 +           sel_unfold_thmsss, sel_corec_thmsss) =
    3.10          if fp = Least_FP then
    3.11            derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
    3.12              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
    3.13              co_iterss co_iter_defss lthy
    3.14            |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
    3.15 -            ([induct], fold_thmss, rec_thmss))
    3.16 +            ([induct], fold_thmss, rec_thmss, [], [], [], []))
    3.17          else
    3.18            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
    3.19              dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
    3.20              ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
    3.21 -          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, _, _) =>
    3.22 -            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss));
    3.23 +          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _,
    3.24 +                  (disc_unfold_thmss, disc_corec_thmss, _),
    3.25 +                  (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
    3.26 +            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
    3.27 +             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));
    3.28  
    3.29        val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
    3.30  
    3.31 @@ -165,7 +169,9 @@
    3.32          {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
    3.33           nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
    3.34           ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss,
    3.35 -         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss]}
    3.36 +         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
    3.37 +         disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
    3.38 +         sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
    3.39          |> morph_fp_sugar phi;
    3.40      in
    3.41        ((true, map_index mk_target_fp_sugar fpTs), lthy)
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Sep 08 19:25:06 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Sep 09 13:47:58 2013 +0200
     4.3 @@ -31,7 +31,10 @@
     4.4       sels: term list,
     4.5       pred: int option,
     4.6       calls: corec_call list,
     4.7 -     corec_thm: thm}
     4.8 +     collapse: thm,
     4.9 +     corec_thm: thm,
    4.10 +     disc_corec: thm,
    4.11 +     sel_corecs: thm list}
    4.12  
    4.13    type rec_spec =
    4.14      {recx: term,
    4.15 @@ -41,6 +44,9 @@
    4.16  
    4.17    type corec_spec =
    4.18      {corec: term,
    4.19 +     nested_maps: thm list,
    4.20 +     nested_map_idents: thm list,
    4.21 +     nested_map_comps: thm list,
    4.22       ctr_specs: corec_ctr_spec list}
    4.23  
    4.24    val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
    4.25 @@ -90,7 +96,10 @@
    4.26     sels: term list,
    4.27     pred: int option,
    4.28     calls: corec_call list,
    4.29 -   corec_thm: thm};
    4.30 +   collapse: thm,
    4.31 +   corec_thm: thm,
    4.32 +   disc_corec: thm,
    4.33 +   sel_corecs: thm list};
    4.34  
    4.35  type rec_spec =
    4.36    {recx: term,
    4.37 @@ -100,6 +109,9 @@
    4.38  
    4.39  type corec_spec =
    4.40    {corec: term,
    4.41 +   nested_maps: thm list,
    4.42 +   nested_map_idents: thm list,
    4.43 +   nested_map_comps: thm list,
    4.44     ctr_specs: corec_ctr_spec list};
    4.45  
    4.46  val id_def = @{thm id_def};
    4.47 @@ -348,7 +360,7 @@
    4.48      val thy = Proof_Context.theory_of lthy;
    4.49  
    4.50      val ((nontriv, missing_res_Ts, perm0_kks,
    4.51 -          fp_sugars as {fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
    4.52 +          fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
    4.53            co_inducts = coinduct_thms, ...} :: _), lthy') =
    4.54        nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
    4.55  
    4.56 @@ -407,27 +419,38 @@
    4.57           else No_Corec) g_i
    4.58        | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
    4.59  
    4.60 -    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss corec_thm =
    4.61 +    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs =
    4.62        let val nullary = not (can dest_funT (fastype_of ctr)) in
    4.63          {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
    4.64 -         calls = map3 (call_of nullary) q_iss f_iss f_Tss, corec_thm = corec_thm}
    4.65 +         calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse,
    4.66 +         corec_thm = corec_thm, disc_corec = disc_corec, sel_corecs = sel_corecs}
    4.67        end;
    4.68  
    4.69 -    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss =
    4.70 +    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
    4.71 +        sel_coiterssss =
    4.72        let
    4.73          val ctrs = #ctrs (nth ctr_sugars index);
    4.74          val discs = #discs (nth ctr_sugars index);
    4.75          val selss = #selss (nth ctr_sugars index);
    4.76          val p_ios = map SOME p_is @ [NONE];
    4.77 -        val corec_thmss = co_rec_of (nth coiter_thmsss index);
    4.78 +        val collapses = #collapses (nth ctr_sugars index);
    4.79 +        val corec_thms = co_rec_of (nth coiter_thmsss index);
    4.80 +        val disc_corecs = co_rec_of (nth disc_coitersss index);
    4.81 +        val sel_corecss = co_rec_of (nth sel_coiterssss index);
    4.82        in
    4.83 -        map8 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss corec_thmss
    4.84 +        map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
    4.85 +          disc_corecs sel_corecss
    4.86        end;
    4.87  
    4.88 -    fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, ...}
    4.89 +    fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
    4.90 +          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...}
    4.91          p_is q_isss f_isss f_Tsss =
    4.92        {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
    4.93 -       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss};
    4.94 +       nested_maps = [] (*FIXME*),
    4.95 +       nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
    4.96 +       nested_map_comps = map map_comp_of_bnf nested_bnfs,
    4.97 +       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
    4.98 +         disc_coitersss sel_coiterssss};
    4.99    in
   4.100      ((nontriv, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
   4.101        co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,