# HG changeset patch # User obua # Date 1126533120 -7200 # Node ID 781abf7011e6efd2b7bf193e45bb4fe22395b751 # Parent 227f1f5c395913f7137f471281eaa5c563d74abe Added HOLLight support to importer. diff -r 227f1f5c3959 -r 781abf7011e6 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Sep 12 15:52:00 2005 +0200 @@ -0,0 +1,88 @@ +(* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy + ID: $Id$ + Author: Steven Obua (TU Muenchen) +*) + +theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin; + +ML {* reset ProofKernel.debug; *} +ML {* reset Shuffler.debug; *} +ML {* set show_types; set show_sorts; *} + +;import_segment "hollight"; + +setup_dump "../HOLLight" "HOLLight"; + +append_dump {*theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":*}; + +;import_theory hollight; + +ignore_thms + TYDEF_1 + DEF_one + TYDEF_prod + TYDEF_num + IND_SUC_0_EXISTS + DEF__0 + DEF_SUC + DEF_IND_SUC + DEF_IND_0 + DEF_NUM_REP + TYDEF_sum + DEF_INL + DEF_INR; + +type_maps + ind > Nat.ind + bool > bool + fun > fun + N_1 > Product_Type.unit + prod > "*" + num > nat + sum > "+"; + +const_maps + T > True + F > False + ONE_ONE > HOL4Setup.ONE_ONE + ONTO > Fun.surj + "=" > "op =" + "==>" > "op -->" + "/\\" > "op &" + "\\/" > "op |" + "!" > All + "?" > Ex + "?!" > Ex1 + "~" > Not + o > Fun.comp + "@" > "Hilbert_Choice.Eps" + I > Fun.id + one > Product_Type.Unity + LET > HOL4Compat.LET + mk_pair > Product_Type.Pair_Rep + "," > Pair + REP_prod > Rep_Prod + ABS_prod > Abs_Prod + FST > fst + SND > snd + "_0" > 0 :: nat + SUC > Suc + PRE > HOLLightCompat.Pred + NUMERAL > HOL4Compat.NUMERAL + "+" > "op +" :: "nat \ nat \ nat" + "*" > "op *" :: "nat \ nat \ nat" + "-" > "op -" :: "nat \ nat \ nat" + BIT0 > HOLLightCompat.NUMERAL_BIT0 + BIT1 > HOL4Compat.NUMERAL_BIT1 + INL > Sum_Type.Inl + INR > Sum_Type.Inr; + +end_import; + +append_dump "end"; + +flush_dump; + +import_segment ""; + +end diff -r 227f1f5c3959 -r 781abf7011e6 src/HOL/Import/Generate-HOLLight/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Import/Generate-HOLLight/ROOT.ML Mon Sep 12 15:52:00 2005 +0200 @@ -0,0 +1,6 @@ +(* Title: HOL/Import/Generate-HOLLight/ROOT.ML + ID: $Id$ + Author: Steven Obua and Sebastian Skalberg (TU Muenchen) +*) + +use_thy "GenHOLLight"; diff -r 227f1f5c3959 -r 781abf7011e6 src/HOL/Import/HOL4Setup.thy --- a/src/HOL/Import/HOL4Setup.thy Mon Sep 12 12:11:17 2005 +0200 +++ b/src/HOL/Import/HOL4Setup.thy Mon Sep 12 15:52:00 2005 +0200 @@ -24,19 +24,18 @@ defs ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y" - ONTO_DEF : "ONTO f == ALL y. EX x. y = f x" lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV" by (simp add: ONE_ONE_DEF inj_on_def) -lemma INFINITY_AX: "EX (f::ind \ ind). (inj f & ~(ONTO f))" +lemma INFINITY_AX: "EX (f::ind \ ind). (inj f & ~(surj f))" proof (rule exI,safe) show "inj Suc_Rep" by (rule inj_Suc_Rep) next - assume "ONTO Suc_Rep" + assume "surj Suc_Rep" hence "ALL y. EX x. y = Suc_Rep x" - by (simp add: ONTO_DEF surj_def) + by (simp add: surj_def) hence "EX x. Zero_Rep = Suc_Rep x" by (rule spec) thus False diff -r 227f1f5c3959 -r 781abf7011e6 src/HOL/Import/HOLLightCompat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Import/HOLLightCompat.thy Mon Sep 12 15:52:00 2005 +0200 @@ -0,0 +1,96 @@ +(* Title: HOL/Import/HOLLightCompat.thy + ID: $Id$ + Author: Steven Obua and Sebastian Skalberg (TU Muenchen) +*) + +theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin + +lemma light_imp_def: "(t1 --> t2) = ((t1 & t2) = t1)" + by auto; + +lemma comb_rule: "[| P1 = P2 ; Q1 = Q2 |] ==> P1 Q1 = P2 Q2" + by simp + +lemma light_and_def: "(t1 & t2) = ((%f. f t1 t2::bool) = (%f. f True True))" +proof auto + assume a: "(%f. f t1 t2::bool) = (%f. f True True)" + have b: "(%(x::bool) (y::bool). x) = (%x y. x)" .. + with a + have "t1 = True" + by (rule comb_rule) + thus t1 + by simp +next + assume a: "(%f. f t1 t2::bool) = (%f. f True True)" + have b: "(%(x::bool) (y::bool). y) = (%x y. y)" .. + with a + have "t2 = True" + by (rule comb_rule) + thus t2 + by simp +qed + +constdefs + Pred :: "nat \ nat" + "Pred n \ n - (Suc 0)" + +lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))" + apply (rule some_equality[symmetric]) + apply (simp add: Pred_def) + apply (rule ext) + apply (induct_tac x) + apply (auto simp add: Pred_def) + done + +lemma NUMERAL_rew[hol4rew]: "NUMERAL x = x" by (simp add: NUMERAL_def) + +lemma REP_ABS_PAIR: "\ x y. Rep_Prod (Abs_Prod (Pair_Rep x y)) = Pair_Rep x y" + apply (subst Abs_Prod_inverse) + apply (auto simp add: Prod_def) + done + +lemma fst_altdef: "fst = (%p. SOME x. EX y. p = (x, y))" + apply (rule ext, rule someI2) + apply (auto intro: fst_conv[symmetric]) + done + +lemma snd_altdef: "snd = (%p. SOME x. EX y. p = (y, x))" + apply (rule ext, rule someI2) + apply (auto intro: snd_conv[symmetric]) + done + +lemma add_altdef: "op + = (SOME add. (ALL n. add 0 n = n) & (ALL m n. add (Suc m) n = Suc (add m n)))" + apply (rule some_equality[symmetric]) + apply auto + apply (rule ext)+ + apply (induct_tac x) + apply auto + done + +lemma mult_altdef: "op * = (SOME mult. (ALL n. mult 0 n = 0) & (ALL m n. mult (Suc m) n = mult m n + n))" + apply (rule some_equality[symmetric]) + apply auto + apply (rule ext)+ + apply (induct_tac x) + apply auto + done + +lemma sub_altdef: "op - = (SOME sub. (ALL m. sub m 0 = m) & (ALL m n. sub m (Suc n) = Pred (sub m n)))" + apply (simp add: Pred_def) + apply (rule some_equality[symmetric]) + apply auto + apply (rule ext)+ + apply (induct_tac xa) + apply auto + done + +constdefs + NUMERAL_BIT0 :: "nat \ nat" + "NUMERAL_BIT0 n \ n + n" + +lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)" + by (simp add: NUMERAL_BIT1_def) + + + +end diff -r 227f1f5c3959 -r 781abf7011e6 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Mon Sep 12 12:11:17 2005 +0200 +++ b/src/HOL/Import/hol4rews.ML Mon Sep 12 15:52:00 2005 +0200 @@ -417,9 +417,11 @@ fun add_hol4_type_mapping bthy bconst internal isaconst thy = let val curmaps = HOL4TypeMaps.get thy - val _ = message ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) + val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst)),curmaps) - val upd_thy = HOL4TypeMaps.put newmaps thy + handle x => let val (internal, isaconst') = the (StringPair.lookup (curmaps, (bthy, bconst))) in + warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end + val upd_thy = HOL4TypeMaps.put newmaps thy in upd_thy end; diff -r 227f1f5c3959 -r 781abf7011e6 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Mon Sep 12 12:11:17 2005 +0200 +++ b/src/HOL/Import/proof_kernel.ML Mon Sep 12 15:52:00 2005 +0200 @@ -109,6 +109,8 @@ val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm val new_axiom : string -> term -> theory -> theory * thm + val prin : term -> unit + end structure ProofKernel :> ProofKernel = @@ -217,8 +219,8 @@ val prin = Library.setmp print_mode [] prin fun pth (HOLThm(ren,thm)) = let - val _ = writeln "Renaming:" - val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren + (*val _ = writeln "Renaming:" + val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*) val _ = prth thm in () @@ -403,11 +405,15 @@ fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty) -local - fun get_type sg thyname name = - case Sign.const_type sg name of - SOME ty => ty - | NONE => raise ERR "get_type" (name ^ ": No such constant") +local + (* fun get_const sg thyname name = + (case term_of (read_cterm sg (name, TypeInfer.logicT)) of + c as Const _ => c) + handle _ => raise ERR "get_type" (name ^ ": No such constant")*) + fun get_const sg thyname name = + (case Sign.const_type sg name of + SOME ty => Const (name, ty) + | NONE => raise ERR "get_type" (name ^ ": No such constant")) in fun prim_mk_const thy Thy Nam = let @@ -416,7 +422,7 @@ in case StringPair.lookup(cmaps,(Thy,Nam)) of SOME(_,_,SOME ty) => Const(name,ty) - | _ => Const(name,get_type (sign_of thy) Thy name) + | _ => get_const (sign_of thy) Thy name end end @@ -447,8 +453,24 @@ s |> no_beg_underscore end +val ty_num_prefix = "N_" + +fun startsWithDigit s = Char.isDigit (hd (String.explode s)) + +fun protect_tyname tyn = + let + val tyn' = + if String.isPrefix ty_num_prefix tyn then raise (ERR "conv_ty_name" ("type name '"^tyn^"' is reserved")) else + (if startsWithDigit tyn then ty_num_prefix^tyn else tyn) + in + tyn' + end + + + structure TypeNet = struct + fun get_type_from_index thy thyname types is = case Int.fromString is of SOME i => (case Array.sub(types,i) of @@ -468,13 +490,13 @@ | gtfx (Elem("tyc",atts,[])) = mk_thy_type thy (get_segment thyname atts) - (get_name atts) + (protect_tyname (get_name atts)) [] | gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s) | gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) = mk_thy_type thy (get_segment thyname atts) - (get_name atts) + (protect_tyname (get_name atts)) (map gtfx tys) | gtfx _ = raise ERR "get_type" "Bad type" in @@ -497,6 +519,7 @@ structure TermNet = struct + fun get_term_from_index thy thyname types terms is = case Int.fromString is of SOME i => (case Array.sub(terms,i) of @@ -663,10 +686,10 @@ val P = xml_to_term xP val t = xml_to_term xt in - mk_proof (PTyIntro(seg,name,abs_name,rep_name,P,t,x2p p)) + mk_proof (PTyIntro(seg,protect_tyname name,abs_name,rep_name,P,t,x2p p)) end | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) = - mk_proof (PTyDef(seg,name,x2p p)) + mk_proof (PTyDef(seg,protect_tyname name,x2p p)) | x2p (xml as Elem("poracle",[],chldr)) = let val (oracles,terms) = Library.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr @@ -834,12 +857,33 @@ x2p prf end +fun import_proof_concl thyname thmname thy = + let + val is = TextIO.openIn(proof_file_name thyname thmname thy) + val (proof_xml,_) = scan_tag (LazySeq.of_instream is) + val _ = TextIO.closeIn is + in + case proof_xml of + Elem("proof",[],xtypes::xterms::prf::rest) => + let + val types = TypeNet.input_types thyname xtypes + val terms = TermNet.input_terms thyname types xterms + fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm + in + case rest of + [] => NONE + | [xtm] => SOME (f xtm) + | _ => raise ERR "import_proof" "Bad argument list" + end + | _ => raise ERR "import_proof" "Bad proof" + end + fun import_proof thyname thmname thy = let val is = TextIO.openIn(proof_file_name thyname thmname thy) val (proof_xml,_) = scan_tag (LazySeq.of_instream is) val _ = TextIO.closeIn is - in + in case proof_xml of Elem("proof",[],xtypes::xterms::prf::rest) => let @@ -1037,75 +1081,20 @@ fun name_of_var (Free(vname,_)) = vname | name_of_var _ = raise ERR "name_of_var" "Not a variable" -fun disamb_helper {vars,rens} tm = - let - val varstm = collect_vars tm - fun process (v as Free(vname,ty),(vars,rens,inst)) = - if v mem vars - then (vars,rens,inst) - else (case try (Lib.assoc v) rens of - SOME vnew => (vars,rens,(v,vnew)::inst) - | NONE => if exists (fn Free(vname',_) => vname = vname' | _ => raise ERR "disamb_helper" "Bad varlist") vars - then - let - val tmnames = map name_of_var varstm - val varnames = map name_of_var vars - val (dom,rng) = ListPair.unzip rens - val rensnames = (map name_of_var dom) @ (map name_of_var rng) - val instnames = map name_of_var (snd (ListPair.unzip inst)) - val allnames = tmnames @ varnames @ rensnames @ instnames - val vnewname = Term.variant allnames vname - val vnew = Free(vnewname,ty) - in - (vars,(v,vnew)::rens,(v,vnew)::inst) - end - else (v::vars,rens,inst)) - | process _ = raise ERR "disamb_helper" "Internal error" - - val (vars',rens',inst) = - foldr process (vars,rens,[]) varstm - in - ({vars=vars',rens=rens'},inst) - end - -fun disamb_term_from info tm = - let - val (info',inst) = disamb_helper info tm - in - (info',apply_inst_term inst tm) - end +fun disamb_term_from info tm = (info, tm) fun swap (x,y) = (y,x) -fun has_ren (HOLThm([],_)) = false - | has_ren _ = true +fun has_ren (HOLThm _) = false fun prinfo {vars,rens} = (writeln "Vars:"; app prin vars; writeln "Renaming:"; app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens) -fun disamb_thm_from info (hth as HOLThm(rens,thm)) = - let - val inv_rens = map swap rens - val orig_thm = apply_inst_term inv_rens (prop_of thm) - val (info',inst) = disamb_helper info orig_thm - val rens' = map (apsnd (apply_inst_term inst)) inv_rens - val (dom,rng) = ListPair.unzip (rens' @ inst) - val sg = sign_of_thm thm - val thm' = mk_INST (map (cterm_of sg) dom) (map (cterm_of sg) rng) thm - in - (info',thm') - end +fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm) -fun disamb_terms_from info tms = - foldr (fn (tm,(info,tms)) => - let - val (info',tm') = disamb_term_from info tm - in - (info',tm'::tms) - end) - (info,[]) tms +fun disamb_terms_from info tms = (info, tms) fun disamb_thms_from info hthms = foldr (fn (hthm,(info,thms)) => @@ -1121,28 +1110,7 @@ fun disamb_thm thm = disamb_thm_from disamb_info_empty thm fun disamb_thms thms = disamb_thms_from disamb_info_empty thms -fun norm_hthm sg (hth as HOLThm([],_)) = hth - | norm_hthm sg (hth as HOLThm(rens,th)) = - let - val vars = collect_vars (prop_of th) - val (rens',inst,_) = - foldr (fn((ren as (vold as Free(vname,_),vnew)), - (rens,inst,vars)) => - (case Library.find_first (fn Free(v,_) => v = vname | _ => false) vars of - SOME v' => if v' = vold - then (rens,(vnew,vold)::inst,vold::vars) - else (ren::rens,(vold,vnew)::inst,vnew::vars) - | NONE => (rens,(vnew,vold)::inst,vold::vars)) - | _ => raise ERR "norm_hthm" "Internal error") - ([],[],vars) rens - val (dom,rng) = ListPair.unzip inst - val th' = mk_INST (map (cterm_of sg) dom) (map (cterm_of sg) rng) th - val nvars = collect_vars (prop_of th') - val rens' = List.filter (fn(_,v) => v mem nvars) rens - val res = HOLThm(rens',th') - in - res - end +fun norm_hthm sg (hth as HOLThm _) = hth (* End of disambiguating code *) @@ -1213,7 +1181,6 @@ Thm.transfer sg (Simplifier.full_rewrite hol4ss (cterm_of sg t)) end - fun get_isabelle_thm thyname thmname hol4conc thy = let val _ = message "get_isabelle_thm called..." @@ -1275,11 +1242,35 @@ end handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE)) +fun get_isabelle_thm_and_warn thyname thmname hol4conc thy = + let + val (a, b) = get_isabelle_thm thyname thmname hol4conc thy + fun warn () = + let + val sg = sign_of thy + val (info,hol4conc') = disamb_term hol4conc + val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) + in + case concl_of i2h_conc of + Const("==",_) $ lhs $ _ => + (warning ("Failed lookup of theorem '"^thmname^"':"); + writeln "Original conclusion:"; + prin hol4conc'; + writeln "Modified conclusion:"; + prin lhs) + | _ => () + end + in + case b of + NONE => (warn () handle _ => (); (a,b)) + | _ => (a, b) + end + fun get_thm thyname thmname thy = case get_hol4_thm thyname thmname thy of SOME hth => (thy,SOME hth) - | NONE => ((case fst (import_proof thyname thmname thy) of - SOME f => get_isabelle_thm thyname thmname (f thy) thy + | NONE => ((case import_proof_concl thyname thmname thy of + SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy | NONE => (message "No conclusion"; (thy,NONE))) handle e as IO.Io _ => (message "IO exception"; (thy,NONE)) | e as PK _ => (message "PK exception"; (thy,NONE))) @@ -1295,7 +1286,7 @@ val (thmname,thy') = get_defname thyname constname thy val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname) in - get_isabelle_thm thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy' + get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy' end fun get_axiom thyname axname thy = @@ -1407,7 +1398,7 @@ (thy,res) end -fun mk_EQ_MP th1 th2 = [beta_eta_thm th1,beta_eta_thm th2] MRS eqmp_thm +fun mk_EQ_MP th1 th2 = [beta_eta_thm th1, beta_eta_thm th2] MRS eqmp_thm fun EQ_MP hth1 hth2 thy = let @@ -2086,7 +2077,7 @@ Replaying _ => (thy,hth) | _ => let - val _ = message "TYPE_INTRO:" + val _ = message "TYPE_INTRO:" val _ = if_debug pth hth val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")") val (HOLThm(rens,td_th)) = norm_hthm (sign_of thy) hth @@ -2105,13 +2096,14 @@ val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy - val th3 = (#type_definition typedef_info) RS typedef_hol2hollight - + val _ = message "step 1" val th4 = Drule.freeze_all th3 + val _ = message "step 2" val fulltyname = Sign.intern_type (sign_of thy') tycname - val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' - + val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname) + val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' + val _ = message "step 4" val sg = sign_of thy'' val (hth' as HOLThm args) = norm_hthm sg (HOLThm(rens,th4)) val _ = if #maxidx (rep_thm th4) <> ~1 @@ -2120,7 +2112,7 @@ val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating") else () val thy4 = add_hol4_pending thyname thmname args thy'' - + val sg = sign_of thy4 val P' = #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) val c = @@ -2129,7 +2121,7 @@ in Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P' end - + val tnames_string = if null tnames then "" else "(" ^ (commafy tnames) ^ ") " @@ -2147,4 +2139,6 @@ handle e => (message "exception in type_introduction"; print_exn e) end +val prin = prin + end diff -r 227f1f5c3959 -r 781abf7011e6 src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Mon Sep 12 12:11:17 2005 +0200 +++ b/src/HOL/Import/replay.ML Mon Sep 12 15:52:00 2005 +0200 @@ -61,7 +61,7 @@ | (thy',NONE) => if seg = thyname then P.new_definition seg name rhs thy' - else raise ERR "replay_proof" "Too late for term definition") + else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname)) | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE" | rp (PSpec(prf,tm)) thy = let @@ -234,6 +234,7 @@ val (f_opt,prf) = import_proof thyname' thmname thy' val prf = prf thy' val (thy',th) = replay_proof int_thms thyname' thmname prf thy' + val _ = writeln ("Successfully finished replaying "^thmname^" !") in case content_of prf of PTmSpec _ => (thy',th)