src/Pure/pure_thy.ML
author wenzelm
Sat Nov 24 16:55:56 2001 +0100 (2001-11-24)
changeset 12284 131e743d168a
parent 12250 c9ff220cb6c7
child 12311 ce5f9e61c037
permissions -rw-r--r--
added gen_merge_lists(') and merge_lists(');
removed obsolete generic_extend, generic_merge, extend_list;
     1 (*  Title:      Pure/pure_thy.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Theorem database, derived theory operations, and the ProtoPure theory.
     7 *)
     8 
     9 signature BASIC_PURE_THY =
    10 sig
    11   val print_theorems: theory -> unit
    12   val print_theory: theory -> unit
    13   val get_thm: theory -> xstring -> thm
    14   val get_thms: theory -> xstring -> thm list
    15   val get_thmss: theory -> xstring list -> thm list
    16   val thms_of: theory -> (string * thm) list
    17   structure ProtoPure:
    18     sig
    19       val thy: theory
    20       val flexpair_def: thm
    21       val Goal_def: thm
    22     end
    23 end;
    24 
    25 signature PURE_THY =
    26 sig
    27   include BASIC_PURE_THY
    28   val get_thm_closure: theory -> xstring -> thm
    29   val get_thms_closure: theory -> xstring -> thm list
    30   val single_thm: string -> thm list -> thm
    31   val cond_extern_thm_sg: Sign.sg -> string -> xstring
    32   val thms_containing: theory -> string list -> (string * thm) list
    33   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
    34   val smart_store_thms: (bstring * thm list) -> thm list
    35   val smart_store_thms_open: (bstring * thm list) -> thm list
    36   val forall_elim_var: int -> thm -> thm
    37   val forall_elim_vars: int -> thm -> thm
    38   val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
    39   val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory * thm list list
    40   val have_thmss: theory attribute list -> ((bstring * theory attribute list) *
    41     (thm list * theory attribute list) list) list -> theory -> theory * (string * thm list) list
    42   val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
    43   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
    44   val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list
    45   val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list
    46   val add_defs: bool -> ((bstring * string) * theory attribute list) list
    47     -> theory -> theory * thm list
    48   val add_defs_i: bool -> ((bstring * term) * theory attribute list) list
    49     -> theory -> theory * thm list
    50   val add_defss: bool -> ((bstring * string list) * theory attribute list) list
    51     -> theory -> theory * thm list list
    52   val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list
    53     -> theory -> theory * thm list list
    54   val get_name: theory -> string
    55   val put_name: string -> theory -> theory
    56   val global_path: theory -> theory
    57   val local_path: theory -> theory
    58   val begin_theory: string -> theory list -> theory
    59   val end_theory: theory -> theory
    60   val checkpoint: theory -> theory
    61   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    62 end;
    63 
    64 structure PureThy: PURE_THY =
    65 struct
    66 
    67 
    68 (*** theorem database ***)
    69 
    70 (** data kind 'Pure/theorems' **)
    71 
    72 structure TheoremsDataArgs =
    73 struct
    74   val name = "Pure/theorems";
    75 
    76   type T =
    77     {space: NameSpace.T,
    78       thms_tab: thm list Symtab.table,
    79       const_idx: int * (int * thm) list Symtab.table} ref;
    80 
    81   fun mk_empty _ =
    82     ref {space = NameSpace.empty, thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)} : T;
    83 
    84   val empty = mk_empty ();
    85   fun copy (ref x) = ref x;
    86   val finish = I;
    87   val prep_ext = mk_empty;
    88   val merge = mk_empty;
    89 
    90   fun pretty sg (ref {space, thms_tab, const_idx = _}) =
    91     let
    92       val prt_thm = Display.pretty_thm_sg sg;
    93       fun prt_thms (name, [th]) =
    94             Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
    95         | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
    96 
    97       val thmss = NameSpace.cond_extern_table space thms_tab;
    98     in Pretty.big_list "theorems:" (map prt_thms thmss) end;
    99 
   100   fun print sg data = Pretty.writeln (pretty sg data);
   101 end;
   102 
   103 structure TheoremsData = TheoryDataFun(TheoremsDataArgs);
   104 val get_theorems_sg = TheoremsData.get_sg;
   105 val get_theorems = TheoremsData.get;
   106 
   107 val cond_extern_thm_sg = NameSpace.cond_extern o #space o ! o get_theorems_sg;
   108 
   109 
   110 (* print theory *)
   111 
   112 val print_theorems = TheoremsData.print;
   113 
   114 fun print_theory thy =
   115   Display.pretty_full_theory thy @
   116   [TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)]
   117   |> Pretty.chunks |> Pretty.writeln;
   118 
   119 
   120 
   121 (** retrieve theorems **)
   122 
   123 (* selections *)
   124 
   125 fun the_thms _ (Some thms) = thms
   126   | the_thms name None = error ("Unknown theorem(s) " ^ quote name);
   127 
   128 fun single_thm _ [thm] = thm
   129   | single_thm name _ = error ("Single theorem expected " ^ quote name);
   130 
   131 
   132 (* get_thm(s)_closure -- statically scoped versions *)
   133 
   134 (*beware of proper order of evaluation!*)
   135 
   136 fun lookup_thms thy =
   137   let
   138     val sg_ref = Sign.self_ref (Theory.sign_of thy);
   139     val ref {space, thms_tab, ...} = get_theorems thy;
   140   in
   141     fn name =>
   142       apsome (map (Thm.transfer_sg (Sign.deref sg_ref)))        (*semi-dynamic identity*)
   143       (Symtab.lookup (thms_tab, NameSpace.intern space name))   (*static content*)
   144   end;
   145 
   146 fun get_thms_closure thy =
   147   let val closures = map lookup_thms (thy :: Theory.ancestors_of thy)
   148   in fn name => the_thms name (get_first (fn f => f name) closures) end;
   149 
   150 fun get_thm_closure thy =
   151   let val get = get_thms_closure thy
   152   in fn name => single_thm name (get name) end;
   153 
   154 
   155 (* get_thm etc. *)
   156 
   157 fun get_thms theory name =
   158   get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
   159   |> the_thms name |> map (Thm.transfer theory);
   160 
   161 fun get_thmss thy names = flat (map (get_thms thy) names);
   162 fun get_thm thy name = single_thm name (get_thms thy name);
   163 
   164 
   165 (* thms_of *)
   166 
   167 fun attach_name thm = (Thm.name_of_thm thm, thm);
   168 
   169 fun thms_of thy =
   170   let val ref {thms_tab, ...} = get_theorems thy in
   171     map attach_name (flat (map snd (Symtab.dest thms_tab)))
   172   end;
   173 
   174 
   175 
   176 (** theorems indexed by constants **)
   177 
   178 (* make index *)
   179 
   180 fun add_const_idx ((next, table), thm) =
   181   let
   182     val {hyps, prop, ...} = Thm.rep_thm thm;
   183     val consts =
   184       foldr add_term_consts (hyps, add_term_consts (prop, []));
   185 
   186     fun add (tab, c) =
   187       Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab);
   188   in (next + 1, foldl add (table, consts)) end;
   189 
   190 fun make_const_idx thm_tab =
   191   Symtab.foldl (fn (x, (_, ths)) => foldl add_const_idx (x, ths)) ((0, Symtab.empty), thm_tab);
   192 
   193 
   194 (* lookup index *)
   195 
   196 (*search locally*)
   197 fun containing [] thy = thms_of thy
   198   | containing consts thy =
   199       let
   200         fun int ([], _) = []
   201           | int (_, []) = []
   202           | int (xxs as ((x as (i:int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
   203               if i = j then x :: int (xs, ys)
   204               else if i > j then int (xs, yys)
   205               else int (xxs, ys);
   206 
   207         fun ints [xs] = xs
   208           | ints xss = if exists null xss then [] else foldl int (hd xss, tl xss);
   209 
   210         val ref {const_idx = (_, ctab), ...} = get_theorems thy;
   211         val ithmss = map (fn c => Symtab.lookup_multi (ctab, c)) consts;
   212       in map (attach_name o snd) (ints ithmss) end;
   213 
   214 (*search globally*)
   215 fun thms_containing thy consts =
   216   (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
   217     [] => flat (map (containing consts) (thy :: Theory.ancestors_of thy))
   218   | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy]))
   219   |> map (apsnd (Thm.transfer thy));
   220 
   221 
   222 
   223 (** store theorems **)                    (*DESTRUCTIVE*)
   224 
   225 (* naming *)
   226 
   227 fun gen_names j len name =
   228   map (fn i => name ^ "_" ^ string_of_int i) (j+1 upto j+len);
   229 
   230 fun name_multi name xs = gen_names 0 (length xs) name ~~ xs;
   231 
   232 fun name_thms name [x] = [Thm.name_thm (name, x)]
   233   | name_thms name xs = map Thm.name_thm (name_multi name xs);
   234 
   235 fun name_thmss name xs = (case filter_out (null o fst) xs of
   236     [([x], z)] => [([Thm.name_thm (name, x)], z)]
   237   | _ => snd (foldl_map (fn (i, (ys, z)) => (i + length ys,
   238   (map Thm.name_thm (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
   239 
   240 
   241 (* enter_thms *)
   242 
   243 fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
   244 fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
   245 
   246 fun enter_thms _ _ _ app_att thy ("", thms) = app_att (thy, thms)
   247   | enter_thms sg pre_name post_name app_att thy (bname, thms) =
   248       let
   249         val name = Sign.full_name sg bname;
   250         val (thy', thms') = app_att (thy, pre_name name thms);
   251         val named_thms = post_name name thms';
   252 
   253         val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
   254 
   255         val overwrite =
   256           (case Symtab.lookup (thms_tab, name) of
   257             None => false
   258           | Some thms' =>
   259               if Library.equal_lists Thm.eq_thm (thms', named_thms) then (warn_same name; false)
   260               else (warn_overwrite name; true));
   261 
   262         val space' = NameSpace.extend (space, [name]);
   263         val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
   264         val const_idx' =
   265           if overwrite then make_const_idx thms_tab'
   266           else foldl add_const_idx (const_idx, named_thms);
   267       in r := {space = space', thms_tab = thms_tab', const_idx = const_idx'};
   268         (thy', named_thms)
   269       end;
   270 
   271 
   272 (* add_thms(s) *)
   273 
   274 fun add_thms_atts pre_name ((bname, thms), atts) thy =
   275   enter_thms (Theory.sign_of thy) pre_name name_thms
   276     (Thm.applys_attributes o rpair atts) thy (bname, thms);
   277 
   278 fun gen_add_thmss pre_name args theory =
   279   foldl_map (fn (thy, arg) => add_thms_atts pre_name arg thy) (theory, args);
   280 
   281 fun gen_add_thms pre_name args =
   282   apsnd (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
   283 
   284 val add_thmss = gen_add_thmss name_thms;
   285 val add_thms = gen_add_thms name_thms;
   286 
   287 
   288 (* have_thmss *)
   289 
   290 local
   291   fun have_thss kind_atts (thy, ((bname, more_atts), ths_atts)) =
   292     let
   293       fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
   294       val (thy', thms) = enter_thms (Theory.sign_of thy)
   295         name_thmss name_thms (apsnd flat o foldl_map app) thy
   296         (bname, map (fn (ths, atts) =>
   297           (ths, atts @ more_atts @ kind_atts)) ths_atts);
   298     in (thy', (bname, thms)) end;
   299 in
   300   fun have_thmss kind_atts args thy = foldl_map (have_thss kind_atts) (thy, args);
   301 end;
   302 
   303 
   304 (* store_thm *)
   305 
   306 fun store_thm ((bname, thm), atts) thy =
   307   let val (thy', [th']) = add_thms_atts name_thms ((bname, [thm]), atts) thy
   308   in (thy', th') end;
   309 
   310 
   311 (* smart_store_thms *)
   312 
   313 fun gen_smart_store_thms _ (name, []) =
   314       error ("Cannot store empty list of theorems: " ^ quote name)
   315   | gen_smart_store_thms name_thm (name, [thm]) =
   316       snd (enter_thms (Thm.sign_of_thm thm) name_thm name_thm I () (name, [thm]))
   317   | gen_smart_store_thms name_thm (name, thms) =
   318       let
   319         val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm);
   320         val sg_ref = foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms);
   321       in snd (enter_thms (Sign.deref sg_ref) name_thm name_thm I () (name, thms)) end;
   322 
   323 val smart_store_thms = gen_smart_store_thms name_thms;
   324 val smart_store_thms_open = gen_smart_store_thms (K I);
   325 
   326 
   327 (* forall_elim_vars (belongs to drule.ML) *)
   328 
   329 (*Replace outermost quantified variable by Var of given index.
   330     Could clash with Vars already present.*)
   331 fun forall_elim_var i th =
   332     let val {prop,sign,...} = rep_thm th
   333     in case prop of
   334           Const("all",_) $ Abs(a,T,_) =>
   335               forall_elim (cterm_of sign (Var((a,i), T)))  th
   336         | _ => raise THM("forall_elim_var", i, [th])
   337     end;
   338 
   339 (*Repeat forall_elim_var until all outer quantifiers are removed*)
   340 fun forall_elim_vars i th =
   341     forall_elim_vars i (forall_elim_var i th)
   342         handle THM _ => th;
   343 
   344 
   345 (* store axioms as theorems *)
   346 
   347 local
   348   fun get_axs thy named_axs =
   349     map (forall_elim_vars 0 o Thm.get_axiom thy o fst) named_axs;
   350 
   351   fun add_single add (thy, ((name, ax), atts)) =
   352     let
   353       val named_ax = [(name, ax)];
   354       val thy' = add named_ax thy;
   355       val thm = hd (get_axs thy' named_ax);
   356     in apsnd hd (gen_add_thms (K I) [((name, thm), atts)] thy') end;
   357 
   358   fun add_multi add (thy, ((name, axs), atts)) =
   359     let
   360       val named_axs = name_multi name axs;
   361       val thy' = add named_axs thy;
   362       val thms = get_axs thy' named_axs;
   363     in apsnd hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end;
   364 
   365   fun add_singles add args thy = foldl_map (add_single add) (thy, args);
   366   fun add_multis add args thy = foldl_map (add_multi add) (thy, args);
   367 in
   368   val add_axioms    = add_singles Theory.add_axioms;
   369   val add_axioms_i  = add_singles Theory.add_axioms_i;
   370   val add_axiomss   = add_multis Theory.add_axioms;
   371   val add_axiomss_i = add_multis Theory.add_axioms_i;
   372   val add_defs      = add_singles o Theory.add_defs;
   373   val add_defs_i    = add_singles o Theory.add_defs_i;
   374   val add_defss     = add_multis o Theory.add_defs;
   375   val add_defss_i   = add_multis o Theory.add_defs_i;
   376 end;
   377 
   378 
   379 
   380 (*** derived theory operations ***)
   381 
   382 (** theory management **)
   383 
   384 (* data kind 'Pure/theory_management' *)
   385 
   386 structure TheoryManagementDataArgs =
   387 struct
   388   val name = "Pure/theory_management";
   389   type T = {name: string, version: int};
   390 
   391   val empty = {name = "", version = 0};
   392   val copy = I;
   393   val finish = I;
   394   val prep_ext  = I;
   395   fun merge _ = empty;
   396   fun print _ _ = ();
   397 end;
   398 
   399 structure TheoryManagementData = TheoryDataFun(TheoryManagementDataArgs);
   400 val get_info = TheoryManagementData.get;
   401 val put_info = TheoryManagementData.put;
   402 
   403 
   404 (* get / put name *)
   405 
   406 val get_name = #name o get_info;
   407 fun put_name name = put_info {name = name, version = 0};
   408 
   409 
   410 (* control prefixing of theory name *)
   411 
   412 val global_path = Theory.root_path;
   413 
   414 fun local_path thy =
   415   thy |> Theory.root_path |> Theory.add_path (get_name thy);
   416 
   417 
   418 (* begin / end theory *)
   419 
   420 fun begin_theory name thys =
   421   Theory.prep_ext_merge thys
   422   |> put_name name
   423   |> local_path;
   424 
   425 fun end_theory thy =
   426   thy
   427   |> Theory.finish
   428   |> Theory.add_name (get_name thy);
   429 
   430 fun checkpoint thy =
   431   if is_draft thy then
   432     let val {name, version} = get_info thy in
   433       thy
   434       |> Theory.add_name (name ^ ":" ^ string_of_int version)
   435       |> put_info {name = name, version = version + 1}
   436     end
   437   else thy;
   438 
   439 
   440 
   441 (** add logical types **)
   442 
   443 fun add_typedecls decls thy =
   444   let
   445     val full = Sign.full_name (Theory.sign_of thy);
   446 
   447     fun type_of (raw_name, vs, mx) =
   448       if null (duplicates vs) then (raw_name, length vs, mx)
   449       else error ("Duplicate parameters in type declaration: " ^ quote raw_name);
   450 
   451     fun arity_of (raw_name, len, mx) =
   452       (full (Syntax.type_name raw_name mx), replicate len logicS, logicS);
   453 
   454     val types = map type_of decls;
   455     val arities = map arity_of types;
   456   in
   457     thy
   458     |> Theory.add_types types
   459     |> Theory.add_arities_i arities
   460   end;
   461 
   462 
   463 
   464 (*** the ProtoPure theory ***)
   465 
   466 val proto_pure =
   467   Theory.pre_pure
   468   |> Library.apply [TheoremsData.init, TheoryManagementData.init, Proofterm.init]
   469   |> put_name "ProtoPure"
   470   |> global_path
   471   |> Theory.add_types
   472    [("fun", 2, NoSyn),
   473     ("prop", 0, NoSyn),
   474     ("itself", 1, NoSyn),
   475     ("dummy", 0, NoSyn)]
   476   |> Theory.add_classes_i [(logicC, [])]
   477   |> Theory.add_defsort_i logicS
   478   |> Theory.add_arities_i
   479    [("fun", [logicS, logicS], logicS),
   480     ("prop", [], logicS),
   481     ("itself", [logicS], logicS)]
   482   |> Theory.add_nonterminals Syntax.pure_nonterms
   483   |> Theory.add_syntax Syntax.pure_syntax
   484   |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
   485   |> Theory.add_syntax
   486    [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
   487     (Term.dummy_patternN, "aprop", Delimfix "'_")]
   488   |> Theory.add_consts
   489    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   490     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   491     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   492     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   493     ("Goal", "prop => prop", NoSyn),
   494     ("TYPE", "'a itself", NoSyn),
   495     (Term.dummy_patternN, "'a", Delimfix "'_")]
   496   |> Theory.add_modesyntax ("", false)
   497     (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
   498   |> Theory.add_trfuns Syntax.pure_trfuns
   499   |> Theory.add_trfunsT Syntax.pure_trfunsT
   500   |> local_path
   501   |> (#1 oo (add_defs false o map Thm.no_attributes))
   502    [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
   503   |> (#1 oo (add_defs_i false o map Thm.no_attributes))
   504    [("Goal_def", let val A = Free ("A", propT) in Logic.mk_equals (Logic.mk_goal A, A) end)]
   505   |> (#1 o add_thmss [(("nothing", []), [])])
   506   |> Theory.add_axioms_i Proofterm.equality_axms
   507   |> end_theory;
   508 
   509 structure ProtoPure =
   510 struct
   511   val thy = proto_pure;
   512   val flexpair_def = get_axiom thy "flexpair_def";
   513   val Goal_def = get_axiom thy "Goal_def";
   514 end;
   515 
   516 
   517 end;
   518 
   519 
   520 structure BasicPureThy: BASIC_PURE_THY = PureThy;
   521 open BasicPureThy;