src/HOL/Tools/Meson/meson.ML
 changeset 42747 f132d13fcf75 parent 42739 017e5dac8642 child 42750 c8b1d9ee3758
```     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
1.3 @@ -22,6 +22,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 is_fol_term: theory -> term -> bool
1.10    val make_clauses_unsorted: thm list -> thm list
1.11    val make_clauses: thm list -> thm list
1.12 @@ -610,12 +612,37 @@
1.13      skolemize_with_choice_theorems ctxt (choice_theorems thy)
1.14    end
1.15
1.16 +fun is_Abs (Abs _) = true
1.17 +  | is_Abs _ = false
1.18 +
1.19 +(* Removes the lambdas from an equation of the form "t = (%x. u)".  *)
1.20 +fun extensionalize_conv ctxt ct =
1.21 +  case term_of ct of
1.22 +    Const (@{const_name HOL.eq}, _) \$ t1 \$ t2 =>
1.23 +    ct |> (if is_Abs t1 orelse is_Abs t2 then
1.24 +             Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
1.25 +             then_conv extensionalize_conv ctxt
1.26 +           else
1.27 +             Conv.comb_conv (extensionalize_conv ctxt))
1.28 +  | _ \$ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
1.29 +  | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
1.30 +  | _ => Conv.all_conv ct
1.31 +
1.32 +val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv
1.33 +
1.34  (* "RS" can fail if "unify_search_bound" is too small. *)
1.35 -fun try_skolemize ctxt th =
1.36 -  try (skolemize ctxt) th
1.37 -  |> tap (fn NONE => trace_msg ctxt (fn () => "Failed to skolemize " ^
1.38 -                                              Display.string_of_thm ctxt th)
1.39 -           | _ => ())
1.40 +fun try_skolemize_etc ctxt =
1.41 +  Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
1.42 +  (* Extensionalize "th", because that makes sense and that's what Sledgehammer
1.43 +     does, but also keep an unextensionalized version of "th" for backward
1.44 +     compatibility. *)
1.45 +  #> (fn th => insert Thm.eq_thm_prop (extensionalize_theorem ctxt th) [th])
1.46 +  #> map_filter (fn th => try (skolemize ctxt) th
1.47 +                          |> tap (fn NONE =>
1.48 +                                     trace_msg ctxt (fn () =>
1.49 +                                         "Failed to skolemize " ^
1.50 +                                          Display.string_of_thm ctxt th)
1.51 +                                   | _ => ()))
1.52
1.53  fun add_clauses th cls =
1.54    let val ctxt0 = Variable.global_thm_context th
1.55 @@ -645,7 +672,7 @@
1.56  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
1.57
1.58  fun skolemize_prems_tac ctxt prems =
1.59 -  cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE
1.60 +  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE
1.61
1.62  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
1.63    Function mkcl converts theorems to clauses.*)
```