Quelle  Blast.thy   Sprache: Isabelle

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