src/Pure/pure_thy.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5933 7b0f502a25b1
child 6027 9dd06eeda95c
permissions -rw-r--r--
tidying
     1 (*  Title:      Pure/pure_thy.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Theorem database, derived theory operations, and the ProtoPure theory.
     6 *)
     7 
     8 signature BASIC_PURE_THY =
     9 sig
    10   val print_theorems: theory -> unit
    11   val print_theory: theory -> unit
    12   val get_thm: theory -> xstring -> thm
    13   val get_thms: theory -> xstring -> thm list
    14   val thms_of: theory -> (string * thm) list
    15   structure ProtoPure:
    16     sig
    17       val thy: theory
    18       val flexpair_def: thm
    19       val Goal_def: thm
    20     end
    21 end;
    22 
    23 signature PURE_THY =
    24 sig
    25   include BASIC_PURE_THY
    26   val thms_closure: theory -> xstring -> tthm list option
    27   val get_tthm: theory -> xstring -> tthm
    28   val get_tthms: theory -> xstring -> tthm list
    29   val get_tthmss: theory -> xstring list -> tthm list
    30   val thms_containing: theory -> string list -> (string * thm) list
    31   val default_name: string -> string
    32   val store_tthm: (bstring * tthm) * theory attribute list -> theory -> theory * tthm
    33   val smart_store_thm: (bstring * thm) -> thm
    34   val add_tthms: ((bstring * tthm) * theory attribute list) list -> theory -> theory
    35   val add_tthmss: ((bstring * tthm list) * theory attribute list) list -> theory -> theory
    36   val have_tthmss: bstring -> theory attribute list ->
    37     (tthm list * theory attribute list) list -> theory -> theory * tthm list
    38   val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory
    39   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    40   val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory
    41   val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory
    42   val add_defs: ((bstring * string) * theory attribute list) list -> theory -> theory
    43   val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    44   val add_defss: ((bstring * string list) * theory attribute list) list -> theory -> theory
    45   val add_defss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory
    46   val get_name: theory -> string
    47   val put_name: string -> theory -> theory
    48   val global_path: theory -> theory
    49   val local_path: theory -> theory
    50   val begin_theory: string -> theory list -> theory
    51   val end_theory: theory -> theory
    52   exception ROLLBACK of theory * exn option
    53   val transaction: (theory -> theory) -> theory -> theory
    54   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    55 end;
    56 
    57 structure PureThy: PURE_THY =
    58 struct
    59 
    60 
    61 (*** theorem database ***)
    62 
    63 (** data kind 'Pure/theorems' **)
    64 
    65 structure TheoremsDataArgs =
    66 struct
    67   val name = "Pure/theorems";
    68 
    69   type T =
    70     {space: NameSpace.T,
    71       thms_tab: tthm list Symtab.table,
    72       const_idx: int * (int * tthm) list Symtab.table} ref;
    73 
    74   fun mk_empty _ =
    75     ref {space = NameSpace.empty, thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)} : T;
    76 
    77   val empty = mk_empty ();
    78   val prep_ext = mk_empty;
    79   val merge = mk_empty;
    80 
    81   fun print sg (ref {space, thms_tab, const_idx = _}) =
    82     let
    83       val prt_thm = Attribute.pretty_tthm o apfst (Thm.transfer_sg sg);
    84       fun prt_thms (name, [th]) =
    85             Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
    86         | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
    87 
    88       val thmss = sort_wrt fst (map (apfst (NameSpace.cond_extern space)) (Symtab.dest thms_tab));
    89     in
    90       Pretty.writeln (Display.pretty_name_space ("theorem name space", space));
    91       Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
    92     end;
    93 end;
    94 
    95 structure TheoremsData = TheoryDataFun(TheoremsDataArgs);
    96 val get_theorems_sg = TheoremsData.get_sg;
    97 val get_theorems = TheoremsData.get;
    98 
    99 
   100 (* print theory *)
   101 
   102 val print_theorems = TheoremsData.print;
   103 fun print_theory thy =
   104   (Display.print_theory thy; print_theorems thy);
   105 
   106 
   107 
   108 (** retrieve theorems **)
   109 
   110 (* thms_closure *)
   111 
   112 (*note: we avoid life references to the theory, so users may safely
   113   keep thms_closure with moderate space consumption*)
   114 
   115 fun thms_closure_aux thy =
   116   let val ref {space, thms_tab, ...} = get_theorems thy
   117   in fn name => Symtab.lookup (thms_tab, NameSpace.intern space name) end;
   118 
   119 fun thms_closure thy =
   120   let val closures = map thms_closure_aux (thy :: Theory.ancestors_of thy)
   121   in fn name => get_first (fn f => f name) closures end;
   122 
   123 
   124 (* get_thms etc. *)
   125 
   126 fun lookup_thms name thy = thms_closure_aux thy name;
   127 
   128 fun get_tthms thy name =
   129   (case get_first (lookup_thms name) (thy :: Theory.ancestors_of thy) of
   130     None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy])
   131   | Some thms => thms);
   132 
   133 fun get_tthm thy name =
   134   (case get_tthms thy name of
   135     [thm] => thm
   136   | _ => raise THEORY ("Single theorem expected " ^ quote name, [thy]));
   137 
   138 fun get_tthmss thy names = flat (map (get_tthms thy) names);
   139 
   140 fun get_thms thy = Attribute.thms_of o get_tthms thy;
   141 fun get_thm thy = Attribute.thm_of o get_tthm thy;
   142 
   143 
   144 (* thms_of *)
   145 
   146 fun attach_name (thm, _) = (Thm.name_of_thm thm, thm);
   147 
   148 fun thms_of thy =
   149   let val ref {thms_tab, ...} = get_theorems thy in
   150     map attach_name (flat (map snd (Symtab.dest thms_tab)))
   151   end;
   152 
   153 
   154 
   155 (** theorems indexed by constants **)
   156 
   157 (* make index *)
   158 
   159 val ignore = ["Trueprop", "all", "==>", "=="];
   160 
   161 fun add_const_idx ((next, table), tthm as (thm, _)) =
   162   let
   163     val {hyps, prop, ...} = Thm.rep_thm thm;
   164     val consts =
   165       foldr add_term_consts (hyps, add_term_consts (prop, [])) \\ ignore;
   166 
   167     fun add (tab, c) =
   168       Symtab.update ((c, (next, tthm) :: Symtab.lookup_multi (tab, c)), tab);
   169   in (next + 1, foldl add (table, consts)) end;
   170 
   171 fun make_const_idx thm_tab =
   172   Symtab.foldl (fn (x, (_, ths)) => foldl add_const_idx (x, ths)) ((0, Symtab.empty), thm_tab);
   173 
   174 
   175 (* lookup index *)
   176 
   177 (*search locally*)
   178 fun containing [] thy = thms_of thy
   179   | containing consts thy =
   180       let
   181         fun int ([], _) = []
   182           | int (_, []) = []
   183           | int (xxs as ((x as (i:int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
   184               if i = j then x :: int (xs, ys)
   185               else if i > j then int (xs, yys)
   186               else int (xxs, ys);
   187 
   188         fun ints [xs] = xs
   189           | ints xss = if exists null xss then [] else foldl int (hd xss, tl xss);
   190 
   191         val ref {const_idx = (_, ctab), ...} = get_theorems thy;
   192         val ithmss = map (fn c => Symtab.lookup_multi (ctab, c)) consts;
   193       in
   194         map (attach_name o snd) (ints ithmss)
   195       end;
   196 
   197 (*search globally*)
   198 fun thms_containing thy consts =
   199   flat (map (containing (consts \\ ignore)) (thy :: Theory.ancestors_of thy));
   200 
   201 
   202 
   203 (** store theorems **)                    (*DESTRUCTIVE*)
   204 
   205 (* naming *)
   206 
   207 val defaultN = "it";
   208 val default_name = fn "" => defaultN | name => name;
   209 
   210 fun gen_names len name =
   211   map (fn i => name ^ "_" ^ string_of_int i) (1 upto len);
   212 
   213 fun name_single name x = [(default_name name, x)];
   214 fun name_multi name xs = gen_names (length xs) (default_name name) ~~ xs;
   215 
   216 
   217 (* enter_tthmx *)
   218 
   219 fun cond_warning name msg = if Sign.base_name name = defaultN then () else warning msg;
   220 
   221 fun warn_overwrite name =
   222   cond_warning name ("Replaced old copy of theorems " ^ quote name);
   223 
   224 fun warn_same name =
   225   cond_warning name ("Theorem database already contains a copy of " ^ quote name);
   226 
   227 fun enter_tthmx sg app_name (bname, tthmx) =
   228   let
   229     val name = Sign.full_name sg bname;
   230     fun name_tthm (nm, (thm, tgs)) = (Thm.name_thm (nm, thm), tgs);
   231     val named_tthms = map name_tthm (app_name name tthmx);
   232 
   233     fun eq_tthm ((th1, _), (th2, _)) = Thm.eq_thm (th1, th2);
   234 
   235     val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
   236 
   237     val overwrite =
   238       (case Symtab.lookup (thms_tab, name) of
   239         None => false
   240       | Some tthms' =>
   241           if length tthms' = length named_tthms andalso forall2 eq_tthm (tthms', named_tthms) then
   242             (warn_same name; false)
   243           else (warn_overwrite name; true));
   244 
   245     val space' = NameSpace.extend (space, [name]);
   246     val thms_tab' = Symtab.update ((name, named_tthms), thms_tab);
   247     val const_idx' =
   248       if overwrite then make_const_idx thms_tab'
   249       else foldl add_const_idx (const_idx, named_tthms);
   250   in
   251     r := {space = space', thms_tab = thms_tab', const_idx = const_idx'};
   252     named_tthms
   253   end;
   254 
   255 
   256 (* add_tthms(s) *)
   257 
   258 fun add_tthmx app_name app_att ((bname, tthmx), atts) thy =
   259   let
   260     val (thy', tthmx') = app_att ((thy, tthmx), atts);
   261     val tthms'' = enter_tthmx (Theory.sign_of thy') app_name (bname, tthmx');
   262   in (thy', tthms'') end;
   263 
   264 fun add_tthmxs name app = Library.apply o map (fst oo add_tthmx name app);
   265 
   266 val add_tthms = add_tthmxs name_single Attribute.apply;
   267 val add_tthmss = add_tthmxs name_multi Attribute.applys;
   268 
   269 
   270 (* have_tthmss *)
   271 
   272 fun have_tthmss bname more_atts ths_atts thy =
   273   let
   274     fun app (x, (ths, atts)) = Attribute.applys ((x, ths), atts);
   275     val (thy', tthmss') =
   276       foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts)) ths_atts);
   277     val tthms'' = enter_tthmx (Theory.sign_of thy') name_multi (bname, flat tthmss');
   278   in (thy, tthms'') end;
   279 
   280 
   281 (* store_tthm *)
   282 
   283 fun store_tthm th_atts thy =
   284   let val (thy', [th']) = add_tthmx name_single Attribute.apply th_atts thy
   285   in (thy', th') end;
   286 
   287 
   288 (* smart_store_thm *)
   289 
   290 fun smart_store_thm (name, thm) =
   291   let val [(thm', _)] = enter_tthmx (Thm.sign_of_thm thm) name_single (name, Attribute.tthm_of thm)
   292   in thm' end;
   293 
   294 
   295 (* store axioms as theorems *)
   296 
   297 local
   298   fun add_ax app_name add ((name, axs), atts) thy =
   299     let
   300       val named_axs = app_name name axs;
   301       val thy' = add named_axs thy;
   302       val tthms = map (Attribute.tthm_of o Thm.get_axiom thy' o fst) named_axs;
   303     in add_tthmss [((name, tthms), atts)] thy' end;
   304 
   305   fun add_axs app_name add = Library.apply o map (add_ax app_name add);
   306 in
   307   val add_axioms    = add_axs name_single Theory.add_axioms;
   308   val add_axioms_i  = add_axs name_single Theory.add_axioms_i;
   309   val add_axiomss   = add_axs name_multi Theory.add_axioms;
   310   val add_axiomss_i = add_axs name_multi Theory.add_axioms_i;
   311   val add_defs      = add_axs name_single Theory.add_defs;
   312   val add_defs_i    = add_axs name_single Theory.add_defs_i;
   313   val add_defss     = add_axs name_multi Theory.add_defs;
   314   val add_defss_i   = add_axs name_multi Theory.add_defs_i;
   315 end;
   316 
   317 
   318 
   319 (*** derived theory operations ***)
   320 
   321 (** theory management **)
   322 
   323 (* data kind 'Pure/theory_management' *)
   324 
   325 structure TheoryManagementDataArgs =
   326 struct
   327   val name = "Pure/theory_management";
   328   type T = {name: string, generation: int};
   329 
   330   val empty = {name = "", generation = 0};
   331   val prep_ext  = I;
   332   fun merge _ = empty;
   333   fun print _ _ = ();
   334 end;
   335 
   336 structure TheoryManagementData = TheoryDataFun(TheoryManagementDataArgs);
   337 val get_info = TheoryManagementData.get;
   338 val put_info = TheoryManagementData.put;
   339 
   340 
   341 (* get / put name *)
   342 
   343 val get_name = #name o get_info;
   344 fun put_name name = put_info {name = name, generation = 0};
   345 
   346 
   347 (* control prefixing of theory name *)
   348 
   349 val global_path = Theory.root_path;
   350 
   351 fun local_path thy =
   352   thy |> Theory.root_path |> Theory.add_path (get_name thy);
   353 
   354 
   355 (* begin / end theory *)
   356 
   357 fun begin_theory name thys =
   358   Theory.prep_ext_merge thys
   359   |> put_name name
   360   |> local_path;
   361 
   362 fun end_theory thy = Theory.add_name (get_name thy) thy;
   363 
   364 
   365 (* atomic transactions *)
   366 
   367 exception ROLLBACK of theory * exn option;
   368 
   369 fun transaction f thy =
   370   let
   371     val {name, generation} = get_info thy;
   372     val copy_thy =
   373       thy
   374       |> Theory.prep_ext
   375       |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation)  (* FIXME !!?? *)
   376       |> put_info {name = name, generation = generation + 1};
   377     val (thy', opt_exn) = (transform_error f thy, None) handle exn => (thy, Some exn);
   378   in
   379     if Sign.is_stale (Theory.sign_of thy') then raise ROLLBACK (copy_thy, opt_exn)
   380     else (case opt_exn of Some exn => raise exn | _ => thy')
   381   end;
   382 
   383 
   384 
   385 (** add logical types **)
   386 
   387 fun add_typedecls decls thy =
   388   let
   389     val full = Sign.full_name (Theory.sign_of thy);
   390 
   391     fun type_of (raw_name, vs, mx) =
   392       if null (duplicates vs) then (raw_name, length vs, mx)
   393       else error ("Duplicate parameters in type declaration: " ^ quote raw_name);
   394 
   395     fun arity_of (raw_name, len, mx) =
   396       (full (Syntax.type_name raw_name mx), replicate len logicS, logicS);
   397 
   398     val types = map type_of decls;
   399     val arities = map arity_of types;
   400   in
   401     thy
   402     |> Theory.add_types types
   403     |> Theory.add_arities_i arities
   404   end;
   405 
   406 
   407 
   408 (*** the ProtoPure theory ***)
   409 
   410 val proto_pure =
   411   Theory.pre_pure
   412   |> Library.apply [TheoremsData.init, TheoryManagementData.init]
   413   |> put_name "ProtoPure"
   414   |> global_path
   415   |> Theory.add_types
   416    [("fun", 2, NoSyn),
   417     ("prop", 0, NoSyn),
   418     ("itself", 1, NoSyn),
   419     ("dummy", 0, NoSyn)]
   420   |> Theory.add_classes_i [(logicC, [])]
   421   |> Theory.add_defsort_i logicS
   422   |> Theory.add_arities_i
   423    [("fun", [logicS, logicS], logicS),
   424     ("prop", [], logicS),
   425     ("itself", [logicS], logicS)]
   426   |> Theory.add_nonterminals Syntax.pure_nonterms
   427   |> Theory.add_syntax Syntax.pure_syntax
   428   |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax
   429   |> Theory.add_trfuns Syntax.pure_trfuns
   430   |> Theory.add_trfunsT Syntax.pure_trfunsT
   431   |> Theory.add_syntax
   432    [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
   433   |> Theory.add_consts
   434    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   435     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   436     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   437     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   438     ("Goal", "prop => prop", Mixfix ("GOAL _", [999], 1000)),
   439     ("TYPE", "'a itself", NoSyn)]
   440   |> Theory.add_modesyntax ("", false)
   441     [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
   442   |> local_path
   443   |> (add_defs o map Attribute.none)
   444    [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
   445     ("Goal_def", "GOAL (PROP A) == PROP A")]
   446   |> end_theory;
   447 
   448 structure ProtoPure =
   449 struct
   450   val thy = proto_pure;
   451   val flexpair_def = get_axiom thy "flexpair_def";
   452   val Goal_def = get_axiom thy "Goal_def";
   453 end;
   454 
   455 
   456 end;
   457 
   458 
   459 structure BasicPureThy: BASIC_PURE_THY = PureThy;
   460 open BasicPureThy;