src/HOL/Lattices_Big.thy
author haftmann
Sun Dec 15 15:10:16 2013 +0100 (2013-12-15)
changeset 54745 46e441e61ff5
parent 54744 1e7f2d296e19
child 54857 5c05f7c5f8ae
permissions -rw-r--r--
disambiguation of interpretation prefixes
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
haftmann@54744
     6
header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
haftmann@54744
     7
haftmann@54744
     8
theory Lattices_Big
haftmann@54744
     9
imports Finite_Set
haftmann@54744
    10
begin
haftmann@54744
    11
haftmann@54744
    12
subsection {* Generic lattice operations over a set *}
haftmann@54744
    13
haftmann@54744
    14
no_notation times (infixl "*" 70)
haftmann@54744
    15
no_notation Groups.one ("1")
haftmann@54744
    16
haftmann@54744
    17
haftmann@54744
    18
subsubsection {* Without neutral element *}
haftmann@54744
    19
haftmann@54744
    20
locale semilattice_set = semilattice
haftmann@54744
    21
begin
haftmann@54744
    22
haftmann@54744
    23
interpretation comp_fun_idem f
haftmann@54744
    24
  by default (simp_all add: fun_eq_iff left_commute)
haftmann@54744
    25
haftmann@54744
    26
definition F :: "'a set \<Rightarrow> 'a"
haftmann@54744
    27
where
haftmann@54744
    28
  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
    29
haftmann@54744
    30
lemma eq_fold:
haftmann@54744
    31
  assumes "finite A"
haftmann@54744
    32
  shows "F (insert x A) = Finite_Set.fold f x A"
haftmann@54744
    33
proof (rule sym)
haftmann@54744
    34
  let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
haftmann@54744
    35
  interpret comp_fun_idem "?f"
haftmann@54744
    36
    by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
haftmann@54744
    37
  from assms show "Finite_Set.fold f x A = F (insert x A)"
haftmann@54744
    38
  proof induct
haftmann@54744
    39
    case empty then show ?case by (simp add: eq_fold')
haftmann@54744
    40
  next
haftmann@54744
    41
    case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
haftmann@54744
    42
  qed
haftmann@54744
    43
qed
haftmann@54744
    44
haftmann@54744
    45
lemma singleton [simp]:
haftmann@54744
    46
  "F {x} = x"
haftmann@54744
    47
  by (simp add: eq_fold)
haftmann@54744
    48
haftmann@54744
    49
lemma insert_not_elem:
haftmann@54744
    50
  assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
haftmann@54744
    51
  shows "F (insert x A) = x * F A"
haftmann@54744
    52
proof -
haftmann@54744
    53
  from `A \<noteq> {}` obtain b where "b \<in> A" by blast
haftmann@54744
    54
  then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
haftmann@54744
    55
  with `finite A` and `x \<notin> A`
haftmann@54744
    56
    have "finite (insert x B)" and "b \<notin> insert x B" by auto
haftmann@54744
    57
  then have "F (insert b (insert x B)) = x * F (insert b B)"
haftmann@54744
    58
    by (simp add: eq_fold)
haftmann@54744
    59
  then show ?thesis by (simp add: * insert_commute)
haftmann@54744
    60
qed
haftmann@54744
    61
haftmann@54744
    62
lemma in_idem:
haftmann@54744
    63
  assumes "finite A" and "x \<in> A"
haftmann@54744
    64
  shows "x * F A = F A"
haftmann@54744
    65
proof -
haftmann@54744
    66
  from assms have "A \<noteq> {}" by auto
haftmann@54744
    67
  with `finite A` show ?thesis using `x \<in> A`
haftmann@54744
    68
    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
haftmann@54744
    69
qed
haftmann@54744
    70
haftmann@54744
    71
lemma insert [simp]:
haftmann@54744
    72
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
    73
  shows "F (insert x A) = x * F A"
haftmann@54744
    74
  using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
haftmann@54744
    75
haftmann@54744
    76
lemma union:
haftmann@54744
    77
  assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
haftmann@54744
    78
  shows "F (A \<union> B) = F A * F B"
haftmann@54744
    79
  using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
haftmann@54744
    80
haftmann@54744
    81
lemma remove:
haftmann@54744
    82
  assumes "finite A" and "x \<in> A"
haftmann@54744
    83
  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
haftmann@54744
    84
proof -
haftmann@54744
    85
  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
haftmann@54744
    86
  with assms show ?thesis by simp
haftmann@54744
    87
qed
haftmann@54744
    88
haftmann@54744
    89
lemma insert_remove:
haftmann@54744
    90
  assumes "finite A"
haftmann@54744
    91
  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
haftmann@54744
    92
  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
haftmann@54744
    93
haftmann@54744
    94
lemma subset:
haftmann@54744
    95
  assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
haftmann@54744
    96
  shows "F B * F A = F A"
haftmann@54744
    97
proof -
haftmann@54744
    98
  from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
haftmann@54744
    99
  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
haftmann@54744
   100
qed
haftmann@54744
   101
haftmann@54744
   102
lemma closed:
haftmann@54744
   103
  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
haftmann@54744
   104
  shows "F A \<in> A"
haftmann@54744
   105
using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
haftmann@54744
   106
  case singleton then show ?case by simp
haftmann@54744
   107
next
haftmann@54744
   108
  case insert with elem show ?case by force
haftmann@54744
   109
qed
haftmann@54744
   110
haftmann@54744
   111
lemma hom_commute:
haftmann@54744
   112
  assumes hom: "\<And>x y. h (x * y) = h x * h y"
haftmann@54744
   113
  and N: "finite N" "N \<noteq> {}"
haftmann@54744
   114
  shows "h (F N) = F (h ` N)"
haftmann@54744
   115
using N proof (induct rule: finite_ne_induct)
haftmann@54744
   116
  case singleton thus ?case by simp
haftmann@54744
   117
next
haftmann@54744
   118
  case (insert n N)
haftmann@54744
   119
  then have "h (F (insert n N)) = h (n * F N)" by simp
haftmann@54744
   120
  also have "\<dots> = h n * h (F N)" by (rule hom)
haftmann@54744
   121
  also have "h (F N) = F (h ` N)" by (rule insert)
haftmann@54744
   122
  also have "h n * \<dots> = F (insert (h n) (h ` N))"
haftmann@54744
   123
    using insert by simp
haftmann@54744
   124
  also have "insert (h n) (h ` N) = h ` insert n N" by simp
haftmann@54744
   125
  finally show ?case .
haftmann@54744
   126
qed
haftmann@54744
   127
haftmann@54744
   128
end
haftmann@54744
   129
haftmann@54745
   130
locale semilattice_order_set = binary?: semilattice_order + semilattice_set
haftmann@54744
   131
begin
haftmann@54744
   132
haftmann@54744
   133
lemma bounded_iff:
haftmann@54744
   134
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   135
  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
haftmann@54744
   136
  using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
haftmann@54744
   137
haftmann@54744
   138
lemma boundedI:
haftmann@54744
   139
  assumes "finite A"
haftmann@54744
   140
  assumes "A \<noteq> {}"
haftmann@54744
   141
  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
haftmann@54744
   142
  shows "x \<preceq> F A"
haftmann@54744
   143
  using assms by (simp add: bounded_iff)
haftmann@54744
   144
haftmann@54744
   145
lemma boundedE:
haftmann@54744
   146
  assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
haftmann@54744
   147
  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
haftmann@54744
   148
  using assms by (simp add: bounded_iff)
haftmann@54744
   149
haftmann@54744
   150
lemma coboundedI:
haftmann@54744
   151
  assumes "finite A"
haftmann@54744
   152
    and "a \<in> A"
haftmann@54744
   153
  shows "F A \<preceq> a"
haftmann@54744
   154
proof -
haftmann@54744
   155
  from assms have "A \<noteq> {}" by auto
haftmann@54744
   156
  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
haftmann@54744
   157
  proof (induct rule: finite_ne_induct)
haftmann@54744
   158
    case singleton thus ?case by (simp add: refl)
haftmann@54744
   159
  next
haftmann@54744
   160
    case (insert x B)
haftmann@54744
   161
    from insert have "a = x \<or> a \<in> B" by simp
haftmann@54744
   162
    then show ?case using insert by (auto intro: coboundedI2)
haftmann@54744
   163
  qed
haftmann@54744
   164
qed
haftmann@54744
   165
haftmann@54744
   166
lemma antimono:
haftmann@54744
   167
  assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
haftmann@54744
   168
  shows "F B \<preceq> F A"
haftmann@54744
   169
proof (cases "A = B")
haftmann@54744
   170
  case True then show ?thesis by (simp add: refl)
haftmann@54744
   171
next
haftmann@54744
   172
  case False
haftmann@54744
   173
  have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
haftmann@54744
   174
  then have "F B = F (A \<union> (B - A))" by simp
haftmann@54744
   175
  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
haftmann@54744
   176
  also have "\<dots> \<preceq> F A" by simp
haftmann@54744
   177
  finally show ?thesis .
haftmann@54744
   178
qed
haftmann@54744
   179
haftmann@54744
   180
end
haftmann@54744
   181
haftmann@54744
   182
haftmann@54744
   183
subsubsection {* With neutral element *}
haftmann@54744
   184
haftmann@54744
   185
locale semilattice_neutr_set = semilattice_neutr
haftmann@54744
   186
begin
haftmann@54744
   187
haftmann@54744
   188
interpretation comp_fun_idem f
haftmann@54744
   189
  by default (simp_all add: fun_eq_iff left_commute)
haftmann@54744
   190
haftmann@54744
   191
definition F :: "'a set \<Rightarrow> 'a"
haftmann@54744
   192
where
haftmann@54744
   193
  eq_fold: "F A = Finite_Set.fold f 1 A"
haftmann@54744
   194
haftmann@54744
   195
lemma infinite [simp]:
haftmann@54744
   196
  "\<not> finite A \<Longrightarrow> F A = 1"
haftmann@54744
   197
  by (simp add: eq_fold)
haftmann@54744
   198
haftmann@54744
   199
lemma empty [simp]:
haftmann@54744
   200
  "F {} = 1"
haftmann@54744
   201
  by (simp add: eq_fold)
haftmann@54744
   202
haftmann@54744
   203
lemma insert [simp]:
haftmann@54744
   204
  assumes "finite A"
haftmann@54744
   205
  shows "F (insert x A) = x * F A"
haftmann@54744
   206
  using assms by (simp add: eq_fold)
haftmann@54744
   207
haftmann@54744
   208
lemma in_idem:
haftmann@54744
   209
  assumes "finite A" and "x \<in> A"
haftmann@54744
   210
  shows "x * F A = F A"
haftmann@54744
   211
proof -
haftmann@54744
   212
  from assms have "A \<noteq> {}" by auto
haftmann@54744
   213
  with `finite A` show ?thesis using `x \<in> A`
haftmann@54744
   214
    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
haftmann@54744
   215
qed
haftmann@54744
   216
haftmann@54744
   217
lemma union:
haftmann@54744
   218
  assumes "finite A" and "finite B"
haftmann@54744
   219
  shows "F (A \<union> B) = F A * F B"
haftmann@54744
   220
  using assms by (induct A) (simp_all add: ac_simps)
haftmann@54744
   221
haftmann@54744
   222
lemma remove:
haftmann@54744
   223
  assumes "finite A" and "x \<in> A"
haftmann@54744
   224
  shows "F A = x * F (A - {x})"
haftmann@54744
   225
proof -
haftmann@54744
   226
  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
haftmann@54744
   227
  with assms show ?thesis by simp
haftmann@54744
   228
qed
haftmann@54744
   229
haftmann@54744
   230
lemma insert_remove:
haftmann@54744
   231
  assumes "finite A"
haftmann@54744
   232
  shows "F (insert x A) = x * F (A - {x})"
haftmann@54744
   233
  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
haftmann@54744
   234
haftmann@54744
   235
lemma subset:
haftmann@54744
   236
  assumes "finite A" and "B \<subseteq> A"
haftmann@54744
   237
  shows "F B * F A = F A"
haftmann@54744
   238
proof -
haftmann@54744
   239
  from assms have "finite B" by (auto dest: finite_subset)
haftmann@54744
   240
  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
haftmann@54744
   241
qed
haftmann@54744
   242
haftmann@54744
   243
lemma closed:
haftmann@54744
   244
  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
haftmann@54744
   245
  shows "F A \<in> A"
haftmann@54744
   246
using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
haftmann@54744
   247
  case singleton then show ?case by simp
haftmann@54744
   248
next
haftmann@54744
   249
  case insert with elem show ?case by force
haftmann@54744
   250
qed
haftmann@54744
   251
haftmann@54744
   252
end
haftmann@54744
   253
haftmann@54745
   254
locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
haftmann@54744
   255
begin
haftmann@54744
   256
haftmann@54744
   257
lemma bounded_iff:
haftmann@54744
   258
  assumes "finite A"
haftmann@54744
   259
  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
haftmann@54744
   260
  using assms by (induct A) (simp_all add: bounded_iff)
haftmann@54744
   261
haftmann@54744
   262
lemma boundedI:
haftmann@54744
   263
  assumes "finite A"
haftmann@54744
   264
  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
haftmann@54744
   265
  shows "x \<preceq> F A"
haftmann@54744
   266
  using assms by (simp add: bounded_iff)
haftmann@54744
   267
haftmann@54744
   268
lemma boundedE:
haftmann@54744
   269
  assumes "finite A" and "x \<preceq> F A"
haftmann@54744
   270
  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
haftmann@54744
   271
  using assms by (simp add: bounded_iff)
haftmann@54744
   272
haftmann@54744
   273
lemma coboundedI:
haftmann@54744
   274
  assumes "finite A"
haftmann@54744
   275
    and "a \<in> A"
haftmann@54744
   276
  shows "F A \<preceq> a"
haftmann@54744
   277
proof -
haftmann@54744
   278
  from assms have "A \<noteq> {}" by auto
haftmann@54744
   279
  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
haftmann@54744
   280
  proof (induct rule: finite_ne_induct)
haftmann@54744
   281
    case singleton thus ?case by (simp add: refl)
haftmann@54744
   282
  next
haftmann@54744
   283
    case (insert x B)
haftmann@54744
   284
    from insert have "a = x \<or> a \<in> B" by simp
haftmann@54744
   285
    then show ?case using insert by (auto intro: coboundedI2)
haftmann@54744
   286
  qed
haftmann@54744
   287
qed
haftmann@54744
   288
haftmann@54744
   289
lemma antimono:
haftmann@54744
   290
  assumes "A \<subseteq> B" and "finite B"
haftmann@54744
   291
  shows "F B \<preceq> F A"
haftmann@54744
   292
proof (cases "A = B")
haftmann@54744
   293
  case True then show ?thesis by (simp add: refl)
haftmann@54744
   294
next
haftmann@54744
   295
  case False
haftmann@54744
   296
  have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
haftmann@54744
   297
  then have "F B = F (A \<union> (B - A))" by simp
haftmann@54744
   298
  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
haftmann@54744
   299
  also have "\<dots> \<preceq> F A" by simp
haftmann@54744
   300
  finally show ?thesis .
haftmann@54744
   301
qed
haftmann@54744
   302
haftmann@54744
   303
end
haftmann@54744
   304
haftmann@54744
   305
notation times (infixl "*" 70)
haftmann@54744
   306
notation Groups.one ("1")
haftmann@54744
   307
haftmann@54744
   308
haftmann@54744
   309
subsection {* Lattice operations on finite sets *}
haftmann@54744
   310
haftmann@54744
   311
text {*
haftmann@54744
   312
  For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
haftmann@54744
   313
  to @{class linorder}.  This is badly designed: both should depend on a common abstract
haftmann@54744
   314
  distributive lattice rather than having this non-subclass dependecy between two
haftmann@54744
   315
  classes.  But for the moment we have to live with it.  This forces us to setup
haftmann@54744
   316
  this sublocale dependency simultaneously with the lattice operations on finite
haftmann@54744
   317
  sets, to avoid garbage.
haftmann@54744
   318
*}
haftmann@54744
   319
haftmann@54744
   320
definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
haftmann@54744
   321
where
haftmann@54744
   322
  "Inf_fin = semilattice_set.F inf"
haftmann@54744
   323
haftmann@54744
   324
definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
haftmann@54744
   325
where
haftmann@54744
   326
  "Sup_fin = semilattice_set.F sup"
haftmann@54744
   327
haftmann@54744
   328
context linorder
haftmann@54744
   329
begin
haftmann@54744
   330
haftmann@54744
   331
definition Min :: "'a set \<Rightarrow> 'a"
haftmann@54744
   332
where
haftmann@54744
   333
  "Min = semilattice_set.F min"
haftmann@54744
   334
haftmann@54744
   335
definition Max :: "'a set \<Rightarrow> 'a"
haftmann@54744
   336
where
haftmann@54744
   337
  "Max = semilattice_set.F max"
haftmann@54744
   338
haftmann@54744
   339
sublocale Min!: semilattice_order_set min less_eq less
haftmann@54744
   340
  + Max!: semilattice_order_set max greater_eq greater
haftmann@54744
   341
where
haftmann@54744
   342
  "semilattice_set.F min = Min"
haftmann@54744
   343
  and "semilattice_set.F max = Max"
haftmann@54744
   344
proof -
haftmann@54744
   345
  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
haftmann@54744
   346
  then interpret Min!: semilattice_order_set min less_eq less .
haftmann@54744
   347
  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
haftmann@54744
   348
  then interpret Max!: semilattice_order_set max greater_eq greater .
haftmann@54744
   349
  from Min_def show "semilattice_set.F min = Min" by rule
haftmann@54744
   350
  from Max_def show "semilattice_set.F max = Max" by rule
haftmann@54744
   351
qed
haftmann@54744
   352
haftmann@54744
   353
haftmann@54744
   354
text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
haftmann@54744
   355
haftmann@54744
   356
sublocale min_max!: distrib_lattice min less_eq less max
haftmann@54744
   357
where
haftmann@54744
   358
  "semilattice_inf.Inf_fin min = Min"
haftmann@54744
   359
  and "semilattice_sup.Sup_fin max = Max"
haftmann@54744
   360
proof -
haftmann@54744
   361
  show "class.distrib_lattice min less_eq less max"
haftmann@54744
   362
  proof
haftmann@54744
   363
    fix x y z
haftmann@54744
   364
    show "max x (min y z) = min (max x y) (max x z)"
haftmann@54744
   365
      by (auto simp add: min_def max_def)
haftmann@54744
   366
  qed (auto simp add: min_def max_def not_le less_imp_le)
haftmann@54744
   367
  then interpret min_max!: distrib_lattice min less_eq less max .
haftmann@54744
   368
  show "semilattice_inf.Inf_fin min = Min"
haftmann@54744
   369
    by (simp only: min_max.Inf_fin_def Min_def)
haftmann@54744
   370
  show "semilattice_sup.Sup_fin max = Max"
haftmann@54744
   371
    by (simp only: min_max.Sup_fin_def Max_def)
haftmann@54744
   372
qed
haftmann@54744
   373
haftmann@54744
   374
lemmas le_maxI1 = min_max.sup_ge1
haftmann@54744
   375
lemmas le_maxI2 = min_max.sup_ge2
haftmann@54744
   376
 
haftmann@54744
   377
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
haftmann@54744
   378
  min.left_commute
haftmann@54744
   379
haftmann@54744
   380
lemmas max_ac = min_max.sup_assoc min_max.sup_commute
haftmann@54744
   381
  max.left_commute
haftmann@54744
   382
haftmann@54744
   383
end
haftmann@54744
   384
haftmann@54744
   385
haftmann@54744
   386
text {* Lattice operations proper *}
haftmann@54744
   387
haftmann@54744
   388
sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
haftmann@54744
   389
where
haftmann@54744
   390
  "semilattice_set.F inf = Inf_fin"
haftmann@54744
   391
proof -
haftmann@54744
   392
  show "semilattice_order_set inf less_eq less" ..
haftmann@54744
   393
  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
haftmann@54744
   394
  from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
haftmann@54744
   395
qed
haftmann@54744
   396
haftmann@54744
   397
sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
haftmann@54744
   398
where
haftmann@54744
   399
  "semilattice_set.F sup = Sup_fin"
haftmann@54744
   400
proof -
haftmann@54744
   401
  show "semilattice_order_set sup greater_eq greater" ..
haftmann@54744
   402
  then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
haftmann@54744
   403
  from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
haftmann@54744
   404
qed
haftmann@54744
   405
haftmann@54744
   406
haftmann@54744
   407
text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
haftmann@54744
   408
haftmann@54744
   409
lemma Inf_fin_Min:
haftmann@54744
   410
  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
haftmann@54744
   411
  by (simp add: Inf_fin_def Min_def inf_min)
haftmann@54744
   412
haftmann@54744
   413
lemma Sup_fin_Max:
haftmann@54744
   414
  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
haftmann@54744
   415
  by (simp add: Sup_fin_def Max_def sup_max)
haftmann@54744
   416
haftmann@54744
   417
haftmann@54744
   418
haftmann@54744
   419
subsection {* Infimum and Supremum over non-empty sets *}
haftmann@54744
   420
haftmann@54744
   421
text {*
haftmann@54744
   422
  After this non-regular bootstrap, things continue canonically.
haftmann@54744
   423
*}
haftmann@54744
   424
haftmann@54744
   425
context lattice
haftmann@54744
   426
begin
haftmann@54744
   427
haftmann@54745
   428
lemma Inf_fin_le_Sup_fin [simp]: 
haftmann@54745
   429
  assumes "finite A" and "A \<noteq> {}"
haftmann@54745
   430
  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
haftmann@54745
   431
proof -
haftmann@54745
   432
  from `A \<noteq> {}` obtain a where "a \<in> A" by blast
haftmann@54745
   433
  with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
haftmann@54745
   434
  moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
haftmann@54745
   435
  ultimately show ?thesis by (rule order_trans)
haftmann@54745
   436
qed
haftmann@54744
   437
haftmann@54744
   438
lemma sup_Inf_absorb [simp]:
haftmann@54745
   439
  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
haftmann@54745
   440
  by (rule sup_absorb2) (rule Inf_fin.coboundedI)
haftmann@54744
   441
haftmann@54744
   442
lemma inf_Sup_absorb [simp]:
haftmann@54745
   443
  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
haftmann@54745
   444
  by (rule inf_absorb1) (rule Sup_fin.coboundedI)
haftmann@54744
   445
haftmann@54744
   446
end
haftmann@54744
   447
haftmann@54744
   448
context distrib_lattice
haftmann@54744
   449
begin
haftmann@54744
   450
haftmann@54744
   451
lemma sup_Inf1_distrib:
haftmann@54744
   452
  assumes "finite A"
haftmann@54744
   453
    and "A \<noteq> {}"
haftmann@54744
   454
  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
   455
using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
haftmann@54744
   456
  (rule arg_cong [where f="Inf_fin"], blast)
haftmann@54744
   457
haftmann@54744
   458
lemma sup_Inf2_distrib:
haftmann@54744
   459
  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
haftmann@54744
   460
  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
   461
using A proof (induct rule: finite_ne_induct)
haftmann@54744
   462
  case singleton then show ?case
haftmann@54744
   463
    by (simp add: sup_Inf1_distrib [OF B])
haftmann@54744
   464
next
haftmann@54744
   465
  case (insert x A)
haftmann@54744
   466
  have finB: "finite {sup x b |b. b \<in> B}"
haftmann@54744
   467
    by (rule finite_surj [where f = "sup x", OF B(1)], auto)
haftmann@54744
   468
  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
haftmann@54744
   469
  proof -
haftmann@54744
   470
    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
haftmann@54744
   471
      by blast
haftmann@54744
   472
    thus ?thesis by(simp add: insert(1) B(1))
haftmann@54744
   473
  qed
haftmann@54744
   474
  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
haftmann@54744
   475
  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
   476
    using insert by simp
haftmann@54744
   477
  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
   478
  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
   479
    using insert by(simp add:sup_Inf1_distrib[OF B])
haftmann@54744
   480
  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
   481
    (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
haftmann@54744
   482
    using B insert
haftmann@54744
   483
    by (simp add: Inf_fin.union [OF finB _ finAB ne])
haftmann@54744
   484
  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
haftmann@54744
   485
    by blast
haftmann@54744
   486
  finally show ?case .
haftmann@54744
   487
qed
haftmann@54744
   488
haftmann@54744
   489
lemma inf_Sup1_distrib:
haftmann@54744
   490
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   491
  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
   492
using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
haftmann@54744
   493
  (rule arg_cong [where f="Sup_fin"], blast)
haftmann@54744
   494
haftmann@54744
   495
lemma inf_Sup2_distrib:
haftmann@54744
   496
  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
haftmann@54744
   497
  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
   498
using A proof (induct rule: finite_ne_induct)
haftmann@54744
   499
  case singleton thus ?case
haftmann@54744
   500
    by(simp add: inf_Sup1_distrib [OF B])
haftmann@54744
   501
next
haftmann@54744
   502
  case (insert x A)
haftmann@54744
   503
  have finB: "finite {inf x b |b. b \<in> B}"
haftmann@54744
   504
    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
haftmann@54744
   505
  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
haftmann@54744
   506
  proof -
haftmann@54744
   507
    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
haftmann@54744
   508
      by blast
haftmann@54744
   509
    thus ?thesis by(simp add: insert(1) B(1))
haftmann@54744
   510
  qed
haftmann@54744
   511
  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
haftmann@54744
   512
  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
   513
    using insert by simp
haftmann@54744
   514
  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
   515
  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
   516
    using insert by(simp add:inf_Sup1_distrib[OF B])
haftmann@54744
   517
  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
   518
    (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
haftmann@54744
   519
    using B insert
haftmann@54744
   520
    by (simp add: Sup_fin.union [OF finB _ finAB ne])
haftmann@54744
   521
  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
haftmann@54744
   522
    by blast
haftmann@54744
   523
  finally show ?case .
haftmann@54744
   524
qed
haftmann@54744
   525
haftmann@54744
   526
end
haftmann@54744
   527
haftmann@54744
   528
context complete_lattice
haftmann@54744
   529
begin
haftmann@54744
   530
haftmann@54744
   531
lemma Inf_fin_Inf:
haftmann@54744
   532
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   533
  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
haftmann@54744
   534
proof -
haftmann@54744
   535
  from assms obtain b B where "A = insert b B" and "finite B" by auto
haftmann@54744
   536
  then show ?thesis
haftmann@54744
   537
    by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
haftmann@54744
   538
qed
haftmann@54744
   539
haftmann@54744
   540
lemma Sup_fin_Sup:
haftmann@54744
   541
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   542
  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
haftmann@54744
   543
proof -
haftmann@54744
   544
  from assms obtain b B where "A = insert b B" and "finite B" by auto
haftmann@54744
   545
  then show ?thesis
haftmann@54744
   546
    by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
haftmann@54744
   547
qed
haftmann@54744
   548
haftmann@54744
   549
end
haftmann@54744
   550
haftmann@54744
   551
haftmann@54744
   552
subsection {* Minimum and Maximum over non-empty sets *}
haftmann@54744
   553
haftmann@54744
   554
context linorder
haftmann@54744
   555
begin
haftmann@54744
   556
haftmann@54744
   557
lemma dual_min:
haftmann@54744
   558
  "ord.min greater_eq = max"
haftmann@54744
   559
  by (auto simp add: ord.min_def max_def fun_eq_iff)
haftmann@54744
   560
haftmann@54744
   561
lemma dual_max:
haftmann@54744
   562
  "ord.max greater_eq = min"
haftmann@54744
   563
  by (auto simp add: ord.max_def min_def fun_eq_iff)
haftmann@54744
   564
haftmann@54744
   565
lemma dual_Min:
haftmann@54744
   566
  "linorder.Min greater_eq = Max"
haftmann@54744
   567
proof -
haftmann@54744
   568
  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
haftmann@54744
   569
  show ?thesis by (simp add: dual.Min_def dual_min Max_def)
haftmann@54744
   570
qed
haftmann@54744
   571
haftmann@54744
   572
lemma dual_Max:
haftmann@54744
   573
  "linorder.Max greater_eq = Min"
haftmann@54744
   574
proof -
haftmann@54744
   575
  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
haftmann@54744
   576
  show ?thesis by (simp add: dual.Max_def dual_max Min_def)
haftmann@54744
   577
qed
haftmann@54744
   578
haftmann@54744
   579
lemmas Min_singleton = Min.singleton
haftmann@54744
   580
lemmas Max_singleton = Max.singleton
haftmann@54744
   581
lemmas Min_insert = Min.insert
haftmann@54744
   582
lemmas Max_insert = Max.insert
haftmann@54744
   583
lemmas Min_Un = Min.union
haftmann@54744
   584
lemmas Max_Un = Max.union
haftmann@54744
   585
lemmas hom_Min_commute = Min.hom_commute
haftmann@54744
   586
lemmas hom_Max_commute = Max.hom_commute
haftmann@54744
   587
haftmann@54744
   588
lemma Min_in [simp]:
haftmann@54744
   589
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   590
  shows "Min A \<in> A"
haftmann@54744
   591
  using assms by (auto simp add: min_def Min.closed)
haftmann@54744
   592
haftmann@54744
   593
lemma Max_in [simp]:
haftmann@54744
   594
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   595
  shows "Max A \<in> A"
haftmann@54744
   596
  using assms by (auto simp add: max_def Max.closed)
haftmann@54744
   597
haftmann@54744
   598
lemma Min_le [simp]:
haftmann@54744
   599
  assumes "finite A" and "x \<in> A"
haftmann@54744
   600
  shows "Min A \<le> x"
haftmann@54744
   601
  using assms by (fact Min.coboundedI)
haftmann@54744
   602
haftmann@54744
   603
lemma Max_ge [simp]:
haftmann@54744
   604
  assumes "finite A" and "x \<in> A"
haftmann@54744
   605
  shows "x \<le> Max A"
haftmann@54744
   606
  using assms by (fact Max.coboundedI)
haftmann@54744
   607
haftmann@54744
   608
lemma Min_eqI:
haftmann@54744
   609
  assumes "finite A"
haftmann@54744
   610
  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
haftmann@54744
   611
    and "x \<in> A"
haftmann@54744
   612
  shows "Min A = x"
haftmann@54744
   613
proof (rule antisym)
haftmann@54744
   614
  from `x \<in> A` have "A \<noteq> {}" by auto
haftmann@54744
   615
  with assms show "Min A \<ge> x" by simp
haftmann@54744
   616
next
haftmann@54744
   617
  from assms show "x \<ge> Min A" by simp
haftmann@54744
   618
qed
haftmann@54744
   619
haftmann@54744
   620
lemma Max_eqI:
haftmann@54744
   621
  assumes "finite A"
haftmann@54744
   622
  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
haftmann@54744
   623
    and "x \<in> A"
haftmann@54744
   624
  shows "Max A = x"
haftmann@54744
   625
proof (rule antisym)
haftmann@54744
   626
  from `x \<in> A` have "A \<noteq> {}" by auto
haftmann@54744
   627
  with assms show "Max A \<le> x" by simp
haftmann@54744
   628
next
haftmann@54744
   629
  from assms show "x \<le> Max A" by simp
haftmann@54744
   630
qed
haftmann@54744
   631
haftmann@54744
   632
context
haftmann@54744
   633
  fixes A :: "'a set"
haftmann@54744
   634
  assumes fin_nonempty: "finite A" "A \<noteq> {}"
haftmann@54744
   635
begin
haftmann@54744
   636
haftmann@54744
   637
lemma Min_ge_iff [simp]:
haftmann@54744
   638
  "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
haftmann@54744
   639
  using fin_nonempty by (fact Min.bounded_iff)
haftmann@54744
   640
haftmann@54744
   641
lemma Max_le_iff [simp]:
haftmann@54744
   642
  "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
haftmann@54744
   643
  using fin_nonempty by (fact Max.bounded_iff)
haftmann@54744
   644
haftmann@54744
   645
lemma Min_gr_iff [simp]:
haftmann@54744
   646
  "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
haftmann@54744
   647
  using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
haftmann@54744
   648
haftmann@54744
   649
lemma Max_less_iff [simp]:
haftmann@54744
   650
  "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
haftmann@54744
   651
  using fin_nonempty by (induct rule: finite_ne_induct) simp_all
haftmann@54744
   652
haftmann@54744
   653
lemma Min_le_iff:
haftmann@54744
   654
  "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
haftmann@54744
   655
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
haftmann@54744
   656
haftmann@54744
   657
lemma Max_ge_iff:
haftmann@54744
   658
  "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
haftmann@54744
   659
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
haftmann@54744
   660
haftmann@54744
   661
lemma Min_less_iff:
haftmann@54744
   662
  "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
haftmann@54744
   663
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
haftmann@54744
   664
haftmann@54744
   665
lemma Max_gr_iff:
haftmann@54744
   666
  "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
haftmann@54744
   667
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
haftmann@54744
   668
haftmann@54744
   669
end
haftmann@54744
   670
haftmann@54744
   671
lemma Min_antimono:
haftmann@54744
   672
  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
haftmann@54744
   673
  shows "Min N \<le> Min M"
haftmann@54744
   674
  using assms by (fact Min.antimono)
haftmann@54744
   675
haftmann@54744
   676
lemma Max_mono:
haftmann@54744
   677
  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
haftmann@54744
   678
  shows "Max M \<le> Max N"
haftmann@54744
   679
  using assms by (fact Max.antimono)
haftmann@54744
   680
haftmann@54744
   681
lemma mono_Min_commute:
haftmann@54744
   682
  assumes "mono f"
haftmann@54744
   683
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   684
  shows "f (Min A) = Min (f ` A)"
haftmann@54744
   685
proof (rule linorder_class.Min_eqI [symmetric])
haftmann@54744
   686
  from `finite A` show "finite (f ` A)" by simp
haftmann@54744
   687
  from assms show "f (Min A) \<in> f ` A" by simp
haftmann@54744
   688
  fix x
haftmann@54744
   689
  assume "x \<in> f ` A"
haftmann@54744
   690
  then obtain y where "y \<in> A" and "x = f y" ..
haftmann@54744
   691
  with assms have "Min A \<le> y" by auto
haftmann@54744
   692
  with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
haftmann@54744
   693
  with `x = f y` show "f (Min A) \<le> x" by simp
haftmann@54744
   694
qed
haftmann@54744
   695
haftmann@54744
   696
lemma mono_Max_commute:
haftmann@54744
   697
  assumes "mono f"
haftmann@54744
   698
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   699
  shows "f (Max A) = Max (f ` A)"
haftmann@54744
   700
proof (rule linorder_class.Max_eqI [symmetric])
haftmann@54744
   701
  from `finite A` show "finite (f ` A)" by simp
haftmann@54744
   702
  from assms show "f (Max A) \<in> f ` A" by simp
haftmann@54744
   703
  fix x
haftmann@54744
   704
  assume "x \<in> f ` A"
haftmann@54744
   705
  then obtain y where "y \<in> A" and "x = f y" ..
haftmann@54744
   706
  with assms have "y \<le> Max A" by auto
haftmann@54744
   707
  with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
haftmann@54744
   708
  with `x = f y` show "x \<le> f (Max A)" by simp
haftmann@54744
   709
qed
haftmann@54744
   710
haftmann@54744
   711
lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
haftmann@54744
   712
  assumes fin: "finite A"
haftmann@54744
   713
  and empty: "P {}" 
haftmann@54744
   714
  and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
haftmann@54744
   715
  shows "P A"
haftmann@54744
   716
using fin empty insert
haftmann@54744
   717
proof (induct rule: finite_psubset_induct)
haftmann@54744
   718
  case (psubset A)
haftmann@54744
   719
  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
   720
  have fin: "finite A" by fact 
haftmann@54744
   721
  have empty: "P {}" by fact
haftmann@54744
   722
  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
   723
  show "P A"
haftmann@54744
   724
  proof (cases "A = {}")
haftmann@54744
   725
    assume "A = {}" 
haftmann@54744
   726
    then show "P A" using `P {}` by simp
haftmann@54744
   727
  next
haftmann@54744
   728
    let ?B = "A - {Max A}" 
haftmann@54744
   729
    let ?A = "insert (Max A) ?B"
haftmann@54744
   730
    have "finite ?B" using `finite A` by simp
haftmann@54744
   731
    assume "A \<noteq> {}"
haftmann@54744
   732
    with `finite A` have "Max A : A" by auto
haftmann@54744
   733
    then have A: "?A = A" using insert_Diff_single insert_absorb by auto
haftmann@54744
   734
    then have "P ?B" using `P {}` step IH [of ?B] by blast
haftmann@54744
   735
    moreover 
haftmann@54744
   736
    have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
haftmann@54744
   737
    ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
haftmann@54744
   738
  qed
haftmann@54744
   739
qed
haftmann@54744
   740
haftmann@54744
   741
lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
haftmann@54744
   742
  "\<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
   743
  by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
haftmann@54744
   744
haftmann@54744
   745
lemma Least_Min:
haftmann@54744
   746
  assumes "finite {a. P a}" and "\<exists>a. P a"
haftmann@54744
   747
  shows "(LEAST a. P a) = Min {a. P a}"
haftmann@54744
   748
proof -
haftmann@54744
   749
  { fix A :: "'a set"
haftmann@54744
   750
    assume A: "finite A" "A \<noteq> {}"
haftmann@54744
   751
    have "(LEAST a. a \<in> A) = Min A"
haftmann@54744
   752
    using A proof (induct A rule: finite_ne_induct)
haftmann@54744
   753
      case singleton show ?case by (rule Least_equality) simp_all
haftmann@54744
   754
    next
haftmann@54744
   755
      case (insert a A)
haftmann@54744
   756
      have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
haftmann@54744
   757
        by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
haftmann@54744
   758
      with insert show ?case by simp
haftmann@54744
   759
    qed
haftmann@54744
   760
  } from this [of "{a. P a}"] assms show ?thesis by simp
haftmann@54744
   761
qed
haftmann@54744
   762
haftmann@54744
   763
end
haftmann@54744
   764
haftmann@54744
   765
context linordered_ab_semigroup_add
haftmann@54744
   766
begin
haftmann@54744
   767
haftmann@54744
   768
lemma add_Min_commute:
haftmann@54744
   769
  fixes k
haftmann@54744
   770
  assumes "finite N" and "N \<noteq> {}"
haftmann@54744
   771
  shows "k + Min N = Min {k + m | m. m \<in> N}"
haftmann@54744
   772
proof -
haftmann@54744
   773
  have "\<And>x y. k + min x y = min (k + x) (k + y)"
haftmann@54744
   774
    by (simp add: min_def not_le)
haftmann@54744
   775
      (blast intro: antisym less_imp_le add_left_mono)
haftmann@54744
   776
  with assms show ?thesis
haftmann@54744
   777
    using hom_Min_commute [of "plus k" N]
haftmann@54744
   778
    by simp (blast intro: arg_cong [where f = Min])
haftmann@54744
   779
qed
haftmann@54744
   780
haftmann@54744
   781
lemma add_Max_commute:
haftmann@54744
   782
  fixes k
haftmann@54744
   783
  assumes "finite N" and "N \<noteq> {}"
haftmann@54744
   784
  shows "k + Max N = Max {k + m | m. m \<in> N}"
haftmann@54744
   785
proof -
haftmann@54744
   786
  have "\<And>x y. k + max x y = max (k + x) (k + y)"
haftmann@54744
   787
    by (simp add: max_def not_le)
haftmann@54744
   788
      (blast intro: antisym less_imp_le add_left_mono)
haftmann@54744
   789
  with assms show ?thesis
haftmann@54744
   790
    using hom_Max_commute [of "plus k" N]
haftmann@54744
   791
    by simp (blast intro: arg_cong [where f = Max])
haftmann@54744
   792
qed
haftmann@54744
   793
haftmann@54744
   794
end
haftmann@54744
   795
haftmann@54744
   796
context linordered_ab_group_add
haftmann@54744
   797
begin
haftmann@54744
   798
haftmann@54744
   799
lemma minus_Max_eq_Min [simp]:
haftmann@54744
   800
  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
haftmann@54744
   801
  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
haftmann@54744
   802
haftmann@54744
   803
lemma minus_Min_eq_Max [simp]:
haftmann@54744
   804
  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
haftmann@54744
   805
  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
haftmann@54744
   806
haftmann@54744
   807
end
haftmann@54744
   808
haftmann@54744
   809
context complete_linorder
haftmann@54744
   810
begin
haftmann@54744
   811
haftmann@54744
   812
lemma Min_Inf:
haftmann@54744
   813
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   814
  shows "Min A = Inf A"
haftmann@54744
   815
proof -
haftmann@54744
   816
  from assms obtain b B where "A = insert b B" and "finite B" by auto
haftmann@54744
   817
  then show ?thesis
haftmann@54744
   818
    by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
haftmann@54744
   819
qed
haftmann@54744
   820
haftmann@54744
   821
lemma Max_Sup:
haftmann@54744
   822
  assumes "finite A" and "A \<noteq> {}"
haftmann@54744
   823
  shows "Max A = Sup A"
haftmann@54744
   824
proof -
haftmann@54744
   825
  from assms obtain b B where "A = insert b B" and "finite B" by auto
haftmann@54744
   826
  then show ?thesis
haftmann@54744
   827
    by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
haftmann@54744
   828
qed
haftmann@54744
   829
haftmann@54744
   830
end
haftmann@54744
   831
haftmann@54744
   832
end