src/ZF/Main.thy
author nipkow
Sun, 05 Jan 2003 21:03:14 +0100
changeset 13771 6cd59cc885a1
parent 13694 be3e2fa01b0f
child 14565 c6dc17aab88a
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13203
diff changeset
     1
(*$Id$*)
12426
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
     2
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13203
diff changeset
     3
header{*Theory Main: Everything Except AC*}
12426
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
     4
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13203
diff changeset
     5
theory Main = List + IntDiv + CardinalArith:
13162
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
     6
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13162
diff changeset
     7
(*The theory of "iterates" logically belongs to Nat, but can't go there because
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13162
diff changeset
     8
  primrec isn't available into after Datatype.  The only theories defined
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13162
diff changeset
     9
  after Datatype are List and the Integ theories.*)
13162
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    10
subsection{* Iteration of the function @{term F} *}
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    11
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    12
consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    13
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    14
primrec
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    15
    "F^0 (x) = x"
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    16
    "F^(succ(n)) (x) = F(F^n (x))"
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    17
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    18
constdefs
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    19
  iterates_omega :: "[i=>i,i] => i"
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    20
    "iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)"
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    21
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    22
syntax (xsymbols)
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    23
  iterates_omega :: "[i=>i,i] => i"   ("(_^\<omega> '(_'))" [60,1000] 60)
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    24
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    25
lemma iterates_triv:
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    26
     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"  
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    27
by (induct n rule: nat_induct, simp_all)
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    28
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    29
lemma iterates_type [TC]:
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    30
     "[| n:nat;  a: A; !!x. x:A ==> F(x) : A |] 
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    31
      ==> F^n (a) : A"  
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    32
by (induct n rule: nat_induct, simp_all)
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    33
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    34
lemma iterates_omega_triv:
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    35
    "F(x) = x ==> F^\<omega> (x) = x" 
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    36
by (simp add: iterates_omega_def iterates_triv) 
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    37
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    38
lemma Ord_iterates [simp]:
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    39
     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |] 
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    40
      ==> Ord(F^n (x))"  
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    41
by (induct n rule: nat_induct, simp_all)
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    42
13396
11219ca224ab A couple of new theorems for Constructible
paulson
parents: 13356
diff changeset
    43
lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
11219ca224ab A couple of new theorems for Constructible
paulson
parents: 13356
diff changeset
    44
by (induct_tac n, simp_all)
11219ca224ab A couple of new theorems for Constructible
paulson
parents: 13356
diff changeset
    45
13162
660a71e712af New theorems from Constructible, and moving some Isar material from Main
paulson
parents: 12820
diff changeset
    46
13694
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    47
subsection{* Transfinite Recursion *}
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    48
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    49
text{*Transfinite recursion for definitions based on the 
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    50
    three cases of ordinals*}
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    51
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    52
constdefs
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    53
  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i"
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    54
    "transrec3(k, a, b, c) ==                     
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    55
       transrec(k, \<lambda>x r.
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    56
         if x=0 then a
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    57
         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    58
         else b(Arith.pred(x), r ` Arith.pred(x)))"
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    59
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    60
lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    61
by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    62
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    63
lemma transrec3_succ [simp]:
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    64
     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    65
by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    66
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    67
lemma transrec3_Limit:
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    68
     "Limit(i) ==> 
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    69
      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    70
by (rule transrec3_def [THEN def_transrec, THEN trans], force)
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    71
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    72
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    73
subsection{* Remaining Declarations *}
be3e2fa01b0f new operator transrec3
paulson
parents: 13396
diff changeset
    74
12426
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
    75
(* belongs to theory IntDiv *)
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
    76
lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
    77
  and negDivAlg_induct = negDivAlg_induct [consumes 2]
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
    78
12620
4e6626725e21 Some new theorems for ordinals
paulson
parents: 12552
diff changeset
    79
12426
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
    80
end