src/HOL/Library/Dual_Ordered_Lattice.thy
 author haftmann Thu Mar 14 09:46:09 2019 +0100 (5 weeks ago) changeset 69909 5382f5691a11 child 69947 77a92e8d5167 permissions -rw-r--r--
proper theory for type of dual ordered lattice in distribution
 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 \Type of dual ordered lattices\ ``` 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 \ ``` haftmann@69909 ` 12` ``` The \<^emph>\dual\ of an ordered structure is an isomorphic copy of the ``` haftmann@69909 ` 13` ``` underlying type, with the \\\ 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` ```\ ``` 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 \ 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 \ 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 \ 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 \ 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 \Pointwise ordering\ ``` 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 \ 'a dual \ bool" ``` haftmann@69909 ` 94` ``` is "(\)" . ``` haftmann@69909 ` 95` haftmann@69909 ` 96` ```lift_definition less_dual :: "'a dual \ 'a dual \ 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 \ y" if "undual y \ 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 \ y \ undual y \ 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 \ dual y \ y \ 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 \ 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 \ 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 \Binary infimum and supremum\ ``` 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 \ 'a dual \ '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 \ 'a dual \ '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 \Top and bottom elements\ ``` 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 \Complement\ ``` 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 \ '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 \ 'a dual \ 'a dual" ``` haftmann@69909 ` 259` ``` is "\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 \Complete lattice operations\ ``` haftmann@69909 ` 276` haftmann@69909 ` 277` ```text \ ``` haftmann@69909 ` 278` ``` The class of complete lattices is closed under formation of dual ``` haftmann@69909 ` 279` ``` structures. ``` haftmann@69909 ` 280` ```\ ``` 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 \ '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 \ '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 \ 'a" ``` haftmann@69909 ` 323` ``` and g :: "'a dual \ 'a dual" ``` haftmann@69909 ` 324` ``` assumes "mono f" ``` haftmann@69909 ` 325` ``` defines "g \ dual \ f \ 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 \ y" ``` haftmann@69909 ` 333` ``` then have "undual y \ undual x" ``` haftmann@69909 ` 334` ``` by (simp add: dual_less_eq_iff) ``` haftmann@69909 ` 335` ``` with \mono f\ have "f (undual y) \ f (undual x)" ``` haftmann@69909 ` 336` ``` by (rule monoD) ``` haftmann@69909 ` 337` ``` then have "(dual \ f \ undual) x \ (dual \ f \ undual) y" ``` haftmann@69909 ` 338` ``` by simp ``` haftmann@69909 ` 339` ``` then show "g x \ 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))) \ dual (f (undual (gfp g)))" ``` haftmann@69909 ` 347` ``` by (simp add: g_def) ``` haftmann@69909 ` 348` ``` with mono_dual have "f (undual (gfp g)) \ 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 \ ?rhs" ``` haftmann@69909 ` 351` ``` by (rule lfp_lowerbound) ``` haftmann@69909 ` 352` ``` from \mono f\ have "dual (lfp f) \ dual (undual (gfp g))" ``` haftmann@69909 ` 353` ``` by (simp add: lfp_fixpoint gfp_upperbound g_def) ``` haftmann@69909 ` 354` ``` then show "?rhs \ ?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 (\x. undual (undual x))" ``` haftmann@69909 ` 362` ``` by (rule monoI) (simp add: dual_less_eq_iff) ``` haftmann@69909 ` 363` ``` moreover have "mono (\a. dual (dual (f a)))" ``` haftmann@69909 ` 364` ``` using \mono f\ by (auto intro: monoI dest: monoD) ``` haftmann@69909 ` 365` ``` moreover have "gfp f = gfp (\x. undual (undual (dual (dual (f x)))))" ``` haftmann@69909 ` 366` ``` by simp ``` haftmann@69909 ` 367` ``` ultimately have "undual (undual (gfp (\x. dual ``` haftmann@69909 ` 368` ``` (dual (f (undual (undual x))))))) = ``` haftmann@69909 ` 369` ``` gfp (\x. undual (undual (dual (dual (f x)))))" ``` haftmann@69909 ` 370` ``` by (subst gfp_rolling [where g = "\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 (\x. dual (dual (f (undual (undual x)))))))" ``` haftmann@69909 ` 375` ``` by simp ``` haftmann@69909 ` 376` ``` also have "\ = undual (undual (gfp (dual \ g \ undual)))" ``` haftmann@69909 ` 377` ``` by (simp add: comp_def g_def) ``` haftmann@69909 ` 378` ``` also have "\ = 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 \Finally\ ``` haftmann@69909 ` 387` haftmann@69909 ` 388` ```lifting_update dual.lifting ``` haftmann@69909 ` 389` ```lifting_forget dual.lifting ``` haftmann@69909 ` 390` haftmann@69909 ` 391` ```end ```