# 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}