src/HOL/Lattices_Big.thy
author paulson <lp15@cam.ac.uk>
Mon Apr 09 15:20:11 2018 +0100 (17 months ago)
changeset 67969 83c8cafdebe8
parent 67613 ce654b0e6d69
child 68779 78d9b1783378
permissions -rw-r--r--
Syntax for the special cases Min(A`I) and Max (A`I)
haftmann@54744
     1
(*  Title:      HOL/Lattices_Big.thy
haftmann@54744
     2
    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
haftmann@54744
     3
                with contributions by Jeremy Avigad
haftmann@54744
     4
*)
haftmann@54744
     5
wenzelm@60758
     6
section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
haftmann@54744
     7
haftmann@54744
     8
theory Lattices_Big
blanchet@66364
     9
  imports Option
haftmann@54744
    10
begin
haftmann@54744
    11
wenzelm@60758
    12
subsection \<open>Generic lattice operations over a set\<close>
haftmann@54744
    13
wenzelm@60758
    14
subsubsection \<open>Without neutral element\<close>
haftmann@54744
    15
haftmann@54744
    16
locale semilattice_set = semilattice
haftmann@54744
    17
begin
haftmann@54744
    18
haftmann@54744
    19
interpretation comp_fun_idem f
wenzelm@61169
    20
  by standard (simp_all add: fun_eq_iff left_commute)
haftmann@54744
    21
haftmann@54744
    22
definition F :: "'a set \<Rightarrow> 'a"
haftmann@54744
    23
where
haftmann@54744
    24
  eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)) None A)"
haftmann@54744
    25
haftmann@54744
    26
lemma eq_fold:
haftmann@54744
    27
  assumes "finite A"
haftmann@54744
    28
  shows "F (insert x A) = Finite_Set.fold f x A"
haftmann@54744
    29
proof (rule sym)
haftmann@54744
    30
  let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
haftmann@54744
    31
  interpret comp_fun_idem "?f"
wenzelm@61169
    32
    by standard (simp_all add: fun_eq_iff commute left_commute split: option.split)
haftmann@54744
    33
  from assms show "Finite_Set.fold f x A = F (insert x A)"
haftmann@54744
    34
  proof induct
haftmann@54744
    35
    case empty then show ?case by (simp add: eq_fold')
haftmann@54744
    36
  next
haftmann@54744
    37
    case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
haftmann@54744
    38
  qed
haftmann@54744
    39
qed
haftmann@54744
    40
haftmann@54744
    41
lemma singleton [simp]:
haftmann@54744
    42
  "F {x} = x"
haftmann@54744
    43
  by (simp add: eq_fold)
haftmann@54744
    44
haftmann@54744
    45
lemma insert_not_elem:
haftmann@54744
    46
  assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
haftmann@63290
    47
  shows "F (insert x A) = x \<^bold>* F A"
haftmann@54744
    48
proof -
wenzelm@60758
    49
  from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast
haftmann@54744
    50
  then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
wenzelm@60758
    51
  with \<open>finite A\<close> and \<open>x \<notin> A\<close>
haftmann@54744
    52
    have "finite (insert x B)" and "b \<notin> insert x B" by auto
haftmann@63290
    53
  then have "F (insert b (insert x B)) = x \<^bold>* F (insert b B)"
haftmann@54744
    54
    by (simp add: eq_fold)
haftmann@54744
    55
  then show ?thesis by (simp add: * insert_commute)
haftmann@54744
    56
qed
haftmann@54744
    57
haftmann@54744
    58
lemma in_idem:
haftmann@54744
    59
  assumes "finite A" and "x \<in> A"
haftmann@63290
    60
  shows "x \<^bold>* F A = F A"
haftmann@54744
    61
proof -
haftmann@54744
    62
  from assms have "A \<noteq> {}" by auto
wenzelm@60758
    63
  with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
haftmann@54744
    64
    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
haftmann@54744
    65
qed
haftmann@54744
    66
haftmann@54744
    67
lemma insert [simp]:
haftmann@54744
    68
  assumes "finite A" and "A \<noteq> {}"
haftmann@63290
    69
  shows "F (insert x A) = x \<^bold>* F A"
haftmann@54744
    70
  using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
haftmann@54744
    71
haftmann@54744
    72
lemma union:
haftmann@54744
    73
  assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
haftmann@63290
    74
  shows "F (A \<union> B) = F A \<^bold>* F B"
haftmann@54744
    75
  using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
haftmann@54744
    76
haftmann@54744
    77
lemma remove:
haftmann@54744
    78
  assumes "finite A" and "x \<in> A"
haftmann@63290
    79
  shows "F A = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
haftmann@54744
    80
proof -
haftmann@54744
    81
  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
haftmann@54744
    82
  with assms show ?thesis by simp
haftmann@54744
    83
qed
haftmann@54744
    84
haftmann@54744
    85
lemma insert_remove:
haftmann@54744
    86
  assumes "finite A"
haftmann@63290
    87
  shows "F (insert x A) = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
haftmann@54744
    88
  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
haftmann@54744
    89
haftmann@54744
    90
lemma subset:
haftmann@54744
    91
  assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
haftmann@63290
    92
  shows "F B \<^bold>* F A = F A"
haftmann@54744
    93
proof -
haftmann@54744
    94
  from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
haftmann@54744
    95
  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
haftmann@54744
    96
qed
haftmann@54744
    97
haftmann@54744
    98
lemma closed:
haftmann@63290
    99
  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
haftmann@54744
   100
  shows "F A \<in> A"
wenzelm@60758
   101
using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
haftmann@54744
   102
  case singleton then show ?case by simp
haftmann@54744
   103
next
haftmann@54744
   104
  case insert with elem show ?case by force
haftmann@54744
   105
qed
haftmann@54744
   106
haftmann@54744
   107
lemma hom_commute:
haftmann@63290
   108
  assumes hom: "\<And>x y. h (x \<^bold>* y) = h x \<^bold>* h y"
haftmann@54744
   109
  and N: "finite N" "N \<noteq> {}"
haftmann@54744
   110
  shows "h (F N) = F (h ` N)"
haftmann@54744
   111
using N proof (induct rule: finite_ne_induct)
haftmann@54744
   112
  case singleton thus ?case by simp
haftmann@54744
   113
next
haftmann@54744
   114
  case (insert n N)
haftmann@63290
   115
  then have "h (F (insert n N)) = h (n \<^bold>* F N)" by simp
haftmann@63290
   116
  also have "\<dots> = h n \<^bold>* h (F N)" by (rule hom)
haftmann@54744
   117
  also have "h (F N) = F (h ` N)" by (rule insert)
haftmann@63290
   118
  also have "h n \<^bold>* \<dots> = F (insert (h n) (h ` N))"
haftmann@54744
   119
    using insert by simp
haftmann@54744
   120
  also have "insert (h n) (h ` N) = h ` insert n N" by simp
haftmann@54744
   121
  finally show ?case .
haftmann@54744
   122
qed
haftmann@54744
   123
hoelzl@56993
   124
lemma infinite: "\<not> finite A \<Longrightarrow> F A = the None"
hoelzl@56993
   125
  unfolding eq_fold' by (cases "finite (UNIV::'a set)") (auto intro: finite_subset fold_infinite)
hoelzl@56993
   126
haftmann@54744
   127
end
haftmann@54744
   128
haftmann@54745
   129
locale semilattice_order_set = binary?: semilattice_order + semilattice_set
haftmann@54744
   130
begin
haftmann@54744
   131
haftmann@54744
   132
lemma bounded_iff:
haftmann@54744
   133
  assumes "finite A" and "A \<noteq> {}"
haftmann@63290
   134
  shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
haftmann@67525
   135
  using assms by (induct rule: finite_ne_induct) simp_all
haftmann@54744
   136
haftmann@54744
   137
lemma boundedI:
haftmann@54744
   138
  assumes "finite A"
haftmann@54744
   139
  assumes "A \<noteq> {}"
haftmann@63290
   140
  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
haftmann@63290
   141
  shows "x \<^bold>\<le> F A"
haftmann@54744
   142
  using assms by (simp add: bounded_iff)
haftmann@54744
   143
haftmann@54744
   144
lemma boundedE:
haftmann@63290
   145
  assumes "finite A" and "A \<noteq> {}" and "x \<^bold>\<le> F A"
haftmann@63290
   146
  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
haftmann@54744
   147
  using assms by (simp add: bounded_iff)
haftmann@54744
   148
haftmann@54744
   149
lemma coboundedI:
haftmann@54744
   150
  assumes "finite A"
haftmann@54744
   151
    and "a \<in> A"
haftmann@63290
   152
  shows "F A \<^bold>\<le> a"
haftmann@54744
   153
proof -
haftmann@54744
   154
  from assms have "A \<noteq> {}" by auto
wenzelm@60758
   155
  from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
haftmann@54744
   156
  proof (induct rule: finite_ne_induct)
haftmann@54744
   157
    case singleton thus ?case by (simp add: refl)
haftmann@54744
   158
  next
haftmann@54744
   159
    case (insert x B)
haftmann@54744
   160
    from insert have "a = x \<or> a \<in> B" by simp
haftmann@54744
   161
    then show ?case using insert by (auto intro: coboundedI2)
haftmann@54744
   162
  qed
haftmann@54744
   163
qed
haftmann@54744
   164
haftmann@67525
   165
lemma subset_imp:
haftmann@54744
   166
  assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
haftmann@63290
   167
  shows "F B \<^bold>\<le> F A"
haftmann@54744
   168
proof (cases "A = B")
haftmann@54744
   169
  case True then show ?thesis by (simp add: refl)
haftmann@54744
   170
next
haftmann@54744
   171
  case False
wenzelm@60758
   172
  have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
haftmann@54744
   173
  then have "F B = F (A \<union> (B - A))" by simp
haftmann@63290
   174
  also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
haftmann@63290
   175
  also have "\<dots> \<^bold>\<le> F A" by simp
haftmann@54744
   176
  finally show ?thesis .
haftmann@54744
   177
qed
haftmann@54744
   178
haftmann@54744
   179
end
haftmann@54744
   180
haftmann@54744
   181
wenzelm@60758
   182
subsubsection \<open>With neutral element\<close>
haftmann@54744
   183
haftmann@54744
   184
locale semilattice_neutr_set = semilattice_neutr
haftmann@54744
   185
begin
haftmann@54744
   186
haftmann@54744
   187
interpretation comp_fun_idem f
wenzelm@61169
   188
  by standard (simp_all add: fun_eq_iff left_commute)
haftmann@54744
   189
haftmann@54744
   190
definition F :: "'a set \<Rightarrow> 'a"
haftmann@54744
   191
where
haftmann@63290
   192
  eq_fold: "F A = Finite_Set.fold f \<^bold>1 A"
haftmann@54744
   193
haftmann@54744
   194
lemma infinite [simp]:
haftmann@63290
   195
  "\<not> finite A \<Longrightarrow> F A = \<^bold>1"
haftmann@54744
   196
  by (simp add: eq_fold)
haftmann@54744
   197
haftmann@54744
   198
lemma empty [simp]:
haftmann@63290
   199
  "F {} = \<^bold>1"
haftmann@54744
   200
  by (simp add: eq_fold)
haftmann@54744
   201
haftmann@54744
   202
lemma insert [simp]:
haftmann@54744
   203
  assumes "finite A"
haftmann@63290
   204
  shows "F (insert x A) = x \<^bold>* F A"
haftmann@54744
   205
  using assms by (simp add: eq_fold)
haftmann@54744
   206
haftmann@54744
   207
lemma in_idem:
haftmann@54744
   208
  assumes "finite A" and "x \<in> A"
haftmann@63290
   209
  shows "x \<^bold>* F A = F A"
haftmann@54744
   210
proof -
haftmann@54744
   211
  from assms have "A \<noteq> {}" by auto
wenzelm@60758
   212
  with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
haftmann@54744
   213
    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
haftmann@54744
   214
qed
haftmann@54744
   215
haftmann@54744
   216
lemma union:
haftmann@54744
   217
  assumes "finite A" and "finite B"
haftmann@63290
   218
  shows "F (A \<union> B) = F A \<^bold>* F B"
haftmann@54744
   219
  using assms by (induct A) (simp_all add: ac_simps)
haftmann@54744
   220
haftmann@54744
   221
lemma remove:
haftmann@54744
   222
  assumes "finite A" and "x \<in> A"
haftmann@63290
   223
  shows "F A = x \<^bold>* F (A - {x})"
haftmann@54744
   224
proof -
haftmann@54744
   225
  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
haftmann@54744
   226
  with assms show ?thesis by simp
haftmann@54744
   227
qed
haftmann@54744
   228
haftmann@54744
   229
lemma insert_remove:
haftmann@54744
   230
  assumes "finite A"
haftmann@63290
   231
  shows "F (insert x A) = x \<^bold>* F (A - {x})"
haftmann@54744
   232
  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
haftmann@54744
   233
haftmann@54744
   234
lemma subset:
haftmann@54744
   235
  assumes "finite A" and "B \<subseteq> A"
haftmann@63290
   236
  shows "F B \<^bold>* F A = F A"
haftmann@54744
   237
proof -
haftmann@54744
   238
  from assms have "finite B" by (auto dest: finite_subset)
haftmann@54744
   239
  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
haftmann@54744
   240
qed
haftmann@54744
   241
haftmann@54744
   242
lemma closed:
haftmann@63290
   243
  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
haftmann@54744
   244
  shows "F A \<in> A"
wenzelm@60758
   245
using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
haftmann@54744
   246
  case singleton then show ?case by simp
haftmann@54744
   247
next
haftmann@54744
   248
  case insert with elem show ?case by force
haftmann@54744
   249
qed
haftmann@54744
   250
haftmann@54744
   251
end
haftmann@54744
   252
haftmann@54745
   253
locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
haftmann@54744
   254
begin
haftmann@54744
   255
haftmann@54744
   256
lemma bounded_iff:
haftmann@54744
   257
  assumes "finite A"
haftmann@63290
   258
  shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
haftmann@67525
   259
  using assms by (induct A) simp_all
haftmann@54744
   260
haftmann@54744
   261
lemma boundedI:
haftmann@54744
   262
  assumes "finite A"
haftmann@63290
   263
  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
haftmann@63290
   264
  shows "x \<^bold>\<le> F A"
haftmann@54744
   265
  using assms by (simp add: bounded_iff)
haftmann@54744
   266
haftmann@54744
   267
lemma boundedE:
haftmann@63290
   268
  assumes "finite A" and "x \<^bold>\<le> F A"
haftmann@63290
   269
  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
haftmann@54744
   270
  using assms by (simp add: bounded_iff)
haftmann@54744
   271
haftmann@54744
   272
lemma coboundedI:
haftmann@54744
   273
  assumes "finite A"
haftmann@54744
   274
    and "a \<in> A"
haftmann@63290
   275
  shows "F A \<^bold>\<le> a"
haftmann@54744
   276
proof -
haftmann@54744
   277
  from assms have "A \<noteq> {}" by auto
wenzelm@60758
   278
  from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
haftmann@54744
   279
  proof (induct rule: finite_ne_induct)
haftmann@54744
   280
    case singleton thus ?case by (simp add: refl)
haftmann@54744
   281
  next
haftmann@54744
   282
    case (insert x B)
haftmann@54744
   283
    from insert have "a = x \<or> a \<in> B" by simp
haftmann@54744
   284
    then show ?case using insert by (auto intro: coboundedI2)
haftmann@54744
   285
  qed
haftmann@54744
   286
qed
haftmann@54744
   287
haftmann@67525
   288
lemma subset_imp:
haftmann@54744
   289
  assumes "A \<subseteq> B" and "finite B"
haftmann@63290
   290
  shows "F B \<^bold>\<le> F A"
haftmann@54744
   291
proof (cases "A = B")
haftmann@54744
   292
  case True then show ?thesis by (simp add: refl)
haftmann@54744
   293
next
haftmann@54744
   294
  case False
wenzelm@60758
   295
  have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
haftmann@54744
   296
  then have "F B = F (A \<union> (B - A))" by simp
haftmann@63290
   297
  also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
haftmann@63290
   298
  also have "\<dots> \<^bold>\<le> F A" by simp
haftmann@54744
   299
  finally show ?thesis .
haftmann@54744
   300
qed
haftmann@54744
   301
haftmann@54744
   302
end
haftmann@54744
   303
haftmann@54744
   304
wenzelm@60758
   305
subsection \<open>Lattice operations on finite sets\<close>
haftmann@54744
   306
haftmann@54868
   307
context semilattice_inf
haftmann@54868
   308
begin
haftmann@54868
   309
wenzelm@61605
   310
sublocale Inf_fin: semilattice_order_set inf less_eq less
haftmann@61776
   311
defines
haftmann@61776
   312
  Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Inf_fin.F ..
haftmann@54744
   313
haftmann@54868
   314
end
haftmann@54868
   315
haftmann@54868
   316
context semilattice_sup
haftmann@54868
   317
begin
haftmann@54868
   318
wenzelm@61605
   319
sublocale Sup_fin: semilattice_order_set sup greater_eq greater
haftmann@61776
   320
defines
haftmann@61776
   321
  Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Sup_fin.F ..
haftmann@54744
   322
haftmann@54868
   323
end
haftmann@54868
   324
haftmann@54744
   325
wenzelm@60758
   326
subsection \<open>Infimum and Supremum over non-empty sets\<close>
haftmann@54744
   327
haftmann@54744
   328
context lattice
haftmann@54744
   329
begin
haftmann@54744
   330
haftmann@54745
   331
lemma Inf_fin_le_Sup_fin [simp]: 
haftmann@54745
   332
  assumes "finite A" and "A \<noteq> {}"
haftmann@54745
   333
  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
haftmann@54745
   334
proof -
wenzelm@60758
   335
  from \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" by blast
wenzelm@60758
   336
  with \<open>finite A\<close> have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
wenzelm@60758
   337
  moreover from \<open>finite A\<close> \<open>a \<in> A\<close> have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
haftmann@54745
   338
  ultimately show ?thesis by (rule order_trans)
haftmann@54745
   339
qed
haftmann@54744
   340
haftmann@54744
   341
lemma sup_Inf_absorb [simp]:
haftmann@54745
   342
  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
haftmann@54745
   343
  by (rule sup_absorb2) (rule Inf_fin.coboundedI)
haftmann@54744
   344
haftmann@54744
   345
lemma inf_Sup_absorb [simp]:
haftmann@54745
   346
  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
haftmann@54745
   347
  by (rule inf_absorb1) (rule Sup_fin.coboundedI)
haftmann@54744
   348
haftmann@54744
   349
end
haftmann@54744
   350
haftmann@54744
   351
context distrib_lattice
haftmann@54744
   352
begin
haftmann@54744
   353
haftmann@54744
   354
lemma sup_Inf1_distrib:
haftmann@54744
   355
  assumes "finite A"
haftmann@54744
   356
    and "A \<noteq> {}"
haftmann@54744
   357
  shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
haftmann@54744
   358
using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
haftmann@54744
   359
  (rule arg_cong [where f="Inf_fin"], blast)
haftmann@54744
   360
haftmann@54744
   361
lemma sup_Inf2_distrib:
haftmann@54744
   362
  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
haftmann@54744
   363
  shows "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B}"
haftmann@54744
   364
using A proof (induct rule: finite_ne_induct)
haftmann@54744
   365
  case singleton then show ?case
haftmann@54744
   366
    by (simp add: sup_Inf1_distrib [OF B])
haftmann@54744
   367
next
haftmann@54744
   368
  case (insert x A)
haftmann@54744
   369
  have finB: "finite {sup x b |b. b \<in> B}"
haftmann@54744
   370
    by (rule finite_surj [where f = "sup x", OF B(1)], auto)
haftmann@54744
   371
  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
haftmann@54744
   372
  proof -
haftmann@54744
   373
    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
haftmann@54744
   374
      by blast
haftmann@54744
   375
    thus ?thesis by(simp add: insert(1) B(1))
haftmann@54744
   376
  qed
haftmann@54744
   377
  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
haftmann@54744
   378
  have "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)"
haftmann@54744
   379
    using insert by simp
haftmann@54744
   380
  also have "\<dots> = inf (sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)) (sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2)
haftmann@54744
   381
  also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B})"
haftmann@54744
   382
    using insert by(simp add:sup_Inf1_distrib[OF B])
haftmann@54744
   383
  also have "\<dots> = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
haftmann@54744
   384
    (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
haftmann@54744
   385
    using B insert
haftmann@54744
   386
    by (simp add: Inf_fin.union [OF finB _ finAB ne])
haftmann@54744
   387
  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
haftmann@54744
   388
    by blast
haftmann@54744
   389
  finally show ?case .
haftmann@54744
   390
qed
haftmann@54744
   391
haftmann@54744
   392
lemma inf_Sup1_distrib:
haftmann@54744
   393
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   394
  shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
haftmann@54744
   395
using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
haftmann@54744
   396
  (rule arg_cong [where f="Sup_fin"], blast)
haftmann@54744
   397
haftmann@54744
   398
lemma inf_Sup2_distrib:
haftmann@54744
   399
  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
haftmann@54744
   400
  shows "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B}"
haftmann@54744
   401
using A proof (induct rule: finite_ne_induct)
haftmann@54744
   402
  case singleton thus ?case
haftmann@54744
   403
    by(simp add: inf_Sup1_distrib [OF B])
haftmann@54744
   404
next
haftmann@54744
   405
  case (insert x A)
haftmann@54744
   406
  have finB: "finite {inf x b |b. b \<in> B}"
haftmann@54744
   407
    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
haftmann@54744
   408
  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
haftmann@54744
   409
  proof -
haftmann@54744
   410
    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
haftmann@54744
   411
      by blast
haftmann@54744
   412
    thus ?thesis by(simp add: insert(1) B(1))
haftmann@54744
   413
  qed
haftmann@54744
   414
  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
haftmann@54744
   415
  have "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)"
haftmann@54744
   416
    using insert by simp
haftmann@54744
   417
  also have "\<dots> = sup (inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)) (inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2)
haftmann@54744
   418
  also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B})"
haftmann@54744
   419
    using insert by(simp add:inf_Sup1_distrib[OF B])
haftmann@54744
   420
  also have "\<dots> = \<Squnion>\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
haftmann@54744
   421
    (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
haftmann@54744
   422
    using B insert
haftmann@54744
   423
    by (simp add: Sup_fin.union [OF finB _ finAB ne])
haftmann@54744
   424
  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
haftmann@54744
   425
    by blast
haftmann@54744
   426
  finally show ?case .
haftmann@54744
   427
qed
haftmann@54744
   428
haftmann@54744
   429
end
haftmann@54744
   430
haftmann@54744
   431
context complete_lattice
haftmann@54744
   432
begin
haftmann@54744
   433
haftmann@54744
   434
lemma Inf_fin_Inf:
haftmann@54744
   435
  assumes "finite A" and "A \<noteq> {}"
haftmann@54868
   436
  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A"
haftmann@54744
   437
proof -
haftmann@54744
   438
  from assms obtain b B where "A = insert b B" and "finite B" by auto
haftmann@54744
   439
  then show ?thesis
haftmann@54744
   440
    by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
haftmann@54744
   441
qed
haftmann@54744
   442
haftmann@54744
   443
lemma Sup_fin_Sup:
haftmann@54744
   444
  assumes "finite A" and "A \<noteq> {}"
haftmann@54868
   445
  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A"
haftmann@54744
   446
proof -
haftmann@54744
   447
  from assms obtain b B where "A = insert b B" and "finite B" by auto
haftmann@54744
   448
  then show ?thesis
haftmann@54744
   449
    by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
haftmann@54744
   450
qed
haftmann@54744
   451
haftmann@54744
   452
end
haftmann@54744
   453
haftmann@54744
   454
wenzelm@60758
   455
subsection \<open>Minimum and Maximum over non-empty sets\<close>
haftmann@54744
   456
haftmann@54744
   457
context linorder
haftmann@54744
   458
begin
haftmann@54744
   459
wenzelm@61605
   460
sublocale Min: semilattice_order_set min less_eq less
wenzelm@61605
   461
  + Max: semilattice_order_set max greater_eq greater
haftmann@61776
   462
defines
haftmann@61776
   463
  Min = Min.F and Max = Max.F ..
haftmann@54864
   464
lp15@67969
   465
abbreviation MINIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
lp15@67969
   466
  where "MINIMUM A f \<equiv> Min(f ` A)"
lp15@67969
   467
abbreviation MAXIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
lp15@67969
   468
  where "MAXIMUM A f \<equiv> Max(f ` A)"
lp15@67969
   469
haftmann@54864
   470
end
haftmann@54864
   471
lp15@67969
   472
lp15@67969
   473
syntax (ASCII)
lp15@67969
   474
  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
lp15@67969
   475
  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _:_./ _)" [0, 0, 10] 10)
lp15@67969
   476
  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
lp15@67969
   477
  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _:_./ _)" [0, 0, 10] 10)
lp15@67969
   478
lp15@67969
   479
syntax (output)
lp15@67969
   480
  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
lp15@67969
   481
  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _:_./ _)" [0, 0, 10] 10)
lp15@67969
   482
  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
lp15@67969
   483
  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _:_./ _)" [0, 0, 10] 10)
lp15@67969
   484
lp15@67969
   485
syntax
lp15@67969
   486
  "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
lp15@67969
   487
  "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _\<in>_./ _)" [0, 0, 10] 10)
lp15@67969
   488
  "_MAX1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MAX _./ _)" [0, 10] 10)
lp15@67969
   489
  "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
lp15@67969
   490
lp15@67969
   491
translations
lp15@67969
   492
  "MIN x y. B"   \<rightleftharpoons> "MIN x. MIN y. B"
lp15@67969
   493
  "MIN x. B"     \<rightleftharpoons> "CONST MINIMUM CONST UNIV (\<lambda>x. B)"
lp15@67969
   494
  "MIN x. B"     \<rightleftharpoons> "MIN x \<in> CONST UNIV. B"
lp15@67969
   495
  "MIN x\<in>A. B"   \<rightleftharpoons> "CONST MINIMUM A (\<lambda>x. B)"
lp15@67969
   496
  "MAX x y. B"   \<rightleftharpoons> "MAX x. MAX y. B"
lp15@67969
   497
  "MAX x. B"     \<rightleftharpoons> "CONST MAXIMUM CONST UNIV (\<lambda>x. B)"
lp15@67969
   498
  "MAX x. B"     \<rightleftharpoons> "MAX x \<in> CONST UNIV. B"
lp15@67969
   499
  "MAX x\<in>A. B"   \<rightleftharpoons> "CONST MAXIMUM A (\<lambda>x. B)"
lp15@67969
   500
lp15@67969
   501
print_translation \<open>
lp15@67969
   502
  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
lp15@67969
   503
    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
lp15@67969
   504
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
lp15@67969
   505
wenzelm@60758
   506
text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close>
haftmann@54864
   507
haftmann@54864
   508
lemma Inf_fin_Min:
haftmann@54864
   509
  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
haftmann@54864
   510
  by (simp add: Inf_fin_def Min_def inf_min)
haftmann@54864
   511
haftmann@54864
   512
lemma Sup_fin_Max:
haftmann@54864
   513
  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
haftmann@54864
   514
  by (simp add: Sup_fin_def Max_def sup_max)
haftmann@54864
   515
haftmann@54864
   516
context linorder
haftmann@54864
   517
begin
haftmann@54864
   518
haftmann@54744
   519
lemma dual_min:
haftmann@54744
   520
  "ord.min greater_eq = max"
haftmann@54744
   521
  by (auto simp add: ord.min_def max_def fun_eq_iff)
haftmann@54744
   522
haftmann@54744
   523
lemma dual_max:
haftmann@54744
   524
  "ord.max greater_eq = min"
haftmann@54744
   525
  by (auto simp add: ord.max_def min_def fun_eq_iff)
haftmann@54744
   526
haftmann@54744
   527
lemma dual_Min:
haftmann@54744
   528
  "linorder.Min greater_eq = Max"
haftmann@54744
   529
proof -
wenzelm@61605
   530
  interpret dual: linorder greater_eq greater by (fact dual_linorder)
haftmann@54744
   531
  show ?thesis by (simp add: dual.Min_def dual_min Max_def)
haftmann@54744
   532
qed
haftmann@54744
   533
haftmann@54744
   534
lemma dual_Max:
haftmann@54744
   535
  "linorder.Max greater_eq = Min"
haftmann@54744
   536
proof -
wenzelm@61605
   537
  interpret dual: linorder greater_eq greater by (fact dual_linorder)
haftmann@54744
   538
  show ?thesis by (simp add: dual.Max_def dual_max Min_def)
haftmann@54744
   539
qed
haftmann@54744
   540
haftmann@54744
   541
lemmas Min_singleton = Min.singleton
haftmann@54744
   542
lemmas Max_singleton = Max.singleton
haftmann@54744
   543
lemmas Min_insert = Min.insert
haftmann@54744
   544
lemmas Max_insert = Max.insert
haftmann@54744
   545
lemmas Min_Un = Min.union
haftmann@54744
   546
lemmas Max_Un = Max.union
haftmann@54744
   547
lemmas hom_Min_commute = Min.hom_commute
haftmann@54744
   548
lemmas hom_Max_commute = Max.hom_commute
haftmann@54744
   549
haftmann@54744
   550
lemma Min_in [simp]:
haftmann@54744
   551
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   552
  shows "Min A \<in> A"
haftmann@54744
   553
  using assms by (auto simp add: min_def Min.closed)
haftmann@54744
   554
haftmann@54744
   555
lemma Max_in [simp]:
haftmann@54744
   556
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   557
  shows "Max A \<in> A"
haftmann@54744
   558
  using assms by (auto simp add: max_def Max.closed)
haftmann@54744
   559
haftmann@58467
   560
lemma Min_insert2:
haftmann@58467
   561
  assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b"
haftmann@58467
   562
  shows "Min (insert a A) = a"
haftmann@58467
   563
proof (cases "A = {}")
wenzelm@63915
   564
  case True
wenzelm@63915
   565
  then show ?thesis by simp
haftmann@58467
   566
next
wenzelm@63915
   567
  case False
wenzelm@63915
   568
  with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
haftmann@58467
   569
    by simp
wenzelm@60758
   570
  moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp
haftmann@58467
   571
  ultimately show ?thesis by (simp add: min.absorb1)
haftmann@58467
   572
qed
haftmann@58467
   573
haftmann@58467
   574
lemma Max_insert2:
haftmann@58467
   575
  assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
haftmann@58467
   576
  shows "Max (insert a A) = a"
haftmann@58467
   577
proof (cases "A = {}")
wenzelm@63915
   578
  case True
wenzelm@63915
   579
  then show ?thesis by simp
haftmann@58467
   580
next
wenzelm@63915
   581
  case False
wenzelm@63915
   582
  with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
haftmann@58467
   583
    by simp
wenzelm@60758
   584
  moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp
haftmann@58467
   585
  ultimately show ?thesis by (simp add: max.absorb1)
haftmann@58467
   586
qed
haftmann@58467
   587
haftmann@54744
   588
lemma Min_le [simp]:
haftmann@54744
   589
  assumes "finite A" and "x \<in> A"
haftmann@54744
   590
  shows "Min A \<le> x"
haftmann@54744
   591
  using assms by (fact Min.coboundedI)
haftmann@54744
   592
haftmann@54744
   593
lemma Max_ge [simp]:
haftmann@54744
   594
  assumes "finite A" and "x \<in> A"
haftmann@54744
   595
  shows "x \<le> Max A"
haftmann@54744
   596
  using assms by (fact Max.coboundedI)
haftmann@54744
   597
haftmann@54744
   598
lemma Min_eqI:
haftmann@54744
   599
  assumes "finite A"
haftmann@54744
   600
  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
haftmann@54744
   601
    and "x \<in> A"
haftmann@54744
   602
  shows "Min A = x"
haftmann@54744
   603
proof (rule antisym)
wenzelm@60758
   604
  from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
haftmann@54744
   605
  with assms show "Min A \<ge> x" by simp
haftmann@54744
   606
next
haftmann@54744
   607
  from assms show "x \<ge> Min A" by simp
haftmann@54744
   608
qed
haftmann@54744
   609
haftmann@54744
   610
lemma Max_eqI:
haftmann@54744
   611
  assumes "finite A"
haftmann@54744
   612
  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
haftmann@54744
   613
    and "x \<in> A"
haftmann@54744
   614
  shows "Max A = x"
haftmann@54744
   615
proof (rule antisym)
wenzelm@60758
   616
  from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
haftmann@54744
   617
  with assms show "Max A \<le> x" by simp
haftmann@54744
   618
next
haftmann@54744
   619
  from assms show "x \<le> Max A" by simp
haftmann@54744
   620
qed
haftmann@54744
   621
nipkow@66425
   622
lemma eq_Min_iff:
nipkow@66425
   623
  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
nipkow@66425
   624
by (meson Min_in Min_le antisym)
nipkow@66425
   625
nipkow@66425
   626
lemma Min_eq_iff:
nipkow@66425
   627
  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
nipkow@66425
   628
by (meson Min_in Min_le antisym)
nipkow@66425
   629
nipkow@66425
   630
lemma eq_Max_iff:
nipkow@66425
   631
  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
nipkow@66425
   632
by (meson Max_in Max_ge antisym)
nipkow@66425
   633
nipkow@66425
   634
lemma Max_eq_iff:
nipkow@66425
   635
  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
nipkow@66425
   636
by (meson Max_in Max_ge antisym)
nipkow@66425
   637
haftmann@54744
   638
context
haftmann@54744
   639
  fixes A :: "'a set"
haftmann@54744
   640
  assumes fin_nonempty: "finite A" "A \<noteq> {}"
haftmann@54744
   641
begin
haftmann@54744
   642
haftmann@54744
   643
lemma Min_ge_iff [simp]:
haftmann@54744
   644
  "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
haftmann@54744
   645
  using fin_nonempty by (fact Min.bounded_iff)
haftmann@54744
   646
haftmann@54744
   647
lemma Max_le_iff [simp]:
haftmann@54744
   648
  "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
haftmann@54744
   649
  using fin_nonempty by (fact Max.bounded_iff)
haftmann@54744
   650
haftmann@54744
   651
lemma Min_gr_iff [simp]:
haftmann@54744
   652
  "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
haftmann@54744
   653
  using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
haftmann@54744
   654
haftmann@54744
   655
lemma Max_less_iff [simp]:
haftmann@54744
   656
  "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
haftmann@54744
   657
  using fin_nonempty by (induct rule: finite_ne_induct) simp_all
haftmann@54744
   658
haftmann@54744
   659
lemma Min_le_iff:
haftmann@54744
   660
  "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
haftmann@54744
   661
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
haftmann@54744
   662
haftmann@54744
   663
lemma Max_ge_iff:
haftmann@54744
   664
  "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
haftmann@54744
   665
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
haftmann@54744
   666
haftmann@54744
   667
lemma Min_less_iff:
haftmann@54744
   668
  "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
haftmann@54744
   669
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
haftmann@54744
   670
haftmann@54744
   671
lemma Max_gr_iff:
haftmann@54744
   672
  "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
haftmann@54744
   673
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
haftmann@54744
   674
haftmann@54744
   675
end
haftmann@54744
   676
nipkow@57800
   677
lemma Max_eq_if:
nipkow@57800
   678
  assumes "finite A"  "finite B"  "\<forall>a\<in>A. \<exists>b\<in>B. a \<le> b"  "\<forall>b\<in>B. \<exists>a\<in>A. b \<le> a"
nipkow@57800
   679
  shows "Max A = Max B"
nipkow@57800
   680
proof cases
nipkow@57800
   681
  assume "A = {}" thus ?thesis using assms by simp
nipkow@57800
   682
next
nipkow@57800
   683
  assume "A \<noteq> {}" thus ?thesis using assms
nipkow@57800
   684
    by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
nipkow@57800
   685
qed
nipkow@57800
   686
haftmann@54744
   687
lemma Min_antimono:
haftmann@54744
   688
  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
haftmann@54744
   689
  shows "Min N \<le> Min M"
haftmann@67525
   690
  using assms by (fact Min.subset_imp)
haftmann@54744
   691
haftmann@54744
   692
lemma Max_mono:
haftmann@54744
   693
  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
haftmann@54744
   694
  shows "Max M \<le> Max N"
haftmann@67525
   695
  using assms by (fact Max.subset_imp)
haftmann@54744
   696
wenzelm@56140
   697
end
wenzelm@56140
   698
wenzelm@56140
   699
context linorder  (* FIXME *)
wenzelm@56140
   700
begin
wenzelm@56140
   701
haftmann@54744
   702
lemma mono_Min_commute:
haftmann@54744
   703
  assumes "mono f"
haftmann@54744
   704
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   705
  shows "f (Min A) = Min (f ` A)"
haftmann@54744
   706
proof (rule linorder_class.Min_eqI [symmetric])
wenzelm@60758
   707
  from \<open>finite A\<close> show "finite (f ` A)" by simp
haftmann@54744
   708
  from assms show "f (Min A) \<in> f ` A" by simp
haftmann@54744
   709
  fix x
haftmann@54744
   710
  assume "x \<in> f ` A"
haftmann@54744
   711
  then obtain y where "y \<in> A" and "x = f y" ..
haftmann@54744
   712
  with assms have "Min A \<le> y" by auto
wenzelm@60758
   713
  with \<open>mono f\<close> have "f (Min A) \<le> f y" by (rule monoE)
wenzelm@60758
   714
  with \<open>x = f y\<close> show "f (Min A) \<le> x" by simp
haftmann@54744
   715
qed
haftmann@54744
   716
haftmann@54744
   717
lemma mono_Max_commute:
haftmann@54744
   718
  assumes "mono f"
haftmann@54744
   719
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   720
  shows "f (Max A) = Max (f ` A)"
haftmann@54744
   721
proof (rule linorder_class.Max_eqI [symmetric])
wenzelm@60758
   722
  from \<open>finite A\<close> show "finite (f ` A)" by simp
haftmann@54744
   723
  from assms show "f (Max A) \<in> f ` A" by simp
haftmann@54744
   724
  fix x
haftmann@54744
   725
  assume "x \<in> f ` A"
haftmann@54744
   726
  then obtain y where "y \<in> A" and "x = f y" ..
haftmann@54744
   727
  with assms have "y \<le> Max A" by auto
wenzelm@60758
   728
  with \<open>mono f\<close> have "f y \<le> f (Max A)" by (rule monoE)
wenzelm@60758
   729
  with \<open>x = f y\<close> show "x \<le> f (Max A)" by simp
haftmann@54744
   730
qed
haftmann@54744
   731
haftmann@54744
   732
lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
haftmann@54744
   733
  assumes fin: "finite A"
haftmann@54744
   734
  and empty: "P {}" 
haftmann@54744
   735
  and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
haftmann@54744
   736
  shows "P A"
haftmann@54744
   737
using fin empty insert
haftmann@54744
   738
proof (induct rule: finite_psubset_induct)
haftmann@54744
   739
  case (psubset A)
haftmann@54744
   740
  have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 
haftmann@54744
   741
  have fin: "finite A" by fact 
haftmann@54744
   742
  have empty: "P {}" by fact
haftmann@54744
   743
  have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
haftmann@54744
   744
  show "P A"
haftmann@54744
   745
  proof (cases "A = {}")
haftmann@54744
   746
    assume "A = {}" 
wenzelm@60758
   747
    then show "P A" using \<open>P {}\<close> by simp
haftmann@54744
   748
  next
haftmann@54744
   749
    let ?B = "A - {Max A}" 
haftmann@54744
   750
    let ?A = "insert (Max A) ?B"
wenzelm@60758
   751
    have "finite ?B" using \<open>finite A\<close> by simp
haftmann@54744
   752
    assume "A \<noteq> {}"
wenzelm@67613
   753
    with \<open>finite A\<close> have "Max A \<in> A" by auto
haftmann@54744
   754
    then have A: "?A = A" using insert_Diff_single insert_absorb by auto
wenzelm@60758
   755
    then have "P ?B" using \<open>P {}\<close> step IH [of ?B] by blast
haftmann@54744
   756
    moreover 
wenzelm@60758
   757
    have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF \<open>finite A\<close>] by fastforce
wenzelm@60758
   758
    ultimately show "P A" using A insert_Diff_single step [OF \<open>finite ?B\<close>] by fastforce
haftmann@54744
   759
  qed
haftmann@54744
   760
qed
haftmann@54744
   761
haftmann@54744
   762
lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
haftmann@54744
   763
  "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
haftmann@54744
   764
  by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
haftmann@54744
   765
haftmann@54744
   766
lemma Least_Min:
haftmann@54744
   767
  assumes "finite {a. P a}" and "\<exists>a. P a"
haftmann@54744
   768
  shows "(LEAST a. P a) = Min {a. P a}"
haftmann@54744
   769
proof -
haftmann@54744
   770
  { fix A :: "'a set"
haftmann@54744
   771
    assume A: "finite A" "A \<noteq> {}"
haftmann@54744
   772
    have "(LEAST a. a \<in> A) = Min A"
haftmann@54744
   773
    using A proof (induct A rule: finite_ne_induct)
haftmann@54744
   774
      case singleton show ?case by (rule Least_equality) simp_all
haftmann@54744
   775
    next
haftmann@54744
   776
      case (insert a A)
haftmann@54744
   777
      have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
haftmann@54744
   778
        by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
haftmann@54744
   779
      with insert show ?case by simp
haftmann@54744
   780
    qed
haftmann@54744
   781
  } from this [of "{a. P a}"] assms show ?thesis by simp
haftmann@54744
   782
qed
haftmann@54744
   783
hoelzl@59000
   784
lemma infinite_growing:
hoelzl@59000
   785
  assumes "X \<noteq> {}"
hoelzl@59000
   786
  assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x"
hoelzl@59000
   787
  shows "\<not> finite X"
hoelzl@59000
   788
proof
hoelzl@59000
   789
  assume "finite X"
wenzelm@60758
   790
  with \<open>X \<noteq> {}\<close> have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X"
hoelzl@59000
   791
    by auto
hoelzl@59000
   792
  with *[of "Max X"] show False
hoelzl@59000
   793
    by auto
hoelzl@59000
   794
qed
hoelzl@59000
   795
haftmann@54744
   796
end
haftmann@54744
   797
haftmann@54744
   798
context linordered_ab_semigroup_add
haftmann@54744
   799
begin
haftmann@54744
   800
haftmann@54744
   801
lemma add_Min_commute:
haftmann@54744
   802
  fixes k
haftmann@54744
   803
  assumes "finite N" and "N \<noteq> {}"
haftmann@54744
   804
  shows "k + Min N = Min {k + m | m. m \<in> N}"
haftmann@54744
   805
proof -
haftmann@54744
   806
  have "\<And>x y. k + min x y = min (k + x) (k + y)"
haftmann@54744
   807
    by (simp add: min_def not_le)
haftmann@54744
   808
      (blast intro: antisym less_imp_le add_left_mono)
haftmann@54744
   809
  with assms show ?thesis
haftmann@54744
   810
    using hom_Min_commute [of "plus k" N]
haftmann@54744
   811
    by simp (blast intro: arg_cong [where f = Min])
haftmann@54744
   812
qed
haftmann@54744
   813
haftmann@54744
   814
lemma add_Max_commute:
haftmann@54744
   815
  fixes k
haftmann@54744
   816
  assumes "finite N" and "N \<noteq> {}"
haftmann@54744
   817
  shows "k + Max N = Max {k + m | m. m \<in> N}"
haftmann@54744
   818
proof -
haftmann@54744
   819
  have "\<And>x y. k + max x y = max (k + x) (k + y)"
haftmann@54744
   820
    by (simp add: max_def not_le)
haftmann@54744
   821
      (blast intro: antisym less_imp_le add_left_mono)
haftmann@54744
   822
  with assms show ?thesis
haftmann@54744
   823
    using hom_Max_commute [of "plus k" N]
haftmann@54744
   824
    by simp (blast intro: arg_cong [where f = Max])
haftmann@54744
   825
qed
haftmann@54744
   826
haftmann@54744
   827
end
haftmann@54744
   828
haftmann@54744
   829
context linordered_ab_group_add
haftmann@54744
   830
begin
haftmann@54744
   831
haftmann@54744
   832
lemma minus_Max_eq_Min [simp]:
haftmann@54744
   833
  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
haftmann@54744
   834
  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
haftmann@54744
   835
haftmann@54744
   836
lemma minus_Min_eq_Max [simp]:
haftmann@54744
   837
  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
haftmann@54744
   838
  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
haftmann@54744
   839
haftmann@54744
   840
end
haftmann@54744
   841
haftmann@54744
   842
context complete_linorder
haftmann@54744
   843
begin
haftmann@54744
   844
haftmann@54744
   845
lemma Min_Inf:
haftmann@54744
   846
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   847
  shows "Min A = Inf A"
haftmann@54744
   848
proof -
haftmann@54744
   849
  from assms obtain b B where "A = insert b B" and "finite B" by auto
haftmann@54744
   850
  then show ?thesis
haftmann@54744
   851
    by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
haftmann@54744
   852
qed
haftmann@54744
   853
haftmann@54744
   854
lemma Max_Sup:
haftmann@54744
   855
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   856
  shows "Max A = Sup A"
haftmann@54744
   857
proof -
haftmann@54744
   858
  from assms obtain b B where "A = insert b B" and "finite B" by auto
haftmann@54744
   859
  then show ?thesis
haftmann@54744
   860
    by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
haftmann@54744
   861
qed
haftmann@54744
   862
haftmann@54744
   863
end
haftmann@54744
   864
nipkow@65817
   865
nipkow@65817
   866
subsection \<open>Arg Min\<close>
nipkow@65817
   867
nipkow@65842
   868
definition is_arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
nipkow@65842
   869
"is_arg_min f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y < f x))"
nipkow@65842
   870
nipkow@65842
   871
definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
nipkow@65842
   872
"arg_min f P = (SOME x. is_arg_min f P x)"
nipkow@65842
   873
nipkow@67169
   874
definition arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
nipkow@67169
   875
"arg_min_on f S = arg_min f (\<lambda>x. x \<in> S)"
nipkow@65842
   876
nipkow@65951
   877
syntax
nipkow@65951
   878
  "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
nipkow@67036
   879
    ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10)
nipkow@65951
   880
translations
nipkow@65951
   881
  "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)"
nipkow@65951
   882
nipkow@65842
   883
lemma is_arg_min_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder"
nipkow@65842
   884
shows "is_arg_min f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<le> f y))"
nipkow@65842
   885
by(auto simp add: is_arg_min_def)
nipkow@65817
   886
nipkow@67566
   887
lemma is_arg_min_antimono: fixes f :: "'a \<Rightarrow> ('b::order)"
nipkow@67566
   888
shows "\<lbrakk> is_arg_min f P x; f y \<le> f x; P y \<rbrakk> \<Longrightarrow> is_arg_min f P y"
nipkow@67566
   889
by (simp add: order.order_iff_strict is_arg_min_def)
nipkow@67566
   890
nipkow@65951
   891
lemma arg_minI:
nipkow@65951
   892
  "\<lbrakk> P x;
nipkow@65951
   893
    \<And>y. P y \<Longrightarrow> \<not> f y < f x;
nipkow@65951
   894
    \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> \<not> f y < f x \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
nipkow@65951
   895
  \<Longrightarrow> Q (arg_min f P)"
nipkow@65951
   896
apply (simp add: arg_min_def is_arg_min_def)
nipkow@65951
   897
apply (rule someI2_ex)
nipkow@65951
   898
 apply blast
nipkow@65951
   899
apply blast
nipkow@65951
   900
done
nipkow@65951
   901
nipkow@65951
   902
lemma arg_min_equality:
nipkow@65952
   903
  "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k"
nipkow@65951
   904
  for f :: "_ \<Rightarrow> 'a::order"
nipkow@65951
   905
apply (rule arg_minI)
nipkow@65951
   906
  apply assumption
nipkow@65951
   907
 apply (simp add: less_le_not_le)
nipkow@65951
   908
by (metis le_less)
nipkow@65951
   909
nipkow@65952
   910
lemma wf_linord_ex_has_least:
nipkow@65952
   911
  "\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk>
nipkow@65952
   912
   \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
nipkow@65952
   913
apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
nipkow@65952
   914
apply (drule_tac x = "m ` Collect P" in spec)
nipkow@65952
   915
by force
nipkow@65952
   916
nipkow@65952
   917
lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
nipkow@65952
   918
  for m :: "'a \<Rightarrow> nat"
nipkow@65952
   919
apply (simp only: pred_nat_trancl_eq_le [symmetric])
nipkow@65952
   920
apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
nipkow@65952
   921
 apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
nipkow@65952
   922
by assumption
nipkow@65952
   923
nipkow@65951
   924
lemma arg_min_nat_lemma:
nipkow@65951
   925
  "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)"
nipkow@65842
   926
  for m :: "'a \<Rightarrow> nat"
nipkow@65842
   927
apply (simp add: arg_min_def is_arg_min_linorder)
nipkow@65842
   928
apply (rule someI_ex)
nipkow@65842
   929
apply (erule ex_has_least_nat)
nipkow@65842
   930
done
nipkow@65842
   931
nipkow@65842
   932
lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1]
nipkow@65817
   933
nipkow@65951
   934
lemma is_arg_min_arg_min_nat: fixes m :: "'a \<Rightarrow> nat"
nipkow@65951
   935
shows "P x \<Longrightarrow> is_arg_min m P (arg_min m P)"
nipkow@65951
   936
by (metis arg_min_nat_lemma is_arg_min_linorder)
nipkow@65951
   937
nipkow@65842
   938
lemma arg_min_nat_le: "P x \<Longrightarrow> m (arg_min m P) \<le> m x"
nipkow@65842
   939
  for m :: "'a \<Rightarrow> nat"
nipkow@65842
   940
by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
nipkow@65842
   941
nipkow@65842
   942
lemma ex_min_if_finite:
nipkow@65842
   943
  "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>m\<in>S. \<not>(\<exists>x\<in>S. x < (m::'a::order))"
nipkow@65842
   944
by(induction rule: finite.induct) (auto intro: order.strict_trans)
nipkow@65842
   945
nipkow@65842
   946
lemma ex_is_arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order"
wenzelm@67613
   947
shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x \<in> S) x"
nipkow@65842
   948
unfolding is_arg_min_def
nipkow@65842
   949
using ex_min_if_finite[of "f ` S"]
nipkow@65842
   950
by auto
nipkow@65817
   951
nipkow@65817
   952
lemma arg_min_SOME_Min:
nipkow@65842
   953
  "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))"
nipkow@67169
   954
unfolding arg_min_on_def arg_min_def is_arg_min_linorder
nipkow@65817
   955
apply(rule arg_cong[where f = Eps])
nipkow@65817
   956
apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
nipkow@65817
   957
done
nipkow@65817
   958
nipkow@65842
   959
lemma arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order"
nipkow@65842
   960
assumes "finite S" "S \<noteq> {}"
nipkow@65842
   961
shows  "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))"
nipkow@65842
   962
using ex_is_arg_min_if_finite[OF assms, of f]
nipkow@67169
   963
unfolding arg_min_on_def arg_min_def is_arg_min_def
nipkow@65842
   964
by(auto dest!: someI_ex)
nipkow@65817
   965
nipkow@65817
   966
lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder"
nipkow@65842
   967
shows "\<lbrakk> finite S;  S \<noteq> {};  y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> f y"
nipkow@65817
   968
by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f)
nipkow@65817
   969
nipkow@65817
   970
lemma arg_min_inj_eq: fixes f :: "'a \<Rightarrow> 'b :: order"
nipkow@65842
   971
shows "\<lbrakk> inj_on f {x. P x}; P a; \<forall>y. P y \<longrightarrow> f a \<le> f y \<rbrakk> \<Longrightarrow> arg_min f P = a"
nipkow@65842
   972
apply(simp add: arg_min_def is_arg_min_def)
nipkow@65817
   973
apply(rule someI2[of _ a])
nipkow@65817
   974
 apply (simp add: less_le_not_le)
nipkow@65842
   975
by (metis inj_on_eq_iff less_le mem_Collect_eq)
nipkow@65817
   976
nipkow@65954
   977
nipkow@65954
   978
subsection \<open>Arg Max\<close>
nipkow@65954
   979
nipkow@65954
   980
definition is_arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
nipkow@65954
   981
"is_arg_max f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y > f x))"
nipkow@65954
   982
nipkow@65954
   983
definition arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
nipkow@65954
   984
"arg_max f P = (SOME x. is_arg_max f P x)"
nipkow@65954
   985
nipkow@67169
   986
definition arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
nipkow@67169
   987
"arg_max_on f S = arg_max f (\<lambda>x. x \<in> S)"
nipkow@65954
   988
nipkow@65954
   989
syntax
nipkow@65954
   990
  "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
nipkow@67036
   991
    ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10)
nipkow@65954
   992
translations
nipkow@65954
   993
  "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"
nipkow@65954
   994
nipkow@65954
   995
lemma is_arg_max_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder"
nipkow@65954
   996
shows "is_arg_max f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<ge> f y))"
nipkow@65954
   997
by(auto simp add: is_arg_max_def)
nipkow@65954
   998
nipkow@65954
   999
lemma arg_maxI:
nipkow@65954
  1000
  "P x \<Longrightarrow>
nipkow@65954
  1001
    (\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow>
nipkow@65954
  1002
    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow>
nipkow@65954
  1003
    Q (arg_max f P)"
nipkow@65954
  1004
apply (simp add: arg_max_def is_arg_max_def)
nipkow@65954
  1005
apply (rule someI2_ex)
nipkow@65954
  1006
 apply blast
nipkow@65954
  1007
apply blast
nipkow@65954
  1008
done
nipkow@65954
  1009
nipkow@65954
  1010
lemma arg_max_equality:
nipkow@65954
  1011
  "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f x \<le> f k \<rbrakk> \<Longrightarrow> f (arg_max f P) = f k"
nipkow@65954
  1012
  for f :: "_ \<Rightarrow> 'a::order"
nipkow@65954
  1013
apply (rule arg_maxI [where f = f])
nipkow@65954
  1014
  apply assumption
nipkow@65954
  1015
 apply (simp add: less_le_not_le)
nipkow@65954
  1016
by (metis le_less)
nipkow@65954
  1017
nipkow@65954
  1018
lemma ex_has_greatest_nat_lemma:
nipkow@65954
  1019
  "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> f y \<le> f x) \<Longrightarrow> \<exists>y. P y \<and> \<not> f y < f k + n"
nipkow@65954
  1020
  for f :: "'a \<Rightarrow> nat"
nipkow@65954
  1021
by (induct n) (force simp: le_Suc_eq)+
nipkow@65954
  1022
nipkow@65954
  1023
lemma ex_has_greatest_nat:
nipkow@65954
  1024
  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f x)"
nipkow@65954
  1025
  for f :: "'a \<Rightarrow> nat"
nipkow@65954
  1026
apply (rule ccontr)
nipkow@65954
  1027
apply (cut_tac P = P and n = "b - f k" in ex_has_greatest_nat_lemma)
nipkow@65954
  1028
  apply (subgoal_tac [3] "f k \<le> b")
nipkow@65954
  1029
   apply auto
nipkow@65954
  1030
done
nipkow@65954
  1031
nipkow@65954
  1032
lemma arg_max_nat_lemma:
nipkow@65954
  1033
  "\<lbrakk> P k;  \<forall>y. P y \<longrightarrow> f y < b \<rbrakk>
nipkow@65954
  1034
  \<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))"
nipkow@65954
  1035
  for f :: "'a \<Rightarrow> nat"
nipkow@65954
  1036
apply (simp add: arg_max_def is_arg_max_linorder)
nipkow@65954
  1037
apply (rule someI_ex)
nipkow@65954
  1038
apply (erule (1) ex_has_greatest_nat)
nipkow@65954
  1039
done
nipkow@65954
  1040
nipkow@65954
  1041
lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1]
nipkow@65954
  1042
nipkow@65954
  1043
lemma arg_max_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> f x \<le> f (arg_max f P)"
nipkow@65954
  1044
  for f :: "'a \<Rightarrow> nat"
nipkow@65954
  1045
by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P])
nipkow@65954
  1046
haftmann@54744
  1047
end