# Theory Main

Up to index of Isabelle/ZF

theory Main
imports List IntDiv CardinalArith
uses [Main.ML]
begin

    (*$Id: Main.thy,v 1.18 2005/06/17 14:15:09 haftmann Exp $*)

    header{*Theory Main: Everything Except AC*}

    theory Main imports List IntDiv CardinalArith begin

    (*The theory of "iterates" logically belongs to Nat, but can't go there because
      primrec isn't available into after Datatype.  The only theories defined
      after Datatype are List and the Integ theories.*)
    subsection{* Iteration of the function @{term F} *}

    consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)

    primrec
        "F^0 (x) = x"
        "F^(succ(n)) (x) = F(F^n (x))"

    constdefs
      iterates_omega :: "[i=>i,i] => i"
        "iterates_omega(F,x) == \<Union>n∈nat. F^n (x)"

    syntax (xsymbols)
      iterates_omega :: "[i=>i,i] => i"   ("(_^ω '(_'))" [60,1000] 60)
    syntax (HTML output)
      iterates_omega :: "[i=>i,i] => i"   ("(_^ω '(_'))" [60,1000] 60)

    lemma iterates_triv:
         "[| n∈nat;  F(x) = x |] ==> F^n (x) = x"
    by (induct n rule: nat_induct, simp_all)

    lemma iterates_type [TC]:
         "[| n:nat;  a: A; !!x. x:A ==> F(x) : A |]
          ==> F^n (a) : A"
    by (induct n rule: nat_induct, simp_all)

    lemma iterates_omega_triv:
        "F(x) = x ==> F^ω (x) = x"
    by (simp add: iterates_omega_def iterates_triv)

    lemma Ord_iterates [simp]:
         "[| n∈nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |]
          ==> Ord(F^n (x))"
    by (induct n rule: nat_induct, simp_all)

    lemma iterates_commute: "n ∈ nat ==> F(F^n (x)) = F^n (F(x))"
    by (induct_tac n, simp_all)

    subsection{* Transfinite Recursion *}

    text{*Transfinite recursion for definitions based on the
        three cases of ordinals*}

    constdefs
      transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i"
        "transrec3(k, a, b, c) ==
           transrec(k, λx r.
             if x=0 then a
             else if Limit(x) then c(x, λy∈x. r`y)
             else b(Arith.pred(x), r ` Arith.pred(x)))"

    lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
    by (rule transrec3_def [THEN def_transrec, THEN trans], simp)

    lemma transrec3_succ [simp]:
         "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
    by (rule transrec3_def [THEN def_transrec, THEN trans], simp)

    lemma transrec3_Limit:
         "Limit(i) ==>
          transrec3(i,a,b,c) = c(i, λj∈i. transrec3(j,a,b,c))"
    by (rule transrec3_def [THEN def_transrec, THEN trans], force)

    subsection{* Remaining Declarations *}

    (* belongs to theory IntDiv *)
    lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
      and negDivAlg_induct = negDivAlg_induct [consumes 2]

    end

### Iteration of the function @{term F}

lemma iterates_triv:

      [| n ∈ nat; F(x) = x |] ==> F^n (x) = x

lemma iterates_type:

      [| n ∈ nat; a ∈ A; !!x. x ∈ A ==> F(x) ∈ A |] ==> F^n (a) ∈ A

lemma iterates_omega_triv:

      F(x) = x ==> F^ω (x) = x

lemma Ord_iterates:

      [| n ∈ nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] ==> Ord(F^n (x))

lemma iterates_commute:

      n ∈ nat ==> F(F^n (x)) = F^n (F(x))

### Transfinite Recursion

lemma transrec3_0:

      transrec3(0, a, b, c) = a

lemma transrec3_succ:

      transrec3(succ(i), a, b, c) = b(i, transrec3(i, a, b, c))

lemma transrec3_Limit:

      Limit(i) ==> transrec3(i, a, b, c) = c(i, λj∈i. transrec3(j, a, b, c))

### Remaining Declarations

lemmas posDivAlg_induct:

      [| u ∈ int; v ∈ int;
         !!a b. [| a ∈ int; b ∈ int; ¬ (a $< b ∨ b $≤ #0) --> P(a, #2 $× b) |]
                ==> P(a, b) |]
      ==> P(u, v)

and negDivAlg_induct:

      [| u ∈ int; v ∈ int;
         !!a b. [| a ∈ int; b ∈ int; ¬ (#0 $≤ a $+ b ∨ b $≤ #0) --> P(a, #2 $× b) |]
                ==> P(a, b) |]
      ==> P(u, v)

lemmas posDivAlg_induct:

      [| u ∈ int; v ∈ int;
         !!a b. [| a ∈ int; b ∈ int; ¬ (a $< b ∨ b $≤ #0) --> P(a, #2 $× b) |]
                ==> P(a, b) |]
      ==> P(u, v)

and negDivAlg_induct:

      [| u ∈ int; v ∈ int;
         !!a b. [| a ∈ int; b ∈ int; ¬ (#0 $≤ a $+ b ∨ b $≤ #0) --> P(a, #2 $× b) |]
                ==> P(a, b) |]
      ==> P(u, v)