# HG changeset patch # User blanchet # Date 1305206959 -7200 # Node ID f132d13fcf75e949af9ded6a9ee0efa71b92dbfc # Parent 7e227e9de779b300050899ae36599078d48a307c use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc. diff -r 7e227e9de779 -r f132d13fcf75 src/HOL/Metis_Examples/Clausify.thy --- a/src/HOL/Metis_Examples/Clausify.thy Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Metis_Examples/Clausify.thy Thu May 12 15:29:19 2011 +0200 @@ -12,6 +12,37 @@ declare [[unify_search_bound = 100]] declare [[unify_trace_bound = 100]] +sledgehammer_params [prover = e, blocking, timeout = 10] + + +text {* Extensionality *} + +lemma plus_1_not_0: "n + (1\nat) \ 0" +by simp + +definition inc :: "nat \ nat" where +"inc x = x + 1" + +lemma "inc \ (\y. 0)" +sledgehammer [expect = some] (inc_def plus_1_not_0) +by (metis inc_def plus_1_not_0) + +lemma "inc = (\y. y + 1)" +sledgehammer [expect = some] (inc_def) +by (metis inc_def) + +lemma "(\y. y + 1) = inc" +sledgehammer [expect = some] (inc_def) +by (metis inc_def) + +definition add_swap :: "nat \ nat \ nat" where +"add_swap = (\x y. y + x)" + +lemma "add_swap m n = n + m" +sledgehammer [expect = some] (add_swap_def) +by (metis add_swap_def) + + text {* Definitional CNF for facts *} declare [[meson_max_clauses = 10]] @@ -83,6 +114,7 @@ (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" by (metisFT rax) + text {* Definitional CNF for goal *} axiomatization p :: "nat \ nat \ bool" where @@ -108,6 +140,7 @@ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" by (metisFT pax) + text {* New Skolemizer *} declare [[metis_new_skolemizer]] diff -r 7e227e9de779 -r f132d13fcf75 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Thu May 12 15:29:19 2011 +0200 @@ -22,6 +22,8 @@ val choice_theorems : theory -> thm list val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm val skolemize : Proof.context -> thm -> thm + val extensionalize_conv : Proof.context -> conv + val extensionalize_theorem : Proof.context -> thm -> thm val is_fol_term: theory -> term -> bool val make_clauses_unsorted: thm list -> thm list val make_clauses: thm list -> thm list @@ -610,12 +612,37 @@ skolemize_with_choice_theorems ctxt (choice_theorems thy) end +fun is_Abs (Abs _) = true + | is_Abs _ = false + +(* Removes the lambdas from an equation of the form "t = (%x. u)". *) +fun extensionalize_conv ctxt ct = + case term_of ct of + Const (@{const_name HOL.eq}, _) $ t1 $ t2 => + ct |> (if is_Abs t1 orelse is_Abs t2 then + Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]} + then_conv extensionalize_conv ctxt + else + Conv.comb_conv (extensionalize_conv ctxt)) + | _ $ _ => Conv.comb_conv (extensionalize_conv ctxt) ct + | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct + | _ => Conv.all_conv ct + +val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv + (* "RS" can fail if "unify_search_bound" is too small. *) -fun try_skolemize ctxt th = - try (skolemize ctxt) th - |> tap (fn NONE => trace_msg ctxt (fn () => "Failed to skolemize " ^ - Display.string_of_thm ctxt th) - | _ => ()) +fun try_skolemize_etc ctxt = + Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt) + (* Extensionalize "th", because that makes sense and that's what Sledgehammer + does, but also keep an unextensionalized version of "th" for backward + compatibility. *) + #> (fn th => insert Thm.eq_thm_prop (extensionalize_theorem ctxt th) [th]) + #> map_filter (fn th => try (skolemize ctxt) th + |> tap (fn NONE => + trace_msg ctxt (fn () => + "Failed to skolemize " ^ + Display.string_of_thm ctxt th) + | _ => ())) fun add_clauses th cls = let val ctxt0 = Variable.global_thm_context th @@ -645,7 +672,7 @@ fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); fun skolemize_prems_tac ctxt prems = - cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE + cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. Function mkcl converts theorems to clauses.*) diff -r 7e227e9de779 -r f132d13fcf75 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu May 12 15:29:19 2011 +0200 @@ -10,7 +10,6 @@ val new_skolem_var_prefix : string val new_nonskolem_var_prefix : string val is_zapped_var_name : string -> bool - val extensionalize_theorem : thm -> thm val introduce_combinators_in_cterm : cterm -> thm val introduce_combinators_in_theorem : thm -> thm val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool @@ -87,16 +86,6 @@ (**** REPLACING ABSTRACTIONS BY COMBINATORS ****) -val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]} - -(* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *) -fun extensionalize_theorem th = - case prop_of th of - _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _])) - $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all) - | _ => th - fun is_quasi_lambda_free (Const (@{const_name Meson.skolem}, _) $ _) = true | is_quasi_lambda_free (t1 $ t2) = is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 @@ -321,7 +310,7 @@ val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single val th = th |> Conv.fconv_rule Object_Logic.atomize |> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt) - |> extensionalize_theorem + |> extensionalize_theorem ctxt |> make_nnf ctxt in if new_skolemizer then diff -r 7e227e9de779 -r f132d13fcf75 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Thu May 12 15:29:19 2011 +0200 @@ -132,20 +132,9 @@ (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg else "")) -(* Extensionalize "th", because that makes sense and that's what Sledgehammer - does, but also keep an unextensionalized version of "th" for backward - compatibility. *) -fun also_extensionalize_theorem th = - let val th' = Meson_Clausify.extensionalize_theorem th in - if Thm.eq_thm (th, th') then [th] - else th :: Meson.make_clauses_unsorted [th'] - end - fun neg_clausify ctxt = single #> Meson.make_clauses_unsorted - #> maps (Raw_Simplifier.rewrite_rule (Meson.unfold_set_const_simps ctxt) - #> also_extensionalize_theorem) #> map Meson_Clausify.introduce_combinators_in_theorem #> Meson.finish_cnf diff -r 7e227e9de779 -r f132d13fcf75 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 @@ -355,24 +355,11 @@ subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) (0 upto length Ts - 1 ~~ Ts)) -(* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_theorem" in "Meson_Clausify".) *) -fun extensionalize_term t = - let - fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t' - | aux j (t as Const (s, Type (_, [Type (_, [_, T']), - Type (_, [_, res_T])])) - $ t2 $ Abs (var_s, var_T, t')) = - if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then - let val var_t = Var ((var_s, j), var_T) in - Const (s, T' --> T' --> res_T) - $ betapply (t2, var_t) $ subst_bound (var_t, t') - |> aux (j + 1) - end - else - t - | aux _ t = t - in aux (maxidx_of_term t + 1) t end +fun extensionalize_term ctxt t = + let val thy = Proof_Context.theory_of ctxt in + t |> cterm_of thy |> Meson.extensionalize_conv ctxt + |> prop_of |> Logic.dest_equals |> snd + end fun introduce_combinators_in_term ctxt kind t = let val thy = Proof_Context.theory_of ctxt in @@ -436,7 +423,7 @@ val t = t |> need_trueprop ? HOLogic.mk_Trueprop |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) [] - |> extensionalize_term + |> extensionalize_term ctxt |> presimp ? presimplify_term thy |> perhaps (try (HOLogic.dest_Trueprop)) |> introduce_combinators_in_term ctxt kind