src/Pure/pure_thy.ML
author wenzelm
Fri Oct 24 17:11:23 1997 +0200 (1997-10-24)
changeset 3987 22f5291012df
child 4002 6b8abfdf3ec4
permissions -rw-r--r--
Init 'theorems' data. The Pure theories.
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@3987
     8
signature PURE_THY =
wenzelm@3987
     9
sig
wenzelm@3987
    10
  val put_thms: (bstring * thm) list -> theory -> theory        (*DESTRUCTIVE*)
wenzelm@3987
    11
  val put_thmss: (bstring * thm list) list -> theory -> theory  (*DESTRUCTIVE*)
wenzelm@3987
    12
  val store_thm: (bstring * thm) -> thm                         (*DESTRUCTIVE*)
wenzelm@3987
    13
  val get_thm: theory -> xstring -> thm
wenzelm@3987
    14
  val get_thms: theory -> xstring -> thm list
wenzelm@3987
    15
  val proto_pure: theory
wenzelm@3987
    16
  val pure: theory
wenzelm@3987
    17
  val cpure: theory
wenzelm@3987
    18
end;
wenzelm@3987
    19
wenzelm@3987
    20
structure PureThy: PURE_THY =
wenzelm@3987
    21
struct
wenzelm@3987
    22
wenzelm@3987
    23
wenzelm@3987
    24
(** init theorems data **)
wenzelm@3987
    25
wenzelm@3987
    26
(* data kind theorems *)
wenzelm@3987
    27
wenzelm@3987
    28
val theorems = "theorems";
wenzelm@3987
    29
wenzelm@3987
    30
exception Theorems of
wenzelm@3987
    31
  {space: NameSpace.T, thms_tab: thm list Symtab.table} ref;
wenzelm@3987
    32
wenzelm@3987
    33
wenzelm@3987
    34
(* methods *)
wenzelm@3987
    35
wenzelm@3987
    36
local
wenzelm@3987
    37
wenzelm@3987
    38
val empty =
wenzelm@3987
    39
  Theorems (ref {space = NameSpace.empty, thms_tab = Symtab.null});
wenzelm@3987
    40
wenzelm@3987
    41
fun ext (Theorems (ref {space, ...})) =
wenzelm@3987
    42
  Theorems (ref {space = space, thms_tab = Symtab.null});
wenzelm@3987
    43
wenzelm@3987
    44
fun merge (Theorems (ref {space = space1, ...}), Theorems (ref {space = space2, ...})) =
wenzelm@3987
    45
  Theorems (ref {space = NameSpace.merge (space1, space2), thms_tab = Symtab.null});
wenzelm@3987
    46
wenzelm@3987
    47
fun print (Theorems (ref {space, thms_tab})) =
wenzelm@3987
    48
  let
wenzelm@3987
    49
    val prt_thm = Pretty.quote o pretty_thm;
wenzelm@3987
    50
    fun prt_thms (name, [th]) =
wenzelm@3987
    51
          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, (prt_thm th)]
wenzelm@3987
    52
      | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
wenzelm@3987
    53
wenzelm@3987
    54
    fun extrn name =
wenzelm@3987
    55
      if ! long_names then name else NameSpace.extern space name;
wenzelm@3987
    56
    val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab));
wenzelm@3987
    57
  in
wenzelm@3987
    58
    Pretty.writeln (Pretty.strs ("theorem name space:" :: map quote (NameSpace.dest space)));
wenzelm@3987
    59
    Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
wenzelm@3987
    60
  end;
wenzelm@3987
    61
wenzelm@3987
    62
in
wenzelm@3987
    63
wenzelm@3987
    64
val theorems_methods = (empty, ext, merge, print);
wenzelm@3987
    65
wenzelm@3987
    66
end;
wenzelm@3987
    67
wenzelm@3987
    68
wenzelm@3987
    69
(* get data record *)
wenzelm@3987
    70
wenzelm@3987
    71
fun get_theorems sg =
wenzelm@3987
    72
  (case Sign.get_data sg theorems of
wenzelm@3987
    73
    Theorems r => r
wenzelm@3987
    74
  | _ => sys_error "get_theorems");
wenzelm@3987
    75
wenzelm@3987
    76
wenzelm@3987
    77
(* retrieve theorems *)
wenzelm@3987
    78
wenzelm@3987
    79
fun lookup_thms theory full_name =
wenzelm@3987
    80
  let
wenzelm@3987
    81
    val tab_of = #thms_tab o ! o get_theorems o sign_of;
wenzelm@3987
    82
    fun lookup [] = raise Match
wenzelm@3987
    83
      | lookup (thy :: thys) =
wenzelm@3987
    84
          (case Symtab.lookup (tab_of thy, full_name) of
wenzelm@3987
    85
            Some thms => thms
wenzelm@3987
    86
          | None => lookup (Theory.parents_of thy) handle Match => lookup thys)
wenzelm@3987
    87
  in
wenzelm@3987
    88
    lookup [theory] handle Match
wenzelm@3987
    89
      => raise THEORY ("No theorems " ^ quote full_name ^ " stored in theory", [theory])
wenzelm@3987
    90
  end;
wenzelm@3987
    91
wenzelm@3987
    92
fun get_thms thy name =
wenzelm@3987
    93
  let
wenzelm@3987
    94
    val ref {space, ...} = get_theorems (sign_of thy);
wenzelm@3987
    95
    val full_name = NameSpace.intern space name;
wenzelm@3987
    96
  in lookup_thms thy full_name end;
wenzelm@3987
    97
wenzelm@3987
    98
fun get_thm thy name =
wenzelm@3987
    99
  (case get_thms thy name of
wenzelm@3987
   100
    [thm] => thm
wenzelm@3987
   101
  | _ => raise THEORY ("Singleton theorem list expected " ^ quote name, [thy]));
wenzelm@3987
   102
wenzelm@3987
   103
wenzelm@3987
   104
(* store theorems *)                    (*DESTRUCTIVE*)
wenzelm@3987
   105
wenzelm@3987
   106
fun err_dup name =
wenzelm@3987
   107
  error ("Duplicate theorems " ^ quote name);
wenzelm@3987
   108
wenzelm@3987
   109
fun warn_overwrite name =
wenzelm@3987
   110
  warning ("Replaced old copy of theorems " ^ quote name);
wenzelm@3987
   111
wenzelm@3987
   112
fun warn_same name =
wenzelm@3987
   113
  warning ("Theorem database already contains a copy of " ^ quote name);
wenzelm@3987
   114
wenzelm@3987
   115
wenzelm@3987
   116
fun enter_thms sg single (raw_name, thms) =
wenzelm@3987
   117
  let
wenzelm@3987
   118
    val len = length thms;
wenzelm@3987
   119
    val name = Sign.full_name sg raw_name;
wenzelm@3987
   120
    val names =
wenzelm@3987
   121
      if single then replicate len name
wenzelm@3987
   122
      else map (fn i => name ^ "_" ^ string_of_int i) (0 upto (len - 1));
wenzelm@3987
   123
    val named_thms = ListPair.map Thm.name_thm (names, thms);
wenzelm@3987
   124
wenzelm@3987
   125
    val eq_thms = ListPair.all Thm.eq_thm;
wenzelm@3987
   126
    val r as ref {space, thms_tab = tab} = get_theorems sg;
wenzelm@3987
   127
  in
wenzelm@3987
   128
    (case Symtab.lookup (tab, name) of
wenzelm@3987
   129
      None =>
wenzelm@3987
   130
        if NameSpace.declared space name then err_dup name else ()
wenzelm@3987
   131
    | Some thms' =>
wenzelm@3987
   132
        if length thms' = len andalso eq_thms (thms', named_thms) then
wenzelm@3987
   133
          warn_overwrite name
wenzelm@3987
   134
        else warn_same name);
wenzelm@3987
   135
wenzelm@3987
   136
    r :=
wenzelm@3987
   137
     {space = NameSpace.extend ([name], space),
wenzelm@3987
   138
      thms_tab = Symtab.update ((name, named_thms), tab)};
wenzelm@3987
   139
wenzelm@3987
   140
    named_thms
wenzelm@3987
   141
  end;
wenzelm@3987
   142
wenzelm@3987
   143
fun do_enter_thms sg single name_thms =
wenzelm@3987
   144
  (enter_thms sg single name_thms; ());
wenzelm@3987
   145
wenzelm@3987
   146
wenzelm@3987
   147
fun put_thmss thmss thy =
wenzelm@3987
   148
  (seq (do_enter_thms (sign_of thy) false) thmss; thy);
wenzelm@3987
   149
wenzelm@3987
   150
fun put_thms thms thy =
wenzelm@3987
   151
  (seq (do_enter_thms (sign_of thy) true) (map (apsnd (fn th => [th])) thms); thy);
wenzelm@3987
   152
wenzelm@3987
   153
fun store_thm (name, thm) =
wenzelm@3987
   154
  let val [named_thm] = enter_thms (Thm.sign_of_thm thm) true (name, [thm])
wenzelm@3987
   155
  in named_thm end;
wenzelm@3987
   156
wenzelm@3987
   157
wenzelm@3987
   158
wenzelm@3987
   159
(** the Pure theories **)
wenzelm@3987
   160
wenzelm@3987
   161
val proto_pure =
wenzelm@3987
   162
  Theory.pre_pure
wenzelm@3987
   163
  |> Theory.init_data theorems theorems_methods
wenzelm@3987
   164
  |> Theory.add_types
wenzelm@3987
   165
   (("fun", 2, NoSyn) ::
wenzelm@3987
   166
    ("prop", 0, NoSyn) ::
wenzelm@3987
   167
    ("itself", 1, NoSyn) ::
wenzelm@3987
   168
    Syntax.pure_types)
wenzelm@3987
   169
  |> Theory.add_classes_i [(logicC, [])]
wenzelm@3987
   170
  |> Theory.add_defsort_i logicS
wenzelm@3987
   171
  |> Theory.add_arities_i
wenzelm@3987
   172
   [("fun", [logicS, logicS], logicS),
wenzelm@3987
   173
    ("prop", [], logicS),
wenzelm@3987
   174
    ("itself", [logicS], logicS)]
wenzelm@3987
   175
  |> Theory.add_syntax Syntax.pure_syntax
wenzelm@3987
   176
  |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax
wenzelm@3987
   177
  |> Theory.add_trfuns Syntax.pure_trfuns
wenzelm@3987
   178
  |> Theory.add_trfunsT Syntax.pure_trfunsT
wenzelm@3987
   179
  |> Theory.add_syntax
wenzelm@3987
   180
   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
wenzelm@3987
   181
  |> Theory.add_consts
wenzelm@3987
   182
   [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
wenzelm@3987
   183
    ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
wenzelm@3987
   184
    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
wenzelm@3987
   185
    ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
wenzelm@3987
   186
    ("TYPE", "'a itself", NoSyn)]
wenzelm@3987
   187
  |> Theory.add_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
wenzelm@3987
   188
  |> Theory.add_name "ProtoPure";
wenzelm@3987
   189
wenzelm@3987
   190
val pure = proto_pure
wenzelm@3987
   191
  |> Theory.add_syntax Syntax.pure_appl_syntax
wenzelm@3987
   192
  |> Theory.add_name "Pure";
wenzelm@3987
   193
wenzelm@3987
   194
val cpure = proto_pure
wenzelm@3987
   195
  |> Theory.add_syntax Syntax.pure_applC_syntax
wenzelm@3987
   196
  |> Theory.add_name "CPure";
wenzelm@3987
   197
wenzelm@3987
   198
wenzelm@3987
   199
end;
wenzelm@3987
   200
wenzelm@3987
   201
wenzelm@3987
   202
wenzelm@3987
   203
(** theory structures **)
wenzelm@3987
   204
wenzelm@3987
   205
structure ProtoPure =
wenzelm@3987
   206
struct
wenzelm@3987
   207
  val thy = PureThy.proto_pure;
wenzelm@3987
   208
  val flexpair_def = get_axiom thy "flexpair_def";
wenzelm@3987
   209
end;
wenzelm@3987
   210
wenzelm@3987
   211
structure Pure = struct val thy = PureThy.pure end;
wenzelm@3987
   212
structure CPure = struct val thy = PureThy.cpure end;