src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 57983 6edc3529bb4e
parent 57932 c29659f77f8d
child 57987 ecb227b40907
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -99,13 +99,13 @@
     1.4  val EqN = "Eq_";
     1.5  
     1.6  val corec_codeN = "corec_code";
     1.7 -val disc_map_iffN = "disc_map_iff";
     1.8 -val sel_mapN = "sel_map";
     1.9 -val sel_setN = "sel_set";
    1.10 +val map_disc_iffN = "map_disc_iff";
    1.11 +val map_selN = "map_sel";
    1.12  val set_casesN = "set_cases";
    1.13  val set_emptyN = "set_empty";
    1.14  val set_introsN = "set_intros";
    1.15  val set_inductN = "set_induct";
    1.16 +val set_selN = "set_sel";
    1.17  
    1.18  structure Data = Generic_Data
    1.19  (
    1.20 @@ -309,14 +309,14 @@
    1.21    * (thm list list list * Args.src list);
    1.22  
    1.23  fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
    1.24 -    corecss, disc_corecss, (disc_corec_iffss, disc_corec_iff_attrs),
    1.25 -    (sel_corecsss, sel_corec_attrs)) =
    1.26 +    corecss, corec_discss, (corec_disc_iffss, corec_disc_iff_attrs),
    1.27 +    (corec_selsss, corec_sel_attrs)) =
    1.28    ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
    1.29      coinduct_attrs_pair),
    1.30     map (map (Morphism.thm phi)) corecss,
    1.31 -   map (map (Morphism.thm phi)) disc_corecss,
    1.32 -   (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
    1.33 -   (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms;
    1.34 +   map (map (Morphism.thm phi)) corec_discss,
    1.35 +   (map (map (Morphism.thm phi)) corec_disc_iffss, corec_disc_iff_attrs),
    1.36 +   (map (map (map (Morphism.thm phi))) corec_selsss, corec_sel_attrs)) : gfp_sugar_thms;
    1.37  
    1.38  val transfer_gfp_sugar_thms =
    1.39    morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
    1.40 @@ -961,7 +961,7 @@
    1.41          val rel_eqs = map rel_eq_of_bnf pre_bnfs;
    1.42          val rel_monos = map rel_mono_of_bnf pre_bnfs;
    1.43          val dtor_coinducts =
    1.44 -          [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
    1.45 +          [dtor_coinduct, mk_coinduct_strong_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
    1.46        in
    1.47          map2 (postproc_co_induct lthy nn mp mp_conj oo prove) dtor_coinducts goals
    1.48        end;
    1.49 @@ -1010,7 +1010,7 @@
    1.50          |> map (map (unfold_thms lthy @{thms case_sum_if}))
    1.51        end;
    1.52  
    1.53 -    val disc_corec_iff_thmss =
    1.54 +    val corec_disc_iff_thmss =
    1.55        let
    1.56          fun mk_goal c cps gcorec n k disc =
    1.57            mk_Trueprop_eq (disc $ (gcorec $ c),
    1.58 @@ -1023,7 +1023,7 @@
    1.59  
    1.60          val case_splitss' = map (map mk_case_split') cpss;
    1.61  
    1.62 -        val tacss = map3 (map oo mk_disc_corec_iff_tac) case_splitss' corec_thmss disc_thmsss;
    1.63 +        val tacss = map3 (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
    1.64  
    1.65          fun prove goal tac =
    1.66            Goal.prove_sorry lthy [] [] goal (tac o #context)
    1.67 @@ -1037,11 +1037,11 @@
    1.68          map2 proves goalss tacss
    1.69        end;
    1.70  
    1.71 -    fun mk_disc_corec_thms corecs discIs = map (op RS) (corecs ~~ discIs);
    1.72 +    fun mk_corec_disc_thms corecs discIs = map (op RS) (corecs ~~ discIs);
    1.73  
    1.74 -    val disc_corec_thmss = map2 mk_disc_corec_thms corec_thmss discIss;
    1.75 +    val corec_disc_thmss = map2 mk_corec_disc_thms corec_thmss discIss;
    1.76  
    1.77 -    fun mk_sel_corec_thm corec_thm sel sel_thm =
    1.78 +    fun mk_corec_sel_thm corec_thm sel sel_thm =
    1.79        let
    1.80          val (domT, ranT) = dest_funT (fastype_of sel);
    1.81          val arg_cong' =
    1.82 @@ -1053,17 +1053,17 @@
    1.83          corec_thm RS arg_cong' RS sel_thm'
    1.84        end;
    1.85  
    1.86 -    fun mk_sel_corec_thms corec_thmss =
    1.87 -      map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
    1.88 +    fun mk_corec_sel_thms corec_thmss =
    1.89 +      map3 (map3 (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss;
    1.90  
    1.91 -    val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
    1.92 +    val corec_sel_thmsss = mk_corec_sel_thms corec_thmss;
    1.93    in
    1.94      ((coinduct_thms_pairs,
    1.95        mk_coinduct_attributes fpTs (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss),
    1.96       corec_thmss,
    1.97 -     disc_corec_thmss,
    1.98 -     (disc_corec_iff_thmss, simp_attrs),
    1.99 -     (sel_corec_thmsss, simp_attrs))
   1.100 +     corec_disc_thmss,
   1.101 +     (corec_disc_iff_thmss, simp_attrs),
   1.102 +     (corec_sel_thmsss, simp_attrs))
   1.103    end;
   1.104  
   1.105  fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
   1.106 @@ -1498,7 +1498,7 @@
   1.107                  map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
   1.108                    rel_inject_thms ms;
   1.109  
   1.110 -              val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
   1.111 +              val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
   1.112                     (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) =
   1.113                  let
   1.114                    val live_AsBs = filter (op <>) (As ~~ Bs);
   1.115 @@ -1702,7 +1702,7 @@
   1.116                        (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
   1.117                      end;
   1.118  
   1.119 -                  val disc_map_iff_thms =
   1.120 +                  val map_disc_iff_thms =
   1.121                      let
   1.122                        val discsB = map (mk_disc_or_sel Bs) discs;
   1.123                        val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs;
   1.124 @@ -1721,14 +1721,14 @@
   1.125                        else
   1.126                          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   1.127                            (fn {context = ctxt, prems = _} =>
   1.128 -                            mk_disc_map_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
   1.129 +                            mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
   1.130                                map_thms)
   1.131                          |> Conjunction.elim_balanced (length goals)
   1.132                          |> Proof_Context.export names_lthy lthy
   1.133                          |> map Thm.close_derivation
   1.134                      end;
   1.135  
   1.136 -                  val sel_map_thms =
   1.137 +                  val map_sel_thms =
   1.138                      let
   1.139                        fun mk_goal (discA, selA) =
   1.140                          let
   1.141 @@ -1755,14 +1755,14 @@
   1.142                        else
   1.143                          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   1.144                            (fn {context = ctxt, prems = _} =>
   1.145 -                            mk_sel_map_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
   1.146 +                            mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
   1.147                                map_thms (flat sel_thmss))
   1.148                          |> Conjunction.elim_balanced (length goals)
   1.149                          |> Proof_Context.export names_lthy lthy
   1.150                          |> map Thm.close_derivation
   1.151                      end;
   1.152  
   1.153 -                  val sel_set_thms =
   1.154 +                  val set_sel_thms =
   1.155                      let
   1.156                        fun mk_goal discA selA setA ctxt =
   1.157                          let
   1.158 @@ -1819,14 +1819,14 @@
   1.159                        else
   1.160                          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   1.161                            (fn {context = ctxt, prems = _} =>
   1.162 -                             mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
   1.163 +                             mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
   1.164                                 (flat sel_thmss) set0_thms)
   1.165                          |> Conjunction.elim_balanced (length goals)
   1.166                          |> Proof_Context.export names_lthy lthy
   1.167                          |> map Thm.close_derivation
   1.168                      end;
   1.169                  in
   1.170 -                  (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
   1.171 +                  (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
   1.172                      (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs))
   1.173                  end;
   1.174  
   1.175 @@ -1836,19 +1836,19 @@
   1.176                  |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   1.177  
   1.178                val notes =
   1.179 -                [(disc_map_iffN, disc_map_iff_thms, K simp_attrs),
   1.180 -                 (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
   1.181 +                [(mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
   1.182 +                 (map_disc_iffN, map_disc_iff_thms, K simp_attrs),
   1.183 +                 (map_selN, map_sel_thms, K []),
   1.184                   (rel_casesN, [rel_cases_thm], K rel_cases_attrs),
   1.185                   (rel_distinctN, rel_distinct_thms, K simp_attrs),
   1.186                   (rel_injectN, rel_inject_thms, K simp_attrs),
   1.187                   (rel_introsN, rel_intro_thms, K []),
   1.188                   (rel_selN, rel_sel_thms, K []),
   1.189                   (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
   1.190 -                 (sel_mapN, sel_map_thms, K []),
   1.191 -                 (sel_setN, sel_set_thms, K []),
   1.192                   (set_casesN, set_cases_thms, nth set_cases_attrss),
   1.193                   (set_emptyN, set_empty_thms, K []),
   1.194 -                 (set_introsN, set_intros_thms, K [])]
   1.195 +                 (set_introsN, set_intros_thms, K []),
   1.196 +                 (set_selN, set_sel_thms, K [])]
   1.197                  |> massage_simple_notes fp_b_name;
   1.198  
   1.199                val (noted, lthy') =
   1.200 @@ -1948,10 +1948,10 @@
   1.201          ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
   1.202            (corecs, corec_defs)), lthy) =
   1.203        let
   1.204 -        val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
   1.205 +        val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)],
   1.206                (coinduct_attrs, common_coinduct_attrs)),
   1.207 -             corec_thmss, disc_corec_thmss,
   1.208 -             (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
   1.209 +             corec_thmss, corec_disc_thmss,
   1.210 +             (corec_disc_iff_thmss, corec_disc_iff_attrs), (corec_sel_thmsss, corec_sel_attrs)) =
   1.211            derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
   1.212              dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
   1.213              ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
   1.214 @@ -1969,7 +1969,7 @@
   1.215                    [thm, eq_ifIN ctxt thms]));
   1.216  
   1.217          val corec_code_thms = map (eq_ifIN lthy) corec_thmss;
   1.218 -        val sel_corec_thmss = map flat sel_corec_thmsss;
   1.219 +        val corec_sel_thmss = map flat corec_sel_thmsss;
   1.220  
   1.221          val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
   1.222          val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
   1.223 @@ -2001,39 +2001,39 @@
   1.224  
   1.225          val simp_thmss =
   1.226            map6 mk_simp_thms ctr_sugars
   1.227 -            (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
   1.228 +            (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
   1.229              mapss rel_injectss rel_distinctss setss;
   1.230  
   1.231          val common_notes =
   1.232            (set_inductN, set_induct_thms, nth set_induct_attrss) ::
   1.233            (if nn > 1 then
   1.234              [(coinductN, [coinduct_thm], K common_coinduct_attrs),
   1.235 -             (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs),
   1.236 -             (strong_coinductN, [strong_coinduct_thm], K common_coinduct_attrs)]
   1.237 +             (coinduct_strongN, [coinduct_strong_thm], K common_coinduct_attrs),
   1.238 +             (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs)]
   1.239             else [])
   1.240            |> massage_simple_notes fp_common_name;
   1.241  
   1.242          val notes =
   1.243            [(coinductN, map single coinduct_thms,
   1.244              fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
   1.245 +           (coinduct_strongN, map single coinduct_strong_thms, K coinduct_attrs),
   1.246             (corecN, corec_thmss, K []),
   1.247             (corec_codeN, map single corec_code_thms, K code_nitpicksimp_attrs),
   1.248 -           (disc_corecN, disc_corec_thmss, K []),
   1.249 -           (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
   1.250 +           (corec_discN, corec_disc_thmss, K []),
   1.251 +           (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
   1.252 +           (corec_selN, corec_sel_thmss, K corec_sel_attrs),
   1.253             (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
   1.254 -           (sel_corecN, sel_corec_thmss, K sel_corec_attrs),
   1.255 -           (simpsN, simp_thmss, K []),
   1.256 -           (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
   1.257 +           (simpsN, simp_thmss, K [])]
   1.258            |> massage_multi_notes;
   1.259        in
   1.260          lthy
   1.261          |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
   1.262 -          [flat sel_corec_thmss, flat corec_thmss]
   1.263 +          [flat corec_sel_thmss, flat corec_thmss]
   1.264          |> Local_Theory.notes (common_notes @ notes)
   1.265          |-> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
   1.266            live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
   1.267 -          [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
   1.268 -          corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
   1.269 +          [coinduct_thm, coinduct_strong_thm] (transpose [coinduct_thms, coinduct_strong_thms])
   1.270 +          corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss
   1.271        end;
   1.272  
   1.273      val lthy'' = lthy'