--- 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 \<Rightarrow> 'b,'a] \<Rightarrow> '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 \<Rightarrow> 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]\<Rightarrow>'b,'b,'a list] \<Rightarrow> '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 \<Rightarrow> '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
--- 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 \<longleftrightarrow> P & x = y"
+definition [simp, import_rew]: "SETSPEC x P y \<longleftrightarrow> P & x = y"
lemma DEF_PSUBSET: "op \<subset> = (\<lambda>u ua. u \<subseteq> ua & u \<noteq> 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 & (\<forall>n. PRE (Suc n) = n))"
apply (rule some_equality[symmetric])
@@ -143,7 +143,7 @@
"inj = (\<lambda>u. \<forall>x1 x2. u x1 = u x2 \<longrightarrow> x1 = x2)"
by (simp add: inj_on_def)
-definition ODD'[hol4rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
+definition ODD'[import_rew]: "(ODD :: nat \<Rightarrow> bool) = odd"
lemma DEF_ODD:
"odd = (SOME ODD. ODD 0 = False \<and> (\<forall>n. ODD (Suc n) = (\<not> 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. \<forall>m n. if n = (0 :: nat) then m div n = 0 \<and>
@@ -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) \<in> 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 \<longleftrightarrow> a \<inter> b = {}"
+definition [import_rew]: "DISJOINT a b \<longleftrightarrow> a \<inter> b = {}"
lemma DEF_DISJOINT:
"DISJOINT = (%u ua. u \<inter> ua = {})"
@@ -278,7 +278,7 @@
"op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> 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 = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> 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 \<longleftrightarrow> \<not> finite S"
+definition [import_rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
by (simp add: INFINITE_def_raw)
--- 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
--- /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
--- 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