# HG changeset patch # User blanchet # Date 1282568057 -7200 # Node ID e063be321438efb694667864dc857d91813d0528 # Parent 8aadda8e133817b19bbd5e69ba1f3ba70549cce4 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes diff -r 8aadda8e1338 -r e063be321438 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 23 14:51:56 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 23 14:54:17 2010 +0200 @@ -141,7 +141,6 @@ hol_context -> bool -> styp -> int -> styp val sel_no_from_name : string -> int val close_form : term -> term - val eta_expand : typ list -> term -> int -> term val distinctness_formula : typ -> term list -> term val register_frac_type : string -> (string * string) list -> morphism -> Context.generic @@ -919,14 +918,6 @@ | aux zs t = close_up zs (Term.add_vars t zs) t in aux [] end -fun eta_expand _ t 0 = t - | eta_expand Ts (Abs (s, T, t')) n = - Abs (s, T, eta_expand (T :: Ts) t' (n - 1)) - | eta_expand Ts t n = - fold_rev (curry3 Abs ("x" ^ nat_subscript n)) - (List.take (binder_types (fastype_of1 (Ts, t)), n)) - (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) - fun distinctness_formula T = all_distinct_unordered_pairs_of #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2)) diff -r 8aadda8e1338 -r e063be321438 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Aug 23 14:51:56 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Aug 23 14:54:17 2010 +0200 @@ -52,6 +52,7 @@ val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option + val nat_subscript : int -> string val flip_polarity : polarity -> polarity val prop_T : typ val bool_T : typ @@ -67,7 +68,7 @@ val monomorphic_term : Type.tyenv -> term -> term val specialize_type : theory -> string * typ -> term -> term val varify_type : Proof.context -> typ -> typ - val nat_subscript : int -> string + val eta_expand : typ list -> term -> int -> term val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b val DETERM_TIMEOUT : Time.time option -> tactic -> tactic val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b @@ -237,6 +238,18 @@ val parse_bool_option = Sledgehammer_Util.parse_bool_option val parse_time_option = Sledgehammer_Util.parse_time_option +val i_subscript = implode o map (prefix "\<^isub>") o explode +fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>" +fun nat_subscript n = + let val s = signed_string_of_int n in + if print_mode_active Symbol.xsymbolsN then + (* cheap trick to ensure proper alphanumeric ordering for one- and + two-digit numbers *) + (if n <= 9 then be_subscript else i_subscript) s + else + s + end + fun flip_polarity Pos = Neg | flip_polarity Neg = Pos | flip_polarity Neut = Neut @@ -258,17 +271,7 @@ Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] |> snd |> the_single |> dest_Const |> snd -val i_subscript = implode o map (prefix "\<^isub>") o explode -fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>" -fun nat_subscript n = - let val s = signed_string_of_int n in - if print_mode_active Symbol.xsymbolsN then - (* cheap trick to ensure proper alphanumeric ordering for one- and - two-digit numbers *) - (if n <= 9 then be_subscript else i_subscript) s - else - s - end +val eta_expand = Sledgehammer_Util.eta_expand fun time_limit NONE = I | time_limit (SOME delay) = TimeLimit.timeLimit delay diff -r 8aadda8e1338 -r e063be321438 src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 23 14:51:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 23 14:54:17 2010 +0200 @@ -7,7 +7,6 @@ signature CLAUSIFIER = sig - val transform_elim_theorem : thm -> thm val extensionalize_theorem : thm -> thm val introduce_combinators_in_cterm : cterm -> thm val introduce_combinators_in_theorem : thm -> thm @@ -25,7 +24,7 @@ (* Converts an elim-rule into an equivalent theorem that does not have the predicate variable. Leaves other theorems unchanged. We simply instantiate the conclusion variable to False. (Cf. "transform_elim_term" in - "ATP_Systems".) *) + "Sledgehammer_Util".) *) fun transform_elim_theorem th = case concl_of th of (*conclusion variable*) @{const Trueprop} $ (v as Var (_, @{typ bool})) => @@ -78,10 +77,6 @@ (**** REPLACING ABSTRACTIONS BY COMBINATORS ****) -(*Returns the vars of a theorem*) -fun vars_of_thm th = - map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); - val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} (* Removes the lambdas from an equation of the form "t = (%x. u)". diff -r 8aadda8e1338 -r e063be321438 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 23 14:51:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 23 14:54:17 2010 +0200 @@ -775,9 +775,6 @@ []) end; -val type_has_top_sort = - exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) - (* Extensionalize "th", because that makes sense and that's what Sledgehammer does, but also keep an unextensionalized version of "th" for backward compatibility. *) @@ -794,6 +791,9 @@ #> map Clausifier.introduce_combinators_in_theorem #> Meson.finish_cnf +val type_has_top_sort = + exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) + fun generic_metis_tac mode ctxt ths i st0 = let val _ = trace_msg (fn () => diff -r 8aadda8e1338 -r e063be321438 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 14:51:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 14:54:17 2010 +0200 @@ -23,6 +23,8 @@ structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = struct +open Sledgehammer_Util + val trace = Unsynchronized.ref false fun trace_msg msg = if !trace then tracing (msg ()) else () @@ -43,7 +45,7 @@ val name = Facts.string_of_ref xref |> forall (member Thm.eq_thm chained_ths) ths ? prefix chained_prefix - in (name, ths |> map Clausifier.transform_elim_theorem) end + in (name, ths) end (***************************************************************) @@ -420,7 +422,7 @@ val exists_sledgehammer_const = exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) -fun is_strange_thm th = +fun is_strange_theorem th = case head_of (concl_of th) of Const (a, _) => (a <> @{const_name Trueprop} andalso a <> @{const_name "=="}) @@ -486,13 +488,15 @@ are omitted. *) fun is_dangerous_term full_types t = not full_types andalso - (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t) + ((has_bound_or_var_of_type dangerous_types t andalso + has_bound_or_var_of_type dangerous_types (transform_elim_term t)) + orelse is_exhaustive_finite t) fun is_theorem_bad_for_atps full_types thm = let val t = prop_of thm in is_formula_too_complex t orelse exists_type type_has_top_sort t orelse is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse - is_strange_thm thm + is_strange_theorem thm end fun all_name_thms_pairs ctxt full_types add_thms chained_ths = @@ -525,8 +529,7 @@ val name1 = Facts.extern facts name; val name2 = Name_Space.extern full_space name; val ths = - ths0 |> map Clausifier.transform_elim_theorem - |> filter ((not o is_theorem_bad_for_atps full_types) orf + ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf member Thm.eq_thm add_thms) val name' = case find_first check_thms [name1, name2, name] of @@ -538,7 +541,7 @@ (prop_of th) ^ "`") |> space_implode " " in - cons (name' |> forall (member Thm.eq_thm chained_ths) ths + cons (name' |> forall (member Thm.eq_thm chained_ths) ths0 ? prefix chained_prefix, ths) end) in diff -r 8aadda8e1338 -r e063be321438 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 23 14:51:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 23 14:54:17 2010 +0200 @@ -119,8 +119,12 @@ @{const Not} $ t1 => @{const Not} $ aux Ts t1 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name All}, _)) $ t1 => + aux Ts (t0 $ eta_expand Ts t1 1) | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name Ex}, _)) $ t1 => + aux Ts (t0 $ eta_expand Ts t1 1) | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 @@ -175,8 +179,10 @@ let val thy = ProofContext.theory_of ctxt val t = t |> Envir.beta_eta_contract + |> transform_elim_term |> atomize_term - val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop + val need_trueprop = (fastype_of t = HOLogic.boolT) + val t = t |> need_trueprop ? HOLogic.mk_Trueprop |> extensionalize_term |> presimp ? presimplify_term thy |> perhaps (try (HOLogic.dest_Trueprop)) diff -r 8aadda8e1338 -r e063be321438 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Aug 23 14:51:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Aug 23 14:54:17 2010 +0200 @@ -16,6 +16,8 @@ val unyxml : string -> string val maybe_quote : string -> string val monomorphic_term : Type.tyenv -> term -> term + val eta_expand : typ list -> term -> int -> term + val transform_elim_term : term -> term val specialize_type : theory -> (string * typ) -> term -> term val subgoal_count : Proof.state -> int val strip_subgoal : thm -> int -> (string * typ) list * term list * term @@ -107,6 +109,25 @@ | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \ \variable", [t]))) t +fun eta_expand _ t 0 = t + | eta_expand Ts (Abs (s, T, t')) n = + Abs (s, T, eta_expand (T :: Ts) t' (n - 1)) + | eta_expand Ts t n = + fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t')) + (List.take (binder_types (fastype_of1 (Ts, t)), n)) + (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) + +(* Converts an elim-rule into an equivalent theorem that does not have the + predicate variable. Leaves other theorems unchanged. We simply instantiate + the conclusion variable to False. (Cf. "transform_elim_theorem" in + "Clausifier".) *) +fun transform_elim_term t = + case Logic.strip_imp_concl t of + @{const Trueprop} $ Var (z, @{typ bool}) => + subst_Vars [(z, @{const False})] t + | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t + | _ => t + fun specialize_type thy (s, T) t = let fun subst_for (Const (s', T')) =