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.*)