src/HOL/Hilbert_Choice.thy
author wenzelm
Thu Mar 14 16:55:06 2019 +0100 (5 weeks ago)
changeset 69913 ca515cf61651
parent 69861 62e47f06d22c
child 70097 4005298550a6
permissions -rw-r--r--
more specific keyword kinds;
paulson@11451
     1
(*  Title:      HOL/Hilbert_Choice.thy
nipkow@32988
     2
    Author:     Lawrence C Paulson, Tobias Nipkow
eberlm@67829
     3
    Author:     Viorel Preoteasa (Results about complete distributive lattices) 
paulson@11451
     4
    Copyright   2001  University of Cambridge
wenzelm@12023
     5
*)
paulson@11451
     6
wenzelm@60758
     7
section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>
paulson@11451
     8
nipkow@15131
     9
theory Hilbert_Choice
wenzelm@63612
    10
  imports Wellfounded
wenzelm@69913
    11
  keywords "specification" :: thy_goal_defn
nipkow@15131
    12
begin
wenzelm@12298
    13
wenzelm@60758
    14
subsection \<open>Hilbert's epsilon\<close>
wenzelm@12298
    15
wenzelm@63612
    16
axiomatization Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
wenzelm@63612
    17
  where someI: "P x \<Longrightarrow> P (Eps P)"
paulson@11451
    18
wenzelm@14872
    19
syntax (epsilon)
wenzelm@63612
    20
  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3\<some>_./ _)" [0, 10] 10)
wenzelm@62521
    21
syntax (input)
wenzelm@63612
    22
  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3@ _./ _)" [0, 10] 10)
paulson@11451
    23
syntax
wenzelm@63612
    24
  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3SOME _./ _)" [0, 10] 10)
paulson@11451
    25
translations
wenzelm@63612
    26
  "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
nipkow@13763
    27
wenzelm@60758
    28
print_translation \<open>
wenzelm@69593
    29
  [(\<^const_syntax>\<open>Eps\<close>, fn _ => fn [Abs abs] =>
wenzelm@42284
    30
      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
wenzelm@69593
    31
      in Syntax.const \<^syntax_const>\<open>_Eps\<close> $ x $ t end)]
wenzelm@61799
    32
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
paulson@11451
    33
nipkow@65815
    34
definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
nipkow@65815
    35
"inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)"
paulson@11454
    36
nipkow@65815
    37
lemma inv_into_def2: "inv_into A f x = (SOME y. y \<in> A \<and> f y = x)"
nipkow@65815
    38
by(simp add: inv_into_def)
nipkow@65815
    39
nipkow@65815
    40
abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
nipkow@65815
    41
"inv \<equiv> inv_into UNIV"
paulson@14760
    42
paulson@14760
    43
wenzelm@60758
    44
subsection \<open>Hilbert's Epsilon-operator\<close>
paulson@14760
    45
wenzelm@63612
    46
text \<open>
wenzelm@63612
    47
  Easier to apply than \<open>someI\<close> if the witness comes from an
wenzelm@63612
    48
  existential formula.
wenzelm@63612
    49
\<close>
wenzelm@63612
    50
lemma someI_ex [elim?]: "\<exists>x. P x \<Longrightarrow> P (SOME x. P x)"
wenzelm@63612
    51
  apply (erule exE)
wenzelm@63612
    52
  apply (erule someI)
wenzelm@63612
    53
  done
paulson@14760
    54
wenzelm@63612
    55
text \<open>
wenzelm@63612
    56
  Easier to apply than \<open>someI\<close> because the conclusion has only one
wenzelm@69593
    57
  occurrence of \<^term>\<open>P\<close>.
wenzelm@63612
    58
\<close>
wenzelm@63612
    59
lemma someI2: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
lp15@60974
    60
  by (blast intro: someI)
paulson@14760
    61
wenzelm@63612
    62
text \<open>
wenzelm@63612
    63
  Easier to apply than \<open>someI2\<close> if the witness comes from an
wenzelm@63612
    64
  existential formula.
wenzelm@63612
    65
\<close>
wenzelm@63612
    66
lemma someI2_ex: "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
lp15@60974
    67
  by (blast intro: someI2)
paulson@14760
    68
wenzelm@63612
    69
lemma someI2_bex: "\<exists>a\<in>A. P a \<Longrightarrow> (\<And>x. x \<in> A \<and> P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. x \<in> A \<and> P x)"
wenzelm@63612
    70
  by (blast intro: someI2)
wenzelm@63612
    71
wenzelm@63612
    72
lemma some_equality [intro]: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x = a) \<Longrightarrow> (SOME x. P x) = a"
wenzelm@63612
    73
  by (blast intro: someI2)
paulson@14760
    74
wenzelm@63629
    75
lemma some1_equality: "\<exists>!x. P x \<Longrightarrow> P a \<Longrightarrow> (SOME x. P x) = a"
wenzelm@63612
    76
  by blast
paulson@14760
    77
wenzelm@63612
    78
lemma some_eq_ex: "P (SOME x. P x) \<longleftrightarrow> (\<exists>x. P x)"
wenzelm@63612
    79
  by (blast intro: someI)
paulson@14760
    80
hoelzl@59000
    81
lemma some_in_eq: "(SOME x. x \<in> A) \<in> A \<longleftrightarrow> A \<noteq> {}"
hoelzl@59000
    82
  unfolding ex_in_conv[symmetric] by (rule some_eq_ex)
hoelzl@59000
    83
wenzelm@63612
    84
lemma some_eq_trivial [simp]: "(SOME y. y = x) = x"
wenzelm@63612
    85
  by (rule some_equality) (rule refl)
paulson@14760
    86
wenzelm@63612
    87
lemma some_sym_eq_trivial [simp]: "(SOME y. x = y) = x"
wenzelm@63612
    88
  apply (rule some_equality)
wenzelm@63612
    89
   apply (rule refl)
wenzelm@63612
    90
  apply (erule sym)
wenzelm@63612
    91
  done
paulson@14760
    92
paulson@14760
    93
wenzelm@63612
    94
subsection \<open>Axiom of Choice, Proved Using the Description Operator\<close>
paulson@14760
    95
wenzelm@63612
    96
lemma choice: "\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
wenzelm@63612
    97
  by (fast elim: someI)
paulson@14760
    98
wenzelm@63612
    99
lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
wenzelm@63612
   100
  by (fast elim: someI)
paulson@14760
   101
hoelzl@50105
   102
lemma choice_iff: "(\<forall>x. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x. Q x (f x))"
wenzelm@63612
   103
  by (fast elim: someI)
hoelzl@50105
   104
hoelzl@50105
   105
lemma choice_iff': "(\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x. P x \<longrightarrow> Q x (f x))"
wenzelm@63612
   106
  by (fast elim: someI)
hoelzl@50105
   107
hoelzl@50105
   108
lemma bchoice_iff: "(\<forall>x\<in>S. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. Q x (f x))"
wenzelm@63612
   109
  by (fast elim: someI)
hoelzl@50105
   110
hoelzl@50105
   111
lemma bchoice_iff': "(\<forall>x\<in>S. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. P x \<longrightarrow> Q x (f x))"
wenzelm@63612
   112
  by (fast elim: someI)
paulson@14760
   113
hoelzl@57275
   114
lemma dependent_nat_choice:
wenzelm@63612
   115
  assumes 1: "\<exists>x. P 0 x"
wenzelm@63612
   116
    and 2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
hoelzl@57448
   117
  shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
hoelzl@57275
   118
proof (intro exI allI conjI)
wenzelm@63040
   119
  fix n
wenzelm@63040
   120
  define f where "f = rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)"
wenzelm@63612
   121
  then have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
wenzelm@63612
   122
    using someI_ex[OF 1] someI_ex[OF 2] by simp_all
hoelzl@57448
   123
  then show "P n (f n)" "Q n (f n) (f (Suc n))"
hoelzl@57275
   124
    by (induct n) auto
hoelzl@57275
   125
qed
hoelzl@57275
   126
lp15@68975
   127
lemma finite_subset_Union:
lp15@68975
   128
  assumes "finite A" "A \<subseteq> \<Union>\<B>"
lp15@68975
   129
  obtains \<F> where "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
lp15@68975
   130
proof -
lp15@68975
   131
  have "\<forall>x\<in>A. \<exists>B\<in>\<B>. x\<in>B"
lp15@68975
   132
    using assms by blast
lp15@68975
   133
  then obtain f where f: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<B> \<and> x \<in> f x"
lp15@68975
   134
    by (auto simp add: bchoice_iff Bex_def)
lp15@68975
   135
  show thesis
lp15@68975
   136
  proof
lp15@68975
   137
    show "finite (f ` A)"
lp15@68975
   138
      using assms by auto
lp15@68975
   139
  qed (use f in auto)
lp15@68975
   140
qed
lp15@68975
   141
blanchet@58074
   142
wenzelm@60758
   143
subsection \<open>Function Inverse\<close>
paulson@14760
   144
wenzelm@63612
   145
lemma inv_def: "inv f = (\<lambda>y. SOME x. f x = y)"
wenzelm@63612
   146
  by (simp add: inv_into_def)
nipkow@33014
   147
wenzelm@63612
   148
lemma inv_into_into: "x \<in> f ` A \<Longrightarrow> inv_into A f x \<in> A"
wenzelm@63612
   149
  by (simp add: inv_into_def) (fast intro: someI2)
paulson@14760
   150
wenzelm@63612
   151
lemma inv_identity [simp]: "inv (\<lambda>a. a) = (\<lambda>a. a)"
haftmann@63365
   152
  by (simp add: inv_def)
haftmann@63365
   153
wenzelm@63612
   154
lemma inv_id [simp]: "inv id = id"
haftmann@63365
   155
  by (simp add: id_def)
paulson@14760
   156
wenzelm@63612
   157
lemma inv_into_f_f [simp]: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> inv_into A f (f x) = x"
wenzelm@63612
   158
  by (simp add: inv_into_def inj_on_def) (blast intro: someI2)
paulson@14760
   159
wenzelm@63612
   160
lemma inv_f_f: "inj f \<Longrightarrow> inv f (f x) = x"
wenzelm@63612
   161
  by simp
nipkow@32988
   162
wenzelm@67613
   163
lemma f_inv_into_f: "y \<in> f`A \<Longrightarrow> f (inv_into A f y) = y"
wenzelm@63612
   164
  by (simp add: inv_into_def) (fast intro: someI2)
nipkow@32988
   165
wenzelm@63612
   166
lemma inv_into_f_eq: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> f x = y \<Longrightarrow> inv_into A f y = x"
wenzelm@63612
   167
  by (erule subst) (fast intro: inv_into_f_f)
nipkow@32988
   168
wenzelm@63612
   169
lemma inv_f_eq: "inj f \<Longrightarrow> f x = y \<Longrightarrow> inv f y = x"
wenzelm@63612
   170
  by (simp add:inv_into_f_eq)
nipkow@32988
   171
wenzelm@63612
   172
lemma inj_imp_inv_eq: "inj f \<Longrightarrow> \<forall>x. f (g x) = x \<Longrightarrow> inv f = g"
huffman@44921
   173
  by (blast intro: inv_into_f_eq)
paulson@14760
   174
wenzelm@63612
   175
text \<open>But is it useful?\<close>
paulson@14760
   176
lemma inj_transfer:
wenzelm@63612
   177
  assumes inj: "inj f"
wenzelm@63612
   178
    and minor: "\<And>y. y \<in> range f \<Longrightarrow> P (inv f y)"
paulson@14760
   179
  shows "P x"
paulson@14760
   180
proof -
paulson@14760
   181
  have "f x \<in> range f" by auto
wenzelm@63612
   182
  then have "P(inv f (f x))" by (rule minor)
wenzelm@63612
   183
  then show "P x" by (simp add: inv_into_f_f [OF inj])
paulson@14760
   184
qed
paulson@11451
   185
wenzelm@63612
   186
lemma inj_iff: "inj f \<longleftrightarrow> inv f \<circ> f = id"
wenzelm@63612
   187
  by (simp add: o_def fun_eq_iff) (blast intro: inj_on_inverseI inv_into_f_f)
paulson@14760
   188
wenzelm@63612
   189
lemma inv_o_cancel[simp]: "inj f \<Longrightarrow> inv f \<circ> f = id"
wenzelm@63612
   190
  by (simp add: inj_iff)
wenzelm@63612
   191
wenzelm@63612
   192
lemma o_inv_o_cancel[simp]: "inj f \<Longrightarrow> g \<circ> inv f \<circ> f = g"
wenzelm@63612
   193
  by (simp add: comp_assoc)
nipkow@23433
   194
wenzelm@63612
   195
lemma inv_into_image_cancel[simp]: "inj_on f A \<Longrightarrow> S \<subseteq> A \<Longrightarrow> inv_into A f ` f ` S = S"
wenzelm@63612
   196
  by (fastforce simp: image_def)
nipkow@23433
   197
wenzelm@63612
   198
lemma inj_imp_surj_inv: "inj f \<Longrightarrow> surj (inv f)"
wenzelm@63612
   199
  by (blast intro!: surjI inv_into_f_f)
nipkow@32988
   200
wenzelm@63612
   201
lemma surj_f_inv_f: "surj f \<Longrightarrow> f (inv f y) = y"
wenzelm@63612
   202
  by (simp add: f_inv_into_f)
paulson@14760
   203
lp15@67673
   204
lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
lp15@67673
   205
  using surj_f_inv_f[of p] by (auto simp add: bij_def)
lp15@67673
   206
nipkow@33057
   207
lemma inv_into_injective:
nipkow@33057
   208
  assumes eq: "inv_into A f x = inv_into A f y"
wenzelm@63612
   209
    and x: "x \<in> f`A"
wenzelm@63612
   210
    and y: "y \<in> f`A"
wenzelm@63612
   211
  shows "x = y"
paulson@14760
   212
proof -
wenzelm@63612
   213
  from eq have "f (inv_into A f x) = f (inv_into A f y)"
wenzelm@63612
   214
    by simp
wenzelm@63612
   215
  with x y show ?thesis
wenzelm@63612
   216
    by (simp add: f_inv_into_f)
paulson@14760
   217
qed
paulson@14760
   218
wenzelm@63612
   219
lemma inj_on_inv_into: "B \<subseteq> f`A \<Longrightarrow> inj_on (inv_into A f) B"
wenzelm@63612
   220
  by (blast intro: inj_onI dest: inv_into_injective injD)
nipkow@32988
   221
wenzelm@63612
   222
lemma bij_betw_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (inv_into A f) B A"
wenzelm@63612
   223
  by (auto simp add: bij_betw_def inj_on_inv_into)
paulson@14760
   224
wenzelm@63612
   225
lemma surj_imp_inj_inv: "surj f \<Longrightarrow> inj (inv f)"
wenzelm@63612
   226
  by (simp add: inj_on_inv_into)
paulson@14760
   227
wenzelm@63612
   228
lemma surj_iff: "surj f \<longleftrightarrow> f \<circ> inv f = id"
wenzelm@63612
   229
  by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
hoelzl@40702
   230
hoelzl@40702
   231
lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
wenzelm@63612
   232
  by (simp add: o_def surj_iff fun_eq_iff)
paulson@14760
   233
wenzelm@63612
   234
lemma surj_imp_inv_eq: "surj f \<Longrightarrow> \<forall>x. g (f x) = x \<Longrightarrow> inv f = g"
wenzelm@63612
   235
  apply (rule ext)
wenzelm@63612
   236
  apply (drule_tac x = "inv f x" in spec)
wenzelm@63612
   237
  apply (simp add: surj_f_inv_f)
wenzelm@63612
   238
  done
paulson@14760
   239
wenzelm@63612
   240
lemma bij_imp_bij_inv: "bij f \<Longrightarrow> bij (inv f)"
wenzelm@63612
   241
  by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)
wenzelm@12372
   242
wenzelm@63612
   243
lemma inv_equality: "(\<And>x. g (f x) = x) \<Longrightarrow> (\<And>y. f (g y) = y) \<Longrightarrow> inv f = g"
wenzelm@63612
   244
  by (rule ext) (auto simp add: inv_into_def)
wenzelm@63612
   245
wenzelm@63612
   246
lemma inv_inv_eq: "bij f \<Longrightarrow> inv (inv f) = f"
wenzelm@63612
   247
  by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
paulson@14760
   248
wenzelm@63612
   249
text \<open>
wenzelm@63612
   250
  \<open>bij (inv f)\<close> implies little about \<open>f\<close>. Consider \<open>f :: bool \<Rightarrow> bool\<close> such
wenzelm@63612
   251
  that \<open>f True = f False = True\<close>. Then it ia consistent with axiom \<open>someI\<close>
wenzelm@63612
   252
  that \<open>inv f\<close> could be any function at all, including the identity function.
wenzelm@63612
   253
  If \<open>inv f = id\<close> then \<open>inv f\<close> is a bijection, but \<open>inj f\<close>, \<open>surj f\<close> and \<open>inv
wenzelm@63612
   254
  (inv f) = f\<close> all fail.
wenzelm@63612
   255
\<close>
paulson@14760
   256
nipkow@33057
   257
lemma inv_into_comp:
wenzelm@63612
   258
  "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
wenzelm@63612
   259
    inv_into A (f \<circ> g) x = (inv_into A g \<circ> inv_into (g ` A) f) x"
wenzelm@63612
   260
  apply (rule inv_into_f_eq)
wenzelm@63612
   261
    apply (fast intro: comp_inj_on)
wenzelm@63612
   262
   apply (simp add: inv_into_into)
wenzelm@63612
   263
  apply (simp add: f_inv_into_f inv_into_into)
wenzelm@63612
   264
  done
nipkow@32988
   265
wenzelm@63612
   266
lemma o_inv_distrib: "bij f \<Longrightarrow> bij g \<Longrightarrow> inv (f \<circ> g) = inv g \<circ> inv f"
wenzelm@63612
   267
  by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
paulson@14760
   268
wenzelm@63807
   269
lemma image_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A"
haftmann@62343
   270
  by (simp add: surj_f_inv_f image_comp comp_def)
paulson@14760
   271
wenzelm@63612
   272
lemma image_inv_f_f: "inj f \<Longrightarrow> inv f ` (f ` A) = A"
haftmann@62343
   273
  by simp
paulson@14760
   274
wenzelm@63612
   275
lemma bij_image_Collect_eq: "bij f \<Longrightarrow> f ` Collect P = {y. P (inv f y)}"
wenzelm@63612
   276
  apply auto
wenzelm@63612
   277
   apply (force simp add: bij_is_inj)
wenzelm@63612
   278
  apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
wenzelm@63612
   279
  done
paulson@14760
   280
wenzelm@63612
   281
lemma bij_vimage_eq_inv_image: "bij f \<Longrightarrow> f -` A = inv f ` A"
wenzelm@63612
   282
  apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
wenzelm@63612
   283
  apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
wenzelm@63612
   284
  done
paulson@14760
   285
nipkow@68610
   286
lemma inv_fn_o_fn_is_id:
nipkow@68610
   287
  fixes f::"'a \<Rightarrow> 'a"
nipkow@68610
   288
  assumes "bij f"
nipkow@68610
   289
  shows "((inv f)^^n) o (f^^n) = (\<lambda>x. x)"
nipkow@68610
   290
proof -
nipkow@68610
   291
  have "((inv f)^^n)((f^^n) x) = x" for x n
nipkow@68610
   292
  proof (induction n)
nipkow@68610
   293
    case (Suc n)
nipkow@68610
   294
    have *: "(inv f) (f y) = y" for y
nipkow@68610
   295
      by (simp add: assms bij_is_inj)
nipkow@68610
   296
    have "(inv f ^^ Suc n) ((f ^^ Suc n) x) = (inv f^^n) (inv f (f ((f^^n) x)))"
nipkow@68610
   297
      by (simp add: funpow_swap1)
nipkow@68610
   298
    also have "... = (inv f^^n) ((f^^n) x)"
nipkow@68610
   299
      using * by auto
nipkow@68610
   300
    also have "... = x" using Suc.IH by auto
nipkow@68610
   301
    finally show ?case by simp
nipkow@68610
   302
  qed (auto)
nipkow@68610
   303
  then show ?thesis unfolding o_def by blast
nipkow@68610
   304
qed
nipkow@68610
   305
nipkow@68610
   306
lemma fn_o_inv_fn_is_id:
nipkow@68610
   307
  fixes f::"'a \<Rightarrow> 'a"
nipkow@68610
   308
  assumes "bij f"
nipkow@68610
   309
  shows "(f^^n) o ((inv f)^^n) = (\<lambda>x. x)"
nipkow@68610
   310
proof -
nipkow@68610
   311
  have "(f^^n) (((inv f)^^n) x) = x" for x n
nipkow@68610
   312
  proof (induction n)
nipkow@68610
   313
    case (Suc n)
nipkow@68610
   314
    have *: "f(inv f y) = y" for y
nipkow@68610
   315
      using bij_inv_eq_iff[OF assms] by auto
nipkow@68610
   316
    have "(f ^^ Suc n) ((inv f ^^ Suc n) x) = (f^^n) (f (inv f ((inv f^^n) x)))"
nipkow@68610
   317
      by (simp add: funpow_swap1)
nipkow@68610
   318
    also have "... = (f^^n) ((inv f^^n) x)"
nipkow@68610
   319
      using * by auto
nipkow@68610
   320
    also have "... = x" using Suc.IH by auto
nipkow@68610
   321
    finally show ?case by simp
nipkow@68610
   322
  qed (auto)
nipkow@68610
   323
  then show ?thesis unfolding o_def by blast
nipkow@68610
   324
qed
nipkow@68610
   325
nipkow@68610
   326
lemma inv_fn:
nipkow@68610
   327
  fixes f::"'a \<Rightarrow> 'a"
nipkow@68610
   328
  assumes "bij f"
nipkow@68610
   329
  shows "inv (f^^n) = ((inv f)^^n)"
nipkow@68610
   330
proof -
nipkow@68610
   331
  have "inv (f^^n) x = ((inv f)^^n) x" for x
nipkow@68610
   332
  apply (rule inv_into_f_eq, auto simp add: inj_fn[OF bij_is_inj[OF assms]])
nipkow@68610
   333
  using fn_o_inv_fn_is_id[OF assms, of n, THEN fun_cong] by (simp)
nipkow@68610
   334
  then show ?thesis by auto
nipkow@68610
   335
qed
nipkow@68610
   336
nipkow@68610
   337
lemma mono_inv:
nipkow@68610
   338
  fixes f::"'a::linorder \<Rightarrow> 'b::linorder"
nipkow@68610
   339
  assumes "mono f" "bij f"
nipkow@68610
   340
  shows "mono (inv f)"
nipkow@68610
   341
proof
nipkow@68610
   342
  fix x y::'b assume "x \<le> y"
nipkow@68610
   343
  from \<open>bij f\<close> obtain a b where x: "x = f a" and y: "y = f b" by(fastforce simp: bij_def surj_def)
nipkow@68610
   344
  show "inv f x \<le> inv f y"
nipkow@68610
   345
  proof (rule le_cases)
nipkow@68610
   346
    assume "a \<le> b"
nipkow@68610
   347
    thus ?thesis using  \<open>bij f\<close> x y by(simp add: bij_def inv_f_f)
nipkow@68610
   348
  next
nipkow@68610
   349
    assume "b \<le> a"
nipkow@68610
   350
    hence "f b \<le> f a" by(rule monoD[OF \<open>mono f\<close>])
nipkow@68610
   351
    hence "y \<le> x" using x y by simp
nipkow@68610
   352
    hence "x = y" using \<open>x \<le> y\<close> by auto
nipkow@68610
   353
    thus ?thesis by simp
nipkow@68610
   354
  qed
nipkow@68610
   355
qed
nipkow@68610
   356
nipkow@68610
   357
lemma mono_bij_Inf:
nipkow@68610
   358
  fixes f :: "'a::complete_linorder \<Rightarrow> 'b::complete_linorder"
nipkow@68610
   359
  assumes "mono f" "bij f"
nipkow@68610
   360
  shows "f (Inf A) = Inf (f`A)"
nipkow@68610
   361
proof -
nipkow@68610
   362
  have "surj f" using \<open>bij f\<close> by (auto simp: bij_betw_def)
nipkow@68610
   363
  have *: "(inv f) (Inf (f`A)) \<le> Inf ((inv f)`(f`A))"
nipkow@68610
   364
    using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp
nipkow@68610
   365
  have "Inf (f`A) \<le> f (Inf ((inv f)`(f`A)))"
nipkow@68610
   366
    using monoD[OF \<open>mono f\<close> *] by(simp add: surj_f_inv_f[OF \<open>surj f\<close>])
nipkow@68610
   367
  also have "... = f(Inf A)"
nipkow@68610
   368
    using assms by (simp add: bij_is_inj)
nipkow@68610
   369
  finally show ?thesis using mono_Inf[OF assms(1), of A] by auto
nipkow@68610
   370
qed
nipkow@68610
   371
haftmann@31380
   372
lemma finite_fun_UNIVD1:
haftmann@31380
   373
  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
wenzelm@63612
   374
    and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
haftmann@31380
   375
  shows "finite (UNIV :: 'a set)"
haftmann@31380
   376
proof -
wenzelm@63630
   377
  let ?UNIV_b = "UNIV :: 'b set"
wenzelm@63630
   378
  from fin have "finite ?UNIV_b"
wenzelm@63612
   379
    by (rule finite_fun_UNIVD2)
wenzelm@63630
   380
  with card have "card ?UNIV_b \<ge> Suc (Suc 0)"
wenzelm@63630
   381
    by (cases "card ?UNIV_b") (auto simp: card_eq_0_iff)
wenzelm@63630
   382
  then have "card ?UNIV_b = Suc (Suc (card ?UNIV_b - Suc (Suc 0)))"
wenzelm@63630
   383
    by simp
wenzelm@63629
   384
  then obtain b1 b2 :: 'b where b1b2: "b1 \<noteq> b2"
wenzelm@63629
   385
    by (auto simp: card_Suc_eq)
wenzelm@63630
   386
  from fin have fin': "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))"
wenzelm@63612
   387
    by (rule finite_imageI)
wenzelm@63630
   388
  have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
haftmann@31380
   389
  proof (rule UNIV_eq_I)
haftmann@31380
   390
    fix x :: 'a
wenzelm@63612
   391
    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1"
wenzelm@63612
   392
      by (simp add: inv_into_def)
wenzelm@63612
   393
    then show "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)"
wenzelm@63612
   394
      by blast
haftmann@31380
   395
  qed
wenzelm@63630
   396
  with fin' show ?thesis
wenzelm@63612
   397
    by simp
haftmann@31380
   398
qed
paulson@14760
   399
wenzelm@60758
   400
text \<open>
traytel@54578
   401
  Every infinite set contains a countable subset. More precisely we
wenzelm@61799
   402
  show that a set \<open>S\<close> is infinite if and only if there exists an
wenzelm@61799
   403
  injective function from the naturals into \<open>S\<close>.
traytel@54578
   404
traytel@54578
   405
  The ``only if'' direction is harder because it requires the
traytel@54578
   406
  construction of a sequence of pairwise different elements of an
wenzelm@61799
   407
  infinite set \<open>S\<close>. The idea is to construct a sequence of
wenzelm@61799
   408
  non-empty and infinite subsets of \<open>S\<close> obtained by successively
wenzelm@61799
   409
  removing elements of \<open>S\<close>.
wenzelm@60758
   410
\<close>
traytel@54578
   411
traytel@54578
   412
lemma infinite_countable_subset:
wenzelm@63629
   413
  assumes inf: "\<not> finite S"
wenzelm@63629
   414
  shows "\<exists>f::nat \<Rightarrow> 'a. inj f \<and> range f \<subseteq> S"
wenzelm@61799
   415
  \<comment> \<open>Courtesy of Stephan Merz\<close>
traytel@54578
   416
proof -
wenzelm@63040
   417
  define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
wenzelm@63040
   418
  define pick where "pick n = (SOME e. e \<in> Sseq n)" for n
wenzelm@63540
   419
  have *: "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" for n
wenzelm@63612
   420
    by (induct n) (auto simp: Sseq_def inf)
wenzelm@63540
   421
  then have **: "\<And>n. pick n \<in> Sseq n"
traytel@55811
   422
    unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
wenzelm@63540
   423
  with * have "range pick \<subseteq> S" by auto
wenzelm@63612
   424
  moreover have "pick n \<noteq> pick (n + Suc m)" for m n
wenzelm@63612
   425
  proof -
wenzelm@63540
   426
    have "pick n \<notin> Sseq (n + Suc m)"
wenzelm@63540
   427
      by (induct m) (auto simp add: Sseq_def pick_def)
wenzelm@63612
   428
    with ** show ?thesis by auto
wenzelm@63612
   429
  qed
wenzelm@63612
   430
  then have "inj pick"
wenzelm@63612
   431
    by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
traytel@54578
   432
  ultimately show ?thesis by blast
traytel@54578
   433
qed
traytel@54578
   434
wenzelm@63629
   435
lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f::nat \<Rightarrow> 'a. inj f \<and> range f \<subseteq> S)"
wenzelm@61799
   436
  \<comment> \<open>Courtesy of Stephan Merz\<close>
traytel@55811
   437
  using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto
traytel@54578
   438
hoelzl@40703
   439
lemma image_inv_into_cancel:
wenzelm@63612
   440
  assumes surj: "f`A = A'"
wenzelm@63612
   441
    and sub: "B' \<subseteq> A'"
hoelzl@40703
   442
  shows "f `((inv_into A f)`B') = B'"
hoelzl@40703
   443
  using assms
wenzelm@63612
   444
proof (auto simp: f_inv_into_f)
wenzelm@63612
   445
  let ?f' = "inv_into A f"
wenzelm@63612
   446
  fix a'
wenzelm@63612
   447
  assume *: "a' \<in> B'"
wenzelm@63612
   448
  with sub have "a' \<in> A'" by auto
wenzelm@63612
   449
  with surj have "a' = f (?f' a')"
wenzelm@63612
   450
    by (auto simp: f_inv_into_f)
wenzelm@63612
   451
  with * show "a' \<in> f ` (?f' ` B')" by blast
hoelzl@40703
   452
qed
hoelzl@40703
   453
hoelzl@40703
   454
lemma inv_into_inv_into_eq:
wenzelm@63612
   455
  assumes "bij_betw f A A'"
wenzelm@63612
   456
    and a: "a \<in> A"
hoelzl@40703
   457
  shows "inv_into A' (inv_into A f) a = f a"
hoelzl@40703
   458
proof -
wenzelm@63612
   459
  let ?f' = "inv_into A f"
wenzelm@63612
   460
  let ?f'' = "inv_into A' ?f'"
wenzelm@63612
   461
  from assms have *: "bij_betw ?f' A' A"
wenzelm@63612
   462
    by (auto simp: bij_betw_inv_into)
wenzelm@63612
   463
  with a obtain a' where a': "a' \<in> A'" "?f' a' = a"
wenzelm@63612
   464
    unfolding bij_betw_def by force
wenzelm@63612
   465
  with a * have "?f'' a = a'"
wenzelm@63612
   466
    by (auto simp: f_inv_into_f bij_betw_def)
wenzelm@63612
   467
  moreover from assms a' have "f a = a'"
wenzelm@63612
   468
    by (auto simp: bij_betw_def)
hoelzl@40703
   469
  ultimately show "?f'' a = f a" by simp
hoelzl@40703
   470
qed
hoelzl@40703
   471
hoelzl@40703
   472
lemma inj_on_iff_surj:
hoelzl@40703
   473
  assumes "A \<noteq> {}"
wenzelm@63629
   474
  shows "(\<exists>f. inj_on f A \<and> f ` A \<subseteq> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
hoelzl@40703
   475
proof safe
wenzelm@63612
   476
  fix f
wenzelm@63612
   477
  assume inj: "inj_on f A" and incl: "f ` A \<subseteq> A'"
wenzelm@63612
   478
  let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'"
wenzelm@63612
   479
  let ?csi = "\<lambda>a. a \<in> A"
hoelzl@40703
   480
  let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)"
hoelzl@40703
   481
  have "?g ` A' = A"
hoelzl@40703
   482
  proof
wenzelm@63612
   483
    show "?g ` A' \<subseteq> A"
hoelzl@40703
   484
    proof clarify
wenzelm@63612
   485
      fix a'
wenzelm@63612
   486
      assume *: "a' \<in> A'"
hoelzl@40703
   487
      show "?g a' \<in> A"
wenzelm@63612
   488
      proof (cases "a' \<in> f ` A")
wenzelm@63612
   489
        case True
hoelzl@40703
   490
        then obtain a where "?phi a' a" by blast
wenzelm@63612
   491
        then have "?phi a' (SOME a. ?phi a' a)"
wenzelm@63612
   492
          using someI[of "?phi a'" a] by blast
wenzelm@63612
   493
        with True show ?thesis by auto
hoelzl@40703
   494
      next
wenzelm@63612
   495
        case False
wenzelm@63612
   496
        with assms have "?csi (SOME a. ?csi a)"
wenzelm@63612
   497
          using someI_ex[of ?csi] by blast
wenzelm@63612
   498
        with False show ?thesis by auto
hoelzl@40703
   499
      qed
hoelzl@40703
   500
    qed
hoelzl@40703
   501
  next
wenzelm@63612
   502
    show "A \<subseteq> ?g ` A'"
wenzelm@63612
   503
    proof -
wenzelm@63612
   504
      have "?g (f a) = a \<and> f a \<in> A'" if a: "a \<in> A" for a
wenzelm@63612
   505
      proof -
wenzelm@63612
   506
        let ?b = "SOME aa. ?phi (f a) aa"
wenzelm@63612
   507
        from a have "?phi (f a) a" by auto
wenzelm@63612
   508
        then have *: "?phi (f a) ?b"
wenzelm@63612
   509
          using someI[of "?phi(f a)" a] by blast
wenzelm@63612
   510
        then have "?g (f a) = ?b" using a by auto
wenzelm@63612
   511
        moreover from inj * a have "a = ?b"
wenzelm@63612
   512
          by (auto simp add: inj_on_def)
wenzelm@63612
   513
        ultimately have "?g(f a) = a" by simp
wenzelm@63612
   514
        with incl a show ?thesis by auto
wenzelm@63612
   515
      qed
wenzelm@63612
   516
      then show ?thesis by force
hoelzl@40703
   517
    qed
hoelzl@40703
   518
  qed
wenzelm@63612
   519
  then show "\<exists>g. g ` A' = A" by blast
hoelzl@40703
   520
next
wenzelm@63612
   521
  fix g
wenzelm@63612
   522
  let ?f = "inv_into A' g"
hoelzl@40703
   523
  have "inj_on ?f (g ` A')"
wenzelm@63612
   524
    by (auto simp: inj_on_inv_into)
wenzelm@63612
   525
  moreover have "?f (g a') \<in> A'" if a': "a' \<in> A'" for a'
wenzelm@63612
   526
  proof -
wenzelm@63612
   527
    let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
wenzelm@63612
   528
    from a' have "?phi a'" by auto
wenzelm@63612
   529
    then have "?phi (SOME b'. ?phi b')"
wenzelm@63612
   530
      using someI[of ?phi] by blast
wenzelm@63612
   531
    then show ?thesis by (auto simp: inv_into_def)
wenzelm@63612
   532
  qed
wenzelm@63612
   533
  ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'"
wenzelm@63612
   534
    by auto
hoelzl@40703
   535
qed
hoelzl@40703
   536
hoelzl@40703
   537
lemma Ex_inj_on_UNION_Sigma:
wenzelm@63629
   538
  "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i))"
hoelzl@40703
   539
proof
wenzelm@63612
   540
  let ?phi = "\<lambda>a i. i \<in> I \<and> a \<in> A i"
wenzelm@63612
   541
  let ?sm = "\<lambda>a. SOME i. ?phi a i"
hoelzl@40703
   542
  let ?f = "\<lambda>a. (?sm a, a)"
wenzelm@63612
   543
  have "inj_on ?f (\<Union>i \<in> I. A i)"
wenzelm@63612
   544
    by (auto simp: inj_on_def)
hoelzl@40703
   545
  moreover
wenzelm@63612
   546
  have "?sm a \<in> I \<and> a \<in> A(?sm a)" if "i \<in> I" and "a \<in> A i" for i a
wenzelm@63612
   547
    using that someI[of "?phi a" i] by auto
wenzelm@63629
   548
  then have "?f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i)"
wenzelm@63612
   549
    by auto
wenzelm@63629
   550
  ultimately show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i)"
wenzelm@63612
   551
    by auto
hoelzl@40703
   552
qed
hoelzl@40703
   553
haftmann@56608
   554
lemma inv_unique_comp:
haftmann@56608
   555
  assumes fg: "f \<circ> g = id"
haftmann@56608
   556
    and gf: "g \<circ> f = id"
haftmann@56608
   557
  shows "inv f = g"
haftmann@56608
   558
  using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
haftmann@56608
   559
haftmann@56608
   560
wenzelm@60758
   561
subsection \<open>Other Consequences of Hilbert's Epsilon\<close>
paulson@14760
   562
wenzelm@69593
   563
text \<open>Hilbert's Epsilon and the \<^term>\<open>split\<close> Operator\<close>
paulson@14760
   564
wenzelm@63612
   565
text \<open>Looping simprule!\<close>
wenzelm@63612
   566
lemma split_paired_Eps: "(SOME x. P x) = (SOME (a, b). P (a, b))"
haftmann@26347
   567
  by simp
paulson@14760
   568
haftmann@61424
   569
lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
haftmann@26347
   570
  by (simp add: split_def)
paulson@14760
   571
wenzelm@63612
   572
lemma Eps_case_prod_eq [simp]: "(SOME (x', y'). x = x' \<and> y = y') = (x, y)"
haftmann@26347
   573
  by blast
paulson@14760
   574
paulson@14760
   575
wenzelm@63612
   576
text \<open>A relation is wellfounded iff it has no infinite descending chain.\<close>
wenzelm@63981
   577
lemma wf_iff_no_infinite_down_chain: "wf r \<longleftrightarrow> (\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> r)"
wenzelm@63981
   578
  (is "_ \<longleftrightarrow> \<not> ?ex")
wenzelm@63981
   579
proof
wenzelm@63981
   580
  assume "wf r"
wenzelm@63981
   581
  show "\<not> ?ex"
wenzelm@63981
   582
  proof
wenzelm@63981
   583
    assume ?ex
wenzelm@63981
   584
    then obtain f where f: "(f (Suc i), f i) \<in> r" for i
wenzelm@63981
   585
      by blast
wenzelm@63981
   586
    from \<open>wf r\<close> have minimal: "x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" for x Q
wenzelm@63981
   587
      by (auto simp: wf_eq_minimal)
wenzelm@63981
   588
    let ?Q = "{w. \<exists>i. w = f i}"
wenzelm@63981
   589
    fix n
wenzelm@63981
   590
    have "f n \<in> ?Q" by blast
wenzelm@63981
   591
    from minimal [OF this] obtain j where "(y, f j) \<in> r \<Longrightarrow> y \<notin> ?Q" for y by blast
wenzelm@63981
   592
    with this [OF \<open>(f (Suc j), f j) \<in> r\<close>] have "f (Suc j) \<notin> ?Q" by simp
wenzelm@63981
   593
    then show False by blast
wenzelm@63981
   594
  qed
wenzelm@63981
   595
next
wenzelm@63981
   596
  assume "\<not> ?ex"
wenzelm@63981
   597
  then show "wf r"
wenzelm@63981
   598
  proof (rule contrapos_np)
wenzelm@63981
   599
    assume "\<not> wf r"
wenzelm@63981
   600
    then obtain Q x where x: "x \<in> Q" and rec: "z \<in> Q \<Longrightarrow> \<exists>y. (y, z) \<in> r \<and> y \<in> Q" for z
wenzelm@63981
   601
      by (auto simp add: wf_eq_minimal)
wenzelm@63981
   602
    obtain descend :: "nat \<Rightarrow> 'a"
wenzelm@63981
   603
      where descend_0: "descend 0 = x"
wenzelm@63981
   604
        and descend_Suc: "descend (Suc n) = (SOME y. y \<in> Q \<and> (y, descend n) \<in> r)" for n
wenzelm@63981
   605
      by (rule that [of "rec_nat x (\<lambda>_ rec. (SOME y. y \<in> Q \<and> (y, rec) \<in> r))"]) simp_all
wenzelm@63981
   606
    have descend_Q: "descend n \<in> Q" for n
wenzelm@63981
   607
    proof (induct n)
wenzelm@63981
   608
      case 0
wenzelm@63981
   609
      with x show ?case by (simp only: descend_0)
wenzelm@63981
   610
    next
wenzelm@63981
   611
      case Suc
wenzelm@63981
   612
      then show ?case by (simp only: descend_Suc) (rule someI2_ex; use rec in blast)
wenzelm@63981
   613
    qed
wenzelm@63981
   614
    have "(descend (Suc i), descend i) \<in> r" for i
wenzelm@63981
   615
      by (simp only: descend_Suc) (rule someI2_ex; use descend_Q rec in blast)
wenzelm@63981
   616
    then show "\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r" by blast
wenzelm@63981
   617
  qed
wenzelm@63981
   618
qed
paulson@14760
   619
nipkow@27760
   620
lemma wf_no_infinite_down_chainE:
wenzelm@63612
   621
  assumes "wf r"
wenzelm@63612
   622
  obtains k where "(f (Suc k), f k) \<notin> r"
wenzelm@63612
   623
  using assms wf_iff_no_infinite_down_chain[of r] by blast
nipkow@27760
   624
nipkow@27760
   625
wenzelm@63612
   626
text \<open>A dynamically-scoped fact for TFL\<close>
wenzelm@63612
   627
lemma tfl_some: "\<forall>P x. P x \<longrightarrow> P (Eps P)"
wenzelm@12298
   628
  by (blast intro: someI)
paulson@11451
   629
wenzelm@12298
   630
wenzelm@60758
   631
subsection \<open>An aside: bounded accessible part\<close>
haftmann@49948
   632
wenzelm@60758
   633
text \<open>Finite monotone eventually stable sequences\<close>
haftmann@49948
   634
haftmann@49948
   635
lemma finite_mono_remains_stable_implies_strict_prefix:
haftmann@49948
   636
  fixes f :: "nat \<Rightarrow> 'a::order"
wenzelm@63612
   637
  assumes S: "finite (range f)" "mono f"
wenzelm@63612
   638
    and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
haftmann@49948
   639
  shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
haftmann@49948
   640
  using assms
haftmann@49948
   641
proof -
haftmann@49948
   642
  have "\<exists>n. f n = f (Suc n)"
haftmann@49948
   643
  proof (rule ccontr)
haftmann@49948
   644
    assume "\<not> ?thesis"
haftmann@49948
   645
    then have "\<And>n. f n \<noteq> f (Suc n)" by auto
wenzelm@63612
   646
    with \<open>mono f\<close> have "\<And>n. f n < f (Suc n)"
wenzelm@63612
   647
      by (auto simp: le_less mono_iff_le_Suc)
wenzelm@63612
   648
    with lift_Suc_mono_less_iff[of f] have *: "\<And>n m. n < m \<Longrightarrow> f n < f m"
wenzelm@63612
   649
      by auto
traytel@55811
   650
    have "inj f"
traytel@55811
   651
    proof (intro injI)
traytel@55811
   652
      fix x y
traytel@55811
   653
      assume "f x = f y"
wenzelm@63612
   654
      then show "x = y"
wenzelm@63612
   655
        by (cases x y rule: linorder_cases) (auto dest: *)
traytel@55811
   656
    qed
wenzelm@60758
   657
    with \<open>finite (range f)\<close> have "finite (UNIV::nat set)"
haftmann@49948
   658
      by (rule finite_imageD)
haftmann@49948
   659
    then show False by simp
haftmann@49948
   660
  qed
haftmann@49948
   661
  then obtain n where n: "f n = f (Suc n)" ..
wenzelm@63040
   662
  define N where "N = (LEAST n. f n = f (Suc n))"
haftmann@49948
   663
  have N: "f N = f (Suc N)"
haftmann@49948
   664
    unfolding N_def using n by (rule LeastI)
haftmann@49948
   665
  show ?thesis
haftmann@49948
   666
  proof (intro exI[of _ N] conjI allI impI)
wenzelm@63612
   667
    fix n
wenzelm@63612
   668
    assume "N \<le> n"
haftmann@49948
   669
    then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
haftmann@49948
   670
    proof (induct rule: dec_induct)
wenzelm@63612
   671
      case base
wenzelm@63612
   672
      then show ?case by simp
wenzelm@63612
   673
    next
wenzelm@63612
   674
      case (step n)
wenzelm@63612
   675
      then show ?case
wenzelm@63612
   676
        using eq [rule_format, of "n - 1"] N
haftmann@49948
   677
        by (cases n) (auto simp add: le_Suc_eq)
wenzelm@63612
   678
    qed
wenzelm@60758
   679
    from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto
haftmann@49948
   680
  next
wenzelm@63612
   681
    fix n m :: nat
wenzelm@63612
   682
    assume "m < n" "n \<le> N"
haftmann@49948
   683
    then show "f m < f n"
wenzelm@62683
   684
    proof (induct rule: less_Suc_induct)
haftmann@49948
   685
      case (1 i)
haftmann@49948
   686
      then have "i < N" by simp
haftmann@49948
   687
      then have "f i \<noteq> f (Suc i)"
haftmann@49948
   688
        unfolding N_def by (rule not_less_Least)
wenzelm@60758
   689
      with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le)
wenzelm@63612
   690
    next
wenzelm@63612
   691
      case 2
wenzelm@63612
   692
      then show ?case by simp
wenzelm@63612
   693
    qed
haftmann@49948
   694
  qed
haftmann@49948
   695
qed
haftmann@49948
   696
haftmann@49948
   697
lemma finite_mono_strict_prefix_implies_finite_fixpoint:
haftmann@49948
   698
  fixes f :: "nat \<Rightarrow> 'a set"
haftmann@49948
   699
  assumes S: "\<And>i. f i \<subseteq> S" "finite S"
wenzelm@63612
   700
    and ex: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
haftmann@49948
   701
  shows "f (card S) = (\<Union>n. f n)"
haftmann@49948
   702
proof -
wenzelm@63612
   703
  from ex obtain N where inj: "\<And>n m. n \<le> N \<Longrightarrow> m \<le> N \<Longrightarrow> m < n \<Longrightarrow> f m \<subset> f n"
wenzelm@63612
   704
    and eq: "\<forall>n\<ge>N. f N = f n"
wenzelm@63612
   705
    by atomize auto
wenzelm@63612
   706
  have "i \<le> N \<Longrightarrow> i \<le> card (f i)" for i
wenzelm@63612
   707
  proof (induct i)
wenzelm@63612
   708
    case 0
wenzelm@63612
   709
    then show ?case by simp
wenzelm@63612
   710
  next
wenzelm@63612
   711
    case (Suc i)
wenzelm@63612
   712
    with inj [of "Suc i" i] have "(f i) \<subset> (f (Suc i))" by auto
wenzelm@63612
   713
    moreover have "finite (f (Suc i))" using S by (rule finite_subset)
wenzelm@63612
   714
    ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
wenzelm@63612
   715
    with Suc inj show ?case by auto
wenzelm@63612
   716
  qed
haftmann@49948
   717
  then have "N \<le> card (f N)" by simp
haftmann@49948
   718
  also have "\<dots> \<le> card S" using S by (intro card_mono)
haftmann@49948
   719
  finally have "f (card S) = f N" using eq by auto
wenzelm@63612
   720
  then show ?thesis
wenzelm@63612
   721
    using eq inj [of N]
haftmann@49948
   722
    apply auto
haftmann@49948
   723
    apply (case_tac "n < N")
wenzelm@63612
   724
     apply (auto simp: not_less)
haftmann@49948
   725
    done
haftmann@49948
   726
qed
haftmann@49948
   727
haftmann@49948
   728
wenzelm@60758
   729
subsection \<open>More on injections, bijections, and inverses\<close>
blanchet@55020
   730
haftmann@63374
   731
locale bijection =
haftmann@63374
   732
  fixes f :: "'a \<Rightarrow> 'a"
haftmann@63374
   733
  assumes bij: "bij f"
haftmann@63374
   734
begin
haftmann@63374
   735
wenzelm@63612
   736
lemma bij_inv: "bij (inv f)"
haftmann@63374
   737
  using bij by (rule bij_imp_bij_inv)
haftmann@63374
   738
wenzelm@63612
   739
lemma surj [simp]: "surj f"
haftmann@63374
   740
  using bij by (rule bij_is_surj)
haftmann@63374
   741
wenzelm@63612
   742
lemma inj: "inj f"
haftmann@63374
   743
  using bij by (rule bij_is_inj)
haftmann@63374
   744
wenzelm@63612
   745
lemma surj_inv [simp]: "surj (inv f)"
haftmann@63374
   746
  using inj by (rule inj_imp_surj_inv)
haftmann@63374
   747
wenzelm@63612
   748
lemma inj_inv: "inj (inv f)"
haftmann@63374
   749
  using surj by (rule surj_imp_inj_inv)
haftmann@63374
   750
wenzelm@63612
   751
lemma eqI: "f a = f b \<Longrightarrow> a = b"
haftmann@63374
   752
  using inj by (rule injD)
haftmann@63374
   753
wenzelm@63612
   754
lemma eq_iff [simp]: "f a = f b \<longleftrightarrow> a = b"
haftmann@63374
   755
  by (auto intro: eqI)
haftmann@63374
   756
wenzelm@63612
   757
lemma eq_invI: "inv f a = inv f b \<Longrightarrow> a = b"
haftmann@63374
   758
  using inj_inv by (rule injD)
haftmann@63374
   759
wenzelm@63612
   760
lemma eq_inv_iff [simp]: "inv f a = inv f b \<longleftrightarrow> a = b"
haftmann@63374
   761
  by (auto intro: eq_invI)
haftmann@63374
   762
wenzelm@63612
   763
lemma inv_left [simp]: "inv f (f a) = a"
haftmann@63374
   764
  using inj by (simp add: inv_f_eq)
haftmann@63374
   765
wenzelm@63612
   766
lemma inv_comp_left [simp]: "inv f \<circ> f = id"
haftmann@63374
   767
  by (simp add: fun_eq_iff)
haftmann@63374
   768
wenzelm@63612
   769
lemma inv_right [simp]: "f (inv f a) = a"
haftmann@63374
   770
  using surj by (simp add: surj_f_inv_f)
haftmann@63374
   771
wenzelm@63612
   772
lemma inv_comp_right [simp]: "f \<circ> inv f = id"
haftmann@63374
   773
  by (simp add: fun_eq_iff)
haftmann@63374
   774
wenzelm@63612
   775
lemma inv_left_eq_iff [simp]: "inv f a = b \<longleftrightarrow> f b = a"
haftmann@63374
   776
  by auto
haftmann@63374
   777
wenzelm@63612
   778
lemma inv_right_eq_iff [simp]: "b = inv f a \<longleftrightarrow> f b = a"
haftmann@63374
   779
  by auto
haftmann@63374
   780
haftmann@63374
   781
end
haftmann@63374
   782
blanchet@55020
   783
lemma infinite_imp_bij_betw:
wenzelm@63612
   784
  assumes infinite: "\<not> finite A"
wenzelm@63612
   785
  shows "\<exists>h. bij_betw h A (A - {a})"
wenzelm@63612
   786
proof (cases "a \<in> A")
wenzelm@63612
   787
  case False
wenzelm@63612
   788
  then have "A - {a} = A" by blast
wenzelm@63612
   789
  then show ?thesis
wenzelm@63612
   790
    using bij_betw_id[of A] by auto
blanchet@55020
   791
next
wenzelm@63612
   792
  case True
wenzelm@63612
   793
  with infinite have "\<not> finite (A - {a})" by auto
wenzelm@63612
   794
  with infinite_iff_countable_subset[of "A - {a}"]
wenzelm@63612
   795
  obtain f :: "nat \<Rightarrow> 'a" where 1: "inj f" and 2: "f ` UNIV \<subseteq> A - {a}" by blast
wenzelm@63612
   796
  define g where "g n = (if n = 0 then a else f (Suc n))" for n
wenzelm@63612
   797
  define A' where "A' = g ` UNIV"
wenzelm@63612
   798
  have *: "\<forall>y. f y \<noteq> a" using 2 by blast
wenzelm@63612
   799
  have 3: "inj_on g UNIV \<and> g ` UNIV \<subseteq> A \<and> a \<in> g ` UNIV"
wenzelm@63612
   800
    apply (auto simp add: True g_def [abs_def])
wenzelm@63612
   801
     apply (unfold inj_on_def)
wenzelm@63612
   802
     apply (intro ballI impI)
wenzelm@63612
   803
     apply (case_tac "x = 0")
wenzelm@63612
   804
      apply (auto simp add: 2)
wenzelm@63612
   805
  proof -
wenzelm@63612
   806
    fix y
wenzelm@63612
   807
    assume "a = (if y = 0 then a else f (Suc y))"
wenzelm@63612
   808
    then show "y = 0" by (cases "y = 0") (use * in auto)
blanchet@55020
   809
  next
blanchet@55020
   810
    fix x y
blanchet@55020
   811
    assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
wenzelm@63612
   812
    with 1 * show "x = y" by (cases "y = 0") (auto simp: inj_on_def)
blanchet@55020
   813
  next
wenzelm@63612
   814
    fix n
wenzelm@63612
   815
    from 2 show "f (Suc n) \<in> A" by blast
blanchet@55020
   816
  qed
wenzelm@63612
   817
  then have 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<subseteq> A"
wenzelm@63612
   818
    using inj_on_imp_bij_betw[of g] by (auto simp: A'_def)
wenzelm@63612
   819
  then have 5: "bij_betw (inv g) A' UNIV"
wenzelm@63612
   820
    by (auto simp add: bij_betw_inv_into)
wenzelm@63612
   821
  from 3 obtain n where n: "g n = a" by auto
wenzelm@63612
   822
  have 6: "bij_betw g (UNIV - {n}) (A' - {a})"
wenzelm@63612
   823
    by (rule bij_betw_subset) (use 3 4 n in \<open>auto simp: image_set_diff A'_def\<close>)
wenzelm@63612
   824
  define v where "v m = (if m < n then m else Suc m)" for m
blanchet@55020
   825
  have 7: "bij_betw v UNIV (UNIV - {n})"
wenzelm@63612
   826
  proof (unfold bij_betw_def inj_on_def, intro conjI, clarify)
wenzelm@63612
   827
    fix m1 m2
wenzelm@63612
   828
    assume "v m1 = v m2"
wenzelm@63612
   829
    then show "m1 = m2"
wenzelm@63612
   830
      apply (cases "m1 < n")
wenzelm@63612
   831
       apply (cases "m2 < n")
wenzelm@63612
   832
        apply (auto simp: inj_on_def v_def [abs_def])
wenzelm@63612
   833
      apply (cases "m2 < n")
wenzelm@63612
   834
       apply auto
wenzelm@63612
   835
      done
blanchet@55020
   836
  next
blanchet@55020
   837
    show "v ` UNIV = UNIV - {n}"
wenzelm@63612
   838
    proof (auto simp: v_def [abs_def])
wenzelm@63612
   839
      fix m
wenzelm@63612
   840
      assume "m \<noteq> n"
wenzelm@63612
   841
      assume *: "m \<notin> Suc ` {m'. \<not> m' < n}"
wenzelm@63612
   842
      have False if "n \<le> m"
wenzelm@63612
   843
      proof -
wenzelm@63612
   844
        from \<open>m \<noteq> n\<close> that have **: "Suc n \<le> m" by auto
wenzelm@63612
   845
        from Suc_le_D [OF this] obtain m' where m': "m = Suc m'" ..
wenzelm@63612
   846
        with ** have "n \<le> m'" by auto
wenzelm@63612
   847
        with m' * show ?thesis by auto
wenzelm@63612
   848
      qed
wenzelm@63612
   849
      then show "m < n" by force
blanchet@55020
   850
    qed
blanchet@55020
   851
  qed
wenzelm@63612
   852
  define h' where "h' = g \<circ> v \<circ> (inv g)"
wenzelm@63612
   853
  with 5 6 7 have 8: "bij_betw h' A' (A' - {a})"
wenzelm@63612
   854
    by (auto simp add: bij_betw_trans)
wenzelm@63612
   855
  define h where "h b = (if b \<in> A' then h' b else b)" for b
wenzelm@63612
   856
  then have "\<forall>b \<in> A'. h b = h' b" by simp
wenzelm@63612
   857
  with 8 have "bij_betw h  A' (A' - {a})"
wenzelm@63612
   858
    using bij_betw_cong[of A' h] by auto
blanchet@55020
   859
  moreover
wenzelm@63612
   860
  have "\<forall>b \<in> A - A'. h b = b" by (auto simp: h_def)
wenzelm@63612
   861
  then have "bij_betw h  (A - A') (A - A')"
wenzelm@63612
   862
    using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
blanchet@55020
   863
  moreover
wenzelm@63612
   864
  from 4 have "(A' \<inter> (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
wenzelm@63612
   865
    ((A' - {a}) \<inter> (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
wenzelm@63612
   866
    by blast
blanchet@55020
   867
  ultimately have "bij_betw h A (A - {a})"
wenzelm@63612
   868
    using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
wenzelm@63612
   869
  then show ?thesis by blast
blanchet@55020
   870
qed
blanchet@55020
   871
blanchet@55020
   872
lemma infinite_imp_bij_betw2:
wenzelm@63612
   873
  assumes "\<not> finite A"
wenzelm@63612
   874
  shows "\<exists>h. bij_betw h A (A \<union> {a})"
wenzelm@63612
   875
proof (cases "a \<in> A")
wenzelm@63612
   876
  case True
wenzelm@63612
   877
  then have "A \<union> {a} = A" by blast
wenzelm@63612
   878
  then show ?thesis using bij_betw_id[of A] by auto
blanchet@55020
   879
next
wenzelm@63612
   880
  case False
blanchet@55020
   881
  let ?A' = "A \<union> {a}"
wenzelm@63612
   882
  from False have "A = ?A' - {a}" by blast
wenzelm@63612
   883
  moreover from assms have "\<not> finite ?A'" by auto
blanchet@55020
   884
  ultimately obtain f where "bij_betw f ?A' A"
wenzelm@63612
   885
    using infinite_imp_bij_betw[of ?A' a] by auto
wenzelm@63612
   886
  then have "bij_betw (inv_into ?A' f) A ?A'" by (rule bij_betw_inv_into)
wenzelm@63612
   887
  then show ?thesis by auto
blanchet@55020
   888
qed
blanchet@55020
   889
wenzelm@63612
   890
lemma bij_betw_inv_into_left: "bij_betw f A A' \<Longrightarrow> a \<in> A \<Longrightarrow> inv_into A f (f a) = a"
wenzelm@63612
   891
  unfolding bij_betw_def by clarify (rule inv_into_f_f)
blanchet@55020
   892
wenzelm@63612
   893
lemma bij_betw_inv_into_right: "bij_betw f A A' \<Longrightarrow> a' \<in> A' \<Longrightarrow> f (inv_into A f a') = a'"
wenzelm@63612
   894
  unfolding bij_betw_def using f_inv_into_f by force
blanchet@55020
   895
blanchet@55020
   896
lemma bij_betw_inv_into_subset:
wenzelm@63612
   897
  "bij_betw f A A' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw (inv_into A f) B' B"
wenzelm@63612
   898
  by (auto simp: bij_betw_def intro: inj_on_inv_into)
blanchet@55020
   899
blanchet@55020
   900
wenzelm@60758
   901
subsection \<open>Specification package -- Hilbertized version\<close>
wenzelm@17893
   902
wenzelm@63612
   903
lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c"
wenzelm@17893
   904
  by (simp only: someI_ex)
wenzelm@17893
   905
wenzelm@69605
   906
ML_file \<open>Tools/choice_specification.ML\<close>
skalberg@14115
   907
eberlm@67829
   908
subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close>
eberlm@67829
   909
eberlm@67829
   910
context complete_distrib_lattice
eberlm@67829
   911
begin
haftmann@69479
   912
haftmann@69479
   913
lemma Sup_Inf: "\<Squnion> (Inf ` A) = \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})"
eberlm@67829
   914
proof (rule antisym)
haftmann@69479
   915
  show "\<Squnion> (Inf ` A) \<le> \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})"
eberlm@67829
   916
    apply (rule Sup_least, rule INF_greatest)
eberlm@67829
   917
    using Inf_lower2 Sup_upper by auto
eberlm@67829
   918
next
haftmann@69479
   919
  show "\<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B}) \<le> \<Squnion> (Inf ` A)"
eberlm@67951
   920
  proof (simp add:  Inf_Sup, rule SUP_least, simp, safe)
eberlm@67829
   921
    fix f
eberlm@67829
   922
    assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
eberlm@67829
   923
    from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
eberlm@67829
   924
      by auto
haftmann@69275
   925
    show "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> \<Squnion>(Inf ` A)"
haftmann@69275
   926
    proof (cases "\<exists> Z \<in> A . \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z")
eberlm@67829
   927
      case True
haftmann@69275
   928
      from this obtain Z where [simp]: "Z \<in> A" and A: "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z"
eberlm@67829
   929
        by blast
haftmann@69275
   930
      have B: "... \<le> \<Squnion>(Inf ` A)"
eberlm@67829
   931
        by (simp add: SUP_upper)
eberlm@67829
   932
      from A and B show ?thesis
eberlm@67951
   933
        by simp
eberlm@67829
   934
    next
eberlm@67829
   935
      case False
haftmann@69275
   936
      from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x"
eberlm@67829
   937
        using Inf_greatest by blast
haftmann@69275
   938
      define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x)"
eberlm@67829
   939
      have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
eberlm@67829
   940
        using X by (simp add: F_def, rule someI2_ex, auto)
haftmann@69275
   941
      have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Y"
eberlm@67829
   942
        using X by (simp add: F_def, rule someI2_ex, auto)
eberlm@67829
   943
      from C and B obtain  Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z"
eberlm@67829
   944
        by blast
haftmann@69275
   945
      from E and D have W: "\<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Z"
eberlm@67829
   946
        by simp
haftmann@69275
   947
      have "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> f (F ` A)"
eberlm@67951
   948
        apply (rule INF_lower)
eberlm@67951
   949
        using C by blast
eberlm@67829
   950
      from this and W and Y show ?thesis
eberlm@67829
   951
        by simp
eberlm@67829
   952
    qed
eberlm@67829
   953
  qed
eberlm@67829
   954
qed
eberlm@67829
   955
  
eberlm@67829
   956
lemma dual_complete_distrib_lattice:
eberlm@67829
   957
  "class.complete_distrib_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>"
eberlm@67829
   958
  apply (rule class.complete_distrib_lattice.intro)
eberlm@67829
   959
   apply (fact dual_complete_lattice)
eberlm@67829
   960
  by (simp add: class.complete_distrib_lattice_axioms_def Sup_Inf)
eberlm@67829
   961
haftmann@68802
   962
lemma sup_Inf: "a \<squnion> \<Sqinter>B = \<Sqinter>((\<squnion>) a ` B)"
eberlm@67829
   963
proof (rule antisym)
haftmann@68802
   964
  show "a \<squnion> \<Sqinter>B \<le> \<Sqinter>((\<squnion>) a ` B)"
eberlm@67951
   965
    apply (rule INF_greatest)
eberlm@67951
   966
    using Inf_lower sup.mono by fastforce
eberlm@67829
   967
next
haftmann@68802
   968
  have "\<Sqinter>((\<squnion>) a ` B) \<le> \<Sqinter>(Sup ` {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B})"
eberlm@67829
   969
    by (rule INF_greatest, auto simp add: INF_lower)
haftmann@69275
   970
  also have "... = \<Squnion>(Inf ` {{a}, B})"
eberlm@67951
   971
    by (unfold Sup_Inf, simp)
haftmann@68802
   972
  finally show "\<Sqinter>((\<squnion>) a ` B) \<le> a \<squnion> \<Sqinter>B"
eberlm@67829
   973
    by simp
eberlm@67829
   974
qed
eberlm@67829
   975
haftmann@68802
   976
lemma inf_Sup: "a \<sqinter> \<Squnion>B = \<Squnion>((\<sqinter>) a ` B)"
eberlm@67829
   977
  using dual_complete_distrib_lattice
eberlm@67829
   978
  by (rule complete_distrib_lattice.sup_Inf)
eberlm@67829
   979
haftmann@69479
   980
lemma INF_SUP: "(\<Sqinter>y. \<Squnion>x. P x y) = (\<Squnion>f. \<Sqinter>x. P (f x) x)"
eberlm@67829
   981
proof (rule antisym)
eberlm@67829
   982
  show "(SUP x. INF y. P (x y) y) \<le> (INF y. SUP x. P x y)"
eberlm@67829
   983
    by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
eberlm@67829
   984
next
eberlm@67829
   985
  have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \<le> ?B")
eberlm@67951
   986
  proof (rule INF_greatest, clarsimp)
eberlm@67829
   987
    fix y
eberlm@67829
   988
    have "?A \<le> (SUP x. P x y)"
eberlm@67829
   989
      by (rule INF_lower, simp)
eberlm@67829
   990
    also have "... \<le> Sup {uu. \<exists>x. uu = P x y}"
eberlm@67829
   991
      by (simp add: full_SetCompr_eq)
eberlm@67829
   992
    finally show "?A \<le> Sup {uu. \<exists>x. uu = P x y}"
eberlm@67829
   993
      by simp
eberlm@67829
   994
  qed
eberlm@67829
   995
  also have "... \<le>  (SUP x. INF y. P (x y) y)"
eberlm@67951
   996
  proof (subst Inf_Sup, rule SUP_least, clarsimp)
eberlm@67829
   997
    fix f
eberlm@67829
   998
    assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y}) \<longrightarrow> f Y \<in> Y"
eberlm@67829
   999
      
haftmann@68802
  1000
    have " \<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le>
haftmann@68802
  1001
      (\<Sqinter>y. P (SOME x. f {P x y |x. True} = P x y) y)"
eberlm@67829
  1002
    proof (rule INF_greatest, clarsimp)
eberlm@67829
  1003
      fix y
haftmann@68802
  1004
        have "(INF x\<in>{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> f {uu. \<exists>x. uu = P x y}"
eberlm@67951
  1005
          by (rule INF_lower, blast)
eberlm@67829
  1006
        also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
eberlm@67951
  1007
          apply (rule someI2_ex)
eberlm@67951
  1008
          using A by auto
haftmann@68802
  1009
        finally show "\<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le>
haftmann@68802
  1010
          P (SOME x. f {uu. \<exists>x. uu = P x y} = P x y) y"
eberlm@67829
  1011
          by simp
eberlm@67829
  1012
      qed
eberlm@67829
  1013
      also have "... \<le> (SUP x. INF y. P (x y) y)"
eberlm@67829
  1014
        by (rule SUP_upper, simp)
haftmann@68802
  1015
      finally show "\<Sqinter>(f ` {uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}) \<le> (\<Squnion>x. \<Sqinter>y. P (x y) y)"
eberlm@67829
  1016
        by simp
eberlm@67829
  1017
    qed
eberlm@67829
  1018
  finally show "(INF y. SUP x. P x y) \<le> (SUP x. INF y. P (x y) y)"
eberlm@67829
  1019
    by simp
eberlm@67829
  1020
qed
eberlm@67829
  1021
haftmann@69478
  1022
lemma INF_SUP_set: "(\<Sqinter>B\<in>A. \<Squnion>(g ` B)) = (\<Squnion>B\<in>{f ` A |f. \<forall>C\<in>A. f C \<in> C}. \<Sqinter>(g ` B))"
eberlm@67829
  1023
proof (rule antisym)
haftmann@69478
  1024
  have "\<Sqinter> ((g \<circ> f) ` A) \<le> \<Squnion> (g ` B)" if "\<And>B. B \<in> A \<Longrightarrow> f B \<in> B" and "B \<in> A"
haftmann@69478
  1025
    for f and B
haftmann@69478
  1026
    using that by (auto intro: SUP_upper2 INF_lower2)
haftmann@69478
  1027
  then show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
haftmann@69861
  1028
    by (auto intro!: SUP_least INF_greatest simp add: image_comp)
eberlm@67829
  1029
next
eberlm@67829
  1030
  show "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
eberlm@67829
  1031
  proof (cases "{} \<in> A")
eberlm@67829
  1032
    case True
eberlm@67829
  1033
    then show ?thesis 
haftmann@69478
  1034
      by (rule INF_lower2) simp_all
eberlm@67829
  1035
  next
eberlm@67829
  1036
    case False
haftmann@69478
  1037
    have *: "\<And>f B. B \<in> A \<Longrightarrow> f B \<in> B \<Longrightarrow>
haftmann@69478
  1038
      (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) \<le> g (f B)"
haftmann@69478
  1039
      by (rule INF_lower2, auto)
haftmann@69478
  1040
    have **: "\<And>f B. B \<in> A \<Longrightarrow> f B \<notin> B \<Longrightarrow>
haftmann@69478
  1041
      (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) \<le> g (SOME x. x \<in> B)"
eberlm@67951
  1042
      by (rule INF_lower2, auto)
haftmann@69478
  1043
    have ****: "\<And>f B. B \<in> A \<Longrightarrow>
haftmann@69478
  1044
      (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>)
haftmann@69478
  1045
        \<le> (if f B \<in> B then g (f B) else g (SOME x. x \<in> B))"
haftmann@69478
  1046
      by (rule INF_lower2) auto
haftmann@69478
  1047
    have ***: "\<And>x. (\<Sqinter>B. if B \<in> A then if x B \<in> B then g (x B) else \<bottom> else \<top>)
haftmann@69478
  1048
        \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
eberlm@67951
  1049
    proof -
eberlm@67951
  1050
      fix x
eberlm@67951
  1051
      define F where "F = (\<lambda> (y::'b set) . if x y \<in> y then x y else (SOME x . x \<in>y))"
eberlm@67951
  1052
      have B: "(\<forall>Y\<in>A. F Y \<in> Y)"
eberlm@67951
  1053
        using False some_in_eq F_def by auto
eberlm@67951
  1054
      have A: "F ` A \<in> {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
eberlm@67951
  1055
        using B by blast
eberlm@67951
  1056
      show "(\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
eberlm@67951
  1057
        using A apply (rule SUP_upper2)
haftmann@69478
  1058
        apply (rule INF_greatest)
haftmann@69768
  1059
        using * **
haftmann@69768
  1060
        apply (auto simp add: F_def)
haftmann@69478
  1061
        done
eberlm@67951
  1062
    qed
eberlm@67951
  1063
eberlm@67951
  1064
    {fix x
eberlm@67951
  1065
      have "(\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
eberlm@67951
  1066
      proof (cases "x \<in> A")
eberlm@67951
  1067
        case True
eberlm@67951
  1068
        then show ?thesis
haftmann@69768
  1069
          apply (rule INF_lower2)
haftmann@69768
  1070
          apply (rule SUP_least)
haftmann@69768
  1071
          apply (rule SUP_upper2)
haftmann@69768
  1072
           apply auto
haftmann@69768
  1073
          done
eberlm@67951
  1074
      next
eberlm@67951
  1075
        case False
eberlm@67951
  1076
        then show ?thesis by simp
eberlm@67951
  1077
      qed
eberlm@67951
  1078
    }
eberlm@67829
  1079
    from this have "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Sqinter>x. \<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
eberlm@67829
  1080
      by (rule INF_greatest)
eberlm@67829
  1081
    also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
haftmann@69768
  1082
      by (simp only: INF_SUP)
eberlm@67829
  1083
    also have "... \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
haftmann@69768
  1084
      apply (rule SUP_least)
haftmann@69768
  1085
      using *** apply simp
haftmann@69768
  1086
      done
eberlm@67829
  1087
    finally show ?thesis by simp
eberlm@67829
  1088
  qed
eberlm@67829
  1089
qed
eberlm@67829
  1090
haftmann@69479
  1091
lemma SUP_INF: "(\<Squnion>y. \<Sqinter>x. P x y) = (\<Sqinter>x. \<Squnion>y. P (x y) y)"
eberlm@67829
  1092
  using dual_complete_distrib_lattice
eberlm@67829
  1093
  by (rule complete_distrib_lattice.INF_SUP)
eberlm@67829
  1094
haftmann@69479
  1095
lemma SUP_INF_set: "(\<Squnion>x\<in>A. \<Sqinter> (g ` x)) = (\<Sqinter>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Squnion> (g ` x))"
eberlm@67829
  1096
  using dual_complete_distrib_lattice
eberlm@67829
  1097
  by (rule complete_distrib_lattice.INF_SUP_set)
eberlm@67829
  1098
paulson@11451
  1099
end
eberlm@67829
  1100
eberlm@67829
  1101
(*properties of the former complete_distrib_lattice*)
eberlm@67829
  1102
context complete_distrib_lattice
eberlm@67829
  1103
begin
eberlm@67829
  1104
eberlm@67829
  1105
lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
haftmann@69861
  1106
  by (simp add: sup_Inf image_comp)
eberlm@67829
  1107
eberlm@67829
  1108
lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
haftmann@69861
  1109
  by (simp add: inf_Sup image_comp)
eberlm@67829
  1110
eberlm@67829
  1111
lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
eberlm@67829
  1112
  by (simp add: sup_Inf sup_commute)
eberlm@67829
  1113
eberlm@67829
  1114
lemma Sup_inf: "\<Squnion>B \<sqinter> a = (\<Squnion>b\<in>B. b \<sqinter> a)"
eberlm@67829
  1115
  by (simp add: inf_Sup inf_commute)
eberlm@67829
  1116
eberlm@67829
  1117
lemma INF_sup: "(\<Sqinter>b\<in>B. f b) \<squnion> a = (\<Sqinter>b\<in>B. f b \<squnion> a)"
eberlm@67829
  1118
  by (simp add: sup_INF sup_commute)
eberlm@67829
  1119
eberlm@67829
  1120
lemma SUP_inf: "(\<Squnion>b\<in>B. f b) \<sqinter> a = (\<Squnion>b\<in>B. f b \<sqinter> a)"
eberlm@67829
  1121
  by (simp add: inf_SUP inf_commute)
eberlm@67829
  1122
eberlm@67829
  1123
lemma Inf_sup_eq_top_iff: "(\<Sqinter>B \<squnion> a = \<top>) \<longleftrightarrow> (\<forall>b\<in>B. b \<squnion> a = \<top>)"
eberlm@67829
  1124
  by (simp only: Inf_sup INF_top_conv)
eberlm@67829
  1125
eberlm@67829
  1126
lemma Sup_inf_eq_bot_iff: "(\<Squnion>B \<sqinter> a = \<bottom>) \<longleftrightarrow> (\<forall>b\<in>B. b \<sqinter> a = \<bottom>)"
eberlm@67829
  1127
  by (simp only: Sup_inf SUP_bot_conv)
eberlm@67829
  1128
eberlm@67829
  1129
lemma INF_sup_distrib2: "(\<Sqinter>a\<in>A. f a) \<squnion> (\<Sqinter>b\<in>B. g b) = (\<Sqinter>a\<in>A. \<Sqinter>b\<in>B. f a \<squnion> g b)"
eberlm@67829
  1130
  by (subst INF_commute) (simp add: sup_INF INF_sup)
eberlm@67829
  1131
eberlm@67829
  1132
lemma SUP_inf_distrib2: "(\<Squnion>a\<in>A. f a) \<sqinter> (\<Squnion>b\<in>B. g b) = (\<Squnion>a\<in>A. \<Squnion>b\<in>B. f a \<sqinter> g b)"
eberlm@67829
  1133
  by (subst SUP_commute) (simp add: inf_SUP SUP_inf)
eberlm@67829
  1134
eberlm@67829
  1135
end
eberlm@67829
  1136
eberlm@67829
  1137
context complete_boolean_algebra
eberlm@67829
  1138
begin
eberlm@67829
  1139
eberlm@67829
  1140
lemma dual_complete_boolean_algebra:
eberlm@67829
  1141
  "class.complete_boolean_algebra Sup Inf sup (\<ge>) (>) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
eberlm@67829
  1142
  by (rule class.complete_boolean_algebra.intro,
eberlm@67829
  1143
      rule dual_complete_distrib_lattice,
eberlm@67829
  1144
      rule dual_boolean_algebra)
eberlm@67829
  1145
end
eberlm@67829
  1146
eberlm@67829
  1147
eberlm@67829
  1148
haftmann@68802
  1149
instantiation set :: (type) complete_distrib_lattice
eberlm@67829
  1150
begin
eberlm@67829
  1151
instance proof (standard, clarsimp)
eberlm@67829
  1152
  fix A :: "(('a set) set) set"
eberlm@67829
  1153
  fix x::'a
eberlm@67829
  1154
  define F where "F = (\<lambda> Y . (SOME X . (Y \<in> A \<and> X \<in> Y \<and> x \<in> X)))"
eberlm@67829
  1155
  assume A: "\<forall>xa\<in>A. \<exists>X\<in>xa. x \<in> X"
eberlm@67829
  1156
    
eberlm@67829
  1157
  from this have B: " (\<forall>xa \<in> F ` A. x \<in> xa)"
eberlm@67829
  1158
    apply (safe, simp add: F_def)
eberlm@67829
  1159
    by (rule someI2_ex, auto)
eberlm@67951
  1160
eberlm@67951
  1161
  have C: "(\<forall>Y\<in>A. F Y \<in> Y)"
eberlm@67951
  1162
    apply (simp  add: F_def, safe)
eberlm@67951
  1163
    apply (rule someI2_ex)
eberlm@67951
  1164
    using A by auto
eberlm@67951
  1165
eberlm@67829
  1166
  have "(\<exists>f. F ` A  = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))"
eberlm@67951
  1167
    using C by blast
eberlm@67829
  1168
    
eberlm@67829
  1169
  from B and this show "\<exists>X. (\<exists>f. X = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>xa\<in>X. x \<in> xa)"
eberlm@67829
  1170
    by auto
eberlm@67829
  1171
qed
eberlm@67829
  1172
end
eberlm@67829
  1173
haftmann@68802
  1174
instance set :: (type) complete_boolean_algebra ..
eberlm@67829
  1175
eberlm@67829
  1176
instantiation "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
eberlm@67829
  1177
begin
haftmann@69861
  1178
instance by standard (simp add: le_fun_def INF_SUP_set image_comp)
eberlm@67829
  1179
end
eberlm@67829
  1180
eberlm@67829
  1181
instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
eberlm@67829
  1182
eberlm@67829
  1183
context complete_linorder
eberlm@67829
  1184
begin
eberlm@67829
  1185
  
eberlm@67829
  1186
subclass complete_distrib_lattice
eberlm@67829
  1187
proof (standard, rule ccontr)
eberlm@67829
  1188
  fix A
haftmann@69275
  1189
  assume "\<not> \<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
haftmann@69275
  1190
  then have C: "\<Sqinter>(Sup ` A) > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
haftmann@69275
  1191
    by (simp add: not_le)
haftmann@69275
  1192
  show False
haftmann@69275
  1193
    proof (cases "\<exists> z . \<Sqinter>(Sup ` A) > z \<and> z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})")
eberlm@67829
  1194
      case True
haftmann@69275
  1195
      from this obtain z where A: "z < \<Sqinter>(Sup ` A)" and X: "z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
eberlm@67829
  1196
        by blast
eberlm@67829
  1197
          
eberlm@67829
  1198
      from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y"
eberlm@67829
  1199
        by (simp add: less_INF_D)
eberlm@67829
  1200
    
eberlm@67829
  1201
      from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . z < k"
eberlm@67829
  1202
        using local.less_Sup_iff by blast
eberlm@67829
  1203
          
eberlm@67829
  1204
      define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)"
eberlm@67829
  1205
        
eberlm@67829
  1206
      have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y"
eberlm@67951
  1207
        using B apply (simp add: F_def)
eberlm@67951
  1208
        by (rule someI2_ex, auto)
eberlm@67951
  1209
eberlm@67829
  1210
    
eberlm@67829
  1211
      have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
eberlm@67951
  1212
        using B apply (simp add: F_def)
eberlm@67951
  1213
        by (rule someI2_ex, auto)
eberlm@67829
  1214
    
eberlm@67829
  1215
      have "z \<le> Inf (F ` A)"
eberlm@67829
  1216
        by (simp add: D local.INF_greatest local.order.strict_implies_order)
eberlm@67829
  1217
    
haftmann@69275
  1218
      also have "... \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
eberlm@67829
  1219
        apply (rule SUP_upper, safe)
eberlm@67829
  1220
        using E by blast
haftmann@69275
  1221
      finally have "z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
eberlm@67829
  1222
        by simp
eberlm@67829
  1223
          
eberlm@67829
  1224
      from X and this show ?thesis
eberlm@67829
  1225
        using local.not_less by blast
eberlm@67829
  1226
    next
eberlm@67829
  1227
      case False
haftmann@69275
  1228
      from this have A: "\<And> z . \<Sqinter>(Sup ` A) \<le> z \<or> z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
eberlm@67829
  1229
        using local.le_less_linear by blast
haftmann@69275
  1230
haftmann@69275
  1231
      from C have "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < Sup Y"
eberlm@67829
  1232
        by (simp add: less_INF_D)
haftmann@69275
  1233
haftmann@69275
  1234
      from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k"
eberlm@67829
  1235
        using local.less_Sup_iff by blast
eberlm@67829
  1236
          
haftmann@69275
  1237
      define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k)"
haftmann@69275
  1238
haftmann@69275
  1239
      have D: "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < F Y"
eberlm@67951
  1240
        using B apply (simp add: F_def)
eberlm@67951
  1241
        by (rule someI2_ex, auto)
eberlm@67829
  1242
    
eberlm@67829
  1243
      have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
eberlm@67951
  1244
        using B apply (simp add: F_def)
eberlm@67951
  1245
        by (rule someI2_ex, auto)
eberlm@67829
  1246
          
haftmann@69275
  1247
      have "\<And> Y . Y \<in> A \<Longrightarrow> \<Sqinter>(Sup ` A) \<le> F Y"
eberlm@67829
  1248
        using D False local.leI by blast
eberlm@67829
  1249
         
haftmann@69275
  1250
      from this have "\<Sqinter>(Sup ` A) \<le> Inf (F ` A)"
eberlm@67829
  1251
        by (simp add: local.INF_greatest)
eberlm@67829
  1252
          
haftmann@69275
  1253
      also have "Inf (F ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
eberlm@67829
  1254
        apply (rule SUP_upper, safe)
eberlm@67829
  1255
        using E by blast
haftmann@69275
  1256
haftmann@69275
  1257
      finally have "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
eberlm@67829
  1258
        by simp
eberlm@67829
  1259
        
eberlm@67829
  1260
      from C and this show ?thesis
eberlm@67951
  1261
        using not_less by blast
eberlm@67829
  1262
    qed
eberlm@67829
  1263
  qed
eberlm@67829
  1264
end
eberlm@67829
  1265
eberlm@67829
  1266
eberlm@67829
  1267
eberlm@67829
  1268
end