src/ZF/Constructible/WF_absolute.thy
changeset 21404 eb85850d3eb7
parent 21233 5a5c8ea5f66a
child 32960 69916a850301
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  subsection{*Transitive closure without fixedpoints*}
     1.5  
     1.6  definition
     1.7 -  rtrancl_alt :: "[i,i]=>i"
     1.8 +  rtrancl_alt :: "[i,i]=>i" where
     1.9      "rtrancl_alt(A,r) ==
    1.10         {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
    1.11                   (\<exists>x y. p = <x,y> &  f`0 = x & f`n = y) &
    1.12 @@ -60,8 +60,7 @@
    1.13  
    1.14  
    1.15  definition
    1.16 -
    1.17 -  rtran_closure_mem :: "[i=>o,i,i,i] => o"
    1.18 +  rtran_closure_mem :: "[i=>o,i,i,i] => o" where
    1.19      --{*The property of belonging to @{text "rtran_closure(r)"}*}
    1.20      "rtran_closure_mem(M,A,r,p) ==
    1.21  	      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M]. 
    1.22 @@ -74,12 +73,14 @@
    1.23  		      fun_apply(M,f,j,fj) & successor(M,j,sj) &
    1.24  		      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"
    1.25  
    1.26 -  rtran_closure :: "[i=>o,i,i] => o"
    1.27 +definition
    1.28 +  rtran_closure :: "[i=>o,i,i] => o" where
    1.29      "rtran_closure(M,r,s) == 
    1.30          \<forall>A[M]. is_field(M,r,A) -->
    1.31   	 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))"
    1.32  
    1.33 -  tran_closure :: "[i=>o,i,i] => o"
    1.34 +definition
    1.35 +  tran_closure :: "[i=>o,i,i] => o" where
    1.36      "tran_closure(M,r,t) ==
    1.37           \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
    1.38