Init 'theorems' data. The Pure theories.
authorwenzelm
Fri Oct 24 17:11:23 1997 +0200 (1997-10-24)
changeset 398722f5291012df
parent 3986 d788dcb86930
child 3988 6ff1a1e2bd21
Init 'theorems' data. The Pure theories.
src/Pure/pure_thy.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/pure_thy.ML	Fri Oct 24 17:11:23 1997 +0200
     1.3 @@ -0,0 +1,212 @@
     1.4 +(*  Title:      Pure/pure_thy.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Init 'theorems' data.  The Pure theories.
     1.9 +*)
    1.10 +
    1.11 +signature PURE_THY =
    1.12 +sig
    1.13 +  val put_thms: (bstring * thm) list -> theory -> theory        (*DESTRUCTIVE*)
    1.14 +  val put_thmss: (bstring * thm list) list -> theory -> theory  (*DESTRUCTIVE*)
    1.15 +  val store_thm: (bstring * thm) -> thm                         (*DESTRUCTIVE*)
    1.16 +  val get_thm: theory -> xstring -> thm
    1.17 +  val get_thms: theory -> xstring -> thm list
    1.18 +  val proto_pure: theory
    1.19 +  val pure: theory
    1.20 +  val cpure: theory
    1.21 +end;
    1.22 +
    1.23 +structure PureThy: PURE_THY =
    1.24 +struct
    1.25 +
    1.26 +
    1.27 +(** init theorems data **)
    1.28 +
    1.29 +(* data kind theorems *)
    1.30 +
    1.31 +val theorems = "theorems";
    1.32 +
    1.33 +exception Theorems of
    1.34 +  {space: NameSpace.T, thms_tab: thm list Symtab.table} ref;
    1.35 +
    1.36 +
    1.37 +(* methods *)
    1.38 +
    1.39 +local
    1.40 +
    1.41 +val empty =
    1.42 +  Theorems (ref {space = NameSpace.empty, thms_tab = Symtab.null});
    1.43 +
    1.44 +fun ext (Theorems (ref {space, ...})) =
    1.45 +  Theorems (ref {space = space, thms_tab = Symtab.null});
    1.46 +
    1.47 +fun merge (Theorems (ref {space = space1, ...}), Theorems (ref {space = space2, ...})) =
    1.48 +  Theorems (ref {space = NameSpace.merge (space1, space2), thms_tab = Symtab.null});
    1.49 +
    1.50 +fun print (Theorems (ref {space, thms_tab})) =
    1.51 +  let
    1.52 +    val prt_thm = Pretty.quote o pretty_thm;
    1.53 +    fun prt_thms (name, [th]) =
    1.54 +          Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, (prt_thm th)]
    1.55 +      | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
    1.56 +
    1.57 +    fun extrn name =
    1.58 +      if ! long_names then name else NameSpace.extern space name;
    1.59 +    val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab));
    1.60 +  in
    1.61 +    Pretty.writeln (Pretty.strs ("theorem name space:" :: map quote (NameSpace.dest space)));
    1.62 +    Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
    1.63 +  end;
    1.64 +
    1.65 +in
    1.66 +
    1.67 +val theorems_methods = (empty, ext, merge, print);
    1.68 +
    1.69 +end;
    1.70 +
    1.71 +
    1.72 +(* get data record *)
    1.73 +
    1.74 +fun get_theorems sg =
    1.75 +  (case Sign.get_data sg theorems of
    1.76 +    Theorems r => r
    1.77 +  | _ => sys_error "get_theorems");
    1.78 +
    1.79 +
    1.80 +(* retrieve theorems *)
    1.81 +
    1.82 +fun lookup_thms theory full_name =
    1.83 +  let
    1.84 +    val tab_of = #thms_tab o ! o get_theorems o sign_of;
    1.85 +    fun lookup [] = raise Match
    1.86 +      | lookup (thy :: thys) =
    1.87 +          (case Symtab.lookup (tab_of thy, full_name) of
    1.88 +            Some thms => thms
    1.89 +          | None => lookup (Theory.parents_of thy) handle Match => lookup thys)
    1.90 +  in
    1.91 +    lookup [theory] handle Match
    1.92 +      => raise THEORY ("No theorems " ^ quote full_name ^ " stored in theory", [theory])
    1.93 +  end;
    1.94 +
    1.95 +fun get_thms thy name =
    1.96 +  let
    1.97 +    val ref {space, ...} = get_theorems (sign_of thy);
    1.98 +    val full_name = NameSpace.intern space name;
    1.99 +  in lookup_thms thy full_name end;
   1.100 +
   1.101 +fun get_thm thy name =
   1.102 +  (case get_thms thy name of
   1.103 +    [thm] => thm
   1.104 +  | _ => raise THEORY ("Singleton theorem list expected " ^ quote name, [thy]));
   1.105 +
   1.106 +
   1.107 +(* store theorems *)                    (*DESTRUCTIVE*)
   1.108 +
   1.109 +fun err_dup name =
   1.110 +  error ("Duplicate theorems " ^ quote name);
   1.111 +
   1.112 +fun warn_overwrite name =
   1.113 +  warning ("Replaced old copy of theorems " ^ quote name);
   1.114 +
   1.115 +fun warn_same name =
   1.116 +  warning ("Theorem database already contains a copy of " ^ quote name);
   1.117 +
   1.118 +
   1.119 +fun enter_thms sg single (raw_name, thms) =
   1.120 +  let
   1.121 +    val len = length thms;
   1.122 +    val name = Sign.full_name sg raw_name;
   1.123 +    val names =
   1.124 +      if single then replicate len name
   1.125 +      else map (fn i => name ^ "_" ^ string_of_int i) (0 upto (len - 1));
   1.126 +    val named_thms = ListPair.map Thm.name_thm (names, thms);
   1.127 +
   1.128 +    val eq_thms = ListPair.all Thm.eq_thm;
   1.129 +    val r as ref {space, thms_tab = tab} = get_theorems sg;
   1.130 +  in
   1.131 +    (case Symtab.lookup (tab, name) of
   1.132 +      None =>
   1.133 +        if NameSpace.declared space name then err_dup name else ()
   1.134 +    | Some thms' =>
   1.135 +        if length thms' = len andalso eq_thms (thms', named_thms) then
   1.136 +          warn_overwrite name
   1.137 +        else warn_same name);
   1.138 +
   1.139 +    r :=
   1.140 +     {space = NameSpace.extend ([name], space),
   1.141 +      thms_tab = Symtab.update ((name, named_thms), tab)};
   1.142 +
   1.143 +    named_thms
   1.144 +  end;
   1.145 +
   1.146 +fun do_enter_thms sg single name_thms =
   1.147 +  (enter_thms sg single name_thms; ());
   1.148 +
   1.149 +
   1.150 +fun put_thmss thmss thy =
   1.151 +  (seq (do_enter_thms (sign_of thy) false) thmss; thy);
   1.152 +
   1.153 +fun put_thms thms thy =
   1.154 +  (seq (do_enter_thms (sign_of thy) true) (map (apsnd (fn th => [th])) thms); thy);
   1.155 +
   1.156 +fun store_thm (name, thm) =
   1.157 +  let val [named_thm] = enter_thms (Thm.sign_of_thm thm) true (name, [thm])
   1.158 +  in named_thm end;
   1.159 +
   1.160 +
   1.161 +
   1.162 +(** the Pure theories **)
   1.163 +
   1.164 +val proto_pure =
   1.165 +  Theory.pre_pure
   1.166 +  |> Theory.init_data theorems theorems_methods
   1.167 +  |> Theory.add_types
   1.168 +   (("fun", 2, NoSyn) ::
   1.169 +    ("prop", 0, NoSyn) ::
   1.170 +    ("itself", 1, NoSyn) ::
   1.171 +    Syntax.pure_types)
   1.172 +  |> Theory.add_classes_i [(logicC, [])]
   1.173 +  |> Theory.add_defsort_i logicS
   1.174 +  |> Theory.add_arities_i
   1.175 +   [("fun", [logicS, logicS], logicS),
   1.176 +    ("prop", [], logicS),
   1.177 +    ("itself", [logicS], logicS)]
   1.178 +  |> Theory.add_syntax Syntax.pure_syntax
   1.179 +  |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax
   1.180 +  |> Theory.add_trfuns Syntax.pure_trfuns
   1.181 +  |> Theory.add_trfunsT Syntax.pure_trfunsT
   1.182 +  |> Theory.add_syntax
   1.183 +   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
   1.184 +  |> Theory.add_consts
   1.185 +   [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   1.186 +    ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   1.187 +    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   1.188 +    ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   1.189 +    ("TYPE", "'a itself", NoSyn)]
   1.190 +  |> Theory.add_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
   1.191 +  |> Theory.add_name "ProtoPure";
   1.192 +
   1.193 +val pure = proto_pure
   1.194 +  |> Theory.add_syntax Syntax.pure_appl_syntax
   1.195 +  |> Theory.add_name "Pure";
   1.196 +
   1.197 +val cpure = proto_pure
   1.198 +  |> Theory.add_syntax Syntax.pure_applC_syntax
   1.199 +  |> Theory.add_name "CPure";
   1.200 +
   1.201 +
   1.202 +end;
   1.203 +
   1.204 +
   1.205 +
   1.206 +(** theory structures **)
   1.207 +
   1.208 +structure ProtoPure =
   1.209 +struct
   1.210 +  val thy = PureThy.proto_pure;
   1.211 +  val flexpair_def = get_axiom thy "flexpair_def";
   1.212 +end;
   1.213 +
   1.214 +structure Pure = struct val thy = PureThy.pure end;
   1.215 +structure CPure = struct val thy = PureThy.cpure end;