src/HOL/Import/import.ML
author wenzelm
Sat Oct 17 16:58:03 2009 +0200 (2009-10-17)
changeset 32970 fbd2bb2489a8
parent 32740 9dd0a2f83429
child 33522 737589bb9bb8
permissions -rw-r--r--
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
     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 = 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 = Unsynchronized.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 Skip_Proof.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 ctxt thm)
    48             val thm = ProofKernel.disambiguate_frees thm
    49             val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt 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 = Thm.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