AC18: meta-level predicate via locale;

--- a/src/ZF/AC/AC18_AC19.thy	Wed Jul 24 00:12:50 2002 +0200
+++ b/src/ZF/AC/AC18_AC19.thy	Wed Jul 24 00:13:41 2002 +0200
@@ -34,8 +34,9 @@
 apply (simp, fast elim!: not_emptyE dest: apply_type [OF _ RepFunI])
 done
 
-lemma AC1_AC18: "AC1 ==> AC18"
-apply (unfold AC1_def AC18_def)
+lemma AC1_AC18: "AC1 ==> PROP AC18"
+apply (unfold AC1_def)
+apply (rule AC18.intro [OF AC18_axioms.intro])
 apply (fast elim!: lemma_AC18 apply_type intro!: equalityI INT_I UN_I)
 done
 
@@ -43,16 +44,11 @@
 (* AC18 ==> AC19                                                          *)
 (* ********************************************************************** *)
 
-text{*Hard to express because of the need for meta-quantifiers in AC18*}
-lemma "AC18 ==> AC19"
-proof -
-  assume ac18 [unfolded AC18_def, norm_hhf]: AC18
-  show AC19
-    apply (unfold AC18_def AC19_def)
-    apply (intro allI impI) 
-    apply (rule ac18 [of _ "%x. x", THEN mp], blast) 
-    done
-qed
+theorem (in AC18) AC19
+apply (unfold AC19_def)
+apply (intro allI impI)
+apply (rule AC18 [of _ "%x. x", THEN mp], blast)
+done
 
 (* ********************************************************************** *)
 (* AC19 ==> AC1                                                           *)

--- a/src/ZF/AC/AC_Equiv.thy	Wed Jul 24 00:12:50 2002 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Wed Jul 24 00:13:41 2002 +0200
@@ -118,12 +118,13 @@
     "AC17 == \<forall>A. \<forall>g \<in> (Pow(A)-{0} -> A) -> Pow(A)-{0}.   
 		   \<exists>f \<in> Pow(A)-{0} -> A. f`(g`f) \<in> g`f"
 
-  AC18 :: "prop" ("AC18")
-    "AC18 == (!!X A B. A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) -->   
-		((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =   
-		(\<Union>f \<in> \<Pi>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))))"
-  --"AC18 can be expressed only using meta-level quantification"
+locale AC18 =
+  assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) -->
+    ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =   
+      (\<Union>f \<in> \<Pi>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
+  --"AC18 cannot be expressed within the object-logic"
 
+constdefs
   AC19 :: o
     "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A --> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =   
 		   (\<Union>f \<in> (\<Pi>B \<in> A. B). \<Inter>a \<in> A. f`a))"