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>\<open>(P \<and> \<not>Q) \<or> (Q \<and> \<not>P)\<close> 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>\<open>P\<close> 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 109lemma imp_forward2: "\<lbrakk>P' \<longrightarrow> Q'; P \<Longrightarrow> P'; P' \<Longrightarrow> Q' \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> P \<longrightarrow> Q" 110 by blast 111 112(*Version of @{text disj_forward} for removal of duplicate literals*) 113lemma disj_forward2: "\<lbrakk> P'\<or>Q'; P' \<Longrightarrow> P; \<lbrakk>Q'; P\<Longrightarrow>False\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> P\<or>Q" 114apply blast 115done 116 117lemma all_forward: "[| \<forall>x. P'(x); !!x. P'(x) ==> P(x) |] ==> \<forall>x. P(x)" 118by blast 119 120lemma ex_forward: "[| \<exists>x. P'(x); !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)" 121by blast 122 123 124subsection \<open>Clausification helper\<close> 125 126lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q" 127by simp 128 129lemma ext_cong_neq: "F g \<noteq> F h \<Longrightarrow> F g \<noteq> F h \<and> (\<exists>x. g x \<noteq> h x)" 130apply (erule contrapos_np) 131apply clarsimp 132apply (rule cong[where f = F]) 133by auto 134 135 136text\<open>Combinator translation helpers\<close> 137 138definition COMBI :: "'a \<Rightarrow> 'a" where 139"COMBI P = P" 140 141definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where 142"COMBK P Q = P" 143 144definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where 145"COMBB P Q R = P (Q R)" 146 147definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where 148"COMBC P Q R = P R Q" 149 150definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where 151"COMBS P Q R = P R (Q R)" 152 153lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" 154apply (rule eq_reflection) 155apply (rule ext) 156apply (simp add: COMBS_def) 157done 158 159lemma abs_I: "\<lambda>x. x \<equiv> COMBI" 160apply (rule eq_reflection) 161apply (rule ext) 162apply (simp add: COMBI_def) 163done 164 165lemma abs_K: "\<lambda>x. y \<equiv> COMBK y" 166apply (rule eq_reflection) 167apply (rule ext) 168apply (simp add: COMBK_def) 169done 170 171lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g" 172apply (rule eq_reflection) 173apply (rule ext) 174apply (simp add: COMBB_def) 175done 176 177lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b" 178apply (rule eq_reflection) 179apply (rule ext) 180apply (simp add: COMBC_def) 181done 182 183 184subsection \<open>Skolemization helpers\<close> 185 186definition skolem :: "'a \<Rightarrow> 'a" where 187"skolem = (\<lambda>x. x)" 188 189lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i::nat))" 190unfolding skolem_def COMBK_def by (rule refl) 191 192lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] 193lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] 194 195 196subsection \<open>Meson package\<close> 197 198ML_file \<open>Tools/Meson/meson.ML\<close> 199ML_file \<open>Tools/Meson/meson_clausify.ML\<close> 200ML_file \<open>Tools/Meson/meson_tactic.ML\<close> 201 202hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem 203hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD 204 not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD 205 disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI 206 ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K 207 abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D 208 209end 210