src/ZF/Constructible/DPow_absolute.thy

--- a/src/ZF/Constructible/DPow_absolute.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -23,7 +23,8 @@
              successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
 *)
 
-definition formula_rec_fm :: "[i, i, i]=>i"
+definition
+  formula_rec_fm :: "[i, i, i]=>i" where
  "formula_rec_fm(mh,p,z) == 
     Exists(Exists(Exists(
       And(finite_ordinal_fm(2),
@@ -80,7 +81,8 @@
 subsubsection{*The Operator @{term is_satisfies}*}
 
 (* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *)
-definition satisfies_fm :: "[i,i,i]=>i"
+definition
+  satisfies_fm :: "[i,i,i]=>i" where
     "satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
 
 lemma is_satisfies_type [TC]:
@@ -120,7 +122,7 @@
 text{*Relativize the use of @{term sats} within @{term DPow'}
 (the comprehension).*}
 definition
-  is_DPow_sats :: "[i=>o,i,i,i,i] => o"
+  is_DPow_sats :: "[i=>o,i,i,i,i] => o" where
    "is_DPow_sats(M,A,env,p,x) ==
       \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
              is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> 
@@ -148,8 +150,9 @@
              is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> 
              fun_apply(M, sp, e, n1) --> number1(M, n1) *)
 
-definition DPow_sats_fm :: "[i,i,i,i]=>i"
- "DPow_sats_fm(A,env,p,x) ==
+definition
+  DPow_sats_fm :: "[i,i,i,i]=>i" where
+  "DPow_sats_fm(A,env,p,x) ==
    Forall(Forall(Forall(
      Implies(satisfies_fm(A#+3,p#+3,0), 
        Implies(Cons_fm(x#+3,env#+3,1), 
@@ -219,7 +222,7 @@
 
 text{*Relativization of the Operator @{term DPow'}*}
 definition 
-  is_DPow' :: "[i=>o,i,i] => o"
+  is_DPow' :: "[i=>o,i,i] => o" where
     "is_DPow'(M,A,Z) == 
        \<forall>X[M]. X \<in> Z <-> 
          subset(M,X,A) & 
@@ -310,7 +313,8 @@
 (* is_Collect :: "[i=>o,i,i=>o,i] => o"
     "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)" *)
 
-definition Collect_fm :: "[i, i, i]=>i"
+definition
+  Collect_fm :: "[i, i, i]=>i" where
  "Collect_fm(A,is_P,z) == 
         Forall(Iff(Member(0,succ(z)),
                    And(Member(0,succ(A)), is_P)))"
@@ -360,8 +364,9 @@
 (*  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
     "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))" *)
 
-definition Replace_fm :: "[i, i, i]=>i"
- "Replace_fm(A,is_P,z) == 
+definition
+  Replace_fm :: "[i, i, i]=>i" where
+  "Replace_fm(A,is_P,z) == 
         Forall(Iff(Member(0,succ(z)),
                    Exists(And(Member(0,A#+2), is_P))))"
 
@@ -413,7 +418,8 @@
            (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
                     is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *)
 
-definition DPow'_fm :: "[i,i]=>i"
+definition
+  DPow'_fm :: "[i,i]=>i" where
     "DPow'_fm(A,Z) == 
       Forall(
        Iff(Member(0,succ(Z)),
@@ -452,7 +458,7 @@
 subsection{*A Locale for Relativizing the Operator @{term Lset}*}
 
 definition
-  transrec_body :: "[i=>o,i,i,i,i] => o"
+  transrec_body :: "[i=>o,i,i,i,i] => o" where
     "transrec_body(M,g,x) ==
       \<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
 
@@ -504,7 +510,7 @@
 text{*Relativization of the Operator @{term Lset}*}
 
 definition
-  is_Lset :: "[i=>o, i, i] => o"
+  is_Lset :: "[i=>o, i, i] => o" where
    --{*We can use the term language below because @{term is_Lset} will
        not have to be internalized: it isn't used in any instance of
        separation.*}
@@ -610,7 +616,7 @@
 
 
 definition
-  constructible :: "[i=>o,i] => o"
+  constructible :: "[i=>o,i] => o" where
     "constructible(M,x) ==
        \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"