Added HOLLight support to importer.
authorobua
Mon Sep 12 15:52:00 2005 +0200 (2005-09-12)
changeset 17322781abf7011e6
parent 17321 227f1f5c3959
child 17323 2fc68de9de1f
Added HOLLight support to importer.
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/Generate-HOLLight/ROOT.ML
src/HOL/Import/HOL4Setup.thy
src/HOL/Import/HOLLightCompat.thy
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Mon Sep 12 15:52:00 2005 +0200
     1.3 @@ -0,0 +1,88 @@
     1.4 +(*  Title:      HOL/Import/Generate-HOLLight/GenHOLLight.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Steven Obua (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9 +theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
    1.10 +
    1.11 +ML {* reset ProofKernel.debug; *}
    1.12 +ML {* reset Shuffler.debug; *}
    1.13 +ML {* set show_types; set show_sorts; *}
    1.14 +
    1.15 +;import_segment "hollight";
    1.16 +
    1.17 +setup_dump "../HOLLight" "HOLLight";
    1.18 +
    1.19 +append_dump {*theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":*};
    1.20 +
    1.21 +;import_theory hollight;
    1.22 +
    1.23 +ignore_thms
    1.24 +  TYDEF_1
    1.25 +  DEF_one
    1.26 +  TYDEF_prod
    1.27 +  TYDEF_num
    1.28 +  IND_SUC_0_EXISTS
    1.29 +  DEF__0
    1.30 +  DEF_SUC
    1.31 +  DEF_IND_SUC
    1.32 +  DEF_IND_0
    1.33 +  DEF_NUM_REP
    1.34 +  TYDEF_sum
    1.35 +  DEF_INL
    1.36 +  DEF_INR;
    1.37 +
    1.38 +type_maps
    1.39 +  ind > Nat.ind
    1.40 +  bool > bool
    1.41 +  fun > fun
    1.42 +  N_1 >  Product_Type.unit
    1.43 +  prod > "*"
    1.44 +  num > nat
    1.45 +  sum > "+";
    1.46 +
    1.47 +const_maps
    1.48 +  T > True
    1.49 +  F > False
    1.50 +  ONE_ONE > HOL4Setup.ONE_ONE
    1.51 +  ONTO    > Fun.surj
    1.52 +  "=" > "op ="
    1.53 +  "==>" > "op -->"
    1.54 +  "/\\" > "op &"
    1.55 +  "\\/" > "op |"
    1.56 +  "!" > All
    1.57 +  "?" > Ex
    1.58 +  "?!" > Ex1
    1.59 +  "~" > Not
    1.60 +  o > Fun.comp
    1.61 +  "@" > "Hilbert_Choice.Eps"
    1.62 +  I > Fun.id
    1.63 +  one > Product_Type.Unity
    1.64 +  LET > HOL4Compat.LET
    1.65 +  mk_pair > Product_Type.Pair_Rep
    1.66 +  "," > Pair
    1.67 +  REP_prod > Rep_Prod
    1.68 +  ABS_prod > Abs_Prod
    1.69 +  FST > fst
    1.70 +  SND > snd
    1.71 +  "_0" > 0 :: nat
    1.72 +  SUC > Suc
    1.73 +  PRE > HOLLightCompat.Pred
    1.74 +  NUMERAL > HOL4Compat.NUMERAL
    1.75 +  "+" > "op +" :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
    1.76 +  "*" > "op *" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.77 +  "-" > "op -" :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.78 +  BIT0 > HOLLightCompat.NUMERAL_BIT0
    1.79 +  BIT1 > HOL4Compat.NUMERAL_BIT1
    1.80 +  INL > Sum_Type.Inl
    1.81 +  INR > Sum_Type.Inr;
    1.82 +
    1.83 +end_import;
    1.84 +
    1.85 +append_dump "end";
    1.86 +
    1.87 +flush_dump;
    1.88 +
    1.89 +import_segment "";
    1.90 +
    1.91 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Import/Generate-HOLLight/ROOT.ML	Mon Sep 12 15:52:00 2005 +0200
     2.3 @@ -0,0 +1,6 @@
     2.4 +(*  Title:      HOL/Import/Generate-HOLLight/ROOT.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
     2.7 +*)
     2.8 +
     2.9 +use_thy "GenHOLLight";
     3.1 --- a/src/HOL/Import/HOL4Setup.thy	Mon Sep 12 12:11:17 2005 +0200
     3.2 +++ b/src/HOL/Import/HOL4Setup.thy	Mon Sep 12 15:52:00 2005 +0200
     3.3 @@ -24,19 +24,18 @@
     3.4  
     3.5  defs
     3.6    ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
     3.7 -  ONTO_DEF   : "ONTO f == ALL y. EX x. y = f x"
     3.8  
     3.9  lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
    3.10    by (simp add: ONE_ONE_DEF inj_on_def)
    3.11  
    3.12 -lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(ONTO f))"
    3.13 +lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"
    3.14  proof (rule exI,safe)
    3.15    show "inj Suc_Rep"
    3.16      by (rule inj_Suc_Rep)
    3.17  next
    3.18 -  assume "ONTO Suc_Rep"
    3.19 +  assume "surj Suc_Rep"
    3.20    hence "ALL y. EX x. y = Suc_Rep x"
    3.21 -    by (simp add: ONTO_DEF surj_def)
    3.22 +    by (simp add: surj_def)
    3.23    hence "EX x. Zero_Rep = Suc_Rep x"
    3.24      by (rule spec)
    3.25    thus False
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Import/HOLLightCompat.thy	Mon Sep 12 15:52:00 2005 +0200
     4.3 @@ -0,0 +1,96 @@
     4.4 +(*  Title:      HOL/Import/HOLLightCompat.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
     4.7 +*)
     4.8 +
     4.9 +theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
    4.10 +
    4.11 +lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)"
    4.12 +  by auto;
    4.13 +
    4.14 +lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2"
    4.15 +  by simp
    4.16 +
    4.17 +lemma light_and_def: "(t1 & t2) = ((%f. f t1 t2::bool) = (%f. f True True))"
    4.18 +proof auto
    4.19 +  assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
    4.20 +  have b: "(%(x::bool) (y::bool). x) = (%x y. x)" ..
    4.21 +  with a
    4.22 +  have "t1 = True"
    4.23 +    by (rule comb_rule)
    4.24 +  thus t1
    4.25 +    by simp
    4.26 +next
    4.27 +  assume a: "(%f. f t1 t2::bool) = (%f. f True True)"
    4.28 +  have b: "(%(x::bool) (y::bool). y) = (%x y. y)" ..
    4.29 +  with a
    4.30 +  have "t2 = True"
    4.31 +    by (rule comb_rule)
    4.32 +  thus t2
    4.33 +    by simp
    4.34 +qed
    4.35 +
    4.36 +constdefs
    4.37 +   Pred :: "nat \<Rightarrow> nat"
    4.38 +   "Pred n \<equiv> n - (Suc 0)"
    4.39 +
    4.40 +lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))"
    4.41 +  apply (rule some_equality[symmetric])
    4.42 +  apply (simp add: Pred_def)
    4.43 +  apply (rule ext)
    4.44 +  apply (induct_tac x)
    4.45 +  apply (auto simp add: Pred_def)
    4.46 +  done
    4.47 +
    4.48 +lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def)
    4.49 +
    4.50 +lemma REP_ABS_PAIR: "\<forall> x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y"
    4.51 +  apply (subst Abs_Prod_inverse)
    4.52 +  apply (auto simp add: Prod_def)
    4.53 +  done
    4.54 +
    4.55 +lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))"
    4.56 +  apply (rule ext, rule someI2)
    4.57 +  apply (auto intro: fst_conv[symmetric])
    4.58 +  done
    4.59 +
    4.60 +lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))"
    4.61 +  apply (rule ext, rule someI2)
    4.62 +  apply (auto intro: snd_conv[symmetric])
    4.63 +  done
    4.64 +
    4.65 +lemma add_altdef: "op + = (SOME add. (ALL n. add 0 n = n) & (ALL m n. add (Suc m) n = Suc (add m n)))"
    4.66 +  apply (rule some_equality[symmetric])
    4.67 +  apply auto
    4.68 +  apply (rule ext)+
    4.69 +  apply (induct_tac x)
    4.70 +  apply auto
    4.71 +  done
    4.72 +
    4.73 +lemma mult_altdef: "op * = (SOME mult. (ALL n. mult 0 n = 0) & (ALL m n. mult (Suc m) n = mult m n + n))"
    4.74 +  apply (rule some_equality[symmetric])
    4.75 +  apply auto
    4.76 +  apply (rule ext)+
    4.77 +  apply (induct_tac x)
    4.78 +  apply auto
    4.79 +  done
    4.80 +
    4.81 +lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))"
    4.82 +  apply (simp add: Pred_def)
    4.83 +  apply (rule some_equality[symmetric])
    4.84 +  apply auto
    4.85 +  apply (rule ext)+
    4.86 +  apply (induct_tac xa)
    4.87 +  apply auto
    4.88 +  done
    4.89 +
    4.90 +constdefs
    4.91 +  NUMERAL_BIT0 :: "nat \<Rightarrow> nat"
    4.92 +  "NUMERAL_BIT0 n \<equiv> n + n"
    4.93 +
    4.94 +lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)"
    4.95 +  by (simp add: NUMERAL_BIT1_def)
    4.96 +
    4.97 +
    4.98 +
    4.99 +end
     5.1 --- a/src/HOL/Import/hol4rews.ML	Mon Sep 12 12:11:17 2005 +0200
     5.2 +++ b/src/HOL/Import/hol4rews.ML	Mon Sep 12 15:52:00 2005 +0200
     5.3 @@ -417,9 +417,11 @@
     5.4  fun add_hol4_type_mapping bthy bconst internal isaconst thy =
     5.5      let
     5.6  	val curmaps = HOL4TypeMaps.get thy
     5.7 -	val _ = message ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
     5.8 +	val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
     5.9  	val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst)),curmaps)
    5.10 -	val upd_thy = HOL4TypeMaps.put newmaps thy
    5.11 +               handle x => let val (internal, isaconst') = the (StringPair.lookup (curmaps, (bthy, bconst))) in
    5.12 +                      warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
    5.13 +        val upd_thy = HOL4TypeMaps.put newmaps thy
    5.14      in
    5.15  	upd_thy
    5.16      end;
     6.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Sep 12 12:11:17 2005 +0200
     6.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Sep 12 15:52:00 2005 +0200
     6.3 @@ -109,6 +109,8 @@
     6.4      val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm
     6.5      val new_axiom : string -> term -> theory -> theory * thm
     6.6  
     6.7 +    val prin : term -> unit 
     6.8 +
     6.9  end
    6.10  
    6.11  structure ProofKernel :> ProofKernel =
    6.12 @@ -217,8 +219,8 @@
    6.13  val prin = Library.setmp print_mode [] prin
    6.14  fun pth (HOLThm(ren,thm)) =
    6.15      let
    6.16 -	val _ = writeln "Renaming:"
    6.17 -	val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren
    6.18 +	(*val _ = writeln "Renaming:"
    6.19 +	val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*)
    6.20  	val _ = prth thm
    6.21      in
    6.22  	()
    6.23 @@ -403,11 +405,15 @@
    6.24  
    6.25  fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
    6.26  
    6.27 -local
    6.28 -    fun get_type sg thyname name =
    6.29 -	case Sign.const_type sg name of
    6.30 -	    SOME ty => ty
    6.31 -	  | NONE => raise ERR "get_type" (name ^ ": No such constant")
    6.32 +local 
    6.33 +    (* fun get_const sg thyname name = 
    6.34 +       (case term_of (read_cterm sg (name, TypeInfer.logicT)) of
    6.35 +          c as Const _ => c)
    6.36 +       handle _ => raise ERR "get_type" (name ^ ": No such constant")*)
    6.37 +      fun get_const sg thyname name = 
    6.38 +       (case Sign.const_type sg name of
    6.39 +          SOME ty => Const (name, ty)
    6.40 +        | NONE => raise ERR "get_type" (name ^ ": No such constant"))
    6.41  in
    6.42  fun prim_mk_const thy Thy Nam =
    6.43      let
    6.44 @@ -416,7 +422,7 @@
    6.45      in
    6.46  	case StringPair.lookup(cmaps,(Thy,Nam)) of
    6.47  	    SOME(_,_,SOME ty) => Const(name,ty)
    6.48 -	  | _ => Const(name,get_type (sign_of thy) Thy name)
    6.49 +	  | _ => get_const (sign_of thy) Thy name
    6.50      end
    6.51  end
    6.52  
    6.53 @@ -447,8 +453,24 @@
    6.54  	s |> no_beg_underscore
    6.55      end
    6.56  
    6.57 +val ty_num_prefix = "N_"
    6.58 +
    6.59 +fun startsWithDigit s = Char.isDigit (hd (String.explode s))
    6.60 +
    6.61 +fun protect_tyname tyn = 
    6.62 +  let
    6.63 +    val tyn' = 
    6.64 +      if String.isPrefix ty_num_prefix tyn then raise (ERR "conv_ty_name" ("type name '"^tyn^"' is reserved")) else 
    6.65 +      (if startsWithDigit tyn then ty_num_prefix^tyn else tyn)
    6.66 +  in
    6.67 +    tyn'
    6.68 +  end
    6.69 +
    6.70 +
    6.71 +
    6.72  structure TypeNet =
    6.73  struct
    6.74 +
    6.75  fun get_type_from_index thy thyname types is =
    6.76      case Int.fromString is of
    6.77  	SOME i => (case Array.sub(types,i) of
    6.78 @@ -468,13 +490,13 @@
    6.79  	  | gtfx (Elem("tyc",atts,[])) =
    6.80  	    mk_thy_type thy
    6.81  			(get_segment thyname atts)
    6.82 -			(get_name atts)
    6.83 +			(protect_tyname (get_name atts))
    6.84  			[]
    6.85  	  | gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s)
    6.86  	  | gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) =
    6.87  	    mk_thy_type thy
    6.88  			(get_segment thyname atts)
    6.89 -			(get_name atts)
    6.90 +			(protect_tyname (get_name atts))
    6.91  			(map gtfx tys)
    6.92  	  | gtfx _ = raise ERR "get_type" "Bad type"
    6.93      in
    6.94 @@ -497,6 +519,7 @@
    6.95  
    6.96  structure TermNet =
    6.97  struct
    6.98 +
    6.99  fun get_term_from_index thy thyname types terms is =
   6.100      case Int.fromString is of
   6.101  	SOME i => (case Array.sub(terms,i) of
   6.102 @@ -663,10 +686,10 @@
   6.103  		val P = xml_to_term xP
   6.104  		val t = xml_to_term xt
   6.105  	    in
   6.106 -		mk_proof (PTyIntro(seg,name,abs_name,rep_name,P,t,x2p p))
   6.107 +		mk_proof (PTyIntro(seg,protect_tyname name,abs_name,rep_name,P,t,x2p p))
   6.108  	    end
   6.109  	  | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =
   6.110 -	    mk_proof (PTyDef(seg,name,x2p p))
   6.111 +	    mk_proof (PTyDef(seg,protect_tyname name,x2p p))
   6.112  	  | x2p (xml as Elem("poracle",[],chldr)) =
   6.113  	    let
   6.114  		val (oracles,terms) = Library.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
   6.115 @@ -834,12 +857,33 @@
   6.116  	x2p prf
   6.117      end
   6.118  
   6.119 +fun import_proof_concl thyname thmname thy = 
   6.120 +    let
   6.121 +	val is = TextIO.openIn(proof_file_name thyname thmname thy)
   6.122 +	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
   6.123 +	val _ = TextIO.closeIn is
   6.124 +    in 
   6.125 +	case proof_xml of
   6.126 +	    Elem("proof",[],xtypes::xterms::prf::rest) =>
   6.127 +	    let
   6.128 +		val types = TypeNet.input_types thyname xtypes
   6.129 +		val terms = TermNet.input_terms thyname types xterms
   6.130 +                fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm               
   6.131 +	    in
   6.132 +		case rest of
   6.133 +		    [] => NONE
   6.134 +		  | [xtm] => SOME (f xtm)
   6.135 +		  | _ => raise ERR "import_proof" "Bad argument list"
   6.136 +	    end
   6.137 +	  | _ => raise ERR "import_proof" "Bad proof"
   6.138 +    end
   6.139 +
   6.140  fun import_proof thyname thmname thy =
   6.141      let
   6.142  	val is = TextIO.openIn(proof_file_name thyname thmname thy)
   6.143  	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
   6.144  	val _ = TextIO.closeIn is
   6.145 -    in
   6.146 +    in 
   6.147  	case proof_xml of
   6.148  	    Elem("proof",[],xtypes::xterms::prf::rest) =>
   6.149  	    let
   6.150 @@ -1037,75 +1081,20 @@
   6.151  fun name_of_var (Free(vname,_)) = vname
   6.152    | name_of_var _ = raise ERR "name_of_var" "Not a variable"
   6.153  
   6.154 -fun disamb_helper {vars,rens} tm =
   6.155 -    let
   6.156 -	val varstm = collect_vars tm
   6.157 -	fun process (v as Free(vname,ty),(vars,rens,inst)) =
   6.158 -	    if v mem vars
   6.159 -	    then (vars,rens,inst)
   6.160 -	    else (case try (Lib.assoc v) rens of
   6.161 -		      SOME vnew => (vars,rens,(v,vnew)::inst)
   6.162 -		    | NONE => if exists (fn Free(vname',_) => vname = vname' | _ => raise ERR "disamb_helper" "Bad varlist") vars
   6.163 -			      then
   6.164 -				  let
   6.165 -				      val tmnames = map name_of_var varstm
   6.166 -				      val varnames = map name_of_var vars
   6.167 -				      val (dom,rng) = ListPair.unzip rens
   6.168 -				      val rensnames = (map name_of_var dom) @ (map name_of_var rng)
   6.169 -				      val instnames = map name_of_var (snd (ListPair.unzip inst))
   6.170 -				      val allnames = tmnames @ varnames @ rensnames @ instnames
   6.171 -				      val vnewname = Term.variant allnames vname
   6.172 -				      val vnew = Free(vnewname,ty)
   6.173 -				  in
   6.174 -				      (vars,(v,vnew)::rens,(v,vnew)::inst)
   6.175 -				  end
   6.176 -			      else (v::vars,rens,inst))
   6.177 -	  | process _ = raise ERR "disamb_helper" "Internal error"
   6.178 -
   6.179 -	val (vars',rens',inst) =
   6.180 -	    foldr process (vars,rens,[]) varstm
   6.181 -    in
   6.182 -	({vars=vars',rens=rens'},inst)
   6.183 -    end
   6.184 -
   6.185 -fun disamb_term_from info tm =
   6.186 -    let
   6.187 -	val (info',inst) = disamb_helper info tm
   6.188 -    in
   6.189 -	(info',apply_inst_term inst tm)
   6.190 -    end
   6.191 +fun disamb_term_from info tm = (info, tm)
   6.192  
   6.193  fun swap (x,y) = (y,x)
   6.194  
   6.195 -fun has_ren (HOLThm([],_)) = false
   6.196 -  | has_ren _ = true
   6.197 +fun has_ren (HOLThm _) = false
   6.198  
   6.199  fun prinfo {vars,rens} = (writeln "Vars:";
   6.200  			  app prin vars;
   6.201  			  writeln "Renaming:";
   6.202  			  app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens)
   6.203  
   6.204 -fun disamb_thm_from info (hth as HOLThm(rens,thm)) =
   6.205 -    let
   6.206 -	val inv_rens = map swap rens
   6.207 -	val orig_thm = apply_inst_term inv_rens (prop_of thm)
   6.208 -	val (info',inst) = disamb_helper info orig_thm
   6.209 -	val rens' = map (apsnd (apply_inst_term inst)) inv_rens
   6.210 -	val (dom,rng) = ListPair.unzip (rens' @ inst)
   6.211 -	val sg = sign_of_thm thm
   6.212 -	val thm' = mk_INST (map (cterm_of sg) dom) (map (cterm_of sg) rng) thm
   6.213 -    in
   6.214 -	(info',thm')
   6.215 -    end
   6.216 +fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm)
   6.217  
   6.218 -fun disamb_terms_from info tms =
   6.219 -    foldr (fn (tm,(info,tms)) =>
   6.220 -	      let
   6.221 -		  val (info',tm') = disamb_term_from info tm
   6.222 -	      in
   6.223 -		  (info',tm'::tms)
   6.224 -	      end)
   6.225 -	  (info,[]) tms
   6.226 +fun disamb_terms_from info tms = (info, tms)
   6.227  
   6.228  fun disamb_thms_from info hthms =
   6.229      foldr (fn (hthm,(info,thms)) =>
   6.230 @@ -1121,28 +1110,7 @@
   6.231  fun disamb_thm thm   = disamb_thm_from disamb_info_empty thm
   6.232  fun disamb_thms thms = disamb_thms_from disamb_info_empty thms
   6.233  
   6.234 -fun norm_hthm sg (hth as HOLThm([],_)) = hth
   6.235 -  | norm_hthm sg (hth as HOLThm(rens,th)) =
   6.236 -    let
   6.237 -	val vars = collect_vars (prop_of th)
   6.238 -	val (rens',inst,_) =
   6.239 -	    foldr (fn((ren as (vold as Free(vname,_),vnew)),
   6.240 -		      (rens,inst,vars)) =>
   6.241 -		     (case Library.find_first (fn Free(v,_) => v = vname | _ => false) vars of
   6.242 -			  SOME v' => if v' = vold
   6.243 -				     then (rens,(vnew,vold)::inst,vold::vars)
   6.244 -				     else (ren::rens,(vold,vnew)::inst,vnew::vars)
   6.245 -			| NONE => (rens,(vnew,vold)::inst,vold::vars))
   6.246 -		   | _ => raise ERR "norm_hthm" "Internal error")
   6.247 -		  ([],[],vars) rens
   6.248 -	val (dom,rng) = ListPair.unzip inst
   6.249 -	val th' = mk_INST (map (cterm_of sg) dom) (map (cterm_of sg) rng) th
   6.250 -	val nvars = collect_vars (prop_of th')
   6.251 -	val rens' = List.filter (fn(_,v) => v mem nvars) rens
   6.252 -	val res = HOLThm(rens',th')
   6.253 -    in
   6.254 -	res
   6.255 -    end
   6.256 +fun norm_hthm sg (hth as HOLThm _) = hth
   6.257  
   6.258  (* End of disambiguating code *)
   6.259  
   6.260 @@ -1213,7 +1181,6 @@
   6.261  	Thm.transfer sg (Simplifier.full_rewrite hol4ss (cterm_of sg t))
   6.262      end
   6.263  
   6.264 -
   6.265  fun get_isabelle_thm thyname thmname hol4conc thy =
   6.266      let
   6.267  	val _ = message "get_isabelle_thm called..."
   6.268 @@ -1275,11 +1242,35 @@
   6.269      end
   6.270      handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE))
   6.271  
   6.272 +fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
   6.273 +  let
   6.274 +    val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
   6.275 +    fun warn () =
   6.276 +        let
   6.277 +            val sg = sign_of thy		     
   6.278 +	    val (info,hol4conc') = disamb_term hol4conc
   6.279 +	    val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
   6.280 +	in
   6.281 +	    case concl_of i2h_conc of
   6.282 +		Const("==",_) $ lhs $ _ => 
   6.283 +		(warning ("Failed lookup of theorem '"^thmname^"':");
   6.284 +	         writeln "Original conclusion:";
   6.285 +		 prin hol4conc';
   6.286 +		 writeln "Modified conclusion:";
   6.287 +		 prin lhs)
   6.288 +	      | _ => ()
   6.289 +	end
   6.290 +  in
   6.291 +      case b of 
   6.292 +	  NONE => (warn () handle _ => (); (a,b))
   6.293 +	| _ => (a, b)
   6.294 +  end 
   6.295 +
   6.296  fun get_thm thyname thmname thy =
   6.297      case get_hol4_thm thyname thmname thy of
   6.298  	SOME hth => (thy,SOME hth)
   6.299 -      | NONE => ((case fst (import_proof thyname thmname thy) of
   6.300 -		      SOME f => get_isabelle_thm thyname thmname (f thy) thy
   6.301 +      | NONE => ((case import_proof_concl thyname thmname thy of
   6.302 +		      SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
   6.303  		    | NONE => (message "No conclusion"; (thy,NONE)))
   6.304  		 handle e as IO.Io _ => (message "IO exception"; (thy,NONE))
   6.305  		      | e as PK _ => (message "PK exception"; (thy,NONE)))
   6.306 @@ -1295,7 +1286,7 @@
   6.307  	val (thmname,thy') = get_defname thyname constname thy
   6.308  	val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname)
   6.309      in
   6.310 -	get_isabelle_thm thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy'
   6.311 +	get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy'
   6.312      end
   6.313  
   6.314  fun get_axiom thyname axname thy =
   6.315 @@ -1407,7 +1398,7 @@
   6.316  	(thy,res)
   6.317      end
   6.318  
   6.319 -fun mk_EQ_MP th1 th2 = [beta_eta_thm th1,beta_eta_thm th2] MRS eqmp_thm
   6.320 +fun mk_EQ_MP th1 th2 = [beta_eta_thm th1, beta_eta_thm th2] MRS eqmp_thm
   6.321  
   6.322  fun EQ_MP hth1 hth2 thy =
   6.323      let
   6.324 @@ -2086,7 +2077,7 @@
   6.325  	Replaying _ => (thy,hth)
   6.326        | _ => 
   6.327  	let
   6.328 -	    val _ = message "TYPE_INTRO:"
   6.329 +            val _ = message "TYPE_INTRO:"
   6.330  	    val _ = if_debug pth hth
   6.331  	    val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")")
   6.332  	    val (HOLThm(rens,td_th)) = norm_hthm (sign_of thy) hth
   6.333 @@ -2105,13 +2096,14 @@
   6.334  	    val tsyn = mk_syn thy tycname
   6.335  	    val typ = (tycname,tnames,tsyn)
   6.336  	    val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
   6.337 -				      
   6.338  	    val th3 = (#type_definition typedef_info) RS typedef_hol2hollight
   6.339 -
   6.340 +            val _ = message "step 1"
   6.341  	    val th4 = Drule.freeze_all th3
   6.342 +            val _ = message "step 2"
   6.343  	    val fulltyname = Sign.intern_type (sign_of thy') tycname
   6.344 -	    val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
   6.345 -
   6.346 +	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
   6.347 +            val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
   6.348 +            val _ = message "step 4"
   6.349  	    val sg = sign_of thy''
   6.350  	    val (hth' as HOLThm args) = norm_hthm sg (HOLThm(rens,th4))
   6.351  	    val _ = if #maxidx (rep_thm th4) <> ~1
   6.352 @@ -2120,7 +2112,7 @@
   6.353  	    val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
   6.354  		    else ()
   6.355  	    val thy4 = add_hol4_pending thyname thmname args thy''
   6.356 -
   6.357 +	   
   6.358  	    val sg = sign_of thy4
   6.359  	    val P' = #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4)))
   6.360  	    val c   =
   6.361 @@ -2129,7 +2121,7 @@
   6.362  		in
   6.363  		    Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
   6.364  		end
   6.365 -
   6.366 +	    
   6.367  	    val tnames_string = if null tnames
   6.368  				then ""
   6.369  				else "(" ^ (commafy tnames) ^ ") "
   6.370 @@ -2147,4 +2139,6 @@
   6.371  	handle e => (message "exception in type_introduction"; print_exn e)
   6.372  end
   6.373  
   6.374 +val prin = prin
   6.375 +
   6.376  end
     7.1 --- a/src/HOL/Import/replay.ML	Mon Sep 12 12:11:17 2005 +0200
     7.2 +++ b/src/HOL/Import/replay.ML	Mon Sep 12 15:52:00 2005 +0200
     7.3 @@ -61,7 +61,7 @@
     7.4  	       | (thy',NONE) => 
     7.5  		 if seg = thyname
     7.6  		 then P.new_definition seg name rhs thy'
     7.7 -		 else raise ERR "replay_proof" "Too late for term definition")
     7.8 +		 else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
     7.9  	  | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    7.10  	  | rp (PSpec(prf,tm)) thy =
    7.11  	    let
    7.12 @@ -234,6 +234,7 @@
    7.13  						    val (f_opt,prf) = import_proof thyname' thmname thy'
    7.14  						    val prf = prf thy'
    7.15  						    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
    7.16 +                                                    val _ = writeln ("Successfully finished replaying "^thmname^" !")
    7.17  						in
    7.18  						    case content_of prf of
    7.19  							PTmSpec _ => (thy',th)