added lemmas from simpdata.ML;
authorwenzelm
Sat Mar 15 22:07:25 2008 +0100 (2008-03-15)
changeset 262863ff5d257f175
parent 26285 3905e52a1a0e
child 26287 df8e5362cff9
added lemmas from simpdata.ML;
src/FOL/FOL.thy
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/FOL.thy	Sat Mar 15 18:08:54 2008 +0100
     1.2 +++ b/src/FOL/FOL.thy	Sat Mar 15 22:07:25 2008 +0100
     1.3 @@ -198,6 +198,91 @@
     1.4  
     1.5  lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast
     1.6  
     1.7 +
     1.8 +
     1.9 +(*** Classical simplification rules ***)
    1.10 +
    1.11 +(*Avoids duplication of subgoals after expand_if, when the true and false
    1.12 +  cases boil down to the same thing.*)
    1.13 +lemma cases_simp: "(P --> Q) & (~P --> Q) <-> Q" by blast
    1.14 +
    1.15 +
    1.16 +(*** Miniscoping: pushing quantifiers in
    1.17 +     We do NOT distribute of ALL over &, or dually that of EX over |
    1.18 +     Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
    1.19 +     show that this step can increase proof length!
    1.20 +***)
    1.21 +
    1.22 +(*existential miniscoping*)
    1.23 +lemma int_ex_simps:
    1.24 +  "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
    1.25 +  "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
    1.26 +  "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
    1.27 +  "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
    1.28 +  by iprover+
    1.29 +
    1.30 +(*classical rules*)
    1.31 +lemma cla_ex_simps:
    1.32 +  "!!P Q. (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
    1.33 +  "!!P Q. (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
    1.34 +  by blast+
    1.35 +
    1.36 +lemmas ex_simps = int_ex_simps cla_ex_simps
    1.37 +
    1.38 +(*universal miniscoping*)
    1.39 +lemma int_all_simps:
    1.40 +  "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
    1.41 +  "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
    1.42 +  "!!P Q. (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
    1.43 +  "!!P Q. (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
    1.44 +  by iprover+
    1.45 +
    1.46 +(*classical rules*)
    1.47 +lemma cla_all_simps:
    1.48 +  "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
    1.49 +  "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
    1.50 +  by blast+
    1.51 +
    1.52 +lemmas all_simps = int_all_simps cla_all_simps
    1.53 +
    1.54 +
    1.55 +(*** Named rewrite rules proved for IFOL ***)
    1.56 +
    1.57 +lemma imp_disj1: "(P-->Q) | R <-> (P-->Q | R)" by blast
    1.58 +lemma imp_disj2: "Q | (P-->R) <-> (P-->Q | R)" by blast
    1.59 +
    1.60 +lemma de_Morgan_conj: "(~(P & Q)) <-> (~P | ~Q)" by blast
    1.61 +
    1.62 +lemma not_imp: "~(P --> Q) <-> (P & ~Q)" by blast
    1.63 +lemma not_iff: "~(P <-> Q) <-> (P <-> ~Q)" by blast
    1.64 +
    1.65 +lemma not_all: "(~ (ALL x. P(x))) <-> (EX x.~P(x))" by blast
    1.66 +lemma imp_all: "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)" by blast
    1.67 +
    1.68 +
    1.69 +lemmas meta_simps =
    1.70 +  triv_forall_equality (* prunes params *)
    1.71 +  True_implies_equals  (* prune asms `True' *)
    1.72 +
    1.73 +lemmas IFOL_simps =
    1.74 +  refl [THEN P_iff_T] conj_simps disj_simps not_simps
    1.75 +  imp_simps iff_simps quant_simps
    1.76 +
    1.77 +lemma notFalseI: "~False" by iprover
    1.78 +
    1.79 +lemma cla_simps_misc:
    1.80 +  "~(P&Q) <-> ~P | ~Q"
    1.81 +  "P | ~P"
    1.82 +  "~P | P"
    1.83 +  "~ ~ P <-> P"
    1.84 +  "(~P --> P) <-> P"
    1.85 +  "(~P <-> ~Q) <-> (P<->Q)" by blast+
    1.86 +
    1.87 +lemmas cla_simps =
    1.88 +  de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
    1.89 +  not_imp not_all not_ex cases_simp cla_simps_misc
    1.90 +
    1.91 +
    1.92  use "simpdata.ML"
    1.93  setup simpsetup
    1.94  setup "Simplifier.method_setup Splitter.split_modifiers"
     2.1 --- a/src/FOL/IFOL.thy	Sat Mar 15 18:08:54 2008 +0100
     2.2 +++ b/src/FOL/IFOL.thy	Sat Mar 15 22:07:25 2008 +0100
     2.3 @@ -784,7 +784,115 @@
     2.4    done
     2.5  
     2.6  
     2.7 -subsection {* ML bindings *}
     2.8 +subsection {* Intuitionistic simplification rules *}
     2.9 +
    2.10 +lemma conj_simps:
    2.11 +  "P & True <-> P"
    2.12 +  "True & P <-> P"
    2.13 +  "P & False <-> False"
    2.14 +  "False & P <-> False"
    2.15 +  "P & P <-> P"
    2.16 +  "P & P & Q <-> P & Q"
    2.17 +  "P & ~P <-> False"
    2.18 +  "~P & P <-> False"
    2.19 +  "(P & Q) & R <-> P & (Q & R)"
    2.20 +  by iprover+
    2.21 +
    2.22 +lemma disj_simps:
    2.23 +  "P | True <-> True"
    2.24 +  "True | P <-> True"
    2.25 +  "P | False <-> P"
    2.26 +  "False | P <-> P"
    2.27 +  "P | P <-> P"
    2.28 +  "P | P | Q <-> P | Q"
    2.29 +  "(P | Q) | R <-> P | (Q | R)"
    2.30 +  by iprover+
    2.31 +
    2.32 +lemma not_simps:
    2.33 +  "~(P|Q)  <-> ~P & ~Q"
    2.34 +  "~ False <-> True"
    2.35 +  "~ True <-> False"
    2.36 +  by iprover+
    2.37 +
    2.38 +lemma imp_simps:
    2.39 +  "(P --> False) <-> ~P"
    2.40 +  "(P --> True) <-> True"
    2.41 +  "(False --> P) <-> True"
    2.42 +  "(True --> P) <-> P"
    2.43 +  "(P --> P) <-> True"
    2.44 +  "(P --> ~P) <-> ~P"
    2.45 +  by iprover+
    2.46 +
    2.47 +lemma iff_simps:
    2.48 +  "(True <-> P) <-> P"
    2.49 +  "(P <-> True) <-> P"
    2.50 +  "(P <-> P) <-> True"
    2.51 +  "(False <-> P) <-> ~P"
    2.52 +  "(P <-> False) <-> ~P"
    2.53 +  by iprover+
    2.54 +
    2.55 +(*The x=t versions are needed for the simplification procedures*)
    2.56 +lemma quant_simps:
    2.57 +  "!!P. (ALL x. P) <-> P"
    2.58 +  "(ALL x. x=t --> P(x)) <-> P(t)"
    2.59 +  "(ALL x. t=x --> P(x)) <-> P(t)"
    2.60 +  "!!P. (EX x. P) <-> P"
    2.61 +  "EX x. x=t"
    2.62 +  "EX x. t=x"
    2.63 +  "(EX x. x=t & P(x)) <-> P(t)"
    2.64 +  "(EX x. t=x & P(x)) <-> P(t)"
    2.65 +  by iprover+
    2.66 +
    2.67 +(*These are NOT supplied by default!*)
    2.68 +lemma distrib_simps:
    2.69 +  "P & (Q | R) <-> P&Q | P&R"
    2.70 +  "(Q | R) & P <-> Q&P | R&P"
    2.71 +  "(P | Q --> R) <-> (P --> R) & (Q --> R)"
    2.72 +  by iprover+
    2.73 +
    2.74 +
    2.75 +text {* Conversion into rewrite rules *}
    2.76 +
    2.77 +lemma P_iff_F: "~P ==> (P <-> False)" by iprover
    2.78 +lemma iff_reflection_F: "~P ==> (P == False)" by (rule P_iff_F [THEN iff_reflection])
    2.79 +
    2.80 +lemma P_iff_T: "P ==> (P <-> True)" by iprover
    2.81 +lemma iff_reflection_T: "P ==> (P == True)" by (rule P_iff_T [THEN iff_reflection])
    2.82 +
    2.83 +
    2.84 +text {* More rewrite rules *}
    2.85 +
    2.86 +lemma conj_commute: "P&Q <-> Q&P" by iprover
    2.87 +lemma conj_left_commute: "P&(Q&R) <-> Q&(P&R)" by iprover
    2.88 +lemmas conj_comms = conj_commute conj_left_commute
    2.89 +
    2.90 +lemma disj_commute: "P|Q <-> Q|P" by iprover
    2.91 +lemma disj_left_commute: "P|(Q|R) <-> Q|(P|R)" by iprover
    2.92 +lemmas disj_comms = disj_commute disj_left_commute
    2.93 +
    2.94 +lemma conj_disj_distribL: "P&(Q|R) <-> (P&Q | P&R)" by iprover
    2.95 +lemma conj_disj_distribR: "(P|Q)&R <-> (P&R | Q&R)" by iprover
    2.96 +
    2.97 +lemma disj_conj_distribL: "P|(Q&R) <-> (P|Q) & (P|R)" by iprover
    2.98 +lemma disj_conj_distribR: "(P&Q)|R <-> (P|R) & (Q|R)" by iprover
    2.99 +
   2.100 +lemma imp_conj_distrib: "(P --> (Q&R)) <-> (P-->Q) & (P-->R)" by iprover
   2.101 +lemma imp_conj: "((P&Q)-->R)   <-> (P --> (Q --> R))" by iprover
   2.102 +lemma imp_disj: "(P|Q --> R)   <-> (P-->R) & (Q-->R)" by iprover
   2.103 +
   2.104 +lemma de_Morgan_disj: "(~(P | Q)) <-> (~P & ~Q)" by iprover
   2.105 +
   2.106 +lemma not_ex: "(~ (EX x. P(x))) <-> (ALL x.~P(x))" by iprover
   2.107 +lemma imp_ex: "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)" by iprover
   2.108 +
   2.109 +lemma ex_disj_distrib:
   2.110 +  "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))" by iprover
   2.111 +
   2.112 +lemma all_conj_distrib:
   2.113 +  "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover
   2.114 +
   2.115 +
   2.116 +subsection {* Legacy ML bindings *}
   2.117  
   2.118  ML {*
   2.119  val refl = @{thm refl}