src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 57983 6edc3529bb4e
parent 57895 a85e0ab840c1
child 58117 9608028d8f43
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -69,15 +69,15 @@
     1.4     calls: corec_call list,
     1.5     discI: thm,
     1.6     sel_thms: thm list,
     1.7 -   disc_excludess: thm list list,
     1.8 +   distinct_discss: thm list list,
     1.9     collapse: thm,
    1.10     corec_thm: thm,
    1.11 -   disc_corec: thm,
    1.12 -   sel_corecs: thm list};
    1.13 +   corec_disc: thm,
    1.14 +   corec_sels: thm list};
    1.15  
    1.16  type corec_spec =
    1.17    {corec: term,
    1.18 -   disc_exhausts: thm list,
    1.19 +   exhaust_discs: thm list,
    1.20     sel_defs: thm list,
    1.21     fp_nesting_maps: thm list,
    1.22     fp_nesting_map_ident0s: thm list,
    1.23 @@ -159,7 +159,7 @@
    1.24              (case fastype_of1 (bound_Ts, nth args n) of
    1.25                Type (s, Ts) =>
    1.26                (case dest_case ctxt s Ts t of
    1.27 -                SOME ({sel_splits = _ :: _, ...}, conds', branches) =>
    1.28 +                SOME ({split_sels = _ :: _, ...}, conds', branches) =>
    1.29                  fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches)
    1.30                | _ => f conds t)
    1.31              | _ => f conds t)
    1.32 @@ -173,7 +173,7 @@
    1.33  
    1.34  fun case_of ctxt s =
    1.35    (case ctr_sugar_of ctxt s of
    1.36 -    SOME {casex = Const (s', _), sel_splits = _ :: _, ...} => SOME s'
    1.37 +    SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s'
    1.38    | _ => NONE);
    1.39  
    1.40  fun massage_let_if_case ctxt has_call massage_leaf =
    1.41 @@ -343,8 +343,8 @@
    1.42  
    1.43  fun case_thms_of_term ctxt t =
    1.44    let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in
    1.45 -    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #disc_exhausts ctr_sugars,
    1.46 -     maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
    1.47 +    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #exhaust_discs ctr_sugars,
    1.48 +     maps #split_sels ctr_sugars, maps #split_sel_asms ctr_sugars)
    1.49    end;
    1.50  
    1.51  fun basic_corec_specs_of ctxt res_T =
    1.52 @@ -444,32 +444,32 @@
    1.53           else No_Corec) g_i
    1.54        | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
    1.55  
    1.56 -    fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse
    1.57 -        corec_thm disc_corec sel_corecs =
    1.58 +    fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms distinct_discss collapse
    1.59 +        corec_thm corec_disc corec_sels =
    1.60        let val nullary = not (can dest_funT (fastype_of ctr)) in
    1.61          {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
    1.62           calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
    1.63 -         disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm,
    1.64 -         disc_corec = disc_corec, sel_corecs = sel_corecs}
    1.65 +         distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm,
    1.66 +         corec_disc = corec_disc, corec_sels = corec_sels}
    1.67        end;
    1.68  
    1.69 -    fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
    1.70 -        : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss =
    1.71 +    fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...}
    1.72 +        : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss =
    1.73        let val p_ios = map SOME p_is @ [NONE] in
    1.74          map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
    1.75 -          disc_excludesss collapses corec_thms disc_corecs sel_corecss
    1.76 +          distinct_discsss collapses corec_thms corec_discs corec_selss
    1.77        end;
    1.78  
    1.79 -    fun mk_spec ({T, ctr_sugar as {disc_exhausts, sel_defs, ...}, co_rec = corec,
    1.80 -        co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
    1.81 -        sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
    1.82 -      {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts,
    1.83 +    fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec,
    1.84 +        co_rec_thms = corec_thms, disc_co_recs = corec_discs,
    1.85 +        sel_co_recss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
    1.86 +      {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, exhaust_discs = exhaust_discs,
    1.87         sel_defs = sel_defs,
    1.88         fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
    1.89         fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
    1.90         fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
    1.91 -       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
    1.92 -         sel_corecss};
    1.93 +       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
    1.94 +         corec_selss};
    1.95    in
    1.96      ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
    1.97        co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
    1.98 @@ -993,8 +993,8 @@
    1.99        |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
   1.100          (ctr, map (K []) sels))) basic_ctr_specss);
   1.101  
   1.102 -    val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
   1.103 -          strong_coinduct_thms), lthy') =
   1.104 +    val ((n2m, corec_specs', _, coinduct_thm, coinduct_strong_thm, coinduct_thms,
   1.105 +          coinduct_strong_thms), lthy') =
   1.106        corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
   1.107      val corec_specs = take actual_nn corec_specs';
   1.108      val ctr_specss = map #ctr_specs corec_specs;
   1.109 @@ -1061,15 +1061,15 @@
   1.110          de_facto_exhaustives disc_eqnss
   1.111        |> list_all_fun_args []
   1.112      val nchotomy_taut_thmss =
   1.113 -      map5 (fn tac_opt => fn {disc_exhausts = res_disc_exhausts, ...} =>
   1.114 +      map5 (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} =>
   1.115            fn {code_rhs_opt, ...} :: _ => fn [] => K []
   1.116              | [goal] => fn true =>
   1.117                let
   1.118 -                val (_, _, arg_disc_exhausts, _, _) =
   1.119 +                val (_, _, arg_exhaust_discs, _, _) =
   1.120                    case_thms_of_term lthy (the_default Term.dummy code_rhs_opt);
   1.121                in
   1.122                  [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.123 -                   mk_primcorec_nchotomy_tac ctxt (res_disc_exhausts @ arg_disc_exhausts))
   1.124 +                   mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs))
   1.125                   |> Thm.close_derivation]
   1.126                end
   1.127              | false =>
   1.128 @@ -1133,7 +1133,7 @@
   1.129              []
   1.130            else
   1.131              let
   1.132 -              val {disc, disc_corec, ...} = nth ctr_specs ctr_no;
   1.133 +              val {disc, corec_disc, ...} = nth ctr_specs ctr_no;
   1.134                val k = 1 + ctr_no;
   1.135                val m = length prems;
   1.136                val goal =
   1.137 @@ -1146,7 +1146,7 @@
   1.138                if prems = [@{term False}] then
   1.139                  []
   1.140                else
   1.141 -                mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
   1.142 +                mk_primcorec_disc_tac lthy def_thms corec_disc k m excludesss
   1.143                  |> K |> Goal.prove_sorry lthy [] [] goal
   1.144                  |> Thm.close_derivation
   1.145                  |> pair (#disc (nth ctr_specs ctr_no))
   1.146 @@ -1163,8 +1163,8 @@
   1.147              val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs;
   1.148              val prems = the_default (maps (s_not_conj o #prems) disc_eqns)
   1.149                (find_first (curry (op =) ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
   1.150 -            val sel_corec = find_index (curry (op =) sel) (#sels ctr_spec)
   1.151 -              |> nth (#sel_corecs ctr_spec);
   1.152 +            val corec_sel = find_index (curry (op =) sel) (#sels ctr_spec)
   1.153 +              |> nth (#corec_sels ctr_spec);
   1.154              val k = 1 + ctr_no;
   1.155              val m = length prems;
   1.156              val goal =
   1.157 @@ -1174,10 +1174,10 @@
   1.158                |> HOLogic.mk_Trueprop o HOLogic.mk_eq
   1.159                |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
   1.160                |> curry Logic.list_all (map dest_Free fun_args);
   1.161 -            val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term;
   1.162 +            val (distincts, _, _, split_sels, split_sel_asms) = case_thms_of_term lthy rhs_term;
   1.163            in
   1.164 -            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms fp_nesting_maps
   1.165 -              fp_nesting_map_ident0s fp_nesting_map_comps sel_corec k m excludesss
   1.166 +            mk_primcorec_sel_tac lthy def_thms distincts split_sels split_sel_asms fp_nesting_maps
   1.167 +              fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss
   1.168              |> K |> Goal.prove_sorry lthy [] [] goal
   1.169              |> Thm.close_derivation
   1.170              |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
   1.171 @@ -1306,16 +1306,16 @@
   1.172                      val (raw_goal, goal) = (raw_rhs, rhs)
   1.173                        |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
   1.174                          #> curry Logic.list_all (map dest_Free fun_args));
   1.175 -                    val (distincts, discIs, _, sel_splits, sel_split_asms) =
   1.176 +                    val (distincts, discIs, _, split_sels, split_sel_asms) =
   1.177                        case_thms_of_term lthy raw_rhs;
   1.178  
   1.179 -                    val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs sel_splits
   1.180 -                        sel_split_asms ms ctr_thms
   1.181 +                    val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs split_sels
   1.182 +                        split_sel_asms ms ctr_thms
   1.183                          (if exhaustive_code then try the_single nchotomys else NONE)
   1.184                        |> K |> Goal.prove_sorry lthy [] [] raw_goal
   1.185                        |> Thm.close_derivation;
   1.186                    in
   1.187 -                    mk_primcorec_code_tac lthy distincts sel_splits raw_code_thm
   1.188 +                    mk_primcorec_code_tac lthy distincts split_sels raw_code_thm
   1.189                      |> K |> Goal.prove_sorry lthy [] [] goal
   1.190                      |> Thm.close_derivation
   1.191                      |> single
   1.192 @@ -1337,14 +1337,14 @@
   1.193              []
   1.194            else
   1.195              let
   1.196 -              val {disc, disc_excludess, ...} = nth ctr_specs ctr_no;
   1.197 +              val {disc, distinct_discss, ...} = nth ctr_specs ctr_no;
   1.198                val goal =
   1.199                  mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc,
   1.200                    mk_conjs prems)
   1.201                  |> curry Logic.list_all (map dest_Free fun_args);
   1.202              in
   1.203                mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
   1.204 -                (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
   1.205 +                (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
   1.206                |> K |> Goal.prove_sorry lthy [] [] goal
   1.207                |> Thm.close_derivation
   1.208                |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
   1.209 @@ -1385,7 +1385,7 @@
   1.210             (exhaustN, nontriv_exhaust_thmss, []),
   1.211             (selN, sel_thmss, simp_attrs),
   1.212             (simpsN, simp_thmss, []),
   1.213 -           (strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]
   1.214 +           (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms, [])]
   1.215            |> maps (fn (thmN, thmss, attrs) =>
   1.216              map2 (fn fun_name => fn thms =>
   1.217                  ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))
   1.218 @@ -1394,7 +1394,7 @@
   1.219  
   1.220          val common_notes =
   1.221            [(coinductN, if n2m then [coinduct_thm] else [], []),
   1.222 -           (strong_coinductN, if n2m then [strong_coinduct_thm] else [], [])]
   1.223 +           (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], [])]
   1.224            |> filter_out (null o #2)
   1.225            |> map (fn (thmN, thms, attrs) =>
   1.226              ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));