src/HOL/Import/import_package.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14848 83f1dc18f1f1
child 15531 08c8dad8e399
permissions -rw-r--r--
import -> imports
skalberg@14620
     1
(*  Title:      HOL/Import/import_package.ML
skalberg@14620
     2
    ID:         $Id$
skalberg@14620
     3
    Author:     Sebastian Skalberg (TU Muenchen)
skalberg@14620
     4
*)
skalberg@14620
     5
skalberg@14516
     6
signature IMPORT_PACKAGE =
skalberg@14516
     7
sig
skalberg@14516
     8
    val import_meth: Args.src -> Proof.context -> Proof.method
skalberg@14516
     9
    val setup      : (theory -> theory) list
skalberg@14516
    10
    val debug      : bool ref
skalberg@14516
    11
end
skalberg@14516
    12
skalberg@14620
    13
structure ImportDataArgs: THEORY_DATA_ARGS =
skalberg@14620
    14
struct
skalberg@14620
    15
val name = "HOL4/import_data"
skalberg@14620
    16
type T = ProofKernel.thm option array option
skalberg@14620
    17
val empty = None
skalberg@14620
    18
val copy = I
skalberg@14620
    19
val prep_ext = I
skalberg@14620
    20
fun merge _ = None
skalberg@14620
    21
fun print sg import_segment =
skalberg@14620
    22
    Pretty.writeln (Pretty.str ("Pretty printing of importer data not implemented"))
skalberg@14620
    23
end
skalberg@14620
    24
skalberg@14620
    25
structure ImportData = TheoryDataFun(ImportDataArgs)
skalberg@14620
    26
skalberg@14516
    27
structure ImportPackage :> IMPORT_PACKAGE =
skalberg@14516
    28
struct
skalberg@14516
    29
skalberg@14516
    30
val debug = ref false
skalberg@14516
    31
fun message s = if !debug then writeln s else ()
skalberg@14516
    32
wenzelm@14848
    33
val string_of_thm = Library.setmp print_mode [] string_of_thm;
wenzelm@14848
    34
val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
skalberg@14516
    35
skalberg@14516
    36
fun import_tac (thyname,thmname) =
skalberg@14516
    37
    if !SkipProof.quick_and_dirty
skalberg@14516
    38
    then SkipProof.cheat_tac
skalberg@14516
    39
    else
skalberg@14516
    40
     fn thy =>
skalberg@14516
    41
     fn th =>
skalberg@14516
    42
	let
skalberg@14516
    43
	    val sg = sign_of_thm th
skalberg@14516
    44
	    val prem = hd (prems_of th)
skalberg@14516
    45
	    val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
skalberg@14620
    46
	    val int_thms = case ImportData.get thy of
skalberg@14620
    47
			       None => fst (Replay.setup_int_thms thyname thy)
skalberg@14620
    48
			     | Some a => a
skalberg@14516
    49
	    val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
skalberg@14516
    50
	    val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
skalberg@14516
    51
	    val thm = snd (ProofKernel.to_isa_thm hol4thm)
skalberg@14516
    52
	    val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
skalberg@14516
    53
	    val thm = equal_elim rew thm
skalberg@14516
    54
	    val prew = ProofKernel.rewrite_hol4_term prem thy
skalberg@14516
    55
	    val prem' = #2 (Logic.dest_equals (prop_of prew))
skalberg@14516
    56
	    val _ = message ("Import proved " ^ (string_of_thm thm))  
skalberg@14516
    57
	in
skalberg@14516
    58
	    case Shuffler.set_prop thy prem' [("",thm)] of
skalberg@14516
    59
		Some (_,thm) =>
skalberg@14516
    60
		let
skalberg@14516
    61
		    val _ = if prem' aconv (prop_of thm)
skalberg@14516
    62
			    then message "import: Terms match up"
skalberg@14516
    63
			    else message "import: Terms DO NOT match up"
skalberg@14516
    64
		    val thm' = equal_elim (symmetric prew) thm
skalberg@14516
    65
		    val res = bicompose true (false,thm',0) 1 th
skalberg@14516
    66
		in
skalberg@14516
    67
		    res
skalberg@14516
    68
		end
skalberg@14516
    69
	      | None => (message "import: set_prop didn't succeed"; no_tac th)
skalberg@14516
    70
	end
skalberg@14516
    71
	
skalberg@14516
    72
val import_meth = Method.simple_args (Args.name -- Args.name)
skalberg@14516
    73
		  (fn arg =>
skalberg@14516
    74
		   fn ctxt =>
skalberg@14516
    75
		      let
skalberg@14516
    76
			  val thy = ProofContext.theory_of ctxt
skalberg@14516
    77
		      in
skalberg@14516
    78
			  Method.SIMPLE_METHOD (import_tac arg thy)
skalberg@14516
    79
		      end)
skalberg@14516
    80
skalberg@14620
    81
val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init]
skalberg@14516
    82
end