src/HOL/Tools/Meson/meson.ML
changeset 47954 aada9fd08b58
parent 47953 a2c3706c4cb1
child 47956 2a420750248b
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
     1.3 @@ -24,6 +24,7 @@
     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 cong_extensionalize_thm : theory -> thm -> thm
     1.8    val abs_extensionalize_conv : Proof.context -> conv
     1.9    val abs_extensionalize_thm : Proof.context -> thm -> thm
    1.10    val make_clauses_unsorted: Proof.context -> thm list -> thm list
    1.11 @@ -571,6 +572,52 @@
    1.12      skolemize_with_choice_theorems ctxt (choice_theorems thy)
    1.13    end
    1.14  
    1.15 +exception NO_F_PATTERN of unit
    1.16 +
    1.17 +fun get_F_pattern t u =
    1.18 +  let
    1.19 +    fun pat t u =
    1.20 +      let
    1.21 +        val ((head1, args1), (head2, args2)) = (t, u) |> pairself strip_comb
    1.22 +      in
    1.23 +        if head1 = head2 then
    1.24 +          let val pats = map2 pat args1 args2 in
    1.25 +            case filter (is_some o fst) pats of
    1.26 +              [(SOME T, _)] => (SOME T, list_comb (head1, map snd pats))
    1.27 +            | [] => (NONE, t)
    1.28 +            | _ => raise NO_F_PATTERN ()
    1.29 +          end
    1.30 +        else
    1.31 +          let val T = fastype_of t in
    1.32 +            if can dest_funT T then (SOME T, Bound 0) else raise NO_F_PATTERN ()
    1.33 +          end
    1.34 +      end
    1.35 +  in
    1.36 +    (case pat t u of
    1.37 +       (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
    1.38 +     | _ => NONE)
    1.39 +    handle NO_F_PATTERN () => NONE
    1.40 +  end
    1.41 +
    1.42 +val ext_cong_neq = @{thm ext_cong_neq}
    1.43 +val F_ext_cong_neq =
    1.44 +  Term.add_vars (prop_of @{thm ext_cong_neq}) []
    1.45 +  |> filter (fn ((s, _), _) => s = "F")
    1.46 +  |> the_single |> Var
    1.47 +
    1.48 +(* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
    1.49 +fun cong_extensionalize_thm thy th =
    1.50 +  case concl_of th of
    1.51 +    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
    1.52 +                                         $ (t as _ $ _) $ (u as _ $ _))) =>
    1.53 +    (case get_F_pattern t u of
    1.54 +       SOME p =>
    1.55 +       let val inst = [pairself (cterm_of thy) (F_ext_cong_neq, p)] in
    1.56 +         th RS cterm_instantiate inst ext_cong_neq
    1.57 +       end
    1.58 +     | NONE => th)
    1.59 +  | _ => th
    1.60 +
    1.61  (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
    1.62     would be desirable to do this symmetrically but there's at least one existing
    1.63     proof in "Tarski" that relies on the current behavior. *)
    1.64 @@ -585,36 +632,24 @@
    1.65  
    1.66  val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
    1.67  
    1.68 -(*
    1.69 -(* Weakens negative occurrences of "f g = f h" to
    1.70 -   "(ALL x. g x = h x) | f g = f h". *)
    1.71 -fun cong_extensionalize_conv ctxt ct =
    1.72 -  case term_of ct of
    1.73 -    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
    1.74 -                                         $ (t as _ $ _) $ (u as _ $ _))) =>
    1.75 -    (case get_f_pattern t u of
    1.76 -       SOME _ => Conv.all_conv ct
    1.77 -     | NONE => Conv.all_conv ct)
    1.78 -  | _ => Conv.all_conv ct
    1.79 -
    1.80 -val cong_extensionalize_thm = Conv.fconv_rule o cong_extensionalize_conv
    1.81 -*)
    1.82 -
    1.83 -fun cong_extensionalize_thm ctxt = I (*###*)
    1.84 -
    1.85  (* "RS" can fail if "unify_search_bound" is too small. *)
    1.86  fun try_skolemize_etc ctxt th =
    1.87 -  (* Extensionalize lambdas in "th", because that makes sense and that's what
    1.88 -     Sledgehammer does, but also keep an unextensionalized version of "th" for
    1.89 -     backward compatibility. *)
    1.90 -  [th |> cong_extensionalize_thm ctxt]
    1.91 -  |> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
    1.92 -  |> map_filter (fn th => th |> try (skolemize ctxt)
    1.93 -                             |> tap (fn NONE =>
    1.94 -                                        trace_msg ctxt (fn () =>
    1.95 -                                            "Failed to skolemize " ^
    1.96 -                                             Display.string_of_thm ctxt th)
    1.97 -                                      | _ => ()))
    1.98 +  let
    1.99 +    val thy = Proof_Context.theory_of ctxt
   1.100 +    val th = th |> cong_extensionalize_thm thy
   1.101 +  in
   1.102 +    [th]
   1.103 +    (* Extensionalize lambdas in "th", because that makes sense and that's what
   1.104 +       Sledgehammer does, but also keep an unextensionalized version of "th" for
   1.105 +       backward compatibility. *)
   1.106 +    |> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
   1.107 +    |> map_filter (fn th => th |> try (skolemize ctxt)
   1.108 +                               |> tap (fn NONE =>
   1.109 +                                          trace_msg ctxt (fn () =>
   1.110 +                                              "Failed to skolemize " ^
   1.111 +                                               Display.string_of_thm ctxt th)
   1.112 +                                        | _ => ()))
   1.113 +  end
   1.114  
   1.115  fun add_clauses ctxt th cls =
   1.116    let val ctxt0 = Variable.global_thm_context th