--- a/src/HOL/Import/README Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/README Sun Mar 04 00:03:04 2012 +0100
@@ -2,7 +2,7 @@
ATTENTION! This is largely outdated. The hint to PROOF_DIRS might be
everything which is still relevant.
-All the files in this directory (except this README, HOL4.thy, and
+All the files in this directory (except this README, Importer.thy, and
ROOT.ML) are automatically generated. Edit the files in
../Generate-HOL and run "isabelle make HOL-Complex-Generate-HOL" in
~~/src/HOL, if something needs to be changed.
--- a/src/HOL/Import/import.ML Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/import.ML Sun Mar 04 00:03:04 2012 +0100
@@ -37,11 +37,11 @@
NONE => fst (Replay.setup_int_thms thyname thy)
| SOME a => a
val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
- val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
- val thm = snd (ProofKernel.to_isa_thm hol4thm)
- val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
+ val importerthm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
+ val thm = snd (ProofKernel.to_isa_thm importerthm)
+ val rew = ProofKernel.rewrite_importer_term (concl_of thm) thy
val thm = Thm.equal_elim rew thm
- val prew = ProofKernel.rewrite_hol4_term prem thy
+ val prew = ProofKernel.rewrite_importer_term prem thy
val prem' = #2 (Logic.dest_equals (prop_of prew))
val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
val thm = ProofKernel.disambiguate_frees thm
--- a/src/HOL/Import/import_rews.ML Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/import_rews.ML Sun Mar 04 00:03:04 2012 +0100
@@ -11,7 +11,7 @@
| Generating of string
| Replaying of string
-structure HOL4DefThy = Theory_Data
+structure Importer_DefThy = Theory_Data
(
type T = ImportStatus
val empty = NoImport
@@ -36,7 +36,7 @@
val get_import_segment = ImportSegment.get
val set_import_segment = ImportSegment.put
-structure HOL4UNames = Theory_Data
+structure Importer_UNames = Theory_Data
(
type T = string list
val empty = []
@@ -45,7 +45,7 @@
| merge _ = error "Used names not empty during merge"
)
-structure HOL4Dump = Theory_Data
+structure Importer_Dump = Theory_Data
(
type T = string * string * string list
val empty = ("","",[])
@@ -54,7 +54,7 @@
| merge _ = error "Dump data not empty during merge"
)
-structure HOL4Moves = Theory_Data
+structure Importer_Moves = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
@@ -62,7 +62,7 @@
fun merge data = Symtab.merge (K true) data
)
-structure HOL4Imports = Theory_Data
+structure Importer_Imports = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
@@ -71,17 +71,17 @@
)
fun get_segment2 thyname thy =
- Symtab.lookup (HOL4Imports.get thy) thyname
+ Symtab.lookup (Importer_Imports.get thy) thyname
fun set_segment thyname segname thy =
let
- val imps = HOL4Imports.get thy
+ val imps = Importer_Imports.get thy
val imps' = Symtab.update_new (thyname,segname) imps
in
- HOL4Imports.put imps' thy
+ Importer_Imports.put imps' thy
end
-structure HOL4CMoves = Theory_Data
+structure Importer_CMoves = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
@@ -89,7 +89,7 @@
fun merge data = Symtab.merge (K true) data
)
-structure HOL4Maps = Theory_Data
+structure Importer_Maps = Theory_Data
(
type T = string option StringPair.table
val empty = StringPair.empty
@@ -97,7 +97,7 @@
fun merge data = StringPair.merge (K true) data
)
-structure HOL4Thms = Theory_Data
+structure Importer_Thms = Theory_Data
(
type T = holthm StringPair.table
val empty = StringPair.empty
@@ -105,7 +105,7 @@
fun merge data = StringPair.merge (K true) data
)
-structure HOL4ConstMaps = Theory_Data
+structure Importer_ConstMaps = Theory_Data
(
type T = (bool * string * typ option) StringPair.table
val empty = StringPair.empty
@@ -113,7 +113,7 @@
fun merge data = StringPair.merge (K true) data
)
-structure HOL4Rename = Theory_Data
+structure Importer_Rename = Theory_Data
(
type T = string StringPair.table
val empty = StringPair.empty
@@ -121,7 +121,7 @@
fun merge data = StringPair.merge (K true) data
)
-structure HOL4DefMaps = Theory_Data
+structure Importer_DefMaps = Theory_Data
(
type T = string StringPair.table
val empty = StringPair.empty
@@ -129,7 +129,7 @@
fun merge data = StringPair.merge (K true) data
)
-structure HOL4TypeMaps = Theory_Data
+structure Importer_TypeMaps = Theory_Data
(
type T = (bool * string) StringPair.table
val empty = StringPair.empty
@@ -137,7 +137,7 @@
fun merge data = StringPair.merge (K true) data
)
-structure HOL4Pending = Theory_Data
+structure Importer_Pending = Theory_Data
(
type T = ((term * term) list * thm) StringPair.table
val empty = StringPair.empty
@@ -145,7 +145,7 @@
fun merge data = StringPair.merge (K true) data
)
-structure HOL4Rewrites = Theory_Data
+structure Importer_Rewrites = Theory_Data
(
type T = thm list
val empty = []
@@ -153,57 +153,57 @@
val merge = Thm.merge_thms
)
-val hol4_debug = Unsynchronized.ref false
-fun message s = if !hol4_debug then writeln s else ()
+val importer_debug = Unsynchronized.ref false
+fun message s = if !importer_debug then writeln s else ()
-fun add_hol4_rewrite (Context.Theory thy, th) =
+fun add_importer_rewrite (Context.Theory thy, th) =
let
val _ = message "Adding external rewrite"
val th1 = th RS @{thm eq_reflection}
handle THM _ => th
- val current_rews = HOL4Rewrites.get thy
+ val current_rews = Importer_Rewrites.get thy
val new_rews = insert Thm.eq_thm th1 current_rews
- val updated_thy = HOL4Rewrites.put new_rews thy
+ val updated_thy = Importer_Rewrites.put new_rews thy
in
(Context.Theory updated_thy,th1)
end
- | add_hol4_rewrite (context, th) = (context,
+ | add_importer_rewrite (context, th) = (context,
(th RS @{thm eq_reflection} handle THM _ => th)
);
-fun ignore_hol4 bthy bthm thy =
+fun ignore_importer bthy bthm thy =
let
val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
- val curmaps = HOL4Maps.get thy
+ val curmaps = Importer_Maps.get thy
val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
- val upd_thy = HOL4Maps.put newmaps thy
+ val upd_thy = Importer_Maps.put newmaps thy
in
upd_thy
end
-val opt_get_output_thy = #2 o HOL4Dump.get
+val opt_get_output_thy = #2 o Importer_Dump.get
fun get_output_thy thy =
- case #2 (HOL4Dump.get thy) of
+ case #2 (Importer_Dump.get thy) of
"" => error "No theory file being output"
| thyname => thyname
-val get_output_dir = #1 o HOL4Dump.get
+val get_output_dir = #1 o Importer_Dump.get
-fun add_hol4_move bef aft thy =
+fun add_importer_move bef aft thy =
let
- val curmoves = HOL4Moves.get thy
+ val curmoves = Importer_Moves.get thy
val newmoves = Symtab.update_new (bef, aft) curmoves
in
- HOL4Moves.put newmoves thy
+ Importer_Moves.put newmoves thy
end
-fun get_hol4_move bef thy =
- Symtab.lookup (HOL4Moves.get thy) bef
+fun get_importer_move bef thy =
+ Symtab.lookup (Importer_Moves.get thy) bef
fun follow_name thmname thy =
let
- val moves = HOL4Moves.get thy
+ val moves = Importer_Moves.get thy
fun F thmname =
case Symtab.lookup moves thmname of
SOME name => F name
@@ -212,20 +212,20 @@
F thmname
end
-fun add_hol4_cmove bef aft thy =
+fun add_importer_cmove bef aft thy =
let
- val curmoves = HOL4CMoves.get thy
+ val curmoves = Importer_CMoves.get thy
val newmoves = Symtab.update_new (bef, aft) curmoves
in
- HOL4CMoves.put newmoves thy
+ Importer_CMoves.put newmoves thy
end
-fun get_hol4_cmove bef thy =
- Symtab.lookup (HOL4CMoves.get thy) bef
+fun get_importer_cmove bef thy =
+ Symtab.lookup (Importer_CMoves.get thy) bef
fun follow_cname thmname thy =
let
- val moves = HOL4CMoves.get thy
+ val moves = Importer_CMoves.get thy
fun F thmname =
case Symtab.lookup moves thmname of
SOME name => F name
@@ -234,140 +234,140 @@
F thmname
end
-fun add_hol4_mapping bthy bthm isathm thy =
+fun add_importer_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 curmaps = Importer_Maps.get thy
val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
- val upd_thy = HOL4Maps.put newmaps thy
+ val upd_thy = Importer_Maps.put newmaps thy
in
upd_thy
end;
-fun get_hol4_type_mapping bthy tycon thy =
+fun get_importer_type_mapping bthy tycon thy =
let
- val maps = HOL4TypeMaps.get thy
+ val maps = Importer_TypeMaps.get thy
in
StringPair.lookup maps (bthy,tycon)
end
-fun get_hol4_mapping bthy bthm thy =
+fun get_importer_mapping bthy bthm thy =
let
- val curmaps = HOL4Maps.get thy
+ val curmaps = Importer_Maps.get thy
in
StringPair.lookup curmaps (bthy,bthm)
end;
-fun add_hol4_const_mapping bthy bconst internal isaconst thy =
+fun add_importer_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
+ then add_importer_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 curmaps = Importer_ConstMaps.get thy
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
- val upd_thy = HOL4ConstMaps.put newmaps thy
+ val upd_thy = Importer_ConstMaps.put newmaps thy
in
upd_thy
end;
-fun add_hol4_const_renaming bthy bconst newname thy =
+fun add_importer_const_renaming bthy bconst newname thy =
let
- val currens = HOL4Rename.get thy
+ val currens = Importer_Rename.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
+ val upd_thy = Importer_Rename.put newrens thy
in
upd_thy
end;
-fun get_hol4_const_renaming bthy bconst thy =
+fun get_importer_const_renaming bthy bconst thy =
let
- val currens = HOL4Rename.get thy
+ val currens = Importer_Rename.get thy
in
StringPair.lookup currens (bthy,bconst)
end;
-fun get_hol4_const_mapping bthy bconst thy =
+fun get_importer_const_mapping bthy bconst thy =
let
- val bconst = case get_hol4_const_renaming bthy bconst thy of
+ val bconst = case get_importer_const_renaming bthy bconst thy of
SOME name => name
| NONE => bconst
- val maps = HOL4ConstMaps.get thy
+ val maps = Importer_ConstMaps.get thy
in
StringPair.lookup maps (bthy,bconst)
end
-fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
+fun add_importer_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
+ then add_importer_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 curmaps = Importer_ConstMaps.get thy
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
- val upd_thy = HOL4ConstMaps.put newmaps thy
+ val upd_thy = Importer_ConstMaps.put newmaps thy
in
upd_thy
end;
-fun add_hol4_type_mapping bthy bconst internal isaconst thy =
+fun add_importer_type_mapping bthy bconst internal isaconst thy =
let
- val curmaps = HOL4TypeMaps.get thy
+ val curmaps = Importer_TypeMaps.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
+ val upd_thy = Importer_TypeMaps.put newmaps thy
in
upd_thy
end;
-fun add_hol4_pending bthy bthm hth thy =
+fun add_importer_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 curpend = Importer_Pending.get thy
val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
- val upd_thy = HOL4Pending.put newpend thy
+ val upd_thy = Importer_Pending.put newpend thy
val thy' = case opt_get_output_thy upd_thy of
- "" => add_hol4_mapping bthy bthm thmname upd_thy
+ "" => add_importer_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
+ upd_thy |> add_importer_move thmname new_thmname
+ |> add_importer_mapping bthy bthm new_thmname
end
in
thy'
end;
-fun get_hol4_theorem thyname thmname thy =
+fun get_importer_theorem thyname thmname thy =
let
- val isathms = HOL4Thms.get thy
+ val isathms = Importer_Thms.get thy
in
StringPair.lookup isathms (thyname,thmname)
end;
-fun add_hol4_theorem thyname thmname hth =
+fun add_importer_theorem thyname thmname hth =
let
val _ = message ("Adding external theorem " ^ thyname ^ "." ^ thmname)
in
- HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
+ Importer_Thms.map (StringPair.update_new ((thyname, thmname), hth))
end;
-fun export_hol4_pending thy =
+fun export_importer_pending thy =
let
- val rews = HOL4Rewrites.get thy;
- val pending = HOL4Pending.get thy;
+ val rews = Importer_Rewrites.get thy;
+ val pending = Importer_Pending.get thy;
fun process ((bthy,bthm), hth as (_,thm)) thy =
let
val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
@@ -376,68 +376,68 @@
thy
|> Global_Theory.store_thm (Binding.name bthm, thm2)
|> snd
- |> add_hol4_theorem bthy bthm hth
+ |> add_importer_theorem bthy bthm hth
end;
in
thy
|> StringPair.fold process pending
- |> HOL4Pending.put StringPair.empty
+ |> Importer_Pending.put StringPair.empty
end;
fun setup_dump (dir,thyname) thy =
- HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
+ Importer_Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
fun add_dump str thy =
let
- val (dir,thyname,curdump) = HOL4Dump.get thy
+ val (dir,thyname,curdump) = Importer_Dump.get thy
in
- HOL4Dump.put (dir,thyname,str::curdump) thy
+ Importer_Dump.put (dir,thyname,str::curdump) thy
end
fun flush_dump thy =
let
- val (dir,thyname,dumpdata) = HOL4Dump.get thy
+ val (dir,thyname,dumpdata) = Importer_Dump.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
+ Importer_Dump.put ("","",[]) thy
end
fun set_generating_thy thyname thy =
- case HOL4DefThy.get thy of
- NoImport => HOL4DefThy.put (Generating thyname) thy
+ case Importer_DefThy.get thy of
+ NoImport => Importer_DefThy.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
+ case Importer_DefThy.get thy of
+ NoImport => Importer_DefThy.put (Replaying thyname) thy
| _ => error "Import already in progess"
fun clear_import_thy thy =
- case HOL4DefThy.get thy of
+ case Importer_DefThy.get thy of
NoImport => error "No import in progress"
- | _ => HOL4DefThy.put NoImport thy
+ | _ => Importer_DefThy.put NoImport thy
fun get_generating_thy thy =
- case HOL4DefThy.get thy of
+ case Importer_DefThy.get thy of
Generating thyname => thyname
| _ => error "No theory being generated"
fun get_replaying_thy thy =
- case HOL4DefThy.get thy of
+ case Importer_DefThy.get thy of
Replaying thyname => thyname
| _ => error "No theory being replayed"
fun get_import_thy thy =
- case HOL4DefThy.get thy of
+ case Importer_DefThy.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
+ case get_importer_mapping thyname thmname thy of
SOME NONE => true
| _ => false
@@ -468,13 +468,13 @@
then case v
of NONE => (bthm :: ign, map)
| SOME w => (ign, (bthm, w) :: map)
- else (ign, map)) (HOL4Maps.get thy) ([],[]);
+ else (ign, map)) (Importer_Maps.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);
+ val constmaps = mk (Importer_ConstMaps.get thy);
+ val constrenames = mk (Importer_Rename.get thy);
+ val typemaps = mk (Importer_TypeMaps.get thy);
+ val defmaps = mk (Importer_DefMaps.get thy);
fun new_name internal isa =
if internal
then
@@ -565,18 +565,18 @@
fun set_used_names names thy =
let
- val unames = HOL4UNames.get thy
+ val unames = Importer_UNames.get thy
in
case unames of
- [] => HOL4UNames.put names thy
+ [] => Importer_UNames.put names thy
| _ => error "import_rews.set_used_names called on initialized data!"
end
-val clear_used_names = HOL4UNames.put [];
+val clear_used_names = Importer_UNames.put [];
fun get_defmap thyname const thy =
let
- val maps = HOL4DefMaps.get thy
+ val maps = Importer_DefMaps.get thy
in
StringPair.lookup maps (thyname,const)
end
@@ -584,23 +584,23 @@
fun add_defmap thyname const defname thy =
let
val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
- val maps = HOL4DefMaps.get thy
+ val maps = Importer_DefMaps.get thy
val maps' = StringPair.update_new ((thyname,const),defname) maps
- val thy' = HOL4DefMaps.put maps' thy
+ val thy' = Importer_DefMaps.put maps' thy
in
thy'
end
fun get_defname thyname name thy =
let
- val maps = HOL4DefMaps.get thy
+ val maps = Importer_DefMaps.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 used = Importer_UNames.get thy
val defname = Thm.def_name name
val pdefname = name ^ "_primdef"
in
@@ -624,16 +624,16 @@
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"}
+ thy |> add_importer_type_mapping "min" "bool" false @{type_name bool}
+ |> add_importer_type_mapping "min" "fun" false "fun"
+ |> add_importer_type_mapping "min" "ind" false @{type_name ind}
+ |> add_importer_const_mapping "min" "=" false @{const_name HOL.eq}
+ |> add_importer_const_mapping "min" "==>" false @{const_name HOL.implies}
+ |> add_importer_const_mapping "min" "@" false @{const_name "Eps"}
in
-val hol4_setup =
+val importer_setup =
initial_maps #>
Attrib.setup @{binding import_rew}
- (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "external rewrite rule"
+ (Scan.succeed (Thm.mixed_attribute add_importer_rewrite)) "external rewrite rule"
end
--- a/src/HOL/Import/import_syntax.ML Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/import_syntax.ML Sun Mar 04 00:03:04 2012 +0100
@@ -2,7 +2,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-signature HOL4_IMPORT_SYNTAX =
+signature IMPORTER_IMPORT_SYNTAX =
sig
val import_segment: (theory -> theory) parser
val import_theory : (theory -> theory) parser
@@ -22,7 +22,7 @@
val setup : unit -> unit
end
-structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
+structure Importer_Import_Syntax :> IMPORTER_IMPORT_SYNTAX =
struct
(* Parsers *)
@@ -51,7 +51,7 @@
|> set_used_names facts
|> replay
|> clear_used_names
- |> export_hol4_pending
+ |> export_importer_pending
|> Sign.parent_path
|> dump_import_thy thyname
|> add_dump ";end_setup"
@@ -63,7 +63,7 @@
let
val thyname = get_import_thy thy
in
- Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
+ Library.foldl (fn (thy,thmname) => ignore_importer thyname thmname thy) (thy,ignored)
end)
val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
@@ -72,7 +72,7 @@
let
val thyname = get_import_thy thy
in
- Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
+ Library.foldl (fn (thy,(hol,isa)) => add_importer_mapping thyname hol isa thy) (thy,thmmaps)
end)
val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
@@ -81,7 +81,7 @@
let
val thyname = get_import_thy thy
in
- Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
+ Library.foldl (fn (thy,(hol,isa)) => add_importer_type_mapping thyname hol false isa thy) (thy,typmaps)
end)
val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
@@ -99,7 +99,7 @@
let
val thyname = get_import_thy thy
in
- Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
+ Library.foldl (fn (thy,(hol,isa)) => add_importer_const_renaming thyname hol isa thy) (thy,renames)
end)
val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
@@ -108,8 +108,8 @@
let
val thyname = get_import_thy thy
in
- Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol false isa thy
- | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
+ Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol false isa thy
+ | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
end)
val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
@@ -118,8 +118,8 @@
let
val thyname = get_import_thy thy
in
- Library.foldl (fn (thy,((hol,isa),NONE)) => add_hol4_const_mapping thyname hol true isa thy
- | (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
+ Library.foldl (fn (thy,((hol,isa),NONE)) => add_importer_const_mapping thyname hol true isa thy
+ | (thy,((hol,isa),SOME ty)) => add_importer_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
end)
fun import_thy location s =
@@ -172,7 +172,7 @@
>>
(fn (location, thyname) =>
fn thy =>
- (case HOL4DefThy.get thy of
+ (case Importer_DefThy.get thy of
NoImport => thy
| Generating _ => error "Currently generating a theory!"
| Replaying _ => thy |> clear_import_thy)
--- a/src/HOL/Import/proof_kernel.ML Sat Mar 03 23:54:44 2012 +0100
+++ b/src/HOL/Import/proof_kernel.ML Sun Mar 04 00:03:04 2012 +0100
@@ -60,7 +60,7 @@
val content_of : proof -> proof_content
val import_proof : string -> string -> theory -> (theory -> term) option * (theory -> proof)
- val rewrite_hol4_term: Term.term -> theory -> Thm.thm
+ val rewrite_importer_term: Term.term -> theory -> Thm.thm
val type_of : term -> hol_type
@@ -330,14 +330,14 @@
end
fun intern_const_name thyname const thy =
- case get_hol4_const_mapping thyname const thy of
+ case get_importer_const_mapping thyname const thy of
SOME (_,cname,_) => cname
- | NONE => (case get_hol4_const_renaming thyname const thy of
+ | NONE => (case get_importer_const_renaming thyname const thy of
SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname)
| NONE => Sign.intern_const thy (thyname ^ "." ^ const))
fun intern_type_name thyname const thy =
- case get_hol4_type_mapping thyname const thy of
+ case get_importer_type_mapping thyname const thy of
SOME (_,cname) => cname
| NONE => Sign.intern_const thy (thyname ^ "." ^ const)
@@ -357,7 +357,7 @@
fun prim_mk_const thy Thy Nam =
let
val name = intern_const_name Thy Nam thy
- val cmaps = HOL4ConstMaps.get thy
+ val cmaps = Importer_ConstMaps.get thy
in
case StringPair.lookup cmaps (Thy,Nam) of
SOME(_,_,SOME ty) => Const(name,ty)
@@ -585,7 +585,7 @@
case get_segment2 thyname thy of
SOME seg => seg
| NONE => get_import_segment thy
- val path = space_explode ":" (getenv "HOL4_PROOFS")
+ val path = space_explode ":" (getenv "IMPORTER_PROOFS")
fun find [] = NONE
| find (p::ps) =
(let
@@ -1081,12 +1081,12 @@
fun if_debug f x = if !debug then f x else ()
val message = if_debug writeln
-fun get_hol4_thm thyname thmname thy =
- case get_hol4_theorem thyname thmname thy of
+fun get_importer_thm thyname thmname thy =
+ case get_importer_theorem thyname thmname thy of
SOME hth => SOME (HOLThm hth)
| NONE =>
let
- val pending = HOL4Pending.get thy
+ val pending = Importer_Pending.get thy
in
case StringPair.lookup pending (thyname,thmname) of
SOME hth => SOME (HOLThm hth)
@@ -1112,30 +1112,30 @@
end
handle _ => NONE (* FIXME avoid handle _ *)
-fun rewrite_hol4_term t thy =
+fun rewrite_importer_term t thy =
let
- val import_rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
- val hol4ss = Simplifier.global_context thy empty_ss addsimps import_rews1
+ val import_rews1 = map (Thm.transfer thy) (Importer_Rewrites.get thy)
+ val importerss = Simplifier.global_context thy empty_ss addsimps import_rews1
in
- Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
+ Thm.transfer thy (Simplifier.full_rewrite importerss (cterm_of thy t))
end
-fun get_isabelle_thm thyname thmname hol4conc thy =
+fun get_isabelle_thm thyname thmname importerconc thy =
let
- val (info,hol4conc') = disamb_term hol4conc
- val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
+ val (info,importerconc') = disamb_term importerconc
+ val i2h_conc = Thm.symmetric (rewrite_importer_term (HOLogic.mk_Trueprop importerconc') thy)
val isaconc =
case concl_of i2h_conc of
Const("==",_) $ lhs $ _ => lhs
| _ => error "get_isabelle_thm" "Bad rewrite rule"
val _ = (message "Original conclusion:";
- if_debug prin hol4conc';
+ if_debug prin importerconc';
message "Modified conclusion:";
if_debug prin isaconc)
fun mk_res th = HOLThm (rens_of info, Thm.equal_elim i2h_conc th)
in
- case get_hol4_mapping thyname thmname thy of
+ case get_importer_mapping thyname thmname thy of
SOME (SOME thmname) =>
let
val th1 = (SOME (Global_Theory.get_thm thy thmname)
@@ -1167,8 +1167,8 @@
SOME (isaname,th) =>
let
val hth as HOLThm args = mk_res th
- val thy' = thy |> add_hol4_theorem thyname thmname args
- |> add_hol4_mapping thyname thmname isaname
+ val thy' = thy |> add_importer_theorem thyname thmname args
+ |> add_importer_mapping thyname thmname isaname
in
(thy',SOME hth)
end
@@ -1182,19 +1182,19 @@
writeln ("Exception in get_isabelle_thm:\n" ^ ML_Compiler.exn_message e)) ();
(thy,NONE))
-fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
+fun get_isabelle_thm_and_warn thyname thmname importerconc thy =
let
- val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
+ val (a, b) = get_isabelle_thm thyname thmname importerconc thy
fun warn () =
let
- val (info,hol4conc') = disamb_term hol4conc
- val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
+ val (info,importerconc') = disamb_term importerconc
+ val i2h_conc = Thm.symmetric (rewrite_importer_term (HOLogic.mk_Trueprop importerconc') thy)
in
case concl_of i2h_conc of
Const("==",_) $ lhs $ _ =>
(warning ("Failed lookup of theorem '"^thmname^"':");
writeln "Original conclusion:";
- prin hol4conc';
+ prin importerconc';
writeln "Modified conclusion:";
prin lhs)
| _ => ()
@@ -1206,7 +1206,7 @@
end
fun get_thm thyname thmname thy =
- case get_hol4_thm thyname thmname thy of
+ case get_importer_thm thyname thmname thy of
SOME hth => (thy,SOME hth)
| NONE => ((case import_proof_concl thyname thmname thy of
SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
@@ -1215,7 +1215,7 @@
| e as PK _ => (message "PK exception"; (thy,NONE)))
fun rename_const thyname thy name =
- case get_hol4_const_renaming thyname name thy of
+ case get_importer_const_renaming thyname name thy of
SOME cname => cname
| NONE => name
@@ -1236,9 +1236,9 @@
fun intern_store_thm gen_output thyname thmname hth thy =
let
val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
- val rew = rewrite_hol4_term (concl_of th) thy
+ val rew = rewrite_importer_term (concl_of th) thy
val th = Thm.equal_elim rew th
- val thy' = add_hol4_pending thyname thmname args thy
+ val thy' = add_importer_pending thyname thmname args thy
val th = disambiguate_frees th
val th = Object_Logic.rulify th
val thy2 =
@@ -1791,7 +1791,7 @@
val (info,rhs') = disamb_term rhs
val ctype = type_of rhs'
val csyn = mk_syn thy constname
- val thy1 = case HOL4DefThy.get thy of
+ val thy1 = case Importer_DefThy.get thy of
Replaying _ => thy
| _ => Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy
val eq = mk_defeq constname rhs' thy1
@@ -1800,9 +1800,9 @@
val thm' = def_thm RS meta_eq_to_obj_eq_thm
val (thy',th) = (thy2, thm')
val fullcname = Sign.intern_const thy' constname
- val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
+ val thy'' = add_importer_const_mapping thyname constname true fullcname thy'
val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
- val rew = rewrite_hol4_term eq thy''
+ val rew = rewrite_importer_term eq thy''
val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
val thy22 =
if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn
@@ -1828,13 +1828,13 @@
| NONE => raise ERR "new_definition" "Bad conclusion"
val fullname = Sign.full_bname thy22 thmname
val thy22' = case opt_get_output_thy thy22 of
- "" => add_hol4_mapping thyname thmname fullname thy22
+ "" => add_importer_mapping thyname thmname fullname thy22
| output_thy =>
let
val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
in
- thy22 |> add_hol4_move fullname moved_thmname
- |> add_hol4_mapping thyname thmname moved_thmname
+ thy22 |> add_importer_move fullname moved_thmname
+ |> add_importer_mapping thyname thmname moved_thmname
end
val _ = message "new_definition:"
val _ = if_debug pth hth
@@ -1843,7 +1843,7 @@
end
fun new_specification thyname thmname names hth thy =
- case HOL4DefThy.get thy of
+ case Importer_DefThy.get thy of
Replaying _ => (thy,hth)
| _ =>
let
@@ -1852,7 +1852,7 @@
val names = map (rename_const thyname thy) names
val _ = warning ("Introducing constants " ^ commas names)
val (HOLThm(rens,th)) = norm_hthm thy hth
- val thy1 = case HOL4DefThy.get thy of
+ val thy1 = case Importer_DefThy.get thy of
Replaying _ => thy
| _ =>
let
@@ -1892,7 +1892,7 @@
(thy1,th)
val res' = Thm.unvarify_global res
val hth = HOLThm(rens,res')
- val rew = rewrite_hol4_term (concl_of res') thy'
+ val rew = rewrite_importer_term (concl_of res') thy'
val th = Thm.equal_elim rew res'
fun handle_const (name,thy) =
let
@@ -1938,7 +1938,7 @@
val typedef_hol2hollight = @{thm typedef_hol2hollight}
in
fun new_type_definition thyname thmname tycname hth thy =
- case HOL4DefThy.get thy of
+ case Importer_DefThy.get thy of
Replaying _ => (thy,hth)
| _ =>
let
@@ -1960,14 +1960,14 @@
val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4
val fulltyname = Sign.intern_type thy' tycname
- val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
+ val thy'' = add_importer_type_mapping thyname tycname true fulltyname thy'
val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
else ()
- val thy4 = add_hol4_pending thyname thmname args thy''
+ val thy4 = add_importer_pending thyname thmname args thy''
- val rew = rewrite_hol4_term (concl_of td_th) thy4
+ val rew = rewrite_importer_term (concl_of td_th) thy4
val th = Thm.equal_elim rew (Thm.transfer thy4 td_th)
val c = case HOLogic.dest_Trueprop (prop_of th) of
Const(@{const_name Ex},exT) $ P =>
@@ -1987,7 +1987,7 @@
val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
- val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
+ val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2importer [OF type_definition_" ^ tycname ^ "]") thy5
val _ = message "RESULT:"
val _ = if_debug pth hth'
@@ -2004,7 +2004,7 @@
end
fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
- case HOL4DefThy.get thy of
+ case Importer_DefThy.get thy of
Replaying _ => (thy,
HOLThm([], Global_Theory.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
| _ =>
@@ -2042,12 +2042,12 @@
val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse
raise ERR "type_introduction" "no term variables expected any more"
val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
- val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
+ val thy'' = add_importer_type_mapping thyname tycname true fulltyname thy'
val _ = message "step 4"
val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
- val thy4 = add_hol4_pending thyname thmname args thy''
+ val thy4 = add_importer_pending thyname thmname args thy''
- val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
+ val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_importer_term P thy4))) *)
val c =
let
val PT = type_of P'