perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
authorblanchet
Mon Aug 23 14:54:17 2010 +0200 (2010-08-23 ago)
changeset 38652e063be321438
parent 38651 8aadda8e1338
child 38653 78d0f18d5b36
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
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 23 14:51:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 23 14:54:17 2010 +0200
     1.3 @@ -141,7 +141,6 @@
     1.4      hol_context -> bool -> styp -> int -> styp
     1.5    val sel_no_from_name : string -> int
     1.6    val close_form : term -> term
     1.7 -  val eta_expand : typ list -> term -> int -> term
     1.8    val distinctness_formula : typ -> term list -> term
     1.9    val register_frac_type :
    1.10      string -> (string * string) list -> morphism -> Context.generic
    1.11 @@ -919,14 +918,6 @@
    1.12        | aux zs t = close_up zs (Term.add_vars t zs) t
    1.13    in aux [] end
    1.14  
    1.15 -fun eta_expand _ t 0 = t
    1.16 -  | eta_expand Ts (Abs (s, T, t')) n =
    1.17 -    Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
    1.18 -  | eta_expand Ts t n =
    1.19 -    fold_rev (curry3 Abs ("x" ^ nat_subscript n))
    1.20 -             (List.take (binder_types (fastype_of1 (Ts, t)), n))
    1.21 -             (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
    1.22 -
    1.23  fun distinctness_formula T =
    1.24    all_distinct_unordered_pairs_of
    1.25    #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Aug 23 14:51:56 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Aug 23 14:54:17 2010 +0200
     2.3 @@ -52,6 +52,7 @@
     2.4    val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
     2.5    val parse_bool_option : bool -> string -> string -> bool option
     2.6    val parse_time_option : string -> string -> Time.time option
     2.7 +  val nat_subscript : int -> string
     2.8    val flip_polarity : polarity -> polarity
     2.9    val prop_T : typ
    2.10    val bool_T : typ
    2.11 @@ -67,7 +68,7 @@
    2.12    val monomorphic_term : Type.tyenv -> term -> term
    2.13    val specialize_type : theory -> string * typ -> term -> term
    2.14    val varify_type : Proof.context -> typ -> typ
    2.15 -  val nat_subscript : int -> string
    2.16 +  val eta_expand : typ list -> term -> int -> term
    2.17    val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
    2.18    val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
    2.19    val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
    2.20 @@ -237,6 +238,18 @@
    2.21  val parse_bool_option = Sledgehammer_Util.parse_bool_option
    2.22  val parse_time_option = Sledgehammer_Util.parse_time_option
    2.23  
    2.24 +val i_subscript = implode o map (prefix "\<^isub>") o explode
    2.25 +fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
    2.26 +fun nat_subscript n =
    2.27 +  let val s = signed_string_of_int n in
    2.28 +    if print_mode_active Symbol.xsymbolsN then
    2.29 +      (* cheap trick to ensure proper alphanumeric ordering for one- and
    2.30 +         two-digit numbers *)
    2.31 +      (if n <= 9 then be_subscript else i_subscript) s
    2.32 +    else
    2.33 +      s
    2.34 +  end
    2.35 +
    2.36  fun flip_polarity Pos = Neg
    2.37    | flip_polarity Neg = Pos
    2.38    | flip_polarity Neut = Neut
    2.39 @@ -258,17 +271,7 @@
    2.40    Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
    2.41    |> snd |> the_single |> dest_Const |> snd
    2.42  
    2.43 -val i_subscript = implode o map (prefix "\<^isub>") o explode
    2.44 -fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
    2.45 -fun nat_subscript n =
    2.46 -  let val s = signed_string_of_int n in
    2.47 -    if print_mode_active Symbol.xsymbolsN then
    2.48 -      (* cheap trick to ensure proper alphanumeric ordering for one- and
    2.49 -         two-digit numbers *)
    2.50 -      (if n <= 9 then be_subscript else i_subscript) s
    2.51 -    else
    2.52 -      s
    2.53 -  end
    2.54 +val eta_expand = Sledgehammer_Util.eta_expand
    2.55  
    2.56  fun time_limit NONE = I
    2.57    | time_limit (SOME delay) = TimeLimit.timeLimit delay
     3.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 23 14:51:56 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 23 14:54:17 2010 +0200
     3.3 @@ -7,7 +7,6 @@
     3.4  
     3.5  signature CLAUSIFIER =
     3.6  sig
     3.7 -  val transform_elim_theorem : thm -> thm
     3.8    val extensionalize_theorem : thm -> thm
     3.9    val introduce_combinators_in_cterm : cterm -> thm
    3.10    val introduce_combinators_in_theorem : thm -> thm
    3.11 @@ -25,7 +24,7 @@
    3.12  (* Converts an elim-rule into an equivalent theorem that does not have the
    3.13     predicate variable. Leaves other theorems unchanged. We simply instantiate
    3.14     the conclusion variable to False. (Cf. "transform_elim_term" in
    3.15 -   "ATP_Systems".) *)
    3.16 +   "Sledgehammer_Util".) *)
    3.17  fun transform_elim_theorem th =
    3.18    case concl_of th of    (*conclusion variable*)
    3.19         @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    3.20 @@ -78,10 +77,6 @@
    3.21  
    3.22  (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    3.23  
    3.24 -(*Returns the vars of a theorem*)
    3.25 -fun vars_of_thm th =
    3.26 -  map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
    3.27 -
    3.28  val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
    3.29  
    3.30  (* Removes the lambdas from an equation of the form "t = (%x. u)".
     4.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 23 14:51:56 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 23 14:54:17 2010 +0200
     4.3 @@ -775,9 +775,6 @@
     4.4               [])
     4.5    end;
     4.6  
     4.7 -val type_has_top_sort =
     4.8 -  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
     4.9 -
    4.10  (* Extensionalize "th", because that makes sense and that's what Sledgehammer
    4.11     does, but also keep an unextensionalized version of "th" for backward
    4.12     compatibility. *)
    4.13 @@ -794,6 +791,9 @@
    4.14    #> map Clausifier.introduce_combinators_in_theorem
    4.15    #> Meson.finish_cnf
    4.16  
    4.17 +val type_has_top_sort =
    4.18 +  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
    4.19 +
    4.20  fun generic_metis_tac mode ctxt ths i st0 =
    4.21    let
    4.22      val _ = trace_msg (fn () =>
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 14:51:56 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 14:54:17 2010 +0200
     5.3 @@ -23,6 +23,8 @@
     5.4  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
     5.5  struct
     5.6  
     5.7 +open Sledgehammer_Util
     5.8 +
     5.9  val trace = Unsynchronized.ref false
    5.10  fun trace_msg msg = if !trace then tracing (msg ()) else ()
    5.11  
    5.12 @@ -43,7 +45,7 @@
    5.13      val name = Facts.string_of_ref xref
    5.14                 |> forall (member Thm.eq_thm chained_ths) ths
    5.15                    ? prefix chained_prefix
    5.16 -  in (name, ths |> map Clausifier.transform_elim_theorem) end
    5.17 +  in (name, ths) end
    5.18  
    5.19  
    5.20  (***************************************************************)
    5.21 @@ -420,7 +422,7 @@
    5.22  val exists_sledgehammer_const =
    5.23    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
    5.24  
    5.25 -fun is_strange_thm th =
    5.26 +fun is_strange_theorem th =
    5.27    case head_of (concl_of th) of
    5.28        Const (a, _) => (a <> @{const_name Trueprop} andalso
    5.29                         a <> @{const_name "=="})
    5.30 @@ -486,13 +488,15 @@
    5.31     are omitted. *)
    5.32  fun is_dangerous_term full_types t =
    5.33    not full_types andalso
    5.34 -  (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t)
    5.35 +  ((has_bound_or_var_of_type dangerous_types t andalso
    5.36 +    has_bound_or_var_of_type dangerous_types (transform_elim_term t))
    5.37 +   orelse is_exhaustive_finite t)
    5.38  
    5.39  fun is_theorem_bad_for_atps full_types thm =
    5.40    let val t = prop_of thm in
    5.41      is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    5.42      is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
    5.43 -    is_strange_thm thm
    5.44 +    is_strange_theorem thm
    5.45    end
    5.46  
    5.47  fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
    5.48 @@ -525,8 +529,7 @@
    5.49              val name1 = Facts.extern facts name;
    5.50              val name2 = Name_Space.extern full_space name;
    5.51              val ths =
    5.52 -              ths0 |> map Clausifier.transform_elim_theorem
    5.53 -                   |> filter ((not o is_theorem_bad_for_atps full_types) orf
    5.54 +              ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
    5.55                                member Thm.eq_thm add_thms)
    5.56              val name' =
    5.57                case find_first check_thms [name1, name2, name] of
    5.58 @@ -538,7 +541,7 @@
    5.59                                           (prop_of th) ^ "`")
    5.60                      |> space_implode " "
    5.61            in
    5.62 -            cons (name' |> forall (member Thm.eq_thm chained_ths) ths
    5.63 +            cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
    5.64                             ? prefix chained_prefix, ths)
    5.65            end)
    5.66    in
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 14:51:56 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 14:54:17 2010 +0200
     6.3 @@ -119,8 +119,12 @@
     6.4              @{const Not} $ t1 => @{const Not} $ aux Ts t1
     6.5            | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
     6.6              t0 $ Abs (s, T, aux (T :: Ts) t')
     6.7 +          | (t0 as Const (@{const_name All}, _)) $ t1 =>
     6.8 +            aux Ts (t0 $ eta_expand Ts t1 1)
     6.9            | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
    6.10              t0 $ Abs (s, T, aux (T :: Ts) t')
    6.11 +          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
    6.12 +            aux Ts (t0 $ eta_expand Ts t1 1)
    6.13            | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
    6.14            | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
    6.15            | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
    6.16 @@ -175,8 +179,10 @@
    6.17    let
    6.18      val thy = ProofContext.theory_of ctxt
    6.19      val t = t |> Envir.beta_eta_contract
    6.20 +              |> transform_elim_term
    6.21                |> atomize_term
    6.22 -    val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
    6.23 +    val need_trueprop = (fastype_of t = HOLogic.boolT)
    6.24 +    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
    6.25                |> extensionalize_term
    6.26                |> presimp ? presimplify_term thy
    6.27                |> perhaps (try (HOLogic.dest_Trueprop))
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Aug 23 14:51:56 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Aug 23 14:54:17 2010 +0200
     7.3 @@ -16,6 +16,8 @@
     7.4    val unyxml : string -> string
     7.5    val maybe_quote : string -> string
     7.6    val monomorphic_term : Type.tyenv -> term -> term
     7.7 +  val eta_expand : typ list -> term -> int -> term
     7.8 +  val transform_elim_term : term -> term
     7.9    val specialize_type : theory -> (string * typ) -> term -> term
    7.10    val subgoal_count : Proof.state -> int
    7.11    val strip_subgoal : thm -> int -> (string * typ) list * term list * term
    7.12 @@ -107,6 +109,25 @@
    7.13        | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
    7.14                              \variable", [t]))) t
    7.15  
    7.16 +fun eta_expand _ t 0 = t
    7.17 +  | eta_expand Ts (Abs (s, T, t')) n =
    7.18 +    Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
    7.19 +  | eta_expand Ts t n =
    7.20 +    fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
    7.21 +             (List.take (binder_types (fastype_of1 (Ts, t)), n))
    7.22 +             (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
    7.23 +
    7.24 +(* Converts an elim-rule into an equivalent theorem that does not have the
    7.25 +   predicate variable. Leaves other theorems unchanged. We simply instantiate
    7.26 +   the conclusion variable to False. (Cf. "transform_elim_theorem" in
    7.27 +   "Clausifier".) *)
    7.28 +fun transform_elim_term t =
    7.29 +  case Logic.strip_imp_concl t of
    7.30 +    @{const Trueprop} $ Var (z, @{typ bool}) =>
    7.31 +    subst_Vars [(z, @{const False})] t
    7.32 +  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
    7.33 +  | _ => t
    7.34 +
    7.35  fun specialize_type thy (s, T) t =
    7.36    let
    7.37      fun subst_for (Const (s', T')) =