Theory Blast

theory Blast imports Main begin

lemma "((∃x. ∀y. p(x)=p(y)) = ((∃x. q(x))=(∀y. p(y))))   =    
       ((∃x. ∀y. q(x)=q(y)) = ((∃x. p(x))=(∀y. q(y))))"
by blast

text‹\noindent Until now, we have proved everything using only induction and
simplification.  Substantial proofs require more elaborate types of
inference.›

lemma "(∀x. honest(x) ∧ industrious(x) ⟶ healthy(x)) ∧  
       ¬ (∃x. grocer(x) ∧ healthy(x)) ∧ 
       (∀x. industrious(x) ∧ grocer(x) ⟶ honest(x)) ∧ 
       (∀x. cyclist(x) ⟶ industrious(x)) ∧ 
       (∀x. ¬healthy(x) ∧ cyclist(x) ⟶ ¬honest(x))  
       ⟶ (∀x. grocer(x) ⟶ ¬cyclist(x))"
by blast

lemma "(⋃i∈I. A(i)) ∩ (⋃j∈J. B(j)) =
        (⋃i∈I. ⋃j∈J. A(i) ∩ B(j))"
by blast

text ‹
@{thm[display] mult_is_0}
 \rulename{mult_is_0}}

@{thm[display] finite_Un}
 \rulename{finite_Un}}
›


lemma [iff]: "(xs@ys = []) = (xs=[] & ys=[])"
  apply (induct_tac xs)
  by (simp_all)

(*ideas for uses of intro, etc.: ex/Primes/is_gcd_unique?*)
end