1(* Title: HOL/Meson.thy 2 Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 3 Author: Tobias Nipkow, TU Muenchen 4 Author: Jasmin Blanchette, TU Muenchen 5 Copyright 2001 University of Cambridge 6*) 7 8section \<open>MESON Proof Method\<close> 9 10theory Meson 11imports Nat 12begin 13 14subsection \<open>Negation Normal Form\<close> 15 16text \<open>de Morgan laws\<close> 17 18lemma not_conjD: "\<not>(P\<and>Q) \<Longrightarrow> \<not>P \<or> \<not>Q" 19 and not_disjD: "\<not>(P\<or>Q) \<Longrightarrow> \<not>P \<and> \<not>Q" 20 and not_notD: "\<not>\<not>P \<Longrightarrow> P" 21 and not_allD: "\<And>P. \<not>(\<forall>x. P(x)) \<Longrightarrow> \<exists>x. \<not>P(x)" 22 and not_exD: "\<And>P. \<not>(\<exists>x. P(x)) \<Longrightarrow> \<forall>x. \<not>P(x)" 23 by fast+ 24 25text \<open>Removal of \<open>\<longrightarrow>\<close> and \<open>\<longleftrightarrow>\<close> (positive and negative occurrences)\<close> 26 27lemma imp_to_disjD: "P\<longrightarrow>Q \<Longrightarrow> \<not>P \<or> Q" 28 and not_impD: "\<not>(P\<longrightarrow>Q) \<Longrightarrow> P \<and> \<not>Q" 29 and iff_to_disjD: "P=Q \<Longrightarrow> (\<not>P \<or> Q) \<and> (\<not>Q \<or> P)" 30 and not_iffD: "\<not>(P=Q) \<Longrightarrow> (P \<or> Q) \<and> (\<not>P \<or> \<not>Q)" 31 \<comment> \<open>Much more efficient than @{prop "(P \<and> \<not>Q) \<or> (Q \<and> \<not>P)"} for computing CNF\<close> 32 and not_refl_disj_D: "x \<noteq> x \<or> P \<Longrightarrow> P" 33 by fast+ 34 35 36subsection \<open>Pulling out the existential quantifiers\<close> 37 38text \<open>Conjunction\<close> 39 40lemma conj_exD1: "\<And>P Q. (\<exists>x. P(x)) \<and> Q \<Longrightarrow> \<exists>x. P(x) \<and> Q" 41 and conj_exD2: "\<And>P Q. P \<and> (\<exists>x. Q(x)) \<Longrightarrow> \<exists>x. P \<and> Q(x)" 42 by fast+ 43 44 45text \<open>Disjunction\<close> 46 47lemma disj_exD: "\<And>P Q. (\<exists>x. P(x)) \<or> (\<exists>x. Q(x)) \<Longrightarrow> \<exists>x. P(x) \<or> Q(x)" 48 \<comment> \<open>DO NOT USE with forall-Skolemization: makes fewer schematic variables!!\<close> 49 \<comment> \<open>With ex-Skolemization, makes fewer Skolem constants\<close> 50 and disj_exD1: "\<And>P Q. (\<exists>x. P(x)) \<or> Q \<Longrightarrow> \<exists>x. P(x) \<or> Q" 51 and disj_exD2: "\<And>P Q. P \<or> (\<exists>x. Q(x)) \<Longrightarrow> \<exists>x. P \<or> Q(x)" 52 by fast+ 53 54lemma disj_assoc: "(P\<or>Q)\<or>R \<Longrightarrow> P\<or>(Q\<or>R)" 55 and disj_comm: "P\<or>Q \<Longrightarrow> Q\<or>P" 56 and disj_FalseD1: "False\<or>P \<Longrightarrow> P" 57 and disj_FalseD2: "P\<or>False \<Longrightarrow> P" 58 by fast+ 59 60 61text\<open>Generation of contrapositives\<close> 62 63text\<open>Inserts negated disjunct after removing the negation; P is a literal. 64 Model elimination requires assuming the negation of every attempted subgoal, 65 hence the negated disjuncts.\<close> 66lemma make_neg_rule: "\<not>P\<or>Q \<Longrightarrow> ((\<not>P\<Longrightarrow>P) \<Longrightarrow> Q)" 67by blast 68 69text\<open>Version for Plaisted's "Postive refinement" of the Meson procedure\<close> 70lemma make_refined_neg_rule: "\<not>P\<or>Q \<Longrightarrow> (P \<Longrightarrow> Q)" 71by blast 72 73text\<open>@{term P} should be a literal\<close> 74lemma make_pos_rule: "P\<or>Q \<Longrightarrow> ((P\<Longrightarrow>\<not>P) \<Longrightarrow> Q)" 75by blast 76 77text\<open>Versions of \<open>make_neg_rule\<close> and \<open>make_pos_rule\<close> that don't 78insert new assumptions, for ordinary resolution.\<close> 79 80lemmas make_neg_rule' = make_refined_neg_rule 81 82lemma make_pos_rule': "\<lbrakk>P\<or>Q; \<not>P\<rbrakk> \<Longrightarrow> Q" 83by blast 84 85text\<open>Generation of a goal clause -- put away the final literal\<close> 86 87lemma make_neg_goal: "\<not>P \<Longrightarrow> ((\<not>P\<Longrightarrow>P) \<Longrightarrow> False)" 88by blast 89 90lemma make_pos_goal: "P \<Longrightarrow> ((P\<Longrightarrow>\<not>P) \<Longrightarrow> False)" 91by blast 92 93 94subsection \<open>Lemmas for Forward Proof\<close> 95 96text\<open>There is a similarity to congruence rules. They are also useful in ordinary proofs.\<close> 97 98(*NOTE: could handle conjunctions (faster?) by 99 nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) 100lemma conj_forward: "\<lbrakk>P'\<and>Q'; P' \<Longrightarrow> P; Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P\<and>Q" 101by blast 102 103lemma disj_forward: "\<lbrakk>P'\<or>Q'; P' \<Longrightarrow> P; Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P\<or>Q" 104by blast 105 106lemma imp_forward: "\<lbrakk>P' \<longrightarrow> Q'; P \<Longrightarrow> P'; Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P \<longrightarrow> Q" 107by blast 108 109(*Version of @{text disj_forward} for removal of duplicate literals*) 110lemma disj_forward2: "\<lbrakk> P'\<or>Q'; P' \<Longrightarrow> P; \<lbrakk>Q'; P\<Longrightarrow>False\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> P\<or>Q" 111apply blast 112done 113 114lemma all_forward: "[| \<forall>x. P'(x); !!x. P'(x) ==> P(x) |] ==> \<forall>x. P(x)" 115by blast 116 117lemma ex_forward: "[| \<exists>x. P'(x); !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)" 118by blast 119 120 121subsection \<open>Clausification helper\<close> 122 123lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q" 124by simp 125 126lemma ext_cong_neq: "F g \<noteq> F h \<Longrightarrow> F g \<noteq> F h \<and> (\<exists>x. g x \<noteq> h x)" 127apply (erule contrapos_np) 128apply clarsimp 129apply (rule cong[where f = F]) 130by auto 131 132 133text\<open>Combinator translation helpers\<close> 134 135definition COMBI :: "'a \<Rightarrow> 'a" where 136"COMBI P = P" 137 138definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where 139"COMBK P Q = P" 140 141definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where 142"COMBB P Q R = P (Q R)" 143 144definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where 145"COMBC P Q R = P R Q" 146 147definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where 148"COMBS P Q R = P R (Q R)" 149 150lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" 151apply (rule eq_reflection) 152apply (rule ext) 153apply (simp add: COMBS_def) 154done 155 156lemma abs_I: "\<lambda>x. x \<equiv> COMBI" 157apply (rule eq_reflection) 158apply (rule ext) 159apply (simp add: COMBI_def) 160done 161 162lemma abs_K: "\<lambda>x. y \<equiv> COMBK y" 163apply (rule eq_reflection) 164apply (rule ext) 165apply (simp add: COMBK_def) 166done 167 168lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g" 169apply (rule eq_reflection) 170apply (rule ext) 171apply (simp add: COMBB_def) 172done 173 174lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b" 175apply (rule eq_reflection) 176apply (rule ext) 177apply (simp add: COMBC_def) 178done 179 180 181subsection \<open>Skolemization helpers\<close> 182 183definition skolem :: "'a \<Rightarrow> 'a" where 184"skolem = (\<lambda>x. x)" 185 186lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i::nat))" 187unfolding skolem_def COMBK_def by (rule refl) 188 189lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] 190lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] 191 192 193subsection \<open>Meson package\<close> 194 195ML_file "Tools/Meson/meson.ML" 196ML_file "Tools/Meson/meson_clausify.ML" 197ML_file "Tools/Meson/meson_tactic.ML" 198 199hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem 200hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD 201 not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD 202 disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI 203 ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K 204 abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D 205 206end 207