author | wenzelm |
Fri, 17 Jun 2005 18:33:05 +0200 | |
changeset 16424 | 18a07ad8fea8 |
parent 15707 | 80b421d8a8be |
child 17370 | 754b7fcff03e |
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 |
14516 | 9 |
val setup : (theory -> theory) list |
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) = |
|
36 |
if !SkipProof.quick_and_dirty |
|
37 |
then SkipProof.cheat_tac |
|
38 |
else |
|
39 |
fn thy => |
|
40 |
fn th => |
|
41 |
let |
|
42 |
val sg = sign_of_thm th |
|
43 |
val prem = hd (prems_of th) |
|
44 |
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
|
45 |
val int_thms = case ImportData.get thy of |
15531 | 46 |
NONE => fst (Replay.setup_int_thms thyname thy) |
47 |
| SOME a => a |
|
14516 | 48 |
val proof = snd (ProofKernel.import_proof thyname thmname thy) thy |
49 |
val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy) |
|
50 |
val thm = snd (ProofKernel.to_isa_thm hol4thm) |
|
51 |
val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy |
|
52 |
val thm = equal_elim rew thm |
|
53 |
val prew = ProofKernel.rewrite_hol4_term prem thy |
|
54 |
val prem' = #2 (Logic.dest_equals (prop_of prew)) |
|
55 |
val _ = message ("Import proved " ^ (string_of_thm thm)) |
|
56 |
in |
|
57 |
case Shuffler.set_prop thy prem' [("",thm)] of |
|
15531 | 58 |
SOME (_,thm) => |
14516 | 59 |
let |
60 |
val _ = if prem' aconv (prop_of thm) |
|
61 |
then message "import: Terms match up" |
|
62 |
else message "import: Terms DO NOT match up" |
|
63 |
val thm' = equal_elim (symmetric prew) thm |
|
64 |
val res = bicompose true (false,thm',0) 1 th |
|
65 |
in |
|
66 |
res |
|
67 |
end |
|
15531 | 68 |
| NONE => (message "import: set_prop didn't succeed"; no_tac th) |
14516 | 69 |
end |
70 |
||
71 |
val import_meth = Method.simple_args (Args.name -- Args.name) |
|
72 |
(fn arg => |
|
73 |
fn ctxt => |
|
74 |
let |
|
75 |
val thy = ProofContext.theory_of ctxt |
|
76 |
in |
|
77 |
Method.SIMPLE_METHOD (import_tac arg thy) |
|
78 |
end) |
|
79 |
||
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
80 |
val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init] |
14516 | 81 |
end |
15707 | 82 |