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