src/ZF/Main_ZF.thy
changeset 26056 6a0801279f4c
child 26339 7825c83c9eff
equal deleted 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