src/ZF/Main_ZF.thy
 author wenzelm Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) changeset 58957 c9e744ea8a38 parent 58871 c399ae4b836f child 59647 c6f413b660cf permissions -rw-r--r--
proper context for match_tac etc.;
```     1 section{*Theory Main: Everything Except AC*}
```
```     2
```
```     3 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
```
```     4
```
```     5 (*The theory of "iterates" logically belongs to Nat, but can't go there because
```
```     6   primrec isn't available into after Datatype.*)
```
```     7
```
```     8 subsection{* Iteration of the function @{term F} *}
```
```     9
```
```    10 consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
```
```    11
```
```    12 primrec
```
```    13     "F^0 (x) = x"
```
```    14     "F^(succ(n)) (x) = F(F^n (x))"
```
```    15
```
```    16 definition
```
```    17   iterates_omega :: "[i=>i,i] => i"  where
```
```    18     "iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)"
```
```    19
```
```    20 notation (xsymbols)
```
```    21   iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)
```
```    22 notation (HTML output)
```
```    23   iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)
```
```    24
```
```    25 lemma iterates_triv:
```
```    26      "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"
```
```    27 by (induct n rule: nat_induct, simp_all)
```
```    28
```
```    29 lemma iterates_type [TC]:
```
```    30      "[| n \<in> nat;  a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |]
```
```    31       ==> F^n (a) \<in> A"
```
```    32 by (induct n rule: nat_induct, simp_all)
```
```    33
```
```    34 lemma iterates_omega_triv:
```
```    35     "F(x) = x ==> F^\<omega> (x) = x"
```
```    36 by (simp add: iterates_omega_def iterates_triv)
```
```    37
```
```    38 lemma Ord_iterates [simp]:
```
```    39      "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |]
```
```    40       ==> Ord(F^n (x))"
```
```    41 by (induct n rule: nat_induct, simp_all)
```
```    42
```
```    43 lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
```
```    44 by (induct_tac n, simp_all)
```
```    45
```
```    46
```
```    47 subsection{* Transfinite Recursion *}
```
```    48
```
```    49 text{*Transfinite recursion for definitions based on the
```
```    50     three cases of ordinals*}
```
```    51
```
```    52 definition
```
```    53   transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
```
```    54     "transrec3(k, a, b, c) ==
```
```    55        transrec(k, \<lambda>x r.
```
```    56          if x=0 then a
```
```    57          else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
```
```    58          else b(Arith.pred(x), r ` Arith.pred(x)))"
```
```    59
```
```    60 lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
```
```    61 by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
```
```    62
```
```    63 lemma transrec3_succ [simp]:
```
```    64      "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
```
```    65 by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
```
```    66
```
```    67 lemma transrec3_Limit:
```
```    68      "Limit(i) ==>
```
```    69       transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
```
```    70 by (rule transrec3_def [THEN def_transrec, THEN trans], force)
```
```    71
```
```    72
```
```    73 declaration {* fn _ =>
```
```    74   Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
```
```    75 *}
```
```    76
```
```    77 end
```