clarified signature;
authorwenzelm
Sun Jul 28 14:28:40 2019 +0200 (3 weeks ago ago)
changeset 706156ec97dc6670e
parent 70614 7f7f149d6843
child 70616 dbb32c2d5c2c
clarified signature;
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/global_theory.ML	Sun Jul 28 12:43:31 2019 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Sun Jul 28 14:28:40 2019 +0200
     1.3 @@ -21,7 +21,8 @@
     1.4    val burrow_facts: ('a list -> 'b list) ->
     1.5      ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
     1.6    val name_multi: string -> 'a list -> (string * 'a) list
     1.7 -  type name_flags = {pre: bool, official: bool}
     1.8 +  type name_flags
     1.9 +  val unnamed: name_flags
    1.10    val official1: name_flags
    1.11    val official2: name_flags
    1.12    val unofficial1: name_flags
    1.13 @@ -110,21 +111,25 @@
    1.14  fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
    1.15  
    1.16  
    1.17 -(* naming *)
    1.18 +(* name theorems *)
    1.19  
    1.20 -type name_flags = {pre: bool, official: bool};
    1.21 +abstype name_flags = No_Name_Flags | Name_Flags of {pre: bool, official: bool}
    1.22 +with
    1.23  
    1.24 -val official1 : name_flags = {pre = true, official = true};
    1.25 -val official2 : name_flags = {pre = false, official = true};
    1.26 -val unofficial1 : name_flags = {pre = true, official = false};
    1.27 -val unofficial2 : name_flags = {pre = false, official = false};
    1.28 +val unnamed = No_Name_Flags;
    1.29 +val official1 = Name_Flags {pre = true, official = true};
    1.30 +val official2 = Name_Flags {pre = false, official = true};
    1.31 +val unofficial1 = Name_Flags {pre = true, official = false};
    1.32 +val unofficial2 = Name_Flags {pre = false, official = false};
    1.33  
    1.34 -fun name_thm {pre, official} name thm = thm
    1.35 -  |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ?
    1.36 -      Thm.name_derivation name
    1.37 -  |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ?
    1.38 -      Thm.put_name_hint name;
    1.39 +fun name_thm No_Name_Flags _ thm = thm
    1.40 +  | name_thm (Name_Flags {pre, official}) name thm = thm
    1.41 +      |> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ?
    1.42 +          Thm.name_derivation name
    1.43 +      |> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ?
    1.44 +          Thm.put_name_hint name;
    1.45  
    1.46 +end;
    1.47  
    1.48  fun name_multi name [x] = [(name, x)]
    1.49    | name_multi "" xs = map (pair "") xs
    1.50 @@ -183,14 +188,14 @@
    1.51  val app_facts =
    1.52    apfst flat oo fold_map (fn (thms, atts) => fold_map (Thm.theory_attributes atts) thms);
    1.53  
    1.54 -fun apply_facts pre_name post_name (b, facts) thy =
    1.55 +fun apply_facts name_flags1 name_flags2 (b, facts) thy =
    1.56    if Binding.is_empty b then app_facts facts thy |-> register_proofs
    1.57    else
    1.58      let
    1.59        val name = Sign.full_name thy b;
    1.60        val (thms', thy') = thy
    1.61 -        |> app_facts (map (apfst (pre_name name)) facts)
    1.62 -        |>> post_name name |-> register_proofs;
    1.63 +        |> app_facts (map (apfst (name_thms name_flags1 name)) facts)
    1.64 +        |>> name_thms name_flags2 name |-> register_proofs;
    1.65        val thy'' = thy' |> add_facts (b, Lazy.value thms');
    1.66      in (map (Thm.transfer thy'') thms', thy'') end;
    1.67  
    1.68 @@ -198,17 +203,16 @@
    1.69  (* store_thm *)
    1.70  
    1.71  fun store_thm (b, th) =
    1.72 -  apply_facts (name_thms official1) (name_thms official2) (b, [([th], [])]) #>> the_single;
    1.73 +  apply_facts official1 official2 (b, [([th], [])]) #>> the_single;
    1.74  
    1.75  fun store_thm_open (b, th) =
    1.76 -  apply_facts (name_thms unofficial1) (name_thms unofficial2) (b, [([th], [])]) #>> the_single;
    1.77 +  apply_facts unofficial1 unofficial2 (b, [([th], [])]) #>> the_single;
    1.78  
    1.79  
    1.80  (* add_thms(s) *)
    1.81  
    1.82  val add_thmss =
    1.83 -  fold_map (fn ((b, thms), atts) =>
    1.84 -    apply_facts (name_thms official1) (name_thms official2) (b, [(thms, atts)]));
    1.85 +  fold_map (fn ((b, thms), atts) => apply_facts official1 official2 (b, [(thms, atts)]));
    1.86  
    1.87  fun add_thms args =
    1.88    add_thmss (map (apfst (apsnd single)) args) #>> map the_single;
    1.89 @@ -232,7 +236,7 @@
    1.90    let
    1.91      val name = Sign.full_name thy b;
    1.92      val facts' = facts |> map (apsnd (fn atts => surround (Thm.kind kind) (atts @ more_atts)));
    1.93 -    val (thms', thy') = thy |> apply_facts (name_thms official1) (name_thms official2) (b, facts');
    1.94 +    val (thms', thy') = thy |> apply_facts official1 official2 (b, facts');
    1.95    in ((name, thms'), thy') end;
    1.96  
    1.97  val note_thmss = fold_map o note_thms;
    1.98 @@ -250,11 +254,7 @@
    1.99        |> Thm.forall_intr_frees
   1.100        |> Thm.forall_elim_vars 0
   1.101        |> Thm.varifyT_global;
   1.102 -  in
   1.103 -    thy'
   1.104 -    |> apply_facts (K I) (name_thms official2) (b, [([thm], atts)])
   1.105 -    |>> the_single
   1.106 -  end);
   1.107 +  in thy' |> apply_facts unnamed official2 (b, [([thm], atts)]) |>> the_single end);
   1.108  
   1.109  in
   1.110