--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Nov 18 11:47:12 2011 +0100
@@ -57,7 +57,7 @@
lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
fun polish_hol_terms ctxt (lifted, old_skolems) =
- map (reveal_lambda_lifted lifted #> reveal_old_skolem_terms old_skolems)
+ map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Nov 18 11:47:12 2011 +0100
@@ -59,7 +59,7 @@
end
|> Meson.make_meta_clause
-fun lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth =
+fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
let
val thy = Proof_Context.theory_of ctxt
val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
@@ -67,7 +67,7 @@
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
-fun introduce_lambda_wrappers_in_theorem ctxt th =
+fun introduce_lam_wrappers ctxt th =
if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
th
else
@@ -104,8 +104,11 @@
let val thy = Proof_Context.theory_of ctxt
val new_skolemizer =
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
- val cls = cls |> map Drule.eta_contraction_rule
- val ths0 = ths0 |> map Drule.eta_contraction_rule
+ val preproc =
+ Drule.eta_contraction_rule
+ #> lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
+ val cls = cls |> map preproc
+ val ths0 = ths0 |> map preproc
val th_cls_pairs =
map2 (fn j => fn th =>
(Thm.get_name_hint th,
@@ -118,16 +121,14 @@
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val type_enc = type_enc_from_string Sound type_enc
- val (sym_tab, axioms0, concealed) =
+ val (sym_tab, axioms, concealed) =
prepare_metis_problem ctxt type_enc lam_trans cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
| get_isa_thm mth Isa_Lambda_Lifted =
- lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth
- | get_isa_thm _ (Isa_Raw ith) =
- ith |> lam_trans = lam_liftingN
- ? introduce_lambda_wrappers_in_theorem ctxt
- val axioms = axioms0 |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
+ lam_lifted_from_metis ctxt type_enc sym_tab concealed 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 () => "ISABELLE CLAUSES")
val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
val _ = trace_msg ctxt (fn () => "METIS CLAUSES")
@@ -149,9 +150,7 @@
val result =
axioms
|> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof
- val used =
- proof |> map_filter (used_axioms axioms0)
- |> map_filter (fn Isa_Raw ith => SOME ith | _ => NONE)
+ val used = proof |> map_filter (used_axioms axioms)
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
val names = th_cls_pairs |> map fst
--- a/src/HOL/Tools/Metis/metis_translate.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Nov 18 11:47:12 2011 +0100
@@ -28,7 +28,7 @@
val verbose_warning : Proof.context -> string -> unit
val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
- val reveal_lambda_lifted : (string * term) list -> term -> term
+ val reveal_lam_lifted : (string * term) list -> term -> term
val prepare_metis_problem :
Proof.context -> type_enc -> string -> thm list -> thm list
-> int Symtab.table * (Metis_Thm.thm * isa_thm) list
@@ -110,14 +110,14 @@
t
| t => t)
-fun reveal_lambda_lifted lambdas =
+fun reveal_lam_lifted lambdas =
map_aterms (fn t as Const (s, _) =>
if String.isPrefix lam_lifted_prefix s then
case AList.lookup (op =) lambdas s of
SOME t =>
Const (@{const_name Metis.lambda}, dummyT)
$ map_types (map_type_tvar (K dummyT))
- (reveal_lambda_lifted lambdas t)
+ (reveal_lam_lifted lambdas t)
| NONE => t
else
t
@@ -199,6 +199,14 @@
end
| metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
+fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
+ eliminate_lam_wrappers t
+ | eliminate_lam_wrappers (t $ u) =
+ eliminate_lam_wrappers t $ eliminate_lam_wrappers u
+ | eliminate_lam_wrappers (Abs (s, T, t)) =
+ Abs (s, T, eliminate_lam_wrappers t)
+ | eliminate_lam_wrappers t = t
+
(* Function to generate metis clauses, including comb and type clauses *)
fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
let
@@ -223,6 +231,7 @@
fold_rev (fn (name, th) => fn (old_skolems, props) =>
th |> prop_of |> Logic.strip_imp_concl
|> conceal_old_skolem_terms (length clauses) old_skolems
+ ||> lam_trans = lam_liftingN ? eliminate_lam_wrappers
||> (fn prop => (name, prop) :: props))
clauses ([], [])
(*