author | paulson |
Tue, 29 Mar 2005 12:30:48 +0200 | |
changeset 15635 | 8408a06590a6 |
parent 15531 | 08c8dad8e399 |
child 15703 | 727ef1b8b3ee |
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 |
|
8 |
val import_meth: Args.src -> Proof.context -> Proof.method |
|
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 |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
19 |
val prep_ext = I |
15531 | 20 |
fun merge _ = NONE |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
21 |
fun print sg import_segment = |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
22 |
Pretty.writeln (Pretty.str ("Pretty printing of importer data not implemented")) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
23 |
end |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
24 |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
25 |
structure ImportData = TheoryDataFun(ImportDataArgs) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
26 |
|
14516 | 27 |
structure ImportPackage :> IMPORT_PACKAGE = |
28 |
struct |
|
29 |
||
30 |
val debug = ref false |
|
31 |
fun message s = if !debug then writeln s else () |
|
32 |
||
14848 | 33 |
val string_of_thm = Library.setmp print_mode [] string_of_thm; |
34 |
val string_of_cterm = Library.setmp print_mode [] string_of_cterm; |
|
14516 | 35 |
|
36 |
fun import_tac (thyname,thmname) = |
|
37 |
if !SkipProof.quick_and_dirty |
|
38 |
then SkipProof.cheat_tac |
|
39 |
else |
|
40 |
fn thy => |
|
41 |
fn th => |
|
42 |
let |
|
43 |
val sg = sign_of_thm th |
|
44 |
val prem = hd (prems_of th) |
|
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)) |
|
56 |
val _ = message ("Import proved " ^ (string_of_thm thm)) |
|
57 |
in |
|
58 |
case Shuffler.set_prop thy prem' [("",thm)] of |
|
15531 | 59 |
SOME (_,thm) => |
14516 | 60 |
let |
61 |
val _ = if prem' aconv (prop_of thm) |
|
62 |
then message "import: Terms match up" |
|
63 |
else message "import: Terms DO NOT match up" |
|
64 |
val thm' = equal_elim (symmetric prew) thm |
|
65 |
val res = bicompose true (false,thm',0) 1 th |
|
66 |
in |
|
67 |
res |
|
68 |
end |
|
15531 | 69 |
| NONE => (message "import: set_prop didn't succeed"; no_tac th) |
14516 | 70 |
end |
71 |
||
72 |
val import_meth = Method.simple_args (Args.name -- Args.name) |
|
73 |
(fn arg => |
|
74 |
fn ctxt => |
|
75 |
let |
|
76 |
val thy = ProofContext.theory_of ctxt |
|
77 |
in |
|
78 |
Method.SIMPLE_METHOD (import_tac arg thy) |
|
79 |
end) |
|
80 |
||
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
81 |
val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init] |
14516 | 82 |
end |