src/ZF/Induct/Brouwer.thy
author nipkow
Sun, 04 Nov 2018 12:07:24 +0100
changeset 69232 2b913054a9cf
parent 65449 c82e63b11b8b
child 76213 e44d86131648
permissions -rw-r--r--
Faster Braun tree functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
     1
(*  Title:      ZF/Induct/Brouwer.thy
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
     3
    Copyright   1994  University of Cambridge
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
     4
*)
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
     5
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
     6
section \<open>Infinite branching datatype definitions\<close>
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
     7
65449
c82e63b11b8b clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents: 61980
diff changeset
     8
theory Brouwer imports ZFC begin
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
     9
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    10
subsection \<open>The Brouwer ordinals\<close>
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    11
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    12
consts
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    13
  brouwer :: i
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    14
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12552
diff changeset
    15
datatype \<subseteq> "Vfrom(0, csucc(nat))"
8b9845807f77 tuned document sources;
wenzelm
parents: 12552
diff changeset
    16
    "brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer")
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    17
  monos Pi_mono
13137
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12610
diff changeset
    18
  type_intros inf_datatype_intros
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    19
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    20
lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)"
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    21
  by (fast intro!: brouwer.intros [unfolded brouwer.con_defs]
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    22
    elim: brouwer.cases [unfolded brouwer.con_defs])
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    23
18372
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    24
lemma brouwer_induct2 [consumes 1, case_names Zero Suc Lim]:
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    25
  assumes b: "b \<in> brouwer"
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    26
    and cases:
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    27
      "P(Zero)"
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    28
      "!!b. [| b \<in> brouwer;  P(b) |] ==> P(Suc(b))"
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    29
      "!!h. [| h \<in> nat -> brouwer;  \<forall>i \<in> nat. P(h`i) |] ==> P(Lim(h))"
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    30
  shows "P(b)"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    31
  \<comment> \<open>A nicer induction rule than the standard one.\<close>
18372
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    32
  using b
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    33
  apply induct
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 18372
diff changeset
    34
    apply (rule cases(1))
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 18372
diff changeset
    35
   apply (erule (1) cases(2))
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 18372
diff changeset
    36
  apply (rule cases(3))
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 18372
diff changeset
    37
   apply (fast elim: fun_weaken_type)
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 18372
diff changeset
    38
  apply (fast dest: apply_type)
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 18372
diff changeset
    39
  done
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    40
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    41
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    42
subsection \<open>The Martin-Löf wellordering type\<close>
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    43
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    44
consts
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    45
  Well :: "[i, i => i] => i"
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    46
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12552
diff changeset
    47
datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    48
    \<comment> \<open>The union with \<open>nat\<close> ensures that the cardinal is infinite.\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12552
diff changeset
    49
  "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    50
  monos Pi_mono
13137
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12610
diff changeset
    51
  type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    52
61980
6b780867d426 clarified syntax;
wenzelm
parents: 61798
diff changeset
    53
lemma Well_unfold: "Well(A, B) = (\<Sum>x \<in> A. B(x) -> Well(A, B))"
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    54
  by (fast intro!: Well.intros [unfolded Well.con_defs]
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    55
    elim: Well.cases [unfolded Well.con_defs])
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    56
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    57
18372
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    58
lemma Well_induct2 [consumes 1, case_names step]:
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    59
  assumes w: "w \<in> Well(A, B)"
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    60
    and step: "!!a f. [| a \<in> A;  f \<in> B(a) -> Well(A,B);  \<forall>y \<in> B(a). P(f`y) |] ==> P(Sup(a,f))"
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    61
  shows "P(w)"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    62
  \<comment> \<open>A nicer induction rule than the standard one.\<close>
18372
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    63
  using w
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    64
  apply induct
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    65
  apply (assumption | rule step)+
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    66
   apply (fast elim: fun_weaken_type)
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    67
  apply (fast dest: apply_type)
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    68
  done
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    69
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12552
diff changeset
    70
lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    71
  \<comment> \<open>In fact it's isomorphic to \<open>nat\<close>, but we need a recursion operator\<close>
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    72
  \<comment> \<open>for \<open>Well\<close> to prove this.\<close>
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    73
  apply (rule Well_unfold [THEN trans])
46900
73555abfa267 tuned proofs;
wenzelm
parents: 40945
diff changeset
    74
  apply (simp add: Sigma_bool succ_def)
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    75
  done
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    76
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents:
diff changeset
    77
end