8 |
8 |
9 header{*Miscellaneous ZF Examples*} |
9 header{*Miscellaneous ZF Examples*} |
10 |
10 |
11 theory misc imports Main begin |
11 theory misc imports Main begin |
12 |
12 |
|
13 |
13 subsection{*Various Small Problems*} |
14 subsection{*Various Small Problems*} |
|
15 |
|
16 text{*The singleton problems are much harder in HOL.*} |
|
17 lemma singleton_example_1: |
|
18 "\<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
|
19 by blast |
|
20 |
|
21 lemma singleton_example_2: |
|
22 "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
|
23 -- {*Variant of the problem above. *} |
|
24 by blast |
|
25 |
|
26 lemma "\<exists>!x. f (g(x)) = x \<Longrightarrow> \<exists>!y. g (f(y)) = y" |
|
27 -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text auto} all fail. *} |
|
28 apply (erule ex1E, rule ex1I, erule subst_context) |
|
29 apply (rule subst, assumption, erule allE, rule subst_context, erule mp) |
|
30 apply (erule subst_context) |
|
31 done |
|
32 |
14 |
33 |
15 text{*A weird property of ordered pairs.*} |
34 text{*A weird property of ordered pairs.*} |
16 lemma "b\<noteq>c ==> <a,b> Int <a,c> = <a,a>" |
35 lemma "b\<noteq>c ==> <a,b> Int <a,c> = <a,a>" |
17 by (simp add: Pair_def Int_cons_left Int_cons_right doubleton_eq_iff, blast) |
36 by (simp add: Pair_def Int_cons_left Int_cons_right doubleton_eq_iff, blast) |
18 |
37 |