src/ZF/Main.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 13694 be3e2fa01b0f
child 16417 9bc16273c2d4
permissions -rw-r--r--
use more symbols in HTML output
paulson@13356
     1
(*$Id$*)
wenzelm@12426
     2
paulson@13356
     3
header{*Theory Main: Everything Except AC*}
wenzelm@12426
     4
paulson@13356
     5
theory Main = List + IntDiv + CardinalArith:
paulson@13162
     6
paulson@13203
     7
(*The theory of "iterates" logically belongs to Nat, but can't go there because
paulson@13203
     8
  primrec isn't available into after Datatype.  The only theories defined
paulson@13203
     9
  after Datatype are List and the Integ theories.*)
paulson@13162
    10
subsection{* Iteration of the function @{term F} *}
paulson@13162
    11
paulson@13162
    12
consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
paulson@13162
    13
paulson@13162
    14
primrec
paulson@13162
    15
    "F^0 (x) = x"
paulson@13162
    16
    "F^(succ(n)) (x) = F(F^n (x))"
paulson@13162
    17
paulson@13162
    18
constdefs
paulson@13162
    19
  iterates_omega :: "[i=>i,i] => i"
paulson@13162
    20
    "iterates_omega(F,x) == \<Union>n\<in>nat. F^n (x)"
paulson@13162
    21
paulson@13162
    22
syntax (xsymbols)
paulson@13162
    23
  iterates_omega :: "[i=>i,i] => i"   ("(_^\<omega> '(_'))" [60,1000] 60)
kleing@14565
    24
syntax (HTML output)
kleing@14565
    25
  iterates_omega :: "[i=>i,i] => i"   ("(_^\<omega> '(_'))" [60,1000] 60)
paulson@13162
    26
paulson@13162
    27
lemma iterates_triv:
paulson@13162
    28
     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"  
paulson@13162
    29
by (induct n rule: nat_induct, simp_all)
paulson@13162
    30
paulson@13162
    31
lemma iterates_type [TC]:
paulson@13162
    32
     "[| n:nat;  a: A; !!x. x:A ==> F(x) : A |] 
paulson@13162
    33
      ==> F^n (a) : A"  
paulson@13162
    34
by (induct n rule: nat_induct, simp_all)
paulson@13162
    35
paulson@13162
    36
lemma iterates_omega_triv:
paulson@13162
    37
    "F(x) = x ==> F^\<omega> (x) = x" 
paulson@13162
    38
by (simp add: iterates_omega_def iterates_triv) 
paulson@13162
    39
paulson@13162
    40
lemma Ord_iterates [simp]:
paulson@13162
    41
     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |] 
paulson@13162
    42
      ==> Ord(F^n (x))"  
paulson@13162
    43
by (induct n rule: nat_induct, simp_all)
paulson@13162
    44
paulson@13396
    45
lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
paulson@13396
    46
by (induct_tac n, simp_all)
paulson@13396
    47
paulson@13162
    48
paulson@13694
    49
subsection{* Transfinite Recursion *}
paulson@13694
    50
paulson@13694
    51
text{*Transfinite recursion for definitions based on the 
paulson@13694
    52
    three cases of ordinals*}
paulson@13694
    53
paulson@13694
    54
constdefs
paulson@13694
    55
  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i"
paulson@13694
    56
    "transrec3(k, a, b, c) ==                     
paulson@13694
    57
       transrec(k, \<lambda>x r.
paulson@13694
    58
         if x=0 then a
paulson@13694
    59
         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
paulson@13694
    60
         else b(Arith.pred(x), r ` Arith.pred(x)))"
paulson@13694
    61
paulson@13694
    62
lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
paulson@13694
    63
by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
paulson@13694
    64
paulson@13694
    65
lemma transrec3_succ [simp]:
paulson@13694
    66
     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
paulson@13694
    67
by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
paulson@13694
    68
paulson@13694
    69
lemma transrec3_Limit:
paulson@13694
    70
     "Limit(i) ==> 
paulson@13694
    71
      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
paulson@13694
    72
by (rule transrec3_def [THEN def_transrec, THEN trans], force)
paulson@13694
    73
paulson@13694
    74
paulson@13694
    75
subsection{* Remaining Declarations *}
paulson@13694
    76
wenzelm@12426
    77
(* belongs to theory IntDiv *)
wenzelm@12426
    78
lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
wenzelm@12426
    79
  and negDivAlg_induct = negDivAlg_induct [consumes 2]
wenzelm@12426
    80
paulson@12620
    81
wenzelm@12426
    82
end