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