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
```