|
16417
|
1 |
theory Blast imports Main begin
|
|
10295
|
2 |
|
|
|
3 |
lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y)))) =
|
|
|
4 |
((\<exists>x. \<forall>y. q(x)=q(y)) = ((\<exists>x. p(x))=(\<forall>y. q(y))))"
|
|
10844
|
5 |
by blast
|
|
10295
|
6 |
|
|
67406
|
7 |
text\<open>\noindent Until now, we have proved everything using only induction and
|
|
10295
|
8 |
simplification. Substantial proofs require more elaborate types of
|
|
67406
|
9 |
inference.\<close>
|
|
10295
|
10 |
|
|
|
11 |
lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>
|
|
|
12 |
\<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and>
|
|
|
13 |
(\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
|
|
|
14 |
(\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
|
|
|
15 |
(\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
|
|
58860
|
16 |
\<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))"
|
|
10844
|
17 |
by blast
|
|
10295
|
18 |
|
|
|
19 |
lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
|
|
|
20 |
(\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
|
|
10844
|
21 |
by blast
|
|
10295
|
22 |
|
|
67406
|
23 |
text \<open>
|
|
10295
|
24 |
@{thm[display] mult_is_0}
|
|
|
25 |
\rulename{mult_is_0}}
|
|
|
26 |
|
|
|
27 |
@{thm[display] finite_Un}
|
|
|
28 |
\rulename{finite_Un}}
|
|
67406
|
29 |
\<close>
|
|
10295
|
30 |
|
|
|
31 |
|
|
|
32 |
lemma [iff]: "(xs@ys = []) = (xs=[] & ys=[])"
|
|
|
33 |
apply (induct_tac xs)
|
|
58860
|
34 |
by (simp_all)
|
|
10295
|
35 |
|
|
|
36 |
(*ideas for uses of intro, etc.: ex/Primes/is_gcd_unique?*)
|
|
|
37 |
end
|