--- a/src/ZF/Main.thy Fri May 17 16:48:11 2002 +0200
+++ b/src/ZF/Main.thy Fri May 17 16:54:25 2002 +0200
@@ -15,21 +15,51 @@
and wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
and wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on]
-(* belongs to theory Ordinal *)
-declare Ord_Least [intro,simp,TC]
-lemmas Ord_induct = Ord_induct [consumes 2]
- and Ord_induct_rule = Ord_induct [rule_format, consumes 2]
- and trans_induct = trans_induct [consumes 1]
- and trans_induct_rule = trans_induct [rule_format, consumes 1]
- and trans_induct3 = trans_induct3 [case_names 0 succ limit, consumes 1]
- and trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]
-
(* belongs to theory Nat *)
lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
and complete_induct = complete_induct [case_names less, consumes 1]
and complete_induct_rule = complete_induct [rule_format, case_names less, consumes 1]
and diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
+
+
+subsection{* Iteration of the function @{term F} *}
+
+consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60)
+
+primrec
+ "F^0 (x) = x"
+ "F^(succ(n)) (x) = F(F^n (x))"
+
+constdefs
+ iterates_omega :: "[i=>i,i] => i"
+ "iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)"
+
+syntax (xsymbols)
+ iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60)
+
+lemma iterates_triv:
+ "[| n\<in>nat; F(x) = x |] ==> F^n (x) = x"
+by (induct n rule: nat_induct, simp_all)
+
+lemma iterates_type [TC]:
+ "[| n:nat; a: A; !!x. x:A ==> F(x) : A |]
+ ==> F^n (a) : A"
+by (induct n rule: nat_induct, simp_all)
+
+lemma iterates_omega_triv:
+ "F(x) = x ==> F^\<omega> (x) = x"
+by (simp add: iterates_omega_def iterates_triv)
+
+lemma Ord_iterates [simp]:
+ "[| n\<in>nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |]
+ ==> Ord(F^n (x))"
+by (induct n rule: nat_induct, simp_all)
+
+
+(* belongs to theory Cardinal *)
+declare Ord_Least [intro,simp,TC]
+
(* belongs to theory Epsilon *)
lemmas eclose_induct = eclose_induct [induct set: eclose]
and eclose_induct_down = eclose_induct_down [consumes 1]
@@ -59,7 +89,7 @@
(* belongs to theory CardinalArith *)
-lemma InfCard_square_eqpoll: "InfCard(K) \<Longrightarrow> K \<times> K \<approx> K"
+lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K"
apply (rule well_ord_InfCard_square_eq)
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel])
apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq])