src/HOL/Import/import.ML
changeset 31723 f5cafe803b55
parent 31244 4ed31c673baf
child 31945 d5f186aa0bed
equal deleted inserted replaced
31717:d1f7b6245a75 31723:f5cafe803b55
       
     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