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