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) = (ΣxA. B(x) -> Well(A, B))

lemma Well_induct2:

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

lemma Well_bool_unfold:

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