1 (* Title: HOL/Import/proof_kernel.ML |
|
2 Author: Sebastian Skalberg and Steven Obua, TU Muenchen |
|
3 *) |
|
4 |
|
5 signature ProofKernel = |
|
6 sig |
|
7 type hol_type |
|
8 type tag |
|
9 type term |
|
10 type thm |
|
11 type ('a,'b) subst |
|
12 |
|
13 type proof_info |
|
14 datatype proof = Proof of proof_info * proof_content |
|
15 and proof_content |
|
16 = PRefl of term |
|
17 | PInstT of proof * (hol_type,hol_type) subst |
|
18 | PSubst of proof list * term * proof |
|
19 | PAbs of proof * term |
|
20 | PDisch of proof * term |
|
21 | PMp of proof * proof |
|
22 | PHyp of term |
|
23 | PAxm of string * term |
|
24 | PDef of string * string * term |
|
25 | PTmSpec of string * string list * proof |
|
26 | PTyDef of string * string * proof |
|
27 | PTyIntro of string * string * string * string * term * term * proof |
|
28 | POracle of tag * term list * term |
|
29 | PDisk |
|
30 | PSpec of proof * term |
|
31 | PInst of proof * (term,term) subst |
|
32 | PGen of proof * term |
|
33 | PGenAbs of proof * term option * term list |
|
34 | PImpAS of proof * proof |
|
35 | PSym of proof |
|
36 | PTrans of proof * proof |
|
37 | PComb of proof * proof |
|
38 | PEqMp of proof * proof |
|
39 | PEqImp of proof |
|
40 | PExists of proof * term * term |
|
41 | PChoose of term * proof * proof |
|
42 | PConj of proof * proof |
|
43 | PConjunct1 of proof |
|
44 | PConjunct2 of proof |
|
45 | PDisj1 of proof * term |
|
46 | PDisj2 of proof * term |
|
47 | PDisjCases of proof * proof * proof |
|
48 | PNotI of proof |
|
49 | PNotE of proof |
|
50 | PContr of proof * term |
|
51 |
|
52 exception PK of string * string |
|
53 |
|
54 val get_proof_dir: string -> theory -> string option |
|
55 val disambiguate_frees : Thm.thm -> Thm.thm |
|
56 val debug : bool Unsynchronized.ref |
|
57 val disk_info_of : proof -> (string * string) option |
|
58 val set_disk_info_of : proof -> string -> string -> unit |
|
59 val mk_proof : proof_content -> proof |
|
60 val content_of : proof -> proof_content |
|
61 val import_proof : string -> string -> theory -> (theory -> term) option * (theory -> proof) |
|
62 |
|
63 val rewrite_importer_term: Term.term -> theory -> Thm.thm |
|
64 |
|
65 val type_of : term -> hol_type |
|
66 |
|
67 val get_thm : string -> string -> theory -> (theory * thm option) |
|
68 val get_def : string -> string -> term -> theory -> (theory * thm option) |
|
69 val get_axiom: string -> string -> theory -> (theory * thm option) |
|
70 |
|
71 val store_thm : string -> string -> thm -> theory -> theory * thm |
|
72 |
|
73 val to_isa_thm : thm -> (term * term) list * Thm.thm |
|
74 val to_isa_term: term -> Term.term |
|
75 val to_hol_thm : Thm.thm -> thm |
|
76 |
|
77 val REFL : term -> theory -> theory * thm |
|
78 val ASSUME : term -> theory -> theory * thm |
|
79 val INST_TYPE : (hol_type,hol_type) subst -> thm -> theory -> theory * thm |
|
80 val INST : (term,term)subst -> thm -> theory -> theory * thm |
|
81 val EQ_MP : thm -> thm -> theory -> theory * thm |
|
82 val EQ_IMP_RULE : thm -> theory -> theory * thm |
|
83 val SUBST : thm list -> term -> thm -> theory -> theory * thm |
|
84 val DISJ_CASES : thm -> thm -> thm -> theory -> theory * thm |
|
85 val DISJ1: thm -> term -> theory -> theory * thm |
|
86 val DISJ2: term -> thm -> theory -> theory * thm |
|
87 val IMP_ANTISYM: thm -> thm -> theory -> theory * thm |
|
88 val SYM : thm -> theory -> theory * thm |
|
89 val MP : thm -> thm -> theory -> theory * thm |
|
90 val GEN : term -> thm -> theory -> theory * thm |
|
91 val CHOOSE : term -> thm -> thm -> theory -> theory * thm |
|
92 val EXISTS : term -> term -> thm -> theory -> theory * thm |
|
93 val ABS : term -> thm -> theory -> theory * thm |
|
94 val GEN_ABS : term option -> term list -> thm -> theory -> theory * thm |
|
95 val TRANS : thm -> thm -> theory -> theory * thm |
|
96 val CCONTR : term -> thm -> theory -> theory * thm |
|
97 val CONJ : thm -> thm -> theory -> theory * thm |
|
98 val CONJUNCT1: thm -> theory -> theory * thm |
|
99 val CONJUNCT2: thm -> theory -> theory * thm |
|
100 val NOT_INTRO: thm -> theory -> theory * thm |
|
101 val NOT_ELIM : thm -> theory -> theory * thm |
|
102 val SPEC : term -> thm -> theory -> theory * thm |
|
103 val COMB : thm -> thm -> theory -> theory * thm |
|
104 val DISCH: term -> thm -> theory -> theory * thm |
|
105 |
|
106 val type_introduction: string -> string -> string -> string -> string -> term * term -> thm -> theory -> theory * thm |
|
107 |
|
108 val new_definition : string -> string -> term -> theory -> theory * thm |
|
109 val new_specification : string -> string -> string list -> thm -> theory -> theory * thm |
|
110 val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm |
|
111 val new_axiom : string -> term -> theory -> theory * thm |
|
112 |
|
113 val prin : term -> unit |
|
114 val protect_factname : string -> string |
|
115 val replay_protect_varname : string -> string -> unit |
|
116 val replay_add_dump : string -> theory -> theory |
|
117 end |
|
118 |
|
119 structure ProofKernel : ProofKernel = |
|
120 struct |
|
121 type hol_type = Term.typ |
|
122 type term = Term.term |
|
123 datatype tag = Tag of string list |
|
124 type ('a,'b) subst = ('a * 'b) list |
|
125 datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm |
|
126 |
|
127 fun hthm2thm (HOLThm (_, th)) = th |
|
128 |
|
129 fun to_hol_thm th = HOLThm ([], th) |
|
130 |
|
131 val replay_add_dump = add_dump |
|
132 fun add_dump s thy = replay_add_dump s thy |
|
133 |
|
134 datatype proof_info |
|
135 = Info of {disk_info: (string * string) option Unsynchronized.ref} |
|
136 |
|
137 datatype proof = Proof of proof_info * proof_content |
|
138 and proof_content |
|
139 = PRefl of term |
|
140 | PInstT of proof * (hol_type,hol_type) subst |
|
141 | PSubst of proof list * term * proof |
|
142 | PAbs of proof * term |
|
143 | PDisch of proof * term |
|
144 | PMp of proof * proof |
|
145 | PHyp of term |
|
146 | PAxm of string * term |
|
147 | PDef of string * string * term |
|
148 | PTmSpec of string * string list * proof |
|
149 | PTyDef of string * string * proof |
|
150 | PTyIntro of string * string * string * string * term * term * proof |
|
151 | POracle of tag * term list * term |
|
152 | PDisk |
|
153 | PSpec of proof * term |
|
154 | PInst of proof * (term,term) subst |
|
155 | PGen of proof * term |
|
156 | PGenAbs of proof * term option * term list |
|
157 | PImpAS of proof * proof |
|
158 | PSym of proof |
|
159 | PTrans of proof * proof |
|
160 | PComb of proof * proof |
|
161 | PEqMp of proof * proof |
|
162 | PEqImp of proof |
|
163 | PExists of proof * term * term |
|
164 | PChoose of term * proof * proof |
|
165 | PConj of proof * proof |
|
166 | PConjunct1 of proof |
|
167 | PConjunct2 of proof |
|
168 | PDisj1 of proof * term |
|
169 | PDisj2 of proof * term |
|
170 | PDisjCases of proof * proof * proof |
|
171 | PNotI of proof |
|
172 | PNotE of proof |
|
173 | PContr of proof * term |
|
174 |
|
175 exception PK of string * string |
|
176 fun ERR f mesg = PK (f,mesg) |
|
177 |
|
178 |
|
179 (* Compatibility. *) |
|
180 |
|
181 val string_of_mixfix = Pretty.string_of o Mixfix.pretty_mixfix; |
|
182 |
|
183 fun mk_syn thy c = |
|
184 if Lexicon.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn |
|
185 else Delimfix (Syntax_Ext.escape c) |
|
186 |
|
187 fun quotename c = |
|
188 if Lexicon.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c |
|
189 |
|
190 exception SMART_STRING |
|
191 |
|
192 fun no_vars context tm = |
|
193 let |
|
194 val ctxt = Variable.set_body false context; |
|
195 val ([tm'], _) = Variable.import_terms true [tm] ctxt; |
|
196 in tm' end |
|
197 |
|
198 fun smart_string_of_cterm ctxt0 ct = |
|
199 let |
|
200 val ctxt = ctxt0 |
|
201 |> Config.put show_brackets false |
|
202 |> Config.put show_all_types false |
|
203 |> Config.put show_types false |
|
204 |> Config.put show_sorts false; |
|
205 val {t,T,...} = rep_cterm ct |
|
206 (* Hack to avoid parse errors with Trueprop *) |
|
207 val t' = HOLogic.dest_Trueprop t |
|
208 handle TERM _ => t |
|
209 val tn = no_vars ctxt t' |
|
210 fun match u = |
|
211 let val _ = Thm.match (ct, cterm_of (Proof_Context.theory_of ctxt) u) in true end |
|
212 handle Pattern.MATCH => false |
|
213 fun G 0 f ctxt x = f ctxt x |
|
214 | G 1 f ctxt x = f (Config.put show_types true ctxt) x |
|
215 | G 2 f ctxt x = G 1 f (Config.put show_sorts true ctxt) x |
|
216 | G 3 f ctxt x = G 2 f (Config.put show_all_types true ctxt) x |
|
217 | G 4 f ctxt x = G 3 f (Config.put show_brackets true ctxt) x |
|
218 | G _ _ _ _ = raise SMART_STRING |
|
219 fun F n = |
|
220 let |
|
221 val str = G n Syntax.string_of_term ctxt tn |
|
222 val _ = warning (@{make_string} (n, str)) |
|
223 val u = Syntax.parse_term ctxt str |
|
224 val u = if t = t' then u else HOLogic.mk_Trueprop u |
|
225 val u = Syntax.check_term ctxt (Type.constraint T u) |
|
226 in |
|
227 if match u |
|
228 then quote str |
|
229 else F (n+1) |
|
230 end |
|
231 handle ERROR _ => F (n + 1) |
|
232 | SMART_STRING => |
|
233 let val _ = |
|
234 warning ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct)) |
|
235 in quote (G 2 Syntax.string_of_term ctxt tn) end |
|
236 in |
|
237 Print_Mode.setmp [] F 0 |
|
238 end |
|
239 |
|
240 fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of |
|
241 |
|
242 fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th); |
|
243 val topctxt = ML_Context.the_local_context (); |
|
244 fun prin t = writeln (Print_Mode.setmp [] |
|
245 (fn () => Syntax.string_of_term topctxt t) ()); |
|
246 fun pth (HOLThm(_,thm)) = |
|
247 let |
|
248 (*val _ = writeln "Renaming:" |
|
249 val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*) |
|
250 val _ = prth thm |
|
251 in |
|
252 () |
|
253 end |
|
254 |
|
255 fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info |
|
256 fun mk_proof p = Proof(Info{disk_info = Unsynchronized.ref NONE},p) |
|
257 fun content_of (Proof(_,p)) = p |
|
258 |
|
259 fun set_disk_info_of (Proof(Info{disk_info,...},_)) thyname thmname = |
|
260 disk_info := SOME(thyname,thmname) |
|
261 |
|
262 structure Lib = |
|
263 struct |
|
264 |
|
265 fun assoc x = |
|
266 let |
|
267 fun F [] = raise PK("Lib.assoc","Not found") |
|
268 | F ((x',y)::rest) = if x = x' |
|
269 then y |
|
270 else F rest |
|
271 in |
|
272 F |
|
273 end |
|
274 infix mem; |
|
275 fun i mem L = |
|
276 let fun itr [] = false |
|
277 | itr (a::rst) = i=a orelse itr rst |
|
278 in itr L end; |
|
279 |
|
280 infix union; |
|
281 fun [] union S = S |
|
282 | S union [] = S |
|
283 | (a::rst) union S2 = rst union (insert (op =) a S2); |
|
284 |
|
285 fun implode_subst [] = [] |
|
286 | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest)) |
|
287 | implode_subst _ = raise ERR "implode_subst" "malformed substitution list" |
|
288 |
|
289 end |
|
290 open Lib |
|
291 |
|
292 structure Tag = |
|
293 struct |
|
294 val empty_tag = Tag [] |
|
295 fun read name = Tag [name] |
|
296 fun merge (Tag tag1) (Tag tag2) = Tag (Lib.union(tag1,tag2)) |
|
297 end |
|
298 |
|
299 (* Actual code. *) |
|
300 |
|
301 fun get_segment thyname l = (Lib.assoc "s" l |
|
302 handle PK _ => thyname) |
|
303 val get_name : (string * string) list -> string = Lib.assoc "n" |
|
304 |
|
305 exception XML of string |
|
306 |
|
307 datatype xml = Elem of string * (string * string) list * xml list |
|
308 datatype XMLtype = XMLty of xml | FullType of hol_type |
|
309 datatype XMLterm = XMLtm of xml | FullTerm of term |
|
310 |
|
311 fun xml_to_import_xml (XML.Elem ((n, l), ts)) = Elem (n, l, map xml_to_import_xml ts) |
|
312 | xml_to_import_xml (XML.Text _) = raise XML "Incorrect proof file: text"; |
|
313 |
|
314 val type_of = Term.type_of |
|
315 |
|
316 val propT = Type("prop",[]) |
|
317 |
|
318 fun mk_defeq name rhs thy = |
|
319 let |
|
320 val ty = type_of rhs |
|
321 in |
|
322 Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs) |
|
323 end |
|
324 |
|
325 fun mk_teq name rhs thy = |
|
326 let |
|
327 val ty = type_of rhs |
|
328 in |
|
329 HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs) |
|
330 end |
|
331 |
|
332 fun intern_const_name thyname const thy = |
|
333 case get_importer_const_mapping thyname const thy of |
|
334 SOME (_,cname,_) => cname |
|
335 | NONE => (case get_importer_const_renaming thyname const thy of |
|
336 SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname) |
|
337 | NONE => Sign.intern_const thy (thyname ^ "." ^ const)) |
|
338 |
|
339 fun intern_type_name thyname const thy = |
|
340 case get_importer_type_mapping thyname const thy of |
|
341 SOME (_,cname) => cname |
|
342 | NONE => Sign.intern_const thy (thyname ^ "." ^ const) |
|
343 |
|
344 fun mk_vartype name = TFree(name,["HOL.type"]) |
|
345 fun mk_thy_type thy Thy Tyop Args = Type(intern_type_name Thy Tyop thy,Args) |
|
346 |
|
347 val mk_var = Free |
|
348 |
|
349 fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty) |
|
350 |
|
351 local |
|
352 fun get_const sg _ name = |
|
353 (case Sign.const_type sg name of |
|
354 SOME ty => Const (name, ty) |
|
355 | NONE => raise ERR "get_type" (name ^ ": No such constant")) |
|
356 in |
|
357 fun prim_mk_const thy Thy Nam = |
|
358 let |
|
359 val name = intern_const_name Thy Nam thy |
|
360 val cmaps = Importer_ConstMaps.get thy |
|
361 in |
|
362 case StringPair.lookup cmaps (Thy,Nam) of |
|
363 SOME(_,_,SOME ty) => Const(name,ty) |
|
364 | _ => get_const thy Thy name |
|
365 end |
|
366 end |
|
367 |
|
368 fun mk_comb(f,a) = f $ a |
|
369 |
|
370 (* Needed for HOL Light *) |
|
371 fun protect_tyvarname s = |
|
372 let |
|
373 fun no_quest s = |
|
374 if Char.contains s #"?" |
|
375 then String.translate (fn #"?" => "q_" | c => Char.toString c) s |
|
376 else s |
|
377 fun beg_prime s = |
|
378 if String.isPrefix "'" s |
|
379 then s |
|
380 else "'" ^ s |
|
381 in |
|
382 s |> no_quest |> beg_prime |
|
383 end |
|
384 |
|
385 val protected_varnames = Unsynchronized.ref (Symtab.empty:string Symtab.table) |
|
386 val invented_isavar = Unsynchronized.ref 0 |
|
387 |
|
388 fun innocent_varname s = Lexicon.is_identifier s andalso not (String.isPrefix "u_" s) |
|
389 |
|
390 fun valid_boundvarname s = |
|
391 can (fn () => Syntax.read_term_global @{theory Main} ("SOME "^s^". True")) (); |
|
392 |
|
393 fun valid_varname s = |
|
394 can (fn () => Syntax.read_term_global @{theory Main} s) (); |
|
395 |
|
396 fun protect_varname s = |
|
397 if innocent_varname s andalso valid_varname s then s else |
|
398 case Symtab.lookup (!protected_varnames) s of |
|
399 SOME t => t |
|
400 | NONE => |
|
401 let |
|
402 val _ = Unsynchronized.inc invented_isavar |
|
403 val t = "u_" ^ string_of_int (!invented_isavar) |
|
404 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) |
|
405 in |
|
406 t |
|
407 end |
|
408 |
|
409 exception REPLAY_PROTECT_VARNAME of string*string*string |
|
410 |
|
411 fun replay_protect_varname s t = |
|
412 case Symtab.lookup (!protected_varnames) s of |
|
413 SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t') |
|
414 | NONE => |
|
415 let |
|
416 val _ = Unsynchronized.inc invented_isavar |
|
417 val t = "u_" ^ string_of_int (!invented_isavar) |
|
418 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) |
|
419 in |
|
420 () |
|
421 end |
|
422 |
|
423 fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u" |
|
424 |
|
425 fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) |
|
426 | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) |
|
427 | mk_lambda v t = raise TERM ("lambda", [v, t]); |
|
428 |
|
429 fun replacestr x y s = |
|
430 let |
|
431 val xl = raw_explode x |
|
432 val yl = raw_explode y |
|
433 fun isprefix [] _ = true |
|
434 | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false |
|
435 | isprefix _ _ = false |
|
436 fun isp s = isprefix xl s |
|
437 fun chg s = yl@(List.drop (s, List.length xl)) |
|
438 fun r [] = [] |
|
439 | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) |
|
440 in |
|
441 implode(r (raw_explode s)) |
|
442 end |
|
443 |
|
444 fun protect_factname s = replacestr "." "_dot_" s |
|
445 fun unprotect_factname s = replacestr "_dot_" "." s |
|
446 |
|
447 val ty_num_prefix = "N_" |
|
448 |
|
449 fun startsWithDigit s = Char.isDigit (hd (String.explode s)) |
|
450 |
|
451 fun protect_tyname tyn = |
|
452 let |
|
453 val tyn' = |
|
454 if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else |
|
455 (if startsWithDigit tyn then ty_num_prefix^tyn else tyn) |
|
456 in |
|
457 tyn' |
|
458 end |
|
459 |
|
460 fun protect_constname tcn = tcn |
|
461 (* if tcn = ".." then "dotdot" |
|
462 else if tcn = "==" then "eqeq" |
|
463 else tcn*) |
|
464 |
|
465 structure TypeNet = |
|
466 struct |
|
467 |
|
468 fun get_type_from_index thy thyname types is = |
|
469 case Int.fromString is of |
|
470 SOME i => (case Array.sub(types,i) of |
|
471 FullType ty => ty |
|
472 | XMLty xty => |
|
473 let |
|
474 val ty = get_type_from_xml thy thyname types xty |
|
475 val _ = Array.update(types,i,FullType ty) |
|
476 in |
|
477 ty |
|
478 end) |
|
479 | NONE => raise ERR "get_type_from_index" "Bad index" |
|
480 and get_type_from_xml thy thyname types = |
|
481 let |
|
482 fun gtfx (Elem("tyi",[("i",iS)],[])) = |
|
483 get_type_from_index thy thyname types iS |
|
484 | gtfx (Elem("tyc",atts,[])) = |
|
485 mk_thy_type thy |
|
486 (get_segment thyname atts) |
|
487 (protect_tyname (get_name atts)) |
|
488 [] |
|
489 | gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s) |
|
490 | gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) = |
|
491 mk_thy_type thy |
|
492 (get_segment thyname atts) |
|
493 (protect_tyname (get_name atts)) |
|
494 (map gtfx tys) |
|
495 | gtfx _ = raise ERR "get_type" "Bad type" |
|
496 in |
|
497 gtfx |
|
498 end |
|
499 |
|
500 fun input_types _ (Elem("tylist",[("i",i)],xtys)) = |
|
501 let |
|
502 val types = Array.array(the (Int.fromString i),XMLty (Elem("",[],[]))) |
|
503 fun IT _ [] = () |
|
504 | IT n (xty::xtys) = |
|
505 (Array.update(types,n,XMLty xty); |
|
506 IT (n+1) xtys) |
|
507 val _ = IT 0 xtys |
|
508 in |
|
509 types |
|
510 end |
|
511 | input_types _ _ = raise ERR "input_types" "Bad type list" |
|
512 end |
|
513 |
|
514 structure TermNet = |
|
515 struct |
|
516 |
|
517 fun get_term_from_index thy thyname types terms is = |
|
518 case Int.fromString is of |
|
519 SOME i => (case Array.sub(terms,i) of |
|
520 FullTerm tm => tm |
|
521 | XMLtm xtm => |
|
522 let |
|
523 val tm = get_term_from_xml thy thyname types terms xtm |
|
524 val _ = Array.update(terms,i,FullTerm tm) |
|
525 in |
|
526 tm |
|
527 end) |
|
528 | NONE => raise ERR "get_term_from_index" "Bad index" |
|
529 and get_term_from_xml thy thyname types terms = |
|
530 let |
|
531 fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) = |
|
532 mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi) |
|
533 | gtfx (Elem("tmc",atts,[])) = |
|
534 let |
|
535 val segment = get_segment thyname atts |
|
536 val name = protect_constname(get_name atts) |
|
537 in |
|
538 mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts)) |
|
539 handle PK _ => prim_mk_const thy segment name |
|
540 end |
|
541 | gtfx (Elem("tma",[("f",tmf),("a",tma)],[])) = |
|
542 let |
|
543 val f = get_term_from_index thy thyname types terms tmf |
|
544 val a = get_term_from_index thy thyname types terms tma |
|
545 in |
|
546 mk_comb(f,a) |
|
547 end |
|
548 | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = |
|
549 let |
|
550 val x = get_term_from_index thy thyname types terms tmx |
|
551 val a = get_term_from_index thy thyname types terms tma |
|
552 in |
|
553 mk_lambda x a |
|
554 end |
|
555 | gtfx (Elem("tmi",[("i",iS)],[])) = |
|
556 get_term_from_index thy thyname types terms iS |
|
557 | gtfx (Elem(tag,_,_)) = |
|
558 raise ERR "get_term" ("Not a term: "^tag) |
|
559 in |
|
560 gtfx |
|
561 end |
|
562 |
|
563 fun input_terms _ _ (Elem("tmlist",[("i",i)],xtms)) = |
|
564 let |
|
565 val terms = Array.array(the (Int.fromString i), XMLtm (Elem("",[],[]))) |
|
566 |
|
567 fun IT _ [] = () |
|
568 | IT n (xtm::xtms) = |
|
569 (Array.update(terms,n,XMLtm xtm); |
|
570 IT (n+1) xtms) |
|
571 val _ = IT 0 xtms |
|
572 in |
|
573 terms |
|
574 end |
|
575 | input_terms _ _ _ = raise ERR "input_terms" "Bad term list" |
|
576 end |
|
577 |
|
578 fun get_proof_dir (thyname:string) thy = |
|
579 let |
|
580 val import_segment = |
|
581 case get_segment2 thyname thy of |
|
582 SOME seg => seg |
|
583 | NONE => get_import_segment thy |
|
584 val path = space_explode ":" (getenv "IMPORTER_PROOFS") |
|
585 fun find [] = NONE |
|
586 | find (p::ps) = |
|
587 (let |
|
588 val dir = OS.Path.joinDirFile {dir = p,file=import_segment} |
|
589 in |
|
590 if OS.FileSys.isDir dir |
|
591 then SOME dir |
|
592 else find ps |
|
593 end) handle OS.SysErr _ => find ps |
|
594 in |
|
595 Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path) |
|
596 end |
|
597 |
|
598 fun proof_file_name thyname thmname thy = |
|
599 let |
|
600 val path = case get_proof_dir thyname thy of |
|
601 SOME p => p |
|
602 | NONE => error "Cannot find proof files" |
|
603 val _ = OS.FileSys.mkDir path handle OS.SysErr _ => () |
|
604 in |
|
605 OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}} |
|
606 end |
|
607 |
|
608 fun xml_to_proof thyname types terms prf thy = |
|
609 let |
|
610 val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types |
|
611 val xml_to_term = TermNet.get_term_from_xml thy thyname types terms |
|
612 |
|
613 fun index_to_term is = |
|
614 TermNet.get_term_from_index thy thyname types terms is |
|
615 |
|
616 fun x2p (Elem("prefl",[("i",is)],[])) = mk_proof (PRefl (index_to_term is)) |
|
617 | x2p (Elem("pinstt",[],p::lambda)) = |
|
618 let |
|
619 val p = x2p p |
|
620 val lambda = implode_subst (map xml_to_hol_type lambda) |
|
621 in |
|
622 mk_proof (PInstT(p,lambda)) |
|
623 end |
|
624 | x2p (Elem("psubst",[("i",is)],prf::prfs)) = |
|
625 let |
|
626 val tm = index_to_term is |
|
627 val prf = x2p prf |
|
628 val prfs = map x2p prfs |
|
629 in |
|
630 mk_proof (PSubst(prfs,tm,prf)) |
|
631 end |
|
632 | x2p (Elem("pabs",[("i",is)],[prf])) = |
|
633 let |
|
634 val p = x2p prf |
|
635 val t = index_to_term is |
|
636 in |
|
637 mk_proof (PAbs (p,t)) |
|
638 end |
|
639 | x2p (Elem("pdisch",[("i",is)],[prf])) = |
|
640 let |
|
641 val p = x2p prf |
|
642 val t = index_to_term is |
|
643 in |
|
644 mk_proof (PDisch (p,t)) |
|
645 end |
|
646 | x2p (Elem("pmp",[],[prf1,prf2])) = |
|
647 let |
|
648 val p1 = x2p prf1 |
|
649 val p2 = x2p prf2 |
|
650 in |
|
651 mk_proof (PMp(p1,p2)) |
|
652 end |
|
653 | x2p (Elem("phyp",[("i",is)],[])) = mk_proof (PHyp (index_to_term is)) |
|
654 | x2p (Elem("paxiom",[("n",n),("i",is)],[])) = |
|
655 mk_proof (PAxm(n,index_to_term is)) |
|
656 | x2p (Elem("pfact",atts,[])) = |
|
657 let |
|
658 val thyname = get_segment thyname atts |
|
659 val thmname = protect_factname (get_name atts) |
|
660 val p = mk_proof PDisk |
|
661 val _ = set_disk_info_of p thyname thmname |
|
662 in |
|
663 p |
|
664 end |
|
665 | x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) = |
|
666 mk_proof (PDef(seg,protect_constname name,index_to_term is)) |
|
667 | x2p (Elem("ptmspec",[("s",seg)],p::names)) = |
|
668 let |
|
669 val names = map (fn Elem("name",[("n",name)],[]) => name |
|
670 | _ => raise ERR "x2p" "Bad proof (ptmspec)") names |
|
671 in |
|
672 mk_proof (PTmSpec(seg,names,x2p p)) |
|
673 end |
|
674 | x2p (Elem("ptyintro",[("s",seg),("n",name),("a",abs_name),("r",rep_name)],[xP,xt,p])) = |
|
675 let |
|
676 val P = xml_to_term xP |
|
677 val t = xml_to_term xt |
|
678 in |
|
679 mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p)) |
|
680 end |
|
681 | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) = |
|
682 mk_proof (PTyDef(seg,protect_tyname name,x2p p)) |
|
683 | x2p (Elem("poracle",[],chldr)) = |
|
684 let |
|
685 val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr |
|
686 val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | _ => raise ERR "x2p" "bad oracle") oracles |
|
687 val (c,asl) = case terms of |
|
688 [] => raise ERR "x2p" "Bad oracle description" |
|
689 | (hd::tl) => (hd,tl) |
|
690 val tg = fold_rev (Tag.merge o Tag.read) ors Tag.empty_tag |
|
691 in |
|
692 mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c)) |
|
693 end |
|
694 | x2p (Elem("pspec",[("i",is)],[prf])) = |
|
695 let |
|
696 val p = x2p prf |
|
697 val tm = index_to_term is |
|
698 in |
|
699 mk_proof (PSpec(p,tm)) |
|
700 end |
|
701 | x2p (Elem("pinst",[],p::theta)) = |
|
702 let |
|
703 val p = x2p p |
|
704 val theta = implode_subst (map xml_to_term theta) |
|
705 in |
|
706 mk_proof (PInst(p,theta)) |
|
707 end |
|
708 | x2p (Elem("pgen",[("i",is)],[prf])) = |
|
709 let |
|
710 val p = x2p prf |
|
711 val tm = index_to_term is |
|
712 in |
|
713 mk_proof (PGen(p,tm)) |
|
714 end |
|
715 | x2p (Elem("pgenabs",[],prf::tms)) = |
|
716 let |
|
717 val p = x2p prf |
|
718 val tml = map xml_to_term tms |
|
719 in |
|
720 mk_proof (PGenAbs(p,NONE,tml)) |
|
721 end |
|
722 | x2p (Elem("pgenabs",[("i",is)],prf::tms)) = |
|
723 let |
|
724 val p = x2p prf |
|
725 val tml = map xml_to_term tms |
|
726 in |
|
727 mk_proof (PGenAbs(p,SOME (index_to_term is),tml)) |
|
728 end |
|
729 | x2p (Elem("pimpas",[],[prf1,prf2])) = |
|
730 let |
|
731 val p1 = x2p prf1 |
|
732 val p2 = x2p prf2 |
|
733 in |
|
734 mk_proof (PImpAS(p1,p2)) |
|
735 end |
|
736 | x2p (Elem("psym",[],[prf])) = |
|
737 let |
|
738 val p = x2p prf |
|
739 in |
|
740 mk_proof (PSym p) |
|
741 end |
|
742 | x2p (Elem("ptrans",[],[prf1,prf2])) = |
|
743 let |
|
744 val p1 = x2p prf1 |
|
745 val p2 = x2p prf2 |
|
746 in |
|
747 mk_proof (PTrans(p1,p2)) |
|
748 end |
|
749 | x2p (Elem("pcomb",[],[prf1,prf2])) = |
|
750 let |
|
751 val p1 = x2p prf1 |
|
752 val p2 = x2p prf2 |
|
753 in |
|
754 mk_proof (PComb(p1,p2)) |
|
755 end |
|
756 | x2p (Elem("peqmp",[],[prf1,prf2])) = |
|
757 let |
|
758 val p1 = x2p prf1 |
|
759 val p2 = x2p prf2 |
|
760 in |
|
761 mk_proof (PEqMp(p1,p2)) |
|
762 end |
|
763 | x2p (Elem("peqimp",[],[prf])) = |
|
764 let |
|
765 val p = x2p prf |
|
766 in |
|
767 mk_proof (PEqImp p) |
|
768 end |
|
769 | x2p (Elem("pexists",[("e",ise),("w",isw)],[prf])) = |
|
770 let |
|
771 val p = x2p prf |
|
772 val ex = index_to_term ise |
|
773 val w = index_to_term isw |
|
774 in |
|
775 mk_proof (PExists(p,ex,w)) |
|
776 end |
|
777 | x2p (Elem("pchoose",[("i",is)],[prf1,prf2])) = |
|
778 let |
|
779 val v = index_to_term is |
|
780 val p1 = x2p prf1 |
|
781 val p2 = x2p prf2 |
|
782 in |
|
783 mk_proof (PChoose(v,p1,p2)) |
|
784 end |
|
785 | x2p (Elem("pconj",[],[prf1,prf2])) = |
|
786 let |
|
787 val p1 = x2p prf1 |
|
788 val p2 = x2p prf2 |
|
789 in |
|
790 mk_proof (PConj(p1,p2)) |
|
791 end |
|
792 | x2p (Elem("pconjunct1",[],[prf])) = |
|
793 let |
|
794 val p = x2p prf |
|
795 in |
|
796 mk_proof (PConjunct1 p) |
|
797 end |
|
798 | x2p (Elem("pconjunct2",[],[prf])) = |
|
799 let |
|
800 val p = x2p prf |
|
801 in |
|
802 mk_proof (PConjunct2 p) |
|
803 end |
|
804 | x2p (Elem("pdisj1",[("i",is)],[prf])) = |
|
805 let |
|
806 val p = x2p prf |
|
807 val t = index_to_term is |
|
808 in |
|
809 mk_proof (PDisj1 (p,t)) |
|
810 end |
|
811 | x2p (Elem("pdisj2",[("i",is)],[prf])) = |
|
812 let |
|
813 val p = x2p prf |
|
814 val t = index_to_term is |
|
815 in |
|
816 mk_proof (PDisj2 (p,t)) |
|
817 end |
|
818 | x2p (Elem("pdisjcases",[],[prf1,prf2,prf3])) = |
|
819 let |
|
820 val p1 = x2p prf1 |
|
821 val p2 = x2p prf2 |
|
822 val p3 = x2p prf3 |
|
823 in |
|
824 mk_proof (PDisjCases(p1,p2,p3)) |
|
825 end |
|
826 | x2p (Elem("pnoti",[],[prf])) = |
|
827 let |
|
828 val p = x2p prf |
|
829 in |
|
830 mk_proof (PNotI p) |
|
831 end |
|
832 | x2p (Elem("pnote",[],[prf])) = |
|
833 let |
|
834 val p = x2p prf |
|
835 in |
|
836 mk_proof (PNotE p) |
|
837 end |
|
838 | x2p (Elem("pcontr",[("i",is)],[prf])) = |
|
839 let |
|
840 val p = x2p prf |
|
841 val t = index_to_term is |
|
842 in |
|
843 mk_proof (PContr (p,t)) |
|
844 end |
|
845 | x2p _ = raise ERR "x2p" "Bad proof" |
|
846 in |
|
847 x2p prf |
|
848 end |
|
849 |
|
850 fun import_proof_concl thyname thmname thy = |
|
851 let |
|
852 val is = TextIO.openIn(proof_file_name thyname thmname thy) |
|
853 val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is)) |
|
854 val _ = TextIO.closeIn is |
|
855 in |
|
856 case proof_xml of |
|
857 Elem("proof",[],xtypes::xterms::_::rest) => |
|
858 let |
|
859 val types = TypeNet.input_types thyname xtypes |
|
860 val terms = TermNet.input_terms thyname types xterms |
|
861 fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm |
|
862 in |
|
863 case rest of |
|
864 [] => NONE |
|
865 | [xtm] => SOME (f xtm) |
|
866 | _ => raise ERR "import_proof" "Bad argument list" |
|
867 end |
|
868 | _ => raise ERR "import_proof" "Bad proof" |
|
869 end |
|
870 |
|
871 fun import_proof thyname thmname thy = |
|
872 let |
|
873 val is = TextIO.openIn(proof_file_name thyname thmname thy) |
|
874 val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is)) |
|
875 val _ = TextIO.closeIn is |
|
876 in |
|
877 case proof_xml of |
|
878 Elem("proof",[],xtypes::xterms::prf::rest) => |
|
879 let |
|
880 val types = TypeNet.input_types thyname xtypes |
|
881 val terms = TermNet.input_terms thyname types xterms |
|
882 in |
|
883 (case rest of |
|
884 [] => NONE |
|
885 | [xtm] => SOME (fn thy => TermNet.get_term_from_xml thy thyname types terms xtm) |
|
886 | _ => raise ERR "import_proof" "Bad argument list", |
|
887 xml_to_proof thyname types terms prf) |
|
888 end |
|
889 | _ => raise ERR "import_proof" "Bad proof" |
|
890 end |
|
891 |
|
892 fun uniq_compose m th i st = |
|
893 let |
|
894 val res = Thm.bicompose false (false,th,m) i st |
|
895 in |
|
896 case Seq.pull res of |
|
897 SOME (th,rest) => (case Seq.pull rest of |
|
898 SOME _ => raise ERR "uniq_compose" "Not unique!" |
|
899 | NONE => th) |
|
900 | NONE => raise ERR "uniq_compose" "No result" |
|
901 end |
|
902 |
|
903 val reflexivity_thm = @{thm refl} |
|
904 val mp_thm = @{thm mp} |
|
905 val imp_antisym_thm = @{thm light_imp_as} |
|
906 val disch_thm = @{thm impI} |
|
907 val ccontr_thm = @{thm ccontr} |
|
908 |
|
909 val meta_eq_to_obj_eq_thm = @{thm meta_eq_to_obj_eq} |
|
910 |
|
911 val gen_thm = @{thm HOLallI} |
|
912 val choose_thm = @{thm exE} |
|
913 val exists_thm = @{thm exI} |
|
914 val conj_thm = @{thm conjI} |
|
915 val conjunct1_thm = @{thm conjunct1} |
|
916 val conjunct2_thm = @{thm conjunct2} |
|
917 val spec_thm = @{thm spec} |
|
918 val disj_cases_thm = @{thm disjE} |
|
919 val disj1_thm = @{thm disjI1} |
|
920 val disj2_thm = @{thm disjI2} |
|
921 |
|
922 local |
|
923 val th = @{thm not_def} |
|
924 val thy = theory_of_thm th |
|
925 val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT))) |
|
926 in |
|
927 val not_elim_thm = Thm.combination pp th |
|
928 end |
|
929 |
|
930 val not_intro_thm = Thm.symmetric not_elim_thm |
|
931 val abs_thm = @{thm ext} |
|
932 val trans_thm = @{thm trans} |
|
933 val symmetry_thm = @{thm sym} |
|
934 val eqmp_thm = @{thm iffD1} |
|
935 val eqimp_thm = @{thm Importer.eq_imp} |
|
936 val comb_thm = @{thm cong} |
|
937 |
|
938 (* Beta-eta normalizes a theorem (only the conclusion, not the * |
|
939 hypotheses!) *) |
|
940 |
|
941 fun beta_eta_thm th = |
|
942 let |
|
943 val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th)) th |
|
944 val th2 = Thm.equal_elim (Thm.eta_conversion (cprop_of th1)) th1 |
|
945 in |
|
946 th2 |
|
947 end |
|
948 |
|
949 fun implies_elim_all th = |
|
950 Library.foldl (fn (th,p) => Thm.implies_elim th (Thm.assume p)) (th,cprems_of th) |
|
951 |
|
952 fun norm_hyps th = |
|
953 th |> beta_eta_thm |
|
954 |> implies_elim_all |
|
955 |> implies_intr_hyps |
|
956 |
|
957 fun mk_GEN v th sg = |
|
958 let |
|
959 val c = HOLogic.dest_Trueprop (concl_of th) |
|
960 val cv = cterm_of sg v |
|
961 val lc = Term.lambda v c |
|
962 val clc = Thm.cterm_of sg lc |
|
963 val cvty = ctyp_of_term cv |
|
964 val th1 = implies_elim_all th |
|
965 val th2 = beta_eta_thm (Thm.forall_intr cv th1) |
|
966 val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm)) |
|
967 val c = prop_of th3 |
|
968 val vname = fst(dest_Free v) |
|
969 val (cold,cnew) = case c of |
|
970 tpc $ (Const(@{const_name All},_) $ Abs(oldname,_,_)) => |
|
971 (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0)) |
|
972 | tpc $ (Const(@{const_name All},_) $ _) => (tpc,tpc) |
|
973 | _ => raise ERR "mk_GEN" "Unknown conclusion" |
|
974 val th4 = Thm.rename_boundvars cold cnew th3 |
|
975 val res = implies_intr_hyps th4 |
|
976 in |
|
977 res |
|
978 end |
|
979 |
|
980 fun rearrange sg tm th = |
|
981 let |
|
982 val tm' = Envir.beta_eta_contract tm |
|
983 fun find [] n = Thm.permute_prems 0 1 (Thm.implies_intr (Thm.cterm_of sg tm) th) |
|
984 | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p) |
|
985 then Thm.permute_prems n 1 th |
|
986 else find ps (n+1) |
|
987 in |
|
988 find (prems_of th) 0 |
|
989 end |
|
990 |
|
991 fun zip (x::xs) (y::ys) = (x,y)::(zip xs ys) |
|
992 | zip [] [] = [] |
|
993 | zip _ _ = raise ERR "zip" "arguments not of same length" |
|
994 |
|
995 fun mk_INST dom rng th = |
|
996 th |> forall_intr_list dom |
|
997 |> forall_elim_list rng |
|
998 |
|
999 (* Code for disambiguating variablenames (wrt. types) *) |
|
1000 |
|
1001 val disamb_info_empty = {vars=[],rens=[]} |
|
1002 |
|
1003 fun rens_of { vars = _, rens = rens } = rens |
|
1004 |
|
1005 fun disamb_term_from info tm = (info, tm) |
|
1006 |
|
1007 fun has_ren (HOLThm _) = false |
|
1008 |
|
1009 fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm) |
|
1010 |
|
1011 fun disamb_terms_from info tms = (info, tms) |
|
1012 |
|
1013 fun disamb_thms_from info hthms = (info, map hthm2thm hthms) |
|
1014 |
|
1015 fun disamb_term tm = disamb_term_from disamb_info_empty tm |
|
1016 fun disamb_thm thm = disamb_thm_from disamb_info_empty thm |
|
1017 fun disamb_thms thms = disamb_thms_from disamb_info_empty thms |
|
1018 |
|
1019 fun norm_hthm _ (hth as HOLThm _) = hth |
|
1020 |
|
1021 (* End of disambiguating code *) |
|
1022 |
|
1023 fun disambiguate_frees thm = |
|
1024 let |
|
1025 fun ERR s = error ("Drule.disambiguate_frees: "^s) |
|
1026 val ct = cprop_of thm |
|
1027 val t = term_of ct |
|
1028 val thy = theory_of_cterm ct |
|
1029 val frees = Misc_Legacy.term_frees t |
|
1030 val freenames = Term.add_free_names t [] |
|
1031 val is_old_name = member (op =) freenames |
|
1032 fun name_of (Free (n, _)) = n |
|
1033 | name_of _ = ERR "name_of" |
|
1034 fun new_name' bump map n = |
|
1035 let val n' = n^bump in |
|
1036 if is_old_name n' orelse Symtab.lookup map n' <> NONE then |
|
1037 new_name' (Symbol.bump_string bump) map n |
|
1038 else |
|
1039 n' |
|
1040 end |
|
1041 val new_name = new_name' "a" |
|
1042 fun replace_name n' (Free (_, t)) = Free (n', t) |
|
1043 | replace_name _ _ = ERR "replace_name" |
|
1044 (* map: old or fresh name -> old free, |
|
1045 invmap: old free which has fresh name assigned to it -> fresh name *) |
|
1046 fun dis v (mapping as (map,invmap)) = |
|
1047 let val n = name_of v in |
|
1048 case Symtab.lookup map n of |
|
1049 NONE => (Symtab.update (n, v) map, invmap) |
|
1050 | SOME v' => |
|
1051 if v=v' then |
|
1052 mapping |
|
1053 else |
|
1054 let val n' = new_name map n in |
|
1055 (Symtab.update (n', v) map, |
|
1056 Termtab.update (v, n') invmap) |
|
1057 end |
|
1058 end |
|
1059 in |
|
1060 if (length freenames = length frees) then |
|
1061 thm |
|
1062 else |
|
1063 let |
|
1064 val (_, invmap) = |
|
1065 fold dis frees (Symtab.empty, Termtab.empty) |
|
1066 fun make_subst (oldfree, newname) (intros, elims) = |
|
1067 (cterm_of thy oldfree :: intros, |
|
1068 cterm_of thy (replace_name newname oldfree) :: elims) |
|
1069 val (intros, elims) = fold make_subst (Termtab.dest invmap) ([], []) |
|
1070 in |
|
1071 forall_elim_list elims (forall_intr_list intros thm) |
|
1072 end |
|
1073 end |
|
1074 |
|
1075 val debug = Unsynchronized.ref false |
|
1076 |
|
1077 fun if_debug f x = if !debug then f x else () |
|
1078 val message = if_debug writeln |
|
1079 |
|
1080 fun get_importer_thm thyname thmname thy = |
|
1081 case get_importer_theorem thyname thmname thy of |
|
1082 SOME hth => SOME (HOLThm hth) |
|
1083 | NONE => |
|
1084 let |
|
1085 val pending = Importer_Pending.get thy |
|
1086 in |
|
1087 case StringPair.lookup pending (thyname,thmname) of |
|
1088 SOME hth => SOME (HOLThm hth) |
|
1089 | NONE => NONE |
|
1090 end |
|
1091 |
|
1092 fun non_trivial_term_consts t = fold_aterms |
|
1093 (fn Const (c, _) => |
|
1094 if c = @{const_name Trueprop} orelse c = @{const_name All} |
|
1095 orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name HOL.eq} |
|
1096 then I else insert (op =) c |
|
1097 | _ => I) t []; |
|
1098 |
|
1099 fun split_name str = |
|
1100 let |
|
1101 val sub = Substring.full str |
|
1102 val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub) |
|
1103 val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f) |
|
1104 in |
|
1105 if not (idx = "") andalso u = "_" |
|
1106 then SOME (newstr, the (Int.fromString idx)) |
|
1107 else NONE |
|
1108 end |
|
1109 handle _ => NONE (* FIXME avoid handle _ *) |
|
1110 |
|
1111 fun rewrite_importer_term t thy = |
|
1112 let |
|
1113 val import_rews1 = map (Thm.transfer thy) (Importer_Rewrites.get thy) |
|
1114 val importerss = Simplifier.global_context thy empty_ss addsimps import_rews1 |
|
1115 in |
|
1116 Thm.transfer thy (Simplifier.full_rewrite importerss (cterm_of thy t)) |
|
1117 end |
|
1118 |
|
1119 fun get_isabelle_thm thyname thmname importerconc thy = |
|
1120 let |
|
1121 val (info,importerconc') = disamb_term importerconc |
|
1122 val i2h_conc = Thm.symmetric (rewrite_importer_term (HOLogic.mk_Trueprop importerconc') thy) |
|
1123 val isaconc = |
|
1124 case concl_of i2h_conc of |
|
1125 Const("==",_) $ lhs $ _ => lhs |
|
1126 | _ => error "get_isabelle_thm" "Bad rewrite rule" |
|
1127 val _ = (message "Original conclusion:"; |
|
1128 if_debug prin importerconc'; |
|
1129 message "Modified conclusion:"; |
|
1130 if_debug prin isaconc) |
|
1131 |
|
1132 fun mk_res th = HOLThm (rens_of info, Thm.equal_elim i2h_conc th) |
|
1133 in |
|
1134 case get_importer_mapping thyname thmname thy of |
|
1135 SOME (SOME thmname) => |
|
1136 let |
|
1137 val th1 = (SOME (Global_Theory.get_thm thy thmname) |
|
1138 handle ERROR _ => |
|
1139 (case split_name thmname of |
|
1140 SOME (listname,idx) => (SOME (nth (Global_Theory.get_thms thy listname) (idx - 1)) |
|
1141 handle _ => NONE) (* FIXME avoid handle _ *) |
|
1142 | NONE => NONE)) |
|
1143 in |
|
1144 case th1 of |
|
1145 SOME th2 => |
|
1146 (case Shuffler.set_prop thy isaconc [(thmname,th2)] of |
|
1147 SOME (_,th) => (message "YES";(thy, SOME (mk_res th))) |
|
1148 | NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping")) |
|
1149 | NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping") |
|
1150 end |
|
1151 | SOME NONE => error ("Trying to access ignored theorem " ^ thmname) |
|
1152 | NONE => |
|
1153 let |
|
1154 val _ = (message "Looking for conclusion:"; |
|
1155 if_debug prin isaconc) |
|
1156 val cs = non_trivial_term_consts isaconc; |
|
1157 val _ = (message "Looking for consts:"; |
|
1158 message (commas cs)) |
|
1159 val pot_thms = Shuffler.find_potential thy isaconc |
|
1160 val _ = message (string_of_int (length pot_thms) ^ " potential theorems") |
|
1161 in |
|
1162 case Shuffler.set_prop thy isaconc pot_thms of |
|
1163 SOME (isaname,th) => |
|
1164 let |
|
1165 val hth as HOLThm args = mk_res th |
|
1166 val thy' = thy |> add_importer_theorem thyname thmname args |
|
1167 |> add_importer_mapping thyname thmname isaname |
|
1168 in |
|
1169 (thy',SOME hth) |
|
1170 end |
|
1171 | NONE => (thy,NONE) |
|
1172 end |
|
1173 end |
|
1174 handle e => |
|
1175 if Exn.is_interrupt e then reraise e |
|
1176 else |
|
1177 (if_debug (fn () => |
|
1178 writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) (); |
|
1179 (thy,NONE)) |
|
1180 |
|
1181 fun get_isabelle_thm_and_warn thyname thmname importerconc thy = |
|
1182 let |
|
1183 val (a, b) = get_isabelle_thm thyname thmname importerconc thy |
|
1184 fun warn () = |
|
1185 let |
|
1186 val (_,importerconc') = disamb_term importerconc |
|
1187 val i2h_conc = Thm.symmetric (rewrite_importer_term (HOLogic.mk_Trueprop importerconc') thy) |
|
1188 in |
|
1189 case concl_of i2h_conc of |
|
1190 Const("==",_) $ lhs $ _ => |
|
1191 (warning ("Failed lookup of theorem '"^thmname^"':"); |
|
1192 writeln "Original conclusion:"; |
|
1193 prin importerconc'; |
|
1194 writeln "Modified conclusion:"; |
|
1195 prin lhs) |
|
1196 | _ => () |
|
1197 end |
|
1198 in |
|
1199 case b of |
|
1200 NONE => (warn () handle _ => (); (a,b)) (* FIXME avoid handle _ *) |
|
1201 | _ => (a, b) |
|
1202 end |
|
1203 |
|
1204 fun get_thm thyname thmname thy = |
|
1205 case get_importer_thm thyname thmname thy of |
|
1206 SOME hth => (thy,SOME hth) |
|
1207 | NONE => ((case import_proof_concl thyname thmname thy of |
|
1208 SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy |
|
1209 | NONE => (message "No conclusion"; (thy,NONE))) |
|
1210 handle IO.Io _ => (message "IO exception"; (thy,NONE)) |
|
1211 | PK _ => (message "PK exception"; (thy,NONE))) |
|
1212 |
|
1213 fun rename_const thyname thy name = |
|
1214 case get_importer_const_renaming thyname name thy of |
|
1215 SOME cname => cname |
|
1216 | NONE => name |
|
1217 |
|
1218 fun get_def thyname constname rhs thy = |
|
1219 let |
|
1220 val constname = rename_const thyname thy constname |
|
1221 val (thmname,thy') = get_defname thyname constname thy |
|
1222 val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname) |
|
1223 in |
|
1224 get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy' |
|
1225 end |
|
1226 |
|
1227 fun get_axiom thyname axname thy = |
|
1228 case get_thm thyname axname thy of |
|
1229 arg as (_,SOME _) => arg |
|
1230 | _ => raise ERR "get_axiom" ("Trying to retrieve axiom (" ^ axname ^ ")") |
|
1231 |
|
1232 fun intern_store_thm gen_output thyname thmname hth thy = |
|
1233 let |
|
1234 val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth |
|
1235 val rew = rewrite_importer_term (concl_of th) thy |
|
1236 val th = Thm.equal_elim rew th |
|
1237 val thy' = add_importer_pending thyname thmname args thy |
|
1238 val th = disambiguate_frees th |
|
1239 val th = Object_Logic.rulify th |
|
1240 val thy2 = |
|
1241 if gen_output |
|
1242 then |
|
1243 add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ |
|
1244 (smart_string_of_thm (Syntax.init_pretty_global thy') th) ^ "\n by (import " ^ |
|
1245 thyname ^ " " ^ (quotename thmname) ^ ")") thy' |
|
1246 else thy' |
|
1247 in |
|
1248 (thy2,hth') |
|
1249 end |
|
1250 |
|
1251 val store_thm = intern_store_thm true |
|
1252 |
|
1253 fun mk_REFL ctm = |
|
1254 let |
|
1255 val cty = Thm.ctyp_of_term ctm |
|
1256 in |
|
1257 Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm |
|
1258 end |
|
1259 |
|
1260 fun REFL tm thy = |
|
1261 let |
|
1262 val _ = message "REFL:" |
|
1263 val (info,tm') = disamb_term tm |
|
1264 val ctm = Thm.cterm_of thy tm' |
|
1265 val res = HOLThm(rens_of info,mk_REFL ctm) |
|
1266 val _ = if_debug pth res |
|
1267 in |
|
1268 (thy,res) |
|
1269 end |
|
1270 |
|
1271 fun ASSUME tm thy = |
|
1272 let |
|
1273 val _ = message "ASSUME:" |
|
1274 val (info,tm') = disamb_term tm |
|
1275 val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm') |
|
1276 val th = Thm.trivial ctm |
|
1277 val res = HOLThm(rens_of info,th) |
|
1278 val _ = if_debug pth res |
|
1279 in |
|
1280 (thy,res) |
|
1281 end |
|
1282 |
|
1283 fun INST_TYPE lambda (hth as HOLThm(_,th)) thy = |
|
1284 let |
|
1285 val _ = message "INST_TYPE:" |
|
1286 val _ = if_debug pth hth |
|
1287 val tys_before = Misc_Legacy.add_term_tfrees (prop_of th,[]) |
|
1288 val th1 = Thm.varifyT_global th |
|
1289 val tys_after = Misc_Legacy.add_term_tvars (prop_of th1,[]) |
|
1290 val tyinst = map (fn (bef, iS) => |
|
1291 (case try (Lib.assoc (TFree bef)) lambda of |
|
1292 SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty) |
|
1293 | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef)) |
|
1294 )) |
|
1295 (zip tys_before tys_after) |
|
1296 val res = Drule.instantiate_normalize (tyinst,[]) th1 |
|
1297 val hth = HOLThm([],res) |
|
1298 val res = norm_hthm thy hth |
|
1299 val _ = message "RESULT:" |
|
1300 val _ = if_debug pth res |
|
1301 in |
|
1302 (thy,res) |
|
1303 end |
|
1304 |
|
1305 fun INST sigma hth thy = |
|
1306 let |
|
1307 val _ = message "INST:" |
|
1308 val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma |
|
1309 val _ = if_debug pth hth |
|
1310 val (sdom,srng) = ListPair.unzip (rev sigma) |
|
1311 val th = hthm2thm hth |
|
1312 val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th |
|
1313 val res = HOLThm([],th1) |
|
1314 val _ = message "RESULT:" |
|
1315 val _ = if_debug pth res |
|
1316 in |
|
1317 (thy,res) |
|
1318 end |
|
1319 |
|
1320 fun EQ_IMP_RULE (hth as HOLThm(rens,th)) thy = |
|
1321 let |
|
1322 val _ = message "EQ_IMP_RULE:" |
|
1323 val _ = if_debug pth hth |
|
1324 val res = HOLThm(rens,th RS eqimp_thm) |
|
1325 val _ = message "RESULT:" |
|
1326 val _ = if_debug pth res |
|
1327 in |
|
1328 (thy,res) |
|
1329 end |
|
1330 |
|
1331 fun mk_EQ_MP th1 th2 = [beta_eta_thm th1, beta_eta_thm th2] MRS eqmp_thm |
|
1332 |
|
1333 fun EQ_MP hth1 hth2 thy = |
|
1334 let |
|
1335 val _ = message "EQ_MP:" |
|
1336 val _ = if_debug pth hth1 |
|
1337 val _ = if_debug pth hth2 |
|
1338 val (info,[th1,th2]) = disamb_thms [hth1,hth2] |
|
1339 val res = HOLThm(rens_of info,mk_EQ_MP th1 th2) |
|
1340 val _ = message "RESULT:" |
|
1341 val _ = if_debug pth res |
|
1342 in |
|
1343 (thy,res) |
|
1344 end |
|
1345 |
|
1346 fun mk_COMB th1 th2 thy = |
|
1347 let |
|
1348 val (f,g) = case concl_of th1 of |
|
1349 _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (f,g) |
|
1350 | _ => raise ERR "mk_COMB" "First theorem not an equality" |
|
1351 val (x,y) = case concl_of th2 of |
|
1352 _ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y) |
|
1353 | _ => raise ERR "mk_COMB" "Second theorem not an equality" |
|
1354 val fty = type_of f |
|
1355 val (fd,fr) = Term.dest_funT fty |
|
1356 val comb_thm' = Drule.instantiate' |
|
1357 [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)] |
|
1358 [SOME (cterm_of thy f),SOME (cterm_of thy g), |
|
1359 SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm |
|
1360 in |
|
1361 [th1,th2] MRS comb_thm' |
|
1362 end |
|
1363 |
|
1364 fun SUBST rews ctxt hth thy = |
|
1365 let |
|
1366 val _ = message "SUBST:" |
|
1367 val _ = if_debug (app pth) rews |
|
1368 val _ = if_debug prin ctxt |
|
1369 val _ = if_debug pth hth |
|
1370 val (info,th) = disamb_thm hth |
|
1371 val (info1,ctxt') = disamb_term_from info ctxt |
|
1372 val (info2,rews') = disamb_thms_from info1 rews |
|
1373 |
|
1374 val cctxt = cterm_of thy ctxt' |
|
1375 fun subst th [] = th |
|
1376 | subst th (rew::rews) = subst (mk_COMB th rew thy) rews |
|
1377 val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th) |
|
1378 val _ = message "RESULT:" |
|
1379 val _ = if_debug pth res |
|
1380 in |
|
1381 (thy,res) |
|
1382 end |
|
1383 |
|
1384 fun DISJ_CASES hth hth1 hth2 thy = |
|
1385 let |
|
1386 val _ = message "DISJ_CASES:" |
|
1387 val _ = if_debug (app pth) [hth,hth1,hth2] |
|
1388 val (info,th) = disamb_thm hth |
|
1389 val (info1,th1) = disamb_thm_from info hth1 |
|
1390 val (info2,th2) = disamb_thm_from info1 hth2 |
|
1391 val th1 = norm_hyps th1 |
|
1392 val th2 = norm_hyps th2 |
|
1393 val (l,r) = case concl_of th of |
|
1394 _ $ (Const(@{const_name HOL.disj},_) $ l $ r) => (l,r) |
|
1395 | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction" |
|
1396 val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1 |
|
1397 val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2 |
|
1398 val res1 = th RS disj_cases_thm |
|
1399 val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1 |
|
1400 val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2 |
|
1401 val res = HOLThm(rens_of info2,res3) |
|
1402 val _ = message "RESULT:" |
|
1403 val _ = if_debug pth res |
|
1404 in |
|
1405 (thy,res) |
|
1406 end |
|
1407 |
|
1408 fun DISJ1 hth tm thy = |
|
1409 let |
|
1410 val _ = message "DISJ1:" |
|
1411 val _ = if_debug pth hth |
|
1412 val _ = if_debug prin tm |
|
1413 val (info,th) = disamb_thm hth |
|
1414 val (info',tm') = disamb_term_from info tm |
|
1415 val ct = Thm.cterm_of thy tm' |
|
1416 val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm |
|
1417 val res = HOLThm(rens_of info',th RS disj1_thm') |
|
1418 val _ = message "RESULT:" |
|
1419 val _ = if_debug pth res |
|
1420 in |
|
1421 (thy,res) |
|
1422 end |
|
1423 |
|
1424 fun DISJ2 tm hth thy = |
|
1425 let |
|
1426 val _ = message "DISJ1:" |
|
1427 val _ = if_debug prin tm |
|
1428 val _ = if_debug pth hth |
|
1429 val (info,th) = disamb_thm hth |
|
1430 val (info',tm') = disamb_term_from info tm |
|
1431 val ct = Thm.cterm_of thy tm' |
|
1432 val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm |
|
1433 val res = HOLThm(rens_of info',th RS disj2_thm') |
|
1434 val _ = message "RESULT:" |
|
1435 val _ = if_debug pth res |
|
1436 in |
|
1437 (thy,res) |
|
1438 end |
|
1439 |
|
1440 fun IMP_ANTISYM hth1 hth2 thy = |
|
1441 let |
|
1442 val _ = message "IMP_ANTISYM:" |
|
1443 val _ = if_debug pth hth1 |
|
1444 val _ = if_debug pth hth2 |
|
1445 val (info,[th1,th2]) = disamb_thms [hth1,hth2] |
|
1446 val th = [beta_eta_thm th1,beta_eta_thm th2] MRS imp_antisym_thm |
|
1447 val res = HOLThm(rens_of info,th) |
|
1448 val _ = message "RESULT:" |
|
1449 val _ = if_debug pth res |
|
1450 in |
|
1451 (thy,res) |
|
1452 end |
|
1453 |
|
1454 fun SYM (hth as HOLThm(rens,th)) thy = |
|
1455 let |
|
1456 val _ = message "SYM:" |
|
1457 val _ = if_debug pth hth |
|
1458 val th = th RS symmetry_thm |
|
1459 val res = HOLThm(rens,th) |
|
1460 val _ = message "RESULT:" |
|
1461 val _ = if_debug pth res |
|
1462 in |
|
1463 (thy,res) |
|
1464 end |
|
1465 |
|
1466 fun MP hth1 hth2 thy = |
|
1467 let |
|
1468 val _ = message "MP:" |
|
1469 val _ = if_debug pth hth1 |
|
1470 val _ = if_debug pth hth2 |
|
1471 val (info,[th1,th2]) = disamb_thms [hth1,hth2] |
|
1472 val th = [beta_eta_thm th1,beta_eta_thm th2] MRS mp_thm |
|
1473 val res = HOLThm(rens_of info,th) |
|
1474 val _ = message "RESULT:" |
|
1475 val _ = if_debug pth res |
|
1476 in |
|
1477 (thy,res) |
|
1478 end |
|
1479 |
|
1480 fun CONJ hth1 hth2 thy = |
|
1481 let |
|
1482 val _ = message "CONJ:" |
|
1483 val _ = if_debug pth hth1 |
|
1484 val _ = if_debug pth hth2 |
|
1485 val (info,[th1,th2]) = disamb_thms [hth1,hth2] |
|
1486 val th = [th1,th2] MRS conj_thm |
|
1487 val res = HOLThm(rens_of info,th) |
|
1488 val _ = message "RESULT:" |
|
1489 val _ = if_debug pth res |
|
1490 in |
|
1491 (thy,res) |
|
1492 end |
|
1493 |
|
1494 fun CONJUNCT1 (hth as HOLThm(rens,th)) thy = |
|
1495 let |
|
1496 val _ = message "CONJUNCT1:" |
|
1497 val _ = if_debug pth hth |
|
1498 val res = HOLThm(rens,th RS conjunct1_thm) |
|
1499 val _ = message "RESULT:" |
|
1500 val _ = if_debug pth res |
|
1501 in |
|
1502 (thy,res) |
|
1503 end |
|
1504 |
|
1505 fun CONJUNCT2 (hth as HOLThm(rens,th)) thy = |
|
1506 let |
|
1507 val _ = message "CONJUNCT1:" |
|
1508 val _ = if_debug pth hth |
|
1509 val res = HOLThm(rens,th RS conjunct2_thm) |
|
1510 val _ = message "RESULT:" |
|
1511 val _ = if_debug pth res |
|
1512 in |
|
1513 (thy,res) |
|
1514 end |
|
1515 |
|
1516 fun EXISTS ex wit hth thy = |
|
1517 let |
|
1518 val _ = message "EXISTS:" |
|
1519 val _ = if_debug prin ex |
|
1520 val _ = if_debug prin wit |
|
1521 val _ = if_debug pth hth |
|
1522 val (info,th) = disamb_thm hth |
|
1523 val (info',[ex',wit']) = disamb_terms_from info [ex,wit] |
|
1524 val cwit = cterm_of thy wit' |
|
1525 val cty = ctyp_of_term cwit |
|
1526 val a = case ex' of |
|
1527 (Const(@{const_name Ex},_) $ a) => a |
|
1528 | _ => raise ERR "EXISTS" "Argument not existential" |
|
1529 val ca = cterm_of thy a |
|
1530 val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm) |
|
1531 val th1 = beta_eta_thm th |
|
1532 val th2 = implies_elim_all th1 |
|
1533 val th3 = th2 COMP exists_thm' |
|
1534 val th = implies_intr_hyps th3 |
|
1535 val res = HOLThm(rens_of info',th) |
|
1536 val _ = message "RESULT:" |
|
1537 val _ = if_debug pth res |
|
1538 in |
|
1539 (thy,res) |
|
1540 end |
|
1541 |
|
1542 fun CHOOSE v hth1 hth2 thy = |
|
1543 let |
|
1544 val _ = message "CHOOSE:" |
|
1545 val _ = if_debug prin v |
|
1546 val _ = if_debug pth hth1 |
|
1547 val _ = if_debug pth hth2 |
|
1548 val (info,[th1,th2]) = disamb_thms [hth1,hth2] |
|
1549 val (info',v') = disamb_term_from info v |
|
1550 fun strip 0 _ th = th |
|
1551 | strip n (p::ps) th = |
|
1552 strip (n-1) ps (Thm.implies_elim th (Thm.assume p)) |
|
1553 | strip _ _ _ = raise ERR "CHOOSE" "strip error" |
|
1554 val cv = cterm_of thy v' |
|
1555 val th2 = norm_hyps th2 |
|
1556 val cvty = ctyp_of_term cv |
|
1557 val c = HOLogic.dest_Trueprop (concl_of th2) |
|
1558 val cc = cterm_of thy c |
|
1559 val a = case concl_of th1 of |
|
1560 _ $ (Const(@{const_name Ex},_) $ a) => a |
|
1561 | _ => raise ERR "CHOOSE" "Conclusion not existential" |
|
1562 val ca = cterm_of (theory_of_thm th1) a |
|
1563 val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm) |
|
1564 val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2 |
|
1565 val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21 |
|
1566 val th23 = beta_eta_thm (Thm.forall_intr cv th22) |
|
1567 val th11 = implies_elim_all (beta_eta_thm th1) |
|
1568 val th' = th23 COMP (th11 COMP choose_thm') |
|
1569 val th = implies_intr_hyps th' |
|
1570 val res = HOLThm(rens_of info',th) |
|
1571 val _ = message "RESULT:" |
|
1572 val _ = if_debug pth res |
|
1573 in |
|
1574 (thy,res) |
|
1575 end |
|
1576 |
|
1577 fun GEN v hth thy = |
|
1578 let |
|
1579 val _ = message "GEN:" |
|
1580 val _ = if_debug prin v |
|
1581 val _ = if_debug pth hth |
|
1582 val (info,th) = disamb_thm hth |
|
1583 val (info',v') = disamb_term_from info v |
|
1584 val res = HOLThm(rens_of info',mk_GEN v' th thy) |
|
1585 val _ = message "RESULT:" |
|
1586 val _ = if_debug pth res |
|
1587 in |
|
1588 (thy,res) |
|
1589 end |
|
1590 |
|
1591 fun SPEC tm hth thy = |
|
1592 let |
|
1593 val _ = message "SPEC:" |
|
1594 val _ = if_debug prin tm |
|
1595 val _ = if_debug pth hth |
|
1596 val (info,th) = disamb_thm hth |
|
1597 val (info',tm') = disamb_term_from info tm |
|
1598 val ctm = Thm.cterm_of thy tm' |
|
1599 val cty = Thm.ctyp_of_term ctm |
|
1600 val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm |
|
1601 val th = th RS spec' |
|
1602 val res = HOLThm(rens_of info',th) |
|
1603 val _ = message "RESULT:" |
|
1604 val _ = if_debug pth res |
|
1605 in |
|
1606 (thy,res) |
|
1607 end |
|
1608 |
|
1609 fun COMB hth1 hth2 thy = |
|
1610 let |
|
1611 val _ = message "COMB:" |
|
1612 val _ = if_debug pth hth1 |
|
1613 val _ = if_debug pth hth2 |
|
1614 val (info,[th1,th2]) = disamb_thms [hth1,hth2] |
|
1615 val res = HOLThm(rens_of info,mk_COMB th1 th2 thy) |
|
1616 val _ = message "RESULT:" |
|
1617 val _ = if_debug pth res |
|
1618 in |
|
1619 (thy,res) |
|
1620 end |
|
1621 |
|
1622 fun TRANS hth1 hth2 thy = |
|
1623 let |
|
1624 val _ = message "TRANS:" |
|
1625 val _ = if_debug pth hth1 |
|
1626 val _ = if_debug pth hth2 |
|
1627 val (info,[th1,th2]) = disamb_thms [hth1,hth2] |
|
1628 val th = [th1,th2] MRS trans_thm |
|
1629 val res = HOLThm(rens_of info,th) |
|
1630 val _ = message "RESULT:" |
|
1631 val _ = if_debug pth res |
|
1632 in |
|
1633 (thy,res) |
|
1634 end |
|
1635 |
|
1636 |
|
1637 fun CCONTR tm hth thy = |
|
1638 let |
|
1639 val _ = message "SPEC:" |
|
1640 val _ = if_debug prin tm |
|
1641 val _ = if_debug pth hth |
|
1642 val (info,th) = disamb_thm hth |
|
1643 val (info',tm') = disamb_term_from info tm |
|
1644 val th = norm_hyps th |
|
1645 val ct = cterm_of thy tm' |
|
1646 val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name Not},HOLogic.boolT-->HOLogic.boolT) $ tm')) th |
|
1647 val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm |
|
1648 val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm' |
|
1649 val res = HOLThm(rens_of info',res1) |
|
1650 val _ = message "RESULT:" |
|
1651 val _ = if_debug pth res |
|
1652 in |
|
1653 (thy,res) |
|
1654 end |
|
1655 |
|
1656 fun mk_ABS v th thy = |
|
1657 let |
|
1658 val cv = cterm_of thy v |
|
1659 val th1 = implies_elim_all (beta_eta_thm th) |
|
1660 val (f,g) = case concl_of th1 of |
|
1661 _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g) |
|
1662 | _ => raise ERR "mk_ABS" "Bad conclusion" |
|
1663 val (fd,fr) = Term.dest_funT (type_of f) |
|
1664 val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm |
|
1665 val th2 = Thm.forall_intr cv th1 |
|
1666 val th3 = th2 COMP abs_thm' |
|
1667 val res = implies_intr_hyps th3 |
|
1668 in |
|
1669 res |
|
1670 end |
|
1671 |
|
1672 fun ABS v hth thy = |
|
1673 let |
|
1674 val _ = message "ABS:" |
|
1675 val _ = if_debug prin v |
|
1676 val _ = if_debug pth hth |
|
1677 val (info,th) = disamb_thm hth |
|
1678 val (info',v') = disamb_term_from info v |
|
1679 val res = HOLThm(rens_of info',mk_ABS v' th thy) |
|
1680 val _ = message "RESULT:" |
|
1681 val _ = if_debug pth res |
|
1682 in |
|
1683 (thy,res) |
|
1684 end |
|
1685 |
|
1686 fun GEN_ABS copt vlist hth thy = |
|
1687 let |
|
1688 val _ = message "GEN_ABS:" |
|
1689 val _ = case copt of |
|
1690 SOME c => if_debug prin c |
|
1691 | NONE => () |
|
1692 val _ = if_debug (app prin) vlist |
|
1693 val _ = if_debug pth hth |
|
1694 val (info,th) = disamb_thm hth |
|
1695 val (info',vlist') = disamb_terms_from info vlist |
|
1696 val th1 = |
|
1697 case copt of |
|
1698 SOME (Const(cname,cty)) => |
|
1699 let |
|
1700 fun inst_type ty1 ty2 (TVar _) = raise ERR "GEN_ABS" "Type variable found!" |
|
1701 | inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty |
|
1702 then ty2 |
|
1703 else ty |
|
1704 | inst_type ty1 ty2 (Type(name,tys)) = |
|
1705 Type(name,map (inst_type ty1 ty2) tys) |
|
1706 in |
|
1707 fold_rev (fn v => fn th => |
|
1708 let |
|
1709 val cdom = fst (Term.dest_funT (fst (Term.dest_funT cty))) |
|
1710 val vty = type_of v |
|
1711 val newcty = inst_type cdom vty cty |
|
1712 val cc = cterm_of thy (Const(cname,newcty)) |
|
1713 in |
|
1714 mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy |
|
1715 end) vlist' th |
|
1716 end |
|
1717 | SOME _ => raise ERR "GEN_ABS" "Bad constant" |
|
1718 | NONE => |
|
1719 fold_rev (fn v => fn th => mk_ABS v th thy) vlist' th |
|
1720 val res = HOLThm(rens_of info',th1) |
|
1721 val _ = message "RESULT:" |
|
1722 val _ = if_debug pth res |
|
1723 in |
|
1724 (thy,res) |
|
1725 end |
|
1726 |
|
1727 fun NOT_INTRO (hth as HOLThm(rens,th)) thy = |
|
1728 let |
|
1729 val _ = message "NOT_INTRO:" |
|
1730 val _ = if_debug pth hth |
|
1731 val th1 = implies_elim_all (beta_eta_thm th) |
|
1732 val a = case concl_of th1 of |
|
1733 _ $ (Const(@{const_name HOL.implies},_) $ a $ Const(@{const_name False},_)) => a |
|
1734 | _ => raise ERR "NOT_INTRO" "Conclusion of bad form" |
|
1735 val ca = cterm_of thy a |
|
1736 val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1 |
|
1737 val res = HOLThm(rens,implies_intr_hyps th2) |
|
1738 val _ = message "RESULT:" |
|
1739 val _ = if_debug pth res |
|
1740 in |
|
1741 (thy,res) |
|
1742 end |
|
1743 |
|
1744 fun NOT_ELIM (hth as HOLThm(rens,th)) thy = |
|
1745 let |
|
1746 val _ = message "NOT_INTRO:" |
|
1747 val _ = if_debug pth hth |
|
1748 val th1 = implies_elim_all (beta_eta_thm th) |
|
1749 val a = case concl_of th1 of |
|
1750 _ $ (Const(@{const_name Not},_) $ a) => a |
|
1751 | _ => raise ERR "NOT_ELIM" "Conclusion of bad form" |
|
1752 val ca = cterm_of thy a |
|
1753 val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1 |
|
1754 val res = HOLThm(rens,implies_intr_hyps th2) |
|
1755 val _ = message "RESULT:" |
|
1756 val _ = if_debug pth res |
|
1757 in |
|
1758 (thy,res) |
|
1759 end |
|
1760 |
|
1761 fun DISCH tm hth thy = |
|
1762 let |
|
1763 val _ = message "DISCH:" |
|
1764 val _ = if_debug prin tm |
|
1765 val _ = if_debug pth hth |
|
1766 val (info,th) = disamb_thm hth |
|
1767 val (info',tm') = disamb_term_from info tm |
|
1768 val th1 = beta_eta_thm th |
|
1769 val th2 = implies_elim_all th1 |
|
1770 val th3 = Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2 |
|
1771 val th4 = th3 COMP disch_thm |
|
1772 val res = HOLThm (rens_of info', implies_intr_hyps th4) |
|
1773 val _ = message "RESULT:" |
|
1774 val _ = if_debug pth res |
|
1775 in |
|
1776 (thy,res) |
|
1777 end |
|
1778 |
|
1779 val spaces = space_implode " " |
|
1780 |
|
1781 fun new_definition thyname constname rhs thy = |
|
1782 let |
|
1783 val constname = rename_const thyname thy constname |
|
1784 val redeclared = is_some (Sign.const_type thy (Sign.intern_const thy constname)); |
|
1785 val _ = warning ("Introducing constant " ^ constname) |
|
1786 val (thmname,thy) = get_defname thyname constname thy |
|
1787 val (_,rhs') = disamb_term rhs |
|
1788 val ctype = type_of rhs' |
|
1789 val csyn = mk_syn thy constname |
|
1790 val thy1 = case Importer_DefThy.get thy of |
|
1791 Replaying _ => thy |
|
1792 | _ => Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy |
|
1793 val eq = mk_defeq constname rhs' thy1 |
|
1794 val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1 |
|
1795 val def_thm = hd thms |
|
1796 val thm' = def_thm RS meta_eq_to_obj_eq_thm |
|
1797 val (thy',th) = (thy2, thm') |
|
1798 val fullcname = Sign.intern_const thy' constname |
|
1799 val thy'' = add_importer_const_mapping thyname constname true fullcname thy' |
|
1800 val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'') |
|
1801 val rew = rewrite_importer_term eq thy'' |
|
1802 val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew))) |
|
1803 val thy22 = |
|
1804 if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn |
|
1805 then |
|
1806 let |
|
1807 val ctxt = Syntax.init_pretty_global thy'' |
|
1808 val p1 = quotename constname |
|
1809 val p2 = Syntax.string_of_typ ctxt ctype |
|
1810 val p3 = string_of_mixfix csyn |
|
1811 val p4 = smart_string_of_cterm ctxt crhs |
|
1812 in |
|
1813 add_dump ("definition\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n " ^ p4) thy'' |
|
1814 end |
|
1815 else |
|
1816 let val ctxt = Syntax.init_pretty_global thy'' in |
|
1817 add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^ |
|
1818 Syntax.string_of_typ ctxt ctype ^ |
|
1819 "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n " ^ |
|
1820 quotename thmname ^ ": " ^ smart_string_of_cterm ctxt crhs) thy'' |
|
1821 end |
|
1822 val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of |
|
1823 SOME (_,res) => HOLThm(rens_of linfo,res) |
|
1824 | NONE => raise ERR "new_definition" "Bad conclusion" |
|
1825 val fullname = Sign.full_bname thy22 thmname |
|
1826 val thy22' = case opt_get_output_thy thy22 of |
|
1827 "" => add_importer_mapping thyname thmname fullname thy22 |
|
1828 | output_thy => |
|
1829 let |
|
1830 val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname |
|
1831 in |
|
1832 thy22 |> add_importer_move fullname moved_thmname |
|
1833 |> add_importer_mapping thyname thmname moved_thmname |
|
1834 end |
|
1835 val _ = message "new_definition:" |
|
1836 val _ = if_debug pth hth |
|
1837 in |
|
1838 (thy22',hth) |
|
1839 end |
|
1840 |
|
1841 fun new_specification thyname thmname names hth thy = |
|
1842 case Importer_DefThy.get thy of |
|
1843 Replaying _ => (thy,hth) |
|
1844 | _ => |
|
1845 let |
|
1846 val _ = message "NEW_SPEC:" |
|
1847 val _ = if_debug pth hth |
|
1848 val names = map (rename_const thyname thy) names |
|
1849 val _ = warning ("Introducing constants " ^ commas names) |
|
1850 val (HOLThm(rens,th)) = norm_hthm thy hth |
|
1851 val thy1 = case Importer_DefThy.get thy of |
|
1852 Replaying _ => thy |
|
1853 | _ => |
|
1854 let |
|
1855 fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body) |
|
1856 | dest_eta_abs body = |
|
1857 let |
|
1858 val (dT,_) = Term.dest_funT (type_of body) |
|
1859 in |
|
1860 ("x",dT,body $ Bound 0) |
|
1861 end |
|
1862 handle TYPE _ => raise ERR "new_specification" "not an abstraction type" |
|
1863 fun dest_exists (Const(@{const_name Ex},_) $ abody) = |
|
1864 dest_eta_abs abody |
|
1865 | dest_exists _ = |
|
1866 raise ERR "new_specification" "Bad existential formula" |
|
1867 |
|
1868 val (consts,_) = Library.foldl (fn ((cs,ex),cname) => |
|
1869 let |
|
1870 val (_,cT,p) = dest_exists ex |
|
1871 in |
|
1872 ((cname,cT,mk_syn thy cname)::cs,p) |
|
1873 end) (([],HOLogic.dest_Trueprop (concl_of th)),names) |
|
1874 val str = Library.foldl (fn (acc, (c, T, csyn)) => |
|
1875 acc ^ "\n " ^ quotename c ^ " :: \"" ^ |
|
1876 Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts) |
|
1877 val thy' = add_dump str thy |
|
1878 in |
|
1879 Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy' |
|
1880 end |
|
1881 |
|
1882 val thy1 = fold_rev (fn name => fn thy => |
|
1883 snd (get_defname thyname name thy)) names thy1 |
|
1884 fun new_name name = fst (get_defname thyname name thy1) |
|
1885 val names' = map (fn name => (new_name name,name,false)) names |
|
1886 val (thy',res) = Choice_Specification.add_specification NONE |
|
1887 names' |
|
1888 (thy1,th) |
|
1889 val res' = Thm.unvarify_global res |
|
1890 val hth = HOLThm(rens,res') |
|
1891 val rew = rewrite_importer_term (concl_of res') thy' |
|
1892 val th = Thm.equal_elim rew res' |
|
1893 fun handle_const (name,thy) = |
|
1894 let |
|
1895 val defname = Thm.def_name name |
|
1896 val (newname,thy') = get_defname thyname name thy |
|
1897 in |
|
1898 (if defname = newname |
|
1899 then quotename name |
|
1900 else (quotename newname) ^ ": " ^ (quotename name),thy') |
|
1901 end |
|
1902 val (new_names,thy') = fold_rev (fn name => fn (names, thy) => |
|
1903 let |
|
1904 val (name',thy') = handle_const (name,thy) |
|
1905 in |
|
1906 (name'::names,thy') |
|
1907 end) names ([], thy') |
|
1908 val thy'' = |
|
1909 add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ |
|
1910 (smart_string_of_thm (Syntax.init_pretty_global thy') th) ^ |
|
1911 "\n by (import " ^ thyname ^ " " ^ thmname ^ ")") |
|
1912 thy' |
|
1913 val _ = message "RESULT:" |
|
1914 val _ = if_debug pth hth |
|
1915 in |
|
1916 intern_store_thm false thyname thmname hth thy'' |
|
1917 end |
|
1918 |
|
1919 fun new_axiom name _ _ = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")") |
|
1920 |
|
1921 fun to_isa_thm (hth as HOLThm(_,th)) = |
|
1922 let |
|
1923 val (HOLThm args) = norm_hthm (theory_of_thm th) hth |
|
1924 in |
|
1925 apsnd Thm.strip_shyps args |
|
1926 end |
|
1927 |
|
1928 fun to_isa_term tm = tm |
|
1929 |
|
1930 local |
|
1931 val light_nonempty = @{thm light_ex_imp_nonempty} |
|
1932 val ex_imp_nonempty = @{thm ex_imp_nonempty} |
|
1933 val typedef_hol2hol4 = @{thm typedef_hol2hol4} |
|
1934 val typedef_hol2hollight = @{thm typedef_hol2hollight} |
|
1935 in |
|
1936 fun new_type_definition thyname thmname tycname hth thy = |
|
1937 case Importer_DefThy.get thy of |
|
1938 Replaying _ => (thy,hth) |
|
1939 | _ => |
|
1940 let |
|
1941 val _ = message "TYPE_DEF:" |
|
1942 val _ = if_debug pth hth |
|
1943 val _ = warning ("Introducing type " ^ tycname) |
|
1944 val (HOLThm(rens,td_th)) = norm_hthm thy hth |
|
1945 val th2 = beta_eta_thm (td_th RS ex_imp_nonempty) |
|
1946 val c = case concl_of th2 of |
|
1947 _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c |
|
1948 | _ => raise ERR "new_type_definition" "Bad type definition theorem" |
|
1949 val tfrees = Misc_Legacy.term_tfrees c |
|
1950 val tnames = map fst tfrees |
|
1951 val tsyn = mk_syn thy tycname |
|
1952 val ((_, typedef_info), thy') = |
|
1953 Typedef.add_typedef_global false (SOME (Binding.name thmname)) |
|
1954 (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy |
|
1955 |
|
1956 val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4 |
|
1957 |
|
1958 val fulltyname = Sign.intern_type thy' tycname |
|
1959 val thy'' = add_importer_type_mapping thyname tycname true fulltyname thy' |
|
1960 |
|
1961 val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3)) |
|
1962 val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating") |
|
1963 else () |
|
1964 val thy4 = add_importer_pending thyname thmname args thy'' |
|
1965 |
|
1966 val rew = rewrite_importer_term (concl_of td_th) thy4 |
|
1967 val th = Thm.equal_elim rew (Thm.transfer thy4 td_th) |
|
1968 val c = case HOLogic.dest_Trueprop (prop_of th) of |
|
1969 Const(@{const_name Ex},exT) $ P => |
|
1970 let |
|
1971 val PT = domain_type exT |
|
1972 in |
|
1973 Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P |
|
1974 end |
|
1975 | _ => error "Internal error in ProofKernel.new_typedefinition" |
|
1976 val tnames_string = if null tnames |
|
1977 then "" |
|
1978 else "(" ^ commas tnames ^ ") " |
|
1979 val proc_prop = |
|
1980 smart_string_of_cterm |
|
1981 (Syntax.init_pretty_global thy4 |
|
1982 |> not (null tnames) ? Config.put show_all_types true) |
|
1983 val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " |
|
1984 ^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4 |
|
1985 |
|
1986 val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2importer [OF type_definition_" ^ tycname ^ "]") thy5 |
|
1987 |
|
1988 val _ = message "RESULT:" |
|
1989 val _ = if_debug pth hth' |
|
1990 in |
|
1991 (thy6,hth') |
|
1992 end |
|
1993 |
|
1994 fun add_dump_syntax thy name = |
|
1995 let |
|
1996 val n = quotename name |
|
1997 val syn = string_of_mixfix (mk_syn thy name) |
|
1998 in |
|
1999 add_dump ("syntax\n "^n^" :: _ "^syn) thy |
|
2000 end |
|
2001 |
|
2002 fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy = |
|
2003 case Importer_DefThy.get thy of |
|
2004 Replaying _ => (thy, |
|
2005 HOLThm([], Global_Theory.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth) |
|
2006 | _ => |
|
2007 let |
|
2008 val _ = message "TYPE_INTRO:" |
|
2009 val _ = if_debug pth hth |
|
2010 val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")") |
|
2011 val (HOLThm(rens,td_th)) = norm_hthm thy hth |
|
2012 val tT = type_of t |
|
2013 val light_nonempty' = |
|
2014 Drule.instantiate' [SOME (ctyp_of thy tT)] |
|
2015 [SOME (cterm_of thy P), |
|
2016 SOME (cterm_of thy t)] light_nonempty |
|
2017 val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty')) |
|
2018 val c = case concl_of th2 of |
|
2019 _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c |
|
2020 | _ => raise ERR "type_introduction" "Bad type definition theorem" |
|
2021 val tfrees = Misc_Legacy.term_tfrees c |
|
2022 val tnames = sort_strings (map fst tfrees) |
|
2023 val tsyn = mk_syn thy tycname |
|
2024 val ((_, typedef_info), thy') = |
|
2025 Typedef.add_typedef_global false NONE |
|
2026 (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c |
|
2027 (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy |
|
2028 val fulltyname = Sign.intern_type thy' tycname |
|
2029 val aty = Type (fulltyname, map mk_vartype tnames) |
|
2030 val typedef_hol2hollight' = |
|
2031 Drule.instantiate' |
|
2032 [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] |
|
2033 [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))] |
|
2034 typedef_hol2hollight |
|
2035 val th4 = (#type_definition (#2 typedef_info)) RS typedef_hol2hollight' |
|
2036 val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse |
|
2037 raise ERR "type_introduction" "no type variables expected any more" |
|
2038 val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse |
|
2039 raise ERR "type_introduction" "no term variables expected any more" |
|
2040 val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname) |
|
2041 val thy'' = add_importer_type_mapping thyname tycname true fulltyname thy' |
|
2042 val _ = message "step 4" |
|
2043 val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4)) |
|
2044 val thy4 = add_importer_pending thyname thmname args thy'' |
|
2045 |
|
2046 val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_importer_term P thy4))) *) |
|
2047 val c = |
|
2048 let |
|
2049 val PT = type_of P' |
|
2050 in |
|
2051 Const (@{const_name Collect},PT-->HOLogic.mk_setT (domain_type PT)) $ P' |
|
2052 end |
|
2053 |
|
2054 val tnames_string = if null tnames |
|
2055 then "" |
|
2056 else "(" ^ commas tnames ^ ") " |
|
2057 val proc_prop = |
|
2058 smart_string_of_cterm |
|
2059 (Syntax.init_pretty_global thy4 |
|
2060 |> not (null tnames) ? Config.put show_all_types true) |
|
2061 val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ |
|
2062 " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ |
|
2063 (string_of_mixfix tsyn) ^ " morphisms "^ |
|
2064 (quote rep_name)^" "^(quote abs_name)^"\n"^ |
|
2065 (" apply (rule light_ex_imp_nonempty[where t="^ |
|
2066 (proc_prop (cterm_of thy4 t))^"])\n"^ |
|
2067 (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4 |
|
2068 val str_aty = Syntax.string_of_typ_global thy aty |
|
2069 val thy = add_dump_syntax thy rep_name |
|
2070 val thy = add_dump_syntax thy abs_name |
|
2071 val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ |
|
2072 " = typedef_hol2hollight \n"^ |
|
2073 " [where a=\"a :: "^str_aty^"\" and r=r" ^ |
|
2074 " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy |
|
2075 val _ = message "RESULT:" |
|
2076 val _ = if_debug pth hth' |
|
2077 in |
|
2078 (thy,hth') |
|
2079 end |
|
2080 end |
|
2081 |
|
2082 val prin = prin |
|
2083 |
|
2084 end |
|