some basic new lemmas
authorpaulson
Tue Sep 23 15:42:01 2003 +0200 (2003-09-23)
changeset 142017ad7ab89c402
parent 14200 d8598e24f8fa
child 14202 643fc73e2910
some basic new lemmas
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Sep 23 15:41:33 2003 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Sep 23 15:42:01 2003 +0200
     1.3 @@ -380,6 +380,18 @@
     1.4    -- {* Miniscoping: pushing in universal quantifiers. *}
     1.5    by (rules | blast)+
     1.6  
     1.7 +lemma disj_absorb: "(A | A) = A"
     1.8 +  by blast
     1.9 +
    1.10 +lemma disj_left_absorb: "(A | (A | B)) = (A | B)"
    1.11 +  by blast
    1.12 +
    1.13 +lemma conj_absorb: "(A & A) = A"
    1.14 +  by blast
    1.15 +
    1.16 +lemma conj_left_absorb: "(A & (A & B)) = (A & B)"
    1.17 +  by blast
    1.18 +
    1.19  lemma eq_ac:
    1.20    shows eq_commute: "(a=b) = (b=a)"
    1.21      and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
    1.22 @@ -514,11 +526,15 @@
    1.23  lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
    1.24  lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules
    1.25  
    1.26 +subsubsection {* Actual Installation of the Simplifier *}
    1.27 +
    1.28  use "simpdata.ML"
    1.29  setup Simplifier.setup
    1.30  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    1.31  setup Splitter.setup setup Clasimp.setup
    1.32  
    1.33 +declare disj_absorb [simp] conj_absorb [simp] 
    1.34 +
    1.35  lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
    1.36  by blast+
    1.37