--- a/src/ZF/AC/AC15_WO6.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC15_WO6.thy Fri Jul 25 07:35:53 2008 +0200
@@ -20,7 +20,9 @@
Rubin & Rubin do.
*)
-theory AC15_WO6 imports HH Cardinal_aux begin
+theory AC15_WO6
+imports HH Cardinal_aux
+begin
(* ********************************************************************** *)
--- a/src/ZF/AC/AC16_WO4.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC16_WO4.thy Fri Jul 25 07:35:53 2008 +0200
@@ -7,7 +7,9 @@
Tidied (using locales) by LCP
*)
-theory AC16_WO4 imports AC16_lemmas begin
+theory AC16_WO4
+imports AC16_lemmas
+begin
(* ********************************************************************** *)
(* The case of finite set *)
@@ -202,8 +204,7 @@
by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
succ_lepoll_natE)
-
-locale (open) AC16 =
+locale AC16 =
fixes x and y and k and l and m and t_n and R and MM and LL and GG and s
defines k_def: "k == succ(l)"
and MM_def: "MM == {v \<in> t_n. succ(k) \<lesssim> v Int y}"
@@ -558,9 +559,11 @@
(* The main theorem AC16(n, k) ==> WO4(n-k) *)
(* ********************************************************************** *)
+term AC16
+
theorem AC16_WO4:
- "[| AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat |] ==> WO4(m)"
-apply (unfold AC16_def WO4_def)
+ "[| AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat |] ==> WO4(m)"
+apply (unfold AC_Equiv.AC16_def WO4_def)
apply (rule allI)
apply (case_tac "Finite (A)")
apply (rule lemma1, assumption+)
@@ -569,7 +572,7 @@
apply (erule_tac x = "A Un y" in allE)
apply (frule infinite_Un, drule mp, assumption)
apply (erule zero_lt_natE, assumption, clarify)
-apply (blast intro: AC16.conclusion)
+apply (blast intro: AC16.conclusion [OF AC16.intro])
done
end
--- a/src/ZF/AC/AC16_lemmas.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC16_lemmas.thy Fri Jul 25 07:35:53 2008 +0200
@@ -5,7 +5,9 @@
Lemmas used in the proofs concerning AC16
*)
-theory AC16_lemmas imports AC_Equiv Hartog Cardinal_aux begin
+theory AC16_lemmas
+imports AC_Equiv Hartog Cardinal_aux
+begin
lemma cons_Diff_eq: "a\<notin>A ==> cons(a,A)-{a}=A"
by fast
--- a/src/ZF/AC/AC17_AC1.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC17_AC1.thy Fri Jul 25 07:35:53 2008 +0200
@@ -8,7 +8,9 @@
to AC0 and AC1.
*)
-theory AC17_AC1 imports HH begin
+theory AC17_AC1
+imports HH
+begin
(** AC0 is equivalent to AC1.
--- a/src/ZF/AC/AC18_AC19.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC18_AC19.thy Fri Jul 25 07:35:53 2008 +0200
@@ -5,7 +5,9 @@
The proof of AC1 ==> AC18 ==> AC19 ==> AC1
*)
-theory AC18_AC19 imports AC_Equiv begin
+theory AC18_AC19
+imports AC_Equiv
+begin
definition
uu :: "i => i" where
--- a/src/ZF/AC/AC7_AC9.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC7_AC9.thy Fri Jul 25 07:35:53 2008 +0200
@@ -6,7 +6,9 @@
instances of AC.
*)
-theory AC7_AC9 imports AC_Equiv begin
+theory AC7_AC9
+imports AC_Equiv
+begin
(* ********************************************************************** *)
(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *)
--- a/src/ZF/AC/AC_Equiv.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC_Equiv.thy Fri Jul 25 07:35:53 2008 +0200
@@ -12,7 +12,9 @@
but slightly changed.
*)
-theory AC_Equiv imports Main begin (*obviously not Main_ZFC*)
+theory AC_Equiv
+imports Main
+begin (*obviously not Main_ZFC*)
(* Well Ordering Theorems *)
--- a/src/ZF/AC/DC.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/DC.thy Fri Jul 25 07:35:53 2008 +0200
@@ -5,7 +5,9 @@
The proofs concerning the Axiom of Dependent Choice
*)
-theory DC imports AC_Equiv Hartog Cardinal_aux begin
+theory DC
+imports AC_Equiv Hartog Cardinal_aux
+begin
lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a"
apply (unfold lepoll_def)
@@ -95,7 +97,7 @@
transrec(b, %c r. THE x. first(x, {x \<in> X. <r``c, x> \<in> R}, Q))"
-locale (open) DC0_imp =
+locale DC0_imp =
fixes XX and RR and X and R
assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat --> (\<exists>x \<in> X. <Y, x> \<in> R)"
@@ -237,16 +239,16 @@
apply (elim allE)
apply (erule impE)
(*these three results comprise Lemma 1*)
-apply (blast intro!: DC0_imp.lemma1_1 DC0_imp.lemma1_2 DC0_imp.lemma1_3)
+apply (blast intro!: DC0_imp.lemma1_1 [OF DC0_imp.intro] DC0_imp.lemma1_2 [OF DC0_imp.intro] DC0_imp.lemma1_3 [OF DC0_imp.intro])
apply (erule bexE)
apply (rule_tac x = "\<lambda>n \<in> nat. f`succ (n) `n" in rev_bexI)
- apply (rule lam_type, blast dest!: DC0_imp.lemma2 intro: fun_weaken_type)
+ apply (rule lam_type, blast dest!: DC0_imp.lemma2 [OF DC0_imp.intro] intro: fun_weaken_type)
apply (rule oallI)
-apply (frule DC0_imp.lemma2, assumption)
+apply (frule DC0_imp.lemma2 [OF DC0_imp.intro], assumption)
apply (blast intro: fun_weaken_type)
apply (erule ltD)
(** LEVEL 11: last subgoal **)
-apply (subst DC0_imp.lemma3, assumption+)
+apply (subst DC0_imp.lemma3 [OF DC0_imp.intro], assumption+)
apply (fast elim!: fun_weaken_type)
apply (erule ltD)
apply (force simp add: lt_def)
@@ -293,7 +295,7 @@
done
-locale (open) imp_DC0 =
+locale imp_DC0 =
fixes XX and RR and x and R and f and allRR
defines XX_def: "XX == (\<Union>n \<in> nat.
{f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})"
--- a/src/ZF/AC/HH.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/HH.thy Fri Jul 25 07:35:53 2008 +0200
@@ -8,7 +8,9 @@
AC15 ==> WO6
*)
-theory HH imports AC_Equiv Hartog begin
+theory HH
+imports AC_Equiv Hartog
+begin
definition
HH :: "[i, i, i] => i" where
--- a/src/ZF/AC/Hartog.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/Hartog.thy Fri Jul 25 07:35:53 2008 +0200
@@ -5,7 +5,9 @@
Hartog's function.
*)
-theory Hartog imports AC_Equiv begin
+theory Hartog
+imports AC_Equiv
+begin
definition
Hartog :: "i => i" where
--- a/src/ZF/AC/WO1_AC.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/WO1_AC.thy Fri Jul 25 07:35:53 2008 +0200
@@ -25,7 +25,9 @@
*)
-theory WO1_AC imports AC_Equiv begin
+theory WO1_AC
+imports AC_Equiv
+begin
(* ********************************************************************** *)
(* WO1 ==> AC1 *)
--- a/src/ZF/AC/WO1_WO7.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/WO1_WO7.thy Fri Jul 25 07:35:53 2008 +0200
@@ -9,7 +9,9 @@
Also, WO1 <-> WO8
*)
-theory WO1_WO7 imports AC_Equiv begin
+theory WO1_WO7
+imports AC_Equiv
+begin
definition
"LEMMA ==
--- a/src/ZF/AC/WO6_WO1.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/WO6_WO1.thy Fri Jul 25 07:35:53 2008 +0200
@@ -11,7 +11,9 @@
Fortunately order types made this proof also very easy.
*)
-theory WO6_WO1 imports Cardinal_aux begin
+theory WO6_WO1
+imports Cardinal_aux
+begin
(* Auxiliary definitions used in proof *)
definition