18 lemma nonempty: "L(0)" |
18 lemma nonempty: "L(0)" |
19 apply (simp add: L_def) |
19 apply (simp add: L_def) |
20 apply (blast intro: zero_in_Lset) |
20 apply (blast intro: zero_in_Lset) |
21 done |
21 done |
22 |
22 |
23 lemma upair_ax: "upair_ax(L)" |
23 theorem upair_ax: "upair_ax(L)" |
24 apply (simp add: upair_ax_def upair_def, clarify) |
24 apply (simp add: upair_ax_def upair_def, clarify) |
25 apply (rule_tac x="{x,y}" in rexI) |
25 apply (rule_tac x="{x,y}" in rexI) |
26 apply (simp_all add: doubleton_in_L) |
26 apply (simp_all add: doubleton_in_L) |
27 done |
27 done |
28 |
28 |
29 lemma Union_ax: "Union_ax(L)" |
29 theorem Union_ax: "Union_ax(L)" |
30 apply (simp add: Union_ax_def big_union_def, clarify) |
30 apply (simp add: Union_ax_def big_union_def, clarify) |
31 apply (rule_tac x="Union(x)" in rexI) |
31 apply (rule_tac x="Union(x)" in rexI) |
32 apply (simp_all add: Union_in_L, auto) |
32 apply (simp_all add: Union_in_L, auto) |
33 apply (blast intro: transL) |
33 apply (blast intro: transL) |
34 done |
34 done |
35 |
35 |
36 lemma power_ax: "power_ax(L)" |
36 theorem power_ax: "power_ax(L)" |
37 apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify) |
37 apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify) |
38 apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI) |
38 apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI) |
39 apply (simp_all add: LPow_in_L, auto) |
39 apply (simp_all add: LPow_in_L, auto) |
|
40 apply (blast intro: transL) |
|
41 done |
|
42 |
|
43 text{*We don't actually need @{term L} to satisfy the foundation axiom.*} |
|
44 theorem foundation_ax: "foundation_ax(L)" |
|
45 apply (simp add: foundation_ax_def) |
|
46 apply (rule rallI) |
|
47 apply (cut_tac A=x in foundation) |
40 apply (blast intro: transL) |
48 apply (blast intro: transL) |
41 done |
49 done |
42 |
50 |
43 subsection{*For L to satisfy Replacement *} |
51 subsection{*For L to satisfy Replacement *} |
44 |
52 |
63 apply (drule L_D, clarify) |
71 apply (drule L_D, clarify) |
64 apply (drule LReplace_in_Lset, assumption+) |
72 apply (drule LReplace_in_Lset, assumption+) |
65 apply (blast intro: L_I Lset_in_Lset_succ) |
73 apply (blast intro: L_I Lset_in_Lset_succ) |
66 done |
74 done |
67 |
75 |
68 lemma replacement: "replacement(L,P)" |
76 theorem replacement: "replacement(L,P)" |
69 apply (simp add: replacement_def, clarify) |
77 apply (simp add: replacement_def, clarify) |
70 apply (frule LReplace_in_L, assumption+, clarify) |
78 apply (frule LReplace_in_L, assumption+, clarify) |
71 apply (rule_tac x=Y in rexI) |
79 apply (rule_tac x=Y in rexI) |
72 apply (simp_all add: Replace_iff univalent_def, blast) |
80 apply (simp_all add: Replace_iff univalent_def, blast) |
73 done |
81 done |