# HG changeset patch # User haftmann # Date 1330814994 -3600 # Node ID 9ae5c21fc88c70c5a9cbc337766377fa08aca4af # Parent bdf9a78d46cff57aa18947a9cc3e18bfa0dd55e5 generalized attribute name diff -r bdf9a78d46cf -r 9ae5c21fc88c src/HOL/Import/HOL4/Compatibility.thy --- a/src/HOL/Import/HOL4/Compatibility.thy Sat Mar 03 23:49:22 2012 +0100 +++ b/src/HOL/Import/HOL4/Compatibility.thy Sat Mar 03 23:49:54 2012 +0100 @@ -23,10 +23,10 @@ definition LET :: "['a \ 'b,'a] \ 'b" where "LET f s == f s" -lemma [hol4rew]: "LET f s = Let s f" +lemma [import_rew]: "LET f s = Let s f" by (simp add: LET_def Let_def) -lemmas [hol4rew] = ONE_ONE_rew +lemmas [import_rew] = ONE_ONE_rew lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)" by simp @@ -122,10 +122,10 @@ definition nat_ge :: "nat => nat => bool" where "nat_ge == %m n. nat_gt m n | m = n" -lemma [hol4rew]: "nat_gt m n = (n < m)" +lemma [import_rew]: "nat_gt m n = (n < m)" by (simp add: nat_gt_def) -lemma [hol4rew]: "nat_ge m n = (n <= m)" +lemma [import_rew]: "nat_ge m n = (n <= m)" by (auto simp add: nat_ge_def nat_gt_def) lemma GREATER_DEF: "ALL m n. (n < m) = (n < m)" @@ -204,7 +204,7 @@ (ALL f n x. (f ^^ Suc n) x = (f ^^ n) (f x))" by (simp add: funpow_swap1) -lemma [hol4rew]: "FUNPOW f n = f ^^ n" +lemma [import_rew]: "FUNPOW f n = f ^^ n" by (simp add: FUNPOW_def) lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))" @@ -237,13 +237,13 @@ definition NUMERAL :: "nat \ nat" where "NUMERAL x == x" -lemma [hol4rew]: "NUMERAL ALT_ZERO = 0" +lemma [import_rew]: "NUMERAL ALT_ZERO = 0" by (simp add: ALT_ZERO_def NUMERAL_def) -lemma [hol4rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1" +lemma [import_rew]: "NUMERAL (NUMERAL_BIT1 ALT_ZERO) = 1" by (simp add: ALT_ZERO_def NUMERAL_BIT1_def NUMERAL_def) -lemma [hol4rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2" +lemma [import_rew]: "NUMERAL (NUMERAL_BIT2 ALT_ZERO) = 2" by (simp add: ALT_ZERO_def NUMERAL_BIT2_def NUMERAL_def) lemma EXP: "(!m. m ^ 0 = (1::nat)) & (!m n. m ^ Suc n = m * (m::nat) ^ n)" @@ -356,7 +356,7 @@ definition FOLDR :: "[['a,'b]\'b,'b,'a list] \ 'b" where "FOLDR f e l == foldr f l e" -lemma [hol4rew]: "FOLDR f e l = foldr f l e" +lemma [import_rew]: "FOLDR f e l = foldr f l e" by (simp add: FOLDR_def) lemma FOLDR: "(!f e. foldr f [] e = e) & (!f e x l. foldr f (x#l) e = f x (foldr f l e))" @@ -407,7 +407,7 @@ (!x1 l1 x2 l2. zip (x1#l1) (x2#l2) = (x1,x2)#zip l1 l2)" by simp -lemma [hol4rew]: "ZIP (a,b) = zip a b" +lemma [import_rew]: "ZIP (a,b) = zip a b" by (simp add: ZIP_def) primrec unzip :: "('a * 'b) list \ 'a list * 'b list" where @@ -460,13 +460,13 @@ lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x" by auto -lemma [hol4rew]: "real (0::nat) = 0" +lemma [import_rew]: "real (0::nat) = 0" by simp -lemma [hol4rew]: "real (1::nat) = 1" +lemma [import_rew]: "real (1::nat) = 1" by simp -lemma [hol4rew]: "real (2::nat) = 2" +lemma [import_rew]: "real (2::nat) = 2" by simp lemma real_lte: "((x::real) <= y) = (~(y < x))" @@ -484,7 +484,7 @@ definition real_gt :: "real => real => bool" where "real_gt == %x y. y < x" -lemma [hol4rew]: "real_gt x y = (y < x)" +lemma [import_rew]: "real_gt x y = (y < x)" by (simp add: real_gt_def) lemma real_gt: "ALL x (y::real). (y < x) = (y < x)" @@ -493,12 +493,12 @@ definition real_ge :: "real => real => bool" where "real_ge x y == y <= x" -lemma [hol4rew]: "real_ge x y = (y <= x)" +lemma [import_rew]: "real_ge x y = (y <= x)" by (simp add: real_ge_def) lemma real_ge: "ALL x y. (y <= x) = (y <= x)" by simp -definition [hol4rew]: "list_mem x xs = List.member xs x" +definition [import_rew]: "list_mem x xs = List.member xs x" end diff -r bdf9a78d46cf -r 9ae5c21fc88c src/HOL/Import/HOL_Light/Compatibility.thy --- a/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:49:22 2012 +0100 +++ b/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:49:54 2012 +0100 @@ -9,11 +9,11 @@ begin (* list *) -lemmas [hol4rew] = list_el_def member_def list_mem_def +lemmas [import_rew] = list_el_def member_def list_mem_def (* int *) -lemmas [hol4rew] = int_coprime.simps int_gcd.simps hl_mod_def hl_div_def int_mod_def eqeq_def +lemmas [import_rew] = int_coprime.simps int_gcd.simps hl_mod_def hl_div_def int_mod_def eqeq_def (* real *) -lemma [hol4rew]: +lemma [import_rew]: "real (0::nat) = 0" "real (1::nat) = 1" "real (2::nat) = 2" by simp_all @@ -124,12 +124,12 @@ unfolding fun_eq_iff by (rule someI2) (auto intro: snd_conv[symmetric] someI2) -definition [simp, hol4rew]: "SETSPEC x P y \ P & x = y" +definition [simp, import_rew]: "SETSPEC x P y \ P & x = y" lemma DEF_PSUBSET: "op \ = (\u ua. u \ ua & u \ ua)" by (metis psubset_eq) -definition [hol4rew]: "Pred n = n - (Suc 0)" +definition [import_rew]: "Pred n = n - (Suc 0)" lemma DEF_PRE: "Pred = (SOME PRE. PRE 0 = 0 & (\n. PRE (Suc n) = n))" apply (rule some_equality[symmetric]) @@ -143,7 +143,7 @@ "inj = (\u. \x1 x2. u x1 = u x2 \ x1 = x2)" by (simp add: inj_on_def) -definition ODD'[hol4rew]: "(ODD :: nat \ bool) = odd" +definition ODD'[import_rew]: "(ODD :: nat \ bool) = odd" lemma DEF_ODD: "odd = (SOME ODD. ODD 0 = False \ (\n. ODD (Suc n) = (\ ODD n)))" @@ -155,7 +155,7 @@ apply simp_all done -definition [hol4rew, simp]: "NUMERAL (x :: nat) = x" +definition [import_rew, simp]: "NUMERAL (x :: nat) = x" lemma DEF_MOD: "op mod = (SOME r. \m n. if n = (0 :: nat) then m div n = 0 \ @@ -171,7 +171,7 @@ definition "MEASURE = (%u x y. (u x :: nat) < u y)" -lemma [hol4rew]: +lemma [import_rew]: "MEASURE u = (%a b. (a, b) \ measure u)" unfolding MEASURE_def measure_def by simp @@ -179,7 +179,7 @@ definition "LET f s = f s" -lemma [hol4rew]: +lemma [import_rew]: "LET f s = Let s f" by (simp add: LET_def Let_def) @@ -268,7 +268,7 @@ by (metis div_mult_self2 gr_implies_not0 mod_div_trivial mod_less nat_add_commute nat_mult_commute plus_nat.add_0) -definition [hol4rew]: "DISJOINT a b \ a \ b = {}" +definition [import_rew]: "DISJOINT a b \ a \ b = {}" lemma DEF_DISJOINT: "DISJOINT = (%u ua. u \ ua = {})" @@ -278,7 +278,7 @@ "op - = (\u ua. {ub. \x. (x \ u \ x \ ua) \ ub = x})" by (metis set_diff_eq) -definition [hol4rew]: "DELETE s e = s - {e}" +definition [import_rew]: "DELETE s e = s - {e}" lemma DEF_DELETE: "DELETE = (\u ua. {ub. \y. (y \ u \ y \ ua) \ ub = y})" @@ -305,7 +305,7 @@ apply auto done -lemma [hol4rew]: +lemma [import_rew]: "NUMERAL_BIT0 n = 2 * n" "NUMERAL_BIT1 n = 2 * n + 1" "2 * 0 = (0 :: nat)" @@ -329,7 +329,7 @@ apply auto done -lemmas [hol4rew] = id_apply +lemmas [import_rew] = id_apply lemma DEF_CHOICE: "Eps = (%u. SOME x. u x)" by simp @@ -337,11 +337,11 @@ definition dotdot :: "nat => nat => nat set" where "dotdot u ua = {ub. EX x. (u <= x & x <= ua) & ub = x}" -lemma [hol4rew]: "dotdot a b = {a..b}" +lemma [import_rew]: "dotdot a b = {a..b}" unfolding fun_eq_iff atLeastAtMost_def atLeast_def atMost_def dotdot_def by (simp add: Collect_conj_eq) -definition [hol4rew,simp]: "INFINITE S \ \ finite S" +definition [import_rew,simp]: "INFINITE S \ \ finite S" lemma DEF_INFINITE: "INFINITE = (\u. \finite u)" by (simp add: INFINITE_def_raw) diff -r bdf9a78d46cf -r 9ae5c21fc88c src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Sat Mar 03 23:49:22 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,639 +0,0 @@ -(* Title: HOL/Import/hol4rews.ML - Author: Sebastian Skalberg (TU Muenchen) -*) - -structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord); - -type holthm = (term * term) list * thm - -datatype ImportStatus = - NoImport - | Generating of string - | Replaying of string - -structure HOL4DefThy = Theory_Data -( - type T = ImportStatus - val empty = NoImport - val extend = I - fun merge (NoImport, NoImport) = NoImport - | merge _ = (warning "Import status set during merge"; NoImport) -) - -structure ImportSegment = Theory_Data -( - type T = string - val empty = "" - val extend = I - fun merge ("",arg) = arg - | merge (arg,"") = arg - | merge (s1,s2) = - if s1 = s2 - then s1 - else error "Trying to merge two different import segments" -) - -val get_import_segment = ImportSegment.get -val set_import_segment = ImportSegment.put - -structure HOL4UNames = Theory_Data -( - type T = string list - val empty = [] - val extend = I - fun merge ([], []) = [] - | merge _ = error "Used names not empty during merge" -) - -structure HOL4Dump = Theory_Data -( - type T = string * string * string list - val empty = ("","",[]) - val extend = I - fun merge (("","",[]),("","",[])) = ("","",[]) - | merge _ = error "Dump data not empty during merge" -) - -structure HOL4Moves = Theory_Data -( - type T = string Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data -) - -structure HOL4Imports = Theory_Data -( - type T = string Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data -) - -fun get_segment2 thyname thy = - Symtab.lookup (HOL4Imports.get thy) thyname - -fun set_segment thyname segname thy = - let - val imps = HOL4Imports.get thy - val imps' = Symtab.update_new (thyname,segname) imps - in - HOL4Imports.put imps' thy - end - -structure HOL4CMoves = Theory_Data -( - type T = string Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data -) - -structure HOL4Maps = Theory_Data -( - type T = string option StringPair.table - val empty = StringPair.empty - val extend = I - fun merge data = StringPair.merge (K true) data -) - -structure HOL4Thms = Theory_Data -( - type T = holthm StringPair.table - val empty = StringPair.empty - val extend = I - fun merge data = StringPair.merge (K true) data -) - -structure HOL4ConstMaps = Theory_Data -( - type T = (bool * string * typ option) StringPair.table - val empty = StringPair.empty - val extend = I - fun merge data = StringPair.merge (K true) data -) - -structure HOL4Rename = Theory_Data -( - type T = string StringPair.table - val empty = StringPair.empty - val extend = I - fun merge data = StringPair.merge (K true) data -) - -structure HOL4DefMaps = Theory_Data -( - type T = string StringPair.table - val empty = StringPair.empty - val extend = I - fun merge data = StringPair.merge (K true) data -) - -structure HOL4TypeMaps = Theory_Data -( - type T = (bool * string) StringPair.table - val empty = StringPair.empty - val extend = I - fun merge data = StringPair.merge (K true) data -) - -structure HOL4Pending = Theory_Data -( - type T = ((term * term) list * thm) StringPair.table - val empty = StringPair.empty - val extend = I - fun merge data = StringPair.merge (K true) data -) - -structure HOL4Rewrites = Theory_Data -( - type T = thm list - val empty = [] - val extend = I - val merge = Thm.merge_thms -) - -val hol4_debug = Unsynchronized.ref false -fun message s = if !hol4_debug then writeln s else () - -fun add_hol4_rewrite (Context.Theory thy, th) = - let - val _ = message "Adding HOL4 rewrite" - val th1 = th RS @{thm eq_reflection} - handle THM _ => th - val current_rews = HOL4Rewrites.get thy - val new_rews = insert Thm.eq_thm th1 current_rews - val updated_thy = HOL4Rewrites.put new_rews thy - in - (Context.Theory updated_thy,th1) - end - | add_hol4_rewrite (context, th) = (context, - (th RS @{thm eq_reflection} handle THM _ => th) - ); - -fun ignore_hol4 bthy bthm thy = - let - val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm) - val curmaps = HOL4Maps.get thy - val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps - val upd_thy = HOL4Maps.put newmaps thy - in - upd_thy - end - -val opt_get_output_thy = #2 o HOL4Dump.get - -fun get_output_thy thy = - case #2 (HOL4Dump.get thy) of - "" => error "No theory file being output" - | thyname => thyname - -val get_output_dir = #1 o HOL4Dump.get - -fun add_hol4_move bef aft thy = - let - val curmoves = HOL4Moves.get thy - val newmoves = Symtab.update_new (bef, aft) curmoves - in - HOL4Moves.put newmoves thy - end - -fun get_hol4_move bef thy = - Symtab.lookup (HOL4Moves.get thy) bef - -fun follow_name thmname thy = - let - val moves = HOL4Moves.get thy - fun F thmname = - case Symtab.lookup moves thmname of - SOME name => F name - | NONE => thmname - in - F thmname - end - -fun add_hol4_cmove bef aft thy = - let - val curmoves = HOL4CMoves.get thy - val newmoves = Symtab.update_new (bef, aft) curmoves - in - HOL4CMoves.put newmoves thy - end - -fun get_hol4_cmove bef thy = - Symtab.lookup (HOL4CMoves.get thy) bef - -fun follow_cname thmname thy = - let - val moves = HOL4CMoves.get thy - fun F thmname = - case Symtab.lookup moves thmname of - SOME name => F name - | NONE => thmname - in - F thmname - end - -fun add_hol4_mapping bthy bthm isathm thy = - let - (* val _ = writeln ("Before follow_name: "^isathm) *) - val isathm = follow_name isathm thy - (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*) - val curmaps = HOL4Maps.get thy - val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps - val upd_thy = HOL4Maps.put newmaps thy - in - upd_thy - end; - -fun get_hol4_type_mapping bthy tycon thy = - let - val maps = HOL4TypeMaps.get thy - in - StringPair.lookup maps (bthy,tycon) - end - -fun get_hol4_mapping bthy bthm thy = - let - val curmaps = HOL4Maps.get thy - in - StringPair.lookup curmaps (bthy,bthm) - end; - -fun add_hol4_const_mapping bthy bconst internal isaconst thy = - let - val thy = case opt_get_output_thy thy of - "" => thy - | output_thy => if internal - then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy - else thy - val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) - val curmaps = HOL4ConstMaps.get thy - val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps - val upd_thy = HOL4ConstMaps.put newmaps thy - in - upd_thy - end; - -fun add_hol4_const_renaming bthy bconst newname thy = - let - val currens = HOL4Rename.get thy - val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname) - val newrens = StringPair.update_new ((bthy,bconst),newname) currens - val upd_thy = HOL4Rename.put newrens thy - in - upd_thy - end; - -fun get_hol4_const_renaming bthy bconst thy = - let - val currens = HOL4Rename.get thy - in - StringPair.lookup currens (bthy,bconst) - end; - -fun get_hol4_const_mapping bthy bconst thy = - let - val bconst = case get_hol4_const_renaming bthy bconst thy of - SOME name => name - | NONE => bconst - val maps = HOL4ConstMaps.get thy - in - StringPair.lookup maps (bthy,bconst) - end - -fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy = - let - val thy = case opt_get_output_thy thy of - "" => thy - | output_thy => if internal - then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy - else thy - val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) - val curmaps = HOL4ConstMaps.get thy - val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps - val upd_thy = HOL4ConstMaps.put newmaps thy - in - upd_thy - end; - -fun add_hol4_type_mapping bthy bconst internal isaconst thy = - let - val curmaps = HOL4TypeMaps.get thy - val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) - val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps - (* FIXME avoid handle x *) - handle x => let val (_, 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; - -fun add_hol4_pending bthy bthm hth thy = - let - val thmname = Sign.full_bname thy bthm - val _ = message ("Add pending " ^ bthy ^ "." ^ bthm) - val curpend = HOL4Pending.get thy - val newpend = StringPair.update_new ((bthy,bthm),hth) curpend - val upd_thy = HOL4Pending.put newpend thy - val thy' = case opt_get_output_thy upd_thy of - "" => add_hol4_mapping bthy bthm thmname upd_thy - | output_thy => - let - val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm - in - upd_thy |> add_hol4_move thmname new_thmname - |> add_hol4_mapping bthy bthm new_thmname - end - in - thy' - end; - -fun get_hol4_theorem thyname thmname thy = - let - val isathms = HOL4Thms.get thy - in - StringPair.lookup isathms (thyname,thmname) - end; - -fun add_hol4_theorem thyname thmname hth = - let - val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname) - in - HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth)) - end; - -fun export_hol4_pending thy = - let - val rews = HOL4Rewrites.get thy; - val pending = HOL4Pending.get thy; - fun process ((bthy,bthm), hth as (_,thm)) thy = - let - val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm); - val thm2 = Drule.export_without_context thm1; - in - thy - |> Global_Theory.store_thm (Binding.name bthm, thm2) - |> snd - |> add_hol4_theorem bthy bthm hth - end; - in - thy - |> StringPair.fold process pending - |> HOL4Pending.put StringPair.empty - end; - -fun setup_dump (dir,thyname) thy = - HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy - -fun add_dump str thy = - let - val (dir,thyname,curdump) = HOL4Dump.get thy - in - HOL4Dump.put (dir,thyname,str::curdump) thy - end - -fun flush_dump thy = - let - val (dir,thyname,dumpdata) = HOL4Dump.get thy - val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir, - file=thyname ^ ".thy"}) - val _ = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata) - val _ = TextIO.closeOut os - in - HOL4Dump.put ("","",[]) thy - end - -fun set_generating_thy thyname thy = - case HOL4DefThy.get thy of - NoImport => HOL4DefThy.put (Generating thyname) thy - | _ => error "Import already in progess" - -fun set_replaying_thy thyname thy = - case HOL4DefThy.get thy of - NoImport => HOL4DefThy.put (Replaying thyname) thy - | _ => error "Import already in progess" - -fun clear_import_thy thy = - case HOL4DefThy.get thy of - NoImport => error "No import in progress" - | _ => HOL4DefThy.put NoImport thy - -fun get_generating_thy thy = - case HOL4DefThy.get thy of - Generating thyname => thyname - | _ => error "No theory being generated" - -fun get_replaying_thy thy = - case HOL4DefThy.get thy of - Replaying thyname => thyname - | _ => error "No theory being replayed" - -fun get_import_thy thy = - case HOL4DefThy.get thy of - Replaying thyname => thyname - | Generating thyname => thyname - | _ => error "No theory being imported" - -fun should_ignore thyname thy thmname = - case get_hol4_mapping thyname thmname thy of - SOME NONE => true - | _ => false - -val trans_string = - let - fun quote s = "\"" ^ s ^ "\"" - fun F [] = [] - | F (#"\\" :: cs) = patch #"\\" cs - | F (#"\"" :: cs) = patch #"\"" cs - | F (c :: cs) = c :: F cs - and patch c rest = #"\\" :: c :: F rest - in - quote o String.implode o F o String.explode - end - -fun dump_import_thy thyname thy = - let - val output_dir = get_output_dir thy - val output_thy = get_output_thy thy - val input_thy = Context.theory_name thy - val import_segment = get_import_segment thy - val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir, - file=thyname ^ ".imp"}) - fun out s = TextIO.output(os,s) - val (ignored, mapped) = StringPair.fold - (fn ((bthy, bthm), v) => fn (ign, map) => - if bthy = thyname - then case v - of NONE => (bthm :: ign, map) - | SOME w => (ign, (bthm, w) :: map) - else (ign, map)) (HOL4Maps.get thy) ([],[]); - fun mk init = StringPair.fold - (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init []; - val constmaps = mk (HOL4ConstMaps.get thy); - val constrenames = mk (HOL4Rename.get thy); - val typemaps = mk (HOL4TypeMaps.get thy); - val defmaps = mk (HOL4DefMaps.get thy); - fun new_name internal isa = - if internal - then - let - val paths = Long_Name.explode isa - val i = drop (length paths - 2) paths - in - case i of - [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con - | _ => error "hol4rews.dump internal error" - end - else - isa - - val _ = out "import\n\n" - - val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n") - val _ = if null defmaps - then () - else out "def_maps" - val _ = app (fn (hol,isa) => - out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps - val _ = if null defmaps - then () - else out "\n\n" - - val _ = if null typemaps - then () - else out "type_maps" - val _ = app (fn (hol,(internal,isa)) => - out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps - val _ = if null typemaps - then () - else out "\n\n" - - val _ = if null constmaps - then () - else out "const_maps" - val _ = app (fn (hol,(_,isa,opt_ty)) => - (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); - case opt_ty of - SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"") - | NONE => ())) constmaps - val _ = if null constmaps - then () - else out "\n\n" - - val _ = if null constrenames - then () - else out "const_renames" - val _ = app (fn (old,new) => - out ("\n " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames - val _ = if null constrenames - then () - else out "\n\n" - - fun gen2replay in_thy out_thy s = - let - val ss = Long_Name.explode s - in - if (hd ss = in_thy) then - Long_Name.implode (out_thy::(tl ss)) - else - s - end - - val _ = if null mapped - then () - else out "thm_maps" - val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped - val _ = if null mapped - then () - else out "\n\n" - - val _ = if null ignored - then () - else out "ignore_thms" - val _ = app (fn ign => out ("\n " ^ (trans_string ign))) ignored - val _ = if null ignored - then () - else out "\n\n" - - val _ = out "end\n" - val _ = TextIO.closeOut os - in - thy - end - -fun set_used_names names thy = - let - val unames = HOL4UNames.get thy - in - case unames of - [] => HOL4UNames.put names thy - | _ => error "hol4rews.set_used_names called on initialized data!" - end - -val clear_used_names = HOL4UNames.put []; - -fun get_defmap thyname const thy = - let - val maps = HOL4DefMaps.get thy - in - StringPair.lookup maps (thyname,const) - end - -fun add_defmap thyname const defname thy = - let - val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname) - val maps = HOL4DefMaps.get thy - val maps' = StringPair.update_new ((thyname,const),defname) maps - val thy' = HOL4DefMaps.put maps' thy - in - thy' - end - -fun get_defname thyname name thy = - let - val maps = HOL4DefMaps.get thy - fun F dname = (dname,add_defmap thyname name dname thy) - in - case StringPair.lookup maps (thyname,name) of - SOME thmname => (thmname,thy) - | NONE => - let - val used = HOL4UNames.get thy - val defname = Thm.def_name name - val pdefname = name ^ "_primdef" - in - if not (member (op =) used defname) - then F defname (* name_def *) - else if not (member (op =) used pdefname) - then F pdefname (* name_primdef *) - else F (singleton (Name.variant_list used) pdefname) (* last resort *) - end - end - -local - fun handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "=="}, _],_,_]] = x - | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax all}, _],_]] = x - | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "==>"}, _],_,_]] = x - | handle_meta [x] = Ast.Appl [Ast.Constant @{const_syntax Trueprop}, x] - | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument" -in -val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)] -end - -local - fun initial_maps thy = - thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool} - |> add_hol4_type_mapping "min" "fun" false "fun" - |> add_hol4_type_mapping "min" "ind" false @{type_name ind} - |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq} - |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies} - |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"} -in -val hol4_setup = - initial_maps #> - Attrib.setup @{binding hol4rew} - (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "HOL4 rewrite rule" - -end diff -r bdf9a78d46cf -r 9ae5c21fc88c src/HOL/Import/import_rews.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Import/import_rews.ML Sat Mar 03 23:49:54 2012 +0100 @@ -0,0 +1,639 @@ +(* Title: HOL/Import/import_rews.ML + Author: Sebastian Skalberg (TU Muenchen) +*) + +structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord); + +type holthm = (term * term) list * thm + +datatype ImportStatus = + NoImport + | Generating of string + | Replaying of string + +structure HOL4DefThy = Theory_Data +( + type T = ImportStatus + val empty = NoImport + val extend = I + fun merge (NoImport, NoImport) = NoImport + | merge _ = (warning "Import status set during merge"; NoImport) +) + +structure ImportSegment = Theory_Data +( + type T = string + val empty = "" + val extend = I + fun merge ("",arg) = arg + | merge (arg,"") = arg + | merge (s1,s2) = + if s1 = s2 + then s1 + else error "Trying to merge two different import segments" +) + +val get_import_segment = ImportSegment.get +val set_import_segment = ImportSegment.put + +structure HOL4UNames = Theory_Data +( + type T = string list + val empty = [] + val extend = I + fun merge ([], []) = [] + | merge _ = error "Used names not empty during merge" +) + +structure HOL4Dump = Theory_Data +( + type T = string * string * string list + val empty = ("","",[]) + val extend = I + fun merge (("","",[]),("","",[])) = ("","",[]) + | merge _ = error "Dump data not empty during merge" +) + +structure HOL4Moves = Theory_Data +( + type T = string Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) + +structure HOL4Imports = Theory_Data +( + type T = string Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) + +fun get_segment2 thyname thy = + Symtab.lookup (HOL4Imports.get thy) thyname + +fun set_segment thyname segname thy = + let + val imps = HOL4Imports.get thy + val imps' = Symtab.update_new (thyname,segname) imps + in + HOL4Imports.put imps' thy + end + +structure HOL4CMoves = Theory_Data +( + type T = string Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) + +structure HOL4Maps = Theory_Data +( + type T = string option StringPair.table + val empty = StringPair.empty + val extend = I + fun merge data = StringPair.merge (K true) data +) + +structure HOL4Thms = Theory_Data +( + type T = holthm StringPair.table + val empty = StringPair.empty + val extend = I + fun merge data = StringPair.merge (K true) data +) + +structure HOL4ConstMaps = Theory_Data +( + type T = (bool * string * typ option) StringPair.table + val empty = StringPair.empty + val extend = I + fun merge data = StringPair.merge (K true) data +) + +structure HOL4Rename = Theory_Data +( + type T = string StringPair.table + val empty = StringPair.empty + val extend = I + fun merge data = StringPair.merge (K true) data +) + +structure HOL4DefMaps = Theory_Data +( + type T = string StringPair.table + val empty = StringPair.empty + val extend = I + fun merge data = StringPair.merge (K true) data +) + +structure HOL4TypeMaps = Theory_Data +( + type T = (bool * string) StringPair.table + val empty = StringPair.empty + val extend = I + fun merge data = StringPair.merge (K true) data +) + +structure HOL4Pending = Theory_Data +( + type T = ((term * term) list * thm) StringPair.table + val empty = StringPair.empty + val extend = I + fun merge data = StringPair.merge (K true) data +) + +structure HOL4Rewrites = Theory_Data +( + type T = thm list + val empty = [] + val extend = I + val merge = Thm.merge_thms +) + +val hol4_debug = Unsynchronized.ref false +fun message s = if !hol4_debug then writeln s else () + +fun add_hol4_rewrite (Context.Theory thy, th) = + let + val _ = message "Adding HOL4 rewrite" + val th1 = th RS @{thm eq_reflection} + handle THM _ => th + val current_rews = HOL4Rewrites.get thy + val new_rews = insert Thm.eq_thm th1 current_rews + val updated_thy = HOL4Rewrites.put new_rews thy + in + (Context.Theory updated_thy,th1) + end + | add_hol4_rewrite (context, th) = (context, + (th RS @{thm eq_reflection} handle THM _ => th) + ); + +fun ignore_hol4 bthy bthm thy = + let + val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm) + val curmaps = HOL4Maps.get thy + val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps + val upd_thy = HOL4Maps.put newmaps thy + in + upd_thy + end + +val opt_get_output_thy = #2 o HOL4Dump.get + +fun get_output_thy thy = + case #2 (HOL4Dump.get thy) of + "" => error "No theory file being output" + | thyname => thyname + +val get_output_dir = #1 o HOL4Dump.get + +fun add_hol4_move bef aft thy = + let + val curmoves = HOL4Moves.get thy + val newmoves = Symtab.update_new (bef, aft) curmoves + in + HOL4Moves.put newmoves thy + end + +fun get_hol4_move bef thy = + Symtab.lookup (HOL4Moves.get thy) bef + +fun follow_name thmname thy = + let + val moves = HOL4Moves.get thy + fun F thmname = + case Symtab.lookup moves thmname of + SOME name => F name + | NONE => thmname + in + F thmname + end + +fun add_hol4_cmove bef aft thy = + let + val curmoves = HOL4CMoves.get thy + val newmoves = Symtab.update_new (bef, aft) curmoves + in + HOL4CMoves.put newmoves thy + end + +fun get_hol4_cmove bef thy = + Symtab.lookup (HOL4CMoves.get thy) bef + +fun follow_cname thmname thy = + let + val moves = HOL4CMoves.get thy + fun F thmname = + case Symtab.lookup moves thmname of + SOME name => F name + | NONE => thmname + in + F thmname + end + +fun add_hol4_mapping bthy bthm isathm thy = + let + (* val _ = writeln ("Before follow_name: "^isathm) *) + val isathm = follow_name isathm thy + (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*) + val curmaps = HOL4Maps.get thy + val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps + val upd_thy = HOL4Maps.put newmaps thy + in + upd_thy + end; + +fun get_hol4_type_mapping bthy tycon thy = + let + val maps = HOL4TypeMaps.get thy + in + StringPair.lookup maps (bthy,tycon) + end + +fun get_hol4_mapping bthy bthm thy = + let + val curmaps = HOL4Maps.get thy + in + StringPair.lookup curmaps (bthy,bthm) + end; + +fun add_hol4_const_mapping bthy bconst internal isaconst thy = + let + val thy = case opt_get_output_thy thy of + "" => thy + | output_thy => if internal + then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy + else thy + val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) + val curmaps = HOL4ConstMaps.get thy + val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps + val upd_thy = HOL4ConstMaps.put newmaps thy + in + upd_thy + end; + +fun add_hol4_const_renaming bthy bconst newname thy = + let + val currens = HOL4Rename.get thy + val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname) + val newrens = StringPair.update_new ((bthy,bconst),newname) currens + val upd_thy = HOL4Rename.put newrens thy + in + upd_thy + end; + +fun get_hol4_const_renaming bthy bconst thy = + let + val currens = HOL4Rename.get thy + in + StringPair.lookup currens (bthy,bconst) + end; + +fun get_hol4_const_mapping bthy bconst thy = + let + val bconst = case get_hol4_const_renaming bthy bconst thy of + SOME name => name + | NONE => bconst + val maps = HOL4ConstMaps.get thy + in + StringPair.lookup maps (bthy,bconst) + end + +fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy = + let + val thy = case opt_get_output_thy thy of + "" => thy + | output_thy => if internal + then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy + else thy + val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) + val curmaps = HOL4ConstMaps.get thy + val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps + val upd_thy = HOL4ConstMaps.put newmaps thy + in + upd_thy + end; + +fun add_hol4_type_mapping bthy bconst internal isaconst thy = + let + val curmaps = HOL4TypeMaps.get thy + val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) + val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps + (* FIXME avoid handle x *) + handle x => let val (_, 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; + +fun add_hol4_pending bthy bthm hth thy = + let + val thmname = Sign.full_bname thy bthm + val _ = message ("Add pending " ^ bthy ^ "." ^ bthm) + val curpend = HOL4Pending.get thy + val newpend = StringPair.update_new ((bthy,bthm),hth) curpend + val upd_thy = HOL4Pending.put newpend thy + val thy' = case opt_get_output_thy upd_thy of + "" => add_hol4_mapping bthy bthm thmname upd_thy + | output_thy => + let + val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm + in + upd_thy |> add_hol4_move thmname new_thmname + |> add_hol4_mapping bthy bthm new_thmname + end + in + thy' + end; + +fun get_hol4_theorem thyname thmname thy = + let + val isathms = HOL4Thms.get thy + in + StringPair.lookup isathms (thyname,thmname) + end; + +fun add_hol4_theorem thyname thmname hth = + let + val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname) + in + HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth)) + end; + +fun export_hol4_pending thy = + let + val rews = HOL4Rewrites.get thy; + val pending = HOL4Pending.get thy; + fun process ((bthy,bthm), hth as (_,thm)) thy = + let + val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm); + val thm2 = Drule.export_without_context thm1; + in + thy + |> Global_Theory.store_thm (Binding.name bthm, thm2) + |> snd + |> add_hol4_theorem bthy bthm hth + end; + in + thy + |> StringPair.fold process pending + |> HOL4Pending.put StringPair.empty + end; + +fun setup_dump (dir,thyname) thy = + HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy + +fun add_dump str thy = + let + val (dir,thyname,curdump) = HOL4Dump.get thy + in + HOL4Dump.put (dir,thyname,str::curdump) thy + end + +fun flush_dump thy = + let + val (dir,thyname,dumpdata) = HOL4Dump.get thy + val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir, + file=thyname ^ ".thy"}) + val _ = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata) + val _ = TextIO.closeOut os + in + HOL4Dump.put ("","",[]) thy + end + +fun set_generating_thy thyname thy = + case HOL4DefThy.get thy of + NoImport => HOL4DefThy.put (Generating thyname) thy + | _ => error "Import already in progess" + +fun set_replaying_thy thyname thy = + case HOL4DefThy.get thy of + NoImport => HOL4DefThy.put (Replaying thyname) thy + | _ => error "Import already in progess" + +fun clear_import_thy thy = + case HOL4DefThy.get thy of + NoImport => error "No import in progress" + | _ => HOL4DefThy.put NoImport thy + +fun get_generating_thy thy = + case HOL4DefThy.get thy of + Generating thyname => thyname + | _ => error "No theory being generated" + +fun get_replaying_thy thy = + case HOL4DefThy.get thy of + Replaying thyname => thyname + | _ => error "No theory being replayed" + +fun get_import_thy thy = + case HOL4DefThy.get thy of + Replaying thyname => thyname + | Generating thyname => thyname + | _ => error "No theory being imported" + +fun should_ignore thyname thy thmname = + case get_hol4_mapping thyname thmname thy of + SOME NONE => true + | _ => false + +val trans_string = + let + fun quote s = "\"" ^ s ^ "\"" + fun F [] = [] + | F (#"\\" :: cs) = patch #"\\" cs + | F (#"\"" :: cs) = patch #"\"" cs + | F (c :: cs) = c :: F cs + and patch c rest = #"\\" :: c :: F rest + in + quote o String.implode o F o String.explode + end + +fun dump_import_thy thyname thy = + let + val output_dir = get_output_dir thy + val output_thy = get_output_thy thy + val input_thy = Context.theory_name thy + val import_segment = get_import_segment thy + val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir, + file=thyname ^ ".imp"}) + fun out s = TextIO.output(os,s) + val (ignored, mapped) = StringPair.fold + (fn ((bthy, bthm), v) => fn (ign, map) => + if bthy = thyname + then case v + of NONE => (bthm :: ign, map) + | SOME w => (ign, (bthm, w) :: map) + else (ign, map)) (HOL4Maps.get thy) ([],[]); + fun mk init = StringPair.fold + (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init []; + val constmaps = mk (HOL4ConstMaps.get thy); + val constrenames = mk (HOL4Rename.get thy); + val typemaps = mk (HOL4TypeMaps.get thy); + val defmaps = mk (HOL4DefMaps.get thy); + fun new_name internal isa = + if internal + then + let + val paths = Long_Name.explode isa + val i = drop (length paths - 2) paths + in + case i of + [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con + | _ => error "import_rews.dump internal error" + end + else + isa + + val _ = out "import\n\n" + + val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n") + val _ = if null defmaps + then () + else out "def_maps" + val _ = app (fn (hol,isa) => + out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps + val _ = if null defmaps + then () + else out "\n\n" + + val _ = if null typemaps + then () + else out "type_maps" + val _ = app (fn (hol,(internal,isa)) => + out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps + val _ = if null typemaps + then () + else out "\n\n" + + val _ = if null constmaps + then () + else out "const_maps" + val _ = app (fn (hol,(_,isa,opt_ty)) => + (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy))); + case opt_ty of + SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"") + | NONE => ())) constmaps + val _ = if null constmaps + then () + else out "\n\n" + + val _ = if null constrenames + then () + else out "const_renames" + val _ = app (fn (old,new) => + out ("\n " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames + val _ = if null constrenames + then () + else out "\n\n" + + fun gen2replay in_thy out_thy s = + let + val ss = Long_Name.explode s + in + if (hd ss = in_thy) then + Long_Name.implode (out_thy::(tl ss)) + else + s + end + + val _ = if null mapped + then () + else out "thm_maps" + val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped + val _ = if null mapped + then () + else out "\n\n" + + val _ = if null ignored + then () + else out "ignore_thms" + val _ = app (fn ign => out ("\n " ^ (trans_string ign))) ignored + val _ = if null ignored + then () + else out "\n\n" + + val _ = out "end\n" + val _ = TextIO.closeOut os + in + thy + end + +fun set_used_names names thy = + let + val unames = HOL4UNames.get thy + in + case unames of + [] => HOL4UNames.put names thy + | _ => error "import_rews.set_used_names called on initialized data!" + end + +val clear_used_names = HOL4UNames.put []; + +fun get_defmap thyname const thy = + let + val maps = HOL4DefMaps.get thy + in + StringPair.lookup maps (thyname,const) + end + +fun add_defmap thyname const defname thy = + let + val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname) + val maps = HOL4DefMaps.get thy + val maps' = StringPair.update_new ((thyname,const),defname) maps + val thy' = HOL4DefMaps.put maps' thy + in + thy' + end + +fun get_defname thyname name thy = + let + val maps = HOL4DefMaps.get thy + fun F dname = (dname,add_defmap thyname name dname thy) + in + case StringPair.lookup maps (thyname,name) of + SOME thmname => (thmname,thy) + | NONE => + let + val used = HOL4UNames.get thy + val defname = Thm.def_name name + val pdefname = name ^ "_primdef" + in + if not (member (op =) used defname) + then F defname (* name_def *) + else if not (member (op =) used pdefname) + then F pdefname (* name_primdef *) + else F (singleton (Name.variant_list used) pdefname) (* last resort *) + end + end + +local + fun handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "=="}, _],_,_]] = x + | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax all}, _],_]] = x + | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "==>"}, _],_,_]] = x + | handle_meta [x] = Ast.Appl [Ast.Constant @{const_syntax Trueprop}, x] + | handle_meta _ = error "import_rews error: Trueprop not applied to single argument" +in +val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)] +end + +local + fun initial_maps thy = + thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool} + |> add_hol4_type_mapping "min" "fun" false "fun" + |> add_hol4_type_mapping "min" "ind" false @{type_name ind} + |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq} + |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies} + |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"} +in +val hol4_setup = + initial_maps #> + Attrib.setup @{binding import_rew} + (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "HOL4 rewrite rule" + +end diff -r bdf9a78d46cf -r 9ae5c21fc88c src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Mar 03 23:49:22 2012 +0100 +++ b/src/HOL/Import/proof_kernel.ML Sat Mar 03 23:49:54 2012 +0100 @@ -1114,8 +1114,8 @@ fun rewrite_hol4_term t thy = let - val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy) - val hol4ss = Simplifier.global_context thy empty_ss addsimps hol4rews1 + val import_rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy) + val hol4ss = Simplifier.global_context thy empty_ss addsimps import_rews1 in Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t)) end