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