wenzelm@3987
|
1 |
(* Title: Pure/pure_thy.ML
|
wenzelm@3987
|
2 |
ID: $Id$
|
wenzelm@3987
|
3 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@3987
|
4 |
|
wenzelm@16441
|
5 |
Theorem storage. The ProtoPure theory.
|
wenzelm@3987
|
6 |
*)
|
wenzelm@3987
|
7 |
|
wenzelm@4022
|
8 |
signature BASIC_PURE_THY =
|
wenzelm@4022
|
9 |
sig
|
berghofe@15456
|
10 |
type thmref
|
wenzelm@5000
|
11 |
val print_theorems: theory -> unit
|
wenzelm@5000
|
12 |
val print_theory: theory -> unit
|
berghofe@15456
|
13 |
val get_thm: theory -> thmref -> thm
|
berghofe@15456
|
14 |
val get_thms: theory -> thmref -> thm list
|
berghofe@15456
|
15 |
val get_thmss: theory -> thmref list -> thm list
|
wenzelm@5091
|
16 |
structure ProtoPure:
|
wenzelm@5091
|
17 |
sig
|
wenzelm@5091
|
18 |
val thy: theory
|
wenzelm@5091
|
19 |
val Goal_def: thm
|
wenzelm@5091
|
20 |
end
|
wenzelm@4853
|
21 |
end;
|
wenzelm@4022
|
22 |
|
wenzelm@3987
|
23 |
signature PURE_THY =
|
wenzelm@3987
|
24 |
sig
|
wenzelm@4022
|
25 |
include BASIC_PURE_THY
|
wenzelm@15703
|
26 |
datatype interval = FromTo of int * int | From of int | Single of int
|
wenzelm@16023
|
27 |
val string_of_thmref: thmref -> string
|
wenzelm@16441
|
28 |
val theorem_space: theory -> NameSpace.T
|
berghofe@15456
|
29 |
val get_thm_closure: theory -> thmref -> thm
|
berghofe@15456
|
30 |
val get_thms_closure: theory -> thmref -> thm list
|
wenzelm@9564
|
31 |
val single_thm: string -> thm list -> thm
|
berghofe@15456
|
32 |
val select_thm: thmref -> thm list -> thm list
|
wenzelm@16023
|
33 |
val selections: string * thm list -> (thmref * thm) list
|
wenzelm@16023
|
34 |
val fact_index_of: theory -> FactIndex.T
|
wenzelm@16023
|
35 |
val valid_thms: theory -> thmref * thm list -> bool
|
wenzelm@16023
|
36 |
val thms_containing: theory -> FactIndex.spec -> (string * thm list) list
|
nipkow@13646
|
37 |
val thms_containing_consts: theory -> string list -> (string * thm) list
|
wenzelm@16336
|
38 |
val thms_of: theory -> (string * thm) list
|
wenzelm@16336
|
39 |
val all_thms_of: theory -> (string * thm) list
|
wenzelm@12695
|
40 |
val hide_thms: bool -> string list -> theory -> theory
|
wenzelm@6091
|
41 |
val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
|
wenzelm@7405
|
42 |
val smart_store_thms: (bstring * thm list) -> thm list
|
wenzelm@12138
|
43 |
val smart_store_thms_open: (bstring * thm list) -> thm list
|
wenzelm@7899
|
44 |
val forall_elim_var: int -> thm -> thm
|
wenzelm@7899
|
45 |
val forall_elim_vars: int -> thm -> thm
|
wenzelm@8419
|
46 |
val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
|
wenzelm@12711
|
47 |
val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
|
wenzelm@12711
|
48 |
-> theory * thm list list
|
wenzelm@16132
|
49 |
val note_thmss: theory attribute -> ((bstring * theory attribute list) *
|
wenzelm@16441
|
50 |
(thmref * theory attribute list) list) list ->
|
wenzelm@16441
|
51 |
theory -> theory * (bstring * thm list) list
|
wenzelm@16132
|
52 |
val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
|
wenzelm@16441
|
53 |
(thm list * theory attribute list) list) list ->
|
wenzelm@16441
|
54 |
theory -> theory * (bstring * thm list) list
|
wenzelm@16441
|
55 |
val add_axioms: ((bstring * string) * theory attribute list) list ->
|
wenzelm@16441
|
56 |
theory -> theory * thm list
|
wenzelm@16441
|
57 |
val add_axioms_i: ((bstring * term) * theory attribute list) list ->
|
wenzelm@16441
|
58 |
theory -> theory * thm list
|
wenzelm@16441
|
59 |
val add_axiomss: ((bstring * string list) * theory attribute list) list ->
|
wenzelm@16441
|
60 |
theory -> theory * thm list list
|
wenzelm@16441
|
61 |
val add_axiomss_i: ((bstring * term list) * theory attribute list) list ->
|
wenzelm@16441
|
62 |
theory -> theory * thm list list
|
wenzelm@16441
|
63 |
val add_defs: bool -> ((bstring * string) * theory attribute list) list ->
|
wenzelm@16441
|
64 |
theory -> theory * thm list
|
wenzelm@16441
|
65 |
val add_defs_i: bool -> ((bstring * term) * theory attribute list) list ->
|
wenzelm@16441
|
66 |
theory -> theory * thm list
|
wenzelm@16441
|
67 |
val add_defss: bool -> ((bstring * string list) * theory attribute list) list ->
|
wenzelm@16441
|
68 |
theory -> theory * thm list list
|
wenzelm@16441
|
69 |
val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
|
wenzelm@16441
|
70 |
theory -> theory * thm list list
|
wenzelm@3987
|
71 |
end;
|
wenzelm@3987
|
72 |
|
wenzelm@3987
|
73 |
structure PureThy: PURE_THY =
|
wenzelm@3987
|
74 |
struct
|
wenzelm@3987
|
75 |
|
wenzelm@3987
|
76 |
|
wenzelm@4922
|
77 |
(*** theorem database ***)
|
wenzelm@3987
|
78 |
|
wenzelm@16441
|
79 |
(** dataype theorems **)
|
wenzelm@3987
|
80 |
|
wenzelm@16441
|
81 |
fun pretty_theorems thy theorems =
|
wenzelm@16441
|
82 |
let
|
wenzelm@16441
|
83 |
val prt_thm = Display.pretty_thm_sg thy;
|
wenzelm@16441
|
84 |
fun prt_thms (name, [th]) =
|
wenzelm@16441
|
85 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
|
wenzelm@16441
|
86 |
| prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
|
wenzelm@16441
|
87 |
val thmss = NameSpace.extern_table theorems;
|
wenzelm@16441
|
88 |
in Pretty.big_list "theorems:" (map prt_thms thmss) end;
|
wenzelm@16441
|
89 |
|
wenzelm@16441
|
90 |
structure TheoremsData = TheoryDataFun
|
wenzelm@16441
|
91 |
(struct
|
wenzelm@5005
|
92 |
val name = "Pure/theorems";
|
wenzelm@5005
|
93 |
type T =
|
wenzelm@16441
|
94 |
{theorems: thm list NameSpace.table,
|
wenzelm@16441
|
95 |
index: FactIndex.T} ref;
|
wenzelm@3987
|
96 |
|
wenzelm@4853
|
97 |
fun mk_empty _ =
|
wenzelm@16336
|
98 |
ref {theorems = NameSpace.empty_table, index = FactIndex.empty}: T;
|
wenzelm@3987
|
99 |
|
wenzelm@5005
|
100 |
val empty = mk_empty ();
|
wenzelm@6547
|
101 |
fun copy (ref x) = ref x;
|
wenzelm@16441
|
102 |
val extend = mk_empty;
|
wenzelm@16441
|
103 |
fun merge _ = mk_empty;
|
wenzelm@16441
|
104 |
fun print thy (ref {theorems, index}) = Pretty.writeln (pretty_theorems thy theorems);
|
wenzelm@16441
|
105 |
end);
|
wenzelm@5005
|
106 |
|
wenzelm@5005
|
107 |
val get_theorems = TheoremsData.get;
|
wenzelm@16441
|
108 |
val theorem_space = #1 o #theorems o ! o get_theorems;
|
wenzelm@16023
|
109 |
val fact_index_of = #index o ! o get_theorems;
|
wenzelm@16023
|
110 |
|
wenzelm@6367
|
111 |
|
wenzelm@5000
|
112 |
(* print theory *)
|
wenzelm@3987
|
113 |
|
wenzelm@5005
|
114 |
val print_theorems = TheoremsData.print;
|
wenzelm@8720
|
115 |
|
wenzelm@5000
|
116 |
fun print_theory thy =
|
wenzelm@9215
|
117 |
Display.pretty_full_theory thy @
|
wenzelm@16441
|
118 |
[pretty_theorems thy (#theorems (! (get_theorems thy)))]
|
wenzelm@8720
|
119 |
|> Pretty.chunks |> Pretty.writeln;
|
wenzelm@3987
|
120 |
|
wenzelm@3987
|
121 |
|
wenzelm@4022
|
122 |
|
wenzelm@4022
|
123 |
(** retrieve theorems **)
|
wenzelm@4022
|
124 |
|
skalberg@15531
|
125 |
fun the_thms _ (SOME thms) = thms
|
skalberg@15531
|
126 |
| the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
|
wenzelm@4922
|
127 |
|
wenzelm@9564
|
128 |
fun single_thm _ [thm] = thm
|
wenzelm@9564
|
129 |
| single_thm name _ = error ("Single theorem expected " ^ quote name);
|
wenzelm@3987
|
130 |
|
wenzelm@15703
|
131 |
|
wenzelm@16023
|
132 |
(* datatype interval *)
|
wenzelm@15703
|
133 |
|
wenzelm@15703
|
134 |
datatype interval =
|
wenzelm@15703
|
135 |
FromTo of int * int |
|
wenzelm@15703
|
136 |
From of int |
|
wenzelm@15703
|
137 |
Single of int;
|
wenzelm@15703
|
138 |
|
wenzelm@15703
|
139 |
fun interval _ (FromTo (i, j)) = i upto j
|
wenzelm@15703
|
140 |
| interval n (From i) = i upto n
|
wenzelm@15703
|
141 |
| interval _ (Single i) = [i];
|
wenzelm@15703
|
142 |
|
wenzelm@16023
|
143 |
fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
|
wenzelm@16023
|
144 |
| string_of_interval (From i) = string_of_int i ^ "-"
|
wenzelm@16023
|
145 |
| string_of_interval (Single i) = string_of_int i;
|
wenzelm@15703
|
146 |
|
wenzelm@16023
|
147 |
|
wenzelm@16023
|
148 |
(* type thmref *)
|
wenzelm@16023
|
149 |
|
wenzelm@16023
|
150 |
type thmref = xstring * interval list option;
|
wenzelm@16023
|
151 |
|
wenzelm@16023
|
152 |
fun string_of_thmref (name, NONE) = name
|
wenzelm@16023
|
153 |
| string_of_thmref (name, SOME is) =
|
wenzelm@16023
|
154 |
name ^ enclose "(" ")" (commas (map string_of_interval is));
|
wenzelm@16023
|
155 |
|
wenzelm@16023
|
156 |
|
wenzelm@16023
|
157 |
(* select_thm *)
|
wenzelm@15703
|
158 |
|
wenzelm@15703
|
159 |
fun select_thm (_, NONE) thms = thms
|
wenzelm@15703
|
160 |
| select_thm (name, SOME is) thms =
|
wenzelm@16023
|
161 |
let
|
wenzelm@16023
|
162 |
val n = length thms;
|
wenzelm@16023
|
163 |
fun select i =
|
wenzelm@16023
|
164 |
if i < 1 orelse i > n then
|
wenzelm@16023
|
165 |
error ("Bad subscript " ^ string_of_int i ^ " for " ^
|
wenzelm@16023
|
166 |
quote name ^ " (length " ^ string_of_int n ^ ")")
|
wenzelm@16023
|
167 |
else List.nth (thms, i - 1);
|
wenzelm@16023
|
168 |
in map select (List.concat (map (interval n) is)) end;
|
wenzelm@15703
|
169 |
|
wenzelm@16023
|
170 |
|
wenzelm@16023
|
171 |
(* selections *)
|
wenzelm@16023
|
172 |
|
wenzelm@16023
|
173 |
fun selections (name, [thm]) = [((name, NONE), thm)]
|
wenzelm@16023
|
174 |
| selections (name, thms) = (1 upto length thms, thms) |> ListPair.map (fn (i, thm) =>
|
wenzelm@16023
|
175 |
((name, SOME [Single i]), thm));
|
berghofe@15456
|
176 |
|
wenzelm@9564
|
177 |
|
wenzelm@9808
|
178 |
(* get_thm(s)_closure -- statically scoped versions *)
|
wenzelm@9564
|
179 |
|
wenzelm@9564
|
180 |
(*beware of proper order of evaluation!*)
|
wenzelm@9564
|
181 |
|
wenzelm@9564
|
182 |
fun lookup_thms thy =
|
wenzelm@9564
|
183 |
let
|
wenzelm@16441
|
184 |
val thy_ref = Theory.self_ref thy;
|
wenzelm@16336
|
185 |
val ref {theorems = (space, thms), ...} = get_theorems thy;
|
wenzelm@9564
|
186 |
in
|
wenzelm@9564
|
187 |
fn name =>
|
wenzelm@16441
|
188 |
Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*)
|
wenzelm@16441
|
189 |
(Symtab.lookup (thms, NameSpace.intern space name)) (*static content*)
|
wenzelm@9564
|
190 |
end;
|
wenzelm@9564
|
191 |
|
wenzelm@9564
|
192 |
fun get_thms_closure thy =
|
wenzelm@16441
|
193 |
let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) in
|
wenzelm@16441
|
194 |
fn (name, i) => select_thm (name, i) (the_thms name (get_first (fn f => f name) closures))
|
berghofe@15456
|
195 |
end;
|
wenzelm@9564
|
196 |
|
wenzelm@9808
|
197 |
fun get_thm_closure thy =
|
wenzelm@9808
|
198 |
let val get = get_thms_closure thy
|
wenzelm@16441
|
199 |
in fn (name, i) => single_thm name (get (name, i)) end;
|
wenzelm@9808
|
200 |
|
wenzelm@9564
|
201 |
|
wenzelm@16441
|
202 |
(* get_thms etc. *)
|
wenzelm@9564
|
203 |
|
wenzelm@16441
|
204 |
fun get_thms theory (name, i) =
|
wenzelm@9564
|
205 |
get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
|
wenzelm@16441
|
206 |
|> the_thms name |> select_thm (name, i) |> map (Thm.transfer theory);
|
wenzelm@3987
|
207 |
|
skalberg@15570
|
208 |
fun get_thmss thy names = List.concat (map (get_thms thy) names);
|
wenzelm@16441
|
209 |
fun get_thm thy (name, i) = single_thm name (get_thms thy (name, i));
|
wenzelm@4783
|
210 |
|
wenzelm@3987
|
211 |
|
wenzelm@16023
|
212 |
(* thms_containing etc. *)
|
wenzelm@16023
|
213 |
|
wenzelm@16023
|
214 |
fun valid_thms thy (thmref, ths) =
|
wenzelm@16023
|
215 |
(case try (transform_error (get_thms thy)) thmref of
|
wenzelm@16023
|
216 |
NONE => false
|
wenzelm@16132
|
217 |
| SOME ths' => Thm.eq_thms (ths, ths'));
|
wenzelm@16023
|
218 |
|
wenzelm@16023
|
219 |
fun thms_containing theory spec =
|
wenzelm@16023
|
220 |
(theory :: Theory.ancestors_of theory)
|
wenzelm@16023
|
221 |
|> map (fn thy =>
|
wenzelm@16023
|
222 |
FactIndex.find (fact_index_of thy) spec
|
wenzelm@16023
|
223 |
|> List.filter (fn (name, ths) => valid_thms theory ((name, NONE), ths))
|
wenzelm@16023
|
224 |
|> gen_distinct eq_fst)
|
wenzelm@16023
|
225 |
|> List.concat;
|
wenzelm@16023
|
226 |
|
wenzelm@16023
|
227 |
fun thms_containing_consts thy consts =
|
wenzelm@16023
|
228 |
thms_containing thy (consts, []) |> map #2 |> List.concat
|
wenzelm@16023
|
229 |
|> map (fn th => (Thm.name_of_thm th, th));
|
wenzelm@16023
|
230 |
|
wenzelm@16023
|
231 |
|
wenzelm@16336
|
232 |
(* thms_of etc. *)
|
wenzelm@3987
|
233 |
|
wenzelm@4022
|
234 |
fun thms_of thy =
|
wenzelm@16336
|
235 |
let val ref {theorems = (_, thms), ...} = get_theorems thy in
|
wenzelm@16336
|
236 |
map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest thms)))
|
wenzelm@4022
|
237 |
end;
|
wenzelm@4022
|
238 |
|
wenzelm@16336
|
239 |
fun all_thms_of thy = List.concat (map thms_of (thy :: Theory.ancestors_of thy));
|
wenzelm@16336
|
240 |
|
wenzelm@4022
|
241 |
|
wenzelm@4022
|
242 |
|
wenzelm@4022
|
243 |
(** store theorems **) (*DESTRUCTIVE*)
|
wenzelm@3987
|
244 |
|
wenzelm@16441
|
245 |
(* hiding -- affects current theory node only *)
|
wenzelm@12695
|
246 |
|
wenzelm@13424
|
247 |
fun hide_thms fully names thy =
|
wenzelm@12695
|
248 |
let
|
wenzelm@16336
|
249 |
val r as ref {theorems = (space, thms), index} = get_theorems thy;
|
wenzelm@16132
|
250 |
val space' = fold (NameSpace.hide fully) names space;
|
wenzelm@16336
|
251 |
in r := {theorems = (space', thms), index = index}; thy end;
|
wenzelm@12695
|
252 |
|
wenzelm@12695
|
253 |
|
wenzelm@4853
|
254 |
(* naming *)
|
wenzelm@4853
|
255 |
|
berghofe@11998
|
256 |
fun gen_names j len name =
|
wenzelm@16441
|
257 |
map (fn i => name ^ "_" ^ string_of_int i) (j + 1 upto j + len);
|
wenzelm@4853
|
258 |
|
berghofe@11998
|
259 |
fun name_multi name xs = gen_names 0 (length xs) name ~~ xs;
|
berghofe@12235
|
260 |
|
wenzelm@16441
|
261 |
fun name_thm pre (name, thm) =
|
wenzelm@16441
|
262 |
if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm (name, thm);
|
berghofe@12872
|
263 |
|
berghofe@12872
|
264 |
fun name_thms pre name [x] = [name_thm pre (name, x)]
|
berghofe@12872
|
265 |
| name_thms pre name xs = map (name_thm pre) (name_multi name xs);
|
berghofe@12235
|
266 |
|
wenzelm@16441
|
267 |
fun name_thmss name xs =
|
wenzelm@16441
|
268 |
(case filter_out (null o fst) xs of
|
berghofe@12872
|
269 |
[([x], z)] => [([name_thm true (name, x)], z)]
|
wenzelm@16441
|
270 |
| _ => snd (foldl_map (fn (i, (ys, z)) =>
|
wenzelm@16441
|
271 |
(i + length ys, (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
|
wenzelm@4853
|
272 |
|
wenzelm@4853
|
273 |
|
berghofe@11998
|
274 |
(* enter_thms *)
|
wenzelm@4853
|
275 |
|
wenzelm@7470
|
276 |
fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
|
wenzelm@7470
|
277 |
fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
|
wenzelm@5933
|
278 |
|
wenzelm@16441
|
279 |
fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms)
|
wenzelm@16441
|
280 |
| enter_thms pre_name post_name app_att (bname, thms) thy =
|
wenzelm@7470
|
281 |
let
|
wenzelm@16441
|
282 |
val name = Sign.full_name thy bname;
|
wenzelm@16441
|
283 |
val r as ref {theorems = (space, theorems), index} = get_theorems thy;
|
wenzelm@16441
|
284 |
val space' = Sign.declare_name thy name space;
|
wenzelm@16441
|
285 |
val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
|
wenzelm@16441
|
286 |
val theorems' = Symtab.update ((name, thms'), theorems);
|
wenzelm@16441
|
287 |
val index' = FactIndex.add (K false) (name, thms') index;
|
wenzelm@13274
|
288 |
in
|
wenzelm@16023
|
289 |
(case Symtab.lookup (theorems, name) of
|
skalberg@15531
|
290 |
NONE => ()
|
wenzelm@16441
|
291 |
| SOME thms'' =>
|
wenzelm@16441
|
292 |
if Thm.eq_thms (thms', thms'') then warn_same name
|
wenzelm@13274
|
293 |
else warn_overwrite name);
|
wenzelm@16336
|
294 |
r := {theorems = (space', theorems'), index = index'};
|
wenzelm@16441
|
295 |
(thy', thms')
|
berghofe@11998
|
296 |
end;
|
wenzelm@3987
|
297 |
|
wenzelm@16023
|
298 |
|
wenzelm@6091
|
299 |
(* add_thms(s) *)
|
wenzelm@3987
|
300 |
|
wenzelm@16441
|
301 |
fun add_thms_atts pre_name ((bname, thms), atts) =
|
wenzelm@16441
|
302 |
enter_thms pre_name (name_thms false)
|
wenzelm@16441
|
303 |
(Thm.applys_attributes o rpair atts) (bname, thms);
|
wenzelm@3987
|
304 |
|
berghofe@12235
|
305 |
fun gen_add_thmss pre_name args theory =
|
berghofe@12235
|
306 |
foldl_map (fn (thy, arg) => add_thms_atts pre_name arg thy) (theory, args);
|
wenzelm@5907
|
307 |
|
berghofe@12235
|
308 |
fun gen_add_thms pre_name args =
|
berghofe@12235
|
309 |
apsnd (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
|
berghofe@12235
|
310 |
|
berghofe@12872
|
311 |
val add_thmss = gen_add_thmss (name_thms true);
|
berghofe@12872
|
312 |
val add_thms = gen_add_thms (name_thms true);
|
wenzelm@5907
|
313 |
|
wenzelm@5907
|
314 |
|
wenzelm@14564
|
315 |
(* note_thmss(_i) *)
|
wenzelm@5907
|
316 |
|
wenzelm@9192
|
317 |
local
|
wenzelm@12711
|
318 |
|
wenzelm@16132
|
319 |
fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
|
wenzelm@12711
|
320 |
let
|
wenzelm@12711
|
321 |
fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
|
wenzelm@16441
|
322 |
val (thy', thms) = thy |> enter_thms
|
wenzelm@16441
|
323 |
name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
|
wenzelm@12711
|
324 |
(bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
|
wenzelm@12711
|
325 |
in (thy', (bname, thms)) end;
|
wenzelm@12711
|
326 |
|
wenzelm@16132
|
327 |
fun gen_note_thmss get kind_att args thy =
|
wenzelm@16132
|
328 |
foldl_map (gen_note_thss get kind_att) (thy, args);
|
wenzelm@12711
|
329 |
|
wenzelm@9192
|
330 |
in
|
wenzelm@12711
|
331 |
|
wenzelm@16132
|
332 |
val note_thmss = gen_note_thmss get_thms;
|
wenzelm@16132
|
333 |
val note_thmss_i = gen_note_thmss (K I);
|
wenzelm@12711
|
334 |
|
wenzelm@9192
|
335 |
end;
|
wenzelm@5280
|
336 |
|
wenzelm@5280
|
337 |
|
wenzelm@6091
|
338 |
(* store_thm *)
|
wenzelm@5280
|
339 |
|
berghofe@11998
|
340 |
fun store_thm ((bname, thm), atts) thy =
|
berghofe@12872
|
341 |
let val (thy', [th']) = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy
|
wenzelm@5280
|
342 |
in (thy', th') end;
|
wenzelm@4783
|
343 |
|
wenzelm@4853
|
344 |
|
wenzelm@16441
|
345 |
(* smart_store_thms(_open) *)
|
wenzelm@3987
|
346 |
|
wenzelm@16441
|
347 |
local
|
wenzelm@16441
|
348 |
|
wenzelm@16441
|
349 |
fun smart_store _ (name, []) =
|
berghofe@11516
|
350 |
error ("Cannot store empty list of theorems: " ^ quote name)
|
wenzelm@16441
|
351 |
| smart_store name_thm (name, [thm]) =
|
wenzelm@16441
|
352 |
#2 (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
|
wenzelm@16441
|
353 |
| smart_store name_thm (name, thms) =
|
wenzelm@7405
|
354 |
let
|
wenzelm@16441
|
355 |
fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
|
wenzelm@16441
|
356 |
val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
|
wenzelm@16441
|
357 |
in #2 (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
|
berghofe@11516
|
358 |
|
wenzelm@16441
|
359 |
in
|
wenzelm@16441
|
360 |
|
wenzelm@16441
|
361 |
val smart_store_thms = smart_store name_thms;
|
wenzelm@16441
|
362 |
val smart_store_thms_open = smart_store (K (K I));
|
wenzelm@16441
|
363 |
|
wenzelm@16441
|
364 |
end;
|
wenzelm@3987
|
365 |
|
wenzelm@3987
|
366 |
|
wenzelm@7899
|
367 |
(* forall_elim_vars (belongs to drule.ML) *)
|
wenzelm@7899
|
368 |
|
berghofe@13713
|
369 |
(*Replace outermost quantified variable by Var of given index.*)
|
wenzelm@7899
|
370 |
fun forall_elim_var i th =
|
wenzelm@16441
|
371 |
let val {prop, thy, ...} = Thm.rep_thm th
|
wenzelm@16441
|
372 |
in case prop of
|
berghofe@13713
|
373 |
Const ("all", _) $ Abs (a, T, _) =>
|
berghofe@13713
|
374 |
let val used = map (fst o fst)
|
skalberg@15570
|
375 |
(List.filter (equal i o snd o fst) (Term.add_vars ([], prop)))
|
wenzelm@16441
|
376 |
in Thm.forall_elim (Thm.cterm_of thy (Var ((variant used a, i), T))) th end
|
wenzelm@16441
|
377 |
| _ => raise THM ("forall_elim_var", i, [th])
|
wenzelm@16441
|
378 |
end;
|
wenzelm@7899
|
379 |
|
wenzelm@7899
|
380 |
(*Repeat forall_elim_var until all outer quantifiers are removed*)
|
wenzelm@7899
|
381 |
fun forall_elim_vars i th =
|
wenzelm@16441
|
382 |
forall_elim_vars i (forall_elim_var i th) handle THM _ => th;
|
wenzelm@7899
|
383 |
|
wenzelm@7899
|
384 |
|
wenzelm@4022
|
385 |
(* store axioms as theorems *)
|
wenzelm@4022
|
386 |
|
wenzelm@4853
|
387 |
local
|
wenzelm@7899
|
388 |
fun get_axs thy named_axs =
|
wenzelm@7899
|
389 |
map (forall_elim_vars 0 o Thm.get_axiom thy o fst) named_axs;
|
wenzelm@7753
|
390 |
|
wenzelm@8419
|
391 |
fun add_single add (thy, ((name, ax), atts)) =
|
wenzelm@4853
|
392 |
let
|
berghofe@11998
|
393 |
val named_ax = [(name, ax)];
|
wenzelm@7753
|
394 |
val thy' = add named_ax thy;
|
wenzelm@7753
|
395 |
val thm = hd (get_axs thy' named_ax);
|
berghofe@12235
|
396 |
in apsnd hd (gen_add_thms (K I) [((name, thm), atts)] thy') end;
|
wenzelm@7753
|
397 |
|
wenzelm@8419
|
398 |
fun add_multi add (thy, ((name, axs), atts)) =
|
wenzelm@7753
|
399 |
let
|
wenzelm@7753
|
400 |
val named_axs = name_multi name axs;
|
wenzelm@4853
|
401 |
val thy' = add named_axs thy;
|
wenzelm@7753
|
402 |
val thms = get_axs thy' named_axs;
|
berghofe@12235
|
403 |
in apsnd hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end;
|
wenzelm@4022
|
404 |
|
wenzelm@8419
|
405 |
fun add_singles add args thy = foldl_map (add_single add) (thy, args);
|
wenzelm@8419
|
406 |
fun add_multis add args thy = foldl_map (add_multi add) (thy, args);
|
wenzelm@4853
|
407 |
in
|
wenzelm@7753
|
408 |
val add_axioms = add_singles Theory.add_axioms;
|
wenzelm@7753
|
409 |
val add_axioms_i = add_singles Theory.add_axioms_i;
|
wenzelm@7753
|
410 |
val add_axiomss = add_multis Theory.add_axioms;
|
wenzelm@7753
|
411 |
val add_axiomss_i = add_multis Theory.add_axioms_i;
|
wenzelm@9318
|
412 |
val add_defs = add_singles o Theory.add_defs;
|
wenzelm@9318
|
413 |
val add_defs_i = add_singles o Theory.add_defs_i;
|
wenzelm@9318
|
414 |
val add_defss = add_multis o Theory.add_defs;
|
wenzelm@9318
|
415 |
val add_defss_i = add_multis o Theory.add_defs_i;
|
wenzelm@4853
|
416 |
end;
|
wenzelm@4022
|
417 |
|
wenzelm@4022
|
418 |
|
wenzelm@3987
|
419 |
|
wenzelm@5091
|
420 |
(*** the ProtoPure theory ***)
|
wenzelm@3987
|
421 |
|
wenzelm@16441
|
422 |
val aT = TFree ("'a", []);
|
wenzelm@16441
|
423 |
val A = Free ("A", propT);
|
wenzelm@16441
|
424 |
|
wenzelm@3987
|
425 |
val proto_pure =
|
wenzelm@16441
|
426 |
Context.pre_pure
|
wenzelm@16441
|
427 |
|> Sign.init
|
wenzelm@16441
|
428 |
|> Theory.init
|
wenzelm@16441
|
429 |
|> Proofterm.init
|
wenzelm@16023
|
430 |
|> TheoremsData.init
|
wenzelm@3987
|
431 |
|> Theory.add_types
|
wenzelm@4922
|
432 |
[("fun", 2, NoSyn),
|
wenzelm@4922
|
433 |
("prop", 0, NoSyn),
|
wenzelm@4922
|
434 |
("itself", 1, NoSyn),
|
wenzelm@4922
|
435 |
("dummy", 0, NoSyn)]
|
wenzelm@4922
|
436 |
|> Theory.add_nonterminals Syntax.pure_nonterms
|
wenzelm@3987
|
437 |
|> Theory.add_syntax Syntax.pure_syntax
|
wenzelm@15801
|
438 |
|> Theory.add_syntax Syntax.pure_appl_syntax
|
wenzelm@6692
|
439 |
|> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
|
wenzelm@3987
|
440 |
|> Theory.add_syntax
|
wenzelm@16441
|
441 |
[("==>", "prop => prop => prop", Delimfix "op ==>"),
|
wenzelm@9534
|
442 |
(Term.dummy_patternN, "aprop", Delimfix "'_")]
|
wenzelm@3987
|
443 |
|> Theory.add_consts
|
wenzelm@16441
|
444 |
[("==", "'a => 'a => prop", InfixrName ("==", 2)),
|
wenzelm@16441
|
445 |
("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
|
wenzelm@3987
|
446 |
("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
|
wenzelm@10667
|
447 |
("Goal", "prop => prop", NoSyn),
|
wenzelm@6547
|
448 |
("TYPE", "'a itself", NoSyn),
|
wenzelm@9534
|
449 |
(Term.dummy_patternN, "'a", Delimfix "'_")]
|
skalberg@14223
|
450 |
|> Theory.add_finals_i false
|
wenzelm@16441
|
451 |
[Const ("==", [aT, aT] ---> propT),
|
wenzelm@16441
|
452 |
Const ("==>", [propT, propT] ---> propT),
|
wenzelm@16441
|
453 |
Const ("all", (aT --> propT) --> propT),
|
wenzelm@16441
|
454 |
Const ("TYPE", a_itselfT)]
|
nipkow@5041
|
455 |
|> Theory.add_modesyntax ("", false)
|
wenzelm@12138
|
456 |
(Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
|
wenzelm@12250
|
457 |
|> Theory.add_trfuns Syntax.pure_trfuns
|
wenzelm@12250
|
458 |
|> Theory.add_trfunsT Syntax.pure_trfunsT
|
wenzelm@16441
|
459 |
|> Sign.local_path
|
wenzelm@10667
|
460 |
|> (#1 oo (add_defs_i false o map Thm.no_attributes))
|
wenzelm@16441
|
461 |
[("Goal_def", Logic.mk_equals (Logic.mk_goal A, A))]
|
wenzelm@9238
|
462 |
|> (#1 o add_thmss [(("nothing", []), [])])
|
berghofe@11516
|
463 |
|> Theory.add_axioms_i Proofterm.equality_axms
|
wenzelm@16441
|
464 |
|> Context.end_theory;
|
wenzelm@3987
|
465 |
|
wenzelm@3987
|
466 |
structure ProtoPure =
|
wenzelm@3987
|
467 |
struct
|
wenzelm@5091
|
468 |
val thy = proto_pure;
|
wenzelm@4788
|
469 |
val Goal_def = get_axiom thy "Goal_def";
|
wenzelm@3987
|
470 |
end;
|
wenzelm@3987
|
471 |
|
wenzelm@5091
|
472 |
end;
|
wenzelm@5091
|
473 |
|
wenzelm@5091
|
474 |
structure BasicPureThy: BASIC_PURE_THY = PureThy;
|
wenzelm@5091
|
475 |
open BasicPureThy;
|