# HG changeset patch # User blanchet # Date 1321613232 -3600 # Node ID eb30a549054356c3f41ba156ff1f8cd805b24998 # Parent 211a6e6cbc04becc97a638833fcee5b9eb5d91af wrap lambdas earlier, to get more control over beta/eta diff -r 211a6e6cbc04 -r eb30a5490543 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 = diff -r 211a6e6cbc04 -r eb30a5490543 src/HOL/Tools/Metis/metis_tactic.ML --- 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 diff -r 211a6e6cbc04 -r eb30a5490543 src/HOL/Tools/Metis/metis_translate.ML --- 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 ([], []) (*