--- a/src/HOL/Induct/Tree.thy Wed Jun 01 18:19:59 2005 +0200
+++ b/src/HOL/Induct/Tree.thy Wed Jun 01 18:29:03 2005 +0200
@@ -69,4 +69,42 @@
text{*We could probably instantiate some axiomatic type classes and use
the standard infix operators.*}
+subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*}
+
+text{*To define recdef style functions we need an ordering on the Brouwer
+ ordinals. Start with a predecessor relation and form its transitive
+ closure. *}
+
+constdefs
+ brouwer_pred :: "(brouwer * brouwer) set"
+ "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
+
+ brouwer_order :: "(brouwer * brouwer) set"
+ "brouwer_order == brouwer_pred^+"
+
+lemma wf_brouwer_pred: "wf brouwer_pred"
+ by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
+
+lemma wf_brouwer_order: "wf brouwer_order"
+ by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
+
+lemma [simp]: "(j, Succ j) : brouwer_order"
+ by(auto simp add: brouwer_order_def brouwer_pred_def)
+
+lemma [simp]: "(f n, Lim f) : brouwer_order"
+ by(auto simp add: brouwer_order_def brouwer_pred_def)
+
+text{*Example of a recdef*}
+consts
+ add2 :: "(brouwer*brouwer) => brouwer"
+recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)"
+ "add2 (i, Zero) = i"
+ "add2 (i, (Succ j)) = Succ (add2 (i, j))"
+ "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
+ (hints recdef_wf: wf_brouwer_order)
+
+lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
+by (induct k, auto)
+
+
end