src/HOL/Library/ContNotDenum.thy
author wenzelm
Mon, 06 Jul 2015 22:06:02 +0200
changeset 60678 17ba2df56dee
parent 60500 903bb1495239
child 61585 a9599d3d7610
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 58881
diff changeset
     1
(*  Title:      HOL/Library/ContNotDenum.thy
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
     2
    Author:     Benjamin Porter, Monash University, NICTA, 2005
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
     3
    Author:     Johannes Hölzl, TU München
23461
wenzelm
parents: 23389
diff changeset
     4
*)
wenzelm
parents: 23389
diff changeset
     5
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
     6
section \<open>Non-denumerability of the Continuum.\<close>
23461
wenzelm
parents: 23389
diff changeset
     7
wenzelm
parents: 23389
diff changeset
     8
theory ContNotDenum
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
     9
imports Complex_Main Countable_Set
23461
wenzelm
parents: 23389
diff changeset
    10
begin
wenzelm
parents: 23389
diff changeset
    11
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    12
subsection \<open>Abstract\<close>
23461
wenzelm
parents: 23389
diff changeset
    13
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    14
text \<open>The following document presents a proof that the Continuum is
23461
wenzelm
parents: 23389
diff changeset
    15
uncountable. It is formalised in the Isabelle/Isar theorem proving
wenzelm
parents: 23389
diff changeset
    16
system.
wenzelm
parents: 23389
diff changeset
    17
wenzelm
parents: 23389
diff changeset
    18
{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    19
words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
23461
wenzelm
parents: 23389
diff changeset
    20
surjective.
wenzelm
parents: 23389
diff changeset
    21
wenzelm
parents: 23389
diff changeset
    22
{\em Outline:} An elegant informal proof of this result uses Cantor's
wenzelm
parents: 23389
diff changeset
    23
Diagonalisation argument. The proof presented here is not this
wenzelm
parents: 23389
diff changeset
    24
one. First we formalise some properties of closed intervals, then we
wenzelm
parents: 23389
diff changeset
    25
prove the Nested Interval Property. This property relies on the
wenzelm
parents: 23389
diff changeset
    26
completeness of the Real numbers and is the foundation for our
wenzelm
parents: 23389
diff changeset
    27
argument. Informally it states that an intersection of countable
wenzelm
parents: 23389
diff changeset
    28
closed intervals (where each successive interval is a subset of the
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    29
last) is non-empty. We then assume a surjective function @{text
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    30
"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    31
by generating a sequence of closed intervals then using the NIP.\<close>
23461
wenzelm
parents: 23389
diff changeset
    32
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    33
theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    34
proof
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    35
  assume "\<exists>f::nat \<Rightarrow> real. surj f"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    36
  then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    37
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    38
  txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
23461
wenzelm
parents: 23389
diff changeset
    39
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    40
  have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    41
    using assms
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    42
    by (auto simp add: not_le cong: conj_cong)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    43
       (metis dense le_less_linear less_linear less_trans order_refl)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    44
  then obtain i j where ij:
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    45
    "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    46
    "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    47
    "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    48
    by metis
23461
wenzelm
parents: 23389
diff changeset
    49
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    50
  def ivl \<equiv> "rec_nat (f 0 + 1, f 0 + 2) (\<lambda>n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    51
  def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
23461
wenzelm
parents: 23389
diff changeset
    52
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    53
  have ivl[simp]:
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    54
    "ivl 0 = (f 0 + 1, f 0 + 2)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    55
    "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    56
    unfolding ivl_def by simp_all
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    57
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    58
  txt \<open>This is a decreasing sequence of non-empty intervals.\<close>
23461
wenzelm
parents: 23389
diff changeset
    59
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    60
  { fix n have "fst (ivl n) < snd (ivl n)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    61
      by (induct n) (auto intro!: ij) }
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    62
  note less = this
23461
wenzelm
parents: 23389
diff changeset
    63
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    64
  have "decseq I"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    65
    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    66
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    67
  txt \<open>Now we apply the finite intersection property of compact sets.\<close>
23461
wenzelm
parents: 23389
diff changeset
    68
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    69
  have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    70
  proof (rule compact_imp_fip_image)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    71
    fix S :: "nat set" assume fin: "finite S"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    72
    have "{} \<subset> I (Max (insert 0 S))"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    73
      unfolding I_def using less[of "Max (insert 0 S)"] by auto
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    74
    also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    75
      using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    76
    also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    77
      by auto
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    78
    finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    79
      by auto
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    80
  qed (auto simp: I_def)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    81
  then obtain x where "\<And>n. x \<in> I n"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    82
    by blast
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    83
  moreover from \<open>surj f\<close> obtain j where "x = f j"
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    84
    by blast
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    85
  ultimately have "f j \<in> I (Suc j)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    86
    by blast
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    87
  with ij(3)[OF less] show False
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    88
    unfolding I_def ivl fst_conv snd_conv by auto
23461
wenzelm
parents: 23389
diff changeset
    89
qed
wenzelm
parents: 23389
diff changeset
    90
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    91
lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    92
  using real_non_denum unfolding uncountable_def by auto
23461
wenzelm
parents: 23389
diff changeset
    93
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    94
lemma bij_betw_open_intervals:
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    95
  fixes a b c d :: real
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    96
  assumes "a < b" "c < d"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    97
  shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    98
proof -
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    99
  def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   100
  { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   101
    moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   102
      by (intro mult_strict_left_mono) simp_all
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   103
    moreover from * have "0 < (d - c) * (x - a) / (b - a)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   104
      by simp
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   105
    ultimately have "f a b c d x < d" "c < f a b c d x"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   106
      by (simp_all add: f_def field_simps) }
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   107
  with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   108
    by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   109
  thus ?thesis by auto
23461
wenzelm
parents: 23389
diff changeset
   110
qed
wenzelm
parents: 23389
diff changeset
   111
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   112
lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
59872
db4000b71fdb Theorem "arctan" is no longer a default simprule
paulson <lp15@cam.ac.uk>
parents: 59720
diff changeset
   113
  using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
23461
wenzelm
parents: 23389
diff changeset
   114
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   115
lemma uncountable_open_interval:
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   116
  fixes a b :: real 
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   117
  shows "uncountable {a<..<b} \<longleftrightarrow> a < b"
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   118
proof
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   119
  assume "uncountable {a<..<b}"
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   120
  then show "a < b"
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   121
    using uncountable_def by force
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   122
next 
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   123
  assume "a < b"
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   124
  show "uncountable {a<..<b}"
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   125
  proof -
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   126
    obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
   127
      using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   128
    then show ?thesis
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   129
      by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   130
  qed
23461
wenzelm
parents: 23389
diff changeset
   131
qed
wenzelm
parents: 23389
diff changeset
   132
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   133
lemma uncountable_half_open_interval_1:
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   134
  fixes a :: real shows "uncountable {a..<b} \<longleftrightarrow> a<b"
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   135
  apply auto
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   136
  using atLeastLessThan_empty_iff apply fastforce
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   137
  using uncountable_open_interval [of a b]
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   138
  by (metis countable_Un_iff ivl_disj_un_singleton(3))
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   139
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   140
lemma uncountable_half_open_interval_2:
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   141
  fixes a :: real shows "uncountable {a<..b} \<longleftrightarrow> a<b"
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   142
  apply auto
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   143
  using atLeastLessThan_empty_iff apply fastforce
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   144
  using uncountable_open_interval [of a b]
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   145
  by (metis countable_Un_iff ivl_disj_un_singleton(4))
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   146
23461
wenzelm
parents: 23389
diff changeset
   147
end