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