src/HOL/Import/import.ML
author haftmann
Fri, 19 Jun 2009 17:23:21 +0200
changeset 31723 f5cafe803b55
parent 31244 src/HOL/Import/import_package.ML@4ed31c673baf
child 31945 d5f186aa0bed
permissions -rw-r--r--
discontinued ancient tradition to suffix certain ML module names with "_package"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
sig
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
     7
    val debug      : bool ref
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
     8
    val import_tac : Proof.context -> string * string -> tactic
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17657
diff changeset
     9
    val setup      : theory -> theory
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
end
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    12
structure ImportData = TheoryDataFun
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    13
(
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    14
  type T = ProofKernel.thm option array option
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    15
  val empty = NONE
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    16
  val copy = I
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    17
  val extend = I
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    18
  fun merge _ _ = NONE
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22578
diff changeset
    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
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
struct
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
val debug = ref false
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
fun message s = if !debug then writeln s else ()
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    27
fun import_tac ctxt (thyname, thmname) =
17370
754b7fcff03e global quick_and_dirty;
wenzelm
parents: 16424
diff changeset
    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
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
    else
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
     fn th =>
21590
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    32
        let
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    33
            val thy = ProofContext.theory_of ctxt
21590
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    34
            val prem = hd (prems_of th)
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    35
            val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname)
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    36
            val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem)
21590
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    37
            val int_thms = case ImportData.get thy of
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    38
                               NONE => fst (Replay.setup_int_thms thyname thy)
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    39
                             | SOME a => a
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    40
            val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    41
            val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    42
            val thm = snd (ProofKernel.to_isa_thm hol4thm)
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    43
            val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    44
            val thm = equal_elim rew thm
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    45
            val prew = ProofKernel.rewrite_hol4_term prem thy
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    46
            val prem' = #2 (Logic.dest_equals (prop_of prew))
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    47
            val _ = message ("Import proved " ^ Display.string_of_thm thm)
17657
2f5f595eb618 moved disambiguate_frees to ProofKernel;
wenzelm
parents: 17652
diff changeset
    48
            val thm = ProofKernel.disambiguate_frees thm
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    49
            val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
21590
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    50
        in
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    51
            case Shuffler.set_prop thy prem' [("",thm)] of
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    52
                SOME (_,thm) =>
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    53
                let
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    54
                    val _ = if prem' aconv (prop_of thm)
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    55
                            then message "import: Terms match up"
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    56
                            else message "import: Terms DO NOT match up"
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    57
                    val thm' = equal_elim (symmetric prew) thm
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    58
                    val res = bicompose true (false,thm',0) 1 th
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    59
                in
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    60
                    res
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    61
                end
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    62
              | NONE => (message "import: set_prop didn't succeed"; no_tac th)
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    63
        end
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 18708
diff changeset
    64
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    65
val setup = Method.setup @{binding import}
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    66
  (Scan.lift (Args.name -- Args.name) >>
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    67
    (fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg)))
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30510
diff changeset
    68
  "import HOL4 theorem"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
end
15707
80b421d8a8be *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
    71