clarified signature;
authorwenzelm
Sun Jul 28 12:11:20 2019 +0200 (3 weeks ago ago)
changeset 70612973bf3e42e54
parent 70611 198be2de1efa
child 70613 4537e82019d3
clarified signature;
src/Pure/Isar/generic_target.ML
src/Pure/Isar/proof_context.ML
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/Isar/generic_target.ML	Sun Jul 28 11:53:51 2019 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Jul 28 12:11:20 2019 +0200
     1.3 @@ -277,7 +277,7 @@
     1.4        |> Drule.zero_var_indexes_list;
     1.5  
     1.6      (*thm definition*)
     1.7 -    val result = Global_Theory.name_thm true true name th'';
     1.8 +    val result = Global_Theory.name_thm Global_Theory.official1 name th'';
     1.9  
    1.10      (*import fixes*)
    1.11      val (tvars, vars) =
    1.12 @@ -299,7 +299,7 @@
    1.13          handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
    1.14        |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
    1.15        |> Goal.norm_result ctxt
    1.16 -      |> Global_Theory.name_thm false false name;
    1.17 +      |> Global_Theory.name_thm Global_Theory.unofficial2 name;
    1.18  
    1.19    in (result'', result) end;
    1.20  
     2.1 --- a/src/Pure/Isar/proof_context.ML	Sun Jul 28 11:53:51 2019 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Jul 28 12:11:20 2019 +0200
     2.3 @@ -1081,18 +1081,20 @@
     2.4      val name = full_name ctxt b;
     2.5      val ths' =
     2.6        Global_Theory.check_thms_lazy ths
     2.7 -      |> Lazy.map_finished (Global_Theory.name_thms true false name #> map (Thm.kind_rule kind));
     2.8 +      |> Lazy.map_finished
     2.9 +          (Global_Theory.name_thms Global_Theory.unofficial1 name #> map (Thm.kind_rule kind));
    2.10      val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
    2.11    in ctxt' end;
    2.12  
    2.13  fun note_thms kind ((b, more_atts), facts) ctxt =
    2.14    let
    2.15      val name = full_name ctxt b;
    2.16 -    val facts' = Global_Theory.burrow_fact (Global_Theory.name_thms true false name) facts;
    2.17 +    val facts' = facts
    2.18 +      |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 name);
    2.19      fun app (ths, atts) =
    2.20        fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
    2.21      val (res, ctxt') = fold_map app facts' ctxt;
    2.22 -    val thms = Global_Theory.name_thms false false name (flat res);
    2.23 +    val thms = Global_Theory.name_thms Global_Theory.unofficial2 name (flat res);
    2.24      val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
    2.25    in ((name, thms), ctxt'') end;
    2.26  
     3.1 --- a/src/Pure/global_theory.ML	Sun Jul 28 11:53:51 2019 +0200
     3.2 +++ b/src/Pure/global_theory.ML	Sun Jul 28 12:11:20 2019 +0200
     3.3 @@ -21,8 +21,13 @@
     3.4    val burrow_facts: ('a list -> 'b list) ->
     3.5      ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
     3.6    val name_multi: string -> 'a list -> (string * 'a) list
     3.7 -  val name_thm: bool -> bool -> string -> thm -> thm
     3.8 -  val name_thms: bool -> bool -> string -> thm list -> thm list
     3.9 +  type name_flags = {pre: bool, official: bool}
    3.10 +  val official1: name_flags
    3.11 +  val official2: name_flags
    3.12 +  val unofficial1: name_flags
    3.13 +  val unofficial2: name_flags
    3.14 +  val name_thm: name_flags -> string -> thm -> thm
    3.15 +  val name_thms: name_flags -> string -> thm list -> thm list
    3.16    val check_thms_lazy: thm list lazy -> thm list lazy
    3.17    val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
    3.18    val store_thm: binding * thm -> theory -> thm * theory
    3.19 @@ -107,18 +112,26 @@
    3.20  
    3.21  (* naming *)
    3.22  
    3.23 -fun name_multi name [x] = [(name, x)]
    3.24 -  | name_multi "" xs = map (pair "") xs
    3.25 -  | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
    3.26 +type name_flags = {pre: bool, official: bool};
    3.27  
    3.28 -fun name_thm pre official name thm = thm
    3.29 +val official1 : name_flags = {pre = true, official = true};
    3.30 +val official2 : name_flags = {pre = false, official = true};
    3.31 +val unofficial1 : name_flags = {pre = true, official = false};
    3.32 +val unofficial2 : name_flags = {pre = false, official = false};
    3.33 +
    3.34 +fun name_thm {pre, official} name thm = thm
    3.35    |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ?
    3.36        Thm.name_derivation name
    3.37    |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ?
    3.38        Thm.put_name_hint name;
    3.39  
    3.40 -fun name_thms pre official name thms =
    3.41 -  map (uncurry (name_thm pre official)) (name_multi name thms);
    3.42 +
    3.43 +fun name_multi name [x] = [(name, x)]
    3.44 +  | name_multi "" xs = map (pair "") xs
    3.45 +  | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
    3.46 +
    3.47 +fun name_thms name_flags name thms =
    3.48 +  map (uncurry (name_thm name_flags)) (name_multi name thms);
    3.49  
    3.50  
    3.51  (* apply theorems and attributes *)
    3.52 @@ -164,7 +177,7 @@
    3.53        val name = Sign.full_name thy b;
    3.54        val thms' =
    3.55          check_thms_lazy thms
    3.56 -        |> Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind));
    3.57 +        |> Lazy.map_finished (name_thms official1 name #> map (Thm.kind_rule kind));
    3.58      in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
    3.59  
    3.60  val app_facts =
    3.61 @@ -185,16 +198,16 @@
    3.62  (* store_thm *)
    3.63  
    3.64  fun store_thm (b, th) =
    3.65 -  apply_facts (name_thms true true) (name_thms false true) (b, [([th], [])]) #>> the_single;
    3.66 +  apply_facts (name_thms official1) (name_thms official2) (b, [([th], [])]) #>> the_single;
    3.67  
    3.68  fun store_thm_open (b, th) =
    3.69 -  apply_facts (name_thms true false) (name_thms false false) (b, [([th], [])]) #>> the_single;
    3.70 +  apply_facts (name_thms unofficial1) (name_thms unofficial2) (b, [([th], [])]) #>> the_single;
    3.71  
    3.72  
    3.73  (* add_thms(s) *)
    3.74  
    3.75  fun add_thms_atts pre_name ((b, thms), atts) =
    3.76 -  apply_facts pre_name (name_thms false true) (b, [(thms, atts)]);
    3.77 +  apply_facts pre_name (name_thms official2) (b, [(thms, atts)]);
    3.78  
    3.79  fun gen_add_thmss pre_name =
    3.80    fold_map (add_thms_atts pre_name);
    3.81 @@ -202,8 +215,8 @@
    3.82  fun gen_add_thms pre_name args =
    3.83    apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
    3.84  
    3.85 -val add_thmss = gen_add_thmss (name_thms true true);
    3.86 -val add_thms = gen_add_thms (name_thms true true);
    3.87 +val add_thmss = gen_add_thmss (name_thms official1);
    3.88 +val add_thms = gen_add_thms (name_thms official1);
    3.89  val add_thm = yield_singleton add_thms;
    3.90  
    3.91  
    3.92 @@ -223,7 +236,7 @@
    3.93    let
    3.94      val name = Sign.full_name thy b;
    3.95      val facts' = facts |> map (apsnd (fn atts => surround (Thm.kind kind) (atts @ more_atts)));
    3.96 -    val (thms', thy') = thy |> apply_facts (name_thms true true) (name_thms false true) (b, facts');
    3.97 +    val (thms', thy') = thy |> apply_facts (name_thms official1) (name_thms official2) (b, facts');
    3.98    in ((name, thms'), thy') end;
    3.99  
   3.100  val note_thmss = fold_map o note_thms;