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