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)
end