# HG changeset patch
# User paulson
# Date 1117643343 -7200
# Node ID a55c796b1f7983aa7c733ed934aebebc621ba055
# Parent  9e2f6c0a779d1377346828acf8992355fb565b35
ordering for the ordinals

diff -r 9e2f6c0a779d -r a55c796b1f79 src/HOL/Induct/Tree.thy
--- 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