3 header{*Theory Main: Everything Except AC*}
5 theory Main = List + IntDiv + CardinalArith:
7 (*The theory of "iterates" logically belongs to Nat, but can't go there because
8 primrec isn't available into after Datatype. The only theories defined
9 after Datatype are List and the Integ theories.*)
10 subsection{* Iteration of the function @{term F} *}
12 consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60)
16 "F^(succ(n)) (x) = F(F^n (x))"
19 iterates_omega :: "[i=>i,i] => i"
20 "iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)"
23 iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60)
25 iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60)
28 "[| n\<in>nat; F(x) = x |] ==> F^n (x) = x"
29 by (induct n rule: nat_induct, simp_all)
31 lemma iterates_type [TC]:
32 "[| n:nat; a: A; !!x. x:A ==> F(x) : A |]
34 by (induct n rule: nat_induct, simp_all)
36 lemma iterates_omega_triv:
37 "F(x) = x ==> F^\<omega> (x) = x"
38 by (simp add: iterates_omega_def iterates_triv)
40 lemma Ord_iterates [simp]:
41 "[| n\<in>nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |]
43 by (induct n rule: nat_induct, simp_all)
45 lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
46 by (induct_tac n, simp_all)
49 subsection{* Transfinite Recursion *}
51 text{*Transfinite recursion for definitions based on the
52 three cases of ordinals*}
55 transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i"
56 "transrec3(k, a, b, c) ==
57 transrec(k, \<lambda>x r.
59 else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
60 else b(Arith.pred(x), r ` Arith.pred(x)))"
62 lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
63 by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
65 lemma transrec3_succ [simp]:
66 "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
67 by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
69 lemma transrec3_Limit:
71 transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
72 by (rule transrec3_def [THEN def_transrec, THEN trans], force)
75 subsection{* Remaining Declarations *}
77 (* belongs to theory IntDiv *)
78 lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
79 and negDivAlg_induct = negDivAlg_induct [consumes 2]