--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200
@@ -556,7 +556,7 @@
(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
appear in the formula. *)
-fun raw_prop_from_atp ctxt textual sym_tab phi =
+fun prop_from_atp ctxt textual sym_tab phi =
let
fun do_formula pos phi =
case phi of
@@ -587,9 +587,9 @@
#> Syntax.check_term
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
-fun prop_from_atp ctxt textual sym_tab =
+fun uncombined_etc_prop_from_atp ctxt textual sym_tab =
let val thy = Proof_Context.theory_of ctxt in
- raw_prop_from_atp ctxt textual sym_tab
+ prop_from_atp ctxt textual sym_tab
#> textual ? uncombine_term thy #> infer_formula_types ctxt
end
@@ -601,12 +601,11 @@
fun decode_line sym_tab (Definition (name, phi1, phi2)) ctxt =
let
val thy = Proof_Context.theory_of ctxt
- (* FIXME: prop or term? *)
- val t1 = raw_prop_from_atp ctxt true sym_tab phi1
+ val t1 = prop_from_atp ctxt true sym_tab phi1
val vars = snd (strip_comb t1)
val frees = map unvarify_term vars
val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = raw_prop_from_atp ctxt true sym_tab phi2
+ val t2 = prop_from_atp ctxt true sym_tab phi2
val (t1, t2) =
HOLogic.eq_const HOLogic.typeT $ t1 $ t2
|> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
@@ -616,7 +615,7 @@
fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
end
| decode_line sym_tab (Inference (name, u, deps)) ctxt =
- let val t = u |> prop_from_atp ctxt true sym_tab in
+ let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in
(Inference (name, t, deps),
fold Variable.declare_term (OldTerm.term_frees t) ctxt)
end
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200
@@ -18,7 +18,8 @@
val verbose : bool Config.T
val verbose_warning : Proof.context -> string -> unit
val hol_clause_from_metis :
- Proof.context -> int Symtab.table -> Metis_Thm.thm -> term
+ Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
+ -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val untyped_aconv : term * term -> bool
val replay_one_inference :
@@ -74,7 +75,7 @@
end;
fun infer_types ctxt =
- Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt);
+ Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
(* We use 1 rather than 0 because variable references in clauses may otherwise
conflict with variable constraints in the goal...at least, type inference
@@ -223,7 +224,8 @@
| atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
fun hol_term_from_metis_MX ctxt sym_tab =
- atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
+ atp_term_from_metis
+ #> term_from_atp ctxt false sym_tab NONE
fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt
| hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt
@@ -236,19 +238,24 @@
| atp_clause_from_metis lits =
lits |> map atp_literal_from_metis |> mk_aconns AOr
-fun hol_clause_from_metis ctxt sym_tab =
+fun reveal_old_skolems_and_infer_types ctxt old_skolems =
+ map (reveal_old_skolem_terms old_skolems)
+ #> infer_types ctxt
+
+fun hol_clause_from_metis ctxt sym_tab old_skolems =
Metis_Thm.clause
#> Metis_LiteralSet.toList
#> atp_clause_from_metis
#> prop_from_atp ctxt false sym_tab
+ #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
let val ts = map (hol_term_from_metis ctxt mode sym_tab) 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
- val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
- |> infer_types ctxt
+ val ts' =
+ ts |> reveal_old_skolems_and_infer_types ctxt old_skolems
val _ = app (fn t => trace_msg ctxt
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
@@ -308,7 +315,7 @@
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
+ (* We call "reveal_old_skolems_and_infer_types" below. *)
val t = hol_term_from_metis ctxt mode sym_tab y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
@@ -327,9 +334,9 @@
| NONE => SOME (a,t) (*internal Metis var?*)
val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
- val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
- val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
- |> infer_types ctxt
+ val (vars, tms) =
+ ListPair.unzip (map_filter subst_translation substs)
+ ||> reveal_old_skolems_and_infer_types ctxt old_skolems
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = trace_msg ctxt (fn () =>
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200
@@ -59,9 +59,9 @@
"t => t'", where "t" and "t'" are the same term modulo type tags.
In Isabelle, type tags are stripped away, so we are left with "t = t" or
"t => t". Type tag idempotence is also handled this way. *)
-fun reflexive_or_trivial_from_metis ctxt sym_tab mth =
+fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth =
let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_from_metis ctxt sym_tab mth of
+ case hol_clause_from_metis ctxt sym_tab old_skolems mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
| Const (@{const_name disj}, _) $ t1 $ t2 =>
@@ -105,7 +105,7 @@
val (mode, sym_tab, {axioms, old_skolems, ...}) =
prepare_metis_problem ctxt mode type_sys cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
- reflexive_or_trivial_from_metis ctxt sym_tab mth
+ reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
| get_isa_thm _ (Isa_Raw ith) = ith
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")