theory Blast imports Main begin
lemma "((\x. \y. p(x)=p(y)) = ((\x. q(x))=(\y. p(y)))) =
((\<exists>x. \<forall>y. q(x)=q(y)) = ((\<exists>x. p(x))=(\<forall>y. q(y))))"
by blast
text\<open>\noindent Until now, we have proved everything using only induction and
simplification. Substantial proofs require more elaborate types of
inference.\<close>
lemma "(\x. honest(x) \ industrious(x) \ healthy(x)) \
\<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and>
(\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
(\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
(\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
\<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))"
by blast
lemma "(\i\I. A(i)) \ (\j\J. B(j)) =
(\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
by blast
text \<open>
@{thm[display] mult_is_0}
\rulename{mult_is_0}}
@{thm[display] finite_Un}
\rulename{finite_Un}}
\<close>
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
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
