--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Oct 29 12:49:05 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Oct 29 12:49:05 2010 +0200
@@ -16,7 +16,7 @@
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val untyped_aconv : term -> term -> bool
val replay_one_inference :
- Proof.context -> mode -> (string * term) list
+ Proof.context -> mode -> (string * term) list * int Unsynchronized.ref
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
@@ -93,7 +93,7 @@
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
(*Maps metis terms to isabelle terms*)
-fun hol_term_from_metis_PT ctxt fol_tm =
+fun hol_term_from_metis_PT ctxt new_skolem_var_count fol_tm =
let val thy = ProofContext.theory_of ctxt
val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
Metis_Term.toString fol_tm)
@@ -126,9 +126,11 @@
val nterms = length ts - ntypes
val tts = map tm_to_tt ts
val tys = types_of (List.take(tts,ntypes))
+ val j = !new_skolem_var_count + 1
+ val _ = new_skolem_var_count := j
val t =
if String.isPrefix new_skolem_const_prefix c then
- Var (new_skolem_var_from_const c,
+ Var ((new_skolem_var_name_from_const c, j),
Type_Infer.paramify_vars (tl tys ---> hd tys))
else
Const (c, dummyT)
@@ -162,7 +164,7 @@
end
(*Maps fully-typed metis terms to isabelle terms*)
-fun hol_term_from_metis_FT ctxt fol_tm =
+fun hol_term_from_metis_FT ctxt new_skolem_var_count fol_tm =
let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
Metis_Term.toString fol_tm)
fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
@@ -193,17 +195,17 @@
SOME v => Free (v, dummyT)
| NONE => (trace_msg ctxt (fn () =>
"hol_term_from_metis_FT bad const: " ^ x);
- hol_term_from_metis_PT ctxt t))
+ hol_term_from_metis_PT ctxt new_skolem_var_count t))
| cvt t = (trace_msg ctxt (fn () =>
"hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
- hol_term_from_metis_PT ctxt t)
+ hol_term_from_metis_PT ctxt new_skolem_var_count t)
in fol_tm |> cvt end
fun hol_term_from_metis FT = hol_term_from_metis_FT
| hol_term_from_metis _ = hol_term_from_metis_PT
-fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
- let val ts = map (hol_term_from_metis mode ctxt) fol_tms
+fun hol_terms_from_metis ctxt mode (old_skolems, new_skolem_var_count) fol_tms =
+ let val ts = map (hol_term_from_metis mode ctxt new_skolem_var_count) fol_tms
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
@@ -249,17 +251,18 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
in cterm_instantiate substs th end;
-fun assume_inf ctxt mode old_skolems atm =
+fun assume_inf ctxt mode skolem_params atm =
inst_excluded_middle
(ProofContext.theory_of ctxt)
- (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
+ (singleton (hol_terms_from_metis ctxt mode skolem_params)
+ (Metis_Term.Fn atm))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
to reconstruct them admits new possibilities of errors, e.g. concerning
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inf ctxt mode old_skolems thpairs fsubst th =
+fun inst_inf ctxt mode (old_skolems, new_skolem_var_count) thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
@@ -267,7 +270,7 @@
fun subst_translation (x,y) =
let val v = find_var x
(* We call "reveal_old_skolem_terms" and "infer_types" below. *)
- val t = hol_term_from_metis mode ctxt y
+ val t = hol_term_from_metis mode ctxt new_skolem_var_count y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
@@ -375,7 +378,7 @@
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
val select_literal = negate_head oo make_last
-fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
+fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
@@ -390,7 +393,7 @@
else
let
val i_atm =
- singleton (hol_terms_from_fol ctxt mode old_skolems)
+ singleton (hol_terms_from_metis ctxt mode skolem_params)
(Metis_Term.Fn atm)
val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
@@ -415,9 +418,9 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inf ctxt mode old_skolems t =
+fun refl_inf ctxt mode skolem_params t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
+ val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
@@ -433,10 +436,10 @@
| get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
-fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
+fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis_Term.Fn atm
- val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
+ val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr]
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -515,17 +518,17 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step ctxt mode old_skolems thpairs p =
+fun step ctxt mode skolem_params thpairs p =
case p of
(fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
- | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
+ | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolem_params f_atm
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
+ factor (inst_inf ctxt mode skolem_params thpairs f_subst f_th1)
| (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
- factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
- | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
+ factor (resolve_inf ctxt mode skolem_params thpairs f_atm f_th1 f_th2)
+ | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolem_params f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inf ctxt mode old_skolems f_lit f_p f_r
+ equality_inf ctxt mode skolem_params f_lit f_p f_r
fun flexflex_first_order th =
case Thm.tpairs_of th of
@@ -545,12 +548,12 @@
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
-fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
+fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
let
val _ = trace_msg ctxt (fn () => "=============================================")
val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = step ctxt mode old_skolems thpairs (fol_th, inf)
+ val th = step ctxt mode skolem_params thpairs (fol_th, inf)
|> flexflex_first_order
val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg ctxt (fn () => "=============================================")
--- a/src/HOL/Tools/Metis/metis_translate.ML Fri Oct 29 12:49:05 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Oct 29 12:49:05 2010 +0200
@@ -59,7 +59,7 @@
val make_fixed_type_const : string -> string
val make_type_class : string -> string
val num_type_args: theory -> string -> int
- val new_skolem_var_from_const: string -> indexname
+ val new_skolem_var_name_from_const : string -> string
val type_literals_for_types : typ list -> type_literal list
val make_class_rel_clauses :
theory -> class list -> class list -> class_rel_clause list
@@ -214,9 +214,9 @@
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-fun new_skolem_var_from_const s =
+fun new_skolem_var_name_from_const s =
let val ss = s |> space_explode Long_Name.separator in
- (nth ss (length ss - 2), 0)
+ nth ss (length ss - 2)
end