# HG changeset patch # User wenzelm # Date 877705883 -7200 # Node ID 22f5291012dfef7d63abbbd00b40e5219c7ceea0 # Parent d788dcb86930031f8ad7031388238193a2c157c1 Init 'theorems' data. The Pure theories. diff -r d788dcb86930 -r 22f5291012df src/Pure/pure_thy.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/pure_thy.ML Fri Oct 24 17:11:23 1997 +0200 @@ -0,0 +1,212 @@ +(* Title: Pure/pure_thy.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Init 'theorems' data. The Pure theories. +*) + +signature PURE_THY = +sig + val put_thms: (bstring * thm) list -> theory -> theory (*DESTRUCTIVE*) + val put_thmss: (bstring * thm list) list -> theory -> theory (*DESTRUCTIVE*) + val store_thm: (bstring * thm) -> thm (*DESTRUCTIVE*) + val get_thm: theory -> xstring -> thm + val get_thms: theory -> xstring -> thm list + val proto_pure: theory + val pure: theory + val cpure: theory +end; + +structure PureThy: PURE_THY = +struct + + +(** init theorems data **) + +(* data kind theorems *) + +val theorems = "theorems"; + +exception Theorems of + {space: NameSpace.T, thms_tab: thm list Symtab.table} ref; + + +(* methods *) + +local + +val empty = + Theorems (ref {space = NameSpace.empty, thms_tab = Symtab.null}); + +fun ext (Theorems (ref {space, ...})) = + Theorems (ref {space = space, thms_tab = Symtab.null}); + +fun merge (Theorems (ref {space = space1, ...}), Theorems (ref {space = space2, ...})) = + Theorems (ref {space = NameSpace.merge (space1, space2), thms_tab = Symtab.null}); + +fun print (Theorems (ref {space, thms_tab})) = + let + val prt_thm = Pretty.quote o pretty_thm; + fun prt_thms (name, [th]) = + Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, (prt_thm th)] + | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths); + + fun extrn name = + if ! long_names then name else NameSpace.extern space name; + val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab)); + in + Pretty.writeln (Pretty.strs ("theorem name space:" :: map quote (NameSpace.dest space))); + Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss)) + end; + +in + +val theorems_methods = (empty, ext, merge, print); + +end; + + +(* get data record *) + +fun get_theorems sg = + (case Sign.get_data sg theorems of + Theorems r => r + | _ => sys_error "get_theorems"); + + +(* retrieve theorems *) + +fun lookup_thms theory full_name = + let + val tab_of = #thms_tab o ! o get_theorems o sign_of; + fun lookup [] = raise Match + | lookup (thy :: thys) = + (case Symtab.lookup (tab_of thy, full_name) of + Some thms => thms + | None => lookup (Theory.parents_of thy) handle Match => lookup thys) + in + lookup [theory] handle Match + => raise THEORY ("No theorems " ^ quote full_name ^ " stored in theory", [theory]) + end; + +fun get_thms thy name = + let + val ref {space, ...} = get_theorems (sign_of thy); + val full_name = NameSpace.intern space name; + in lookup_thms thy full_name end; + +fun get_thm thy name = + (case get_thms thy name of + [thm] => thm + | _ => raise THEORY ("Singleton theorem list expected " ^ quote name, [thy])); + + +(* store theorems *) (*DESTRUCTIVE*) + +fun err_dup name = + error ("Duplicate theorems " ^ quote name); + +fun warn_overwrite name = + warning ("Replaced old copy of theorems " ^ quote name); + +fun warn_same name = + warning ("Theorem database already contains a copy of " ^ quote name); + + +fun enter_thms sg single (raw_name, thms) = + let + val len = length thms; + val name = Sign.full_name sg raw_name; + val names = + if single then replicate len name + else map (fn i => name ^ "_" ^ string_of_int i) (0 upto (len - 1)); + val named_thms = ListPair.map Thm.name_thm (names, thms); + + val eq_thms = ListPair.all Thm.eq_thm; + val r as ref {space, thms_tab = tab} = get_theorems sg; + in + (case Symtab.lookup (tab, name) of + None => + if NameSpace.declared space name then err_dup name else () + | Some thms' => + if length thms' = len andalso eq_thms (thms', named_thms) then + warn_overwrite name + else warn_same name); + + r := + {space = NameSpace.extend ([name], space), + thms_tab = Symtab.update ((name, named_thms), tab)}; + + named_thms + end; + +fun do_enter_thms sg single name_thms = + (enter_thms sg single name_thms; ()); + + +fun put_thmss thmss thy = + (seq (do_enter_thms (sign_of thy) false) thmss; thy); + +fun put_thms thms thy = + (seq (do_enter_thms (sign_of thy) true) (map (apsnd (fn th => [th])) thms); thy); + +fun store_thm (name, thm) = + let val [named_thm] = enter_thms (Thm.sign_of_thm thm) true (name, [thm]) + in named_thm end; + + + +(** the Pure theories **) + +val proto_pure = + Theory.pre_pure + |> Theory.init_data theorems theorems_methods + |> Theory.add_types + (("fun", 2, NoSyn) :: + ("prop", 0, NoSyn) :: + ("itself", 1, NoSyn) :: + Syntax.pure_types) + |> Theory.add_classes_i [(logicC, [])] + |> Theory.add_defsort_i logicS + |> Theory.add_arities_i + [("fun", [logicS, logicS], logicS), + ("prop", [], logicS), + ("itself", [logicS], logicS)] + |> Theory.add_syntax Syntax.pure_syntax + |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax + |> Theory.add_trfuns Syntax.pure_trfuns + |> Theory.add_trfunsT Syntax.pure_trfunsT + |> Theory.add_syntax + [("==>", "[prop, prop] => prop", Delimfix "op ==>")] + |> Theory.add_consts + [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)), + ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)), + ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), + ("all", "('a => prop) => prop", Binder ("!!", 0, 0)), + ("TYPE", "'a itself", NoSyn)] + |> Theory.add_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")] + |> Theory.add_name "ProtoPure"; + +val pure = proto_pure + |> Theory.add_syntax Syntax.pure_appl_syntax + |> Theory.add_name "Pure"; + +val cpure = proto_pure + |> Theory.add_syntax Syntax.pure_applC_syntax + |> Theory.add_name "CPure"; + + +end; + + + +(** theory structures **) + +structure ProtoPure = +struct + val thy = PureThy.proto_pure; + val flexpair_def = get_axiom thy "flexpair_def"; +end; + +structure Pure = struct val thy = PureThy.pure end; +structure CPure = struct val thy = PureThy.cpure end;