# HG changeset patch # User blanchet # Date 1321391619 -3600 # Node ID 9b0f8ca4388e0212632caf6da1bd5eeaf329772f # Parent 96696c360b3eebab51b7f7bdebb78ca98c6629f4 continued implementation of lambda-lifting in Metis diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Metis.thy --- a/src/HOL/Metis.thy Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Metis.thy Tue Nov 15 22:13:39 2011 +0100 @@ -15,7 +15,7 @@ ("Tools/try_methods.ML") begin -subsection {* Literal selection helpers *} +subsection {* Literal selection and lambda-lifting helpers *} definition select :: "'a \ 'a" where [no_atp]: "select = (\x. x)" @@ -31,6 +31,12 @@ lemma select_FalseI: "False \ select False" by simp +definition lambda :: "'a \ 'a" where +[no_atp]: "lambda = (\x. x)" + +lemma eq_lambdaI: "x \ y \ x \ lambda y" +unfolding lambda_def by assumption + subsection {* Metis package *} @@ -40,10 +46,11 @@ setup {* Metis_Tactic.setup *} -hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select +hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fequal_def select_def not_atomize atomize_not_select not_atomize_select - select_FalseI + select_FalseI lambda_def eq_lambdaI + subsection {* Try Methods *} diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100 @@ -283,26 +283,26 @@ constrained by information from type literals, or by type inference. *) fun typ_from_atp ctxt (u as ATerm (a, us)) = let val Ts = map (typ_from_atp ctxt) us in - case strip_prefix_and_unascii type_const_prefix a of + case unprefix_and_unascii type_const_prefix a of SOME b => Type (invert_const b, Ts) | NONE => if not (null us) then raise HO_TERM [u] (* only "tconst"s have type arguments *) - else case strip_prefix_and_unascii tfree_prefix a of + else case unprefix_and_unascii tfree_prefix a of SOME b => make_tfree ctxt b | NONE => (* Could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018". Sometimes variables from the ATP are indistinguishable from Isabelle variables, which forces us to use a type parameter in all cases. *) - (a |> perhaps (strip_prefix_and_unascii tvar_prefix), HOLogic.typeS) + (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS) |> Type_Infer.param 0 end (* Type class literal applied to a type. Returns triple of polarity, class, type. *) fun type_constraint_from_term ctxt (u as ATerm (a, us)) = - case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of + case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of (SOME b, [T]) => (b, T) | _ => raise HO_TERM [u] @@ -335,6 +335,8 @@ fun num_type_args thy s = if String.isPrefix skolem_const_prefix s then s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the + else if String.isPrefix lambda_lifted_prefix s then + if String.isPrefix lambda_lifted_poly_prefix s then 2 else 0 else (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length @@ -364,7 +366,7 @@ else list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts) end - else case strip_prefix_and_unascii const_prefix s of + else case unprefix_and_unascii const_prefix s of SOME s' => let val ((s', s''), mangled_us) = @@ -429,12 +431,10 @@ SOME T => map slack_fastype_of term_ts ---> T | NONE => map slack_fastype_of ts ---> HOLogic.typeT val t = - case strip_prefix_and_unascii fixed_var_prefix s of - SOME s => - (* FIXME: reconstruction of lambda-lifting *) - Free (s, T) + case unprefix_and_unascii fixed_var_prefix s of + SOME s => Free (s, T) | NONE => - case strip_prefix_and_unascii schematic_var_prefix s of + case unprefix_and_unascii schematic_var_prefix s of SOME s => Var ((s, var_index), T) | NONE => Var ((s |> textual ? repair_variable_name Char.toLower, diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 22:13:39 2011 +0100 @@ -46,6 +46,8 @@ val type_const_prefix : string val class_prefix : string val lambda_lifted_prefix : string + val lambda_lifted_mono_prefix : string + val lambda_lifted_poly_prefix : string val skolem_const_prefix : string val old_skolem_const_prefix : string val new_skolem_const_prefix : string @@ -59,6 +61,7 @@ val class_rel_clause_prefix : string val arity_clause_prefix : string val tfree_clause_prefix : string + val lambda_fact_prefix : string val typed_helper_suffix : string val untyped_helper_suffix : string val type_tag_idempotence_helper_name : string @@ -72,7 +75,7 @@ val prefixed_type_tag_name : string val ascii_of : string -> string val unascii_of : string -> string - val strip_prefix_and_unascii : string -> string -> string option + val unprefix_and_unascii : string -> string -> string option val proxy_table : (string * (string * (thm * (string * string)))) list val proxify_const : string -> (string * string) option val invert_const : string -> string @@ -228,7 +231,7 @@ (* If string s has the prefix s1, return the result of deleting it, un-ASCII'd. *) -fun strip_prefix_and_unascii s1 s = +fun unprefix_and_unascii s1 s = if String.isPrefix s1 s then SOME (unascii_of (String.extract (s, size s1, NONE))) else @@ -488,7 +491,7 @@ fun robust_const_type thy s = if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"} - else if String.isPrefix lambda_lifted_poly_prefix s then + else if String.isPrefix lambda_lifted_prefix s then Logic.varifyT_global @{typ "'a => 'b"} else (* Old Skolems throw a "TYPE" exception here, which will be caught. *) @@ -500,8 +503,11 @@ let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end else if String.isPrefix old_skolem_const_prefix s then [] |> Term.add_tvarsT T |> rev |> map TVar - else if String.isPrefix lambda_lifted_poly_prefix s then - let val (T1, T2) = T |> dest_funT in [T1, T2] end + else if String.isPrefix lambda_lifted_prefix s then + if String.isPrefix lambda_lifted_poly_prefix s then + let val (T1, T2) = T |> dest_funT in [T1, T2] end + else + [] else (s, T) |> Sign.const_typargs thy @@ -678,16 +684,21 @@ (if String.isPrefix lambda_lifted_prefix s then Const else Free) x | constify_lifted t = t +(* Requires bound variables to have distinct names and not to clash with any + schematic variables (as should be the case right after lambda-lifting). *) +fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) = + open_form (subst_bound (Var ((s, 0), T), t)) + | open_form t = t + fun lift_lambdas ctxt type_enc = - map (close_form o Envir.eta_contract) #> rpair ctxt + map (Envir.eta_contract #> close_form) #> rpair ctxt #-> Lambda_Lifting.lift_lambdas (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then lambda_lifted_poly_prefix else lambda_lifted_mono_prefix)) Lambda_Lifting.is_quantifier - #> fst - #> pairself (map constify_lifted) + #> fst #> pairself (map (open_form o constify_lifted)) fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) = intentionalize_def t @@ -968,7 +979,7 @@ fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2) | mangle (tm as IConst (_, _, [])) = tm | mangle (tm as IConst (name as (s, _), T, T_args)) = - (case strip_prefix_and_unascii const_prefix s of + (case unprefix_and_unascii const_prefix s of NONE => tm | SOME s'' => case type_arg_policy type_enc (invert_const s'') of @@ -1004,7 +1015,7 @@ fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2) | filt _ (tm as IConst (_, _, [])) = tm | filt ary (IConst (name as (s, _), T, T_args)) = - (case strip_prefix_and_unascii const_prefix s of + (case unprefix_and_unascii const_prefix s of NONE => (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then @@ -1223,7 +1234,7 @@ (** Finite and infinite type inference **) fun tvar_footprint thy s ary = - (case strip_prefix_and_unascii const_prefix s of + (case unprefix_and_unascii const_prefix s of SOME s => s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst |> map (fn T => Term.add_tvarsT T [] |> map fst) @@ -1446,7 +1457,7 @@ case Symtab.lookup sym_tab s of SOME ({min_ary, ...} : sym_info) => min_ary | NONE => - case strip_prefix_and_unascii const_prefix s of + case unprefix_and_unascii const_prefix s of SOME s => let val s = s |> unmangled_const_name |> invert_const in if s = predicator_name then 1 @@ -1581,7 +1592,7 @@ not (null (Term.hidden_polymorphism t)) fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) = - case strip_prefix_and_unascii const_prefix s of + case unprefix_and_unascii const_prefix s of SOME mangled_s => let val thy = Proof_Context.theory_of ctxt @@ -1657,21 +1668,37 @@ fun type_constrs_of_terms thy ts = Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty) -val extract_lambda_def = - let - fun extr [] (@{const Trueprop} $ t) = extr [] t - | extr bs (Const (@{const_name All}, _) $ Abs (s, T, t)) = - extr ((s, T) :: bs) t - | extr bs (Const (@{const_name HOL.eq}, _) $ t $ u) = - (t |> head_of |> dest_Const |> fst, - fold_rev (fn (s, T) => fn u => Abs (s, T, u)) bs u) - | extr _ _ = raise Fail "malformed lifted lambda" - in extr [] end +fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) = + let val (head, args) = strip_comb t in + (head |> dest_Const |> fst, + fold_rev (fn t as Var ((s, _), T) => + (fn u => Abs (s, T, abstract_over (t, u))) + | _ => raise Fail "expected Var") args u) + end + | extract_lambda_def _ = raise Fail "malformed lifted lambda" -fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc +fun translate_formulas ctxt format prem_kind type_enc lambda_trans presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt + val trans_lambdas = + if lambda_trans = no_lambdasN then + rpair [] + else if lambda_trans = concealedN then + lift_lambdas ctxt type_enc ##> K [] + else if lambda_trans = liftingN then + lift_lambdas ctxt type_enc + else if lambda_trans = combinatorsN then + map (introduce_combinators ctxt) #> rpair [] + else if lambda_trans = hybridN then + lift_lambdas ctxt type_enc + ##> maps (fn t => [t, introduce_combinators ctxt + (intentionalize_def t)]) + else if lambda_trans = lambdasN then + map (Envir.eta_contract) #> rpair [] + else + error ("Unknown lambda translation method: " ^ + quote lambda_trans ^ ".") val presimp_consts = Meson.presimplified_consts ctxt val fact_ts = facts |> map snd (* Remove existing facts from the conjecture, as this can dramatically @@ -1685,13 +1712,15 @@ |> map (apsnd freeze_term) |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts) val ((conjs, facts), lambda_facts) = - if preproc then - conjs @ facts - |> map (apsnd (uncurry (presimp_prop ctxt presimp_consts))) - |> preprocess_abstractions_in_terms trans_lambdas - |>> chop (length conjs) - else - ((conjs, facts), []) + (conjs, facts) + |> presimp + ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))) + |> (if lambda_trans = no_lambdasN then + rpair [] + else + op @ + #> preprocess_abstractions_in_terms trans_lambdas + #>> chop (length conjs)) val conjs = conjs |> make_conjecture ctxt format type_enc val (fact_names, facts) = facts @@ -2115,7 +2144,7 @@ val (T, T_args) = if null T_args then (T, []) - else case strip_prefix_and_unascii const_prefix s of + else case unprefix_and_unascii const_prefix s of SOME s' => let val s' = s' |> invert_const @@ -2323,27 +2352,9 @@ \encoding.") else lambda_trans - val trans_lambdas = - if lambda_trans = no_lambdasN then - rpair [] - else if lambda_trans = concealedN then - lift_lambdas ctxt type_enc ##> K [] - else if lambda_trans = liftingN then - lift_lambdas ctxt type_enc - else if lambda_trans = combinatorsN then - map (introduce_combinators ctxt) #> rpair [] - else if lambda_trans = hybridN then - lift_lambdas ctxt type_enc - ##> maps (fn t => [t, introduce_combinators ctxt - (intentionalize_def t)]) - else if lambda_trans = lambdasN then - map (Envir.eta_contract) #> rpair [] - else - error ("Unknown lambda translation method: " ^ - quote lambda_trans ^ ".") val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses, lifted) = - translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc + translate_formulas ctxt format prem_kind type_enc lambda_trans preproc hyp_ts concl_t facts val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Tue Nov 15 22:13:39 2011 +0100 @@ -268,7 +268,8 @@ fun close_form t = fold (fn ((x, i), T) => fn t' => - HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) + HOLogic.all_const T + $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) (Term.add_vars t []) t fun monomorphic_term subst = diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Nov 15 22:13:39 2011 +0100 @@ -10,6 +10,7 @@ val new_skolem_var_prefix : string val new_nonskolem_var_prefix : string val is_zapped_var_name : string -> bool + val is_quasi_lambda_free : term -> bool val introduce_combinators_in_cterm : cterm -> thm val introduce_combinators_in_theorem : thm -> thm val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool @@ -174,7 +175,7 @@ (warning ("Error in the combinator translation of " ^ Display.string_of_thm_without_context th ^ "\nException message: " ^ msg ^ "."); - (* A type variable of sort "{}" will make abstraction fail. *) + (* A type variable of sort "{}" will make "abstraction" fail. *) TrueI) (*cterms are used throughout for efficiency*) diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100 @@ -57,8 +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_lambda_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 = @@ -146,10 +145,10 @@ NONE) fun remove_typeinst (a, t) = let val a = Metis_Name.toString a in - case strip_prefix_and_unascii schematic_var_prefix a of + case unprefix_and_unascii schematic_var_prefix a of SOME b => SOME (b, t) | NONE => - case strip_prefix_and_unascii tvar_prefix a of + case unprefix_and_unascii tvar_prefix a of SOME _ => NONE (* type instantiations are forbidden *) | NONE => SOME (a, t) (* internal Metis var? *) end @@ -337,7 +336,7 @@ | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = let val s = s |> Metis_Name.toString - |> perhaps (try (strip_prefix_and_unascii const_prefix + |> perhaps (try (unprefix_and_unascii const_prefix #> the #> unmangled_const_name)) in if s = metis_predicator orelse s = predicator_name orelse diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:13:39 2011 +0100 @@ -86,10 +86,34 @@ | Const (@{const_name disj}, _) $ t1 $ t2 => (if can HOLogic.dest_not t1 then t2 else t1) |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial - | _ => raise Fail "unexpected tags sym clause" + | _ => raise Fail "expected reflexive or trivial clause" end |> Meson.make_meta_clause +fun lambda_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 + val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth + 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 = + if Meson_Clausify.is_quasi_lambda_free (prop_of th) then + th + else + let + fun conv wrap ctxt ct = + if Meson_Clausify.is_quasi_lambda_free (term_of ct) then + Thm.reflexive ct + else case term_of ct of + Abs _ => + Conv.abs_conv (conv false o snd) ctxt ct + |> wrap ? (fn th => th RS @{thm Metis.eq_lambdaI}) + | _ => Conv.comb_conv (conv true ctxt) ct + val eqth = conv true ctxt (cprop_of th) + in Thm.equal_elim eqth th end + val clause_params = {ordering = Metis_KnuthBendixOrder.default, orderLiterals = Metis_Clause.UnsignedLiteralOrder, @@ -126,7 +150,11 @@ prepare_metis_problem ctxt type_enc lambda_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 _ (Isa_Raw ith) = ith + | 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 |> lambda_trans = liftingN + ? introduce_lambda_wrappers_in_theorem ctxt val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") val _ = app (fn (_, th) => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) axioms diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:13:39 2011 +0100 @@ -13,6 +13,7 @@ datatype isa_thm = Isa_Reflexive_or_Trivial | + Isa_Lambda_Lifted | Isa_Raw of thm val metis_equal : string @@ -114,10 +115,12 @@ | t => t) fun reveal_lambda_lifted lambdas = - map_aterms (fn t as Free (s, _) => + map_aterms (fn t as Const (s, _) => if String.isPrefix lambda_lifted_prefix s then case AList.lookup (op =) lambdas s of - SOME t => t |> map_types (map_type_tvar (K dummyT)) + SOME t => + Const (@{const_name Metis.lambda}, dummyT) + $ map_types (map_type_tvar (K dummyT)) t | NONE => t else t @@ -130,6 +133,7 @@ datatype isa_thm = Isa_Reflexive_or_Trivial | + Isa_Lambda_Lifted | Isa_Raw of thm val proxy_defs = map (fst o snd o snd) proxy_table @@ -183,9 +187,17 @@ | _ => raise Fail ("malformed helper identifier " ^ quote ident) else case try (unprefix fact_prefix) ident of SOME s => - let - val j = s |> space_explode "_" |> List.last |> Int.fromString |> the - in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end + let val s = s |> space_explode "_" |> tl |> space_implode "_" + in + case Int.fromString s of + SOME j => + Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some + | NONE => + if String.isPrefix lambda_fact_prefix (unascii_of s) then + Isa_Lambda_Lifted |> some + else + raise Fail ("malformed fact identifier " ^ quote ident) + end | NONE => TrueI |> Isa_Raw |> some end | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula" @@ -221,12 +233,11 @@ tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt o snd) props)) *) - val (lambda_trans, preproc) = - if lambda_trans = combinatorsN then (no_lambdasN, false) - else (lambda_trans, true) + val lambda_trans = + if lambda_trans = combinatorsN then no_lambdasN else lambda_trans val (atp_problem, _, _, _, _, _, lifted, sym_tab) = prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans - false preproc [] @{prop False} props + false false [] @{prop False} props (* val _ = tracing ("ATP PROBLEM: " ^ cat_lines (lines_for_atp_problem CNF atp_problem)) diff -r 96696c360b3e -r 9b0f8ca4388e src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/cnf_funcs.ML Tue Nov 15 22:13:39 2011 +0100 @@ -261,8 +261,7 @@ val thy = Proof_Context.theory_of ctxt fun conv ctxt ct = case term_of ct of - (t1 as Const _) $ (t2 as Abs _) => - Conv.comb_conv (conv ctxt) ct + Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct | Abs _ => Conv.abs_conv (conv o snd) ctxt ct | Const _ => Conv.all_conv ct | t => make t RS eq_reflection