src/HOL/Tools/Meson/meson.ML
 changeset 47953 a2c3706c4cb1 parent 47035 5248fae40f09 child 47954 aada9fd08b58
```     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon May 21 16:37:28 2012 +0200
1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
1.3 @@ -24,8 +24,8 @@
1.4    val choice_theorems : theory -> thm list
1.5    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
1.6    val skolemize : Proof.context -> thm -> thm
1.7 -  val extensionalize_conv : Proof.context -> conv
1.8 -  val extensionalize_theorem : Proof.context -> thm -> thm
1.9 +  val abs_extensionalize_conv : Proof.context -> conv
1.10 +  val abs_extensionalize_thm : Proof.context -> thm -> thm
1.11    val make_clauses_unsorted: Proof.context -> thm list -> thm list
1.12    val make_clauses: Proof.context -> thm list -> thm list
1.13    val make_horns: thm list -> thm list
1.14 @@ -574,29 +574,47 @@
1.15  (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
1.16     would be desirable to do this symmetrically but there's at least one existing
1.17     proof in "Tarski" that relies on the current behavior. *)
1.18 -fun extensionalize_conv ctxt ct =
1.19 +fun abs_extensionalize_conv ctxt ct =
1.20    case term_of ct of
1.21      Const (@{const_name HOL.eq}, _) \$ _ \$ Abs _ =>
1.22      ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
1.23 -           then_conv extensionalize_conv ctxt)
1.24 -  | _ \$ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
1.25 -  | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
1.26 +           then_conv abs_extensionalize_conv ctxt)
1.27 +  | _ \$ _ => Conv.comb_conv (abs_extensionalize_conv ctxt) ct
1.28 +  | Abs _ => Conv.abs_conv (abs_extensionalize_conv o snd) ctxt ct
1.29    | _ => Conv.all_conv ct
1.30
1.31 -val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv
1.32 +val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
1.33 +
1.34 +(*
1.35 +(* Weakens negative occurrences of "f g = f h" to
1.36 +   "(ALL x. g x = h x) | f g = f h". *)
1.37 +fun cong_extensionalize_conv ctxt ct =
1.38 +  case term_of ct of
1.39 +    @{const Trueprop} \$ (@{const Not} \$ (Const (@{const_name HOL.eq}, _)
1.40 +                                         \$ (t as _ \$ _) \$ (u as _ \$ _))) =>
1.41 +    (case get_f_pattern t u of
1.42 +       SOME _ => Conv.all_conv ct
1.43 +     | NONE => Conv.all_conv ct)
1.44 +  | _ => Conv.all_conv ct
1.45 +
1.46 +val cong_extensionalize_thm = Conv.fconv_rule o cong_extensionalize_conv
1.47 +*)
1.48 +
1.49 +fun cong_extensionalize_thm ctxt = I (*###*)
1.50
1.51  (* "RS" can fail if "unify_search_bound" is too small. *)
1.52  fun try_skolemize_etc ctxt th =
1.53 -  (* Extensionalize "th", because that makes sense and that's what Sledgehammer
1.54 -     does, but also keep an unextensionalized version of "th" for backward
1.55 -     compatibility. *)
1.56 -  [th] |> insert Thm.eq_thm_prop (extensionalize_theorem ctxt th)
1.57 -       |> map_filter (fn th => th |> try (skolemize ctxt)
1.58 -                                  |> tap (fn NONE =>
1.59 -                                             trace_msg ctxt (fn () =>
1.60 -                                                 "Failed to skolemize " ^
1.61 -                                                  Display.string_of_thm ctxt th)
1.62 -                                           | _ => ()))
1.63 +  (* Extensionalize lambdas in "th", because that makes sense and that's what
1.64 +     Sledgehammer does, but also keep an unextensionalized version of "th" for
1.65 +     backward compatibility. *)
1.66 +  [th |> cong_extensionalize_thm ctxt]
1.67 +  |> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
1.68 +  |> map_filter (fn th => th |> try (skolemize ctxt)
1.69 +                             |> tap (fn NONE =>
1.70 +                                        trace_msg ctxt (fn () =>
1.71 +                                            "Failed to skolemize " ^
1.72 +                                             Display.string_of_thm ctxt th)
1.73 +                                      | _ => ()))
1.74
1.75  fun add_clauses ctxt th cls =
1.76    let val ctxt0 = Variable.global_thm_context th
```