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