# HG changeset patch
# User paulson
# Date 1036507878 -3600
# Node ID be3e2fa01b0fc13571ce5a61ba45bc612ba14df0
# Parent  77052bb8aed33a6384a80e9bd7582793403780f6
new operator transrec3

diff -r 77052bb8aed3 -r be3e2fa01b0f src/ZF/Main.thy
--- a/src/ZF/Main.thy	Mon Nov 04 14:17:00 2002 +0100
+++ b/src/ZF/Main.thy	Tue Nov 05 15:51:18 2002 +0100
@@ -44,6 +44,34 @@
 by (induct_tac n, simp_all)
 
 
+subsection{* Transfinite Recursion *}
+
+text{*Transfinite recursion for definitions based on the 
+    three cases of ordinals*}
+
+constdefs
+  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i"
+    "transrec3(k, a, b, c) ==                     
+       transrec(k, \<lambda>x r.
+         if x=0 then a
+         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
+         else b(Arith.pred(x), r ` Arith.pred(x)))"
+
+lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
+by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
+
+lemma transrec3_succ [simp]:
+     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
+by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
+
+lemma transrec3_Limit:
+     "Limit(i) ==> 
+      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
+by (rule transrec3_def [THEN def_transrec, THEN trans], force)
+
+
+subsection{* Remaining Declarations *}
+
 (* belongs to theory IntDiv *)
 lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
   and negDivAlg_induct = negDivAlg_induct [consumes 2]