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