|
1 (* Title: HOL/Import/import.ML |
|
2 Author: Sebastian Skalberg (TU Muenchen) |
|
3 *) |
|
4 |
|
5 signature IMPORT = |
|
6 sig |
|
7 val debug : bool ref |
|
8 val import_tac : Proof.context -> string * string -> tactic |
|
9 val setup : theory -> theory |
|
10 end |
|
11 |
|
12 structure ImportData = TheoryDataFun |
|
13 ( |
|
14 type T = ProofKernel.thm option array option |
|
15 val empty = NONE |
|
16 val copy = I |
|
17 val extend = I |
|
18 fun merge _ _ = NONE |
|
19 ) |
|
20 |
|
21 structure Import :> IMPORT = |
|
22 struct |
|
23 |
|
24 val debug = ref false |
|
25 fun message s = if !debug then writeln s else () |
|
26 |
|
27 fun import_tac ctxt (thyname, thmname) = |
|
28 if ! quick_and_dirty |
|
29 then SkipProof.cheat_tac (ProofContext.theory_of ctxt) |
|
30 else |
|
31 fn th => |
|
32 let |
|
33 val thy = ProofContext.theory_of ctxt |
|
34 val prem = hd (prems_of th) |
|
35 val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname) |
|
36 val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem) |
|
37 val int_thms = case ImportData.get thy of |
|
38 NONE => fst (Replay.setup_int_thms thyname thy) |
|
39 | SOME a => a |
|
40 val proof = snd (ProofKernel.import_proof thyname thmname thy) thy |
|
41 val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy) |
|
42 val thm = snd (ProofKernel.to_isa_thm hol4thm) |
|
43 val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy |
|
44 val thm = equal_elim rew thm |
|
45 val prew = ProofKernel.rewrite_hol4_term prem thy |
|
46 val prem' = #2 (Logic.dest_equals (prop_of prew)) |
|
47 val _ = message ("Import proved " ^ Display.string_of_thm thm) |
|
48 val thm = ProofKernel.disambiguate_frees thm |
|
49 val _ = message ("Disambiguate: " ^ Display.string_of_thm thm) |
|
50 in |
|
51 case Shuffler.set_prop thy prem' [("",thm)] of |
|
52 SOME (_,thm) => |
|
53 let |
|
54 val _ = if prem' aconv (prop_of thm) |
|
55 then message "import: Terms match up" |
|
56 else message "import: Terms DO NOT match up" |
|
57 val thm' = equal_elim (symmetric prew) thm |
|
58 val res = bicompose true (false,thm',0) 1 th |
|
59 in |
|
60 res |
|
61 end |
|
62 | NONE => (message "import: set_prop didn't succeed"; no_tac th) |
|
63 end |
|
64 |
|
65 val setup = Method.setup @{binding import} |
|
66 (Scan.lift (Args.name -- Args.name) >> |
|
67 (fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg))) |
|
68 "import HOL4 theorem" |
|
69 |
|
70 end |
|
71 |