src/HOL/Import/import.ML
changeset 31723 f5cafe803b55
parent 31244 4ed31c673baf
child 31945 d5f186aa0bed
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/import.ML	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -0,0 +1,71 @@
     1.4 +(*  Title:      HOL/Import/import.ML
     1.5 +    Author:     Sebastian Skalberg (TU Muenchen)
     1.6 +*)
     1.7 +
     1.8 +signature IMPORT =
     1.9 +sig
    1.10 +    val debug      : bool ref
    1.11 +    val import_tac : Proof.context -> string * string -> tactic
    1.12 +    val setup      : theory -> theory
    1.13 +end
    1.14 +
    1.15 +structure ImportData = TheoryDataFun
    1.16 +(
    1.17 +  type T = ProofKernel.thm option array option
    1.18 +  val empty = NONE
    1.19 +  val copy = I
    1.20 +  val extend = I
    1.21 +  fun merge _ _ = NONE
    1.22 +)
    1.23 +
    1.24 +structure Import :> IMPORT =
    1.25 +struct
    1.26 +
    1.27 +val debug = ref false
    1.28 +fun message s = if !debug then writeln s else ()
    1.29 +
    1.30 +fun import_tac ctxt (thyname, thmname) =
    1.31 +    if ! quick_and_dirty
    1.32 +    then SkipProof.cheat_tac (ProofContext.theory_of ctxt)
    1.33 +    else
    1.34 +     fn th =>
    1.35 +        let
    1.36 +            val thy = ProofContext.theory_of ctxt
    1.37 +            val prem = hd (prems_of th)
    1.38 +            val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname)
    1.39 +            val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem)
    1.40 +            val int_thms = case ImportData.get thy of
    1.41 +                               NONE => fst (Replay.setup_int_thms thyname thy)
    1.42 +                             | SOME a => a
    1.43 +            val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
    1.44 +            val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
    1.45 +            val thm = snd (ProofKernel.to_isa_thm hol4thm)
    1.46 +            val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
    1.47 +            val thm = equal_elim rew thm
    1.48 +            val prew = ProofKernel.rewrite_hol4_term prem thy
    1.49 +            val prem' = #2 (Logic.dest_equals (prop_of prew))
    1.50 +            val _ = message ("Import proved " ^ Display.string_of_thm thm)
    1.51 +            val thm = ProofKernel.disambiguate_frees thm
    1.52 +            val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
    1.53 +        in
    1.54 +            case Shuffler.set_prop thy prem' [("",thm)] of
    1.55 +                SOME (_,thm) =>
    1.56 +                let
    1.57 +                    val _ = if prem' aconv (prop_of thm)
    1.58 +                            then message "import: Terms match up"
    1.59 +                            else message "import: Terms DO NOT match up"
    1.60 +                    val thm' = equal_elim (symmetric prew) thm
    1.61 +                    val res = bicompose true (false,thm',0) 1 th
    1.62 +                in
    1.63 +                    res
    1.64 +                end
    1.65 +              | NONE => (message "import: set_prop didn't succeed"; no_tac th)
    1.66 +        end
    1.67 +
    1.68 +val setup = Method.setup @{binding import}
    1.69 +  (Scan.lift (Args.name -- Args.name) >>
    1.70 +    (fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg)))
    1.71 +  "import HOL4 theorem"
    1.72 +
    1.73 +end
    1.74 +