# HG changeset patch # User wenzelm # Date 1205615245 -3600 # Node ID 3ff5d257f1755e842adf8dbb91992eff864cc9a4 # Parent 3905e52a1a0eec6e017ea567921565892d67eed0 added lemmas from simpdata.ML; diff -r 3905e52a1a0e -r 3ff5d257f175 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Sat Mar 15 18:08:54 2008 +0100 +++ b/src/FOL/FOL.thy Sat Mar 15 22:07:25 2008 +0100 @@ -198,6 +198,91 @@ lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast + + +(*** Classical simplification rules ***) + +(*Avoids duplication of subgoals after expand_if, when the true and false + cases boil down to the same thing.*) +lemma cases_simp: "(P --> Q) & (~P --> Q) <-> Q" by blast + + +(*** Miniscoping: pushing quantifiers in + We do NOT distribute of ALL over &, or dually that of EX over | + Baaz and Leitsch, On Skolemization and Proof Complexity (1994) + show that this step can increase proof length! +***) + +(*existential miniscoping*) +lemma int_ex_simps: + "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q" + "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))" + "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q" + "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))" + by iprover+ + +(*classical rules*) +lemma cla_ex_simps: + "!!P Q. (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q" + "!!P Q. (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))" + by blast+ + +lemmas ex_simps = int_ex_simps cla_ex_simps + +(*universal miniscoping*) +lemma int_all_simps: + "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q" + "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))" + "!!P Q. (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q" + "!!P Q. (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))" + by iprover+ + +(*classical rules*) +lemma cla_all_simps: + "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q" + "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))" + by blast+ + +lemmas all_simps = int_all_simps cla_all_simps + + +(*** Named rewrite rules proved for IFOL ***) + +lemma imp_disj1: "(P-->Q) | R <-> (P-->Q | R)" by blast +lemma imp_disj2: "Q | (P-->R) <-> (P-->Q | R)" by blast + +lemma de_Morgan_conj: "(~(P & Q)) <-> (~P | ~Q)" by blast + +lemma not_imp: "~(P --> Q) <-> (P & ~Q)" by blast +lemma not_iff: "~(P <-> Q) <-> (P <-> ~Q)" by blast + +lemma not_all: "(~ (ALL x. P(x))) <-> (EX x.~P(x))" by blast +lemma imp_all: "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)" by blast + + +lemmas meta_simps = + triv_forall_equality (* prunes params *) + True_implies_equals (* prune asms `True' *) + +lemmas IFOL_simps = + refl [THEN P_iff_T] conj_simps disj_simps not_simps + imp_simps iff_simps quant_simps + +lemma notFalseI: "~False" by iprover + +lemma cla_simps_misc: + "~(P&Q) <-> ~P | ~Q" + "P | ~P" + "~P | P" + "~ ~ P <-> P" + "(~P --> P) <-> P" + "(~P <-> ~Q) <-> (P<->Q)" by blast+ + +lemmas cla_simps = + de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 + not_imp not_all not_ex cases_simp cla_simps_misc + + use "simpdata.ML" setup simpsetup setup "Simplifier.method_setup Splitter.split_modifiers" diff -r 3905e52a1a0e -r 3ff5d257f175 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sat Mar 15 18:08:54 2008 +0100 +++ b/src/FOL/IFOL.thy Sat Mar 15 22:07:25 2008 +0100 @@ -784,7 +784,115 @@ done -subsection {* ML bindings *} +subsection {* Intuitionistic simplification rules *} + +lemma conj_simps: + "P & True <-> P" + "True & P <-> P" + "P & False <-> False" + "False & P <-> False" + "P & P <-> P" + "P & P & Q <-> P & Q" + "P & ~P <-> False" + "~P & P <-> False" + "(P & Q) & R <-> P & (Q & R)" + by iprover+ + +lemma disj_simps: + "P | True <-> True" + "True | P <-> True" + "P | False <-> P" + "False | P <-> P" + "P | P <-> P" + "P | P | Q <-> P | Q" + "(P | Q) | R <-> P | (Q | R)" + by iprover+ + +lemma not_simps: + "~(P|Q) <-> ~P & ~Q" + "~ False <-> True" + "~ True <-> False" + by iprover+ + +lemma imp_simps: + "(P --> False) <-> ~P" + "(P --> True) <-> True" + "(False --> P) <-> True" + "(True --> P) <-> P" + "(P --> P) <-> True" + "(P --> ~P) <-> ~P" + by iprover+ + +lemma iff_simps: + "(True <-> P) <-> P" + "(P <-> True) <-> P" + "(P <-> P) <-> True" + "(False <-> P) <-> ~P" + "(P <-> False) <-> ~P" + by iprover+ + +(*The x=t versions are needed for the simplification procedures*) +lemma quant_simps: + "!!P. (ALL x. P) <-> P" + "(ALL x. x=t --> P(x)) <-> P(t)" + "(ALL x. t=x --> P(x)) <-> P(t)" + "!!P. (EX x. P) <-> P" + "EX x. x=t" + "EX x. t=x" + "(EX x. x=t & P(x)) <-> P(t)" + "(EX x. t=x & P(x)) <-> P(t)" + by iprover+ + +(*These are NOT supplied by default!*) +lemma distrib_simps: + "P & (Q | R) <-> P&Q | P&R" + "(Q | R) & P <-> Q&P | R&P" + "(P | Q --> R) <-> (P --> R) & (Q --> R)" + by iprover+ + + +text {* Conversion into rewrite rules *} + +lemma P_iff_F: "~P ==> (P <-> False)" by iprover +lemma iff_reflection_F: "~P ==> (P == False)" by (rule P_iff_F [THEN iff_reflection]) + +lemma P_iff_T: "P ==> (P <-> True)" by iprover +lemma iff_reflection_T: "P ==> (P == True)" by (rule P_iff_T [THEN iff_reflection]) + + +text {* More rewrite rules *} + +lemma conj_commute: "P&Q <-> Q&P" by iprover +lemma conj_left_commute: "P&(Q&R) <-> Q&(P&R)" by iprover +lemmas conj_comms = conj_commute conj_left_commute + +lemma disj_commute: "P|Q <-> Q|P" by iprover +lemma disj_left_commute: "P|(Q|R) <-> Q|(P|R)" by iprover +lemmas disj_comms = disj_commute disj_left_commute + +lemma conj_disj_distribL: "P&(Q|R) <-> (P&Q | P&R)" by iprover +lemma conj_disj_distribR: "(P|Q)&R <-> (P&R | Q&R)" by iprover + +lemma disj_conj_distribL: "P|(Q&R) <-> (P|Q) & (P|R)" by iprover +lemma disj_conj_distribR: "(P&Q)|R <-> (P|R) & (Q|R)" by iprover + +lemma imp_conj_distrib: "(P --> (Q&R)) <-> (P-->Q) & (P-->R)" by iprover +lemma imp_conj: "((P&Q)-->R) <-> (P --> (Q --> R))" by iprover +lemma imp_disj: "(P|Q --> R) <-> (P-->R) & (Q-->R)" by iprover + +lemma de_Morgan_disj: "(~(P | Q)) <-> (~P & ~Q)" by iprover + +lemma not_ex: "(~ (EX x. P(x))) <-> (ALL x.~P(x))" by iprover +lemma imp_ex: "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)" by iprover + +lemma ex_disj_distrib: + "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))" by iprover + +lemma all_conj_distrib: + "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover + + +subsection {* Legacy ML bindings *} ML {* val refl = @{thm refl}