src/ZF/Main_ZF.thy
 changeset 26056 6a0801279f4c child 26339 7825c83c9eff
equal inserted replaced
26055:a7a537e0413a 26056:6a0801279f4c
`       `
`     1 (*\$Id\$*)`
`       `
`     2 `
`       `
`     3 header{*Theory Main: Everything Except AC*}`
`       `
`     4 `
`       `
`     5 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin`
`       `
`     6 `
`       `
`     7 (*The theory of "iterates" logically belongs to Nat, but can't go there because`
`       `
`     8   primrec isn't available into after Datatype.*)`
`       `
`     9 `
`       `
`    10 subsection{* Iteration of the function @{term F} *}`
`       `
`    11 `
`       `
`    12 consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)`
`       `
`    13 `
`       `
`    14 primrec`
`       `
`    15     "F^0 (x) = x"`
`       `
`    16     "F^(succ(n)) (x) = F(F^n (x))"`
`       `
`    17 `
`       `
`    18 definition`
`       `
`    19   iterates_omega :: "[i=>i,i] => i"  where`
`       `
`    20     "iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)"`
`       `
`    21 `
`       `
`    22 notation (xsymbols)`
`       `
`    23   iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)`
`       `
`    24 notation (HTML output)`
`       `
`    25   iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)`
`       `
`    26 `
`       `
`    27 lemma iterates_triv:`
`       `
`    28      "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"  `
`       `
`    29 by (induct n rule: nat_induct, simp_all)`
`       `
`    30 `
`       `
`    31 lemma iterates_type [TC]:`
`       `
`    32      "[| n:nat;  a: A; !!x. x:A ==> F(x) : A |] `
`       `
`    33       ==> F^n (a) : A"  `
`       `
`    34 by (induct n rule: nat_induct, simp_all)`
`       `
`    35 `
`       `
`    36 lemma iterates_omega_triv:`
`       `
`    37     "F(x) = x ==> F^\<omega> (x) = x" `
`       `
`    38 by (simp add: iterates_omega_def iterates_triv) `
`       `
`    39 `
`       `
`    40 lemma Ord_iterates [simp]:`
`       `
`    41      "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |] `
`       `
`    42       ==> Ord(F^n (x))"  `
`       `
`    43 by (induct n rule: nat_induct, simp_all)`
`       `
`    44 `
`       `
`    45 lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"`
`       `
`    46 by (induct_tac n, simp_all)`
`       `
`    47 `
`       `
`    48 `
`       `
`    49 subsection{* Transfinite Recursion *}`
`       `
`    50 `
`       `
`    51 text{*Transfinite recursion for definitions based on the `
`       `
`    52     three cases of ordinals*}`
`       `
`    53 `
`       `
`    54 definition`
`       `
`    55   transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where`
`       `
`    56     "transrec3(k, a, b, c) ==                     `
`       `
`    57        transrec(k, \<lambda>x r.`
`       `
`    58          if x=0 then a`
`       `
`    59          else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)`
`       `
`    60          else b(Arith.pred(x), r ` Arith.pred(x)))"`
`       `
`    61 `
`       `
`    62 lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"`
`       `
`    63 by (rule transrec3_def [THEN def_transrec, THEN trans], simp)`
`       `
`    64 `
`       `
`    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)`
`       `
`    68 `
`       `
`    69 lemma transrec3_Limit:`
`       `
`    70      "Limit(i) ==> `
`       `
`    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)`
`       `
`    73 `
`       `
`    74 `
`       `
`    75 ML_setup {*`
`       `
`    76   change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));`
`       `
`    77 *}`
`       `
`    78 `
`       `
`    79 end`