src/ZF/Main_ZF.thy
author wenzelm
Tue Sep 01 22:32:58 2015 +0200 (2015-09-01)
changeset 61076 bdc1e2f0a86a
parent 60822 4f58f3662e7d
child 61378 3e04c9ca001a
permissions -rw-r--r--
eliminated \<Colon>;
     1 section\<open>Theory Main: Everything Except AC\<close>
     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\<open>Iteration of the function @{term F}\<close>
     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\<open>Transfinite Recursion\<close>
    48 
    49 text\<open>Transfinite recursion for definitions based on the
    50     three cases of ordinals\<close>
    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 \<open>fn _ =>
    74   Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
    75     map mk_eq o Ord_atomize o Variable.gen_all ctxt))
    76 \<close>
    77 
    78 end