src/Pure/pure_thy.ML
author wenzelm
Sun Dec 28 14:56:44 1997 +0100 (1997-12-28)
changeset 4487 9b4c1db5aca1
parent 4258 f2ca5a87f0a7
child 4498 a088ec3e4f5e
permissions -rw-r--r--
renamed Symtab.null to Symtab.empty;
wenzelm@3987
     1
(*  Title:      Pure/pure_thy.ML
wenzelm@3987
     2
    ID:         $Id$
wenzelm@3987
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@3987
     4
wenzelm@3987
     5
Init 'theorems' data.  The Pure theories.
wenzelm@3987
     6
*)
wenzelm@3987
     7
wenzelm@4022
     8
signature BASIC_PURE_THY =
wenzelm@4022
     9
sig
wenzelm@4022
    10
  val get_thm: theory -> xstring -> thm
wenzelm@4022
    11
  val get_thms: theory -> xstring -> thm list
wenzelm@4022
    12
  val thms_of: theory -> (string * thm) list
wenzelm@4022
    13
end
wenzelm@4022
    14
wenzelm@3987
    15
signature PURE_THY =
wenzelm@3987
    16
sig
wenzelm@4022
    17
  include BASIC_PURE_THY
wenzelm@4022
    18
  val thms_containing: theory -> string list -> (string * thm) list
wenzelm@4022
    19
  val store_thms: (bstring * thm) list -> theory -> theory
wenzelm@4022
    20
  val store_thmss: (bstring * thm list) list -> theory -> theory
wenzelm@4022
    21
  val smart_store_thm: (bstring * thm) -> thm
wenzelm@4022
    22
  val add_store_axioms: (bstring * string) list -> theory -> theory
wenzelm@4022
    23
  val add_store_axioms_i: (bstring * term) list -> theory -> theory
wenzelm@4022
    24
  val add_store_defs: (bstring * string) list -> theory -> theory
wenzelm@4022
    25
  val add_store_defs_i: (bstring * term) list -> theory -> theory
wenzelm@3987
    26
  val proto_pure: theory
wenzelm@3987
    27
  val pure: theory
wenzelm@3987
    28
  val cpure: theory
wenzelm@3987
    29
end;
wenzelm@3987
    30
wenzelm@3987
    31
structure PureThy: PURE_THY =
wenzelm@3987
    32
struct
wenzelm@3987
    33
wenzelm@3987
    34
wenzelm@4022
    35
(*** init theorems data ***)
wenzelm@3987
    36
wenzelm@4022
    37
(** data kind theorems **)
wenzelm@3987
    38
wenzelm@4049
    39
val theoremsK = "theorems";
wenzelm@3987
    40
wenzelm@3987
    41
exception Theorems of
wenzelm@4022
    42
 {space: NameSpace.T,
wenzelm@4022
    43
  thms_tab: thm list Symtab.table,
wenzelm@4022
    44
  const_idx: int * (int * thm) list Symtab.table} ref;
wenzelm@3987
    45
wenzelm@3987
    46
wenzelm@3987
    47
(* methods *)
wenzelm@3987
    48
wenzelm@3987
    49
local
wenzelm@3987
    50
wenzelm@4022
    51
fun mk_empty _ =
wenzelm@4022
    52
  Theorems (ref {space = NameSpace.empty,
wenzelm@4487
    53
    thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)});
wenzelm@3987
    54
wenzelm@4258
    55
fun print sg (Theorems (ref {space, thms_tab, const_idx = _})) =
wenzelm@3987
    56
  let
wenzelm@4258
    57
    val prt_thm = Pretty.quote o Display.pretty_thm o Thm.transfer_sg sg;
wenzelm@3987
    58
    fun prt_thms (name, [th]) =
wenzelm@4037
    59
          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
wenzelm@3987
    60
      | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
wenzelm@3987
    61
wenzelm@3987
    62
    fun extrn name =
wenzelm@3987
    63
      if ! long_names then name else NameSpace.extern space name;
wenzelm@3987
    64
    val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab));
wenzelm@3987
    65
  in
wenzelm@3987
    66
    Pretty.writeln (Pretty.strs ("theorem name space:" :: map quote (NameSpace.dest space)));
wenzelm@3987
    67
    Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
wenzelm@3987
    68
  end;
wenzelm@3987
    69
wenzelm@3987
    70
in
wenzelm@3987
    71
wenzelm@4124
    72
val theorems_data: string * (object * (object -> object) *
wenzelm@4258
    73
  (object * object -> object) * (Sign.sg -> object -> unit)) =
wenzelm@4073
    74
    (theoremsK, (mk_empty (), mk_empty, mk_empty, print));
wenzelm@3987
    75
wenzelm@3987
    76
end;
wenzelm@3987
    77
wenzelm@3987
    78
wenzelm@3987
    79
(* get data record *)
wenzelm@3987
    80
wenzelm@4022
    81
fun get_theorems_sg sg =
wenzelm@4049
    82
  (case Sign.get_data sg theoremsK of
wenzelm@3987
    83
    Theorems r => r
wenzelm@4022
    84
  | _ => sys_error "get_theorems_sg");
wenzelm@4022
    85
wenzelm@4022
    86
val get_theorems = get_theorems_sg o sign_of;
wenzelm@4022
    87
wenzelm@3987
    88
wenzelm@3987
    89
wenzelm@4022
    90
(** retrieve theorems **)
wenzelm@3987
    91
wenzelm@4022
    92
fun local_thms thy name =
wenzelm@3987
    93
  let
wenzelm@4022
    94
    val ref {space, thms_tab, ...} = get_theorems thy;
wenzelm@4022
    95
    val full_name = NameSpace.intern space name;
wenzelm@4022
    96
  in Symtab.lookup (thms_tab, full_name) end;
wenzelm@4022
    97
wenzelm@4022
    98
fun all_local_thms [] _ = None
wenzelm@4022
    99
  | all_local_thms (thy :: thys) name =
wenzelm@4022
   100
      (case local_thms thy name of
wenzelm@4022
   101
        None => all_local_thms thys name
wenzelm@4022
   102
      | some => some);
wenzelm@4022
   103
wenzelm@3987
   104
wenzelm@4037
   105
(* get_thm(s) *)
wenzelm@4037
   106
wenzelm@3987
   107
fun get_thms thy name =
wenzelm@4022
   108
  (case all_local_thms (thy :: Theory.ancestors_of thy) name of
wenzelm@4022
   109
    None => raise THEORY ("Theorems " ^ quote name ^ " not stored in theory", [thy])
wenzelm@4022
   110
  | Some thms => thms);
wenzelm@3987
   111
wenzelm@3987
   112
fun get_thm thy name =
wenzelm@3987
   113
  (case get_thms thy name of
wenzelm@3987
   114
    [thm] => thm
wenzelm@4022
   115
  | _ => raise THEORY ("Singleton list of theorems expected " ^ quote name, [thy]));
wenzelm@4022
   116
wenzelm@4022
   117
wenzelm@4022
   118
(* thms_of *)
wenzelm@4022
   119
wenzelm@4022
   120
fun attach_name thm = (Thm.name_of_thm thm, thm);
wenzelm@4022
   121
wenzelm@4022
   122
fun thms_of thy =
wenzelm@4022
   123
  let val ref {thms_tab, ...} = get_theorems thy in
wenzelm@4022
   124
    map attach_name (flat (map snd (Symtab.dest thms_tab)))
wenzelm@4022
   125
  end;
wenzelm@4022
   126
wenzelm@3987
   127
wenzelm@3987
   128
wenzelm@4022
   129
(** theorems indexed by constants **)
wenzelm@4022
   130
wenzelm@4022
   131
(* make index *)
wenzelm@4022
   132
wenzelm@4037
   133
val ignore = ["Trueprop", "all", "==>", "=="];
wenzelm@4022
   134
wenzelm@4022
   135
fun add_const_idx ((next, table), thm) =
wenzelm@4022
   136
  let
wenzelm@4022
   137
    val {hyps, prop, ...} = Thm.rep_thm thm;
wenzelm@4022
   138
    val consts =
wenzelm@4037
   139
      foldr add_term_consts (hyps, add_term_consts (prop, [])) \\ ignore;
wenzelm@4022
   140
wenzelm@4022
   141
    fun add (tab, c) =
wenzelm@4022
   142
      Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab);
wenzelm@4022
   143
  in (next + 1, foldl add (table, consts)) end;
wenzelm@4022
   144
wenzelm@4022
   145
fun make_const_idx thm_tab =
wenzelm@4487
   146
  foldl (foldl add_const_idx) ((0, Symtab.empty), map snd (Symtab.dest thm_tab));
wenzelm@4022
   147
wenzelm@4022
   148
wenzelm@4022
   149
(* lookup index *)
wenzelm@3987
   150
wenzelm@4022
   151
(*search locally*)
wenzelm@4022
   152
fun containing [] thy = thms_of thy
wenzelm@4022
   153
  | containing consts thy =
wenzelm@4022
   154
      let
wenzelm@4037
   155
        fun int ([], _) = []
wenzelm@4037
   156
          | int (_, []) = []
wenzelm@4037
   157
          | int (xxs as ((x as (i:int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
wenzelm@4037
   158
              if i = j then x :: int (xs, ys)
wenzelm@4037
   159
              else if i > j then int (xs, yys)
wenzelm@4037
   160
              else int (xxs, ys);
wenzelm@4022
   161
wenzelm@4037
   162
        fun ints [xs] = xs
wenzelm@4037
   163
          | ints xss = if exists null xss then [] else foldl int (hd xss, tl xss);
wenzelm@4022
   164
wenzelm@4022
   165
        val ref {const_idx = (_, ctab), ...} = get_theorems thy;
wenzelm@4022
   166
        val ithmss = map (fn c => Symtab.lookup_multi (ctab, c)) consts;
wenzelm@4022
   167
      in
wenzelm@4037
   168
        map (attach_name o snd) (ints ithmss)
wenzelm@4022
   169
      end;
wenzelm@4022
   170
wenzelm@4022
   171
(*search globally*)
wenzelm@4022
   172
fun thms_containing thy consts =
wenzelm@4037
   173
  flat (map (containing (consts \\ ignore)) (thy :: Theory.ancestors_of thy));
wenzelm@4022
   174
wenzelm@4022
   175
wenzelm@4022
   176
wenzelm@4022
   177
(** store theorems **)                    (*DESTRUCTIVE*)
wenzelm@3987
   178
wenzelm@3987
   179
fun warn_overwrite name =
wenzelm@3987
   180
  warning ("Replaced old copy of theorems " ^ quote name);
wenzelm@3987
   181
wenzelm@3987
   182
fun warn_same name =
wenzelm@3987
   183
  warning ("Theorem database already contains a copy of " ^ quote name);
wenzelm@3987
   184
wenzelm@3987
   185
fun enter_thms sg single (raw_name, thms) =
wenzelm@3987
   186
  let
wenzelm@3987
   187
    val len = length thms;
wenzelm@3987
   188
    val name = Sign.full_name sg raw_name;
wenzelm@3987
   189
    val names =
wenzelm@3987
   190
      if single then replicate len name
wenzelm@3987
   191
      else map (fn i => name ^ "_" ^ string_of_int i) (0 upto (len - 1));
wenzelm@3987
   192
    val named_thms = ListPair.map Thm.name_thm (names, thms);
wenzelm@3987
   193
wenzelm@3987
   194
    val eq_thms = ListPair.all Thm.eq_thm;
wenzelm@4022
   195
wenzelm@4022
   196
    val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
wenzelm@4022
   197
wenzelm@4022
   198
    val overwrite =
wenzelm@4022
   199
      (case Symtab.lookup (thms_tab, name) of
wenzelm@4022
   200
        None => false
wenzelm@4022
   201
      | Some thms' =>
wenzelm@4022
   202
          if length thms' = len andalso eq_thms (thms', named_thms) then
wenzelm@4022
   203
            (warn_same name; false)
wenzelm@4022
   204
          else (warn_overwrite name; true));
wenzelm@4022
   205
wenzelm@4487
   206
    val space' = NameSpace.extend (space, [name]);
wenzelm@4022
   207
    val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
wenzelm@4022
   208
    val const_idx' =
wenzelm@4022
   209
      if overwrite then make_const_idx thms_tab'
wenzelm@4022
   210
      else foldl add_const_idx (const_idx, named_thms);
wenzelm@3987
   211
  in
wenzelm@4022
   212
    r := {space = space', thms_tab = thms_tab', const_idx = const_idx'};
wenzelm@3987
   213
    named_thms
wenzelm@3987
   214
  end;
wenzelm@3987
   215
wenzelm@4037
   216
fun do_enter_thms sg single thms = (enter_thms sg single thms; ());
wenzelm@3987
   217
wenzelm@3987
   218
wenzelm@4012
   219
fun store_thmss thmss thy =
wenzelm@3987
   220
  (seq (do_enter_thms (sign_of thy) false) thmss; thy);
wenzelm@3987
   221
wenzelm@4012
   222
fun store_thms thms thy =
wenzelm@3987
   223
  (seq (do_enter_thms (sign_of thy) true) (map (apsnd (fn th => [th])) thms); thy);
wenzelm@3987
   224
wenzelm@4012
   225
fun smart_store_thm (name, thm) =
wenzelm@3987
   226
  let val [named_thm] = enter_thms (Thm.sign_of_thm thm) true (name, [thm])
wenzelm@3987
   227
  in named_thm end;
wenzelm@3987
   228
wenzelm@3987
   229
wenzelm@4022
   230
(* store axioms as theorems *)
wenzelm@4022
   231
wenzelm@4022
   232
fun add_store add named_axs thy =
wenzelm@4022
   233
  let
wenzelm@4022
   234
    val thy' = add named_axs thy;
wenzelm@4037
   235
    val named_thms = map (fn (name, _) => (name, get_axiom thy' name)) named_axs;
wenzelm@4022
   236
  in store_thms named_thms thy' end;
wenzelm@4022
   237
wenzelm@4022
   238
val add_store_axioms = add_store Theory.add_axioms;
wenzelm@4022
   239
val add_store_axioms_i = add_store Theory.add_axioms_i;
wenzelm@4022
   240
val add_store_defs = add_store Theory.add_defs;
wenzelm@4022
   241
val add_store_defs_i = add_store Theory.add_defs_i;
wenzelm@4022
   242
wenzelm@4022
   243
wenzelm@3987
   244
wenzelm@3987
   245
(** the Pure theories **)
wenzelm@3987
   246
wenzelm@3987
   247
val proto_pure =
wenzelm@3987
   248
  Theory.pre_pure
wenzelm@4049
   249
  |> Theory.init_data [theorems_data]
wenzelm@3987
   250
  |> Theory.add_types
wenzelm@3987
   251
   (("fun", 2, NoSyn) ::
wenzelm@3987
   252
    ("prop", 0, NoSyn) ::
wenzelm@3987
   253
    ("itself", 1, NoSyn) ::
wenzelm@3987
   254
    Syntax.pure_types)
wenzelm@3987
   255
  |> Theory.add_classes_i [(logicC, [])]
wenzelm@3987
   256
  |> Theory.add_defsort_i logicS
wenzelm@3987
   257
  |> Theory.add_arities_i
wenzelm@3987
   258
   [("fun", [logicS, logicS], logicS),
wenzelm@3987
   259
    ("prop", [], logicS),
wenzelm@3987
   260
    ("itself", [logicS], logicS)]
wenzelm@3987
   261
  |> Theory.add_syntax Syntax.pure_syntax
wenzelm@3987
   262
  |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax
wenzelm@3987
   263
  |> Theory.add_trfuns Syntax.pure_trfuns
wenzelm@3987
   264
  |> Theory.add_trfunsT Syntax.pure_trfunsT
wenzelm@3987
   265
  |> Theory.add_syntax
wenzelm@3987
   266
   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
wenzelm@3987
   267
  |> Theory.add_consts
wenzelm@3987
   268
   [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
wenzelm@3987
   269
    ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
wenzelm@3987
   270
    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
wenzelm@3987
   271
    ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
wenzelm@3987
   272
    ("TYPE", "'a itself", NoSyn)]
wenzelm@4022
   273
  |> Theory.add_path "ProtoPure"
wenzelm@4022
   274
  |> add_store_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
wenzelm@3987
   275
  |> Theory.add_name "ProtoPure";
wenzelm@3987
   276
wenzelm@4022
   277
val pure =
wenzelm@4022
   278
  Theory.prep_ext_merge [proto_pure]
wenzelm@3987
   279
  |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@4022
   280
  |> Theory.add_path "Pure"
wenzelm@3987
   281
  |> Theory.add_name "Pure";
wenzelm@3987
   282
wenzelm@4022
   283
val cpure =
wenzelm@4022
   284
  Theory.prep_ext_merge [proto_pure]
wenzelm@3987
   285
  |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@4022
   286
  |> Theory.add_path "CPure"
wenzelm@3987
   287
  |> Theory.add_name "CPure";
wenzelm@3987
   288
wenzelm@3987
   289
wenzelm@3987
   290
end;
wenzelm@3987
   291
wenzelm@3987
   292
wenzelm@4022
   293
structure BasicPureThy: BASIC_PURE_THY = PureThy;
wenzelm@4022
   294
open BasicPureThy;
wenzelm@4022
   295
wenzelm@4022
   296
wenzelm@3987
   297
wenzelm@3987
   298
(** theory structures **)
wenzelm@3987
   299
wenzelm@3987
   300
structure ProtoPure =
wenzelm@3987
   301
struct
wenzelm@3987
   302
  val thy = PureThy.proto_pure;
wenzelm@3987
   303
  val flexpair_def = get_axiom thy "flexpair_def";
wenzelm@3987
   304
end;
wenzelm@3987
   305
wenzelm@3987
   306
structure Pure = struct val thy = PureThy.pure end;
wenzelm@3987
   307
structure CPure = struct val thy = PureThy.cpure end;