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