repaired named derivations
authorblanchet
Thu Jul 24 00:24:00 2014 +0200 (2014-07-24)
changeset 576334ff8c090d580
parent 57632 231e90cf2892
child 57634 efc00b9b8680
repaired named derivations
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4           co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
     1.5           sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk,
     1.6           rel_distincts = nth rel_distinctss kk}
     1.7 -        |> morph_fp_sugar (substitute_noted_thm noted)) Ts
     1.8 +        |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
     1.9    in
    1.10      register_fp_sugars fp_sugars
    1.11    end;
    1.12 @@ -601,11 +601,7 @@
    1.13            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    1.14              mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses
    1.15                abs_inverses fp_nesting_set_maps pre_set_defss)
    1.16 -          |> singleton (Proof_Context.export names_lthy lthy)
    1.17 -          (* for "datatype_realizer.ML": *)
    1.18 -          |> Thm.name_derivation (fst (dest_Type (hd fpTs)) ^ Long_Name.separator ^
    1.19 -            (if nn > 1 then space_implode "_" (tl fp_b_names) ^ Long_Name.separator else "") ^
    1.20 -            inductN);
    1.21 +          |> singleton (Proof_Context.export names_lthy lthy);
    1.22        in
    1.23          `(conj_dests nn) thm
    1.24        end;
    1.25 @@ -1702,7 +1698,8 @@
    1.26            (if nn > 1 then
    1.27               [(inductN, [induct_thm], induct_attrs),
    1.28                (rel_inductN, common_rel_induct_thms, common_rel_induct_attrs)]
    1.29 -           else [])
    1.30 +           else
    1.31 +             [])
    1.32            |> massage_simple_notes fp_common_name;
    1.33  
    1.34          val notes =
    1.35 @@ -1715,6 +1712,9 @@
    1.36          lthy
    1.37          |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
    1.38          |> Local_Theory.notes (common_notes @ notes)
    1.39 +        (* for "datatype_realizer.ML": *)
    1.40 +        |>> name_noted_thms
    1.41 +          (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
    1.42          |-> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs
    1.43            live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
    1.44            (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Jul 24 00:24:00 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Jul 24 00:24:00 2014 +0200
     2.3 @@ -163,7 +163,8 @@
     2.4    in
     2.5      lthy
     2.6      |> Local_Theory.raw_theory register_interpret
     2.7 -    |> Local_Theory.notes all_notes |> snd
     2.8 +    |> Local_Theory.notes all_notes
     2.9 +    |> snd
    2.10    end;
    2.11  
    2.12  val _ =
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     3.3 @@ -481,8 +481,8 @@
     3.4                mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
     3.5                  def_thms rec_thm
     3.6                |> K |> Goal.prove_sorry lthy' [] [] user_eqn
     3.7 +              |> singleton (Proof_Context.export lthy' lthy)
     3.8                (* for code extraction from proof terms: *)
     3.9 -              |> singleton (Proof_Context.export lthy' lthy)
    3.10                |> Thm.name_derivation (Sign.full_name thy (Binding.name fun_name) ^
    3.11                  Long_Name.separator ^ simpsN ^
    3.12                  (if js = [0] then "" else "_" ^ string_of_int (j + 1))))
     4.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jul 24 00:24:00 2014 +0200
     4.3 @@ -629,14 +629,9 @@
     4.4  
     4.5      val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
     4.6  
     4.7 -    fun after_qed thmss lthy =
     4.8 +    fun after_qed ([exhaust_thm] :: thmss) lthy =
     4.9        let
    4.10 -        val ([exhaust_thm0], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
    4.11 -        (* for "datatype_realizer.ML": *)
    4.12 -        val exhaust_thm =
    4.13 -          Thm.name_derivation (fcT_name ^ Long_Name.separator ^ exhaustN) exhaust_thm0;
    4.14 -
    4.15 -        val inject_thms = flat inject_thmss;
    4.16 +        val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
    4.17  
    4.18          val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
    4.19  
    4.20 @@ -1011,7 +1006,9 @@
    4.21                       (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
    4.22                       (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
    4.23                    I)
    4.24 -          |> Local_Theory.notes (anonymous_notes @ notes);
    4.25 +          |> Local_Theory.notes (anonymous_notes @ notes)
    4.26 +          (* for "datatype_realizer.ML": *)
    4.27 +          |>> name_noted_thms fcT_name exhaustN;
    4.28  
    4.29          val ctr_sugar =
    4.30            {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
     5.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 24 00:24:00 2014 +0200
     5.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Thu Jul 24 00:24:00 2014 +0200
     5.3 @@ -68,6 +68,7 @@
     5.4    val certifyT: Proof.context -> typ -> ctyp
     5.5    val certify: Proof.context -> term -> cterm
     5.6  
     5.7 +  val name_noted_thms: string -> string -> (string * thm list) list -> (string * thm list) list
     5.8    val substitute_noted_thm: (string * thm list) list -> morphism
     5.9  
    5.10    val standard_binding: binding
    5.11 @@ -233,14 +234,23 @@
    5.12  fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
    5.13  
    5.14  (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
    5.15 -fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
    5.16 -fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
    5.17 +val certifyT = Thm.ctyp_of o Proof_Context.theory_of;
    5.18 +val certify = Thm.cterm_of o Proof_Context.theory_of;
    5.19 +
    5.20 +fun name_noted_thms _ _ [] = []
    5.21 +  | name_noted_thms qualifier base ((local_name, thms) :: noted) =
    5.22 +    if Long_Name.base_name local_name = base then
    5.23 +      (local_name,
    5.24 +       map_index (uncurry (fn j => Thm.name_derivation (qualifier ^ Long_Name.separator ^ base ^
    5.25 +         (if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted
    5.26 +    else
    5.27 +      ((local_name, thms) :: name_noted_thms qualifier base noted);
    5.28  
    5.29  fun substitute_noted_thm noted =
    5.30    let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in
    5.31      Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm"
    5.32        (perhaps (Termtab.lookup tab o Thm.full_prop_of) o Drule.zero_var_indexes)
    5.33 -  end
    5.34 +  end;
    5.35  
    5.36  (* The standard binding stands for a name generated following the canonical convention (e.g.,
    5.37     "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no