src/HOL/Import/import_package.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17657 2f5f595eb618
child 21590 ef7278f553eb
permissions -rw-r--r--
setup: theory -> theory;
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
wenzelm@15703
     8
    val import_meth: Method.src -> Proof.context -> Proof.method
wenzelm@18708
     9
    val setup      : theory -> theory
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@15531
    17
val empty = NONE
skalberg@14620
    18
val copy = I
wenzelm@16424
    19
val extend = I
wenzelm@16424
    20
fun merge _ _ = NONE
wenzelm@16424
    21
fun print _ _ = ()
skalberg@14620
    22
end
skalberg@14620
    23
skalberg@14620
    24
structure ImportData = TheoryDataFun(ImportDataArgs)
skalberg@14620
    25
skalberg@14516
    26
structure ImportPackage :> IMPORT_PACKAGE =
skalberg@14516
    27
struct
skalberg@14516
    28
skalberg@14516
    29
val debug = ref false
skalberg@14516
    30
fun message s = if !debug then writeln s else ()
skalberg@14516
    31
wenzelm@14848
    32
val string_of_thm = Library.setmp print_mode [] string_of_thm;
wenzelm@14848
    33
val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
skalberg@14516
    34
skalberg@14516
    35
fun import_tac (thyname,thmname) =
wenzelm@17370
    36
    if ! quick_and_dirty
skalberg@14516
    37
    then SkipProof.cheat_tac
skalberg@14516
    38
    else
skalberg@14516
    39
     fn thy =>
skalberg@14516
    40
     fn th =>
skalberg@14516
    41
	let
obua@17490
    42
            val sg = sign_of_thm th
skalberg@14516
    43
	    val prem = hd (prems_of th)
obua@17644
    44
            val _ = message ("Import_tac: thyname="^thyname^", thmname="^thmname)
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@15531
    47
			       NONE => fst (Replay.setup_int_thms thyname thy)
skalberg@15531
    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))
obua@17652
    56
            val _ = message ("Import proved " ^ (string_of_thm thm))    
wenzelm@17657
    57
            val thm = ProofKernel.disambiguate_frees thm
obua@17652
    58
	    val _ = message ("Disambiguate: " ^ (string_of_thm thm))  
skalberg@14516
    59
	in
skalberg@14516
    60
	    case Shuffler.set_prop thy prem' [("",thm)] of
skalberg@15531
    61
		SOME (_,thm) =>
skalberg@14516
    62
		let
skalberg@14516
    63
		    val _ = if prem' aconv (prop_of thm)
skalberg@14516
    64
			    then message "import: Terms match up"
skalberg@14516
    65
			    else message "import: Terms DO NOT match up"
skalberg@14516
    66
		    val thm' = equal_elim (symmetric prew) thm
skalberg@14516
    67
		    val res = bicompose true (false,thm',0) 1 th
skalberg@14516
    68
		in
skalberg@14516
    69
		    res
skalberg@14516
    70
		end
skalberg@15531
    71
	      | NONE => (message "import: set_prop didn't succeed"; no_tac th)
skalberg@14516
    72
	end
skalberg@14516
    73
	
skalberg@14516
    74
val import_meth = Method.simple_args (Args.name -- Args.name)
skalberg@14516
    75
		  (fn arg =>
skalberg@14516
    76
		   fn ctxt =>
skalberg@14516
    77
		      let
skalberg@14516
    78
			  val thy = ProofContext.theory_of ctxt
skalberg@14516
    79
		      in
skalberg@14516
    80
			  Method.SIMPLE_METHOD (import_tac arg thy)
skalberg@14516
    81
		      end)
skalberg@14516
    82
wenzelm@18708
    83
val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
skalberg@14516
    84
end
wenzelm@15707
    85