author | haftmann |
Wed, 03 May 2006 17:41:28 +0200 | |
changeset 19554 | bc0bef4a124e |
parent 18708 | 4b3dadb4fe33 |
child 21590 | ef7278f553eb |
permissions | -rw-r--r-- |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
1 |
(* Title: HOL/Import/import_package.ML |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
2 |
ID: $Id$ |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
3 |
Author: Sebastian Skalberg (TU Muenchen) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
4 |
*) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
5 |
|
14516 | 6 |
signature IMPORT_PACKAGE = |
7 |
sig |
|
15703 | 8 |
val import_meth: Method.src -> Proof.context -> Proof.method |
18708 | 9 |
val setup : theory -> theory |
14516 | 10 |
val debug : bool ref |
11 |
end |
|
12 |
||
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
13 |
structure ImportDataArgs: THEORY_DATA_ARGS = |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
14 |
struct |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
15 |
val name = "HOL4/import_data" |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
16 |
type T = ProofKernel.thm option array option |
15531 | 17 |
val empty = NONE |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
18 |
val copy = I |
16424 | 19 |
val extend = I |
20 |
fun merge _ _ = NONE |
|
21 |
fun print _ _ = () |
|
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
22 |
end |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
23 |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
24 |
structure ImportData = TheoryDataFun(ImportDataArgs) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
25 |
|
14516 | 26 |
structure ImportPackage :> IMPORT_PACKAGE = |
27 |
struct |
|
28 |
||
29 |
val debug = ref false |
|
30 |
fun message s = if !debug then writeln s else () |
|
31 |
||
14848 | 32 |
val string_of_thm = Library.setmp print_mode [] string_of_thm; |
33 |
val string_of_cterm = Library.setmp print_mode [] string_of_cterm; |
|
14516 | 34 |
|
35 |
fun import_tac (thyname,thmname) = |
|
17370 | 36 |
if ! quick_and_dirty |
14516 | 37 |
then SkipProof.cheat_tac |
38 |
else |
|
39 |
fn thy => |
|
40 |
fn th => |
|
41 |
let |
|
17490 | 42 |
val sg = sign_of_thm th |
14516 | 43 |
val prem = hd (prems_of th) |
17644 | 44 |
val _ = message ("Import_tac: thyname="^thyname^", thmname="^thmname) |
14516 | 45 |
val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem))) |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
46 |
val int_thms = case ImportData.get thy of |
15531 | 47 |
NONE => fst (Replay.setup_int_thms thyname thy) |
48 |
| SOME a => a |
|
14516 | 49 |
val proof = snd (ProofKernel.import_proof thyname thmname thy) thy |
50 |
val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy) |
|
51 |
val thm = snd (ProofKernel.to_isa_thm hol4thm) |
|
52 |
val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy |
|
53 |
val thm = equal_elim rew thm |
|
54 |
val prew = ProofKernel.rewrite_hol4_term prem thy |
|
55 |
val prem' = #2 (Logic.dest_equals (prop_of prew)) |
|
17652 | 56 |
val _ = message ("Import proved " ^ (string_of_thm thm)) |
17657 | 57 |
val thm = ProofKernel.disambiguate_frees thm |
17652 | 58 |
val _ = message ("Disambiguate: " ^ (string_of_thm thm)) |
14516 | 59 |
in |
60 |
case Shuffler.set_prop thy prem' [("",thm)] of |
|
15531 | 61 |
SOME (_,thm) => |
14516 | 62 |
let |
63 |
val _ = if prem' aconv (prop_of thm) |
|
64 |
then message "import: Terms match up" |
|
65 |
else message "import: Terms DO NOT match up" |
|
66 |
val thm' = equal_elim (symmetric prew) thm |
|
67 |
val res = bicompose true (false,thm',0) 1 th |
|
68 |
in |
|
69 |
res |
|
70 |
end |
|
15531 | 71 |
| NONE => (message "import: set_prop didn't succeed"; no_tac th) |
14516 | 72 |
end |
73 |
||
74 |
val import_meth = Method.simple_args (Args.name -- Args.name) |
|
75 |
(fn arg => |
|
76 |
fn ctxt => |
|
77 |
let |
|
78 |
val thy = ProofContext.theory_of ctxt |
|
79 |
in |
|
80 |
Method.SIMPLE_METHOD (import_tac arg thy) |
|
81 |
end) |
|
82 |
||
18708 | 83 |
val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init |
14516 | 84 |
end |
15707 | 85 |