src/Pure/pure_thy.ML
author wenzelm
Thu Oct 30 10:01:46 1997 +0100 (1997-10-30)
changeset 4037 dae5afe7733f
parent 4022 0770a19c48d3
child 4049 b2a70d318df2
permissions -rw-r--r--
tuned;
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@3987
    39
val theorems = "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@4022
    53
    thms_tab = Symtab.null, const_idx = (0, Symtab.null)});
wenzelm@3987
    54
wenzelm@4022
    55
fun print (Theorems (ref {space, thms_tab, const_idx = _})) =
wenzelm@3987
    56
  let
wenzelm@4037
    57
    val prt_thm = Pretty.quote o Display.pretty_thm;
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@4022
    72
val theorems_methods = (mk_empty (), mk_empty, mk_empty, print);
wenzelm@3987
    73
wenzelm@3987
    74
end;
wenzelm@3987
    75
wenzelm@3987
    76
wenzelm@3987
    77
(* get data record *)
wenzelm@3987
    78
wenzelm@4022
    79
fun get_theorems_sg sg =
wenzelm@3987
    80
  (case Sign.get_data sg theorems of
wenzelm@3987
    81
    Theorems r => r
wenzelm@4022
    82
  | _ => sys_error "get_theorems_sg");
wenzelm@4022
    83
wenzelm@4022
    84
val get_theorems = get_theorems_sg o sign_of;
wenzelm@4022
    85
wenzelm@3987
    86
wenzelm@3987
    87
wenzelm@4022
    88
(** retrieve theorems **)
wenzelm@3987
    89
wenzelm@4022
    90
fun local_thms thy name =
wenzelm@3987
    91
  let
wenzelm@4022
    92
    val ref {space, thms_tab, ...} = get_theorems thy;
wenzelm@4022
    93
    val full_name = NameSpace.intern space name;
wenzelm@4022
    94
  in Symtab.lookup (thms_tab, full_name) end;
wenzelm@4022
    95
wenzelm@4022
    96
fun all_local_thms [] _ = None
wenzelm@4022
    97
  | all_local_thms (thy :: thys) name =
wenzelm@4022
    98
      (case local_thms thy name of
wenzelm@4022
    99
        None => all_local_thms thys name
wenzelm@4022
   100
      | some => some);
wenzelm@4022
   101
wenzelm@3987
   102
wenzelm@4037
   103
(* get_thm(s) *)
wenzelm@4037
   104
wenzelm@3987
   105
fun get_thms thy name =
wenzelm@4022
   106
  (case all_local_thms (thy :: Theory.ancestors_of thy) name of
wenzelm@4022
   107
    None => raise THEORY ("Theorems " ^ quote name ^ " not stored in theory", [thy])
wenzelm@4022
   108
  | Some thms => thms);
wenzelm@3987
   109
wenzelm@3987
   110
fun get_thm thy name =
wenzelm@3987
   111
  (case get_thms thy name of
wenzelm@3987
   112
    [thm] => thm
wenzelm@4022
   113
  | _ => raise THEORY ("Singleton list of theorems expected " ^ quote name, [thy]));
wenzelm@4022
   114
wenzelm@4022
   115
wenzelm@4022
   116
(* thms_of *)
wenzelm@4022
   117
wenzelm@4022
   118
fun attach_name thm = (Thm.name_of_thm thm, thm);
wenzelm@4022
   119
wenzelm@4022
   120
fun thms_of thy =
wenzelm@4022
   121
  let val ref {thms_tab, ...} = get_theorems thy in
wenzelm@4022
   122
    map attach_name (flat (map snd (Symtab.dest thms_tab)))
wenzelm@4022
   123
  end;
wenzelm@4022
   124
wenzelm@3987
   125
wenzelm@3987
   126
wenzelm@4022
   127
(** theorems indexed by constants **)
wenzelm@4022
   128
wenzelm@4022
   129
(* make index *)
wenzelm@4022
   130
wenzelm@4037
   131
val ignore = ["Trueprop", "all", "==>", "=="];
wenzelm@4022
   132
wenzelm@4022
   133
fun add_const_idx ((next, table), thm) =
wenzelm@4022
   134
  let
wenzelm@4022
   135
    val {hyps, prop, ...} = Thm.rep_thm thm;
wenzelm@4022
   136
    val consts =
wenzelm@4037
   137
      foldr add_term_consts (hyps, add_term_consts (prop, [])) \\ ignore;
wenzelm@4022
   138
wenzelm@4022
   139
    fun add (tab, c) =
wenzelm@4022
   140
      Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab);
wenzelm@4022
   141
  in (next + 1, foldl add (table, consts)) end;
wenzelm@4022
   142
wenzelm@4022
   143
fun make_const_idx thm_tab =
wenzelm@4022
   144
  foldl (foldl add_const_idx) ((0, Symtab.null), map snd (Symtab.dest thm_tab));
wenzelm@4022
   145
wenzelm@4022
   146
wenzelm@4022
   147
(* lookup index *)
wenzelm@3987
   148
wenzelm@4022
   149
(*search locally*)
wenzelm@4022
   150
fun containing [] thy = thms_of thy
wenzelm@4022
   151
  | containing consts thy =
wenzelm@4022
   152
      let
wenzelm@4037
   153
        fun int ([], _) = []
wenzelm@4037
   154
          | int (_, []) = []
wenzelm@4037
   155
          | int (xxs as ((x as (i:int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
wenzelm@4037
   156
              if i = j then x :: int (xs, ys)
wenzelm@4037
   157
              else if i > j then int (xs, yys)
wenzelm@4037
   158
              else int (xxs, ys);
wenzelm@4022
   159
wenzelm@4037
   160
        fun ints [xs] = xs
wenzelm@4037
   161
          | ints xss = if exists null xss then [] else foldl int (hd xss, tl xss);
wenzelm@4022
   162
wenzelm@4022
   163
        val ref {const_idx = (_, ctab), ...} = get_theorems thy;
wenzelm@4022
   164
        val ithmss = map (fn c => Symtab.lookup_multi (ctab, c)) consts;
wenzelm@4022
   165
      in
wenzelm@4037
   166
        map (attach_name o snd) (ints ithmss)
wenzelm@4022
   167
      end;
wenzelm@4022
   168
wenzelm@4022
   169
(*search globally*)
wenzelm@4022
   170
fun thms_containing thy consts =
wenzelm@4037
   171
  flat (map (containing (consts \\ ignore)) (thy :: Theory.ancestors_of thy));
wenzelm@4022
   172
wenzelm@4022
   173
wenzelm@4022
   174
wenzelm@4022
   175
(** store theorems **)                    (*DESTRUCTIVE*)
wenzelm@3987
   176
wenzelm@3987
   177
fun warn_overwrite name =
wenzelm@3987
   178
  warning ("Replaced old copy of theorems " ^ quote name);
wenzelm@3987
   179
wenzelm@3987
   180
fun warn_same name =
wenzelm@3987
   181
  warning ("Theorem database already contains a copy of " ^ quote name);
wenzelm@3987
   182
wenzelm@3987
   183
fun enter_thms sg single (raw_name, thms) =
wenzelm@3987
   184
  let
wenzelm@3987
   185
    val len = length thms;
wenzelm@3987
   186
    val name = Sign.full_name sg raw_name;
wenzelm@3987
   187
    val names =
wenzelm@3987
   188
      if single then replicate len name
wenzelm@3987
   189
      else map (fn i => name ^ "_" ^ string_of_int i) (0 upto (len - 1));
wenzelm@3987
   190
    val named_thms = ListPair.map Thm.name_thm (names, thms);
wenzelm@3987
   191
wenzelm@3987
   192
    val eq_thms = ListPair.all Thm.eq_thm;
wenzelm@4022
   193
wenzelm@4022
   194
    val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
wenzelm@4022
   195
wenzelm@4022
   196
    val overwrite =
wenzelm@4022
   197
      (case Symtab.lookup (thms_tab, name) of
wenzelm@4022
   198
        None => false
wenzelm@4022
   199
      | Some thms' =>
wenzelm@4022
   200
          if length thms' = len andalso eq_thms (thms', named_thms) then
wenzelm@4022
   201
            (warn_same name; false)
wenzelm@4022
   202
          else (warn_overwrite name; true));
wenzelm@4022
   203
wenzelm@4022
   204
    val space' = NameSpace.extend ([name], space);
wenzelm@4022
   205
    val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
wenzelm@4022
   206
    val const_idx' =
wenzelm@4022
   207
      if overwrite then make_const_idx thms_tab'
wenzelm@4022
   208
      else foldl add_const_idx (const_idx, named_thms);
wenzelm@3987
   209
  in
wenzelm@4022
   210
    r := {space = space', thms_tab = thms_tab', const_idx = const_idx'};
wenzelm@3987
   211
    named_thms
wenzelm@3987
   212
  end;
wenzelm@3987
   213
wenzelm@4037
   214
fun do_enter_thms sg single thms = (enter_thms sg single thms; ());
wenzelm@3987
   215
wenzelm@3987
   216
wenzelm@4012
   217
fun store_thmss thmss thy =
wenzelm@3987
   218
  (seq (do_enter_thms (sign_of thy) false) thmss; thy);
wenzelm@3987
   219
wenzelm@4012
   220
fun store_thms thms thy =
wenzelm@3987
   221
  (seq (do_enter_thms (sign_of thy) true) (map (apsnd (fn th => [th])) thms); thy);
wenzelm@3987
   222
wenzelm@4012
   223
fun smart_store_thm (name, thm) =
wenzelm@3987
   224
  let val [named_thm] = enter_thms (Thm.sign_of_thm thm) true (name, [thm])
wenzelm@3987
   225
  in named_thm end;
wenzelm@3987
   226
wenzelm@3987
   227
wenzelm@4022
   228
(* store axioms as theorems *)
wenzelm@4022
   229
wenzelm@4022
   230
fun add_store add named_axs thy =
wenzelm@4022
   231
  let
wenzelm@4022
   232
    val thy' = add named_axs thy;
wenzelm@4037
   233
    val named_thms = map (fn (name, _) => (name, get_axiom thy' name)) named_axs;
wenzelm@4022
   234
  in store_thms named_thms thy' end;
wenzelm@4022
   235
wenzelm@4022
   236
val add_store_axioms = add_store Theory.add_axioms;
wenzelm@4022
   237
val add_store_axioms_i = add_store Theory.add_axioms_i;
wenzelm@4022
   238
val add_store_defs = add_store Theory.add_defs;
wenzelm@4022
   239
val add_store_defs_i = add_store Theory.add_defs_i;
wenzelm@4022
   240
wenzelm@4022
   241
wenzelm@3987
   242
wenzelm@3987
   243
(** the Pure theories **)
wenzelm@3987
   244
wenzelm@3987
   245
val proto_pure =
wenzelm@3987
   246
  Theory.pre_pure
wenzelm@3987
   247
  |> Theory.init_data theorems theorems_methods
wenzelm@3987
   248
  |> Theory.add_types
wenzelm@3987
   249
   (("fun", 2, NoSyn) ::
wenzelm@3987
   250
    ("prop", 0, NoSyn) ::
wenzelm@3987
   251
    ("itself", 1, NoSyn) ::
wenzelm@3987
   252
    Syntax.pure_types)
wenzelm@3987
   253
  |> Theory.add_classes_i [(logicC, [])]
wenzelm@3987
   254
  |> Theory.add_defsort_i logicS
wenzelm@3987
   255
  |> Theory.add_arities_i
wenzelm@3987
   256
   [("fun", [logicS, logicS], logicS),
wenzelm@3987
   257
    ("prop", [], logicS),
wenzelm@3987
   258
    ("itself", [logicS], logicS)]
wenzelm@3987
   259
  |> Theory.add_syntax Syntax.pure_syntax
wenzelm@3987
   260
  |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax
wenzelm@3987
   261
  |> Theory.add_trfuns Syntax.pure_trfuns
wenzelm@3987
   262
  |> Theory.add_trfunsT Syntax.pure_trfunsT
wenzelm@3987
   263
  |> Theory.add_syntax
wenzelm@3987
   264
   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
wenzelm@3987
   265
  |> Theory.add_consts
wenzelm@3987
   266
   [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
wenzelm@3987
   267
    ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
wenzelm@3987
   268
    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
wenzelm@3987
   269
    ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
wenzelm@3987
   270
    ("TYPE", "'a itself", NoSyn)]
wenzelm@4022
   271
  |> Theory.add_path "ProtoPure"
wenzelm@4022
   272
  |> add_store_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
wenzelm@3987
   273
  |> Theory.add_name "ProtoPure";
wenzelm@3987
   274
wenzelm@4022
   275
val pure =
wenzelm@4022
   276
  Theory.prep_ext_merge [proto_pure]
wenzelm@3987
   277
  |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@4022
   278
  |> Theory.add_path "Pure"
wenzelm@3987
   279
  |> Theory.add_name "Pure";
wenzelm@3987
   280
wenzelm@4022
   281
val cpure =
wenzelm@4022
   282
  Theory.prep_ext_merge [proto_pure]
wenzelm@3987
   283
  |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@4022
   284
  |> Theory.add_path "CPure"
wenzelm@3987
   285
  |> Theory.add_name "CPure";
wenzelm@3987
   286
wenzelm@3987
   287
wenzelm@3987
   288
end;
wenzelm@3987
   289
wenzelm@3987
   290
wenzelm@4022
   291
structure BasicPureThy: BASIC_PURE_THY = PureThy;
wenzelm@4022
   292
open BasicPureThy;
wenzelm@4022
   293
wenzelm@4022
   294
wenzelm@3987
   295
wenzelm@3987
   296
(** theory structures **)
wenzelm@3987
   297
wenzelm@3987
   298
structure ProtoPure =
wenzelm@3987
   299
struct
wenzelm@3987
   300
  val thy = PureThy.proto_pure;
wenzelm@3987
   301
  val flexpair_def = get_axiom thy "flexpair_def";
wenzelm@3987
   302
end;
wenzelm@3987
   303
wenzelm@3987
   304
structure Pure = struct val thy = PureThy.pure end;
wenzelm@3987
   305
structure CPure = struct val thy = PureThy.cpure end;