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