author | wenzelm |
Mon, 17 May 2010 15:11:25 +0200 | |
changeset 36959 | f5417836dbea |
parent 36945 | 9bec62c10714 |
child 42361 | 23f352990944 |
permissions | -rw-r--r-- |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31244
diff
changeset
|
1 |
(* Title: HOL/Import/import.ML |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
2 |
Author: Sebastian Skalberg (TU Muenchen) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
3 |
*) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
4 |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31244
diff
changeset
|
5 |
signature IMPORT = |
14516 | 6 |
sig |
32740 | 7 |
val debug : bool Unsynchronized.ref |
31241 | 8 |
val import_tac : Proof.context -> string * string -> tactic |
18708 | 9 |
val setup : theory -> theory |
14516 | 10 |
end |
11 |
||
33522 | 12 |
structure ImportData = Theory_Data |
22846 | 13 |
( |
33522 | 14 |
type T = ProofKernel.thm option array option (* FIXME mutable array !??!!! *) |
22846 | 15 |
val empty = NONE |
16 |
val extend = I |
|
33522 | 17 |
fun merge _ = NONE |
22846 | 18 |
) |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
19 |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31244
diff
changeset
|
20 |
structure Import :> IMPORT = |
14516 | 21 |
struct |
22 |
||
32740 | 23 |
val debug = Unsynchronized.ref false |
14516 | 24 |
fun message s = if !debug then writeln s else () |
25 |
||
31241 | 26 |
fun import_tac ctxt (thyname, thmname) = |
17370 | 27 |
if ! quick_and_dirty |
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32740
diff
changeset
|
28 |
then Skip_Proof.cheat_tac (ProofContext.theory_of ctxt) |
14516 | 29 |
else |
30 |
fn th => |
|
21590 | 31 |
let |
31241 | 32 |
val thy = ProofContext.theory_of ctxt |
21590 | 33 |
val prem = hd (prems_of th) |
31241 | 34 |
val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname) |
35 |
val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem) |
|
21590 | 36 |
val int_thms = case ImportData.get thy of |
37 |
NONE => fst (Replay.setup_int_thms thyname thy) |
|
38 |
| SOME a => a |
|
39 |
val proof = snd (ProofKernel.import_proof thyname thmname thy) thy |
|
40 |
val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy) |
|
41 |
val thm = snd (ProofKernel.to_isa_thm hol4thm) |
|
42 |
val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy |
|
36945 | 43 |
val thm = Thm.equal_elim rew thm |
21590 | 44 |
val prew = ProofKernel.rewrite_hol4_term prem thy |
45 |
val prem' = #2 (Logic.dest_equals (prop_of prew)) |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset
|
46 |
val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm) |
17657 | 47 |
val thm = ProofKernel.disambiguate_frees thm |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31945
diff
changeset
|
48 |
val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt thm) |
21590 | 49 |
in |
50 |
case Shuffler.set_prop thy prem' [("",thm)] of |
|
51 |
SOME (_,thm) => |
|
52 |
let |
|
53 |
val _ = if prem' aconv (prop_of thm) |
|
54 |
then message "import: Terms match up" |
|
55 |
else message "import: Terms DO NOT match up" |
|
36945 | 56 |
val thm' = Thm.equal_elim (Thm.symmetric prew) thm |
31945 | 57 |
val res = Thm.bicompose true (false,thm',0) 1 th |
21590 | 58 |
in |
59 |
res |
|
60 |
end |
|
61 |
| NONE => (message "import: set_prop didn't succeed"; no_tac th) |
|
62 |
end |
|
63 |
||
31241 | 64 |
val setup = Method.setup @{binding import} |
65 |
(Scan.lift (Args.name -- Args.name) >> |
|
66 |
(fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg))) |
|
67 |
"import HOL4 theorem" |
|
14516 | 68 |
|
69 |
end |
|
15707 | 70 |