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