# Theory Brouwer

Up to index of Isabelle/ZF/Induct

theory Brouwer
imports Main_ZFC
begin

    (*  Title:      ZF/Induct/Brouwer.thy
        ID:         $Id: Brouwer.thy,v 1.6 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header {* Infinite branching datatype definitions *}

    theory Brouwer imports Main_ZFC begin

    subsection {* The Brouwer ordinals *}

    consts
      brouwer :: i

    datatype ⊆ "Vfrom(0, csucc(nat))"
        "brouwer" = Zero | Suc ("b ∈ brouwer") | Lim ("h ∈ nat -> brouwer")
      monos Pi_mono
      type_intros inf_datatype_intros

    lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)"
      by (fast intro!: brouwer.intros [unfolded brouwer.con_defs]
        elim: brouwer.cases [unfolded brouwer.con_defs])

    lemma brouwer_induct2:
      "[| b ∈ brouwer;
          P(Zero);
          !!b. [| b ∈ brouwer;  P(b) |] ==> P(Suc(b));
          !!h. [| h ∈ nat -> brouwer;  ∀i ∈ nat. P(h`i)
               |] ==> P(Lim(h))
       |] ==> P(b)"
      -- {* A nicer induction rule than the standard one. *}
    proof -
      case rule_context
      assume "b ∈ brouwer"
      thus ?thesis
        apply induct
        apply (assumption | rule rule_context)+
         apply (fast elim: fun_weaken_type)
        apply (fast dest: apply_type)
        done
    qed

    subsection {* The Martin-Löf wellordering type *}

    consts
      Well :: "[i, i => i] => i"

    datatype ⊆ "Vfrom(A ∪ (\<Union>x ∈ A. B(x)), csucc(nat ∪ |\<Union>x ∈ A. B(x)|))"
        -- {* The union with @{text nat} ensures that the cardinal is infinite. *}
      "Well(A, B)" = Sup ("a ∈ A", "f ∈ B(a) -> Well(A, B)")
      monos Pi_mono
      type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros

    lemma Well_unfold: "Well(A, B) = (Σ x ∈ A. B(x) -> Well(A, B))"
      by (fast intro!: Well.intros [unfolded Well.con_defs]
        elim: Well.cases [unfolded Well.con_defs])

    lemma Well_induct2:
      "[| w ∈ Well(A, B);
          !!a f. [| a ∈ A;  f ∈ B(a) -> Well(A,B);  ∀y ∈ B(a). P(f`y)
               |] ==> P(Sup(a,f))
       |] ==> P(w)"
      -- {* A nicer induction rule than the standard one. *}
    proof -
      case rule_context
      assume "w ∈ Well(A, B)"
      thus ?thesis
        apply induct
        apply (assumption | rule rule_context)+
         apply (fast elim: fun_weaken_type)
        apply (fast dest: apply_type)
        done
    qed

    lemma Well_bool_unfold: "Well(bool, λx. x) = 1 + (1 -> Well(bool, λx. x))"
      -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
      -- {* for @{text Well} to prove this. *}
      apply (rule Well_unfold [THEN trans])
      apply (simp add: Sigma_bool Pi_empty1 succ_def)
      done

    end

### The Brouwer ordinals

lemma brouwer_unfold:

      brouwer = {0} + brouwer + (nat -> brouwer)

lemma brouwer_induct2:

      [| b ∈ brouwer; P(Zero); !!b. [| b ∈ brouwer; P(b) |] ==> P(Suc(b));
         !!h. [| h ∈ nat -> brouwer; ∀i∈nat. P(h ` i) |] ==> P(Lim(h)) |]
      ==> P(b)

### The Martin-Löf wellordering type

lemma Well_unfold:

      Well(A, B) = (Σx∈A. B(x) -> Well(A, B))

lemma Well_induct2:

      [| w ∈ Well(A, B);
         !!a f. [| a ∈ A; f ∈ B(a) -> Well(A, B); ∀y∈B(a). P(f ` y) |]
                ==> P(Sup(a, f)) |]
      ==> P(w)

lemma Well_bool_unfold:

      Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))