author  wenzelm 
Mon, 06 Jul 2009 21:24:30 +0200  
changeset 31945  d5f186aa0bed 
parent 31723  f5cafe803b55 
child 32091  30e2ffbba718 
permissions  rwrr 
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 
31241  7 
val debug : bool ref 
8 
val import_tac : Proof.context > string * string > tactic 

18708  9 
val setup : theory > theory 
14516  10 
end 
11 

22846  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 
) 

14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

20 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31244
diff
changeset

21 
structure Import :> IMPORT = 
14516  22 
struct 
23 

24 
val debug = ref false 

25 
fun message s = if !debug then writeln s else () 

26 

31241  27 
fun import_tac ctxt (thyname, thmname) = 
17370  28 
if ! quick_and_dirty 
31244
4ed31c673baf
fixed superficial ML lapses introduced in b3c7044d47b6;
wenzelm
parents:
31241
diff
changeset

29 
then SkipProof.cheat_tac (ProofContext.theory_of ctxt) 
14516  30 
else 
31 
fn th => 

21590  32 
let 
31241  33 
val thy = ProofContext.theory_of ctxt 
21590  34 
val prem = hd (prems_of th) 
31241  35 
val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname) 
36 
val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem) 

21590  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)) 

31241  47 
val _ = message ("Import proved " ^ Display.string_of_thm thm) 
17657  48 
val thm = ProofKernel.disambiguate_frees thm 
31241  49 
val _ = message ("Disambiguate: " ^ Display.string_of_thm thm) 
21590  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 

31945  58 
val res = Thm.bicompose true (false,thm',0) 1 th 
21590  59 
in 
60 
res 

61 
end 

62 
 NONE => (message "import: set_prop didn't succeed"; no_tac th) 

63 
end 

64 

31241  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" 

14516  69 

70 
end 

15707  71 