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