--- a/src/ZF/Constructible/L_axioms.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Tue Nov 07 19:40:13 2006 +0100
@@ -114,7 +114,7 @@
subsection{*Instantiation of the locale @{text reflection}*}
text{*instances of locale constants*}
-constdefs
+definition
L_F0 :: "[i=>o,i] => i"
"L_F0(P,y) == \<mu> b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
@@ -127,7 +127,7 @@
text{*We must use the meta-existential quantifier; otherwise the reflection
terms become enormous!*}
-constdefs
+definition
L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])")
"REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) &
(\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x))))"
@@ -265,28 +265,26 @@
subsubsection{*Some numbers to help write de Bruijn indices*}
-syntax
- "3" :: i ("3")
- "4" :: i ("4")
- "5" :: i ("5")
- "6" :: i ("6")
- "7" :: i ("7")
- "8" :: i ("8")
- "9" :: i ("9")
-
-translations
- "3" == "succ(2)"
- "4" == "succ(3)"
- "5" == "succ(4)"
- "6" == "succ(5)"
- "7" == "succ(6)"
- "8" == "succ(7)"
- "9" == "succ(8)"
+abbreviation
+ digit3 :: i ("3")
+ "3 == succ(2)"
+ digit4 :: i ("4")
+ "4 == succ(3)"
+ digit5 :: i ("5")
+ "5 == succ(4)"
+ digit6 :: i ("6")
+ "6 == succ(5)"
+ digit7 :: i ("7")
+ "7 == succ(6)"
+ digit8 :: i ("8")
+ "8 == succ(7)"
+ digit9 :: i ("9")
+ "9 == succ(8)"
subsubsection{*The Empty Set, Internalized*}
-constdefs empty_fm :: "i=>i"
+definition empty_fm :: "i=>i"
"empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
lemma empty_type [TC]:
@@ -324,7 +322,7 @@
subsubsection{*Unordered Pairs, Internalized*}
-constdefs upair_fm :: "[i,i,i]=>i"
+definition upair_fm :: "[i,i,i]=>i"
"upair_fm(x,y,z) ==
And(Member(x,z),
And(Member(y,z),
@@ -366,7 +364,7 @@
subsubsection{*Ordered pairs, Internalized*}
-constdefs pair_fm :: "[i,i,i]=>i"
+definition pair_fm :: "[i,i,i]=>i"
"pair_fm(x,y,z) ==
Exists(And(upair_fm(succ(x),succ(x),0),
Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),
@@ -398,7 +396,7 @@
subsubsection{*Binary Unions, Internalized*}
-constdefs union_fm :: "[i,i,i]=>i"
+definition union_fm :: "[i,i,i]=>i"
"union_fm(x,y,z) ==
Forall(Iff(Member(0,succ(z)),
Or(Member(0,succ(x)),Member(0,succ(y)))))"
@@ -429,7 +427,7 @@
subsubsection{*Set ``Cons,'' Internalized*}
-constdefs cons_fm :: "[i,i,i]=>i"
+definition cons_fm :: "[i,i,i]=>i"
"cons_fm(x,y,z) ==
Exists(And(upair_fm(succ(x),succ(x),0),
union_fm(0,succ(y),succ(z))))"
@@ -461,7 +459,7 @@
subsubsection{*Successor Function, Internalized*}
-constdefs succ_fm :: "[i,i]=>i"
+definition succ_fm :: "[i,i]=>i"
"succ_fm(x,y) == cons_fm(x,x,y)"
lemma succ_type [TC]:
@@ -491,7 +489,7 @@
subsubsection{*The Number 1, Internalized*}
(* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *)
-constdefs number1_fm :: "i=>i"
+definition number1_fm :: "i=>i"
"number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"
lemma number1_type [TC]:
@@ -520,7 +518,7 @@
subsubsection{*Big Union, Internalized*}
(* "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
-constdefs big_union_fm :: "[i,i]=>i"
+definition big_union_fm :: "[i,i]=>i"
"big_union_fm(A,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"
@@ -600,7 +598,7 @@
subsubsection{*Membership Relation, Internalized*}
-constdefs Memrel_fm :: "[i,i]=>i"
+definition Memrel_fm :: "[i,i]=>i"
"Memrel_fm(A,r) ==
Forall(Iff(Member(0,succ(r)),
Exists(And(Member(0,succ(succ(A))),
@@ -633,7 +631,7 @@
subsubsection{*Predecessor Set, Internalized*}
-constdefs pred_set_fm :: "[i,i,i,i]=>i"
+definition pred_set_fm :: "[i,i,i,i]=>i"
"pred_set_fm(A,x,r,B) ==
Forall(Iff(Member(0,succ(B)),
Exists(And(Member(0,succ(succ(r))),
@@ -671,7 +669,7 @@
(* "is_domain(M,r,z) ==
\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
-constdefs domain_fm :: "[i,i]=>i"
+definition domain_fm :: "[i,i]=>i"
"domain_fm(r,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(r))),
@@ -705,7 +703,7 @@
(* "is_range(M,r,z) ==
\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
-constdefs range_fm :: "[i,i]=>i"
+definition range_fm :: "[i,i]=>i"
"range_fm(r,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(r))),
@@ -740,7 +738,7 @@
(* "is_field(M,r,z) ==
\<exists>dr[M]. is_domain(M,r,dr) &
(\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *)
-constdefs field_fm :: "[i,i]=>i"
+definition field_fm :: "[i,i]=>i"
"field_fm(r,z) ==
Exists(And(domain_fm(succ(r),0),
Exists(And(range_fm(succ(succ(r)),0),
@@ -775,7 +773,7 @@
(* "image(M,r,A,z) ==
\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)
-constdefs image_fm :: "[i,i,i]=>i"
+definition image_fm :: "[i,i,i]=>i"
"image_fm(r,A,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(r))),
@@ -810,7 +808,7 @@
(* "pre_image(M,r,A,z) ==
\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *)
-constdefs pre_image_fm :: "[i,i,i]=>i"
+definition pre_image_fm :: "[i,i,i]=>i"
"pre_image_fm(r,A,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(r))),
@@ -846,7 +844,7 @@
(* "fun_apply(M,f,x,y) ==
(\<exists>xs[M]. \<exists>fxs[M].
upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
-constdefs fun_apply_fm :: "[i,i,i]=>i"
+definition fun_apply_fm :: "[i,i,i]=>i"
"fun_apply_fm(f,x,y) ==
Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
And(image_fm(succ(succ(f)), 1, 0),
@@ -881,7 +879,7 @@
(* "is_relation(M,r) ==
(\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)
-constdefs relation_fm :: "i=>i"
+definition relation_fm :: "i=>i"
"relation_fm(r) ==
Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))"
@@ -913,7 +911,7 @@
(* "is_function(M,r) ==
\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'" *)
-constdefs function_fm :: "i=>i"
+definition function_fm :: "i=>i"
"function_fm(r) ==
Forall(Forall(Forall(Forall(Forall(
Implies(pair_fm(4,3,1),
@@ -950,7 +948,7 @@
is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
(\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))" *)
-constdefs typed_function_fm :: "[i,i,i]=>i"
+definition typed_function_fm :: "[i,i,i]=>i"
"typed_function_fm(A,B,r) ==
And(function_fm(r),
And(relation_fm(r),
@@ -1009,7 +1007,7 @@
(\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
xy \<in> s & yz \<in> r)" *)
-constdefs composition_fm :: "[i,i,i]=>i"
+definition composition_fm :: "[i,i,i]=>i"
"composition_fm(r,s,t) ==
Forall(Iff(Member(0,succ(t)),
Exists(Exists(Exists(Exists(Exists(
@@ -1048,7 +1046,7 @@
typed_function(M,A,B,f) &
(\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')" *)
-constdefs injection_fm :: "[i,i,i]=>i"
+definition injection_fm :: "[i,i,i]=>i"
"injection_fm(A,B,f) ==
And(typed_function_fm(A,B,f),
Forall(Forall(Forall(Forall(Forall(
@@ -1088,7 +1086,7 @@
"surjection(M,A,B,f) ==
typed_function(M,A,B,f) &
(\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *)
-constdefs surjection_fm :: "[i,i,i]=>i"
+definition surjection_fm :: "[i,i,i]=>i"
"surjection_fm(A,B,f) ==
And(typed_function_fm(A,B,f),
Forall(Implies(Member(0,succ(B)),
@@ -1124,7 +1122,7 @@
(* bijection :: "[i=>o,i,i,i] => o"
"bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)
-constdefs bijection_fm :: "[i,i,i]=>i"
+definition bijection_fm :: "[i,i,i]=>i"
"bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))"
lemma bijection_type [TC]:
@@ -1156,7 +1154,7 @@
(* "restriction(M,r,A,z) ==
\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *)
-constdefs restriction_fm :: "[i,i,i]=>i"
+definition restriction_fm :: "[i,i,i]=>i"
"restriction_fm(r,A,z) ==
Forall(Iff(Member(0,succ(z)),
And(Member(0,succ(r)),
@@ -1197,7 +1195,7 @@
pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
*)
-constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i"
+definition order_isomorphism_fm :: "[i,i,i,i,i]=>i"
"order_isomorphism_fm(A,r,B,s,f) ==
And(bijection_fm(A,B,f),
Forall(Implies(Member(0,succ(A)),
@@ -1244,7 +1242,7 @@
ordinal(M,a) & ~ empty(M,a) &
(\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))" *)
-constdefs limit_ordinal_fm :: "i=>i"
+definition limit_ordinal_fm :: "i=>i"
"limit_ordinal_fm(x) ==
And(ordinal_fm(x),
And(Neg(empty_fm(x)),
@@ -1280,7 +1278,7 @@
(* "finite_ordinal(M,a) ==
ordinal(M,a) & ~ limit_ordinal(M,a) &
(\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))" *)
-constdefs finite_ordinal_fm :: "i=>i"
+definition finite_ordinal_fm :: "i=>i"
"finite_ordinal_fm(x) ==
And(ordinal_fm(x),
And(Neg(limit_ordinal_fm(x)),
@@ -1313,7 +1311,7 @@
subsubsection{*Omega: The Set of Natural Numbers*}
(* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
-constdefs omega_fm :: "i=>i"
+definition omega_fm :: "i=>i"
"omega_fm(x) ==
And(limit_ordinal_fm(x),
Forall(Implies(Member(0,succ(x)),