ordering for the ordinals
authorpaulson
Wed Jun 01 18:29:03 2005 +0200 (2005-06-01)
changeset 16174a55c796b1f79
parent 16173 9e2f6c0a779d
child 16175 749e6b68ca84
ordering for the ordinals
src/HOL/Induct/Tree.thy
     1.1 --- a/src/HOL/Induct/Tree.thy	Wed Jun 01 18:19:59 2005 +0200
     1.2 +++ b/src/HOL/Induct/Tree.thy	Wed Jun 01 18:29:03 2005 +0200
     1.3 @@ -69,4 +69,42 @@
     1.4  text{*We could probably instantiate some axiomatic type classes and use
     1.5  the standard infix operators.*}
     1.6  
     1.7 +subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*}
     1.8 +
     1.9 +text{*To define recdef style functions we need an ordering on the Brouwer
    1.10 +  ordinals.  Start with a predecessor relation and form its transitive 
    1.11 +  closure. *} 
    1.12 +
    1.13 +constdefs
    1.14 +  brouwer_pred :: "(brouwer * brouwer) set"
    1.15 +  "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
    1.16 +
    1.17 +  brouwer_order :: "(brouwer * brouwer) set"
    1.18 +  "brouwer_order == brouwer_pred^+"
    1.19 +
    1.20 +lemma wf_brouwer_pred: "wf brouwer_pred"
    1.21 +  by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
    1.22 +
    1.23 +lemma wf_brouwer_order: "wf brouwer_order"
    1.24 +  by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
    1.25 +
    1.26 +lemma [simp]: "(j, Succ j) : brouwer_order"
    1.27 +  by(auto simp add: brouwer_order_def brouwer_pred_def)
    1.28 +
    1.29 +lemma [simp]: "(f n, Lim f) : brouwer_order"
    1.30 +  by(auto simp add: brouwer_order_def brouwer_pred_def)
    1.31 +
    1.32 +text{*Example of a recdef*}
    1.33 +consts
    1.34 +  add2 :: "(brouwer*brouwer) => brouwer"
    1.35 +recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)"
    1.36 +  "add2 (i, Zero) = i"
    1.37 +  "add2 (i, (Succ j)) = Succ (add2 (i, j))"
    1.38 +  "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
    1.39 +  (hints recdef_wf: wf_brouwer_order)
    1.40 +
    1.41 +lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
    1.42 +by (induct k, auto)
    1.43 +
    1.44 +
    1.45  end