diff --git a/thys/Order_Lattice_Props/Closure_Operators.thy b/thys/Order_Lattice_Props/Closure_Operators.thy
--- a/thys/Order_Lattice_Props/Closure_Operators.thy
+++ b/thys/Order_Lattice_Props/Closure_Operators.thy
@@ -1,514 +1,516 @@
 (* 
   Title: Closure and Co-Closure Operators
   Author: Georg Struth 
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
 *)
 
 section \<open>Closure and Co-Closure Operators\<close>
 
 theory Closure_Operators
   imports Galois_Connections 
 
 begin
 
 subsection \<open>Closure Operators\<close>
 
 text \<open>Closure and coclosure operators in orders and complete lattices are defined in this section,
 and some basic properties are proved. Isabelle infers the appropriate types. Facts are 
 taken mainly from the Compendium of Continuous Lattices~\<^cite>\<open>"GierzHKLMS80"\<close> and 
 Rosenthal's book on quantales~\<^cite>\<open>"Rosenthal90"\<close>.\<close>
 
 definition clop :: "('a::order \<Rightarrow> 'a) \<Rightarrow> bool" where
   "clop f = (id \<le> f \<and> mono f \<and> f \<circ> f \<le> f)"
 
 lemma clop_extensive: "clop f \<Longrightarrow> id \<le> f"
   by (simp add: clop_def)
 
 lemma clop_extensive_var: "clop f \<Longrightarrow> x \<le> f x"
   by (simp add: clop_def le_fun_def)
 
 lemma clop_iso: "clop f \<Longrightarrow> mono f"
   by (simp add: clop_def)
 
 lemma clop_iso_var: "clop f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   by (simp add: clop_def mono_def)
 
 lemma clop_idem: "clop f \<Longrightarrow> f \<circ> f = f"
   by (simp add: antisym clop_def le_fun_def)
 
 lemma clop_Fix_range: "clop f \<Longrightarrow> (Fix f = range f)"
   by (simp add: clop_idem retraction_prop_fix)
 
 lemma clop_idem_var: "clop f \<Longrightarrow> f (f x) = f x"
   by (simp add: clop_idem retraction_prop)
 
 lemma clop_Inf_closed_var: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a" 
   shows "clop f \<Longrightarrow> f \<circ> Inf \<circ> (`) f  = Inf \<circ> (`) f"    
   unfolding clop_def mono_def comp_def le_fun_def 
   by (metis (mono_tags, lifting) antisym id_apply le_INF_iff order_refl)
 
 lemma clop_top:
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows "clop f \<Longrightarrow> f \<top> = \<top>"
   by (simp add: clop_extensive_var top.extremum_uniqueI)
 
 lemma "clop (f::'a::complete_lattice \<Rightarrow> 'a) \<Longrightarrow> f (\<Squnion>x \<in> X. f x) = (\<Squnion>x \<in> X. f x)" (*nitpick*)
   oops
 
 lemma "clop (f::'a::complete_lattice \<Rightarrow> 'a) \<Longrightarrow> f (f x \<squnion> f y) = f x \<squnion> f y" (*nitpick*)
   oops
 
 lemma  "clop (f::'a::complete_lattice \<Rightarrow> 'a) \<Longrightarrow> f \<bottom> = \<bottom>" (*nitpick *)
   oops
   
 lemma "clop (f::'a set \<Rightarrow> 'a set) \<Longrightarrow> f (\<Squnion>x \<in> X. f x) = (\<Squnion>x \<in> X. f x)" (*nitpick*)
   oops
 
 lemma "clop (f::'a set \<Rightarrow> 'a set) \<Longrightarrow> f (f x \<squnion> f y) = f x \<squnion> f y" (*nitpick*)
   oops
 
 lemma  "clop (f::'a set \<Rightarrow> 'a set) \<Longrightarrow> f \<bottom> = \<bottom>" (*nitpick *)
   oops
 
 lemma clop_closure: "clop f \<Longrightarrow> (x \<in> range f) = (f x = x)"
   by (simp add: clop_idem retraction_prop)
 
 lemma clop_closure_set: "clop f \<Longrightarrow> range f = Fix f"
   by (simp add: clop_Fix_range)
 
 lemma clop_closure_prop: "(clop::('a::complete_lattice_with_dual\<Rightarrow> 'a) \<Rightarrow> bool) (Inf \<circ> \<up>)"
   by (simp add: clop_def mono_def)
 
 lemma clop_closure_prop_var: "clop (\<lambda>x::'a::complete_lattice. \<Sqinter>{y. x \<le> y})"
   unfolding clop_def comp_def le_fun_def mono_def by (simp add: Inf_lower le_Inf_iff)
 
 lemma clop_alt: "(clop f) = (\<forall>x y. x \<le> f y \<longleftrightarrow> f x \<le> f y)"
   unfolding clop_def mono_def le_fun_def comp_def id_def by (meson dual_order.refl order_trans)
 
 text \<open>Finally it is shown that adjoints in a Galois connection yield closure operators.\<close>
 
 lemma clop_adj: 
   fixes f :: "'a::order \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> clop (g \<circ> f)"
   by (simp add: adj_cancel2 adj_idem2 adj_iso4 clop_def)
 
 text \<open>Closure operators are monads for posets, and monads arise from adjunctions. 
 This fact is not formalised at this point. But here is the first step: every function 
 can be decomposed into a surjection followed by an injection.\<close>
 
 definition "surj_on f Y = (\<forall>y \<in> Y. \<exists>x. y = f x)"
 
 lemma surj_surj_on: "surj f \<Longrightarrow> surj_on f Y"
   by (simp add: surjD surj_on_def)
 
 lemma fun_surj_inj: "\<exists>g h. f = g \<circ> h \<and> surj_on h (range f) \<and> inj_on g (range f)"
 proof-
   obtain h where a: "\<forall>x. f x = h x"
     by blast
   then have "surj_on h (range f)"
     by (metis (mono_tags, lifting) imageE surj_on_def)
   then show ?thesis
     unfolding inj_on_def surj_on_def fun_eq_iff using a by auto
 qed
 
 text \<open>Connections between downsets, upsets and closure operators are outlined next.\<close>
 
 lemma preorder_clop: "clop (\<Down>::'a::preorder set \<Rightarrow> 'a set)"
   by (simp add: clop_def downset_set_ext downset_set_iso)
 
 lemma clop_preorder_aux: "clop f \<Longrightarrow> (x \<in> f {y} \<longleftrightarrow> f {x} \<subseteq> f {y})"
   by (simp add: clop_alt)
 
 lemma clop_preorder: "clop f \<Longrightarrow> class.preorder (\<lambda>x y. f {x} \<subseteq> f {y}) (\<lambda>x y. f {x} \<subset> f {y})"
   unfolding clop_def mono_def le_fun_def id_def comp_def by standard (auto simp: subset_not_subset_eq)
 
 lemma preorder_clop_dual: "clop (\<Up>::'a::preorder_with_dual set \<Rightarrow> 'a set)"
   by (simp add: clop_def upset_set_anti upset_set_ext)
 
 text \<open>The closed elements of any closure operator over a complete lattice form an Inf-closed set (a Moore family).\<close>
 
 lemma clop_Inf_closed: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows  "clop f \<Longrightarrow> Inf_closed_set (Fix f)" 
   unfolding clop_def Inf_closed_set_def mono_def le_fun_def comp_def id_def Fix_def
-  by (smt Inf_greatest Inf_lower antisym mem_Collect_eq subsetCE)
+  by (smt (verit) Inf_greatest Inf_lower antisym mem_Collect_eq subsetCE)
 
 lemma clop_top_Fix: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows  "clop f \<Longrightarrow> \<top> \<in> Fix f"
   by (simp add: clop_Fix_range clop_closure clop_top)
 
 
 text \<open>Conversely, every Inf-closed subset of a complete lattice is the set of fixpoints of some closure operator.\<close>
  
 lemma Inf_closed_clop: 
   fixes X :: "'a::complete_lattice set"
   shows "Inf_closed_set X \<Longrightarrow> clop (\<lambda>y. \<Sqinter>{x \<in> X. y \<le> x})"
-  by (smt Collect_mono_iff Inf_superset_mono clop_alt dual_order.trans le_Inf_iff mem_Collect_eq)
+  by (smt (verit) Collect_mono_iff Inf_superset_mono clop_alt dual_order.trans le_Inf_iff mem_Collect_eq)
 
 lemma Inf_closed_clop_var: 
   fixes X :: "'a::complete_lattice set"
   shows "clop f \<Longrightarrow> \<forall>x \<in> X. x \<in> range f \<Longrightarrow> \<Sqinter>X \<in> range f"
   by (metis Inf_closed_set_def clop_Fix_range clop_Inf_closed subsetI)
 
 text \<open>It is well known that downsets and upsets over an ordering form subalgebras of the complete powerset lattice.\<close>
 
 typedef (overloaded) 'a downsets = "range (\<Down>::'a::order set \<Rightarrow> 'a set)"
   by fastforce
 
 setup_lifting type_definition_downsets
 
 typedef (overloaded) 'a upsets = "range (\<Up>::'a::order set \<Rightarrow> 'a set)"
   by fastforce
 
 setup_lifting type_definition_upsets
 
 instantiation downsets :: (order) Inf_lattice
 begin
 
 lift_definition Inf_downsets :: "'a downsets set \<Rightarrow> 'a downsets" is "Abs_downsets \<circ> Inf \<circ> (`) Rep_downsets".
   
 lift_definition less_eq_downsets :: "'a downsets \<Rightarrow> 'a downsets \<Rightarrow> bool" is "\<lambda>X Y. Rep_downsets X \<subseteq> Rep_downsets Y".
 
 lift_definition less_downsets :: "'a downsets \<Rightarrow> 'a downsets \<Rightarrow> bool" is "\<lambda>X Y. Rep_downsets X \<subset> Rep_downsets Y".
 
 instance
   apply intro_classes 
       apply (transfer, simp)
      apply (transfer, blast)
     apply (simp add: Closure_Operators.less_eq_downsets.abs_eq Rep_downsets_inject)
-   apply (transfer, smt Abs_downsets_inverse INF_lower Inf_closed_clop_var Rep_downsets image_iff o_def preorder_clop)
-  by transfer (smt comp_def Abs_downsets_inverse Inf_closed_clop_var Rep_downsets image_iff le_INF_iff preorder_clop)
+   apply (transfer, smt (verit) Abs_downsets_inverse INF_lower Inf_closed_clop_var Rep_downsets image_iff o_def preorder_clop)
+  apply (transfer, smt (verit) comp_def Abs_downsets_inverse Inf_closed_clop_var Rep_downsets image_iff le_INF_iff preorder_clop)
+  done
 
 end
 
 instantiation upsets :: (order_with_dual) Inf_lattice
 begin
 
 lift_definition Inf_upsets :: "'a upsets set \<Rightarrow> 'a upsets" is "Abs_upsets \<circ> Inf \<circ> (`) Rep_upsets".
   
 lift_definition less_eq_upsets :: "'a upsets \<Rightarrow> 'a upsets \<Rightarrow> bool" is "\<lambda>X Y. Rep_upsets X \<subseteq> Rep_upsets Y".
 
 lift_definition less_upsets :: "'a upsets \<Rightarrow> 'a upsets \<Rightarrow> bool" is "\<lambda>X Y. Rep_upsets X \<subset> Rep_upsets Y".
 
 instance
   apply intro_classes
       apply (transfer, simp)
      apply (transfer, blast)
     apply (simp add: Closure_Operators.less_eq_upsets.abs_eq Rep_upsets_inject)
-   apply (transfer, smt Abs_upsets_inverse Inf_closed_clop_var Inf_lower Rep_upsets comp_apply image_iff preorder_clop_dual)
-  by transfer (smt comp_def Abs_upsets_inverse Inf_closed_clop_var Inter_iff Rep_upsets image_iff preorder_clop_dual subsetCE subsetI)
+   apply (transfer, smt (verit) Abs_upsets_inverse Inf_closed_clop_var Inf_lower Rep_upsets comp_apply image_iff preorder_clop_dual)
+  apply (transfer, smt (verit) comp_def Abs_upsets_inverse Inf_closed_clop_var Inter_iff Rep_upsets image_iff preorder_clop_dual subsetCE subsetI)
+  done
 
 end
 
 text \<open>It has already been shown in the section on representations that the map ds, which maps elements of the order to its downset, is an order 
 embedding. However, the duality between the underlying ordering and the lattices of up- and down-closed sets as categories can probably not be expressed, 
 as there is no easy access to contravariant functors. \<close>
 
 
 subsection \<open>Co-Closure Operators\<close>
                                 
 text \<open>Next, the co-closure (or kernel) operation satisfies dual laws.\<close>
 
 definition coclop :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool" where
   "coclop f = (f \<le> id \<and> mono f \<and> f \<le> f \<circ> f)"
 
 lemma coclop_dual: "(coclop::('a::order_with_dual \<Rightarrow> 'a) \<Rightarrow> bool) = clop \<circ> \<partial>\<^sub>F"
   unfolding coclop_def clop_def id_def mono_def map_dual_def comp_def fun_eq_iff le_fun_def
   by (metis invol_dual_var ord_dual)
 
 lemma coclop_dual_var: 
   fixes f :: "'a::order_with_dual \<Rightarrow> 'a"
   shows "coclop f = clop (\<partial>\<^sub>F f)"
   by (simp add: coclop_dual)
 
 lemma clop_dual: "(clop::('a::order_with_dual \<Rightarrow> 'a) \<Rightarrow> bool) = coclop \<circ> \<partial>\<^sub>F"
   by (simp add: coclop_dual comp_assoc map_dual_invol)
 
 lemma clop_dual_var: 
   fixes f :: "'a::order_with_dual \<Rightarrow> 'a"
   shows "clop f = coclop (\<partial>\<^sub>F f)"
   by (simp add: clop_dual)
 
 lemma coclop_coextensive: "coclop f \<Longrightarrow> f \<le> id"
   by (simp add: coclop_def)
 
 lemma coclop_coextensive_var: "coclop f \<Longrightarrow> f x \<le> x"
   using coclop_def le_funD by fastforce
 
 lemma coclop_iso: "coclop f \<Longrightarrow> mono f"
   by (simp add: coclop_def)
 
 lemma coclop_iso_var: "coclop f \<Longrightarrow> (x \<le> y \<longrightarrow> f x \<le> f y)"
   by (simp add: coclop_iso monoD)
 
 lemma coclop_idem: "coclop f \<Longrightarrow> f \<circ> f = f"
   by (simp add: antisym coclop_def le_fun_def)
 
 lemma coclop_closure: "coclop f \<Longrightarrow> (x \<in> range f) = (f x = x)"
   by (simp add: coclop_idem retraction_prop)
 
 lemma coclop_Fix_range: "coclop f \<Longrightarrow> (Fix f = range f)"
   by (simp add: coclop_idem retraction_prop_fix)
 
 lemma coclop_idem_var: "coclop f \<Longrightarrow> f (f x) = f x"
   by (simp add: coclop_idem retraction_prop)
 
 lemma coclop_Sup_closed_var: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'a"
   shows "coclop f \<Longrightarrow> f \<circ> Sup \<circ> (`) f  = Sup \<circ> (`) f"
   unfolding coclop_def mono_def comp_def le_fun_def 
   by (metis (mono_tags, lifting) SUP_le_iff antisym id_apply order_refl)
 
 lemma Sup_closed_coclop_var: 
   fixes X :: "'a::complete_lattice set"
   shows "coclop f \<Longrightarrow> \<forall>x \<in> X. x \<in> range f \<Longrightarrow> \<Squnion>X \<in> range f"
-  by (smt Inf.INF_id_eq Sup.SUP_cong antisym coclop_closure coclop_coextensive_var coclop_iso id_apply mono_SUP)
+  by (smt (verit) Inf.INF_id_eq Sup.SUP_cong antisym coclop_closure coclop_coextensive_var coclop_iso id_apply mono_SUP)
 
 lemma coclop_bot: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'a"
   shows "coclop f \<Longrightarrow> f \<bottom> = \<bottom>"
   by (simp add: bot.extremum_uniqueI coclop_coextensive_var)
 
 lemma "coclop (f::'a::complete_lattice \<Rightarrow> 'a) \<Longrightarrow> f (\<Sqinter>x \<in> X. f x) = (\<Sqinter>x \<in> X. f x)" (*nitpick*)
   oops
 
 lemma "coclop (f::'a::complete_lattice \<Rightarrow> 'a) \<Longrightarrow> f (f x \<sqinter> f y) = f x \<sqinter> f y" (*nitpick*)
   oops
 
 lemma  "coclop (f::'a::complete_lattice \<Rightarrow> 'a) \<Longrightarrow> f \<top> = \<top>" (*nitpick*) 
   oops
   
 lemma "coclop (f::'a set \<Rightarrow> 'a set) \<Longrightarrow> f (\<Sqinter>x \<in> X. f x) = (\<Sqinter>x \<in> X. f x)" (*nitpick*)
   oops
 
 lemma "coclop (f::'a set \<Rightarrow> 'a set) \<Longrightarrow> f (f x \<sqinter> f y) = f x \<sqinter> f y" (*nitpick*)
   oops
 
 lemma  "coclop (f::'a set \<Rightarrow> 'a set) \<Longrightarrow> f \<top> = \<top>" (*nitpick *)
   oops
 
 lemma coclop_coclosure: "coclop f \<Longrightarrow> f x = x \<longleftrightarrow> x \<in> range f"
  by (simp add: coclop_idem retraction_prop)
                                               
 lemma coclop_coclosure_set: "coclop f \<Longrightarrow> range f = Fix f"
   by (simp add: coclop_idem retraction_prop_fix)
 
 lemma coclop_coclosure_prop: "(coclop::('a::complete_lattice \<Rightarrow> 'a) \<Rightarrow> bool) (Sup \<circ> \<down>)"
   by (simp add: coclop_def mono_def)
 
 lemma coclop_coclosure_prop_var: "coclop (\<lambda>x::'a::complete_lattice. \<Squnion>{y. y \<le> x})"
   by (metis (mono_tags, lifting) Sup_atMost atMost_def coclop_def comp_apply eq_id_iff eq_refl mono_def)
 
 lemma coclop_alt: "(coclop f) = (\<forall>x y. f x \<le> y \<longleftrightarrow> f x \<le> f y)"
   unfolding coclop_def mono_def le_fun_def comp_def id_def
   by (meson dual_order.refl order_trans)
 
 lemma coclop_adj: 
   fixes f :: "'a::order \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> coclop (f \<circ> g)"
   by (simp add: adj_cancel1 adj_idem1 adj_iso3 coclop_def)
 
 text \<open>Finally, a subset of a complete lattice is Sup-closed if and only if it is the set of fixpoints
 of some co-closure operator.\<close>
 
 lemma coclop_Sup_closed: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows  "coclop f \<Longrightarrow> Sup_closed_set (Fix f)"
   unfolding coclop_def Sup_closed_set_def mono_def le_fun_def comp_def id_def Fix_def
-  by (smt Sup_least Sup_upper antisym_conv mem_Collect_eq subsetCE)
+  by (smt (verit) Sup_least Sup_upper antisym_conv mem_Collect_eq subsetCE)
 
 lemma Sup_closed_coclop: 
   fixes X :: "'a::complete_lattice set"
   shows "Sup_closed_set X \<Longrightarrow> coclop (\<lambda>y. \<Squnion>{x \<in> X. x \<le> y})"
   unfolding Sup_closed_set_def coclop_def mono_def le_fun_def comp_def
   apply safe
   apply (metis (no_types, lifting) Sup_least eq_id_iff mem_Collect_eq)
-  apply (smt Collect_mono_iff Sup_subset_mono dual_order.trans)
+  apply (smt (verit) Collect_mono_iff Sup_subset_mono dual_order.trans)
   by (simp add: Collect_mono_iff Sup_subset_mono Sup_upper)
 
 
 subsection \<open>Complete Lattices of Closed Elements\<close>
 
 text \<open>The machinery developed allows showing that the closed elements in a complete
 lattice (with respect to some closure operation) form themselves a complete lattice.\<close>
 
 class cl_op = ord +
   fixes cl_op :: "'a \<Rightarrow> 'a"
   assumes clop_ext: "x \<le> cl_op x"
   and clop_iso: "x \<le> y \<Longrightarrow> cl_op x \<le> cl_op y"
   and clop_wtrans: "cl_op (cl_op x) \<le> cl_op x"
 
 class clattice_with_clop = complete_lattice + cl_op
 
 begin
 
 lemma clop_cl_op: "clop cl_op"
   unfolding clop_def le_fun_def comp_def
   by (simp add: cl_op_class.clop_ext cl_op_class.clop_iso cl_op_class.clop_wtrans order_class.mono_def)
 
 lemma clop_idem [simp]: "cl_op \<circ> cl_op = cl_op"
   using clop_ext clop_wtrans order.antisym by auto
 
 lemma clop_idem_var [simp]: "cl_op (cl_op x) = cl_op x"
   by (simp add: order.antisym clop_ext clop_wtrans)
 
 lemma clop_range_Fix: "range cl_op = Fix cl_op"
   by (simp add: retraction_prop_fix)
 
 lemma Inf_closed_cl_op_var: 
   fixes X :: "'a set"
   shows "\<forall>x \<in> X. x \<in> range cl_op \<Longrightarrow> \<Sqinter>X \<in> range cl_op"
 proof-
   assume h: "\<forall>x \<in> X. x \<in> range cl_op"
   hence "\<forall>x \<in> X. cl_op x = x"
     by (simp add: retraction_prop)
   hence "cl_op (\<Sqinter>X) = \<Sqinter>X"
     by (metis Inf_lower clop_ext clop_iso dual_order.antisym le_Inf_iff)
   thus ?thesis
     by (metis rangeI)
 qed
 
 lemma inf_closed_cl_op_var: "x \<in> range cl_op \<Longrightarrow> y \<in> range cl_op \<Longrightarrow> x \<sqinter> y \<in> range cl_op"
-  by (smt Inf_closed_cl_op_var UnI1 insert_iff insert_is_Un inf_Inf)
+  by (smt (verit) Inf_closed_cl_op_var UnI1 insert_iff insert_is_Un inf_Inf)
 
 end
 
 typedef (overloaded) 'a::clattice_with_clop cl_op_im = "range (cl_op::'a \<Rightarrow> 'a)"
   by force
 
 setup_lifting type_definition_cl_op_im
 
 lemma cl_op_prop [iff]: "(cl_op (x \<squnion> y) = cl_op y) = (cl_op (x::'a::clattice_with_clop) \<le> cl_op y)"
-  by (smt cl_op_class.clop_iso clop_ext clop_wtrans inf_sup_ord(4) le_iff_sup sup.absorb_iff1 sup_left_commute)
+  by (smt (verit) cl_op_class.clop_iso clop_ext clop_wtrans inf_sup_ord(4) le_iff_sup sup.absorb_iff1 sup_left_commute)
 
 lemma cl_op_prop_var [iff]: "(cl_op (x \<squnion> cl_op y) = cl_op y) = (cl_op (x::'a::clattice_with_clop) \<le> cl_op y)"
   by (metis cl_op_prop clattice_with_clop_class.clop_idem_var)
 
 instantiation cl_op_im :: (clattice_with_clop) complete_lattice
 begin
 
 lift_definition Inf_cl_op_im :: "'a cl_op_im set \<Rightarrow> 'a cl_op_im" is Inf
   by (simp add: Inf_closed_cl_op_var)
  
 lift_definition Sup_cl_op_im :: "'a cl_op_im set \<Rightarrow> 'a cl_op_im" is "\<lambda>X. cl_op (\<Squnion>X)"
   by simp
 
 lift_definition inf_cl_op_im :: "'a cl_op_im \<Rightarrow> 'a cl_op_im \<Rightarrow> 'a cl_op_im" is inf
   by (simp add: inf_closed_cl_op_var)
 
 lift_definition sup_cl_op_im :: "'a cl_op_im \<Rightarrow> 'a cl_op_im \<Rightarrow> 'a cl_op_im" is "\<lambda>x y. cl_op (x \<squnion> y)"
   by simp
 
 lift_definition less_eq_cl_op_im :: "'a cl_op_im \<Rightarrow> 'a cl_op_im \<Rightarrow> bool" is "(\<le>)".
 
 lift_definition less_cl_op_im :: "'a cl_op_im \<Rightarrow> 'a cl_op_im \<Rightarrow> bool" is "(<)".
 
 lift_definition bot_cl_op_im :: "'a cl_op_im" is "cl_op \<bottom>"
   by simp
 
 lift_definition top_cl_op_im :: "'a cl_op_im" is "\<top>"
   by (simp add: clop_cl_op clop_closure clop_top)
 
 
 instance
   apply (intro_classes; transfer)
                  apply (simp_all add: less_le_not_le Inf_lower Inf_greatest)
       apply (meson clop_cl_op clop_extensive_var dual_order.trans inf_sup_ord(3))
      apply (meson clop_cl_op clop_extensive_var dual_order.trans sup_ge2)
     apply (metis cl_op_class.clop_iso clop_cl_op clop_closure le_sup_iff)
    apply (meson Sup_upper clop_cl_op clop_extensive_var dual_order.trans)
   by (metis Sup_le_iff cl_op_class.clop_iso clop_cl_op clop_closure)
 
 end
 
 text \<open>This statement is perhaps less useful as it might seem, because it is difficult to make it cooperate with concrete closure operators, 
 which one would not generally like to define within a type class. Alternatively, a sublocale statement could perhaps be given. It would also 
 have been nice to prove this statement for Sup-lattices---this would have cut down the number of proof obligations significantly.
 But this would require a tighter integration of these structures. A similar statement could have been proved for co-closure operators. But this would
 not lead to new insights.\<close>
 
 text \<open>Next I show that for every surjective Sup-preserving function between complete lattices there is a closure operator 
 such that the set of closed elements is isomorphic to the range of the surjection.\<close>
 
 lemma surj_Sup_pres_id:
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   assumes "surj f"
   and "Sup_pres f" 
   shows "f \<circ> (radj f) = id"
 proof-
   have "f \<stileturn> (radj f)"
     using Sup_pres_ladj assms(2) radj_adj by auto
   thus ?thesis
     using adj_sur_inv assms(1) by blast
 qed
 
 lemma surj_Sup_pres_inj:
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   assumes "surj f"
   and "Sup_pres f" 
   shows "inj (radj f)"
   by (metis assms comp_eq_dest_lhs id_apply injI surj_Sup_pres_id)
 
 lemma surj_Sup_pres_inj_on: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   assumes "surj f"
   and "Sup_pres f" 
   shows "inj_on f (range (radj f \<circ> f))"
-  by (smt Sup_pres_ladj_aux adj_idem2 assms(2) comp_apply inj_on_def retraction_prop)
+  by (smt (verit) Sup_pres_ladj_aux adj_idem2 assms(2) comp_apply inj_on_def retraction_prop)
 
 lemma surj_Sup_pres_bij_on: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   assumes "surj f"
   and "Sup_pres f" 
   shows "bij_betw f (range (radj f \<circ> f)) UNIV"
   unfolding bij_betw_def
   apply safe
     apply (simp add: assms(1) assms(2) surj_Sup_pres_inj_on cong del: image_cong_simp)
    apply auto
   apply (metis (mono_tags) UNIV_I assms(1) assms(2) comp_apply id_apply image_image surj_Sup_pres_id surj_def)
   done
 
 text \<open>Thus the restriction of $f$ to the set of closed elements is indeed a bijection. The final fact
 shows that it preserves Sups of closed elements, and hence is an isomorphism of complete lattices.\<close>
 
 lemma surj_Sup_pres_iso: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   assumes "surj f"
   and "Sup_pres f" 
   shows "f ((radj f \<circ> f) (\<Squnion>X)) = (\<Squnion>x \<in> X. f x)"
   by (metis assms(1) assms(2) comp_def pointfree_idE surj_Sup_pres_id)
 
 
 subsection \<open>A Quick Example: Dedekind-MacNeille Completions\<close>
 
 text \<open>I only outline the basic construction. Additional facts about join density, and that the completion yields 
 the least complete lattice that contains all Sups and Infs of the underlying posets, are left for future consideration.\<close>
 
 abbreviation "dm \<equiv> lb_set \<circ> ub_set"
 
 lemma up_set_prop: "(X::'a::preorder set) \<noteq> {} \<Longrightarrow> ub_set X = \<Inter>{\<up>x |x. x \<in> X}"
   unfolding ub_set_def upset_def upset_set_def by (safe, simp_all, blast)
 
 lemma lb_set_prop: "(X::'a::preorder set) \<noteq> {} \<Longrightarrow> lb_set X = \<Inter>{\<down>x |x. x \<in> X}"
   unfolding lb_set_def downset_def downset_set_def by (safe, simp_all, blast)
 
 lemma dm_downset_var: "dm {x} = \<down>(x::'a::preorder)"
   unfolding lb_set_def ub_set_def downset_def downset_set_def 
   by (clarsimp, meson order_refl order_trans)
 
 lemma dm_downset: "dm \<circ> \<eta> = (\<down>::'a::preorder \<Rightarrow> 'a set)"
   using dm_downset_var fun.map_cong by fastforce
 
 lemma dm_inj: "inj ((dm::'a::order set \<Rightarrow> 'a set) \<circ> \<eta>)"
   by (simp add: dm_downset downset_inj)
 
 lemma "clop (lb_set \<circ> ub_set)"
   unfolding clop_def lb_set_def ub_set_def
   apply safe
   unfolding le_fun_def comp_def id_def mono_def
   by auto
 
 end
 
diff --git a/thys/Order_Lattice_Props/Galois_Connections.thy b/thys/Order_Lattice_Props/Galois_Connections.thy
--- a/thys/Order_Lattice_Props/Galois_Connections.thy
+++ b/thys/Order_Lattice_Props/Galois_Connections.thy
@@ -1,243 +1,243 @@
 (* 
   Title: Galois Connections
   Author: Georg Struth 
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
 *)
 
 section \<open>Galois Connections\<close>
 
 theory Galois_Connections
   imports Order_Lattice_Props
 
 begin
 
 subsection \<open>Definitions and Basic Properties\<close>
 
 text \<open>The approach follows the Compendium of Continuous Lattices~\<^cite>\<open>"GierzHKLMS80"\<close>, without attempting completeness. 
 First, left and right adjoints of a Galois connection are defined.\<close>
 
 definition adj :: "('a::ord \<Rightarrow> 'b::ord) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool" (infixl "\<stileturn>" 70) where 
   "(f \<stileturn> g) = (\<forall>x y. (f x \<le> y) = (x \<le> g y))"
 
 definition "ladj (g::'a::Inf \<Rightarrow> 'b::ord) = (\<lambda>x. \<Sqinter>{y. x \<le> g y})"
 
 definition "radj (f::'a::Sup \<Rightarrow> 'b::ord)  = (\<lambda>y. \<Squnion>{x. f x \<le> y})"
 
 lemma ladj_radj_dual:
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::ord_with_dual"
   shows "ladj f x = \<partial> (radj (\<partial>\<^sub>F f) (\<partial> x))"
 proof-
   have "ladj f x = \<partial> (\<Squnion>(\<partial> ` {y. \<partial> (f y) \<le> \<partial> x}))"
     unfolding ladj_def by (metis (no_types, lifting) Collect_cong Inf_dual_var dual_dual_ord dual_iff)
   also have "... =  \<partial> (\<Squnion>{\<partial> y|y. \<partial> (f y) \<le> \<partial> x})"
     by (simp add: setcompr_eq_image)
   ultimately show ?thesis
     unfolding ladj_def radj_def map_dual_def comp_def
-    by (smt Collect_cong invol_dual_var)
+    by (smt (verit) Collect_cong invol_dual_var)
 qed
 
 lemma radj_ladj_dual: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::ord_with_dual"
   shows "radj f x = \<partial> (ladj (\<partial>\<^sub>F f) (\<partial> x))"
   by (metis fun_dual5 invol_dual_var ladj_radj_dual map_dual_def)
 
 lemma ladj_prop: 
   fixes g :: "'b::Inf \<Rightarrow> 'a::ord_with_dual"
   shows "ladj g = Inf \<circ> (-`) g \<circ> \<up>"
   unfolding ladj_def vimage_def upset_prop fun_eq_iff comp_def by simp
 
 lemma radj_prop: 
   fixes f :: "'b::Sup \<Rightarrow> 'a::ord"
   shows "radj f = Sup \<circ> (-`) f \<circ> \<down>"
   unfolding radj_def vimage_def downset_prop fun_eq_iff comp_def by simp
 
 text \<open>The first set of properties holds without any sort assumptions.\<close>
 
 lemma adj_iso1: "f \<stileturn> g \<Longrightarrow> mono f"
   unfolding adj_def mono_def by (meson dual_order.refl dual_order.trans) 
 
 lemma adj_iso2: "f \<stileturn> g \<Longrightarrow> mono g"
   unfolding adj_def mono_def by (meson dual_order.refl dual_order.trans) 
 
 lemma adj_comp: "f \<stileturn> g \<Longrightarrow> adj h k \<Longrightarrow> (f \<circ> h) \<stileturn> (k \<circ> g)"
   by (simp add: adj_def)
 
 lemma adj_dual: 
   fixes f :: "'a::ord_with_dual \<Rightarrow> 'b::ord_with_dual"
   shows "f \<stileturn> g = (\<partial>\<^sub>F g) \<stileturn> (\<partial>\<^sub>F f)"
   unfolding adj_def map_dual_def comp_def by (metis (mono_tags, opaque_lifting) dual_dual_ord invol_dual_var)
 
 subsection \<open>Properties for (Pre)Orders\<close>
 
 text \<open>The next set of properties holds in preorders or orders.\<close>
 
 lemma adj_cancel1: 
   fixes f :: "'a::preorder \<Rightarrow> 'b::ord"
   shows "f \<stileturn> g \<Longrightarrow> f \<circ> g \<le> id"
   by (simp add: adj_def le_funI)
 
 lemma adj_cancel2: 
   fixes f :: "'a::ord \<Rightarrow> 'b::preorder"
   shows "f \<stileturn> g \<Longrightarrow> id \<le> g \<circ> f"
   by (simp add: adj_def eq_iff le_funI)
 
 lemma adj_prop: 
   fixes f :: "'a::preorder \<Rightarrow>'a"
   shows "f \<stileturn> g \<Longrightarrow> f \<circ> g \<le> g \<circ> f"
   using adj_cancel1 adj_cancel2 order_trans by blast
 
 lemma adj_cancel_eq1: 
   fixes f :: "'a::preorder \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> f \<circ> g \<circ> f = f"
   unfolding adj_def comp_def fun_eq_iff by (meson eq_iff order_refl order_trans)
 
 lemma adj_cancel_eq2: 
   fixes f :: "'a::order \<Rightarrow> 'b::preorder"
   shows "f \<stileturn> g \<Longrightarrow> g \<circ> f \<circ> g = g"
   unfolding adj_def comp_def fun_eq_iff by (meson eq_iff order_refl order_trans) 
 
 lemma adj_idem1: 
   fixes f :: "'a::preorder \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> (f \<circ> g) \<circ> (f \<circ> g) = f \<circ> g"
   by (simp add: adj_cancel_eq1 rewriteL_comp_comp)
 
 lemma adj_idem2: 
   fixes f :: "'a::order \<Rightarrow> 'b::preorder"
   shows "f \<stileturn> g \<Longrightarrow> (g \<circ> f) \<circ> (g \<circ> f) = g \<circ> f"
   by (simp add: adj_cancel_eq2 rewriteL_comp_comp)
 
 lemma adj_iso3: 
   fixes f :: "'a::order \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> mono (f \<circ> g)"
    by (simp add: adj_iso1 adj_iso2 monoD monoI)
 
 lemma adj_iso4: 
   fixes f :: "'a::order \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> mono (g \<circ> f)"
   by (simp add: adj_iso1 adj_iso2 monoD monoI)
 
 lemma adj_canc1: 
   fixes f :: "'a::order \<Rightarrow> 'b::ord"
   shows "f \<stileturn> g \<Longrightarrow> ((f \<circ> g) x = (f \<circ> g) y \<longrightarrow> g x = g y)"
   unfolding adj_def comp_def by (metis eq_iff)
  
 lemma adj_canc2: 
   fixes f :: "'a::ord \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> ((g \<circ> f) x = (g \<circ> f) y \<longrightarrow> f x = f y)"
   unfolding adj_def comp_def by (metis eq_iff)
 
 lemma adj_sur_inv: 
   fixes f :: "'a::preorder \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> ((surj f) = (f \<circ> g = id))"
   unfolding adj_def surj_def comp_def by (metis eq_id_iff eq_iff order_refl order_trans)
 
 lemma adj_surj_inj: 
   fixes f :: "'a::order \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> ((surj f) = (inj g))"
   unfolding adj_def inj_def surj_def by (metis eq_iff order_trans)
 
 lemma adj_inj_inv: 
   fixes f :: "'a::preorder \<Rightarrow> 'b::order"
   shows "f \<stileturn> g \<Longrightarrow> ((inj f) = (g \<circ> f = id))"
   by (metis adj_cancel_eq1 eq_id_iff inj_def o_apply)
 
 lemma adj_inj_surj: 
   fixes f :: "'a::order \<Rightarrow> 'b::order" 
   shows "f \<stileturn> g \<Longrightarrow> ((inj f) = (surj g))"
   unfolding adj_def inj_def surj_def by (metis eq_iff order_trans)
 
 lemma surj_id_the_inv: "surj f \<Longrightarrow> g \<circ> f = id \<Longrightarrow> g = the_inv f"
   by (metis comp_apply id_apply inj_on_id inj_on_imageI2 surj_fun_eq the_inv_f_f)
 
 lemma inj_id_the_inv: "inj f \<Longrightarrow> f \<circ> g = id \<Longrightarrow> f = the_inv g"
 proof -
   assume a1: "inj f"
   assume "f \<circ> g = id"
   hence "\<forall>x. the_inv g x = f x"
     using a1 by (metis (no_types) comp_apply eq_id_iff inj_on_id inj_on_imageI2 the_inv_f_f)
   thus ?thesis 
     by presburger
 qed
 
 
 subsection \<open>Properties for Complete Lattices\<close>
 
 text \<open>The next laws state that a function between complete lattices preserves infs 
   if and only if it has a lower adjoint.\<close>
 
 lemma radj_Inf_pres: 
   fixes g :: "'b::complete_lattice \<Rightarrow> 'a::complete_lattice"
   shows "(\<exists>f. f \<stileturn> g) \<Longrightarrow> Inf_pres g"
   apply (rule antisym, simp_all add: le_fun_def adj_def, safe)
   apply (meson INF_greatest Inf_lower dual_order.refl dual_order.trans)
   by (meson Inf_greatest dual_order.refl le_INF_iff)
 
 lemma ladj_Sup_pres: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   shows "(\<exists>g. f \<stileturn> g) \<Longrightarrow> Sup_pres f"
   using Sup_pres_map_dual_var adj_dual radj_Inf_pres by blast
 
 lemma radj_adj: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "f \<stileturn> g \<Longrightarrow> g = (radj f)"
   unfolding adj_def radj_def by (metis (mono_tags, lifting) cSup_eq_maximum eq_iff mem_Collect_eq)
 
 lemma ladj_adj: 
   fixes g :: "'b::complete_lattice_with_dual \<Rightarrow> 'a::complete_lattice_with_dual" 
   shows "f \<stileturn> g \<Longrightarrow> f = (ladj g)"
   unfolding adj_def ladj_def by (metis (no_types, lifting) cInf_eq_minimum eq_iff mem_Collect_eq)
 
 lemma Inf_pres_radj_aux: 
   fixes g :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Inf_pres g \<Longrightarrow> (ladj g) \<stileturn> g"
 proof-
   assume a: "Inf_pres g"
   {fix x y
    assume b: "ladj g x \<le> y" 
   hence "g (ladj g x) \<le> g y"
     by (simp add: Inf_subdistl_iso a monoD)
   hence "\<Sqinter>{g y |y. x \<le> g y} \<le> g y"
     by (metis a comp_eq_dest_lhs setcompr_eq_image ladj_def)
   hence "x \<le> g y"
     using dual_order.trans le_Inf_iff by blast  
   hence "ladj g x \<le> y \<longrightarrow> x \<le> g y"
     by simp}
   thus ?thesis 
     unfolding adj_def ladj_def by (meson CollectI Inf_lower)
 qed
 
 lemma Sup_pres_ladj_aux: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual" 
   shows "Sup_pres f \<Longrightarrow> f \<stileturn> (radj f)"
   by (metis (no_types, opaque_lifting) Inf_pres_radj_aux Sup_pres_map_dual_var adj_dual fun_dual5 map_dual_def radj_adj)
 
 lemma Inf_pres_radj: 
   fixes g :: "'b::complete_lattice \<Rightarrow> 'a::complete_lattice"
   shows "Inf_pres g \<Longrightarrow> (\<exists>f. f \<stileturn> g)"
   using Inf_pres_radj_aux by fastforce
 
 lemma Sup_pres_ladj: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   shows "Sup_pres f \<Longrightarrow> (\<exists>g. f \<stileturn> g)"
   using Sup_pres_ladj_aux by fastforce
 
 lemma Inf_pres_upper_adj_eq: 
   fixes g :: "'b::complete_lattice \<Rightarrow> 'a::complete_lattice"
   shows "(Inf_pres g) = (\<exists>f. f \<stileturn> g)"
   using radj_Inf_pres Inf_pres_radj by blast
 
 lemma Sup_pres_ladj_eq:
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   shows  "(Sup_pres f) = (\<exists>g. f \<stileturn> g)"
   using Sup_pres_ladj ladj_Sup_pres by blast
 
 lemma Sup_downset_adj: "(Sup::'a::complete_lattice set \<Rightarrow> 'a) \<stileturn> \<down>"
   unfolding adj_def downset_prop Sup_le_iff by force
 
 lemma Sup_downset_adj_var: "(Sup (X::'a::complete_lattice set) \<le> y) = (X \<subseteq> \<down>y)"
   using Sup_downset_adj adj_def by auto
 
 text \<open>Once again many statements arise by duality, which Isabelle usually picks up.\<close>
 
 
 end
\ No newline at end of file
diff --git a/thys/Order_Lattice_Props/Order_Duality.thy b/thys/Order_Lattice_Props/Order_Duality.thy
--- a/thys/Order_Lattice_Props/Order_Duality.thy
+++ b/thys/Order_Lattice_Props/Order_Duality.thy
@@ -1,315 +1,315 @@
 (* 
   Title: Ad-Hoc Duality for Orderings and Lattices
   Author: Georg Struth 
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
 *)
 
 section \<open>Ad-Hoc Duality for Orderings and Lattices\<close>
 
 theory Order_Duality
   imports Sup_Lattice
 
 begin
 
 text \<open>This component presents an "explicit" formalisation of order and lattice duality. It augments the data type based one
  used by Wenzel in his lattice components \<^cite>\<open>"Wenzel"\<close>, and complements the "implicit" formalisation given by locales. It uses a functor dual, 
 supplied within a type class, which is simply a bijection (isomorphism) between types, with the constraint that
 the dual of a dual object is the original object. In Wenzel's formalisation, by contrast, dual is a bijection, but not
  idempotent or involutive. In the past, Preoteasa has used a similar approach with Isabelle~\<^cite>\<open>"Preoteasa11b"\<close>.\<close>
 
 text \<open>Duality is such a fundamental concept in order and lattice theory that it probably deserves to be included in the type classes
 for these objects, as in this section.\<close>
 
 class dual =
   fixes dual :: "'a \<Rightarrow> 'a" ("\<partial>")
   assumes inj_dual: "inj \<partial>"
   and invol_dual [simp]: "\<partial> \<circ> \<partial> = id"
 
 text \<open>This type class allows one to define a type dual. It is actually a dependent type
 for which dual can be instantiated.\<close>
 
 typedef (overloaded) 'a dual = "range (dual::'a::dual \<Rightarrow> 'a)"
   by fastforce
 
 setup_lifting type_definition_dual
 
 text \<open>At the moment I have no use for this type.\<close>
 
 context dual
 begin
 
 lemma invol_dual_var [simp]: "\<partial> (\<partial> x) = x"
   by (simp add: pointfree_idE)
 
 lemma surj_dual: "surj \<partial>"
   unfolding surj_def by (metis invol_dual_var)
 
 lemma bij_dual: "bij \<partial>"
   by (simp add: bij_def inj_dual surj_dual)
 
 lemma inj_dual_iff: "(\<partial> x = \<partial> y) = (x = y)"
   by (meson inj_dual injD)
 
 lemma dual_iff: "(\<partial> x = y) = (x = \<partial> y)"
   by auto
 
 lemma the_inv_dual: "the_inv \<partial> = \<partial>"
   by (metis comp_apply id_def invol_dual_var inj_dual surj_dual surj_fun_eq the_inv_f_o_f_id)
 
 end
 
 text \<open>In boolean algebras, duality is of course De Morgan duality and can be expressed within the language.\<close>
 
 sublocale boolean_algebra \<subseteq> ba_dual: dual "uminus"  
   by (unfold_locales, simp_all add: inj_def)
 
 definition map_dual:: "('a \<Rightarrow> 'b) \<Rightarrow> 'a::dual \<Rightarrow> 'b::dual" ("\<partial>\<^sub>F") where 
   "\<partial>\<^sub>F f = \<partial> \<circ> f \<circ> \<partial>"  
 
 lemma map_dual_func1: "\<partial>\<^sub>F (f \<circ> g) = \<partial>\<^sub>F f \<circ> \<partial>\<^sub>F g"
   by (metis (no_types, lifting) comp_assoc comp_id invol_dual map_dual_def)
 
 lemma map_dual_func2 [simp]: "\<partial>\<^sub>F id = id"
   by (simp add: map_dual_def)
 
 lemma map_dual_nat_iso: "\<partial>\<^sub>F f \<circ> \<partial> = \<partial> \<circ> id f"
   by (simp add: comp_assoc map_dual_def)
 
 lemma map_dual_invol [simp]: "\<partial>\<^sub>F \<circ> \<partial>\<^sub>F = id"
   unfolding map_dual_def comp_def fun_eq_iff by simp
   
 text \<open>Thus map-dual is naturally isomorphic to the identify functor: The function dual is a natural transformation 
 between  map-dual and the identity functor, and, because it has a two-sided inverse --- itself, it is a natural isomorphism.\<close>
 
 text \<open>The generic function set-dual provides another natural transformation (see below). Before introducing it, we introduce useful notation 
 for a widely used function.\<close>
 
 abbreviation "\<eta> \<equiv> (\<lambda>x. {x})"
 
 lemma eta_inj: "inj \<eta>"
   by simp
 
 definition "set_dual = \<eta> \<circ> \<partial>"
 
 lemma set_dual_prop: "set_dual (\<partial> x) = {x}"
   by (metis comp_apply dual_iff set_dual_def)
 
 text \<open>The next four lemmas show that (functional) image and preimage are functors (on functions). This does not really belong here, 
 but it is useful for what follows. The interaction between duality and (pre)images is needed in applications.\<close>
 
 lemma image_func1: "(`) (f \<circ> g) = (`) f \<circ> (`) g"
   unfolding fun_eq_iff by (simp add: image_comp) 
 
 lemma image_func2: "(`) id = id"
   by simp
 
 lemma vimage_func1: "(-`) (f \<circ> g) = (-`) g \<circ> (-`) f"
   unfolding fun_eq_iff by (simp add: vimage_comp)
 
 lemma vimage_func2: "(-`) id = id"
   by simp
 
 lemma iso_image: "mono ((`) f)"
   by (simp add: image_mono monoI)
 
 lemma iso_preimage: "mono ((-`) f)"
   by (simp add: monoI vimage_mono)
 
 context dual
 begin
 
 lemma image_dual [simp]: "(`) \<partial> \<circ> (`) \<partial> = id"
   by (metis image_func1 image_func2 invol_dual)
 
 lemma vimage_dual [simp]: "(-`) \<partial> \<circ> (-`) \<partial> = id"
   by (simp add: set.comp)
 
 end
 
 text \<open>The following natural transformation between the powerset functor (image) and the identity functor
 is well known.\<close>
 
 lemma power_set_func_nat_trans: "\<eta> \<circ> id f = (`) f \<circ> \<eta>"
   unfolding fun_eq_iff comp_def by simp
 
 text \<open>As an instance, set-dual is a natural transformation with built-in type coercion.\<close>
 
 lemma dual_singleton: "(`) \<partial> \<circ> \<eta> = \<eta> \<circ> \<partial>"  
   by auto
 
 lemma finite_dual [simp]: "finite \<circ> (`) \<partial> = finite"
   unfolding fun_eq_iff comp_def using inj_dual finite_vimageI inj_vimage_image_eq by fastforce
 
 lemma finite_dual_var [simp]: "finite (\<partial> ` X) = finite X"
   by (metis comp_def finite_dual)
 
 lemma subset_dual: "(X = \<partial> ` Y) = (\<partial> ` X = Y)"
   by (metis image_dual pointfree_idE)
 
 lemma subset_dual1: "(X \<subseteq> Y) = (\<partial> ` X \<subseteq> \<partial> ` Y)"
   by (simp add: inj_dual inj_image_subset_iff) 
 
 lemma dual_empty [simp]: "\<partial> ` {} = {}"
   by simp
 
 lemma dual_UNIV [simp]: "\<partial> ` UNIV = UNIV"
   by (simp add: surj_dual)
 
 lemma fun_dual1: "(f = g \<circ> \<partial>) = (f \<circ> \<partial> = g)"
   by (metis comp_assoc comp_id invol_dual)
 
 lemma fun_dual2: "(f = \<partial> \<circ> g) = (\<partial> \<circ> f = g)"
   by (metis comp_assoc fun.map_id invol_dual)
 
 lemma fun_dual3: "(f = g \<circ> (`) \<partial>) = (f \<circ> (`) \<partial> = g)"
   by (metis comp_id image_dual o_assoc)
 
 lemma fun_dual4: "(f = (`) \<partial> \<circ> g) = ((`) \<partial> \<circ> f = g)"
   by (metis comp_assoc id_comp image_dual)
 
 lemma fun_dual5: "(f = \<partial> \<circ> g \<circ> \<partial>) = (\<partial> \<circ> f \<circ> \<partial> = g)"
   by (metis comp_assoc fun_dual1 fun_dual2)
 
 lemma fun_dual6: "(f = (`) \<partial> \<circ> g \<circ> (`) \<partial>) = ((`) \<partial> \<circ> f \<circ> (`) \<partial> = g)"
   by (simp add: comp_assoc fun_dual3 fun_dual4)
 
 lemma fun_dual7: "(f = \<partial> \<circ> g \<circ> (`) \<partial>) = (\<partial> \<circ> f \<circ> (`) \<partial> = g)"
   by (simp add: comp_assoc fun_dual2 fun_dual3)
 
 lemma fun_dual8: "(f = (`) \<partial> \<circ> g \<circ> \<partial>) = ((`) \<partial> \<circ> f \<circ> \<partial> = g)"
   by (simp add: comp_assoc fun_dual1 fun_dual4)
 
 lemma map_dual_dual: "(\<partial>\<^sub>F f = g) = (\<partial>\<^sub>F g = f)"
   by (metis map_dual_invol pointfree_idE)
 
 text \<open>The next facts show incrementally that the dual of a complete lattice is a complete lattice.\<close>
 
 class ord_with_dual = dual + ord +
   assumes ord_dual: "x \<le> y \<Longrightarrow> \<partial> y \<le> \<partial> x"
 
 begin
 
 lemma dual_dual_ord: "(\<partial> x \<le> \<partial> y) = (y \<le> x)"
   by (metis dual_iff ord_dual)
 
 end
 
 lemma ord_pres_dual:
   fixes f :: "'a::ord_with_dual \<Rightarrow> 'b::ord_with_dual"   
   shows "ord_pres f \<Longrightarrow> ord_pres (\<partial>\<^sub>F f)"
   by (simp add: dual_dual_ord map_dual_def ord_pres_def)
 
 lemma map_dual_anti: "(f::'a::ord_with_dual \<Rightarrow> 'b::ord_with_dual) \<le> g  \<Longrightarrow> \<partial>\<^sub>F g \<le> \<partial>\<^sub>F f"
   by (simp add: le_fun_def map_dual_def ord_dual)
   
 class preorder_with_dual = ord_with_dual + preorder
 
 begin
 
 lemma less_dual_def_var: "(\<partial> y < \<partial> x) = (x < y)"
   by (simp add: dual_dual_ord less_le_not_le)
 
 end
 
 class order_with_dual = preorder_with_dual + order
 
 lemma iso_map_dual: 
   fixes f :: "'a::order_with_dual \<Rightarrow> 'b::order_with_dual"   
   shows "mono f \<Longrightarrow> mono (\<partial>\<^sub>F f)"
   by (simp add: ord_pres_dual ord_pres_mono)
 
 class lattice_with_dual = lattice + dual +
   assumes sup_dual_def: "\<partial> (x \<squnion> y) = \<partial> x \<sqinter> \<partial> y"
 
 begin
 
 subclass order_with_dual
   by (unfold_locales, metis inf.absorb_iff2 sup_absorb1 sup_commute sup_dual_def)
 
 lemma inf_dual: "\<partial> (x \<sqinter> y) = \<partial> x \<squnion> \<partial> y"
   by (metis invol_dual_var sup_dual_def) 
 
 lemma inf_to_sup: "x \<sqinter> y = \<partial> (\<partial> x \<squnion> \<partial> y)"
   using inf_dual dual_iff by fastforce
 
 lemma sup_to_inf: "x \<squnion> y = \<partial> (\<partial> x \<sqinter> \<partial> y)"
   by (simp add: inf_dual)
 
 end
 
 class bounded_lattice_with_dual = lattice_with_dual + bounded_lattice
 
 begin
 
 lemma bot_dual: "\<partial> \<bottom> = \<top>"
   by (metis dual_dual_ord dual_iff le_bot top_greatest)
 
 lemma top_dual: "\<partial> \<top> = \<bottom>"
   using bot_dual dual_iff by force
 
 end
 
 class boolean_algebra_with_dual = lattice_with_dual + boolean_algebra
 
 sublocale boolean_algebra \<subseteq> badual: boolean_algebra_with_dual _ _ _ _ _ _ _ _ uminus
   by unfold_locales simp_all
 
 class Sup_lattice_with_dual = Sup_lattice + dual +
   assumes Sups_dual_def: "\<partial> \<circ> Sup = Infs \<circ> (`) \<partial>"
 
 class Inf_lattice_with_dual = Inf_lattice + dual +
   assumes Sups_dual_def: "\<partial> \<circ> Supi = Inf \<circ> (`) \<partial>"
 
 class complete_lattice_with_dual = complete_lattice + dual +
   assumes Sups_dual_def: "\<partial> \<circ> Sup = Inf \<circ> (`) \<partial>"
 
 sublocale Sup_lattice_with_dual \<subseteq> sclatd: complete_lattice_with_dual Infs Sup infs "(\<le>)" le sups bots tops "\<partial>"
   by (unfold_locales, simp add: Sups_dual_def)
 
 sublocale Inf_lattice_with_dual \<subseteq> iclatd: complete_lattice_with_dual Inf Supi infi "(\<le>)" le supi boti topi "\<partial>"
   by (unfold_locales, simp add: Sups_dual_def)
 
 context complete_lattice_with_dual
 begin
 
 lemma Inf_dual: "\<partial> \<circ> Inf = Sup \<circ> (`) \<partial>"
   by (metis comp_assoc comp_id fun.map_id Sups_dual_def image_dual invol_dual)
 
 lemma Inf_dual_var: "\<partial> (\<Sqinter>X) = \<Squnion>(\<partial> ` X)"
   using comp_eq_dest Inf_dual by fastforce
 
 lemma Inf_to_Sup: "Inf = \<partial> \<circ> Sup \<circ> (`) \<partial>"
   by (auto simp add: Sups_dual_def image_comp)
 
 lemma Inf_to_Sup_var: "\<Sqinter>X = \<partial> (\<Squnion>(\<partial> ` X))"
   using Inf_dual_var dual_iff by fastforce
 
 lemma Sup_to_Inf: "Sup = \<partial> \<circ> Inf \<circ> (`) \<partial>"
   by (auto simp add: Inf_dual image_comp)
 
 lemma Sup_to_Inf_var: "\<Squnion>X = \<partial> (\<Sqinter>(\<partial> ` X))"
   using Sup_to_Inf by force
 
 lemma Sup_dual_def_var: "\<partial> (\<Squnion>X) = \<Sqinter> (\<partial> ` X)"
   using comp_eq_dest Sups_dual_def by fastforce
 
 lemma bot_dual_def: "\<partial> \<top> = \<bottom>"
-  by (smt Inf_UNIV Sup_UNIV Sups_dual_def surj_dual o_eq_dest)
+  by (smt (verit) Inf_UNIV Sup_UNIV Sups_dual_def surj_dual o_eq_dest)
 
 lemma top_dual_def: "\<partial> \<bottom> = \<top>"
   using bot_dual_def dual_iff by blast
 
 lemma inf_dual2: "\<partial> (x \<sqinter> y) = \<partial> x \<squnion> \<partial> y"
-  by (smt comp_eq_elim Inf_dual Inf_empty Inf_insert SUP_insert inf_top.right_neutral)
+  by (smt (verit) comp_eq_elim Inf_dual Inf_empty Inf_insert SUP_insert inf_top.right_neutral)
 
 lemma sup_dual: "\<partial> (x \<squnion> y) = \<partial> x \<sqinter> \<partial> y"
   by (metis inf_dual2 dual_iff)
 
 subclass lattice_with_dual
   by (unfold_locales, auto simp: inf_dual sup_dual)
 
 subclass bounded_lattice_with_dual..
 
 end
 
 end
diff --git a/thys/Order_Lattice_Props/Order_Lattice_Props.thy b/thys/Order_Lattice_Props/Order_Lattice_Props.thy
--- a/thys/Order_Lattice_Props/Order_Lattice_Props.thy
+++ b/thys/Order_Lattice_Props/Order_Lattice_Props.thy
@@ -1,1227 +1,1227 @@
 (* 
   Title: Properties of Orderings and Lattices
   Author: Georg Struth 
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
 *)
 
 section \<open>Properties of Orderings and Lattices\<close>
 
 theory Order_Lattice_Props
   imports Order_Duality
 
 begin
 
 subsection \<open>Basic Definitions for Orderings and Lattices\<close>
 
 text \<open>The first definition is for order morphisms --- isotone (order-preserving, monotone) functions. 
 An order isomorphism is an order-preserving bijection. This should be defined in the class ord, but mono requires order.\<close>
 
 definition ord_homset :: "('a::order \<Rightarrow> 'b::order) set" where
  "ord_homset = {f::'a::order \<Rightarrow> 'b::order. mono f}"
 
 definition ord_embed :: "('a::order \<Rightarrow> 'b::order) \<Rightarrow> bool" where
  "ord_embed f = (\<forall>x y. f x \<le> f y \<longleftrightarrow> x \<le> y)"
 
 definition ord_iso :: "('a::order \<Rightarrow> 'b::order) \<Rightarrow> bool" where
   "ord_iso = bij \<sqinter> mono \<sqinter> (mono \<circ> the_inv)"
 
 lemma ord_embed_alt: "ord_embed f = (mono f \<and> (\<forall>x y. f x \<le> f y \<longrightarrow> x \<le> y))"
   using mono_def ord_embed_def by auto
 
 lemma ord_embed_homset: "ord_embed f \<Longrightarrow> f \<in> ord_homset"
   by (simp add: mono_def ord_embed_def ord_homset_def)
 
 lemma ord_embed_inj: "ord_embed f \<Longrightarrow> inj f"
   unfolding ord_embed_def inj_def by (simp add: eq_iff)
 
 lemma ord_iso_ord_embed: "ord_iso f \<Longrightarrow> ord_embed f"
   unfolding ord_iso_def ord_embed_def bij_def inj_def mono_def
   by (clarsimp, metis inj_def the_inv_f_f)
 
 lemma ord_iso_alt: "ord_iso f = (ord_embed f \<and> surj f)"
   unfolding ord_iso_def ord_embed_def surj_def bij_def inj_def mono_def 
   apply safe
   by simp_all (metis eq_iff inj_def the_inv_f_f)+
 
 lemma ord_iso_the_inv: "ord_iso f \<Longrightarrow> mono (the_inv f)"
   by (simp add: ord_iso_def)
 
 lemma ord_iso_inv1: "ord_iso f \<Longrightarrow> (the_inv f) \<circ> f = id"
   using ord_embed_inj ord_iso_ord_embed the_inv_into_f_f by fastforce
 
 lemma ord_iso_inv2: "ord_iso f \<Longrightarrow> f \<circ> (the_inv f) = id"
   using f_the_inv_into_f ord_embed_inj ord_iso_alt by fastforce
 
 typedef (overloaded) ('a,'b) ord_homset = "ord_homset::('a::order \<Rightarrow> 'b::order) set" 
   by (force simp: ord_homset_def mono_def) 
 
 setup_lifting type_definition_ord_homset 
 
 text \<open>The next definition is for the set of fixpoints of a given function. It is important in the context of orders,
 for instance for proving Tarski's fixpoint theorem, but does not really belong here.\<close>
 
 definition Fix :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set" where 
   "Fix f = {x. f x = x}"
 
 lemma retraction_prop: "f \<circ> f = f \<Longrightarrow> f x = x \<longleftrightarrow> x \<in> range f"
   by (metis comp_apply f_inv_into_f rangeI)
 
 lemma retraction_prop_fix: "f \<circ> f = f \<Longrightarrow> range f = Fix f"
   unfolding Fix_def using retraction_prop by fastforce
 
 lemma Fix_map_dual: "Fix \<circ> \<partial>\<^sub>F = (`) \<partial> \<circ> Fix"
   unfolding Fix_def map_dual_def comp_def fun_eq_iff
-  by (smt Collect_cong invol_dual pointfree_idE setcompr_eq_image)
+  by (smt (verit) Collect_cong invol_dual pointfree_idE setcompr_eq_image)
 
 lemma Fix_map_dual_var: "Fix (\<partial>\<^sub>F f) = \<partial> ` (Fix f)"
   by (metis Fix_map_dual o_def)
 
 lemma gfp_dual: "(\<partial>::'a::complete_lattice_with_dual \<Rightarrow> 'a) \<circ> gfp = lfp \<circ> \<partial>\<^sub>F"
 proof-
   {fix f:: "'a \<Rightarrow> 'a"
   have "\<partial> (gfp f) = \<partial> (\<Squnion>{u. u \<le> f u})"
     by (simp add: gfp_def)
   also have "... = \<Sqinter>(\<partial> ` {u. u \<le> f u})"
     by (simp add: Sup_dual_def_var)
   also have "... = \<Sqinter>{\<partial> u |u. u \<le> f u}"
     by (simp add: setcompr_eq_image)
   also have "... = \<Sqinter>{u |u. (\<partial>\<^sub>F f) u \<le> u}"
     by (metis (no_types, opaque_lifting) dual_dual_ord dual_iff map_dual_def o_def)
   finally have "\<partial> (gfp f) = lfp (\<partial>\<^sub>F f)"
     by (metis lfp_def)}
   thus ?thesis
     by auto
 qed
 
 lemma gfp_dual_var: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'a"
   shows "\<partial> (gfp f) = lfp (\<partial>\<^sub>F f)"
   using comp_eq_elim gfp_dual by blast
 
 lemma gfp_to_lfp: "gfp = (\<partial>::'a::complete_lattice_with_dual \<Rightarrow> 'a) \<circ> lfp \<circ> \<partial>\<^sub>F"
   by (simp add: comp_assoc fun_dual2 gfp_dual)
 
 lemma gfp_to_lfp_var: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'a"
   shows "gfp f = \<partial> (lfp (\<partial>\<^sub>F f))"
   by (metis gfp_dual_var invol_dual_var)
 
 lemma lfp_dual: "(\<partial>::'a::complete_lattice_with_dual \<Rightarrow> 'a) \<circ> lfp = gfp \<circ> \<partial>\<^sub>F"
   by (simp add: comp_assoc gfp_to_lfp map_dual_invol)
 
 lemma lfp_dual_var: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'a"
   shows "\<partial> (lfp f) = gfp (map_dual f)"
   using comp_eq_dest_lhs lfp_dual by fastforce
 
 lemma lfp_to_gfp: "lfp = (\<partial>::'a::complete_lattice_with_dual \<Rightarrow> 'a) \<circ> gfp \<circ> \<partial>\<^sub>F"
   by (simp add: comp_assoc gfp_dual map_dual_invol)
 
 lemma lfp_to_gfp_var: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'a"
   shows "lfp f = \<partial> (gfp (\<partial>\<^sub>F f))"
   by (metis invol_dual_var lfp_dual_var)
 
 lemma lfp_in_Fix: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows "mono f \<Longrightarrow> lfp f \<in> Fix f"
   by (metis (mono_tags, lifting) Fix_def lfp_unfold mem_Collect_eq)
 
 lemma gfp_in_Fix: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows "mono f \<Longrightarrow> gfp f \<in> Fix f"
   by (metis (mono_tags, lifting) Fix_def gfp_unfold mem_Collect_eq)
 
 lemma nonempty_Fix: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows "mono f \<Longrightarrow> Fix f \<noteq> {}"
   using lfp_in_Fix by fastforce
 
 
 text \<open>Next the minimal and maximal elements of an ordering are defined.\<close>
 
 context ord
 begin
 
 definition min_set :: "'a set \<Rightarrow> 'a set" where 
   "min_set X = {y \<in> X. \<forall>x \<in> X. x \<le> y \<longrightarrow> x = y}"
 
 definition max_set :: "'a set \<Rightarrow> 'a set" where 
   "max_set X = {x \<in> X. \<forall>y \<in> X. x \<le> y \<longrightarrow> x = y}"
 
 end
 
 context ord_with_dual
 begin
 
 lemma min_max_set_dual: "(`) \<partial> \<circ> min_set = max_set \<circ> (`) \<partial>"  
   unfolding max_set_def min_set_def fun_eq_iff comp_def 
   apply safe
   using dual_dual_ord inj_dual_iff by auto
 
 lemma min_max_set_dual_var: "\<partial> ` (min_set X) = max_set (\<partial> ` X)"
   using comp_eq_dest min_max_set_dual by fastforce  
 
 lemma max_min_set_dual: "(`) \<partial> \<circ> max_set = min_set \<circ> (`) \<partial>"
   by (metis (no_types, opaque_lifting) comp_id fun.map_comp id_comp image_dual min_max_set_dual)  
 
 lemma min_to_max_set: "min_set = (`) \<partial> \<circ> max_set \<circ> (`) \<partial>"
   by (metis comp_id image_dual max_min_set_dual o_assoc)
 
 lemma max_min_set_dual_var: "\<partial> ` (max_set X) = min_set (\<partial> ` X)"
   using comp_eq_dest max_min_set_dual by fastforce
 
 lemma min_to_max_set_var: "min_set X = \<partial> ` (max_set (\<partial> ` X))"
   by (simp add: max_min_set_dual_var pointfree_idE)
 
 end
 
 text \<open>Next, directed and filtered sets, upsets, downsets, filters and ideals in posets are defined.\<close>
 
 context ord
 begin
 
 definition directed :: "'a set \<Rightarrow> bool" where
  "directed X = (\<forall>Y. finite Y \<and> Y \<subseteq> X \<longrightarrow> (\<exists>x \<in> X. \<forall>y \<in> Y. y \<le> x))"
 
 definition filtered :: "'a set \<Rightarrow> bool" where
  "filtered X = (\<forall>Y. finite Y \<and> Y \<subseteq> X \<longrightarrow> (\<exists>x \<in> X. \<forall>y \<in> Y. x \<le> y))"
 
 definition downset_set :: "'a set \<Rightarrow> 'a set" ("\<Down>") where
   "\<Down>X = {y. \<exists>x \<in> X. y \<le> x}"
 
 definition upset_set :: "'a set \<Rightarrow> 'a set" ("\<Up>") where
  "\<Up>X = {y. \<exists>x \<in> X. x \<le> y}"
 
 definition downset :: "'a \<Rightarrow> 'a set" ("\<down>") where 
   "\<down> = \<Down> \<circ> \<eta>"
 
 definition upset :: "'a \<Rightarrow> 'a set" ("\<up>") where 
   "\<up> = \<Up> \<circ> \<eta>"
 
 definition downsets :: "'a set set" where  
   "downsets = Fix \<Down>"
  
 definition upsets :: "'a set set" where
   "upsets = Fix \<Up>"
 
 definition "downclosed_set X = (X \<in> downsets)"
 
 definition "upclosed_set X = (X \<in> upsets)"
 
 definition ideals :: "'a set set" where
   "ideals = {X. X \<noteq> {} \<and> downclosed_set X \<and> directed X}"
 
 definition filters :: "'a set set" where
   "filters = {X. X \<noteq> {} \<and> upclosed_set X \<and> filtered X}"
 
 abbreviation "idealp X \<equiv> X \<in> ideals"
 
 abbreviation "filterp X \<equiv> X \<in> filters"
 
 end
 
 text \<open>These notions are pair-wise dual.\<close>
 
 text \<open>Filtered and directed sets are dual.\<close>
 
 context ord_with_dual
 begin
 
 lemma filtered_directed_dual: "filtered \<circ> (`) \<partial> = directed"
   unfolding filtered_def directed_def fun_eq_iff comp_def
   apply clarsimp
   apply safe
    apply (meson finite_imageI imageI image_mono dual_dual_ord)
-  by (smt finite_subset_image imageE ord_dual)
+  by (smt (verit, ccfv_threshold) finite_subset_image imageE ord_dual)
 
 lemma directed_filtered_dual: "directed \<circ> (`) \<partial> = filtered"
   using filtered_directed_dual by (metis comp_id image_dual o_assoc) 
 
 lemma filtered_to_directed: "filtered X = directed (\<partial> ` X)"
   by (metis comp_apply directed_filtered_dual)
 
 text \<open>Upsets and downsets are dual.\<close>
 
 lemma downset_set_upset_set_dual: "(`) \<partial> \<circ> \<Down> = \<Up> \<circ> (`) \<partial>"
   unfolding downset_set_def upset_set_def fun_eq_iff comp_def
   apply safe
    apply (meson image_eqI ord_dual)
   by (clarsimp, metis (mono_tags, lifting) dual_iff image_iff mem_Collect_eq ord_dual)
 
 lemma upset_set_downset_set_dual: "(`) \<partial> \<circ> \<Up> = \<Down> \<circ> (`) \<partial>"
   using downset_set_upset_set_dual by (metis (no_types, opaque_lifting) comp_id id_comp image_dual o_assoc)
 
 lemma upset_set_to_downset_set: "\<Up> = (`) \<partial> \<circ> \<Down> \<circ> (`) \<partial>"
   by (simp add: comp_assoc downset_set_upset_set_dual)
 
 lemma upset_set_to_downset_set2: "\<Up> X = \<partial> ` (\<Down> (\<partial> ` X))"
   by (simp add: upset_set_to_downset_set)
 
 lemma downset_upset_dual: "(`) \<partial> \<circ> \<down> = \<up> \<circ> \<partial>"
   using downset_def upset_def upset_set_to_downset_set by fastforce
 
 lemma upset_to_downset: "(`) \<partial> \<circ> \<up> = \<down> \<circ> \<partial>"
   by (metis comp_assoc id_apply ord.downset_def ord.upset_def power_set_func_nat_trans upset_set_downset_set_dual)
 
 lemma upset_to_downset2: "\<up> = (`) \<partial> \<circ> \<down> \<circ> \<partial>"
   by (simp add: comp_assoc downset_upset_dual)
 
 lemma upset_to_downset3: "\<up> x = \<partial> ` (\<down> (\<partial> x))"
   by (simp add: upset_to_downset2)
 
 lemma downsets_upsets_dual: "(X \<in> downsets) = (\<partial> ` X \<in> upsets)"
   unfolding downsets_def upsets_def Fix_def
-  by (smt comp_eq_dest downset_set_upset_set_dual image_inv_f_f inj_dual mem_Collect_eq)
+  by (smt (verit) comp_eq_dest downset_set_upset_set_dual image_inv_f_f inj_dual mem_Collect_eq)
 
 lemma downset_setp_upset_setp_dual: "upclosed_set \<circ> (`) \<partial> = downclosed_set"
   unfolding downclosed_set_def upclosed_set_def using downsets_upsets_dual by fastforce
 
 lemma upsets_to_downsets: "(X \<in> upsets) = (\<partial> ` X \<in> downsets)"
   by (simp add: downsets_upsets_dual image_comp)
 
 lemma upset_setp_downset_setp_dual: "downclosed_set \<circ> (`) \<partial> = upclosed_set"
   by (metis comp_id downset_setp_upset_setp_dual image_dual o_assoc)
 
 text \<open>Filters and ideals are dual.\<close>
 
 lemma ideals_filters_dual: "(X \<in> ideals) = ((\<partial> ` X) \<in> filters)"
-  by (smt comp_eq_dest_lhs directed_filtered_dual image_inv_f_f image_is_empty inv_unique_comp filters_def ideals_def inj_dual invol_dual mem_Collect_eq upset_setp_downset_setp_dual)
+  by (smt (verit) comp_eq_dest_lhs directed_filtered_dual image_inv_f_f image_is_empty inv_unique_comp filters_def ideals_def inj_dual invol_dual mem_Collect_eq upset_setp_downset_setp_dual)
 
 lemma idealp_filterp_dual: "idealp = filterp \<circ> (`) \<partial>"
   unfolding fun_eq_iff by (simp add: ideals_filters_dual)
 
 lemma filters_to_ideals: "(X \<in> filters) = ((\<partial> ` X) \<in> ideals)"
   by (simp add: ideals_filters_dual image_comp)
 
 lemma filterp_idealp_dual: "filterp = idealp \<circ> (`) \<partial>"
   unfolding fun_eq_iff by (simp add: filters_to_ideals)
 
 end
 
 subsection \<open>Properties of Orderings\<close>
 
 context ord
 begin
 
 lemma directed_nonempty: "directed X \<Longrightarrow> X \<noteq> {}"
   unfolding directed_def by fastforce
 
 lemma directed_ub: "directed X \<Longrightarrow> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. x \<le> z \<and> y \<le> z)"
   by (meson empty_subsetI directed_def finite.emptyI finite_insert insert_subset order_refl)
 
 lemma downset_set_prop: "\<Down> = Union \<circ> (`) \<down>"
   unfolding downset_set_def downset_def fun_eq_iff by fastforce
 
 lemma downset_set_prop_var: "\<Down>X = (\<Union>x \<in> X. \<down>x)"
   by (simp add: downset_set_prop)
 
 lemma downset_prop: "\<down>x = {y. y \<le> x}"
   unfolding downset_def downset_set_def fun_eq_iff by fastforce
 
 lemma downset_prop2: "y \<le> x \<Longrightarrow> y \<in> \<down>x"
   by (simp add: downset_prop)
 
 lemma ideals_downsets: "X \<in> ideals \<Longrightarrow> X \<in> downsets"
   by (simp add: downclosed_set_def ideals_def)
 
 lemma ideals_directed: "X \<in> ideals \<Longrightarrow> directed X"
   by (simp add: ideals_def)
 
 end
 
 context preorder
 begin
 
 lemma directed_prop: "X \<noteq> {} \<Longrightarrow> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. x \<le> z \<and> y \<le> z) \<Longrightarrow> directed X"
 proof-
   assume h1: "X \<noteq> {}"
   and h2: "\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. x \<le> z \<and> y \<le> z"
   {fix Y
   have "finite Y \<Longrightarrow> Y \<subseteq> X \<Longrightarrow> (\<exists>x \<in> X. \<forall>y \<in> Y. y \<le> x)"
   proof (induct rule: finite_induct)
     case empty
     then show ?case
       using h1 by blast 
   next
     case (insert x F)
     then show ?case
       by (metis h2 insert_iff insert_subset order_trans) 
   qed}
   thus ?thesis
     by (simp add: directed_def)
 qed
 
 lemma directed_alt: "directed X = (X \<noteq> {} \<and> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. x \<le> z \<and> y \<le> z))"
   by (metis directed_prop directed_nonempty directed_ub)
 
 lemma downset_set_prop_var2: "x \<in> \<Down>X \<Longrightarrow> y \<le> x \<Longrightarrow> y \<in> \<Down>X"
   unfolding downset_set_def using order_trans by blast
 
 lemma downclosed_set_iff: "downclosed_set X = (\<forall>x \<in> X. \<forall>y. y \<le> x \<longrightarrow> y \<in> X)"
   unfolding downclosed_set_def downsets_def Fix_def downset_set_def by auto
 
 lemma downclosed_downset_set: "downclosed_set (\<Down>X)"
   by (simp add: downclosed_set_iff downset_set_prop_var2 downset_def)
 
 lemma downclosed_downset: "downclosed_set (\<down>x)"
   by (simp add: downclosed_downset_set downset_def)
  
 lemma downset_set_ext: "id \<le> \<Down>"
   unfolding le_fun_def id_def downset_set_def by auto 
 
 lemma downset_set_iso: "mono \<Down>"
   unfolding mono_def downset_set_def by blast
 
 lemma downset_set_idem [simp]: "\<Down> \<circ> \<Down> = \<Down>"
   unfolding fun_eq_iff downset_set_def using order_trans by auto
 
 lemma downset_faithful: "\<down>x \<subseteq> \<down>y \<Longrightarrow> x \<le> y"
   by (simp add: downset_prop subset_eq)
 
 lemma downset_iso_iff: "(\<down>x \<subseteq> \<down>y) = (x \<le> y)"
   using atMost_iff downset_prop order_trans by blast
 
 text \<open>The following proof uses the Axiom of Choice.\<close>
 
 lemma downset_directed_downset_var [simp]: "directed (\<Down>X) = directed X"
 proof
   assume h1: "directed X"
   {fix Y
   assume h2: "finite Y" and h3: "Y \<subseteq> \<Down>X"
   hence "\<forall>y. \<exists>x. y \<in> Y \<longrightarrow> x \<in> X \<and>  y \<le> x"
     by (force simp: downset_set_def)
   hence "\<exists>f. \<forall>y. y \<in> Y \<longrightarrow>  f y \<in> X \<and> y \<le> f y"
     by (rule choice)
   hence "\<exists>f. finite (f ` Y) \<and> f ` Y \<subseteq> X \<and> (\<forall>y \<in> Y. y \<le> f y)"
     by (metis finite_imageI h2 image_subsetI)
   hence "\<exists>Z. finite Z \<and> Z \<subseteq> X \<and> (\<forall>y \<in> Y. \<exists> z \<in> Z. y \<le> z)"
     by fastforce
   hence "\<exists>Z. finite Z \<and> Z \<subseteq> X \<and> (\<forall>y \<in> Y. \<exists> z \<in> Z. y \<le> z) \<and> (\<exists>x \<in> X. \<forall> z \<in> Z. z \<le> x)"
     by (metis directed_def h1)
   hence "\<exists>x \<in> X. \<forall>y \<in> Y. y \<le> x"
     by (meson order_trans)}
   thus "directed (\<Down>X)"
     unfolding directed_def downset_set_def by fastforce
 next 
   assume "directed (\<Down>X)"
   thus "directed X"
     unfolding directed_def downset_set_def 
     apply clarsimp
-    by (smt Ball_Collect order_refl order_trans subsetCE)
+    by (smt (verit) Ball_Collect order_refl order_trans subsetCE)
 qed
 
 lemma downset_directed_downset [simp]: "directed \<circ> \<Down> = directed"
   unfolding fun_eq_iff by simp
 
 lemma directed_downset_ideals: "directed (\<Down>X) = (\<Down>X \<in> ideals)"
   by (metis (mono_tags, lifting) CollectI Fix_def directed_alt downset_set_idem downclosed_set_def downsets_def ideals_def o_def ord.ideals_directed)
 
 lemma downclosed_Fix: "downclosed_set X = (\<Down>X = X)"
   by (metis (mono_tags, lifting) CollectD Fix_def downclosed_downset_set downclosed_set_def downsets_def)
   
 end
 
 lemma downset_iso: "mono (\<down>::'a::order \<Rightarrow> 'a set)"
   by (simp add: downset_iso_iff mono_def)
 
 lemma mono_downclosed: 
   fixes f :: "'a::order \<Rightarrow> 'b::order"
   assumes "mono f"
   shows "\<forall>Y. downclosed_set Y \<longrightarrow> downclosed_set (f -` Y)"   
   by (simp add: assms downclosed_set_iff monoD)
 
 lemma
   fixes f :: "'a::order \<Rightarrow> 'b::order"
   assumes "mono f"
   shows "\<forall>Y. downclosed_set X \<longrightarrow> downclosed_set (f ` X)" (*nitpick*)
   oops
 
 lemma downclosed_mono:
   fixes f :: "'a::order \<Rightarrow> 'b::order"
   assumes "\<forall>Y. downclosed_set Y \<longrightarrow> downclosed_set (f -` Y)"
   shows "mono f"
 proof-
   {fix x y :: "'a::order"
   assume h: "x \<le> y"
   have "downclosed_set (\<down> (f y))"
     unfolding downclosed_set_def downsets_def Fix_def downset_set_def downset_def by auto
   hence "downclosed_set (f -` (\<down> (f y)))"
     by (simp add: assms)
   hence "downclosed_set {z. f z \<le> f y}"
     unfolding vimage_def downset_def downset_set_def by auto
   hence "\<forall>z w. (f z \<le> f y \<and> w \<le> z) \<longrightarrow> f w \<le> f y"
     unfolding downclosed_set_def downclosed_set_def downsets_def Fix_def downset_set_def by force
   hence "f x \<le> f y"
     using h by blast}
   thus ?thesis..
 qed
 
 lemma mono_downclosed_iff: "mono f = (\<forall>Y. downclosed_set Y \<longrightarrow> downclosed_set (f -` Y))"
   using mono_downclosed downclosed_mono by auto
 
 context order
 begin
 
 lemma downset_inj: "inj \<down>"
   by (metis injI downset_iso_iff order.eq_iff)
 
 lemma "(X \<subseteq> Y) = (\<Down>X \<subseteq> \<Down>Y)" (*nitpick*)
   oops
 
 end
 
 context lattice
 begin
 
 lemma lat_ideals: "X \<in> ideals = (X \<noteq> {} \<and> X \<in> downsets \<and> (\<forall>x \<in> X. \<forall> y \<in> X. x \<squnion> y \<in> X))"
   unfolding ideals_def directed_alt downsets_def Fix_def downset_set_def downclosed_set_def
-  by (clarsimp, smt sup.cobounded1 sup.orderE sup.orderI sup_absorb2 sup_left_commute mem_Collect_eq)
+  using local.sup.bounded_iff local.sup_ge2 by blast
+    
 
 end
 
 context bounded_lattice
 begin
 
 lemma bot_ideal: "X \<in> ideals \<Longrightarrow> \<bottom> \<in> X"
   unfolding ideals_def downclosed_set_def downsets_def Fix_def downset_set_def by fastforce
 
 end
 
 context complete_lattice
 begin
 
 lemma Sup_downset_id [simp]: "Sup \<circ> \<down> = id"
   using Sup_atMost atMost_def downset_prop by fastforce
 
 lemma downset_Sup_id: "id \<le> \<down> \<circ> Sup"
   by (simp add: Sup_upper downset_prop le_funI subsetI)
 
 lemma Inf_Sup_var: "\<Squnion>(\<Inter>x \<in> X. \<down>x) = \<Sqinter>X"
   unfolding downset_prop by (simp add: Collect_ball_eq Inf_eq_Sup)
 
 lemma Inf_pres_downset_var: "(\<Inter>x \<in> X. \<down>x) = \<down>(\<Sqinter>X)"
   unfolding downset_prop by (safe, simp_all add: le_Inf_iff)
 
 end
 
 
 subsection \<open>Dual Properties of Orderings\<close>
 
 context ord_with_dual
 begin
 
 lemma filtered_nonempty: "filtered X \<Longrightarrow> X \<noteq> {}"
   using filtered_to_directed ord.directed_nonempty by auto
 
 lemma filtered_lb: "filtered X \<Longrightarrow> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. z \<le> x \<and> z \<le> y)"
   using filtered_to_directed directed_ub dual_dual_ord by fastforce
 
 lemma upset_set_prop_var: "\<Up>X = (\<Union>x \<in> X. \<up>x)"
   by (simp add: image_Union downset_set_prop_var upset_set_to_downset_set2 upset_to_downset2)
 
 lemma upset_set_prop: "\<Up> = Union \<circ> (`) \<up>"
   unfolding fun_eq_iff by (simp add: upset_set_prop_var)
 
 lemma upset_prop: "\<up>x = {y. x \<le> y}"
   unfolding upset_to_downset3 downset_prop image_def using dual_dual_ord by fastforce
 
 lemma upset_prop2: "x \<le> y \<Longrightarrow> y \<in> \<up>x"
   by (simp add: upset_prop)
 
 lemma filters_upsets: "X \<in> filters \<Longrightarrow> X \<in> upsets"
   by (simp add: upclosed_set_def filters_def)
 
 lemma filters_filtered: "X \<in> filters \<Longrightarrow> filtered X"
   by (simp add: filters_def)
 
 end
 
 context preorder_with_dual
 begin
 
 lemma filtered_prop: "X \<noteq> {} \<Longrightarrow> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. z \<le> x \<and> z \<le> y) \<Longrightarrow> filtered X"
   unfolding filtered_to_directed 
     by (rule directed_prop, blast, metis (full_types) image_iff ord_dual)
  
 lemma filtered_alt: "filtered X = (X \<noteq> {} \<and> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. z \<le> x \<and> z \<le> y))"
   by (metis image_empty directed_alt filtered_to_directed filtered_lb filtered_prop)
 
 lemma up_set_prop_var2: "x \<in> \<Up>X \<Longrightarrow> x \<le> y \<Longrightarrow> y \<in> \<Up>X"
   using downset_set_prop_var2 dual_iff ord_dual upset_set_to_downset_set2 by fastforce
 
 lemma upclosed_set_iff: "upclosed_set X = (\<forall>x \<in> X. \<forall>y. x \<le> y \<longrightarrow> y \<in> X)"
   unfolding upclosed_set_def upsets_def Fix_def upset_set_def by auto
 
 lemma upclosed_upset_set: "upclosed_set (\<Up>X)"
   using up_set_prop_var2 upclosed_set_iff by blast
 
 lemma upclosed_upset: "upclosed_set (\<up>x)"
   by (simp add: upset_def upclosed_upset_set) 
   
 lemma upset_set_ext: "id \<le> \<Up>"
-  by (smt comp_def comp_id image_mono le_fun_def downset_set_ext image_dual upset_set_to_downset_set2)
+  by (smt (verit) comp_def comp_id image_mono le_fun_def downset_set_ext image_dual upset_set_to_downset_set2)
 
 lemma upset_set_anti: "mono \<Up>"
   by (metis image_mono downset_set_iso upset_set_to_downset_set2 mono_def)
 
 lemma up_set_idem [simp]: "\<Up> \<circ> \<Up> = \<Up>"
   by (metis comp_assoc downset_set_idem upset_set_downset_set_dual upset_set_to_downset_set)
 
 lemma upset_faithful: "\<up>x \<subseteq> \<up>y \<Longrightarrow> y \<le> x"
   by (metis inj_image_subset_iff downset_faithful dual_dual_ord inj_dual upset_to_downset3)
 
 lemma upset_anti_iff: "(\<up>y \<subseteq> \<up>x) = (x \<le> y)"
   by (metis downset_iso_iff ord_dual upset_to_downset3 subset_image_iff upset_faithful)
 
 lemma upset_filtered_upset [simp]: "filtered \<circ> \<Up> = filtered"
   by (metis comp_assoc directed_filtered_dual downset_directed_downset upset_set_downset_set_dual)
 
 lemma filtered_upset_filters: "filtered (\<Up>X) = (\<Up>X \<in> filters)"
   by (metis comp_apply directed_downset_ideals filtered_to_directed filterp_idealp_dual upset_set_downset_set_dual)
 
 lemma upclosed_Fix: "upclosed_set X = (\<Up>X = X)"
   by (simp add: Fix_def upclosed_set_def upsets_def)
 
 end
 
 lemma upset_anti: "antimono (\<up>::'a::order_with_dual \<Rightarrow> 'a set)"
   by (simp add: antimono_def upset_anti_iff)
 
 lemma mono_upclosed: 
   fixes f :: "'a::order_with_dual \<Rightarrow> 'b::order_with_dual"
   assumes "mono f"
   shows "\<forall>Y. upclosed_set Y \<longrightarrow> upclosed_set (f -` Y)"
   by (simp add: assms monoD upclosed_set_iff)
 
 lemma mono_upclosed: 
   fixes f :: "'a::order_with_dual \<Rightarrow> 'b::order_with_dual"
   assumes "mono f"
   shows "\<forall>Y. upclosed_set X \<longrightarrow> upclosed_set (f ` X)" (*nitpick*)
   oops
 
 lemma upclosed_mono:
   fixes f :: "'a::order_with_dual \<Rightarrow> 'b::order_with_dual"
   assumes "\<forall>Y. upclosed_set Y \<longrightarrow> upclosed_set (f -` Y)"
   shows "mono f"
   by (metis (mono_tags, lifting) assms dual_order.refl mem_Collect_eq monoI order.trans upclosed_set_iff vimageE vimageI2)
 
 lemma mono_upclosed_iff: 
   fixes f :: "'a::order_with_dual \<Rightarrow> 'b::order_with_dual"
   shows "mono f = (\<forall>Y. upclosed_set Y \<longrightarrow> upclosed_set (f -` Y))"
   using mono_upclosed upclosed_mono by auto
 
 context order_with_dual
 begin
 
 lemma upset_inj: "inj \<up>"
   by (metis inj_compose inj_on_imageI2 downset_inj inj_dual upset_to_downset)
 
 lemma "(X \<subseteq> Y) = (\<Up>Y \<subseteq> \<Up>X)" (*nitpick*)
   oops
 
 end
 
 context lattice_with_dual
 begin
 
 lemma lat_filters: "X \<in> filters = (X \<noteq> {} \<and> X \<in> upsets \<and> (\<forall>x \<in> X. \<forall> y \<in> X. x \<sqinter> y \<in> X))"
   unfolding filters_to_ideals upsets_to_downsets inf_to_sup lat_ideals
-  by (smt image_iff image_inv_f_f image_is_empty inj_image_mem_iff inv_unique_comp inj_dual invol_dual)
+  by (smt (verit) image_iff image_inv_f_f image_is_empty inj_image_mem_iff inv_unique_comp inj_dual invol_dual)
 
 end
 
 context bounded_lattice_with_dual
 begin
 
 lemma top_filter: "X \<in> filters \<Longrightarrow> \<top> \<in> X"
   using bot_ideal inj_image_mem_iff inj_dual filters_to_ideals top_dual by fastforce
 
 end
 
 context complete_lattice_with_dual
 begin
 
 lemma Inf_upset_id [simp]: "Inf \<circ> \<up> = id"
   by (metis comp_assoc comp_id Sup_downset_id Sups_dual_def downset_upset_dual invol_dual)
 
 lemma upset_Inf_id: "id \<le> \<up> \<circ> Inf"
   by (simp add: Inf_lower le_funI subsetI upset_prop)
 
 lemma Sup_Inf_var: " \<Sqinter>(\<Inter>x \<in> X. \<up>x) = \<Squnion>X"
   unfolding upset_prop by (simp add: Collect_ball_eq Sup_eq_Inf)
 
 lemma Sup_dual_upset_var: "(\<Inter>x \<in> X. \<up>x) = \<up>(\<Squnion>X)"
   unfolding upset_prop by (safe, simp_all add: Sup_le_iff)
 
 end
 
 
 subsection \<open>Properties of Complete Lattices\<close>
 
 definition "Inf_closed_set X = (\<forall>Y \<subseteq> X. \<Sqinter>Y \<in> X)"
 
 definition "Sup_closed_set X = (\<forall>Y \<subseteq> X. \<Squnion>Y \<in> X)"
 
 definition "inf_closed_set X = (\<forall>x \<in> X. \<forall>y \<in> X. x \<sqinter> y \<in> X)" 
 
 definition "sup_closed_set X = (\<forall>x \<in> X. \<forall>y \<in> X. x \<squnion> y \<in> X)"
 
 text \<open>The following facts about complete lattices add to those in the Isabelle libraries.\<close>
 
 context complete_lattice 
 begin
 
 text \<open>The translation between sup and Sup could be improved. The sup-theorems should be direct
 consequences of Sup-ones. In addition, duality between sup and inf is currently not exploited.\<close>
 
 lemma sup_Sup: "x \<squnion> y = \<Squnion>{x,y}"
   by simp
 
 lemma inf_Inf: "x \<sqinter> y = \<Sqinter>{x,y}"
   by simp
 
 text \<open>The next two lemmas are about Sups and Infs of indexed families. These are interesting for
 iterations and fixpoints.\<close>
 
 lemma fSup_unfold: "(f::nat \<Rightarrow> 'a) 0 \<squnion> (\<Squnion>n. f (Suc n)) = (\<Squnion>n. f n)"
   apply (intro order.antisym sup_least)
     apply (rule Sup_upper, force)
    apply (rule Sup_mono, force)
   apply (safe intro!: Sup_least)
  by (case_tac n, simp_all add: Sup_upper le_supI2)
 
 lemma fInf_unfold: "(f::nat \<Rightarrow> 'a) 0 \<sqinter> (\<Sqinter>n. f (Suc n)) = (\<Sqinter>n. f n)"
   apply (intro order.antisym inf_greatest)
   apply (rule Inf_greatest, safe)
   apply (case_tac n)
    apply simp_all
   using Inf_lower inf.coboundedI2 apply force
    apply (simp add: Inf_lower)
   by (auto intro: Inf_mono)
 
 end
 
 lemma Sup_sup_closed: "Sup_closed_set (X::'a::complete_lattice set) \<Longrightarrow> sup_closed_set X"
   by (metis Sup_closed_set_def empty_subsetI insert_subsetI sup_Sup sup_closed_set_def)
 
 lemma Inf_inf_closed: "Inf_closed_set (X::'a::complete_lattice set) \<Longrightarrow> inf_closed_set X"
   by (metis Inf_closed_set_def empty_subsetI inf_Inf inf_closed_set_def insert_subset)
 
 
 subsection \<open>Sup- and Inf-Preservation\<close>
 
 text \<open>Next, important notation for morphism between posets and lattices is introduced: 
 sup-preservation, inf-preservation and related properties.\<close>
 
 abbreviation Sup_pres :: "('a::Sup \<Rightarrow> 'b::Sup) \<Rightarrow> bool" where
   "Sup_pres f \<equiv> f \<circ> Sup = Sup \<circ> (`) f"
 
 abbreviation Inf_pres :: "('a::Inf \<Rightarrow> 'b::Inf) \<Rightarrow> bool" where
   "Inf_pres f \<equiv> f \<circ> Inf = Inf \<circ> (`) f"
 
 abbreviation sup_pres :: "('a::sup \<Rightarrow> 'b::sup) \<Rightarrow> bool" where
   "sup_pres f \<equiv> (\<forall>x y. f (x \<squnion> y) = f x \<squnion> f y)"
 
 abbreviation inf_pres :: "('a::inf \<Rightarrow> 'b::inf) \<Rightarrow> bool" where
  "inf_pres f \<equiv> (\<forall>x y. f (x \<sqinter> y) = f x \<sqinter> f y)"
 
 abbreviation bot_pres :: "('a::bot \<Rightarrow> 'b::bot) \<Rightarrow> bool" where
   "bot_pres f \<equiv> f \<bottom> = \<bottom>"
 
 abbreviation top_pres :: "('a::top \<Rightarrow> 'b::top) \<Rightarrow> bool" where
   "top_pres f \<equiv> f \<top> = \<top>"
 
 abbreviation Sup_dual :: "('a::Sup \<Rightarrow> 'b::Inf) \<Rightarrow> bool" where
   "Sup_dual f \<equiv> f \<circ> Sup = Inf \<circ> (`) f"
 
 abbreviation Inf_dual :: "('a::Inf \<Rightarrow> 'b::Sup) \<Rightarrow> bool" where
   "Inf_dual f \<equiv> f \<circ> Inf = Sup \<circ> (`) f"
 
 abbreviation sup_dual :: "('a::sup \<Rightarrow> 'b::inf) \<Rightarrow> bool" where
   "sup_dual f \<equiv> (\<forall>x y. f (x \<squnion> y) = f x \<sqinter> f y)"
 
 abbreviation inf_dual :: "('a::inf \<Rightarrow> 'b::sup) \<Rightarrow> bool" where
  "inf_dual f \<equiv> (\<forall>x y. f (x \<sqinter> y) = f x \<squnion> f y)"
 
 abbreviation bot_dual :: "('a::bot \<Rightarrow> 'b::top) \<Rightarrow> bool" where 
  "bot_dual f \<equiv> f \<bottom> = \<top>"
 
 abbreviation top_dual :: "('a::top \<Rightarrow> 'b::bot) \<Rightarrow> bool" where 
   "top_dual f \<equiv> f \<top> = \<bottom>"
 
 text \<open>Inf-preservation and sup-preservation relate with duality.\<close>
 
 lemma Inf_pres_map_dual_var: 
   "Inf_pres f = Sup_pres (\<partial>\<^sub>F f)"
   for f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
 proof -
   { fix x :: "'a set"
     assume "\<partial> (f (\<Sqinter> (\<partial> ` x))) = (\<Squnion>y\<in>x. \<partial> (f (\<partial> y)))" for x
     then have "\<Sqinter> (f ` \<partial> ` A) = f (\<partial> (\<Squnion> A))" for A
       by (metis (no_types) Sup_dual_def_var image_image invol_dual_var subset_dual)
     then have "\<Sqinter> (f ` x) = f (\<Sqinter> x)"
       by (metis Sup_dual_def_var subset_dual) }
   then show ?thesis
     by (auto simp add: map_dual_def fun_eq_iff Inf_dual_var Sup_dual_def_var image_comp)
 qed
 
 lemma Inf_pres_map_dual: "Inf_pres = Sup_pres \<circ> (\<partial>\<^sub>F::('a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual) \<Rightarrow> 'a \<Rightarrow> 'b)"
 proof-
   {fix f::"'a \<Rightarrow> 'b"
   have "Inf_pres f = (Sup_pres \<circ> \<partial>\<^sub>F) f"
     by (simp add: Inf_pres_map_dual_var)}
   thus ?thesis
     by force
 qed
 
 lemma Sup_pres_map_dual_var: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   shows "Sup_pres f = Inf_pres (\<partial>\<^sub>F f)"
   by (metis Inf_pres_map_dual_var fun_dual5 map_dual_def)
 
 lemma Sup_pres_map_dual: "Sup_pres = Inf_pres \<circ> (\<partial>\<^sub>F::('a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual) \<Rightarrow> 'a \<Rightarrow> 'b)"
   by (simp add: Inf_pres_map_dual comp_assoc map_dual_invol)
 
 text \<open>The following lemmas relate isotonicity of functions between complete lattices 
 with weak (left) preservation properties of sups and infs.\<close>
 
 lemma fun_isol: "mono f \<Longrightarrow> mono ((\<circ>) f)"
   by (simp add: le_fun_def mono_def)
 
 lemma fun_isor: "mono f \<Longrightarrow> mono (\<lambda>x. x \<circ> f)"
   by (simp add: le_fun_def mono_def)
 
 lemma Sup_sup_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Sup_pres f \<Longrightarrow> sup_pres f"
   by (metis (no_types, opaque_lifting) Sup_empty Sup_insert comp_apply image_insert sup_bot.right_neutral)
 
 lemma Inf_inf_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows"Inf_pres f \<Longrightarrow> inf_pres f"
-  by (smt INF_insert Inf_empty Inf_insert comp_eq_elim inf_top.right_neutral)
+  by (smt (verit) INF_insert Inf_empty Inf_insert comp_eq_elim inf_top.right_neutral)
 
 lemma Sup_bot_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Sup_pres f \<Longrightarrow> bot_pres f"
   by (metis SUP_empty Sup_empty comp_eq_elim)
 
 lemma Inf_top_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Inf_pres f \<Longrightarrow> top_pres f"
   by (metis INF_empty Inf_empty comp_eq_elim)
 
 lemma Sup_sup_dual: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Sup_dual f \<Longrightarrow> sup_dual f"
-  by (smt comp_eq_elim image_empty image_insert inf_Inf sup_Sup)    
+  by (smt (verit) comp_eq_elim image_empty image_insert inf_Inf sup_Sup)    
 
 lemma Inf_inf_dual: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Inf_dual f \<Longrightarrow> inf_dual f"
-  by (smt comp_eq_elim image_empty image_insert inf_Inf sup_Sup)   
+  by (smt (verit) comp_eq_elim image_empty image_insert inf_Inf sup_Sup)   
 
 lemma Sup_bot_dual: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Sup_dual f \<Longrightarrow> bot_dual f"
   by (metis INF_empty Sup_empty comp_eq_elim)
 
 lemma Inf_top_dual: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Inf_dual f \<Longrightarrow> top_dual f"
   by (metis Inf_empty SUP_empty comp_eq_elim)
 
 text \<open>However, Inf-preservation does not imply top-preservation and 
 Sup-preservation does not imply bottom-preservation.\<close>
 
 lemma
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Sup_pres f \<Longrightarrow> top_pres f" (*nitpick*)
   oops
 
 lemma  
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Inf_pres f \<Longrightarrow> bot_pres f" (*nitpick*)
   oops
 
 context complete_lattice
 begin
 
 lemma iso_Inf_subdistl: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "mono f \<Longrightarrow>f \<circ> Inf \<le> Inf \<circ> (`) f"
   by (simp add: complete_lattice_class.le_Inf_iff le_funI Inf_lower monoD)
 
 lemma iso_Sup_supdistl: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice" 
   shows "mono f \<Longrightarrow> Sup \<circ> (`) f \<le> f \<circ> Sup"
   by (simp add: complete_lattice_class.Sup_le_iff le_funI Sup_upper monoD)
 
 lemma Inf_subdistl_iso: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "f \<circ> Inf \<le> Inf \<circ> (`) f \<Longrightarrow> mono f"
   unfolding mono_def le_fun_def comp_def by (metis complete_lattice_class.le_INF_iff Inf_atLeast atLeast_iff)
 
 lemma Sup_supdistl_iso: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "Sup \<circ> (`) f \<le> f \<circ> Sup \<Longrightarrow> mono f"
   unfolding mono_def le_fun_def comp_def by (metis complete_lattice_class.SUP_le_iff Sup_atMost atMost_iff)
 
 lemma supdistl_iso: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "(Sup \<circ> (`) f \<le> f \<circ> Sup) = mono f"
   using Sup_supdistl_iso iso_Sup_supdistl by force
 
 lemma subdistl_iso: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "(f \<circ> Inf \<le> Inf \<circ> (`) f) = mono f"
   using Inf_subdistl_iso iso_Inf_subdistl by force
 
 end
 
 lemma ord_iso_Inf_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "ord_iso f \<Longrightarrow> Inf \<circ> (`) f = f \<circ> Inf"
 proof-
   let ?g = "the_inv f"
   assume h: "ord_iso f"
   hence a: "mono ?g"
     by (simp add: ord_iso_the_inv)
   {fix X :: "'a::complete_lattice set"
     {fix y :: "'b::complete_lattice"
    have "(y \<le> f (\<Sqinter>X)) = (?g y \<le> \<Sqinter>X)"
      by (metis (mono_tags, lifting) UNIV_I f_the_inv_into_f h monoD ord_embed_alt ord_embed_inj ord_iso_alt)
    also have "... = (\<forall>x \<in> X. ?g y \<le> x)"
     by (simp add: le_Inf_iff)
   also have "... = (\<forall>x \<in> X. y \<le> f x)"
     by (metis (mono_tags, lifting) UNIV_I f_the_inv_into_f h monoD ord_embed_alt ord_embed_inj ord_iso_alt)
   also have "... = (y \<le> \<Sqinter> (f ` X))"
     by (simp add: le_INF_iff)
   finally have "(y \<le> f (\<Sqinter>X)) = (y \<le> \<Sqinter> (f ` X))".}
   hence "f (\<Sqinter>X) = \<Sqinter> (f ` X)"
     by (meson dual_order.antisym order_refl)}
   thus ?thesis
     unfolding fun_eq_iff by simp
 qed
 
 lemma ord_iso_Sup_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "ord_iso f \<Longrightarrow> Sup \<circ> (`) f = f \<circ> Sup"
 proof-
   let ?g = "the_inv f"
   assume h: "ord_iso f"
   hence a: "mono ?g"
     by (simp add: ord_iso_the_inv)
   {fix X :: "'a::complete_lattice set"
     {fix y :: "'b::complete_lattice"
    have "(f (\<Squnion>X) \<le> y) = (\<Squnion>X \<le> ?g y)"
      by (metis (mono_tags, lifting) UNIV_I f_the_inv_into_f h monoD ord_embed_alt ord_embed_inj ord_iso_alt)
    also have "... = (\<forall>x \<in> X. x \<le> ?g y)"
      by (simp add: Sup_le_iff)
      also have "... = (\<forall>x \<in> X. f x \<le> y)"
     by (metis (mono_tags, lifting) UNIV_I f_the_inv_into_f h monoD ord_embed_alt ord_embed_inj ord_iso_alt)
   also have "... = (\<Squnion> (f ` X) \<le> y)"
     by (simp add: SUP_le_iff)
   finally have "(f (\<Squnion>X) \<le> y) = (\<Squnion> (f ` X) \<le> y)".}
   hence "f (\<Squnion>X) = \<Squnion> (f ` X)"
     by (meson dual_order.antisym order_refl)}
   thus ?thesis
     unfolding fun_eq_iff by simp
 qed
 
 text \<open>Right preservation of sups and infs is trivial.\<close>
 
 lemma fSup_distr: "Sup_pres (\<lambda>x. x \<circ> f)"
   unfolding fun_eq_iff by (simp add: image_comp)
 
 lemma fSup_distr_var: "\<Squnion>F \<circ> g = (\<Squnion>f \<in> F. f \<circ> g)"
   unfolding fun_eq_iff by (simp add: image_comp)
 
 lemma fInf_distr: "Inf_pres (\<lambda>x. x \<circ> f)"
   unfolding fun_eq_iff comp_def
-  by (smt INF_apply Inf_fun_def Sup.SUP_cong) 
+  by (smt (verit) INF_apply Inf_fun_def Sup.SUP_cong) 
 
 lemma fInf_distr_var: "\<Sqinter>F \<circ> g = (\<Sqinter>f \<in> F. f \<circ> g)"
   unfolding fun_eq_iff comp_def
-  by (smt INF_apply INF_cong INF_image Inf_apply image_comp image_def image_image)
+  by (smt (verit) INF_apply INF_cong INF_image Inf_apply image_comp image_def image_image)
 
 
 text \<open>The next set of lemma revisits the preservation properties in the function space.\<close>
 
 lemma fSup_subdistl: 
   assumes "mono (f::'a::complete_lattice \<Rightarrow> 'b::complete_lattice)"
   shows "Sup \<circ> (`) ((\<circ>) f) \<le> (\<circ>) f \<circ> Sup"
   using assms by (simp add: fun_isol supdistl_iso) 
 
 lemma fSup_subdistl_var: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows  "mono f \<Longrightarrow> (\<Squnion>g \<in> G. f \<circ> g) \<le> f \<circ> \<Squnion>G"
   by (simp add: fun_isol mono_Sup)
 
 lemma fInf_subdistl: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows  "mono f \<Longrightarrow> (\<circ>) f \<circ> Inf \<le> Inf \<circ> (`) ((\<circ>) f)"
   by (simp add: fun_isol subdistl_iso)
 
 lemma fInf_subdistl_var: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "mono f \<Longrightarrow> f \<circ> \<Sqinter>G \<le> (\<Sqinter>g \<in> G. f \<circ> g)"
   by (simp add: fun_isol mono_Inf)
 
 lemma fSup_distl: "Sup_pres f \<Longrightarrow> Sup_pres ((\<circ>) f)"
   unfolding fun_eq_iff by (simp add: image_comp)
 
 lemma fSup_distl_var: "Sup_pres f \<Longrightarrow> f \<circ> \<Squnion>G = (\<Squnion>g \<in> G. f \<circ> g)"
   unfolding fun_eq_iff by (simp add: image_comp)
 
 lemma fInf_distl: "Inf_pres f \<Longrightarrow> Inf_pres ((\<circ>) f)"
   unfolding fun_eq_iff by (simp add: image_comp)
 
 lemma fInf_distl_var: "Inf_pres f \<Longrightarrow> f \<circ> \<Sqinter>G = (\<Sqinter>g \<in> G. f \<circ> g)"
   unfolding fun_eq_iff by (simp add: image_comp)
 
 text \<open>Downsets preserve infs whereas upsets preserve sups.\<close>
 
 lemma Inf_pres_downset: "Inf_pres (\<down>::'a::complete_lattice_with_dual \<Rightarrow> 'a set)"
   unfolding downset_prop fun_eq_iff
   by (safe, simp_all add: le_Inf_iff)
  
 lemma Sup_dual_upset: "Sup_dual (\<up>::'a::complete_lattice_with_dual \<Rightarrow> 'a set)"
   unfolding upset_prop fun_eq_iff
   by (safe, simp_all add: Sup_le_iff)
 
 text \<open>Images of Sup-morphisms are closed under Sups and images of Inf-morphisms are closed under Infs.\<close>
 
 lemma Sup_pres_Sup_closed: "Sup_pres f \<Longrightarrow> Sup_closed_set (range f)"
   by (metis (mono_tags, lifting) Sup_closed_set_def comp_eq_elim range_eqI subset_image_iff)
 
 lemma Inf_pres_Inf_closed: "Inf_pres f \<Longrightarrow> Inf_closed_set (range f)"
   by (metis (mono_tags, lifting) Inf_closed_set_def comp_eq_elim range_eqI subset_image_iff)
 
 text \<open>It is well known that functions into complete lattices form complete lattices. Here, such results are shown for
 the subclasses of isotone functions, where additional closure conditions must be respected.\<close>
 
 typedef (overloaded) 'a iso = "{f::'a::order \<Rightarrow> 'a::order. mono f}"
   by (metis Abs_ord_homset_cases ord_homset_def)
 
 setup_lifting type_definition_iso
 
 instantiation iso :: (complete_lattice) complete_lattice
 begin
 
 lift_definition Inf_iso :: "'a::complete_lattice iso set \<Rightarrow> 'a iso" is Sup
   by (metis (mono_tags, lifting) SUP_subset_mono Sup_apply mono_def subsetI)
 
 lift_definition Sup_iso :: "'a::complete_lattice iso set \<Rightarrow> 'a iso" is Inf
-  by (smt INF_lower2 Inf_apply le_INF_iff mono_def)
+  by (smt (verit) INF_lower2 Inf_apply le_INF_iff mono_def)
 
 lift_definition bot_iso :: "'a::complete_lattice iso" is "\<top>"
   by (simp add: monoI)
 
 lift_definition sup_iso :: "'a::complete_lattice iso \<Rightarrow> 'a iso \<Rightarrow> 'a iso" is inf
-  by (smt inf_apply inf_mono monoD monoI)
+  by (smt (verit) inf_apply inf_mono monoD monoI)
 
 lift_definition top_iso :: "'a::complete_lattice iso" is "\<bottom>"
   by (simp add: mono_def)
 
 lift_definition inf_iso :: "'a::complete_lattice iso \<Rightarrow> 'a iso \<Rightarrow> 'a iso" is sup
-  by (smt mono_def sup.mono sup_apply)
+  by (smt (verit) mono_def sup.mono sup_apply)
 
 lift_definition less_eq_iso :: "'a::complete_lattice iso \<Rightarrow> 'a iso \<Rightarrow> bool" is "(\<ge>)".
 
 lift_definition less_iso :: "'a::complete_lattice iso \<Rightarrow> 'a iso \<Rightarrow> bool" is "(>)".
 
 instance
   by (intro_classes; transfer, simp_all add: less_fun_def Sup_upper Sup_least Inf_lower Inf_greatest)
 
 end
 
 text \<open>Duality has been baked into this result because of its relevance for predicate transformers. A proof
 where Sups are mapped to Sups and Infs to Infs is certainly possible, but two instantiation of the same type
 and the same classes are unfortunately impossible. Interpretations could be used instead.
 
 A corresponding result for Inf-preseving functions and Sup-lattices, is proved in components on transformers,
 as more advanced properties about Inf-preserving functions are needed.\<close>
 
 
 subsection \<open>Alternative Definitions for Complete Boolean Algebras\<close>
 
 text \<open>The current definitions of complete boolean algebras deviates from that in most textbooks in that
 a distributive law with infinite sups and infinite infs is used. There are interesting applications, for instance 
 in topology, where weaker laws are needed --- for instance for frames and locales.\<close>
 
 class complete_heyting_algebra = complete_lattice +
   assumes ch_dist: "x \<sqinter> \<Squnion>Y = (\<Squnion>y \<in> Y. x \<sqinter> y)"
 
 text \<open>Complete Heyting algebras are also known as frames or locales (they differ with respect to their morphisms).\<close>
 
 class complete_co_heyting_algebra = complete_lattice +
   assumes co_ch_dist: "x \<squnion> \<Sqinter>Y = (\<Sqinter>y \<in> Y. x \<squnion> y)"
 
 class complete_boolean_algebra_alt = complete_lattice + boolean_algebra
 
 instance set :: (type) complete_boolean_algebra_alt..
 
 context complete_boolean_algebra_alt
 begin
 
 subclass complete_heyting_algebra
 proof
   fix x Y 
   {fix t
     have "(x \<sqinter> \<Squnion>Y \<le> t) = (\<Squnion>Y \<le> -x \<squnion> t)"
       by (simp add: inf.commute shunt1[symmetric])
     also have "... = (\<forall>y \<in> Y. y \<le> -x \<squnion> t)"
       using Sup_le_iff by blast
     also have "... = (\<forall>y \<in> Y. x \<sqinter> y \<le> t)"
       by (simp add: inf.commute shunt1)
     finally have "(x \<sqinter> \<Squnion>Y \<le> t) = ((\<Squnion>y\<in>Y. x \<sqinter> y) \<le> t)"
       by (simp add: local.SUP_le_iff)}
   thus "x \<sqinter> \<Squnion>Y = (\<Squnion>y\<in>Y. x \<sqinter> y)"
     using order.eq_iff by blast
 qed
 
 subclass complete_co_heyting_algebra
   apply unfold_locales
   apply (rule order.antisym)
    apply (simp add: INF_greatest Inf_lower2)
   by (meson eq_refl le_INF_iff le_Inf_iff shunt2)
 
 lemma de_morgan1: "-(\<Squnion>X) = (\<Sqinter>x \<in> X. -x)"
 proof-
   {fix y
   have "(y \<le> -(\<Squnion>X)) = (\<Squnion>X \<le> -y)"
     using compl_le_swap1 by blast
   also have "... = (\<forall>x \<in> X. x \<le> -y)"
     by (simp add: Sup_le_iff)
   also have "... = (\<forall>x \<in> X. y \<le> -x)"
     using compl_le_swap1 by blast
   also have "... = (y \<le> (\<Sqinter>x \<in> X. -x))"
     using le_INF_iff by force
   finally have "(y \<le> -(\<Squnion>X)) = (y \<le>(\<Sqinter>x \<in> X. -x))".}
   thus ?thesis
     using order.antisym by blast
 qed
 
 lemma de_morgan2: "-(\<Sqinter>X) = (\<Squnion>x \<in> X. -x)"
   by (metis de_morgan1 ba_dual.dual_iff ba_dual.image_dual pointfree_idE)
 
 end
 
 class complete_boolean_algebra_alt_with_dual = complete_lattice_with_dual + complete_boolean_algebra_alt
 
 instantiation set :: (type) complete_boolean_algebra_alt_with_dual
 begin
 
 definition dual_set :: "'a set \<Rightarrow> 'a set" where
   "dual_set = uminus"
 
 instance
   by intro_classes (simp_all add: ba_dual.inj_dual dual_set_def comp_def uminus_Sup id_def)
 
 end
 
 context complete_boolean_algebra_alt
 begin
 
 sublocale cba_dual: complete_boolean_algebra_alt_with_dual _ _ _ _ _ _ _ _ uminus _ _
   by unfold_locales (auto simp: de_morgan2 de_morgan1)
 
 end
 
 
 subsection \<open>Atomic Boolean Algebras\<close>
 
 text \<open>Next, atomic boolean algebras are defined.\<close>
 
 context bounded_lattice
 begin
 
 text \<open>Atoms are covers of bottom.\<close>
 
 definition "atom x = (x \<noteq> \<bottom> \<and> \<not>(\<exists>y. \<bottom> < y \<and> y < x))"
 
 definition "atom_map x = {y. atom y \<and> y \<le> x}"
 
 lemma atom_map_def_var: "atom_map x = \<down>x \<inter> Collect atom"
   unfolding atom_map_def downset_def downset_set_def comp_def atom_def by fastforce
 
 lemma atom_map_atoms: "\<Union>(range atom_map) = Collect atom"
   unfolding atom_map_def atom_def by auto
 
 end
 
 typedef (overloaded) 'a atoms = "range (atom_map::'a::bounded_lattice \<Rightarrow> 'a set)"
   by blast
 
 setup_lifting type_definition_atoms
 
 definition at_map :: "'a::bounded_lattice \<Rightarrow> 'a atoms" where
   "at_map = Abs_atoms \<circ> atom_map"
 
 class atomic_boolean_algebra = boolean_algebra +
   assumes atomicity: "x \<noteq> \<bottom> \<Longrightarrow> (\<exists>y. atom y \<and> y \<le> x)"
 
 class complete_atomic_boolean_algebra = complete_lattice + atomic_boolean_algebra
 
 begin
 
 subclass complete_boolean_algebra_alt..
 
 end
 
 text \<open>Here are two equivalent definitions for atoms; first in boolean algebras, and then in complete 
 boolean algebras.\<close>
 
 context boolean_algebra
 begin
 
 text \<open>The following two conditions are taken from Koppelberg's book~\<^cite>\<open>"Koppelberg89"\<close>.\<close>
 
 lemma atom_neg: "atom x \<Longrightarrow> x \<noteq> \<bottom> \<and> (\<forall>y z. x \<le> y \<or> x \<le> -y)"
   by (auto simp add: atom_def) (metis local.dual_order.not_eq_order_implies_strict local.inf.cobounded1 local.inf.cobounded2 local.inf_shunt)
 
 lemma atom_sup: "(\<forall>y. x \<le> y \<or> x \<le> -y) \<Longrightarrow> (\<forall>y z. (x \<le> y \<or> x \<le> z) = (x \<le> y \<squnion> z))"
   by (metis inf.orderE le_supI1 shunt2)
 
 lemma sup_atom: "x \<noteq> \<bottom> \<Longrightarrow> (\<forall>y z. (x \<le> y \<or> x \<le> z) = (x \<le> y \<squnion> z)) \<Longrightarrow> atom x"
   by (auto simp add: atom_def) (metis (full_types) local.inf.boundedI local.inf.cobounded2 local.inf_shunt local.inf_sup_ord(4) local.le_iff_sup local.shunt1 local.sup.absorb1 local.sup.strict_order_iff)
 
 lemma atom_sup_iff: "atom x = (x \<noteq> \<bottom> \<and> (\<forall>y z. (x \<le> y \<or> x \<le> z) = (x \<le> y \<squnion> z)))"
   by rule (auto simp add: atom_neg atom_sup sup_atom)  
 
 lemma atom_neg_iff: "atom x = (x \<noteq> \<bottom> \<and> (\<forall>y z. x \<le> y \<or> x \<le> -y))"
   by rule (auto simp add: atom_neg atom_sup sup_atom)
 
 lemma atom_map_bot_pres: "atom_map \<bottom> = {}"
   using atom_def atom_map_def le_bot by auto
 
 lemma atom_map_top_pres: "atom_map \<top> = Collect atom"
   using atom_map_def by auto
 
 end
 
 context complete_boolean_algebra_alt
 begin
 
 lemma atom_Sup: "\<And>Y. x \<noteq> \<bottom> \<Longrightarrow> (\<forall>y. x \<le> y \<or> x \<le> -y) \<Longrightarrow> ((\<exists>y \<in> Y. x \<le> y) = (x \<le> \<Squnion>Y))"
   by (metis Sup_least Sup_upper2 compl_le_swap1 le_iff_inf inf_shunt)
 
 lemma Sup_atom: "x \<noteq> \<bottom> \<Longrightarrow> (\<forall>Y. (\<exists>y \<in> Y. x \<le> y) = (x \<le> \<Squnion>Y)) \<Longrightarrow> atom x"
 proof-
   assume h1: "x \<noteq> \<bottom>"
   and h2: "\<forall>Y. (\<exists>y \<in> Y. x \<le> y) = (x \<le> \<Squnion>Y)"
   hence "\<forall>y z. (x \<le> y \<or> x \<le> z) = (x \<le> y \<squnion> z)"
-
-    by (smt insert_iff sup_Sup sup_bot.right_neutral)
+    by (smt (verit) insert_iff sup_Sup sup_bot.right_neutral)
   thus "atom x"
     by (simp add: h1 sup_atom)
 qed
 
 lemma atom_Sup_iff: "atom x = (x \<noteq> \<bottom> \<and> (\<forall>Y. (\<exists>y \<in> Y. x \<le> y) = (x \<le> \<Squnion>Y)))"
   by standard (auto simp: atom_neg atom_Sup Sup_atom)
 
 end
 
 end
diff --git a/thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy b/thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy
--- a/thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy
+++ b/thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy
@@ -1,575 +1,575 @@
 (* 
   Title: Locale-Based Duality
   Author: Georg Struth 
   Maintainer:Georg Struth <g.struth@sheffield.ac.uk> 
 *)
 
 section \<open>Locale-Based Duality\<close>
 
 theory Order_Lattice_Props_Loc
   imports Main 
 begin
 
 unbundle lattice_syntax
 
 text \<open>This section explores order and lattice duality based on locales. Used within the context of a class or locale, 
 this is very effective, though more opaque than the previous approach. Outside of such a context, however, it apparently
 cannot be used for dualising theorems. Examples are properties of  functions between orderings or lattices.\<close>
 
 definition Fix :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set" where 
   "Fix f = {x. f x = x}"
 
 context ord
 begin
 
 definition min_set :: "'a set \<Rightarrow> 'a set" where 
  "min_set X = {y \<in> X. \<forall>x \<in> X. x \<le> y \<longrightarrow> x = y}"
 
 definition max_set :: "'a set \<Rightarrow> 'a set" where 
  "max_set X = {x \<in> X. \<forall>y \<in> X. x \<le> y \<longrightarrow> x = y}"
 
 definition directed :: "'a set \<Rightarrow> bool" where
  "directed X = (\<forall>Y. finite Y \<and> Y \<subseteq> X \<longrightarrow> (\<exists>x \<in> X. \<forall>y \<in> Y. y \<le> x))"
 
 definition filtered :: "'a set \<Rightarrow> bool" where
  "filtered X = (\<forall>Y. finite Y \<and> Y \<subseteq> X \<longrightarrow> (\<exists>x \<in> X. \<forall>y \<in> Y. x \<le> y))"
 
 definition downset_set :: "'a set \<Rightarrow> 'a set" ("\<Down>") where
   "\<Down>X = {y. \<exists>x \<in> X. y \<le> x}"
 
 definition upset_set :: "'a set \<Rightarrow> 'a set" ("\<Up>") where
  "\<Up>X = {y. \<exists>x \<in> X. x \<le> y}"
 
 definition downset :: "'a \<Rightarrow> 'a set" ("\<down>") where 
   "\<down> = \<Down> \<circ> (\<lambda>x. {x})"
 
 definition upset :: "'a \<Rightarrow> 'a set" ("\<up>") where 
   "\<up> = \<Up> \<circ> (\<lambda>x. {x})"
 
 definition downsets :: "'a set set" where  
   "downsets = Fix \<Down>"
  
 definition upsets :: "'a set set" where
   "upsets = Fix \<Up>"
 
 abbreviation "downset_setp X \<equiv> X \<in> downsets"
 
 abbreviation "upset_setp X \<equiv> X \<in> upsets"
 
 definition ideals :: "'a set set" where
   "ideals = {X. X \<noteq> {} \<and> downset_setp X \<and> directed X}"
 
 definition filters :: "'a  set set" where
   "filters = {X. X \<noteq> {} \<and> upset_setp X \<and> filtered X}"
 
 abbreviation "idealp X \<equiv> X \<in> ideals"
 
 abbreviation "filterp X \<equiv> X \<in> filters"
 
 end
 
 abbreviation Sup_pres :: "('a::Sup \<Rightarrow> 'b::Sup) \<Rightarrow> bool" where
   "Sup_pres f \<equiv> f \<circ> Sup = Sup \<circ> (`) f"
 
 abbreviation Inf_pres :: "('a::Inf \<Rightarrow> 'b::Inf) \<Rightarrow> bool" where
   "Inf_pres f \<equiv> f \<circ> Inf = Inf \<circ> (`) f"
 
 abbreviation sup_pres :: "('a::sup \<Rightarrow> 'b::sup) \<Rightarrow> bool" where
   "sup_pres f \<equiv> (\<forall>x y. f (x \<squnion> y) = f x \<squnion> f y)"
 
 abbreviation inf_pres :: "('a::inf \<Rightarrow> 'b::inf) \<Rightarrow> bool" where
  "inf_pres f \<equiv> (\<forall>x y. f (x \<sqinter> y) = f x \<sqinter> f y)"
 
 abbreviation bot_pres :: "('a::bot \<Rightarrow> 'b::bot) \<Rightarrow> bool" where
   "bot_pres f \<equiv> f \<bottom> = \<bottom>"
 
 abbreviation top_pres :: "('a::top \<Rightarrow> 'b::top) \<Rightarrow> bool" where
   "top_pres f \<equiv> f \<top> = \<top>"
 
 abbreviation Sup_dual :: "('a::Sup \<Rightarrow> 'b::Inf) \<Rightarrow> bool" where
   "Sup_dual f \<equiv> f \<circ> Sup = Inf \<circ> (`) f"
 
 abbreviation Inf_dual :: "('a::Inf \<Rightarrow> 'b::Sup) \<Rightarrow> bool" where
   "Inf_dual f \<equiv> f \<circ> Inf = Sup \<circ> (`) f"
 
 abbreviation sup_dual :: "('a::sup \<Rightarrow> 'b::inf) \<Rightarrow> bool" where
   "sup_dual f \<equiv> (\<forall>x y. f (x \<squnion> y) = f x \<sqinter> f y)"
 
 abbreviation inf_dual :: "('a::inf \<Rightarrow> 'b::sup) \<Rightarrow> bool" where
  "inf_dual f \<equiv> (\<forall>x y. f (x \<sqinter> y) = f x \<squnion> f y)"
 
 abbreviation bot_dual :: "('a::bot \<Rightarrow> 'b::top) \<Rightarrow> bool" where 
  "bot_dual f \<equiv> f \<bottom> = \<top>"
 
 abbreviation top_dual :: "('a::top \<Rightarrow> 'b::bot) \<Rightarrow> bool" where 
   "top_dual f \<equiv> f \<top> = \<bottom>"
 
 
 subsection \<open>Duality via Locales\<close>
 
 sublocale ord \<subseteq> dual_ord: ord "(\<ge>)" "(>)"
   rewrites dual_max_set: "max_set = dual_ord.min_set"
   and dual_filtered: "filtered = dual_ord.directed"
   and dual_upset_set: "upset_set = dual_ord.downset_set"
   and dual_upset: "upset = dual_ord.downset"
   and dual_upsets: "upsets = dual_ord.downsets"
   and dual_filters: "filters = dual_ord.ideals"
        apply unfold_locales
   unfolding max_set_def ord.min_set_def fun_eq_iff apply blast
   unfolding filtered_def ord.directed_def apply simp 
   unfolding upset_set_def ord.downset_set_def apply simp
   apply (simp add: ord.downset_def ord.downset_set_def ord.upset_def ord.upset_set_def)
   unfolding upsets_def ord.downsets_def apply (metis ord.downset_set_def upset_set_def)
   unfolding filters_def ord.ideals_def Fix_def ord.downsets_def upsets_def ord.downset_set_def upset_set_def ord.directed_def filtered_def
   by simp
 
 sublocale preorder \<subseteq> dual_preorder: preorder "(\<ge>)" "(>)"
   apply unfold_locales
   apply (simp add: less_le_not_le)
   apply simp
   using order_trans by blast
 
 sublocale order \<subseteq> dual_order: order "(\<ge>)" "(>)"
   by (unfold_locales, simp)
 
 sublocale lattice \<subseteq> dual_lattice: lattice sup "(\<ge>)" "(>)" inf
   by (unfold_locales, simp_all)
 
 sublocale bounded_lattice \<subseteq> dual_bounded_lattice: bounded_lattice sup "(\<ge>)" "(>)" inf \<top> \<bottom>
   by (unfold_locales, simp_all)
 
 sublocale boolean_algebra \<subseteq> dual_boolean_algebra: boolean_algebra "\<lambda>x y. x \<squnion> -y" uminus sup "(\<ge>)" "(>)" inf \<top> \<bottom>
   by (unfold_locales, simp_all add: inf_sup_distrib1)
 
 sublocale complete_lattice \<subseteq> dual_complete_lattice: complete_lattice Sup Inf sup "(\<ge>)" "(>)" inf \<top> \<bottom>
   rewrites dual_gfp: "gfp = dual_complete_lattice.lfp"  
 proof-
   show "class.complete_lattice Sup Inf sup (\<ge>) (>) inf \<top> \<bottom>"
     by (unfold_locales, simp_all add: Sup_upper Sup_least Inf_lower Inf_greatest)
   then interpret dual_complete_lattice: complete_lattice Sup Inf sup "(\<ge>)" "(>)" inf \<top> \<bottom>.
   show "gfp = dual_complete_lattice.lfp"  
     unfolding gfp_def dual_complete_lattice.lfp_def fun_eq_iff by simp
 qed
 
 context ord
 begin
 
 lemma dual_min_set: "min_set = dual_ord.max_set"
   by (simp add: dual_ord.dual_max_set)
 
 lemma dual_directed: "directed = dual_ord.filtered"
   by (simp add:dual_ord.dual_filtered)
 
 lemma dual_downset: "downset = dual_ord.upset"
   by (simp add: dual_ord.dual_upset)
 
 lemma dual_downset_set: "downset_set = dual_ord.upset_set"
   by (simp add: dual_ord.dual_upset_set)
 
 lemma dual_downsets: "downsets = dual_ord.upsets"
   by (simp add: dual_ord.dual_upsets)
 
 lemma dual_ideals: "ideals = dual_ord.filters"
   by (simp add: dual_ord.dual_filters)
 
 end
 
 context complete_lattice
 begin
 
 lemma dual_lfp: "lfp = dual_complete_lattice.gfp"
   by (simp add: dual_complete_lattice.dual_gfp)
 
 end
 
 subsection \<open>Properties of Orderings, Again\<close>
 
 context ord
 begin
 
 lemma directed_nonempty: "directed X \<Longrightarrow> X \<noteq> {}"
   unfolding directed_def by fastforce
 
 lemma directed_ub: "directed X \<Longrightarrow> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. x \<le> z \<and> y \<le> z)"
   by (meson empty_subsetI directed_def finite.emptyI finite_insert insert_subset order_refl)
 
 lemma downset_set_prop: "\<Down> = Union \<circ> (`) \<down>"
   unfolding downset_set_def downset_def fun_eq_iff by fastforce
 
 lemma downset_set_prop_var: "\<Down>X = (\<Union>x \<in> X. \<down>x)"
   by (simp add: downset_set_prop)
 
 lemma downset_prop: "\<down>x = {y. y \<le> x}"
   unfolding downset_def downset_set_def fun_eq_iff comp_def by fastforce
 
 end
 
 context preorder
 begin
 
 lemma directed_prop: "X \<noteq> {} \<Longrightarrow> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. x \<le> z \<and> y \<le> z) \<Longrightarrow> directed X"
 proof-
   assume h1: "X \<noteq> {}"
   and h2: "\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. x \<le> z \<and> y \<le> z"
   {fix Y
   have "finite Y \<Longrightarrow> Y \<subseteq> X \<Longrightarrow> (\<exists>x \<in> X. \<forall>y \<in> Y. y \<le> x)"
   proof (induct rule: finite_induct)
     case empty
     then show ?case
       using h1 by blast 
   next
     case (insert x F)
     then show ?case
       by (metis h2 insert_iff insert_subset order_trans) 
   qed}
   thus ?thesis
     by (simp add: directed_def)
 qed
 
 lemma directed_alt: "directed X = (X \<noteq> {} \<and> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. x \<le> z \<and> y \<le> z))"
   by (metis directed_prop directed_nonempty directed_ub)
 
 lemma downset_set_ext: "id \<le> \<Down>"
   unfolding le_fun_def id_def downset_set_def by auto 
 
 lemma downset_set_iso: "mono \<Down>"
   unfolding mono_def downset_set_def by blast
 
 lemma downset_set_idem [simp]: "\<Down> \<circ> \<Down> = \<Down>"
   unfolding fun_eq_iff downset_set_def comp_def using order_trans by auto
 
 lemma downset_faithful: "\<down>x \<subseteq> \<down>y \<Longrightarrow> x \<le> y"
   by (simp add: downset_prop subset_eq)
 
 lemma downset_iso_iff: "(\<down>x \<subseteq> \<down>y) = (x \<le> y)"
   using atMost_iff downset_prop order_trans by blast
 
 lemma downset_directed_downset_var [simp]: "directed (\<Down>X) = directed X"
 proof
   assume h1: "directed X"
   {fix Y
   assume h2: "finite Y" and h3: "Y \<subseteq> \<Down>X"
   hence "\<forall>y. \<exists>x. y \<in> Y \<longrightarrow> x \<in> X \<and>  y \<le> x"
     by (force simp: downset_set_def)
   hence "\<exists>f. \<forall>y. y \<in> Y \<longrightarrow>  f y \<in> X \<and> y \<le> f y"
     by (rule choice)
   hence "\<exists>f. finite (f ` Y) \<and> f ` Y \<subseteq> X \<and> (\<forall>y \<in> Y. y \<le> f y)"
     by (metis finite_imageI h2 image_subsetI)
   hence "\<exists>Z. finite Z \<and> Z \<subseteq> X \<and> (\<forall>y \<in> Y. \<exists> z \<in> Z. y \<le> z)"
     by fastforce
   hence "\<exists>Z. finite Z \<and> Z \<subseteq> X \<and> (\<forall>y \<in> Y. \<exists> z \<in> Z. y \<le> z) \<and> (\<exists>x \<in> X. \<forall> z \<in> Z. z \<le> x)"
     by (metis directed_def h1)
   hence "\<exists>x \<in> X. \<forall>y \<in> Y. y \<le> x"
     by (meson order_trans)}
   thus "directed (\<Down>X)"
     unfolding directed_def downset_set_def by fastforce
 next 
   assume "directed (\<Down>X)"
   thus "directed X"
     unfolding directed_def downset_set_def 
     apply clarsimp
-    by (smt Ball_Collect order_refl order_trans subsetCE)
+    by (smt (verit) Ball_Collect order_refl order_trans subsetCE)
 qed
 
 lemma downset_directed_downset [simp]: "directed \<circ> \<Down> = directed"
   unfolding fun_eq_iff comp_def by simp
 
 lemma directed_downset_ideals: "directed (\<Down>X) = (\<Down>X \<in> ideals)"
   by (metis (mono_tags, lifting) Fix_def comp_apply directed_alt downset_set_idem downsets_def ideals_def mem_Collect_eq)
 
 end
 
 lemma downset_iso: "mono (\<down>::'a::order \<Rightarrow> 'a set)"
   by (simp add: downset_iso_iff mono_def)
 
 context order
 begin
 
 lemma downset_inj: "inj \<down>"
   by (metis injI downset_iso_iff order.eq_iff)
 
 end
 
 context lattice
 begin
 
 lemma lat_ideals: "X \<in> ideals = (X \<noteq> {} \<and> X \<in> downsets \<and> (\<forall>x \<in> X. \<forall> y \<in> X. x \<squnion> y \<in> X))"
   unfolding ideals_def directed_alt downsets_def Fix_def downset_set_def 
-  by (clarsimp, smt sup.cobounded1 sup.orderE sup.orderI sup_absorb2 sup_left_commute mem_Collect_eq)
+  using local.sup.bounded_iff by blast
 
 end
 
 context bounded_lattice
 begin
 
 lemma bot_ideal: "X \<in> ideals \<Longrightarrow> \<bottom> \<in> X"
   unfolding ideals_def downsets_def Fix_def downset_set_def by fastforce
 
 end
 
 context complete_lattice
 begin
 
 lemma Sup_downset_id [simp]: "Sup \<circ> \<down> = id"
   using Sup_atMost atMost_def downset_prop by fastforce
 
 lemma downset_Sup_id: "id \<le> \<down> \<circ> Sup"
   by (simp add: Sup_upper downset_prop le_funI subsetI)
 
 lemma Inf_Sup_var: "\<Squnion>(\<Inter>x \<in> X. \<down>x) = \<Sqinter>X"
   unfolding downset_prop by (simp add: Collect_ball_eq Inf_eq_Sup)
 
 lemma Inf_pres_downset_var: "(\<Inter>x \<in> X. \<down>x) = \<down>(\<Sqinter>X)"
   unfolding downset_prop by (safe, simp_all add: le_Inf_iff)
 
 end
 
 lemma lfp_in_Fix: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows "mono f \<Longrightarrow> lfp f \<in> Fix f"
   using Fix_def lfp_unfold by fastforce
 
 lemma gfp_in_Fix: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows "mono f \<Longrightarrow> gfp f \<in> Fix f"
   using Fix_def gfp_unfold by fastforce
 
 lemma nonempty_Fix: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   shows "mono f \<Longrightarrow> Fix f \<noteq> {}"
   using lfp_in_Fix by fastforce
 
 
 subsection \<open>Dual Properties of Orderings from Locales\<close>
 
 text \<open>These properties can be proved very smoothly overall. But only within the context of a class
 or locale!\<close>
 
 context ord
 begin
 
 lemma filtered_nonempty: "filtered X \<Longrightarrow> X \<noteq> {}"
   by (simp add: dual_filtered dual_ord.directed_nonempty)
 
 lemma filtered_lb: "filtered X \<Longrightarrow> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. z \<le> x \<and> z \<le> y)"
   by (simp add: dual_filtered dual_ord.directed_ub)
 
 lemma upset_set_prop: "\<Up> = Union \<circ> (`) \<up>"
   by (simp add: dual_ord.downset_set_prop dual_upset dual_upset_set)
 
 lemma upset_set_prop_var: "\<Up>X = (\<Union>x \<in> X. \<up>x)"
   by (simp add: dual_ord.downset_set_prop_var dual_upset dual_upset_set)
 
 lemma upset_prop: "\<up>x = {y. x \<le> y}"
   by (simp add: dual_ord.downset_prop dual_upset)
 
 end
 
 context preorder
 begin
 
 lemma filtered_prop: "X \<noteq> {} \<Longrightarrow> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. z \<le> x \<and> z \<le> y) \<Longrightarrow> filtered X"
   by (simp add: dual_filtered dual_preorder.directed_prop)
 
 lemma filtered_alt: "filtered X = (X \<noteq> {} \<and> (\<forall>x \<in> X. \<forall>y \<in> X. \<exists>z \<in> X. z \<le> x \<and> z \<le> y))"
   by (simp add: dual_filtered dual_preorder.directed_alt)
 
 lemma upset_set_ext: "id \<le> \<Up>"
   by (simp add: dual_preorder.downset_set_ext dual_upset_set)
 
 lemma upset_set_anti: "mono \<Up>"
   by (simp add: dual_preorder.downset_set_iso dual_upset_set) 
 
 lemma up_set_idem [simp]: "\<Up> \<circ> \<Up> = \<Up>"
   by (simp add: dual_upset_set)
 
 lemma upset_faithful: "\<up>x \<subseteq> \<up>y \<Longrightarrow> y \<le> x"
   by (metis dual_preorder.downset_faithful dual_upset)
 
 lemma upset_anti_iff: "(\<up>y \<subseteq> \<up>x) = (x \<le> y)"
   by (simp add: dual_preorder.downset_iso_iff dual_upset)
 
 lemma upset_filtered_upset [simp]: "filtered \<circ> \<Up> = filtered"
   by (simp add: dual_filtered dual_upset_set)
 
 lemma filtered_upset_filters: "filtered (\<Up>X) = (\<Up>X \<in> filters)"
   using dual_filtered dual_preorder.directed_downset_ideals dual_upset_set ord.dual_filters by fastforce
 
 end
 
 context order
 begin
 
 lemma upset_inj: "inj \<up>"
   by (simp add: dual_order.downset_inj dual_upset)
 
 end
 
 context lattice
 begin
 
 lemma lat_filters: "X \<in> filters = (X \<noteq> {} \<and> X \<in> upsets \<and> (\<forall>x \<in> X. \<forall> y \<in> X. x \<sqinter> y \<in> X))"
   by (simp add: dual_filters dual_lattice.lat_ideals dual_ord.downsets_def dual_upset_set upsets_def)
 
 end
 
 context bounded_lattice
 begin
 
 lemma top_filter: "X \<in> filters \<Longrightarrow> \<top> \<in> X"
   by (simp add: dual_bounded_lattice.bot_ideal dual_filters)
 
 end
 
 context complete_lattice
 begin
 
 lemma Inf_upset_id [simp]: "Inf \<circ> \<up> = id"
   by (simp add:  dual_upset)
 
 lemma upset_Inf_id: "id \<le> \<up> \<circ> Inf"
   by (simp add: dual_complete_lattice.downset_Sup_id dual_upset)
 
 lemma Sup_Inf_var: " \<Sqinter>(\<Inter>x \<in> X. \<up>x) = \<Squnion>X"
   by (simp add: dual_complete_lattice.Inf_Sup_var dual_upset)
 
 lemma Sup_dual_upset_var: "(\<Inter>x \<in> X. \<up>x) = \<up>(\<Squnion>X)"
   by (simp add: dual_complete_lattice.Inf_pres_downset_var dual_upset)
 
 end
 
 subsection \<open>Examples that Do Not Dualise\<close>
 
 lemma upset_anti: "antimono (\<up>::'a::order \<Rightarrow> 'a set)"
   by (simp add: antimono_def upset_anti_iff)
 
 context complete_lattice 
 begin
 
 lemma fSup_unfold: "(f::nat \<Rightarrow> 'a) 0 \<squnion> (\<Squnion>n. f (Suc n)) = (\<Squnion>n. f n)"
   apply (intro order.antisym sup_least)
     apply (rule Sup_upper, force)
    apply (rule Sup_mono, force)
   apply (safe intro!: Sup_least)
  by (case_tac n, simp_all add: Sup_upper le_supI2)
 
 
 lemma fInf_unfold: "(f::nat \<Rightarrow> 'a) 0 \<sqinter> (\<Sqinter>n. f (Suc n)) = (\<Sqinter>n. f n)"
   apply (intro order.antisym inf_greatest)
   apply (rule Inf_greatest, safe)
   apply (case_tac n)
    apply simp_all
   using Inf_lower inf.coboundedI2 apply force
    apply (simp add: Inf_lower)
   by (auto intro: Inf_mono)
 
 end
 
 lemma fun_isol: "mono f \<Longrightarrow> mono ((\<circ>) f)"
   by (simp add: le_fun_def mono_def)
 
 lemma fun_isor: "mono f \<Longrightarrow> mono (\<lambda>x. x \<circ> f)"
   by (simp add: le_fun_def mono_def)
 
 lemma Sup_sup_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Sup_pres f \<Longrightarrow> sup_pres f"
   by (metis (no_types, opaque_lifting) Sup_empty Sup_insert comp_apply image_insert sup_bot.right_neutral)
 
 lemma Inf_inf_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows"Inf_pres f \<Longrightarrow> inf_pres f"
-  by (smt INF_insert comp_eq_elim dual_complete_lattice.Sup_empty dual_complete_lattice.Sup_insert inf_top.right_neutral)
+  by (smt (verit) INF_insert comp_eq_elim dual_complete_lattice.Sup_empty dual_complete_lattice.Sup_insert inf_top.right_neutral)
 
 lemma Sup_bot_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Sup_pres f \<Longrightarrow> bot_pres f"
   by (metis SUP_empty Sup_empty comp_eq_elim)
 
 lemma Inf_top_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "Inf_pres f \<Longrightarrow> top_pres f"
   by (metis INF_empty comp_eq_elim dual_complete_lattice.Sup_empty)
 
 context complete_lattice
 begin
 
 lemma iso_Inf_subdistl: 
   assumes "mono (f::'a \<Rightarrow> 'b::complete_lattice)"
   shows "f \<circ> Inf \<le> Inf \<circ> (`) f"
   by (simp add: assms complete_lattice_class.le_Inf_iff le_funI Inf_lower monoD)
 
 lemma iso_Sup_supdistl: 
   assumes "mono (f::'a \<Rightarrow> 'b::complete_lattice)"
   shows "Sup \<circ> (`) f \<le> f \<circ> Sup"
   by (simp add: assms complete_lattice_class.SUP_le_iff le_funI dual_complete_lattice.Inf_lower monoD)
 
 lemma Inf_subdistl_iso: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "f \<circ> Inf \<le> Inf \<circ> (`) f \<Longrightarrow> mono f"
   unfolding mono_def le_fun_def comp_def by (metis complete_lattice_class.le_INF_iff Inf_atLeast atLeast_iff)
 
 lemma Sup_supdistl_iso: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "Sup \<circ> (`) f \<le> f \<circ> Sup \<Longrightarrow> mono f"
   unfolding mono_def le_fun_def comp_def by (metis complete_lattice_class.SUP_le_iff Sup_atMost atMost_iff)
 
 lemma supdistl_iso: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "(Sup \<circ> (`) f \<le> f \<circ> Sup) = mono f"
   using Sup_supdistl_iso iso_Sup_supdistl by force
 
 lemma subdistl_iso: 
   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   shows "(f \<circ> Inf \<le> Inf \<circ> (`) f) = mono f"
   using Inf_subdistl_iso iso_Inf_subdistl by force
 
 end
 
 lemma fSup_distr: "Sup_pres (\<lambda>x. x \<circ> f)"
   unfolding fun_eq_iff comp_def
-  by (smt Inf.INF_cong SUP_apply Sup_apply)
+  by (smt (verit) Inf.INF_cong SUP_apply Sup_apply)
 
 lemma fSup_distr_var: "\<Squnion>F \<circ> g = (\<Squnion>f \<in> F. f \<circ> g)"
   unfolding fun_eq_iff comp_def
-  by (smt Inf.INF_cong SUP_apply Sup_apply)
+  by (smt (verit) Inf.INF_cong SUP_apply Sup_apply)
 
 lemma fInf_distr: "Inf_pres (\<lambda>x. x \<circ> f)"
   unfolding fun_eq_iff comp_def
-  by (smt INF_apply Inf.INF_cong Inf_apply)
+  by (smt (verit) INF_apply Inf.INF_cong Inf_apply)
 
 lemma fInf_distr_var: "\<Sqinter>F \<circ> g = (\<Sqinter>f \<in> F. f \<circ> g)"
   unfolding fun_eq_iff comp_def
-  by (smt INF_apply Inf.INF_cong Inf_apply)
+  by (smt (verit) INF_apply Inf.INF_cong Inf_apply)
 
 lemma fSup_subdistl: 
   assumes "mono (f::'a::complete_lattice \<Rightarrow> 'b::complete_lattice)"
   shows "Sup \<circ> (`) ((\<circ>) f) \<le> (\<circ>) f \<circ> Sup"
   using assms by (simp add: SUP_least Sup_upper le_fun_def monoD image_comp)
 
 lemma fSup_subdistl_var: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows  "mono f \<Longrightarrow> (\<Squnion>g \<in> G. f \<circ> g) \<le> f \<circ> \<Squnion>G"
   by (simp add: SUP_least Sup_upper le_fun_def monoD image_comp)
 
 lemma fInf_subdistl: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows  "mono f \<Longrightarrow> (\<circ>) f \<circ> Inf \<le> Inf \<circ> (`) ((\<circ>) f)"
   by (simp add: INF_greatest Inf_lower le_fun_def monoD image_comp)
 
 lemma fInf_subdistl_var: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "mono f \<Longrightarrow> f \<circ> \<Sqinter>G \<le> (\<Sqinter>g \<in> G. f \<circ> g)"
   by (simp add: INF_greatest Inf_lower le_fun_def monoD image_comp)
 
 lemma Inf_pres_downset: "Inf_pres (\<down>::'a::complete_lattice \<Rightarrow> 'a set)"
   unfolding downset_prop fun_eq_iff comp_def
   by (safe, simp_all add: le_Inf_iff)
  
 lemma Sup_dual_upset: "Sup_dual (\<up>::'a::complete_lattice \<Rightarrow> 'a set)"
   unfolding upset_prop fun_eq_iff comp_def
   by (safe, simp_all add: Sup_le_iff)
 
 text \<open>This approach could probably be combined with the explicit functor-based one. This may be good for proofs, but seems conceptually rather ugly.\<close>
 
 end
\ No newline at end of file
diff --git a/thys/Order_Lattice_Props/Representations.thy b/thys/Order_Lattice_Props/Representations.thy
--- a/thys/Order_Lattice_Props/Representations.thy
+++ b/thys/Order_Lattice_Props/Representations.thy
@@ -1,620 +1,621 @@
 (* 
   Title: Representation Theorems for Orderings and Lattices
   Author: Georg Struth 
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
 *)
 
 section \<open>Representation Theorems for Orderings and Lattices\<close>
 
 theory Representations
   imports Order_Lattice_Props
 
 begin
 
 subsection \<open>Representation of Posets\<close>
 
 text \<open>The isomorphism between partial orders and downsets with set inclusion is well known. It forms the basis of Priestley and Stone duality.
 I show it not only for objects, but also order morphisms, hence establish equivalences and isomorphisms between categories.\<close>
 
 typedef (overloaded) 'a downset = "range (\<down>::'a::ord \<Rightarrow> 'a set)"
   by fastforce
 
 setup_lifting type_definition_downset
   
 text \<open>The map ds yields the isomorphism between the set and the powerset level if its range is restricted to downsets.\<close>
   
 definition ds :: "'a::ord \<Rightarrow> 'a downset" where 
   "ds = Abs_downset \<circ> \<down>"
 
 text \<open>In a complete lattice, its inverse is Sup.\<close>
 
 definition SSup :: "'a::complete_lattice downset \<Rightarrow> 'a" where
   "SSup = Sup \<circ> Rep_downset"
 
 lemma ds_SSup_inv: "ds \<circ> SSup = (id::'a::complete_lattice downset \<Rightarrow> 'a downset)"
   unfolding ds_def SSup_def
-  by (smt Rep_downset Rep_downset_inverse cSup_atMost eq_id_iff imageE o_def ord_class.atMost_def ord_class.downset_prop)
+  by (smt (verit) Rep_downset Rep_downset_inverse cSup_atMost eq_id_iff imageE o_def ord_class.atMost_def ord_class.downset_prop)
 
 lemma SSup_ds_inv: "SSup \<circ> ds = (id::'a::complete_lattice \<Rightarrow> 'a)"
   unfolding ds_def SSup_def fun_eq_iff id_def comp_def by (simp add: Abs_downset_inverse pointfree_idE) 
 
 instantiation downset :: (ord) order
 begin 
   
 lift_definition less_eq_downset :: "'a downset \<Rightarrow> 'a downset \<Rightarrow> bool" is "(\<lambda>X Y. Rep_downset X \<subseteq> Rep_downset Y)" .
 
 lift_definition less_downset :: "'a downset \<Rightarrow> 'a downset \<Rightarrow> bool" is "(\<lambda>X Y. Rep_downset X \<subset> Rep_downset Y)" .
 
 instance
   by (intro_classes, transfer, auto simp: Rep_downset_inject less_eq_downset_def)
 
 end
 
 lemma ds_iso: "mono ds"
   unfolding mono_def ds_def fun_eq_iff comp_def
   by (metis Abs_downset_inverse downset_iso_iff less_eq_downset.rep_eq rangeI)
  
 lemma ds_faithful: "ds x \<le> ds y \<Longrightarrow> x \<le> (y::'a::order)"
   by (simp add: Abs_downset_inverse downset_faithful ds_def less_eq_downset.rep_eq)
 
 lemma ds_inj: "inj (ds::'a::order \<Rightarrow> 'a downset)"
   by (simp add: ds_faithful dual_order.antisym injI)
 
 lemma ds_surj: "surj ds"
   by (metis (no_types, opaque_lifting) Rep_downset Rep_downset_inverse ds_def image_iff o_apply surj_def)
 
 lemma ds_bij: "bij (ds::'a::order \<Rightarrow> 'a downset)"
   by (simp add: bijI ds_inj ds_surj)
 
 lemma ds_ord_iso: "ord_iso ds"
-  unfolding ord_iso_def comp_def inf_bool_def by (smt UNIV_I ds_bij ds_faithful ds_inj ds_iso ds_surj f_the_inv_into_f inf1I mono_def)
+  unfolding ord_iso_def comp_def inf_bool_def by (smt (verit) UNIV_I ds_bij ds_faithful ds_inj ds_iso ds_surj f_the_inv_into_f inf1I mono_def)
 
 text \<open>The morphishms between orderings and downsets are isotone functions. One can define functors mapping back and forth between these.\<close>
 
 definition map_ds :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a downset \<Rightarrow> 'b downset)" where
   "map_ds f = ds \<circ> f \<circ> SSup"
 
 text \<open>This definition is actually contrived. We have shown that a function f between posets P and Q is isotone if and only if the 
 inverse image of f maps downclosed sets in Q to downclosed sets in P. There is the following duality: ds is a natural transformation 
 between the identity functor and the preimage functor as a contravariant functor from P to Q. Hence orderings with isotone maps and 
 downsets with downset-preserving maps are dual, which is a first step towards Stone duality. I don't see a way of proving this with Isabelle, 
 as the types of the preimage of f are the wrong way and I don't see how I could capture opposition with what I have.\<close> 
 
 (*lemma "mono (f::'a::complete_lattice \<Rightarrow> 'b::complete_lattimap_ds f = Abs_downset \<circ> (-`) f \<circ> Rep_downset" doesn't work! *)
 
 lemma map_ds_prop: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice" 
   shows "map_ds f \<circ> ds = ds \<circ> f"
   unfolding map_ds_def by (simp add: SSup_ds_inv comp_assoc)
 
 lemma map_ds_prop2: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "map_ds f \<circ> ds = ds \<circ> id f"
   unfolding map_ds_def by (simp add: SSup_ds_inv comp_assoc)
 
 text \<open>This is part of showing that map-ds is naturally isomorphic to the identity functor, ds being the natural isomorphism.\<close>
 
 definition map_SSup :: "('a downset \<Rightarrow> 'b downset) \<Rightarrow> ('a::complete_lattice \<Rightarrow> 'b::complete_lattice)" where
   "map_SSup F = SSup \<circ> F \<circ> ds"
 
 lemma map_ds_iso_pres: 
   fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "mono f \<Longrightarrow> mono (map_ds f)"
   unfolding fun_eq_iff mono_def map_ds_def ds_def SSup_def comp_def
   by (metis Abs_downset_inverse Sup_subset_mono downset_iso_iff less_eq_downset.rep_eq rangeI)
 
 lemma map_SSup_iso_pres: 
   fixes F :: "'a::complete_lattice downset \<Rightarrow> 'b::complete_lattice downset"
   shows "mono F \<Longrightarrow> mono (map_SSup F)"
   unfolding fun_eq_iff mono_def map_SSup_def ds_def SSup_def comp_def
   by (metis Abs_downset_inverse Sup_subset_mono downset_iso_iff less_eq_downset.rep_eq rangeI)
 
 lemma map_SSup_prop: 
   fixes F :: "'a::complete_lattice downset \<Rightarrow> 'b::complete_lattice downset"
   shows "ds \<circ> map_SSup F = F \<circ> ds"
   unfolding map_SSup_def by (metis ds_SSup_inv fun.map_id0 id_def rewriteL_comp_comp)
 
 lemma map_SSup_prop2: 
   fixes F :: "'a::complete_lattice downset \<Rightarrow> 'b::complete_lattice downset"
   shows "ds \<circ> map_SSup F = id F \<circ> ds"
   by (simp add: map_SSup_prop)
 
 lemma map_ds_func1: "map_ds id = (id::'a::complete_lattice downset\<Rightarrow> 'a downset)"
   by (simp add: ds_SSup_inv map_ds_def)
 
 lemma map_ds_func2: 
   fixes g :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "map_ds (f \<circ> g) = map_ds f \<circ> map_ds g"
   unfolding map_ds_def fun_eq_iff comp_def ds_def SSup_def
   by (metis Abs_downset_inverse Sup_atMost atMost_def downset_prop rangeI)
 
 lemma map_SSup_func1: "map_SSup (id::'a::complete_lattice downset\<Rightarrow> 'a downset) = id"
   by (simp add: SSup_ds_inv map_SSup_def)
 
 lemma map_SSup_func2: 
   fixes F :: "'c::complete_lattice downset \<Rightarrow> 'b::complete_lattice downset"
   and G :: "'a::complete_lattice downset \<Rightarrow> 'c downset"
   shows "map_SSup (F \<circ> G) = map_SSup F \<circ> map_SSup G"
   unfolding map_SSup_def fun_eq_iff comp_def id_def ds_def
   by (metis comp_apply ds_SSup_inv ds_def id_apply)
 
 lemma map_SSup_map_ds_inv: "map_SSup \<circ> map_ds = (id::('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a \<Rightarrow> 'b))"
   by (metis (no_types, opaque_lifting) SSup_ds_inv comp_def eq_id_iff fun.map_comp fun.map_id0 id_apply map_SSup_prop map_ds_prop)
 
 lemma map_ds_map_SSup_inv: "map_ds \<circ> map_SSup = (id::('a::complete_lattice downset \<Rightarrow> 'b::complete_lattice downset) \<Rightarrow> ('a downset \<Rightarrow> 'b downset))"
   unfolding map_SSup_def map_ds_def SSup_def ds_def id_def comp_def fun_eq_iff
   by (metis (no_types, lifting) Rep_downset Rep_downset_inverse Sup_downset_id image_iff pointfree_idE)
 
 lemma inj_map_ds: "inj (map_ds::('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a downset \<Rightarrow> 'b downset))"
   by (metis (no_types, lifting) SSup_ds_inv fun.map_id0 id_comp inj_def map_ds_prop rewriteR_comp_comp2)
 
 lemma inj_map_SSup: "inj (map_SSup::('a::complete_lattice downset \<Rightarrow> 'b::complete_lattice downset) \<Rightarrow> ('a \<Rightarrow> 'b))"
   by (metis inj_on_id inj_on_imageI2 map_ds_map_SSup_inv)
 
 lemma map_ds_map_SSup_iff: 
   fixes g :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
   shows "(f = map_ds g) = (map_SSup f = g)"
   by (metis inj_eq inj_map_ds map_ds_map_SSup_inv pointfree_idE)
 
 text \<open>This gives an isomorphism between categories.\<close>
 
 lemma surj_map_ds: "surj (map_ds::('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a downset \<Rightarrow> 'b downset))"
   by (simp add: map_ds_map_SSup_iff surj_def)
 
 lemma surj_map_SSup: "surj (map_SSup::('a::complete_lattice_with_dual downset \<Rightarrow> 'b::complete_lattice_with_dual downset) \<Rightarrow> ('a \<Rightarrow> 'b))"
   by (metis map_ds_map_SSup_iff surjI)
 
 text \<open>There is of course a dual result for upsets with the reverse inclusion ordering. Once again, it seems impossible to capture 
 the "real" duality that uses the inverse image functor.\<close>
 
 typedef (overloaded) 'a upset = "range (\<up>::'a::ord \<Rightarrow> 'a set)"
   by fastforce
 
 setup_lifting type_definition_upset
     
 definition us :: "'a::ord \<Rightarrow> 'a upset" where 
   "us = Abs_upset \<circ> \<up>"
 
 definition IInf :: "'a::complete_lattice upset \<Rightarrow> 'a" where
   "IInf = Inf \<circ> Rep_upset"
 
 lemma us_ds: "us = Abs_upset \<circ> (`) \<partial> \<circ> Rep_downset \<circ> ds \<circ> (\<partial>::'a::ord_with_dual \<Rightarrow> 'a)" 
   unfolding us_def ds_def fun_eq_iff comp_def by (simp add: Abs_downset_inverse upset_to_downset2)
 
 lemma IInf_SSup: "IInf = \<partial> \<circ> SSup \<circ> Abs_downset \<circ> (`) (\<partial>::'a::complete_lattice_with_dual \<Rightarrow> 'a) \<circ> Rep_upset"
   unfolding IInf_def SSup_def fun_eq_iff comp_def
   by (metis (no_types, opaque_lifting) Abs_downset_inverse Rep_upset Sup_dual_def_var image_iff rangeI subset_dual upset_to_downset3)
 
 lemma us_IInf_inv: "us \<circ> IInf = (id::'a::complete_lattice_with_dual upset \<Rightarrow> 'a upset)"
   unfolding us_def IInf_def fun_eq_iff id_def comp_def
   by (metis (no_types, lifting) Inf_upset_id Rep_upset Rep_upset_inverse f_the_inv_into_f pointfree_idE upset_inj)
 
 lemma IInf_us_inv: "IInf \<circ> us = (id::'a::complete_lattice_with_dual \<Rightarrow> 'a)"
   unfolding us_def IInf_def fun_eq_iff id_def comp_def
   by (metis Abs_upset_inverse Sup_Inf_var Sup_atLeastAtMost Sup_dual_upset_var order_refl rangeI)
  
 instantiation upset :: (ord) order
 begin
   
 lift_definition less_eq_upset :: "'a upset \<Rightarrow> 'a upset \<Rightarrow> bool" is "(\<lambda>X Y. Rep_upset X \<supseteq> Rep_upset Y)" .
 
 lift_definition less_upset :: "'a upset \<Rightarrow> 'a upset \<Rightarrow> bool" is "(\<lambda>X Y. Rep_upset X \<supset> Rep_upset Y)" .
 
 instance
   by (intro_classes, transfer, simp_all add: less_le_not_le less_eq_upset.rep_eq Rep_upset_inject)
 
 end
   
 lemma us_iso: "x \<le> y \<Longrightarrow> us x \<le> us (y::'a::order_with_dual)"
   by (simp add: Abs_upset_inverse less_eq_upset.rep_eq upset_anti_iff us_def)
  
 lemma us_faithful: "us x \<le> us y \<Longrightarrow> x \<le> (y::'a::order_with_dual)"
   by (simp add: Abs_upset_inverse upset_faithful us_def less_eq_upset.rep_eq)
 
 lemma us_inj: "inj (us::'a::order_with_dual \<Rightarrow> 'a upset)"
   unfolding inj_def by (simp add: us_faithful dual_order.antisym)
 
 lemma us_surj: "surj (us::'a::order_with_dual \<Rightarrow> 'a upset)"
   unfolding surj_def by (metis Rep_upset Rep_upset_inverse comp_def image_iff us_def)
 
 lemma us_bij: "bij (us::'a::order_with_dual \<Rightarrow> 'a upset)"
   by (simp add: bij_def us_surj us_inj)
 
 lemma us_ord_iso: "ord_iso (us::'a::order_with_dual \<Rightarrow> 'a upset)"
   unfolding ord_iso_def 
   by (simp, metis (no_types, lifting) UNIV_I f_the_inv_into_f monoI us_iso us_bij us_faithful us_inj us_surj)
 
 definition map_us :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a upset \<Rightarrow> 'b upset)" where
   "map_us f = us \<circ> f \<circ> IInf"
 
 lemma map_us_prop: "map_us f \<circ> (us::'a::complete_lattice_with_dual \<Rightarrow> 'a upset) = us \<circ> id f"
   unfolding map_us_def by (simp add: IInf_us_inv comp_assoc) 
 
 definition map_IInf :: "('a upset \<Rightarrow> 'b upset) \<Rightarrow> ('a::complete_lattice \<Rightarrow> 'b::complete_lattice)" where
   "map_IInf F = IInf \<circ> F \<circ> us"
 
 lemma map_IInf_prop: "(us::'a::complete_lattice_with_dual \<Rightarrow> 'a upset) \<circ> map_IInf F = id F \<circ> us"
 proof-
   have "us \<circ> map_IInf F = (us \<circ> IInf) \<circ> F \<circ> us"
     by (simp add: fun.map_comp map_IInf_def)
   thus ?thesis
     by (simp add: us_IInf_inv)
 qed
 
 lemma map_us_func1: "map_us id = (id::'a::complete_lattice_with_dual upset \<Rightarrow> 'a upset)"
   unfolding map_us_def fun_eq_iff comp_def us_def id_def IInf_def
   by (metis (no_types, lifting) Inf_upset_id Rep_upset Rep_upset_inverse image_iff pointfree_idE)
 
 lemma map_us_func2: 
   fixes f :: "'c::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   and g :: "'a::complete_lattice_with_dual \<Rightarrow> 'c"
   shows "map_us (f \<circ> g) = map_us f \<circ> map_us g"
   unfolding map_us_def fun_eq_iff comp_def us_def IInf_def
   by (metis Abs_upset_inverse Sup_Inf_var Sup_atLeastAtMost Sup_dual_upset_var order_refl rangeI)
 
 lemma map_IInf_func1: "map_IInf id = (id::'a::complete_lattice_with_dual \<Rightarrow> 'a)"
   unfolding map_IInf_def fun_eq_iff comp_def id_def us_def IInf_def by (simp add: Abs_upset_inverse pointfree_idE)
 
 lemma map_IInf_func2: 
   fixes F :: "'c::complete_lattice_with_dual upset \<Rightarrow> 'b::complete_lattice_with_dual upset"
   and G :: "'a::complete_lattice_with_dual upset \<Rightarrow> 'c upset"
   shows "map_IInf (F \<circ> G) = map_IInf F \<circ> map_IInf G"
   unfolding map_IInf_def fun_eq_iff comp_def id_def us_def
   by (metis comp_apply id_apply us_IInf_inv us_def)
 
 lemma map_IInf_map_us_inv: "map_IInf \<circ> map_us = (id::('a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual) \<Rightarrow> ('a \<Rightarrow> 'b))"
   unfolding map_IInf_def map_us_def IInf_def us_def id_def comp_def fun_eq_iff by (simp add: Abs_upset_inverse pointfree_idE)
 
 lemma map_us_map_IInf_inv: "map_us \<circ> map_IInf = (id::('a::complete_lattice_with_dual upset \<Rightarrow> 'b::complete_lattice_with_dual upset) \<Rightarrow> ('a upset \<Rightarrow> 'b upset))"
   unfolding map_IInf_def map_us_def IInf_def us_def id_def comp_def fun_eq_iff
   by (metis (no_types, lifting) Inf_upset_id Rep_upset Rep_upset_inverse image_iff pointfree_idE)
 
 lemma inj_map_us: "inj (map_us::('a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual) \<Rightarrow> ('a upset \<Rightarrow> 'b upset))"
   unfolding map_us_def us_def IInf_def inj_def comp_def fun_eq_iff
   by (metis (no_types, opaque_lifting) Abs_upset_inverse Inf_upset_id pointfree_idE rangeI)
 
 lemma inj_map_IInf: "inj (map_IInf::('a::complete_lattice_with_dual upset \<Rightarrow> 'b::complete_lattice_with_dual upset) \<Rightarrow> ('a \<Rightarrow> 'b))"
   unfolding map_IInf_def fun_eq_iff inj_def comp_def IInf_def us_def
   by (metis (no_types, opaque_lifting) Inf_upset_id Rep_upset Rep_upset_inverse image_iff pointfree_idE)
 
 lemma map_us_map_IInf_iff: 
   fixes g :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual" 
   shows "(f = map_us g) = (map_IInf f = g)"
   by (metis inj_eq inj_map_us map_us_map_IInf_inv pointfree_idE)
 
 lemma map_us_mono_pres: 
   fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
   shows "mono f \<Longrightarrow> mono (map_us f)"
   unfolding mono_def map_us_def comp_def us_def IInf_def
   by (metis Abs_upset_inverse Inf_superset_mono less_eq_upset.rep_eq rangeI upset_anti_iff)
 
 lemma map_IInf_mono_pres: 
   fixes F :: "'a::complete_lattice_with_dual upset \<Rightarrow> 'b::complete_lattice_with_dual upset"
   shows "mono F \<Longrightarrow> mono (map_IInf F)"
   unfolding mono_def map_IInf_def comp_def us_def IInf_def
   oops 
 
 lemma surj_map_us: "surj (map_us::('a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual) \<Rightarrow> ('a upset \<Rightarrow> 'b upset))"
   by (simp add: map_us_map_IInf_iff surj_def)
 
 lemma surj_map_IInf: "surj (map_IInf::('a::complete_lattice_with_dual upset \<Rightarrow> 'b::complete_lattice_with_dual upset) \<Rightarrow> ('a \<Rightarrow> 'b))"
   by (metis map_us_map_IInf_iff surjI)
 
 text \<open>Hence we have again an isomorphism --- or rather equivalence --- between categories. Here, however, duality is not consistently picked up.\<close>
 
 
 subsection \<open>Stone's Theorem in the Presence of Atoms\<close>
 
 text \<open>Atom-map is a boolean algebra morphism.\<close>
 
 context boolean_algebra
 begin
 
 lemma atom_map_compl_pres: "atom_map (-x) = Collect atom - atom_map x"
 proof-
   {fix y
   have "(y \<in> atom_map (-x)) = (atom y \<and> y \<le> -x)"
     by (simp add: atom_map_def)
   also have "... = (atom y \<and> \<not>(y \<le> x))"
     by (metis atom_sup_iff inf.orderE inf_shunt sup_compl_top top.ordering_top_axioms ordering_top.extremum)
    also have "... = (y \<in> Collect atom - atom_map x)"
      using atom_map_def by auto
    finally have "(y \<in> atom_map (-x)) = (y \<in> Collect atom - atom_map x)".}
   thus ?thesis
     by blast
 qed
 
 lemma atom_map_sup_pres: "atom_map (x \<squnion> y) = atom_map x \<union> atom_map y"
 proof-
   {fix z
   have "(z \<in> atom_map (x \<squnion> y)) = (atom z \<and> z \<le> x \<squnion> y)"
     by (simp add: atom_map_def)
   also have "... = (atom z \<and> (z \<le> x \<or> z \<le> y))"
     using atom_sup_iff by auto
   also have "... = (z \<in> atom_map x \<union> atom_map y)"
     using atom_map_def by auto
   finally have "(z \<in> atom_map (x \<squnion> y)) = (z \<in> atom_map x \<union> atom_map y)"
     by blast}
   thus ?thesis
     by blast
 qed
 
 lemma atom_map_inf_pres: "atom_map (x \<sqinter> y) = atom_map x \<inter> atom_map y"
-  by (smt Diff_Un atom_map_compl_pres atom_map_sup_pres compl_inf double_compl)
+  by (smt (verit) Diff_Un atom_map_compl_pres atom_map_sup_pres compl_inf double_compl)
 
 lemma atom_map_minus_pres: "atom_map (x - y) = atom_map x - atom_map y"
   using atom_map_compl_pres atom_map_def diff_eq by auto
 
 end
 
 text \<open>The homomorphic images of boolean algebras under atom-map are boolean algebras 
 --- in fact powerset boolean algebras.\<close>
 
 instantiation atoms :: (boolean_algebra) boolean_algebra
 begin
 
 lift_definition minus_atoms :: "'a atoms \<Rightarrow> 'a atoms \<Rightarrow> 'a atoms" is "\<lambda>x y. Abs_atoms (Rep_atoms x - Rep_atoms y)".
 
 lift_definition uminus_atoms :: "'a atoms \<Rightarrow> 'a atoms" is  "\<lambda>x. Abs_atoms (Collect atom - Rep_atoms x)".
 
 lift_definition bot_atoms :: "'a atoms" is "Abs_atoms {}".
 
 lift_definition sup_atoms ::  "'a atoms \<Rightarrow> 'a atoms \<Rightarrow> 'a atoms" is "\<lambda>x y. Abs_atoms (Rep_atoms x \<union> Rep_atoms y)".
 
 lift_definition top_atoms :: "'a atoms" is "Abs_atoms (Collect atom)".
 
 lift_definition inf_atoms ::  "'a atoms \<Rightarrow> 'a atoms \<Rightarrow> 'a atoms" is "\<lambda>x y. Abs_atoms (Rep_atoms x \<inter> Rep_atoms y)".
 
 lift_definition less_eq_atoms :: "'a atoms \<Rightarrow> 'a atoms \<Rightarrow> bool" is "(\<lambda>x y. Rep_atoms x \<subseteq> Rep_atoms y)".
 
 lift_definition less_atoms :: "'a atoms \<Rightarrow> 'a atoms \<Rightarrow> bool" is "(\<lambda>x y. Rep_atoms x \<subset> Rep_atoms y)".
 
 instance
   apply intro_classes
                  apply (transfer, simp add: less_le_not_le)
                 apply (transfer, simp)
                apply (transfer, blast)
               apply (simp add: Rep_atoms_inject less_eq_atoms.abs_eq)
-             apply (transfer, smt Abs_atoms_inverse Rep_atoms atom_map_inf_pres image_iff inf_le1 rangeI)
-            apply (transfer, smt Abs_atoms_inverse Rep_atoms atom_map_inf_pres image_iff inf_le2 rangeI)
-           apply (transfer, smt Abs_atoms_inverse Rep_atoms atom_map_inf_pres image_iff le_iff_sup rangeI sup_inf_distrib1)
-          apply (transfer, smt Abs_atoms_inverse Rep_atoms atom_map_sup_pres image_iff image_iff inf.orderE inf_sup_aci(6) le_iff_sup order_refl rangeI rangeI)
-         apply (transfer, smt Abs_atoms_inverse Rep_atoms atom_map_sup_pres image_iff inf_sup_aci(6) le_iff_sup rangeI sup.left_commute sup.right_idem)
+             apply (transfer, smt (verit) Abs_atoms_inverse Rep_atoms atom_map_inf_pres image_iff inf_le1 rangeI)
+            apply (transfer, smt (verit) Abs_atoms_inverse Rep_atoms atom_map_inf_pres image_iff inf_le2 rangeI)
+           apply (transfer, smt (verit) Abs_atoms_inverse Rep_atoms atom_map_inf_pres image_iff le_iff_sup rangeI sup_inf_distrib1)
+          apply (transfer, smt (verit) Abs_atoms_inverse Rep_atoms atom_map_sup_pres image_iff image_iff inf.orderE inf_sup_aci(6) le_iff_sup order_refl rangeI rangeI)
+         apply (transfer, smt (verit) Abs_atoms_inverse Rep_atoms atom_map_sup_pres image_iff inf_sup_aci(6) le_iff_sup rangeI sup.left_commute sup.right_idem)
         apply (transfer, subst Abs_atoms_inverse, metis (no_types, lifting) Rep_atoms atom_map_sup_pres image_iff rangeI, simp)
        apply transfer using Abs_atoms_inverse atom_map_bot_pres apply blast
       apply (transfer, metis Abs_atoms_inverse Rep_atoms atom_map_compl_pres atom_map_top_pres diff_eq double_compl inf_le1 rangeE rangeI)
-     apply (transfer, smt Abs_atoms_inverse Rep_atoms atom_map_inf_pres atom_map_sup_pres image_iff rangeI sup_inf_distrib1)
+     apply (transfer, smt (verit, ccfv_threshold) Abs_atoms_inverse Rep_atoms atom_map_inf_pres atom_map_sup_pres image_iff rangeI sup_inf_distrib1)
     apply (transfer, metis (no_types, opaque_lifting) Abs_atoms_inverse Diff_disjoint Rep_atoms atom_map_compl_pres rangeE rangeI)
    apply (transfer, smt Abs_atoms_inverse uminus_atoms.abs_eq Rep_atoms Un_Diff_cancel atom_map_compl_pres atom_map_inf_pres atom_map_minus_pres atom_map_sup_pres atom_map_top_pres diff_eq double_compl inf_compl_bot_right rangeE rangeI sup_commute sup_compl_top)
-  by transfer (smt Abs_atoms_inverse Rep_atoms atom_map_compl_pres atom_map_inf_pres atom_map_minus_pres diff_eq rangeE rangeI)
+  apply (transfer, smt Abs_atoms_inverse Rep_atoms atom_map_compl_pres atom_map_inf_pres atom_map_minus_pres diff_eq rangeE rangeI)
+  done
 
 end
 
 text \<open>The homomorphism atom-map can then be restricted in its output type to the powerset boolean algebra.\<close>
 
 lemma at_map_bot_pres: "at_map \<bottom> = \<bottom>"
   by (simp add: at_map_def atom_map_bot_pres bot_atoms.transfer)
 
 lemma at_map_top_pres: "at_map \<top> = \<top>"
   by (simp add: at_map_def atom_map_top_pres top_atoms.transfer)
 
 lemma at_map_compl_pres: "at_map \<circ> uminus = uminus \<circ> at_map"
   unfolding fun_eq_iff by (simp add: Abs_atoms_inverse at_map_def atom_map_compl_pres uminus_atoms.abs_eq)
 
 lemma at_map_sup_pres: "at_map (x \<squnion> y) = at_map x \<squnion> at_map y"
   unfolding at_map_def comp_def by (metis (mono_tags, lifting) Abs_atoms_inverse atom_map_sup_pres rangeI sup_atoms.transfer)
 
 lemma at_map_inf_pres: "at_map (x \<sqinter> y) = at_map x \<sqinter> at_map y"
   unfolding at_map_def comp_def by (metis (mono_tags, lifting) Abs_atoms_inverse atom_map_inf_pres inf_atoms.transfer rangeI)
 
 lemma at_map_minus_pres: "at_map (x - y) = at_map x - at_map y"
   unfolding at_map_def comp_def by (simp add: Abs_atoms_inverse atom_map_minus_pres minus_atoms.abs_eq)
 
 
 context atomic_boolean_algebra
 begin
 
 text \<open>In atomic boolean algebras, atom-map is an embedding that maps atoms of the boolean algebra to 
 those of the powerset boolean algebra. Analogous properties hold for at-map.\<close>
 
 lemma inj_atom_map: "inj atom_map"
 proof-
   {fix x y ::'a
     assume "x \<noteq> y"
   hence "x \<sqinter> -y \<noteq> \<bottom> \<or> -x \<sqinter> y \<noteq> \<bottom>"
     by (auto simp: inf_shunt) 
   hence "\<exists>z. atom z \<and> (z \<le> x \<sqinter> -y \<or> z \<le> -x \<sqinter> y)"
     using atomicity by blast
   hence "\<exists>z. atom z \<and> ((z \<in> atom_map x \<and> \<not>(z \<in> atom_map y)) \<or> (\<not>(z \<in> atom_map x) \<and> z \<in> atom_map y))"
     unfolding atom_def atom_map_def by (clarsimp, metis diff_eq inf.orderE diff_shunt_var)
   hence "atom_map x \<noteq> atom_map y"
     by blast}
   thus ?thesis
     by (meson injI)
 qed
 
 lemma atom_map_atom_pres: "atom x \<Longrightarrow> atom_map x = {x}"
   unfolding atom_def atom_map_def by (auto simp: bot_less dual_order.order_iff_strict)
 
 lemma atom_map_atom_pres2: "atom x \<Longrightarrow> atom (atom_map x)"
 proof-
   assume "atom x"
   hence "atom_map x = {x}"
     by (simp add: atom_map_atom_pres)
   thus "atom (atom_map x)"
     using bounded_lattice_class.atom_def by auto
 qed
 
 end
 
 lemma inj_at_map: "inj (at_map::'a::atomic_boolean_algebra \<Rightarrow> 'a atoms)"
   unfolding at_map_def comp_def by (metis (no_types, lifting) Abs_atoms_inverse inj_atom_map inj_def rangeI)
 
 lemma at_map_atom_pres: "atom (x::'a::atomic_boolean_algebra) \<Longrightarrow> at_map x = Abs_atoms {x}"
   unfolding at_map_def comp_def by (simp add: atom_map_atom_pres)
 
 lemma at_map_atom_pres2: "atom (x::'a::atomic_boolean_algebra) \<Longrightarrow> atom (at_map x)"
   unfolding at_map_def comp_def
   by (metis Abs_atoms_inverse atom_def atom_map_atom_pres2 atom_map_bot_pres bot_atoms.abs_eq less_atoms.abs_eq rangeI)
 
 text \<open>Homomorphic images of atomic boolean algebras under atom-map are therefore atomic (rather obviously).\<close>
 
 instance atoms :: (atomic_boolean_algebra) atomic_boolean_algebra
 proof intro_classes
   fix x::"'a atoms"
   assume "x \<noteq> \<bottom>"
   hence "\<exists>y. x = at_map y \<and> x \<noteq> \<bottom>"
     unfolding at_map_def comp_def by (metis Abs_atoms_cases rangeE)
   hence "\<exists>y. x = at_map y \<and> (\<exists>z. atom z \<and> z \<le> y)"
     using at_map_bot_pres atomicity by force
   hence "\<exists>y. x = at_map y \<and> (\<exists>z. atom (at_map z) \<and> at_map z \<le> at_map y)"
     by (metis at_map_atom_pres2 at_map_sup_pres sup.orderE sup_ge2)
   thus "\<exists>y. atom y \<and> y \<le> x"
     by fastforce
 qed
 
 context complete_boolean_algebra_alt
 begin
 
 text \<open>In complete boolean algebras, atom-map is surjective; more precisely it is the left inverse
 of Sup, at least for sets of atoms. Below, this statement is made more explicit for at-map.\<close>
 
 lemma surj_atom_map: "Y \<subseteq> Collect atom \<Longrightarrow> Y = atom_map (\<Squnion>Y)"
 proof
   assume "Y \<subseteq> Collect atom"
   thus "Y \<subseteq> atom_map (\<Squnion>Y)"
     using Sup_upper atom_map_def by force
 next
   assume "Y \<subseteq> Collect atom"
   hence a: "\<forall>y. y \<in> Y \<longrightarrow> atom y"
     by blast
   {fix z
   assume h: "z \<in> Collect atom - Y"
   hence "\<forall>y \<in> Y. y \<sqinter> z = \<bottom>"
     by (metis DiffE a h atom_def dual_order.not_eq_order_implies_strict inf.absorb_iff2 inf_le2 inf_shunt mem_Collect_eq)
   hence "\<Squnion>Y \<sqinter> z = \<bottom>"
     using Sup_least inf_shunt by simp
   hence "z \<notin> atom_map (\<Squnion>Y)"
     using atom_map_bot_pres atom_map_def by force}
   thus  "atom_map (\<Squnion>Y) \<subseteq> Y"
     using atom_map_def by force
 qed
 
 text \<open>In this setting, atom-map is a complete boolean algebra morphism.\<close>
 
 lemma atom_map_Sup_pres: "atom_map (\<Squnion>X) = (\<Union>x \<in> X. atom_map x)"
 proof-
   {fix z
   have "(z \<in> atom_map (\<Squnion>X)) = (atom z \<and> z \<le> \<Squnion>X)"
     by (simp add: atom_map_def)
   also have "... = (atom z \<and> (\<exists>x \<in> X. z \<le> x))"
     using atom_Sup_iff by auto
   also have "... = (z \<in> (\<Union>x \<in> X. atom_map x))"
     using atom_map_def by auto
   finally have "(z \<in> atom_map (\<Squnion>X)) = (z \<in> (\<Union>x \<in> X. atom_map x))"
     by blast}
   thus ?thesis
     by blast
 qed
 
 lemma atom_map_Sup_pres_var: "atom_map \<circ> Sup = Sup \<circ> (`) atom_map"
   unfolding fun_eq_iff comp_def by (simp add: atom_map_Sup_pres) 
 
 text \<open>For Inf-preservation, it is important that Infs are restricted to homomorphic images; 
 hence they need to be pushed into the set of all atoms.\<close>
 
 lemma atom_map_Inf_pres: "atom_map (\<Sqinter>X) = Collect atom \<inter> (\<Inter>x \<in> X. atom_map x)"
 proof-
   have "atom_map (\<Sqinter>X) = atom_map (-(\<Squnion>x \<in> X. -x))"
     by (smt Collect_cong SUP_le_iff atom_map_def compl_le_compl_iff compl_le_swap1 le_Inf_iff)
   also have "... = Collect atom - atom_map (\<Squnion>x \<in> X. -x)"
     using atom_map_compl_pres by blast
   also have "... = Collect atom - (\<Union>x \<in> X. atom_map (-x))"  
     by (simp add: atom_map_Sup_pres)
   also have "... = Collect atom - (\<Union>x \<in> X. Collect atom - atom_map (x))" 
     using atom_map_compl_pres by blast
   also have "... = Collect atom \<inter> (\<Inter>x \<in> X. atom_map x)"
     by blast
   finally show ?thesis.
 qed
 
 end
 
 text \<open>It follows that homomorphic images of complete boolean algebras under atom-map form
 complete boolean algebras.\<close>
 
 instantiation atoms :: (complete_boolean_algebra_alt) complete_boolean_algebra_alt
 begin
 
 lift_definition Inf_atoms :: "'a::complete_boolean_algebra_alt atoms set \<Rightarrow> 'a::complete_boolean_algebra_alt atoms" is "\<lambda>X. Abs_atoms (Collect atom \<inter> Inter ((`) Rep_atoms X))".
 
 lift_definition  Sup_atoms :: "'a::complete_boolean_algebra_alt atoms set \<Rightarrow> 'a::complete_boolean_algebra_alt atoms" is "\<lambda>X. Abs_atoms (Union ((`) Rep_atoms X))".
 
 instance
   apply (intro_classes; transfer)
        apply (metis (no_types, opaque_lifting) Abs_atoms_inverse image_iff inf_le1 le_Inf_iff le_infI2 order_refl rangeI surj_atom_map)
       apply (metis (no_types, lifting) Abs_atoms_inverse Int_subset_iff Rep_atoms Sup_upper atom_map_atoms inf_le1 le_INF_iff rangeI surj_atom_map)
      apply (metis Abs_atoms_inverse Rep_atoms SUP_least SUP_upper Sup_upper atom_map_atoms rangeI surj_atom_map)
     apply (metis Abs_atoms_inverse Rep_atoms SUP_least Sup_upper atom_map_atoms rangeI surj_atom_map)
   by simp_all
 
 end
 
 text \<open>Once more, properties proved above can now be restricted to at-map.\<close>
 
 lemma  surj_at_map_var: "at_map \<circ> Sup \<circ> Rep_atoms = (id::'a::complete_boolean_algebra_alt atoms \<Rightarrow> 'a atoms)"
   unfolding at_map_def comp_def fun_eq_iff id_def by (metis Rep_atoms Rep_atoms_inverse Sup_upper atom_map_atoms surj_atom_map)
 
 lemma surj_at_map: "surj (at_map::'a::complete_boolean_algebra_alt \<Rightarrow> 'a atoms)"
   unfolding surj_def at_map_def comp_def by (metis Rep_atoms Rep_atoms_inverse image_iff)
 
 lemma at_map_Sup_pres: "at_map \<circ> Sup = Sup \<circ> (`) (at_map::'a::complete_boolean_algebra_alt \<Rightarrow> 'a atoms)"
   unfolding fun_eq_iff at_map_def comp_def atom_map_Sup_pres by (smt Abs_atoms_inverse Sup.SUP_cong Sup_atoms.transfer UN_extend_simps(10) rangeI)
 
 lemma at_map_Sup_pres_var: "at_map (\<Squnion>X) = (\<Squnion>(x::'a::complete_boolean_algebra_alt) \<in> X. (at_map x))"
   using at_map_Sup_pres comp_eq_elim by blast
 
 lemma at_map_Inf_pres: "at_map (\<Sqinter>X) = Abs_atoms (Collect atom \<sqinter> (\<Sqinter>x \<in> X. (Rep_atoms (at_map (x::'a::complete_boolean_algebra_alt)))))"
   unfolding at_map_def comp_def by (metis (no_types, lifting) Abs_atoms_inverse Sup.SUP_cong atom_map_Inf_pres rangeI)
 
 lemma at_map_Inf_pres_var: "at_map \<circ> Inf = Inf \<circ> (`) (at_map::'a::complete_boolean_algebra_alt \<Rightarrow> 'a atoms)"
   unfolding fun_eq_iff comp_def by (metis Inf_atoms.abs_eq at_map_Inf_pres image_image)
 
 text \<open>Finally, on complete atomic boolean algebras (CABAs), at-map is an isomorphism, that is, a bijection 
 that preserves the complete boolean algebra operations. Thus every CABA is isomorphic to a powerset boolean algebra
 and every powerset boolean algebra is a CABA. The bijective pair is given by at-map and Sup (defined on the powerset algebra).
 This theorem is a little version of Stone's theorem. In the general case, ultrafilters play the role of atoms.\<close>
 
 lemma "Sup \<circ> atom_map = (id::'a::complete_atomic_boolean_algebra \<Rightarrow> 'a)"
   unfolding fun_eq_iff comp_def id_def
   by (metis Union_upper atom_map_atoms inj_atom_map inj_def rangeI surj_atom_map)
 
 lemma inj_at_map_var: "Sup \<circ> Rep_atoms \<circ> at_map  = (id ::'a::complete_atomic_boolean_algebra \<Rightarrow> 'a)"
 
   unfolding at_map_def comp_def fun_eq_iff id_def
   by (metis Abs_atoms_inverse Union_upper atom_map_atoms inj_atom_map inj_def rangeI surj_atom_map)
 
 lemma bij_at_map: "bij (at_map::'a::complete_atomic_boolean_algebra \<Rightarrow> 'a atoms)"
   unfolding bij_def by (simp add: inj_at_map surj_at_map)
 
 instance atoms :: (complete_atomic_boolean_algebra) complete_atomic_boolean_algebra..
 
 text \<open>A full consideration of Stone duality is left for future work.\<close>
 
 (* Failed attempt to prove Tarski's fixpoint theorem: The problem is that we want to use mono, but this has two type parameters. It doesn't work inside of the one-type-parameter typedef.
 Yet isotonicity is needed to prove inhabitance of the type. I could develop a theory of isotone endos and prove the existence of 
 lfps and gfps, duplicating the more general facts for mono. But that's not the point. Because of this I see no direct way of proving
 Tarski's fixpoint theorem. Any way out?
 
 class complete_lattice_with_iso = complete_lattice +
   fixes f :: "'a \<Rightarrow> 'a"
 (*  assumes isof: "x \<le> y \<Longrightarrow> f x \<le> f y"*)
 
 typedef (overloaded) 'a Fix = "Fix (f::'a::complete_lattice_with_iso \<Rightarrow> 'a)" 
 
 
 setup_lifting type_definition_Fix
 
 *)
 
 end