src/HOL/HOL.thy

   "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
   "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
   -- {* Miniscoping: pushing in universal quantifiers. *}
   by (rules | blast)+
 
+lemma disj_absorb: "(A | A) = A"
+  by blast
+
+lemma disj_left_absorb: "(A | (A | B)) = (A | B)"
+  by blast
+
+lemma conj_absorb: "(A & A) = A"
+  by blast
+
+lemma conj_left_absorb: "(A & (A & B)) = (A & B)"
+  by blast
+
 lemma eq_ac:
   shows eq_commute: "(a=b) = (b=a)"
     and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
     and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)
 lemma neq_commute: "(a~=b) = (b~=a)" by rules

   done
 
 lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
 lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules
 
+subsubsection {* Actual Installation of the Simplifier *}
+
 use "simpdata.ML"
 setup Simplifier.setup
 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
 setup Splitter.setup setup Clasimp.setup
+
+declare disj_absorb [simp] conj_absorb [simp] 
 
 lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
 by blast+
 
 theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"