make higher-order goals more first-order via extensionality
authorblanchet
Tue May 22 16:59:27 2012 +0200 (2012-05-22)
changeset 47954aada9fd08b58
parent 47953 a2c3706c4cb1
child 47955 a2a821abab83
make higher-order goals more first-order via extensionality
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 16:59:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 16:59:27 2012 +0200
     1.3 @@ -1272,7 +1272,8 @@
     1.4      val is_ho = is_type_enc_higher_order type_enc
     1.5    in
     1.6      t |> need_trueprop ? HOLogic.mk_Trueprop
     1.7 -      |> (if is_ho then unextensionalize_def else abs_extensionalize_term ctxt)
     1.8 +      |> (if is_ho then unextensionalize_def
     1.9 +          else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
    1.10        |> presimplify_term thy
    1.11        |> HOLogic.dest_Trueprop
    1.12    end
     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Tue May 22 16:59:27 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Tue May 22 16:59:27 2012 +0200
     2.3 @@ -36,6 +36,7 @@
     2.4    val open_form : (string -> string) -> term -> term
     2.5    val monomorphic_term : Type.tyenv -> term -> term
     2.6    val eta_expand : typ list -> term -> int -> term
     2.7 +  val cong_extensionalize_term : theory -> term -> term
     2.8    val abs_extensionalize_term : Proof.context -> term -> term
     2.9    val transform_elim_prop : term -> term
    2.10    val specialize_type : theory -> (string * typ) -> term -> term
    2.11 @@ -298,6 +299,14 @@
    2.12               (List.take (binder_types (fastype_of1 (Ts, t)), n))
    2.13               (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
    2.14  
    2.15 +fun cong_extensionalize_term thy t =
    2.16 +  if exists_Const (fn (s, _) => s = @{const_name Not}) t then
    2.17 +    t |> Skip_Proof.make_thm thy
    2.18 +      |> Meson.cong_extensionalize_thm thy
    2.19 +      |> prop_of
    2.20 +  else
    2.21 +    t
    2.22 +
    2.23  fun is_fun_equality (@{const_name HOL.eq},
    2.24                       Type (_, [Type (@{type_name fun}, _), _])) = true
    2.25    | is_fun_equality _ = false
     3.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
     3.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
     3.3 @@ -24,6 +24,7 @@
     3.4    val choice_theorems : theory -> thm list
     3.5    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
     3.6    val skolemize : Proof.context -> thm -> thm
     3.7 +  val cong_extensionalize_thm : theory -> thm -> thm
     3.8    val abs_extensionalize_conv : Proof.context -> conv
     3.9    val abs_extensionalize_thm : Proof.context -> thm -> thm
    3.10    val make_clauses_unsorted: Proof.context -> thm list -> thm list
    3.11 @@ -571,6 +572,52 @@
    3.12      skolemize_with_choice_theorems ctxt (choice_theorems thy)
    3.13    end
    3.14  
    3.15 +exception NO_F_PATTERN of unit
    3.16 +
    3.17 +fun get_F_pattern t u =
    3.18 +  let
    3.19 +    fun pat t u =
    3.20 +      let
    3.21 +        val ((head1, args1), (head2, args2)) = (t, u) |> pairself strip_comb
    3.22 +      in
    3.23 +        if head1 = head2 then
    3.24 +          let val pats = map2 pat args1 args2 in
    3.25 +            case filter (is_some o fst) pats of
    3.26 +              [(SOME T, _)] => (SOME T, list_comb (head1, map snd pats))
    3.27 +            | [] => (NONE, t)
    3.28 +            | _ => raise NO_F_PATTERN ()
    3.29 +          end
    3.30 +        else
    3.31 +          let val T = fastype_of t in
    3.32 +            if can dest_funT T then (SOME T, Bound 0) else raise NO_F_PATTERN ()
    3.33 +          end
    3.34 +      end
    3.35 +  in
    3.36 +    (case pat t u of
    3.37 +       (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
    3.38 +     | _ => NONE)
    3.39 +    handle NO_F_PATTERN () => NONE
    3.40 +  end
    3.41 +
    3.42 +val ext_cong_neq = @{thm ext_cong_neq}
    3.43 +val F_ext_cong_neq =
    3.44 +  Term.add_vars (prop_of @{thm ext_cong_neq}) []
    3.45 +  |> filter (fn ((s, _), _) => s = "F")
    3.46 +  |> the_single |> Var
    3.47 +
    3.48 +(* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
    3.49 +fun cong_extensionalize_thm thy th =
    3.50 +  case concl_of th of
    3.51 +    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
    3.52 +                                         $ (t as _ $ _) $ (u as _ $ _))) =>
    3.53 +    (case get_F_pattern t u of
    3.54 +       SOME p =>
    3.55 +       let val inst = [pairself (cterm_of thy) (F_ext_cong_neq, p)] in
    3.56 +         th RS cterm_instantiate inst ext_cong_neq
    3.57 +       end
    3.58 +     | NONE => th)
    3.59 +  | _ => th
    3.60 +
    3.61  (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
    3.62     would be desirable to do this symmetrically but there's at least one existing
    3.63     proof in "Tarski" that relies on the current behavior. *)
    3.64 @@ -585,36 +632,24 @@
    3.65  
    3.66  val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
    3.67  
    3.68 -(*
    3.69 -(* Weakens negative occurrences of "f g = f h" to
    3.70 -   "(ALL x. g x = h x) | f g = f h". *)
    3.71 -fun cong_extensionalize_conv ctxt ct =
    3.72 -  case term_of ct of
    3.73 -    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
    3.74 -                                         $ (t as _ $ _) $ (u as _ $ _))) =>
    3.75 -    (case get_f_pattern t u of
    3.76 -       SOME _ => Conv.all_conv ct
    3.77 -     | NONE => Conv.all_conv ct)
    3.78 -  | _ => Conv.all_conv ct
    3.79 -
    3.80 -val cong_extensionalize_thm = Conv.fconv_rule o cong_extensionalize_conv
    3.81 -*)
    3.82 -
    3.83 -fun cong_extensionalize_thm ctxt = I (*###*)
    3.84 -
    3.85  (* "RS" can fail if "unify_search_bound" is too small. *)
    3.86  fun try_skolemize_etc ctxt th =
    3.87 -  (* Extensionalize lambdas in "th", because that makes sense and that's what
    3.88 -     Sledgehammer does, but also keep an unextensionalized version of "th" for
    3.89 -     backward compatibility. *)
    3.90 -  [th |> cong_extensionalize_thm ctxt]
    3.91 -  |> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
    3.92 -  |> map_filter (fn th => th |> try (skolemize ctxt)
    3.93 -                             |> tap (fn NONE =>
    3.94 -                                        trace_msg ctxt (fn () =>
    3.95 -                                            "Failed to skolemize " ^
    3.96 -                                             Display.string_of_thm ctxt th)
    3.97 -                                      | _ => ()))
    3.98 +  let
    3.99 +    val thy = Proof_Context.theory_of ctxt
   3.100 +    val th = th |> cong_extensionalize_thm thy
   3.101 +  in
   3.102 +    [th]
   3.103 +    (* Extensionalize lambdas in "th", because that makes sense and that's what
   3.104 +       Sledgehammer does, but also keep an unextensionalized version of "th" for
   3.105 +       backward compatibility. *)
   3.106 +    |> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
   3.107 +    |> map_filter (fn th => th |> try (skolemize ctxt)
   3.108 +                               |> tap (fn NONE =>
   3.109 +                                          trace_msg ctxt (fn () =>
   3.110 +                                              "Failed to skolemize " ^
   3.111 +                                               Display.string_of_thm ctxt th)
   3.112 +                                        | _ => ()))
   3.113 +  end
   3.114  
   3.115  fun add_clauses ctxt th cls =
   3.116    let val ctxt0 = Variable.global_thm_context th
     4.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue May 22 16:59:27 2012 +0200
     4.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue May 22 16:59:27 2012 +0200
     4.3 @@ -309,7 +309,9 @@
     4.4           |> new_skolemizer ? forall_intr_vars
     4.5      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     4.6      val th = th |> Conv.fconv_rule Object_Logic.atomize
     4.7 -                |> abs_extensionalize_thm ctxt |> make_nnf ctxt
     4.8 +                |> cong_extensionalize_thm thy
     4.9 +                |> abs_extensionalize_thm ctxt
    4.10 +                |> make_nnf ctxt
    4.11    in
    4.12      if new_skolemizer then
    4.13        let