# HG changeset patch # User blanchet # Date 1286221747 -7200 # Node ID 02fcd9cd1eaca7fdf0d83c50c4a6d18ca9ee2bc8 # Parent 1f01c9b2b76b8f929b13ad59e5435209e82cb12a move Meson to Plain diff -r 1f01c9b2b76b -r 02fcd9cd1eac src/HOL/Meson.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Meson.thy Mon Oct 04 21:49:07 2010 +0200 @@ -0,0 +1,205 @@ +(* Title: HOL/Meson.thy + Author: Lawrence C Paulson, Tobias Nipkow + Copyright 2001 University of Cambridge +*) + +header {* MESON Proof Procedure (Model Elimination) *} + +theory Meson +imports Nat +uses ("Tools/Meson/meson.ML") + ("Tools/Meson/meson_clausify.ML") +begin + +section {* Negation Normal Form *} + +text {* de Morgan laws *} + +lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q" + and meson_not_disjD: "~(P|Q) ==> ~P & ~Q" + and meson_not_notD: "~~P ==> P" + and meson_not_allD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" + and meson_not_exD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" + by fast+ + +text {* Removal of @{text "-->"} and @{text "<->"} (positive and +negative occurrences) *} + +lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q" + and meson_not_impD: "~(P-->Q) ==> P & ~Q" + and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)" + and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)" + -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *} + and meson_not_refl_disj_D: "x ~= x | P ==> P" + by fast+ + + +section {* Pulling out the existential quantifiers *} + +text {* Conjunction *} + +lemma meson_conj_exD1: "!!P Q. (\x. P(x)) & Q ==> \x. P(x) & Q" + and meson_conj_exD2: "!!P Q. P & (\x. Q(x)) ==> \x. P & Q(x)" + by fast+ + + +text {* Disjunction *} + +lemma meson_disj_exD: "!!P Q. (\x. P(x)) | (\x. Q(x)) ==> \x. P(x) | Q(x)" + -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *} + -- {* With ex-Skolemization, makes fewer Skolem constants *} + and meson_disj_exD1: "!!P Q. (\x. P(x)) | Q ==> \x. P(x) | Q" + and meson_disj_exD2: "!!P Q. P | (\x. Q(x)) ==> \x. P | Q(x)" + by fast+ + +lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)" + and meson_disj_comm: "P|Q ==> Q|P" + and meson_disj_FalseD1: "False|P ==> P" + and meson_disj_FalseD2: "P|False ==> P" + by fast+ + + +text{* Generation of contrapositives *} + +text{*Inserts negated disjunct after removing the negation; P is a literal. + Model elimination requires assuming the negation of every attempted subgoal, + hence the negated disjuncts.*} +lemma make_neg_rule: "~P|Q ==> ((~P==>P) ==> Q)" +by blast + +text{*Version for Plaisted's "Postive refinement" of the Meson procedure*} +lemma make_refined_neg_rule: "~P|Q ==> (P ==> Q)" +by blast + +text{*@{term P} should be a literal*} +lemma make_pos_rule: "P|Q ==> ((P==>~P) ==> Q)" +by blast + +text{*Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't +insert new assumptions, for ordinary resolution.*} + +lemmas make_neg_rule' = make_refined_neg_rule + +lemma make_pos_rule': "[|P|Q; ~P|] ==> Q" +by blast + +text{* Generation of a goal clause -- put away the final literal *} + +lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)" +by blast + +lemma make_pos_goal: "P ==> ((P==>~P) ==> False)" +by blast + + +section {* Lemmas for Forward Proof *} + +text{*There is a similarity to congruence rules*} + +(*NOTE: could handle conjunctions (faster?) by + nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) +lemma conj_forward: "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q" +by blast + +lemma disj_forward: "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q" +by blast + +(*Version of @{text disj_forward} for removal of duplicate literals*) +lemma disj_forward2: + "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q" +apply blast +done + +lemma all_forward: "[| \x. P'(x); !!x. P'(x) ==> P(x) |] ==> \x. P(x)" +by blast + +lemma ex_forward: "[| \x. P'(x); !!x. P'(x) ==> P(x) |] ==> \x. P(x)" +by blast + + +section {* Clausification helper *} + +lemma TruepropI: "P \ Q \ Trueprop P \ Trueprop Q" +by simp + + +text{* Combinator translation helpers *} + +definition COMBI :: "'a \ 'a" where +[no_atp]: "COMBI P = P" + +definition COMBK :: "'a \ 'b \ 'a" where +[no_atp]: "COMBK P Q = P" + +definition COMBB :: "('b => 'c) \ ('a => 'b) \ 'a \ 'c" where [no_atp]: +"COMBB P Q R = P (Q R)" + +definition COMBC :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where +[no_atp]: "COMBC P Q R = P R Q" + +definition COMBS :: "('a \ 'b \ 'c) \ ('a \ 'b) \ 'a \ 'c" where +[no_atp]: "COMBS P Q R = P R (Q R)" + +lemma abs_S [no_atp]: "\x. (f x) (g x) \ COMBS f g" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBS_def) +done + +lemma abs_I [no_atp]: "\x. x \ COMBI" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBI_def) +done + +lemma abs_K [no_atp]: "\x. y \ COMBK y" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBK_def) +done + +lemma abs_B [no_atp]: "\x. a (g x) \ COMBB a g" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBB_def) +done + +lemma abs_C [no_atp]: "\x. (f x) b \ COMBC f b" +apply (rule eq_reflection) +apply (rule ext) +apply (simp add: COMBC_def) +done + + +section {* Skolemization helpers *} + +definition skolem :: "'a \ 'a" where +[no_atp]: "skolem = (\x. x)" + +lemma skolem_COMBK_iff: "P \ skolem (COMBK P (i\nat))" +unfolding skolem_def COMBK_def by (rule refl) + +lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] +lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] + + +section {* Meson package *} + +ML {* +structure Meson_Choices = Named_Thms +( + val name = "meson_choice" + val description = "choice axioms for MESON's (and Metis's) skolemizer" +) +*} + +use "Tools/Meson/meson.ML" +use "Tools/Meson/meson_clausify.ML" + +setup {* + Meson_Choices.setup + #> Meson.setup + #> Meson_Clausify.setup +*} + +end diff -r 1f01c9b2b76b -r 02fcd9cd1eac src/HOL/Plain.thy --- a/src/HOL/Plain.thy Mon Oct 04 21:37:42 2010 +0200 +++ b/src/HOL/Plain.thy Mon Oct 04 21:49:07 2010 +0200 @@ -1,7 +1,7 @@ header {* Plain HOL *} theory Plain -imports Datatype FunDef Extraction +imports Datatype FunDef Extraction Meson begin text {* diff -r 1f01c9b2b76b -r 02fcd9cd1eac src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Mon Oct 04 21:37:42 2010 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Mon Oct 04 21:49:07 2010 +0200 @@ -1,5 +1,6 @@ -(* Title: HOL/Tools/meson.ML +(* Title: HOL/Tools/Meson/meson.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen The MESON resolution proof procedure for HOL. When making clauses, avoids using the rewriter -- instead uses RS recursively. diff -r 1f01c9b2b76b -r 02fcd9cd1eac src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Oct 04 21:37:42 2010 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Oct 04 21:49:07 2010 +0200 @@ -1,8 +1,9 @@ -(* Title: HOL/Tools/Sledgehammer/meson_clausify.ML +(* Title: HOL/Tools/Meson/meson_clausify.ML Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen -Transformation of axiom rules (elim/intro/etc) into CNF forms. +Transformation of HOL theorems into CNF forms. +The "meson" proof method for HOL. *) signature MESON_CLAUSIFY = @@ -204,7 +205,7 @@ val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of val T = case hilbert of - Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T + Const (_, Type (@{type_name fun}, [_, T])) => T | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"", [hilbert]) val cex = cterm_of thy (HOLogic.exists_const T) @@ -214,7 +215,8 @@ |> Drule.beta_conv cabs |> Thm.capply cTrueprop fun tacf [prem] = rewrite_goals_tac skolem_def_raw - THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1 + THEN rtac ((prem |> rewrite_rule skolem_def_raw) + RS Global_Theory.get_thm thy "someI_ex") 1 in Goal.prove_internal [ex_tm] conc tacf |> forall_intr_list frees