src/HOL/Library/Dual_Ordered_Lattice.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69909 5382f5691a11
child 69947 77a92e8d5167
permissions -rw-r--r--
improved code equations taken over from AFP
haftmann@69909
     1
(*  Title:      Dual_Ordered_Lattice.thy
haftmann@69909
     2
    Authors:    Makarius; Peter Gammie; Brian Huffman; Florian Haftmann, TU Muenchen
haftmann@69909
     3
*)
haftmann@69909
     4
haftmann@69909
     5
section \<open>Type of dual ordered lattices\<close>
haftmann@69909
     6
haftmann@69909
     7
theory Dual_Ordered_Lattice
haftmann@69909
     8
imports Main
haftmann@69909
     9
begin
haftmann@69909
    10
haftmann@69909
    11
text \<open>
haftmann@69909
    12
  The \<^emph>\<open>dual\<close> of an ordered structure is an isomorphic copy of the
haftmann@69909
    13
  underlying type, with the \<open>\<le>\<close> relation defined as the inverse
haftmann@69909
    14
  of the original one.
haftmann@69909
    15
haftmann@69909
    16
  The class of lattices is closed under formation of dual structures.
haftmann@69909
    17
  This means that for any theorem of lattice theory, the dualized
haftmann@69909
    18
  statement holds as well; this important fact simplifies many proofs
haftmann@69909
    19
  of lattice theory.
haftmann@69909
    20
\<close>
haftmann@69909
    21
haftmann@69909
    22
typedef 'a dual = "UNIV :: 'a set"
haftmann@69909
    23
  morphisms undual dual ..
haftmann@69909
    24
haftmann@69909
    25
setup_lifting type_definition_dual
haftmann@69909
    26
haftmann@69909
    27
lemma dual_eqI:
haftmann@69909
    28
  "x = y" if "undual x = undual y"
haftmann@69909
    29
  using that by transfer assumption
haftmann@69909
    30
haftmann@69909
    31
lemma dual_eq_iff:
haftmann@69909
    32
  "x = y \<longleftrightarrow> undual x = undual y"
haftmann@69909
    33
  by transfer simp
haftmann@69909
    34
haftmann@69909
    35
lemma eq_dual_iff [iff]:
haftmann@69909
    36
  "dual x = dual y \<longleftrightarrow> x = y"
haftmann@69909
    37
  by transfer simp
haftmann@69909
    38
haftmann@69909
    39
lemma undual_dual [simp]:
haftmann@69909
    40
  "undual (dual x) = x"
haftmann@69909
    41
  by transfer rule
haftmann@69909
    42
haftmann@69909
    43
lemma dual_undual [simp]:
haftmann@69909
    44
  "dual (undual x) = x"
haftmann@69909
    45
  by transfer rule
haftmann@69909
    46
haftmann@69909
    47
lemma undual_comp_dual [simp]:
haftmann@69909
    48
  "undual \<circ> dual = id"
haftmann@69909
    49
  by (simp add: fun_eq_iff)
haftmann@69909
    50
haftmann@69909
    51
lemma dual_comp_undual [simp]:
haftmann@69909
    52
  "dual \<circ> undual = id"
haftmann@69909
    53
  by (simp add: fun_eq_iff)
haftmann@69909
    54
haftmann@69909
    55
lemma inj_dual:
haftmann@69909
    56
  "inj dual"
haftmann@69909
    57
  by (rule injI) simp
haftmann@69909
    58
haftmann@69909
    59
lemma inj_undual:
haftmann@69909
    60
  "inj undual"
haftmann@69909
    61
  by (rule injI) (rule dual_eqI)
haftmann@69909
    62
haftmann@69909
    63
lemma surj_dual:
haftmann@69909
    64
  "surj dual"
haftmann@69909
    65
  by (rule surjI [of _ undual]) simp
haftmann@69909
    66
haftmann@69909
    67
lemma surj_undual:
haftmann@69909
    68
  "surj undual"
haftmann@69909
    69
  by (rule surjI [of _ dual]) simp
haftmann@69909
    70
haftmann@69909
    71
lemma bij_dual:
haftmann@69909
    72
  "bij dual"
haftmann@69909
    73
  using inj_dual surj_dual by (rule bijI)
haftmann@69909
    74
haftmann@69909
    75
lemma bij_undual:
haftmann@69909
    76
  "bij undual"
haftmann@69909
    77
  using inj_undual surj_undual by (rule bijI)
haftmann@69909
    78
haftmann@69909
    79
instance dual :: (finite) finite
haftmann@69909
    80
proof
haftmann@69909
    81
  from finite have "finite (range dual :: 'a dual set)"
haftmann@69909
    82
    by (rule finite_imageI)
haftmann@69909
    83
  then show "finite (UNIV :: 'a dual set)"
haftmann@69909
    84
    by (simp add: surj_dual)
haftmann@69909
    85
qed
haftmann@69909
    86
haftmann@69909
    87
haftmann@69909
    88
subsection \<open>Pointwise ordering\<close>
haftmann@69909
    89
haftmann@69909
    90
instantiation dual :: (ord) ord
haftmann@69909
    91
begin
haftmann@69909
    92
haftmann@69909
    93
lift_definition less_eq_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool"
haftmann@69909
    94
  is "(\<ge>)" .
haftmann@69909
    95
haftmann@69909
    96
lift_definition less_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool"
haftmann@69909
    97
  is "(>)" .
haftmann@69909
    98
haftmann@69909
    99
instance ..
haftmann@69909
   100
haftmann@69909
   101
end
haftmann@69909
   102
haftmann@69909
   103
lemma dual_less_eqI:
haftmann@69909
   104
  "x \<le> y" if "undual y \<le> undual x"
haftmann@69909
   105
  using that by transfer assumption
haftmann@69909
   106
haftmann@69909
   107
lemma dual_less_eq_iff:
haftmann@69909
   108
  "x \<le> y \<longleftrightarrow> undual y \<le> undual x"
haftmann@69909
   109
  by transfer simp
haftmann@69909
   110
haftmann@69909
   111
lemma less_eq_dual_iff [iff]:
haftmann@69909
   112
  "dual x \<le> dual y \<longleftrightarrow> y \<le> x"
haftmann@69909
   113
  by transfer simp
haftmann@69909
   114
haftmann@69909
   115
lemma dual_lessI:
haftmann@69909
   116
  "x < y" if "undual y < undual x"
haftmann@69909
   117
  using that by transfer assumption
haftmann@69909
   118
haftmann@69909
   119
lemma dual_less_iff:
haftmann@69909
   120
  "x < y \<longleftrightarrow> undual y < undual x"
haftmann@69909
   121
  by transfer simp
haftmann@69909
   122
haftmann@69909
   123
lemma less_dual_iff [iff]:
haftmann@69909
   124
  "dual x < dual y \<longleftrightarrow> y < x"
haftmann@69909
   125
  by transfer simp
haftmann@69909
   126
haftmann@69909
   127
instance dual :: (preorder) preorder
haftmann@69909
   128
  by (standard; transfer) (auto simp add: less_le_not_le intro: order_trans)
haftmann@69909
   129
haftmann@69909
   130
instance dual :: (order) order
haftmann@69909
   131
  by (standard; transfer) simp
haftmann@69909
   132
haftmann@69909
   133
haftmann@69909
   134
subsection \<open>Binary infimum and supremum\<close>
haftmann@69909
   135
haftmann@69909
   136
instantiation dual :: (sup) inf
haftmann@69909
   137
begin
haftmann@69909
   138
haftmann@69909
   139
lift_definition inf_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> 'a dual"
haftmann@69909
   140
  is sup .
haftmann@69909
   141
haftmann@69909
   142
instance ..
haftmann@69909
   143
haftmann@69909
   144
end
haftmann@69909
   145
haftmann@69909
   146
lemma undual_inf_eq [simp]:
haftmann@69909
   147
  "undual (inf x y) = sup (undual x) (undual y)"
haftmann@69909
   148
  by (fact inf_dual.rep_eq)
haftmann@69909
   149
haftmann@69909
   150
lemma dual_sup_eq [simp]:
haftmann@69909
   151
  "dual (sup x y) = inf (dual x) (dual y)"
haftmann@69909
   152
  by transfer rule
haftmann@69909
   153
haftmann@69909
   154
instantiation dual :: (inf) sup
haftmann@69909
   155
begin
haftmann@69909
   156
haftmann@69909
   157
lift_definition sup_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> 'a dual"
haftmann@69909
   158
  is inf .
haftmann@69909
   159
haftmann@69909
   160
instance ..
haftmann@69909
   161
haftmann@69909
   162
end
haftmann@69909
   163
haftmann@69909
   164
lemma undual_sup_eq [simp]:
haftmann@69909
   165
  "undual (sup x y) = inf (undual x) (undual y)"
haftmann@69909
   166
  by (fact sup_dual.rep_eq)
haftmann@69909
   167
haftmann@69909
   168
lemma dual_inf_eq [simp]:
haftmann@69909
   169
  "dual (inf x y) = sup (dual x) (dual y)"
haftmann@69909
   170
  by transfer simp
haftmann@69909
   171
haftmann@69909
   172
instance dual :: (semilattice_sup) semilattice_inf
haftmann@69909
   173
  by (standard; transfer) simp_all
haftmann@69909
   174
haftmann@69909
   175
instance dual :: (semilattice_inf) semilattice_sup
haftmann@69909
   176
  by (standard; transfer) simp_all
haftmann@69909
   177
haftmann@69909
   178
instance dual :: (lattice) lattice ..
haftmann@69909
   179
haftmann@69909
   180
instance dual :: (distrib_lattice) distrib_lattice
haftmann@69909
   181
  by (standard; transfer) (fact inf_sup_distrib1)
haftmann@69909
   182
haftmann@69909
   183
haftmann@69909
   184
subsection \<open>Top and bottom elements\<close>
haftmann@69909
   185
haftmann@69909
   186
instantiation dual :: (top) bot
haftmann@69909
   187
begin
haftmann@69909
   188
haftmann@69909
   189
lift_definition bot_dual :: "'a dual"
haftmann@69909
   190
  is top .
haftmann@69909
   191
haftmann@69909
   192
instance ..
haftmann@69909
   193
haftmann@69909
   194
end
haftmann@69909
   195
haftmann@69909
   196
lemma undual_bot_eq [simp]:
haftmann@69909
   197
  "undual bot = top"
haftmann@69909
   198
  by (fact bot_dual.rep_eq)
haftmann@69909
   199
haftmann@69909
   200
lemma dual_top_eq [simp]:
haftmann@69909
   201
  "dual top = bot"
haftmann@69909
   202
  by transfer rule
haftmann@69909
   203
haftmann@69909
   204
instantiation dual :: (bot) top
haftmann@69909
   205
begin
haftmann@69909
   206
haftmann@69909
   207
lift_definition top_dual :: "'a dual"
haftmann@69909
   208
  is bot .
haftmann@69909
   209
haftmann@69909
   210
instance ..
haftmann@69909
   211
haftmann@69909
   212
end
haftmann@69909
   213
haftmann@69909
   214
lemma undual_top_eq [simp]:
haftmann@69909
   215
  "undual top = bot"
haftmann@69909
   216
  by (fact top_dual.rep_eq)
haftmann@69909
   217
haftmann@69909
   218
lemma dual_bot_eq [simp]:
haftmann@69909
   219
  "dual bot = top"
haftmann@69909
   220
  by transfer rule
haftmann@69909
   221
haftmann@69909
   222
instance dual :: (order_top) order_bot
haftmann@69909
   223
  by (standard; transfer) simp
haftmann@69909
   224
haftmann@69909
   225
instance dual :: (order_bot) order_top
haftmann@69909
   226
  by (standard; transfer) simp
haftmann@69909
   227
haftmann@69909
   228
instance dual :: (bounded_lattice_top) bounded_lattice_bot ..
haftmann@69909
   229
haftmann@69909
   230
instance dual :: (bounded_lattice_bot) bounded_lattice_top ..
haftmann@69909
   231
haftmann@69909
   232
instance dual :: (bounded_lattice) bounded_lattice ..
haftmann@69909
   233
haftmann@69909
   234
haftmann@69909
   235
subsection \<open>Complement\<close>
haftmann@69909
   236
haftmann@69909
   237
instantiation dual :: (uminus) uminus
haftmann@69909
   238
begin
haftmann@69909
   239
haftmann@69909
   240
lift_definition uminus_dual :: "'a dual \<Rightarrow> 'a dual"
haftmann@69909
   241
  is uminus .
haftmann@69909
   242
haftmann@69909
   243
instance ..
haftmann@69909
   244
haftmann@69909
   245
end
haftmann@69909
   246
haftmann@69909
   247
lemma undual_uminus_eq [simp]:
haftmann@69909
   248
  "undual (- x) = - undual x"
haftmann@69909
   249
  by (fact uminus_dual.rep_eq)
haftmann@69909
   250
haftmann@69909
   251
lemma dual_uminus_eq [simp]:
haftmann@69909
   252
  "dual (- x) = - dual x"
haftmann@69909
   253
  by transfer rule
haftmann@69909
   254
haftmann@69909
   255
instantiation dual :: (boolean_algebra) boolean_algebra
haftmann@69909
   256
begin
haftmann@69909
   257
haftmann@69909
   258
lift_definition minus_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> 'a dual"
haftmann@69909
   259
  is "\<lambda>x y. - (y - x)" .
haftmann@69909
   260
haftmann@69909
   261
instance
haftmann@69909
   262
  by (standard; transfer) (simp_all add: diff_eq ac_simps)
haftmann@69909
   263
haftmann@69909
   264
end
haftmann@69909
   265
haftmann@69909
   266
lemma undual_minus_eq [simp]:
haftmann@69909
   267
  "undual (x - y) = - (undual y - undual x)"
haftmann@69909
   268
  by (fact minus_dual.rep_eq)
haftmann@69909
   269
haftmann@69909
   270
lemma dual_minus_eq [simp]:
haftmann@69909
   271
  "dual (x - y) = - (dual y - dual x)"
haftmann@69909
   272
  by transfer simp
haftmann@69909
   273
haftmann@69909
   274
haftmann@69909
   275
subsection \<open>Complete lattice operations\<close>
haftmann@69909
   276
haftmann@69909
   277
text \<open>
haftmann@69909
   278
  The class of complete lattices is closed under formation of dual
haftmann@69909
   279
  structures.
haftmann@69909
   280
\<close>
haftmann@69909
   281
haftmann@69909
   282
instantiation dual :: (Sup) Inf
haftmann@69909
   283
begin
haftmann@69909
   284
haftmann@69909
   285
lift_definition Inf_dual :: "'a dual set \<Rightarrow> 'a dual"
haftmann@69909
   286
  is Sup .
haftmann@69909
   287
haftmann@69909
   288
instance ..
haftmann@69909
   289
haftmann@69909
   290
end
haftmann@69909
   291
haftmann@69909
   292
lemma undual_Inf_eq [simp]:
haftmann@69909
   293
  "undual (Inf A) = Sup (undual ` A)"
haftmann@69909
   294
  by (fact Inf_dual.rep_eq)
haftmann@69909
   295
haftmann@69909
   296
lemma dual_Sup_eq [simp]:
haftmann@69909
   297
  "dual (Sup A) = Inf (dual ` A)"
haftmann@69909
   298
  by transfer simp
haftmann@69909
   299
haftmann@69909
   300
instantiation dual :: (Inf) Sup
haftmann@69909
   301
begin
haftmann@69909
   302
haftmann@69909
   303
lift_definition Sup_dual :: "'a dual set \<Rightarrow> 'a dual"
haftmann@69909
   304
  is Inf .
haftmann@69909
   305
haftmann@69909
   306
instance ..
haftmann@69909
   307
haftmann@69909
   308
end
haftmann@69909
   309
haftmann@69909
   310
lemma undual_Sup_eq [simp]:
haftmann@69909
   311
  "undual (Sup A) = Inf (undual ` A)"
haftmann@69909
   312
  by (fact Sup_dual.rep_eq)
haftmann@69909
   313
haftmann@69909
   314
lemma dual_Inf_eq [simp]:
haftmann@69909
   315
  "dual (Inf A) = Sup (dual ` A)"
haftmann@69909
   316
  by transfer simp
haftmann@69909
   317
haftmann@69909
   318
instance dual :: (complete_lattice) complete_lattice
haftmann@69909
   319
  by (standard; transfer) (auto intro: Inf_lower Sup_upper Inf_greatest Sup_least)
haftmann@69909
   320
haftmann@69909
   321
context
haftmann@69909
   322
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
haftmann@69909
   323
    and g :: "'a dual \<Rightarrow> 'a dual"
haftmann@69909
   324
  assumes "mono f"
haftmann@69909
   325
  defines "g \<equiv> dual \<circ> f \<circ> undual"
haftmann@69909
   326
begin
haftmann@69909
   327
haftmann@69909
   328
private lemma mono_dual:
haftmann@69909
   329
  "mono g"
haftmann@69909
   330
proof
haftmann@69909
   331
  fix x y :: "'a dual"
haftmann@69909
   332
  assume "x \<le> y"
haftmann@69909
   333
  then have "undual y \<le> undual x"
haftmann@69909
   334
    by (simp add: dual_less_eq_iff)
haftmann@69909
   335
  with \<open>mono f\<close> have "f (undual y) \<le> f (undual x)"
haftmann@69909
   336
    by (rule monoD)
haftmann@69909
   337
  then have "(dual \<circ> f \<circ> undual) x \<le> (dual \<circ> f \<circ> undual) y"
haftmann@69909
   338
    by simp
haftmann@69909
   339
  then show "g x \<le> g y"
haftmann@69909
   340
    by (simp add: g_def)
haftmann@69909
   341
qed
haftmann@69909
   342
haftmann@69909
   343
lemma lfp_dual_gfp:
haftmann@69909
   344
  "lfp f = undual (gfp g)" (is "?lhs = ?rhs")
haftmann@69909
   345
proof (rule antisym)
haftmann@69909
   346
  have "dual (undual (g (gfp g))) \<le> dual (f (undual (gfp g)))"
haftmann@69909
   347
    by (simp add: g_def)
haftmann@69909
   348
  with mono_dual have "f (undual (gfp g)) \<le> undual (gfp g)"
haftmann@69909
   349
    by (simp add: gfp_unfold [where f = g, symmetric] dual_less_eq_iff)
haftmann@69909
   350
  then show "?lhs \<le> ?rhs"
haftmann@69909
   351
    by (rule lfp_lowerbound)
haftmann@69909
   352
  from \<open>mono f\<close> have "dual (lfp f) \<le> dual (undual (gfp g))"
haftmann@69909
   353
    by (simp add: lfp_fixpoint gfp_upperbound g_def)
haftmann@69909
   354
  then show "?rhs \<le> ?lhs"
haftmann@69909
   355
    by (simp only: less_eq_dual_iff)
haftmann@69909
   356
qed
haftmann@69909
   357
haftmann@69909
   358
lemma gfp_dual_lfp:
haftmann@69909
   359
  "gfp f = undual (lfp g)"
haftmann@69909
   360
proof -
haftmann@69909
   361
  have "mono (\<lambda>x. undual (undual x))"
haftmann@69909
   362
    by (rule monoI)  (simp add: dual_less_eq_iff)
haftmann@69909
   363
  moreover have "mono (\<lambda>a. dual (dual (f a)))"
haftmann@69909
   364
    using \<open>mono f\<close> by (auto intro: monoI dest: monoD)
haftmann@69909
   365
  moreover have "gfp f = gfp (\<lambda>x. undual (undual (dual (dual (f x)))))"
haftmann@69909
   366
    by simp
haftmann@69909
   367
  ultimately have "undual (undual (gfp (\<lambda>x. dual
haftmann@69909
   368
    (dual (f (undual (undual x))))))) =
haftmann@69909
   369
      gfp (\<lambda>x. undual (undual (dual (dual (f x)))))"
haftmann@69909
   370
    by (subst gfp_rolling [where g = "\<lambda>x. undual (undual x)"]) simp_all
haftmann@69909
   371
  then have "gfp f =
haftmann@69909
   372
    undual
haftmann@69909
   373
     (undual
haftmann@69909
   374
       (gfp (\<lambda>x. dual (dual (f (undual (undual x)))))))"
haftmann@69909
   375
    by simp
haftmann@69909
   376
  also have "\<dots> = undual (undual (gfp (dual \<circ> g \<circ> undual)))"
haftmann@69909
   377
    by (simp add: comp_def g_def)
haftmann@69909
   378
  also have "\<dots> = undual (lfp g)"
haftmann@69909
   379
    using mono_dual by (simp only: Dual_Ordered_Lattice.lfp_dual_gfp)
haftmann@69909
   380
  finally show ?thesis .
haftmann@69909
   381
qed
haftmann@69909
   382
haftmann@69909
   383
end
haftmann@69909
   384
haftmann@69909
   385
haftmann@69909
   386
text \<open>Finally\<close>
haftmann@69909
   387
haftmann@69909
   388
lifting_update dual.lifting
haftmann@69909
   389
lifting_forget dual.lifting
haftmann@69909
   390
haftmann@69909
   391
end