(* Rudolf Berghammer and Walter Guttmann, 2016.01.29 *)

theory AAMP

imports Main

begin

(* Base *)

-- {* This theory and the subsequent theories have been developed with Isabelle2015. *}

class mult = times

begin

notation
  times (infixl "\<cdot>" 70) and
  times (infixl ";" 70)

end

class neg = uminus

begin

no_notation
  uminus ("- _" [81] 80)

notation
  uminus ("- _" [80] 80)

end

class while =
  fixes while :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<star>" 59)

class L =
  fixes L :: "'a"

class n =
  fixes n :: "'a \<Rightarrow> 'a"

class d =
  fixes d :: "'a \<Rightarrow> 'a"

class diamond =
  fixes diamond :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("| _ > _" [50,90] 95)

class box =
  fixes box :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("| _ ] _" [50,90] 95)

context ord

begin

definition isotone :: "('a \<Rightarrow> 'a) \<Rightarrow> bool"
  where "isotone f \<longleftrightarrow> (\<forall>x y . x \<le> y \<longrightarrow> f(x) \<le> f(y))"

definition lifted_less_eq :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("(_ \<le>\<le> _)" [51, 51] 50)
  where "f \<le>\<le> g \<longleftrightarrow> (\<forall>x . f(x) \<le> g(x))"

definition galois :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
  where "galois l u \<longleftrightarrow> (\<forall>x y . l(x) \<le> y \<longleftrightarrow> x \<le> u(y))"

definition ascending_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
  where "ascending_chain f \<longleftrightarrow> (\<forall>n . f n \<le> f (Suc n))"

definition descending_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
  where "descending_chain f \<longleftrightarrow> (\<forall>n . f (Suc n) \<le> f n)"

definition directed :: "'a set \<Rightarrow> bool"
  where "directed X \<longleftrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X . \<forall>y\<in>X . \<exists>z\<in>X . x \<le> z \<and> y \<le> z)"

definition codirected :: "'a set \<Rightarrow> bool"
  where "codirected X \<longleftrightarrow> X \<noteq> {} \<and> (\<forall>x\<in>X . \<forall>y\<in>X . \<exists>z\<in>X . z \<le> x \<and> z \<le> y)"

definition chain :: "'a set \<Rightarrow> bool"
  where "chain X \<longleftrightarrow> (\<forall>x\<in>X . \<forall>y\<in>X . x \<le> y \<or> y \<le> x)"

end

context order

begin

lemma lifted_reflexive: "f = g \<longrightarrow> f \<le>\<le> g"
  by (metis lifted_less_eq_def order_refl)

lemma lifted_transitive: "f \<le>\<le> g \<and> g \<le>\<le> h \<longrightarrow> f \<le>\<le> h"
  by (smt lifted_less_eq_def order_trans)

lemma lifted_antisymmetric: "f \<le>\<le> g \<and> g \<le>\<le> f \<longrightarrow> f = g"
  by (metis (full_types) antisym ext lifted_less_eq_def)

lemma galois_char: "galois l u \<longleftrightarrow> (\<forall>x . x \<le> u(l(x))) \<and> (\<forall>x . l(u(x)) \<le> x) \<and> isotone l \<and> isotone u"
  apply (rule iffI)
  apply (metis (full_types) galois_def isotone_def order_refl order_trans)
  apply (metis galois_def isotone_def order_trans)
  done

lemma galois_closure: "galois l u \<longrightarrow> l(x) = l(u(l(x))) \<and> u(x) = u(l(u(x)))"
  by (simp add: galois_char isotone_def order.antisym)

lemma ascending_chain_k: "ascending_chain f \<longrightarrow> f m \<le> f (m + k)"
  apply (induct k)
  apply simp
  apply (metis add_Suc_right ascending_chain_def order_trans)
  done

lemma ascending_chain_isotone: "ascending_chain f \<and> m \<le> k \<longrightarrow> f m \<le> f k"
  by (metis ascending_chain_k le_iff_add)

lemma ascending_chain_comparable: "ascending_chain f \<longrightarrow> f k \<le> f m \<or> f m \<le> f k"
  by (metis nat_le_linear ascending_chain_isotone)

lemma ascending_chain_chain: "ascending_chain f \<longrightarrow> chain (range f)"
  by (smt ascending_chain_comparable chain_def image_iff)

lemma chain_directed: "X \<noteq> {} \<and> chain X \<longrightarrow> directed X"
  by (metis chain_def directed_def)

lemma ascending_chain_directed: "ascending_chain f \<longrightarrow> directed (range f)"
  by (metis UNIV_not_empty ascending_chain_chain chain_directed empty_is_image)

lemma descending_chain_k: "descending_chain f \<longrightarrow> f (m + k) \<le> f m"
  apply (induct k)
  apply simp
  apply (metis add_Suc_right descending_chain_def order_trans)
  done

lemma descending_chain_antitone: "descending_chain f \<and> m \<le> k \<longrightarrow> f k \<le> f m"
  by (metis descending_chain_k le_iff_add)

lemma descending_chain_comparable: "descending_chain f \<longrightarrow> f k \<le> f m \<or> f m \<le> f k"
  by (metis nat_le_linear descending_chain_antitone)

lemma descending_chain_chain: "descending_chain f \<longrightarrow> chain (range f)"
  unfolding chain_def
  apply simp
  apply (smt descending_chain_comparable)
  done

lemma chain_codirected: "X \<noteq> {} \<and> chain X \<longrightarrow> codirected X"
  by (metis chain_def codirected_def)

lemma descending_chain_codirected: "descending_chain f \<longrightarrow> codirected (range f)"
  by (metis UNIV_not_empty descending_chain_chain chain_codirected empty_is_image)

end

context complete_lattice

begin

lemma sup_Sup: assumes nonempty: "A \<noteq> {}"
   shows "sup x (Sup A) = Sup ((sup x) ` A)"
  apply (rule antisym)
  apply (metis Sup_mono Sup_upper2 assms ex_in_conv imageI le_supI sup_ge1 sup_ge2)
  apply (smt Sup_least Sup_upper image_iff le_iff_sup sup.commute sup_ge1 sup_left_commute)
  done

lemma sup_SUP: "Y \<noteq> {} \<longrightarrow> sup x (SUP y:Y . f y) = (SUP y:Y. sup x (f y))"
  unfolding SUP_def
  apply rule
  apply (subst sup_Sup)
  apply (smt empty_is_image)
  apply (metis image_image)
  done

lemma inf_Inf: assumes nonempty: "A \<noteq> {}"
   shows "inf x (Inf A) = Inf ((inf x) ` A)"
  apply (rule antisym)
  apply (smt Inf_greatest Inf_lower image_iff le_iff_inf inf.commute inf_le1 inf_left_commute)
  apply (metis Inf_mono Inf_lower2 assms ex_in_conv imageI le_infI inf_le1 inf_le2)
  done

lemma inf_INF: "Y \<noteq> {} \<longrightarrow> inf x (INF y:Y . f y) = (INF y:Y. inf x (f y))"
  unfolding INF_def
  apply rule
  apply (subst inf_Inf)
  apply (smt empty_is_image)
  apply (metis image_image)
  done

lemma SUP_image_id[simp]: "(SUP x:f`A . x) = (SUP x:A . f x)"
  by simp

lemma INF_image_id[simp]: "(INF x:f`A . x) = (INF x:A . f x)"
  by simp

end

lemma image_Collect_2: "f ` { g x | x . P x } = { f (g x) | x . P x }"
  by auto

-- {* The following instantiation and four lemmas are from Jose Divason Mallagaray. *}

instantiation "fun" :: (type, type) power

begin

definition one_fun :: "'a \<Rightarrow> 'a"
  where one_fun_def: "one_fun \<equiv> id"

definition times_fun :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
  where times_fun_def: "times_fun \<equiv> comp"

instance
  by intro_classes

end

lemma id_power: "id^m = id"
  apply (induct m)
  apply (metis one_fun_def power_0)
  apply (simp add: times_fun_def)
  done

lemma power_zero_id: "f^0 = id"
  by (metis one_fun_def power_0)

lemma power_succ_unfold: "f^Suc m = f \<circ> f^m"
  by (metis power_Suc times_fun_def)

lemma power_succ_unfold_ext: "(f^Suc m) x = f ((f^m) x)"
  by (metis o_apply power_succ_unfold)

(* Fixpoint *)

context order

begin

definition is_fixpoint               :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where "is_fixpoint              f x \<longleftrightarrow> f(x) = x"
definition is_prefixpoint            :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where "is_prefixpoint           f x \<longleftrightarrow> f(x) \<le> x"
definition is_postfixpoint           :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where "is_postfixpoint          f x \<longleftrightarrow> f(x) \<ge> x"
definition is_least_fixpoint         :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where "is_least_fixpoint        f x \<longleftrightarrow> f(x) = x \<and> (\<forall>y . f(y) = y \<longrightarrow> x \<le> y)"
definition is_greatest_fixpoint      :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where "is_greatest_fixpoint     f x \<longleftrightarrow> f(x) = x \<and> (\<forall>y . f(y) = y \<longrightarrow> x \<ge> y)"
definition is_least_prefixpoint      :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where "is_least_prefixpoint     f x \<longleftrightarrow> f(x) \<le> x \<and> (\<forall>y . f(y) \<le> y \<longrightarrow> x \<le> y)"
definition is_greatest_postfixpoint  :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where "is_greatest_postfixpoint f x \<longleftrightarrow> f(x) \<ge> x \<and> (\<forall>y . f(y) \<ge> y \<longrightarrow> x \<ge> y)"
definition has_fixpoint              :: "('a \<Rightarrow> 'a) \<Rightarrow> bool" where "has_fixpoint              f \<longleftrightarrow> (\<exists>x . is_fixpoint f x)"
definition has_prefixpoint           :: "('a \<Rightarrow> 'a) \<Rightarrow> bool" where "has_prefixpoint           f \<longleftrightarrow> (\<exists>x . is_prefixpoint f x)"
definition has_postfixpoint          :: "('a \<Rightarrow> 'a) \<Rightarrow> bool" where "has_postfixpoint          f \<longleftrightarrow> (\<exists>x . is_postfixpoint f x)"
definition has_least_fixpoint        :: "('a \<Rightarrow> 'a) \<Rightarrow> bool" where "has_least_fixpoint        f \<longleftrightarrow> (\<exists>x . is_least_fixpoint f x)"
definition has_greatest_fixpoint     :: "('a \<Rightarrow> 'a) \<Rightarrow> bool" where "has_greatest_fixpoint     f \<longleftrightarrow> (\<exists>x . is_greatest_fixpoint f x)"
definition has_least_prefixpoint     :: "('a \<Rightarrow> 'a) \<Rightarrow> bool" where "has_least_prefixpoint     f \<longleftrightarrow> (\<exists>x . is_least_prefixpoint f x)"
definition has_greatest_postfixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> bool" where "has_greatest_postfixpoint f \<longleftrightarrow> (\<exists>x . is_greatest_postfixpoint f x)"
definition the_least_fixpoint        :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<mu> _"  [201] 200) where "\<mu>  f = (THE x . is_least_fixpoint f x)"
definition the_greatest_fixpoint     :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<nu> _"  [201] 200) where "\<nu>  f = (THE x . is_greatest_fixpoint f x)"
definition the_least_prefixpoint     :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("p\<mu> _" [201] 200) where "p\<mu> f = (THE x . is_least_prefixpoint f x)"
definition the_greatest_postfixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("p\<nu> _" [201] 200) where "p\<nu> f = (THE x . is_greatest_postfixpoint f x)"

lemma least_fixpoint_unique: "has_least_fixpoint f \<longrightarrow> (\<exists>!x . is_least_fixpoint f x)"
  by (smt antisym has_least_fixpoint_def is_least_fixpoint_def)

lemma greatest_fixpoint_unique: "has_greatest_fixpoint f \<longrightarrow> (\<exists>!x . is_greatest_fixpoint f x)"
  by (smt antisym has_greatest_fixpoint_def is_greatest_fixpoint_def)

lemma least_prefixpoint_unique: "has_least_prefixpoint f \<longrightarrow> (\<exists>!x . is_least_prefixpoint f x)"
  by (smt antisym has_least_prefixpoint_def is_least_prefixpoint_def)

lemma greatest_postfixpoint_unique: "has_greatest_postfixpoint f \<longrightarrow> (\<exists>!x . is_greatest_postfixpoint f x)"
  by (smt antisym has_greatest_postfixpoint_def is_greatest_postfixpoint_def)

lemma least_fixpoint: "has_least_fixpoint f \<longrightarrow> is_least_fixpoint f (\<mu> f)"
proof
  assume "has_least_fixpoint f"
  hence "is_least_fixpoint f (THE x . is_least_fixpoint f x)"
    by (smt least_fixpoint_unique theI')
  thus "is_least_fixpoint f (\<mu> f)"
    by (simp add: is_least_fixpoint_def the_least_fixpoint_def)
qed

lemma greatest_fixpoint: "has_greatest_fixpoint f \<longrightarrow> is_greatest_fixpoint f (\<nu> f)"
proof
  assume "has_greatest_fixpoint f"
  hence "is_greatest_fixpoint f (THE x . is_greatest_fixpoint f x)"
    by (smt greatest_fixpoint_unique theI')
  thus "is_greatest_fixpoint f (\<nu> f)"
    by (simp add: is_greatest_fixpoint_def the_greatest_fixpoint_def)
qed

lemma least_prefixpoint: "has_least_prefixpoint f \<longrightarrow> is_least_prefixpoint f (p\<mu> f)"
proof
  assume "has_least_prefixpoint f"
  hence "is_least_prefixpoint f (THE x . is_least_prefixpoint f x)"
    by (smt least_prefixpoint_unique theI')
  thus "is_least_prefixpoint f (p\<mu> f)"
    by (simp add: is_least_prefixpoint_def the_least_prefixpoint_def)
qed

lemma greatest_postfixpoint: "has_greatest_postfixpoint f \<longrightarrow> is_greatest_postfixpoint f (p\<nu> f)"
proof
  assume "has_greatest_postfixpoint f"
  hence "is_greatest_postfixpoint f (THE x . is_greatest_postfixpoint f x)"
    by (smt greatest_postfixpoint_unique theI')
  thus "is_greatest_postfixpoint f (p\<nu> f)"
    by (simp add: is_greatest_postfixpoint_def the_greatest_postfixpoint_def)
qed

lemma least_fixpoint_same: "is_least_fixpoint f x \<longrightarrow> x = \<mu> f"
  by (metis least_fixpoint least_fixpoint_unique has_least_fixpoint_def)

lemma greatest_fixpoint_same: "is_greatest_fixpoint f x \<longrightarrow> x = \<nu> f"
  by (metis greatest_fixpoint greatest_fixpoint_unique has_greatest_fixpoint_def)

lemma least_prefixpoint_same: "is_least_prefixpoint f x \<longrightarrow> x = p\<mu> f"
  by (metis least_prefixpoint least_prefixpoint_unique has_least_prefixpoint_def)

lemma greatest_postfixpoint_same: "is_greatest_postfixpoint f x \<longrightarrow> x = p\<nu> f"
  by (metis greatest_postfixpoint greatest_postfixpoint_unique has_greatest_postfixpoint_def)

lemma least_fixpoint_char: "is_least_fixpoint f x \<longleftrightarrow> has_least_fixpoint f \<and> x = \<mu> f"
  by (metis least_fixpoint_same has_least_fixpoint_def)

lemma least_prefixpoint_char: "is_least_prefixpoint f x \<longleftrightarrow> has_least_prefixpoint f \<and> x = p\<mu> f"
  by (metis least_prefixpoint_same has_least_prefixpoint_def)

lemma greatest_fixpoint_char: "is_greatest_fixpoint f x \<longleftrightarrow> has_greatest_fixpoint f \<and> x = \<nu> f"
  by (metis greatest_fixpoint_same has_greatest_fixpoint_def)

lemma greatest_postfixpoint_char: "is_greatest_postfixpoint f x \<longleftrightarrow> has_greatest_postfixpoint f \<and> x = p\<nu> f"
  by (metis greatest_postfixpoint_same has_greatest_postfixpoint_def)

lemma mu_unfold: "has_least_fixpoint f \<longrightarrow> f (\<mu> f) = \<mu> f"
  by (metis is_least_fixpoint_def least_fixpoint)

lemma pmu_unfold: "has_least_prefixpoint f \<longrightarrow> f (p\<mu> f) \<le> p\<mu> f"
  by (metis is_least_prefixpoint_def least_prefixpoint)

lemma nu_unfold: "has_greatest_fixpoint f \<longrightarrow> \<nu> f = f (\<nu> f)"
  by (metis is_greatest_fixpoint_def greatest_fixpoint)

lemma pnu_unfold: "has_greatest_postfixpoint f \<longrightarrow> p\<nu> f \<le> f (p\<nu> f)"
  by (metis is_greatest_postfixpoint_def greatest_postfixpoint)

lemma least_prefixpoint_fixpoint: "has_least_prefixpoint f \<and> isotone f \<longrightarrow> is_least_fixpoint f (p\<mu> f)"
  by (smt eq_iff is_least_fixpoint_def is_least_prefixpoint_def isotone_def least_prefixpoint)

lemma pmu_mu: "has_least_prefixpoint f \<and> isotone f \<longrightarrow> p\<mu> f = \<mu> f"
  by (smt has_least_fixpoint_def is_least_fixpoint_def least_fixpoint_unique least_prefixpoint_fixpoint least_fixpoint)

lemma greatest_postfixpoint_fixpoint: "has_greatest_postfixpoint f \<and> isotone f \<longrightarrow> is_greatest_fixpoint f (p\<nu> f)"
  by (smt eq_iff is_greatest_fixpoint_def is_greatest_postfixpoint_def isotone_def greatest_postfixpoint)

lemma pnu_nu: "has_greatest_postfixpoint f \<and> isotone f \<longrightarrow> p\<nu> f = \<nu> f"
  by (smt has_greatest_fixpoint_def is_greatest_fixpoint_def greatest_fixpoint_unique greatest_postfixpoint_fixpoint greatest_fixpoint)

lemma pmu_isotone: "has_least_prefixpoint f \<and> has_least_prefixpoint g \<and> f \<le>\<le> g \<longrightarrow> p\<mu> f \<le> p\<mu> g"
  by (smt is_least_prefixpoint_def least_prefixpoint lifted_less_eq_def order_trans)

lemma mu_isotone: "has_least_prefixpoint f \<and> has_least_prefixpoint g \<and> isotone f \<and> isotone g \<and> f \<le>\<le> g \<longrightarrow> \<mu> f \<le> \<mu> g"
  by (metis pmu_isotone pmu_mu)

lemma pnu_isotone: "has_greatest_postfixpoint f \<and> has_greatest_postfixpoint g \<and> f \<le>\<le> g \<longrightarrow> p\<nu> f \<le> p\<nu> g"
  by (smt is_greatest_postfixpoint_def lifted_less_eq_def order_trans greatest_postfixpoint)

lemma nu_isotone: "has_greatest_postfixpoint f \<and> has_greatest_postfixpoint g \<and> isotone f \<and> isotone g \<and> f \<le>\<le> g \<longrightarrow> \<nu> f \<le> \<nu> g"
  by (metis pnu_isotone pnu_nu)

lemma mu_square: "isotone f \<and> has_least_fixpoint f \<and> has_least_fixpoint (f \<circ> f) \<longrightarrow> \<mu> f = \<mu> (f \<circ> f)"
proof
  assume 1: "isotone f \<and> has_least_fixpoint f \<and> has_least_fixpoint (f \<circ> f)"
  hence 2: "is_least_fixpoint (f \<circ> f) (\<mu> (f \<circ> f)) \<and> is_least_fixpoint f (\<mu> f)"
    using least_fixpoint by auto
  hence "f (\<mu> (f \<circ> f)) \<le> \<mu> (f \<circ> f)" using 1
    by (metis (no_types) comp_def is_least_fixpoint_def isotone_def)
  thus "\<mu> f = \<mu> (f \<circ> f)" using 2
    by (metis comp_def is_least_fixpoint_def antisym_conv)
qed

lemma nu_square: "isotone f \<and> has_greatest_fixpoint f \<and> has_greatest_fixpoint (f \<circ> f) \<longrightarrow> \<nu> f = \<nu> (f \<circ> f)"
proof
  assume 1: "isotone f \<and> has_greatest_fixpoint f \<and> has_greatest_fixpoint (f \<circ> f)"
  hence 2: "is_greatest_fixpoint (f \<circ> f) (\<nu> (f \<circ> f)) \<and> is_greatest_fixpoint f (\<nu> f)"
    using greatest_fixpoint by auto
  hence "\<nu> (f \<circ> f) \<le> f (\<nu> (f \<circ> f))" using 1
    by (metis (no_types) comp_def is_greatest_fixpoint_def isotone_def)
  thus "\<nu> f = \<nu> (f \<circ> f)" using 2
    by (metis comp_def is_greatest_fixpoint_def antisym_conv)
qed

lemma mu_roll: "isotone g \<and> has_least_fixpoint (f \<circ> g) \<and> has_least_fixpoint (g \<circ> f) \<longrightarrow> \<mu> (g \<circ> f) = g(\<mu> (f \<circ> g))"
  apply (rule impI)
  apply (rule antisym)
  apply (smt is_least_fixpoint_def least_fixpoint o_apply)
  apply (smt is_least_fixpoint_def isotone_def least_fixpoint o_apply)
  done

lemma nu_roll: "isotone g \<and> has_greatest_fixpoint (f \<circ> g) \<and> has_greatest_fixpoint (g \<circ> f) \<longrightarrow> \<nu> (g \<circ> f) = g(\<nu> (f \<circ> g))"
  apply (rule impI)
  apply (rule antisym)
  apply (smt is_greatest_fixpoint_def greatest_fixpoint isotone_def o_apply)
  apply (smt is_greatest_fixpoint_def greatest_fixpoint o_apply)
  done

lemma mu_below_nu: "has_least_fixpoint f \<and> has_greatest_fixpoint f \<longrightarrow> \<mu> f \<le> \<nu> f"
  by (metis is_greatest_fixpoint_def is_least_fixpoint_def least_fixpoint greatest_fixpoint)

lemma pmu_below_pnu_fix: "has_fixpoint f \<and> has_least_prefixpoint f \<and> has_greatest_postfixpoint f \<longrightarrow> p\<mu> f \<le> p\<nu> f"
  by (smt has_fixpoint_def is_fixpoint_def is_greatest_postfixpoint_def is_least_prefixpoint_def le_less order_trans least_prefixpoint greatest_postfixpoint)

lemma pmu_below_pnu_iso: "isotone f \<and> has_least_prefixpoint f \<and> has_greatest_postfixpoint f \<longrightarrow> p\<mu> f \<le> p\<nu> f"
  by (metis has_fixpoint_def is_fixpoint_def is_least_fixpoint_def least_prefixpoint_fixpoint pmu_below_pnu_fix)

lemma mu_fusion_1: "galois l u \<and> isotone h \<and> has_least_prefixpoint g \<and> has_least_fixpoint h \<and> l(g(u(\<mu> h))) \<le> h(l(u(\<mu> h))) \<longrightarrow> l(p\<mu> g) \<le> \<mu> h"
proof
  assume 1: "galois l u \<and> isotone h \<and> has_least_prefixpoint g \<and> has_least_fixpoint h \<and> l(g(u(\<mu> h))) \<le> h(l(u(\<mu> h)))"
  hence "l(g(u(\<mu> h))) \<le> \<mu> h"
    by (metis galois_char least_fixpoint_same least_fixpoint_unique is_least_fixpoint_def isotone_def order_trans)
  thus "l(p\<mu> g) \<le> \<mu> h" using 1
    by (metis galois_def least_prefixpoint is_least_prefixpoint_def least_fixpoint_same least_fixpoint_unique)
qed

lemma mu_fusion_2: "galois l u \<and> isotone h \<and> has_least_prefixpoint g \<and> has_least_fixpoint h \<and> l \<circ> g \<le>\<le> h \<circ> l \<longrightarrow> l(p\<mu> g) \<le> \<mu> h"
  by (metis lifted_less_eq_def mu_fusion_1 o_apply)

lemma mu_fusion_equal_1: "galois l u \<and> isotone g \<and> isotone h \<and> has_least_prefixpoint g \<and> has_least_fixpoint h \<and> l(g(u(\<mu> h))) \<le> h(l(u(\<mu> h))) \<and> l(g(p\<mu> g)) = h(l(p\<mu> g)) \<longrightarrow> \<mu> h = l(p\<mu> g) \<and> \<mu> h = l(\<mu> g)"
  by (metis antisym least_fixpoint least_prefixpoint_fixpoint is_least_fixpoint_def mu_fusion_1 pmu_mu)

lemma mu_fusion_equal_2: "galois l u \<and> isotone h \<and> has_least_prefixpoint g \<and> has_least_prefixpoint h \<and> l(g(u(\<mu> h))) \<le> h(l(u(\<mu> h))) \<and> l(g(p\<mu> g)) = h(l(p\<mu> g)) \<longrightarrow> p\<mu> h = l(p\<mu> g) \<and> \<mu> h = l(p\<mu> g)"
proof -
  have "galois l u \<and> isotone h \<and> has_least_prefixpoint g \<and> has_least_prefixpoint h \<and> l(g(p\<mu> g)) = h(l(p\<mu> g)) \<longrightarrow> \<mu> h \<le> l(p\<mu> g)"
    by (metis galois_char is_least_prefixpoint_def isotone_def least_fixpoint_char least_prefixpoint least_prefixpoint_fixpoint)
  thus ?thesis
    by (metis antisym least_fixpoint_char least_prefixpoint_fixpoint mu_fusion_1)
qed

lemma mu_fusion_equal_3: "galois l u \<and> isotone g \<and> isotone h \<and> has_least_prefixpoint g \<and> has_least_fixpoint h \<and> l \<circ> g = h \<circ> l \<longrightarrow> \<mu> h = l(p\<mu> g) \<and> \<mu> h = l(\<mu> g)"
  by (metis mu_fusion_equal_1 o_apply order_refl)

lemma mu_fusion_equal_4: "galois l u \<and> isotone h \<and> has_least_prefixpoint g \<and> has_least_prefixpoint h \<and> l \<circ> g = h \<circ> l \<longrightarrow> p\<mu> h = l(p\<mu> g) \<and> \<mu> h = l(p\<mu> g)"
  by (metis mu_fusion_equal_2 o_apply order_refl)

lemma nu_fusion_1: "galois l u \<and> isotone h \<and> has_greatest_postfixpoint g \<and> has_greatest_fixpoint h \<and> h(u(l(\<nu> h))) \<le> u(g(l(\<nu> h))) \<longrightarrow> \<nu> h \<le> u(p\<nu> g)"
proof
  assume 1: "galois l u \<and> isotone h \<and> has_greatest_postfixpoint g \<and> has_greatest_fixpoint h \<and> h(u(l(\<nu> h))) \<le> u(g(l(\<nu> h)))"
  hence "\<nu> h \<le> u(g(l(\<nu> h)))" using 1
    by (metis galois_char greatest_fixpoint_same greatest_fixpoint_unique is_greatest_fixpoint_def isotone_def order_trans)
  thus "\<nu> h \<le> u(p\<nu> g)" using 1
    by (smt galois_def greatest_postfixpoint is_greatest_postfixpoint_def greatest_fixpoint_same greatest_fixpoint_unique)
qed

lemma nu_fusion_2: "galois l u \<and> isotone h \<and> has_greatest_postfixpoint g \<and> has_greatest_fixpoint h \<and> h \<circ> u \<le>\<le> u \<circ> g \<longrightarrow> \<nu> h \<le> u(p\<nu> g)"
  by (metis lifted_less_eq_def nu_fusion_1 o_apply)

lemma nu_fusion_equal_1: "galois l u \<and> isotone g \<and> isotone h \<and> has_greatest_postfixpoint g \<and> has_greatest_fixpoint h \<and> h(u(l(\<nu> h))) \<le> u(g(l(\<nu> h))) \<and> h(u(p\<nu> g)) = u(g(p\<nu> g)) \<longrightarrow> \<nu> h = u(p\<nu> g) \<and> \<nu> h = u(\<nu> g)"
  by (metis antisym greatest_fixpoint greatest_postfixpoint_fixpoint is_greatest_fixpoint_def nu_fusion_1 pnu_nu)

lemma nu_fusion_equal_2: "galois l u \<and> isotone h \<and> has_greatest_postfixpoint g \<and> has_greatest_postfixpoint h \<and> h(u(l(\<nu> h))) \<le> u(g(l(\<nu> h))) \<and> h(u(p\<nu> g)) = u(g(p\<nu> g)) \<longrightarrow> p\<nu> h = u(p\<nu> g) \<and> \<nu> h = u(p\<nu> g)"
proof -
  have "galois l u \<and> isotone h \<and> has_greatest_postfixpoint g \<and> has_greatest_postfixpoint h \<and> h(u(p\<nu> g)) = u(g(p\<nu> g)) \<longrightarrow> u(p\<nu> g) \<le> \<nu> h"
    by (metis galois_char greatest_fixpoint_char greatest_postfixpoint greatest_postfixpoint_fixpoint is_greatest_postfixpoint_def isotone_def)
  thus ?thesis
    by (metis antisym greatest_fixpoint_char greatest_postfixpoint_fixpoint nu_fusion_1)
qed

lemma nu_fusion_equal_3: "galois l u \<and> isotone g \<and> isotone h \<and> has_greatest_postfixpoint g \<and> has_greatest_fixpoint h \<and> h \<circ> u = u \<circ> g \<longrightarrow> \<nu> h = u(p\<nu> g) \<and> \<nu> h = u(\<nu> g)"
  by (metis nu_fusion_equal_1 o_apply order_refl)

lemma nu_fusion_equal_4: "galois l u \<and> isotone h \<and> has_greatest_postfixpoint g \<and> has_greatest_postfixpoint h \<and> h \<circ> u = u \<circ> g \<longrightarrow> p\<nu> h = u(p\<nu> g) \<and> \<nu> h = u(p\<nu> g)"
  by (metis nu_fusion_equal_2 o_apply order_refl)

lemma mu_exchange_1: "galois l u \<and> isotone g \<and> isotone h \<and> has_least_prefixpoint (l \<circ> h) \<and> has_least_prefixpoint (h \<circ> g) \<and> has_least_fixpoint (g \<circ> h) \<and> l \<circ> h \<circ> g \<le>\<le> g \<circ> h \<circ> l \<longrightarrow> \<mu>(l \<circ> h) \<le> \<mu>(g \<circ> h)"
proof
  assume 1: "galois l u \<and> isotone g \<and> isotone h \<and> has_least_prefixpoint (l \<circ> h) \<and> has_least_prefixpoint (h \<circ> g) \<and> has_least_fixpoint (g \<circ> h) \<and> l \<circ> h \<circ> g \<le>\<le> g \<circ> h \<circ> l"
  hence 2: "l \<circ> (h \<circ> g) \<le>\<le> (g \<circ> h) \<circ> l"
    by (metis o_assoc)
  have "(l \<circ> h) (\<mu>(g \<circ> h)) = l(\<mu>(h \<circ> g))" using 1
    by (metis isotone_def least_fixpoint_char least_prefixpoint_fixpoint mu_roll o_apply)
  also have "... \<le> \<mu>(g \<circ> h)" using 1 2
    by (metis isotone_def least_fixpoint_char least_prefixpoint_fixpoint mu_fusion_2 o_apply)
  finally have "p\<mu>(l \<circ> h) \<le> \<mu>(g \<circ> h)" using 1
    by (metis is_least_prefixpoint_def least_prefixpoint)
  thus "\<mu>(l \<circ> h) \<le> \<mu>(g \<circ> h)" using 1
    by (metis galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint o_apply)
qed

lemma mu_exchange_2: "galois l u \<and> isotone g \<and> isotone h \<and> has_least_prefixpoint (l \<circ> h) \<and> has_least_prefixpoint (h \<circ> l) \<and> has_least_prefixpoint (h \<circ> g) \<and> has_least_fixpoint (g \<circ> h) \<and> has_least_fixpoint (h \<circ> g) \<and> l \<circ> h \<circ> g \<le>\<le> g \<circ> h \<circ> l \<longrightarrow> \<mu>(h \<circ> l) \<le> \<mu>(h \<circ> g)"
proof
  assume 1: "galois l u \<and> isotone g \<and> isotone h \<and> has_least_prefixpoint (l \<circ> h) \<and> has_least_prefixpoint (h \<circ> l) \<and> has_least_prefixpoint (h \<circ> g) \<and> has_least_fixpoint (g \<circ> h) \<and> has_least_fixpoint (h \<circ> g) \<and> l \<circ> h \<circ> g \<le>\<le> g \<circ> h \<circ> l"
  have "\<mu>(h \<circ> l) = h(\<mu>(l \<circ> h))" using 1
    by (metis (no_types, lifting) galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint mu_roll o_apply)
  also have "... \<le> h(\<mu>(g \<circ> h))" using 1
    using isotone_def mu_exchange_1 by blast
  also have "... = \<mu>(h \<circ> g)" using 1
    by (metis mu_roll)
  finally show "\<mu>(h \<circ> l) \<le> \<mu>(h \<circ> g)"
    .
qed

lemma mu_exchange_equal: "galois l u \<and> galois k t \<and> isotone h \<and> has_least_prefixpoint (l \<circ> h) \<and> has_least_prefixpoint (h \<circ> l) \<and> has_least_prefixpoint (k \<circ> h) \<and> has_least_prefixpoint (h \<circ> k) \<and> l \<circ> h \<circ> k = k \<circ> h \<circ> l \<longrightarrow> \<mu>(l \<circ> h) = \<mu>(k \<circ> h) \<and> \<mu>(h \<circ> l) = \<mu>(h \<circ> k)"
  using antisym galois_char isotone_def least_fixpoint_char least_prefixpoint_fixpoint lifted_reflexive mu_exchange_1 mu_exchange_2 by force

lemma nu_exchange_1: "galois l u \<and> isotone g \<and> isotone h \<and> has_greatest_postfixpoint (u \<circ> h) \<and> has_greatest_postfixpoint (h \<circ> g) \<and> has_greatest_fixpoint (g \<circ> h) \<and> g \<circ> h \<circ> u \<le>\<le> u \<circ> h \<circ> g \<longrightarrow> \<nu>(g \<circ> h) \<le> \<nu>(u \<circ> h)"
proof
  assume 1: "galois l u \<and> isotone g \<and> isotone h \<and> has_greatest_postfixpoint (u \<circ> h) \<and> has_greatest_postfixpoint (h \<circ> g) \<and> has_greatest_fixpoint (g \<circ> h) \<and> g \<circ> h \<circ> u \<le>\<le> u \<circ> h \<circ> g"
  hence "(g \<circ> h) \<circ> u \<le>\<le> u \<circ> (h \<circ> g)"
    by (metis o_assoc)
  hence "\<nu>(g \<circ> h) \<le> u(\<nu>(h \<circ> g))" using 1
    by (metis greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def nu_fusion_2 o_apply)
  also have "... = (u \<circ> h) (\<nu>(g \<circ> h))" using 1
    by (metis greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def nu_roll o_apply)
  finally have "\<nu>(g \<circ> h) \<le> p\<nu>(u \<circ> h)" using 1
    using greatest_postfixpoint is_greatest_postfixpoint_def by blast
  thus "\<nu>(g \<circ> h) \<le> \<nu>(u \<circ> h)" using 1
    using galois_char greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def by auto
qed

lemma nu_exchange_2: "galois l u \<and> isotone g \<and> isotone h \<and> has_greatest_postfixpoint (u \<circ> h) \<and> has_greatest_postfixpoint (h \<circ> u) \<and> has_greatest_postfixpoint (h \<circ> g) \<and> has_greatest_fixpoint (g \<circ> h) \<and> has_greatest_fixpoint (h \<circ> g) \<and> g \<circ> h \<circ> u \<le>\<le> u \<circ> h \<circ> g \<longrightarrow> \<nu>(h \<circ> g) \<le> \<nu>(h \<circ> u)"
proof
  assume 1: "galois l u \<and> isotone g \<and> isotone h \<and> has_greatest_postfixpoint (u \<circ> h) \<and> has_greatest_postfixpoint (h \<circ> u) \<and> has_greatest_postfixpoint (h \<circ> g) \<and> has_greatest_fixpoint (g \<circ> h) \<and> has_greatest_fixpoint (h \<circ> g) \<and> g \<circ> h \<circ> u \<le>\<le> u \<circ> h \<circ> g"
  have "\<nu>(h \<circ> g) = h(\<nu>(g \<circ> h))" using 1
    using nu_roll by blast
  also have "... \<le> h(\<nu>(u \<circ> h))" using 1
    using isotone_def nu_exchange_1 by blast
  also have "... = \<nu>(h \<circ> u)" using 1
    by (metis (no_types, lifting) galois_char greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def nu_roll o_apply)
  finally show "\<nu>(h \<circ> g) \<le> \<nu>(h \<circ> u)"
    .
qed

lemma nu_exchange_equal: "galois l u \<and> galois k t \<and> isotone h \<and> has_greatest_postfixpoint (u \<circ> h) \<and> has_greatest_postfixpoint (h \<circ> u) \<and> has_greatest_postfixpoint (t \<circ> h) \<and> has_greatest_postfixpoint (h \<circ> t) \<and> u \<circ> h \<circ> t = t \<circ> h \<circ> u \<longrightarrow> \<nu>(u \<circ> h) = \<nu>(t \<circ> h) \<and> \<nu>(h \<circ> u) = \<nu>(h \<circ> t)"
  using antisym galois_char greatest_fixpoint_char greatest_postfixpoint_fixpoint isotone_def lifted_reflexive nu_exchange_1 nu_exchange_2 by auto

lemma mu_commute_fixpoint_1: "isotone f \<and> has_least_fixpoint (f \<circ> g) \<and> f \<circ> g = g \<circ> f \<longrightarrow> is_fixpoint f (\<mu>(f \<circ> g))"
  by (metis is_fixpoint_def mu_roll)

lemma mu_commute_fixpoint_2: "isotone g \<and> has_least_fixpoint (f \<circ> g) \<and> f \<circ> g = g \<circ> f \<longrightarrow> is_fixpoint g (\<mu>(f \<circ> g))"
  by (metis is_fixpoint_def mu_roll)

lemma mu_commute_least_fixpoint: "isotone f \<and> isotone g \<and> has_least_fixpoint f \<and> has_least_fixpoint g \<and> has_least_fixpoint (f \<circ> g) \<and> f \<circ> g = g \<circ> f \<longrightarrow> (\<mu>(f \<circ> g) = \<mu> f \<longrightarrow> \<mu> g \<le> \<mu> f)"
  by (metis is_least_fixpoint_def least_fixpoint_same least_fixpoint_unique mu_roll)

(* converse claimed by [Davey & Priestley 2002, page 200, exercise 8.27(iii)] for continuous f, g on a CPO ; does it hold without additional assumptions?
lemma mu_commute_least_fixpoint_converse: "isotone f \<and> isotone g \<and> has_least_prefixpoint f \<and> has_least_prefixpoint g \<and> has_least_prefixpoint (f \<circ> g) \<and> f \<circ> g = g \<circ> f \<longrightarrow> (\<mu> g \<le> \<mu> f \<longrightarrow> \<mu>(f \<circ> g) = \<mu> f)"
*)

lemma nu_commute_fixpoint_1: "isotone f \<and> has_greatest_fixpoint (f \<circ> g) \<and> f \<circ> g = g \<circ> f \<longrightarrow> is_fixpoint f (\<nu>(f \<circ> g))"
  by (metis is_fixpoint_def nu_roll)

lemma nu_commute_fixpoint_2: "isotone g \<and> has_greatest_fixpoint (f \<circ> g) \<and> f \<circ> g = g \<circ> f \<longrightarrow> is_fixpoint g (\<nu>(f \<circ> g))"
  by (metis is_fixpoint_def nu_roll)

lemma nu_commute_greatest_fixpoint: "isotone f \<and> isotone g \<and> has_greatest_fixpoint f \<and> has_greatest_fixpoint g \<and> has_greatest_fixpoint (f \<circ> g) \<and> f \<circ> g = g \<circ> f \<longrightarrow> (\<nu>(f \<circ> g) = \<nu> f \<longrightarrow> \<nu> f \<le> \<nu> g)"
  by (smt is_greatest_fixpoint_def greatest_fixpoint_same greatest_fixpoint_unique nu_roll)

lemma mu_diagonal_1: "isotone (\<lambda>x . f x x) \<and> (\<forall>x . isotone (\<lambda>y . f x y)) \<and> isotone (\<lambda>x . \<mu>(\<lambda>y . f x y)) \<and> (\<forall>x . has_least_fixpoint (\<lambda>y . f x y)) \<and> has_least_prefixpoint (\<lambda>x . \<mu>(\<lambda>y . f x y)) \<longrightarrow> \<mu>(\<lambda>x . f x x) = \<mu>(\<lambda>x . \<mu>(\<lambda>y . f x y))"
  by (smt is_least_fixpoint_def is_least_prefixpoint_def least_fixpoint_same least_fixpoint_unique least_prefixpoint least_prefixpoint_fixpoint)

lemma mu_diagonal_2: "(\<forall>x . isotone (\<lambda>y . f x y) \<and> isotone (\<lambda>y . f y x) \<and> has_least_prefixpoint (\<lambda>y . f x y)) \<and> has_least_prefixpoint (\<lambda>x . \<mu>(\<lambda>y . f x y)) \<longrightarrow> \<mu>(\<lambda>x . f x x) = \<mu>(\<lambda>x . \<mu>(\<lambda>y . f x y))"
proof
  assume 1: "(\<forall>x . isotone (\<lambda>y . f x y) \<and> isotone (\<lambda>y . f y x) \<and> has_least_prefixpoint (\<lambda>y . f x y)) \<and> has_least_prefixpoint (\<lambda>x . \<mu>(\<lambda>y . f x y))"
  hence "isotone (\<lambda>x . \<mu>(\<lambda>y . f x y))"
    by (smt isotone_def lifted_less_eq_def mu_isotone)
  thus "\<mu>(\<lambda>x . f x x) = \<mu>(\<lambda>x . \<mu>(\<lambda>y . f x y))" using 1
    by (smt is_least_fixpoint_def is_least_prefixpoint_def least_fixpoint_same least_prefixpoint least_prefixpoint_fixpoint)
qed

lemma nu_diagonal_1: "isotone (\<lambda>x . f x x) \<and> (\<forall>x . isotone (\<lambda>y . f x y)) \<and> isotone (\<lambda>x . \<nu>(\<lambda>y . f x y)) \<and> (\<forall>x . has_greatest_fixpoint (\<lambda>y . f x y)) \<and> has_greatest_postfixpoint (\<lambda>x . \<nu>(\<lambda>y . f x y)) \<longrightarrow> \<nu>(\<lambda>x . f x x) = \<nu>(\<lambda>x . \<nu>(\<lambda>y . f x y))"
  by (smt is_greatest_fixpoint_def is_greatest_postfixpoint_def greatest_fixpoint_same greatest_fixpoint_unique greatest_postfixpoint greatest_postfixpoint_fixpoint)

lemma nu_diagonal_2: "(\<forall>x . isotone (\<lambda>y . f x y) \<and> isotone (\<lambda>y . f y x) \<and> has_greatest_postfixpoint (\<lambda>y . f x y)) \<and> has_greatest_postfixpoint (\<lambda>x . \<nu>(\<lambda>y . f x y)) \<longrightarrow> \<nu>(\<lambda>x . f x x) = \<nu>(\<lambda>x . \<nu>(\<lambda>y . f x y))"
proof
  assume 1: "(\<forall>x . isotone (\<lambda>y . f x y) \<and> isotone (\<lambda>y . f y x) \<and> has_greatest_postfixpoint (\<lambda>y . f x y)) \<and> has_greatest_postfixpoint (\<lambda>x . \<nu>(\<lambda>y . f x y))"
  hence "isotone (\<lambda>x . \<nu>(\<lambda>y . f x y))"
    by (smt isotone_def lifted_less_eq_def nu_isotone)
  thus "\<nu>(\<lambda>x . f x x) = \<nu>(\<lambda>x . \<nu>(\<lambda>y . f x y))" using 1
    by (smt greatest_fixpoint_same greatest_postfixpoint greatest_postfixpoint_fixpoint is_greatest_fixpoint_def is_greatest_postfixpoint_def)
qed

end

(* Lattice *)

class join_semilattice = plus + ord +
  assumes add_associative: "(x + y) + z = x + (y + z)"
  assumes add_commutative: "x + y = y + x"
  assumes add_idempotent: "x + x = x"
  assumes less_eq_def: "x \<le> y \<longleftrightarrow> x + y = y"
  assumes less_def: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> (y \<le> x)"

begin

subclass order
  apply unfold_locales
  apply (metis less_def)
  apply (metis add_idempotent less_eq_def)
  apply (metis add_associative less_eq_def)
  apply (metis add_commutative less_eq_def)
  done

lemma add_left_isotone: "x \<le> y \<longrightarrow> x + z \<le> y + z"
  by (smt add_associative add_commutative add_idempotent less_eq_def)

lemma add_right_isotone: "x \<le> y \<longrightarrow> z + x \<le> z + y"
  by (metis add_commutative add_left_isotone)

lemma add_isotone: "w \<le> y \<and> x \<le> z \<longrightarrow> w + x \<le> y + z"
  by (smt add_associative add_commutative less_eq_def)

lemma add_left_upper_bound: "x \<le> x + y"
  by (metis add_associative add_idempotent less_eq_def)

lemma add_right_upper_bound: "y \<le> x + y"
  by (metis add_commutative add_left_upper_bound)

lemma add_least_upper_bound: "x \<le> z \<and> y \<le> z \<longleftrightarrow> x + y \<le> z"
  by (smt add_associative add_commutative add_left_upper_bound less_eq_def)

lemma add_left_divisibility: "x \<le> y \<longleftrightarrow> (\<exists>z . x + z = y)"
  by (metis add_left_upper_bound less_eq_def)

lemma add_right_divisibility: "x \<le> y \<longleftrightarrow> (\<exists>z . z + x = y)"
  by (metis add_commutative add_left_divisibility)

lemma add_same_context:"x \<le> y + z \<and> y \<le> x + z \<longrightarrow> x + z = y + z"
  by (smt add_associative add_commutative less_eq_def)

lemma add_relative_same_increasing: "x \<le> y \<and> x + z = x + w \<longrightarrow> y + z = y + w"
  by (smt add_associative add_right_divisibility)

lemma ascending_chain_left_add: "ascending_chain f \<longrightarrow> ascending_chain (\<lambda>n . x + f n)"
  by (metis ascending_chain_def add_right_isotone)

lemma ascending_chain_right_add: "ascending_chain f \<longrightarrow> ascending_chain (\<lambda>n . f n + x)"
  by (metis ascending_chain_def add_left_isotone)

lemma descending_chain_left_add: "descending_chain f \<longrightarrow> descending_chain (\<lambda>n . x + f n)"
  by (metis descending_chain_def add_right_isotone)

lemma descending_chain_right_add: "descending_chain f \<longrightarrow> descending_chain (\<lambda>n . f n + x)"
  by (metis descending_chain_def add_left_isotone)

primrec pSum0 :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
  where "pSum0 f 0 = f 0"
      | "pSum0 f (Suc m) = pSum0 f m + f m"

lemma pSum0_below: "(\<forall>i . f i \<le> x) \<longrightarrow> pSum0 f m \<le> x"
  apply (induct m)
  apply (metis pSum0.simps(1))
  by (metis add_least_upper_bound pSum0.simps(2))

end

class bounded_join_semilattice = join_semilattice + zero +
  assumes add_left_zero: "0 + x = x"

begin

lemma add_right_zero: "x + 0 = x"
  by (metis add_commutative add_left_zero)

lemma zero_least: "0 \<le> x"
  by (metis add_left_upper_bound add_left_zero)

end

class meet =
  fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<frown>" 65)

class meet_semilattice = meet + ord +
  assumes meet_associative: "(x \<frown> y) \<frown> z = x \<frown> (y \<frown> z)"
  assumes meet_commutative: "x \<frown> y = y \<frown> x"
  assumes meet_idempotent: "x \<frown> x = x"
  assumes meet_less_eq_def: "x \<le> y \<longleftrightarrow> x \<frown> y = x"
  assumes meet_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> (y \<le> x)"

sublocale meet_semilattice < meet!: join_semilattice where plus = meet and less_eq = "(\<lambda>x y . y \<le> x)" and less = "(\<lambda>x y . y < x)"
  apply unfold_locales
  apply (rule meet_associative)
  apply (rule meet_commutative)
  apply (rule meet_idempotent)
  apply (metis meet_commutative meet_less_eq_def)
  apply (metis meet_less_def)
  done

class T =
  fixes T :: "'a" ("\<top>")

class bounded_meet_semilattice = meet_semilattice + T +
  assumes meet_left_top: "T \<frown> x = x"

sublocale bounded_meet_semilattice < meet!: bounded_join_semilattice where plus = meet and less_eq = "(\<lambda>x y . y \<le> x)" and less = "(\<lambda>x y . y < x)" and zero = T
  apply unfold_locales
  apply (rule meet_left_top)
  done

class bounded_distributive_lattice = bounded_join_semilattice + bounded_meet_semilattice +
  assumes meet_left_dist_add: "x \<frown> (y + z) = (x \<frown> y) + (x \<frown> z)"
  assumes add_left_dist_meet: "x + (y \<frown> z) = (x + y) \<frown> (x + z)"
  assumes meet_absorb: "x \<frown> (x + y) = x"
  assumes add_absorb: "x + (x \<frown> y) = x"

begin

lemma meet_left_zero: "0 \<frown> x = 0"
  by (metis add_absorb add_left_zero)

lemma meet_right_zero: "x \<frown> 0 = 0"
  by (metis meet_commutative meet_left_zero)

lemma add_left_top_1: "T + x = T"
  by (metis add_absorb meet_left_top)

lemma add_right_top_1: "x + T = T"
  by (metis add_commutative add_left_top_1)

lemma meet_same_context:"x \<le> y \<frown> z \<and> y \<le> x \<frown> z \<longrightarrow> x \<frown> z = y \<frown> z"
  by (metis eq_iff meet.add_least_upper_bound)

lemma relative_equality: "x + z = y + z \<and> x \<frown> z = y \<frown> z \<longrightarrow> x = y"
  by (metis add_absorb add_commutative add_left_dist_meet)

end

(* Semiring *)

class monoid = mult + one +
  assumes mult_associative: "(x ; y) ; z = x ; (y ; z)"
  assumes mult_left_one_1: "1 ; x = x"
  assumes mult_right_one: "x ; 1 = x"

class non_associative_left_semiring = bounded_join_semilattice + mult + one +
  assumes mult_left_sub_dist_add: "x ; y + x ; z \<le> x ; (y + z)"
  assumes mult_right_dist_add: "(x + y) ; z = x ; z + y ; z"
  assumes mult_left_zero: "0 ; x = 0"
  assumes mult_left_one: "1 ; x = x"
  assumes mult_sub_right_one: "x \<le> x ; 1"

begin

lemma mult_left_isotone: "x \<le> y \<longrightarrow> x ; z \<le> y ; z"
  by (metis less_eq_def mult_right_dist_add)

lemma mult_right_isotone: "x \<le> y \<longrightarrow> z ; x \<le> z ; y"
  by (metis add_least_upper_bound less_eq_def mult_left_sub_dist_add)

lemma mult_isotone: "w \<le> y \<and> x \<le> z \<longrightarrow> w ; x \<le> y ; z"
  by (metis mult_left_isotone mult_right_isotone order_trans)

lemma affine_isotone: "isotone (\<lambda>x . y ; x + z)"
  by (smt add_commutative add_right_isotone isotone_def mult_right_isotone)

lemma mult_left_sub_dist_add_left: "x ; y \<le> x ; (y + z)"
  by (metis add_left_upper_bound mult_right_isotone)

lemma mult_left_sub_dist_add_right: "x ; z \<le> x ; (y + z)"
  by (metis add_right_upper_bound mult_right_isotone)

lemma mult_right_sub_dist_add_left: "x ; z \<le> (x + y) ; z"
  by (metis add_left_upper_bound mult_right_dist_add)

lemma mult_right_sub_dist_add_right: "y ; z \<le> (x + y) ; z"
  by (metis add_right_upper_bound mult_right_dist_add)

lemma case_split_left: "1 \<le> w + z \<and> w ; x \<le> y \<and> z ; x \<le> y \<longrightarrow> x \<le> y"
  by (smt add_associative add_commutative less_eq_def mult_left_one mult_right_dist_add order_refl)

lemma case_split_left_equal: "w + z = 1 \<and> w ; x = w ; y \<and> z ; x = z ; y \<longrightarrow> x = y"
  by (metis mult_left_one mult_right_dist_add)

lemma ascending_chain_left_mult: "ascending_chain f \<longrightarrow> ascending_chain (\<lambda>n . x ; f n)"
  by (metis ascending_chain_def mult_right_isotone)

lemma ascending_chain_right_mult: "ascending_chain f \<longrightarrow> ascending_chain (\<lambda>n . f n ; x)"
  by (metis ascending_chain_def mult_left_isotone)

lemma descending_chain_left_mult: "descending_chain f \<longrightarrow> descending_chain (\<lambda>n . x ; f n)"
  by (metis descending_chain_def mult_right_isotone)

lemma descending_chain_right_mult: "descending_chain f \<longrightarrow> descending_chain (\<lambda>n . f n ; x)"
  by (metis descending_chain_def mult_left_isotone)

-- {* Theorem 5 *}

abbreviation Lf :: "'a \<Rightarrow> ('a \<Rightarrow> 'a)" where "Lf y \<equiv> (\<lambda> x . 1 + x ; y)"
abbreviation Rf :: "'a \<Rightarrow> ('a \<Rightarrow> 'a)" where "Rf y \<equiv> (\<lambda> x . 1 + y ; x)"
abbreviation Sf :: "'a \<Rightarrow> ('a \<Rightarrow> 'a)" where "Sf y \<equiv> (\<lambda> x . 1 + y + x ; x)"

abbreviation lstar :: "'a \<Rightarrow> 'a" where "lstar y \<equiv> p\<mu> (Lf y)"
abbreviation rstar :: "'a \<Rightarrow> 'a" where "rstar y \<equiv> p\<mu> (Rf y)"
abbreviation sstar :: "'a \<Rightarrow> 'a" where "sstar y \<equiv> p\<mu> (Sf y)"

lemma lstar_rec_isotone: "isotone (Lf y)"
  by (smt add_isotone add_right_divisibility isotone_def mult_right_sub_dist_add_right order.refl)

lemma rstar_rec_isotone: "isotone (Rf y)"
  by (metis add_isotone isotone_def less_eq_def mult_left_sub_dist_add_left order_refl)

lemma sstar_rec_isotone: "isotone (Sf y)"
  by (simp add: add_right_isotone isotone_def mult_isotone)

lemma lstar_fixpoint: "has_least_prefixpoint (Lf y) \<longrightarrow> lstar y = \<mu> (Lf y)"
  by (metis pmu_mu lstar_rec_isotone)

lemma rstar_fixpoint: "has_least_prefixpoint (Rf y) \<longrightarrow> rstar y = \<mu> (Rf y)"
  by (metis pmu_mu rstar_rec_isotone)

lemma sstar_fixpoint: "has_least_prefixpoint (Sf y) \<longrightarrow> sstar y = \<mu> (Sf y)"
  by (metis pmu_mu sstar_rec_isotone)

lemma sstar_increasing: "has_least_prefixpoint (Sf y) \<longrightarrow> y \<le> sstar y"
  by (metis add_least_upper_bound add_left_upper_bound order.trans pmu_unfold)

-- {* Theorem 5 part 2 *}

lemma rstar_below_sstar: "has_least_prefixpoint (Rf y) \<and> has_least_prefixpoint (Sf y) \<longrightarrow> rstar y \<le> sstar y"
proof
  assume 1: "has_least_prefixpoint (Rf y) \<and> has_least_prefixpoint (Sf y)"
  hence "Rf y (sstar y) \<le> Sf y (sstar y)"
    by (smt add_isotone add_left_upper_bound add_right_upper_bound dual_order.trans mult_left_isotone pmu_unfold)
  also have "... \<le> sstar y" using 1
    by (metis (erased, lifting) pmu_unfold)
  finally show "rstar y \<le> sstar y" using 1
    by (metis (erased, lifting) is_least_prefixpoint_def least_prefixpoint)
qed

end

class pre_left_semiring = non_associative_left_semiring +
  assumes mult_semi_associative: "(x ; y) ; z \<le> x ; (y ; z)"

begin

lemma mult_one_associative: "x ; 1 ; y = x ; y"
  by (metis dual_order.antisym mult_left_isotone mult_left_one mult_semi_associative mult_sub_right_one)

lemma mult_sup_associative_one: "(x ; (y ; 1)) ; z \<le> x ; (y ; z)"
  by (metis mult_semi_associative mult_one_associative)

lemma rstar_increasing: "has_least_prefixpoint (Rf y) \<longrightarrow> y \<le> rstar y"
proof
  assume "has_least_prefixpoint (Rf y)"
  hence "Rf y (rstar y) \<le> rstar y"
    by (metis pmu_unfold)
  thus "y \<le> rstar y"
    by (metis add_least_upper_bound mult_right_isotone mult_sub_right_one order.trans)
qed

end

class residuated_pre_left_semiring = pre_left_semiring + inverse +
  assumes lres_galois: "x ; y \<le> z \<longleftrightarrow> x \<le> z / y"

begin

lemma lres_left_isotone: "x \<le> y \<longrightarrow> x / z \<le> y / z"
  by (metis lres_galois order.refl order.trans)

lemma lres_right_antitone: "x \<le> y \<longrightarrow> z / y \<le> z / x"
  by (metis lres_galois mult_right_isotone order.refl order_trans)

lemma lres_inverse: "(x / y) ; y \<le> x"
  by (metis lres_galois order_refl)

lemma lres_one: "x / 1 \<le> x"
  by (metis dual_order.trans mult_sub_right_one lres_inverse)

lemma lres_mult_sub_lres_lres: "x / (z ; y) \<le> (x / y) / z"
  by (metis lres_galois lres_inverse mult_semi_associative order.trans)

lemma mult_lres_sub_assoc: "x ; (y / z) \<le> (x ; y) / z"
  by (metis (full_types) lres_galois lres_inverse mult_right_isotone mult_semi_associative order_trans)

-- {* Theorem 5 part 1 *}

lemma lstar_below_rstar: "has_least_prefixpoint (Lf y) \<and> has_least_prefixpoint (Rf y) \<longrightarrow> lstar y \<le> rstar y"
proof
  assume 1: "has_least_prefixpoint (Lf y) \<and> has_least_prefixpoint (Rf y)"
  have "y ; (rstar y / y) ; y \<le> y ; rstar y"
    by (metis mult_right_isotone mult_semi_associative order_trans lres_inverse)
  also have "... \<le> rstar y" using 1
    by (metis add_least_upper_bound pmu_unfold)
  finally have "y ; (rstar y / y) \<le> rstar y / y"
    by (metis lres_galois)
  hence "Rf y (rstar y / y) \<le> rstar y / y" using 1
    by (metis add_least_upper_bound lres_galois mult_left_one rstar_increasing)
  hence "rstar y \<le> rstar y / y" using 1
    by (metis is_least_prefixpoint_def least_prefixpoint)
  hence "Lf y (rstar y) \<le> rstar y" using 1
    by (metis add_least_upper_bound lres_galois pmu_unfold)
  thus "lstar y \<le> rstar y" using 1
    by (metis (erased, lifting) is_least_prefixpoint_def least_prefixpoint)
qed

-- {* Theorem 5 part 3 *}

lemma rstar_sstar: "has_least_prefixpoint (Rf y) \<and> has_least_prefixpoint (Sf y) \<longrightarrow> rstar y = sstar y"
proof
  assume 1: "has_least_prefixpoint (Rf y) \<and> has_least_prefixpoint (Sf y)"
  have "Rf y (rstar y / rstar y) ; rstar y \<le> rstar y + y ; ((rstar y / rstar y) ; rstar y)"
    by (metis add_isotone mult_left_one mult_right_dist_add mult_semi_associative)
  also have "... \<le> rstar y + y ; rstar y"
    by (metis add_right_isotone mult_right_isotone lres_inverse)
  also have "... \<le> rstar y" using 1
    by (metis (full_types) add_least_upper_bound order_refl pmu_unfold)
  finally have "Rf y (rstar y / rstar y) \<le> rstar y / rstar y"
    by (metis lres_galois)
  hence "rstar y ; rstar y \<le> rstar y" using 1
    by (metis (erased, lifting) is_least_prefixpoint_def least_prefixpoint lres_galois)
  hence "y + rstar y ; rstar y \<le> rstar y" using 1
    by (metis add_least_upper_bound rstar_increasing)
  hence "Sf y (rstar y) \<le> rstar y" using 1
    by (metis (full_types) add_least_upper_bound pmu_unfold)
  hence "sstar y \<le> rstar y" using 1
    by (metis (erased, lifting) is_least_prefixpoint_def least_prefixpoint)
  thus "rstar y = sstar y" using 1
    by (metis antisym rstar_below_sstar)
qed

end

class idempotent_left_semiring = non_associative_left_semiring + monoid

begin

subclass pre_left_semiring
  apply unfold_locales
  apply (metis mult_associative order_refl)
  done

lemma zero_right_mult_decreasing: "x ; 0 \<le> x"
  by (metis add_right_zero mult_left_sub_dist_add_right mult_right_one)

lemma test_preserves_equation: "p \<le> p ; p \<and> p \<le> 1 \<longrightarrow> (p ; x \<le> x ; p \<longleftrightarrow> p ; x = p ; x ; p)"
  apply rule
  apply rule
  apply (rule antisym)
  apply (metis antisym mult_associative mult_right_isotone mult_right_one)
  apply (metis mult_right_isotone mult_right_one)
  apply (metis mult_left_isotone mult_left_one)
  done

end

class idempotent_left_zero_semiring = idempotent_left_semiring +
  assumes mult_left_dist_add: "x ; (y + z) = x ; y + x ; z"

begin

lemma case_split_right: "1 \<le> w + z \<and> x ; w \<le> y \<and> x ; z \<le> y \<longrightarrow> x \<le> y"
proof
  assume 1: "1 \<le> w + z \<and> x ; w \<le> y \<and> x ; z \<le> y"
  hence "x \<le> x ; (w + z)"
    by (metis less_eq_def mult_left_dist_add mult_right_one)
  also have "... \<le> y" using 1
    by (smt add_associative less_eq_def mult_left_dist_add)
  finally show "x \<le> y"
    .
qed

lemma case_split_right_equal: "w + z = 1 \<and> x ; w = y ; w \<and> x ; z = y ; z \<longrightarrow> x = y"
  by (metis mult_left_dist_add mult_right_one)

end

class idempotent_semiring = idempotent_left_zero_semiring +
  assumes mult_right_zero: "x ; 0 = 0"

class bounded_pre_left_semiring = pre_left_semiring + T +
  assumes add_right_top: "x + T = T"

begin

lemma add_left_top: "T + x = T"
  by (metis add_commutative add_right_top)

lemma top_greatest: "x \<le> T"
  by (metis add_left_top add_right_upper_bound)

lemma top_left_mult_increasing: "x \<le> T ; x"
  by (metis mult_left_isotone mult_left_one top_greatest)

lemma top_right_mult_increasing: "x \<le> x ; T"
  by (metis order_trans mult_right_isotone mult_sub_right_one top_greatest)

lemma top_mult_top: "T ; T = T"
  by (metis add_right_divisibility add_right_top top_right_mult_increasing)

definition vector :: "'a \<Rightarrow> bool"
  where "vector x \<longleftrightarrow> x = x ; T"

lemma vector_zero: "vector 0"
  by (metis mult_left_zero vector_def)

lemma vector_top: "vector T"
  by (metis top_mult_top vector_def)

lemma vector_add_closed: "vector x \<and> vector y \<longrightarrow> vector (x + y)"
  by (metis mult_right_dist_add vector_def)

lemma vector_left_mult_closed: "vector y \<longrightarrow> vector (x ; y)"
  by (metis antisym mult_semi_associative top_right_mult_increasing vector_def)

end

class bounded_residuated_pre_left_semiring = residuated_pre_left_semiring + bounded_pre_left_semiring

begin

lemma lres_top_decreasing: "x / T \<le> x"
  by (metis lres_one lres_right_antitone order_trans top_greatest)

lemma top_lres_absorb: "T / x = T"
  by (metis eq_iff lres_galois top_greatest)

end

class bounded_idempotent_left_semiring = bounded_pre_left_semiring + idempotent_left_semiring

class bounded_idempotent_left_zero_semiring = bounded_idempotent_left_semiring + idempotent_left_zero_semiring

class bounded_idempotent_semiring = bounded_idempotent_left_zero_semiring + idempotent_semiring

(* BooleanAlgebra *)

notation
  sup (infixl "\<squnion>" 65) and
  inf (infixl "\<sqinter>" 69) and
  uminus ("_ '" [80] 80)

context order

begin

lemma order_lesseq_imp: "(\<forall>z . x \<le> z \<longrightarrow> y \<le> z) \<longleftrightarrow> y \<le> x"
  using order_trans by blast

end

context semilattice_sup

begin

lemma sup_left_isotone: "x \<le> y \<longrightarrow> x \<squnion> z \<le> y \<squnion> z"
  using sup.mono by blast

lemma sup_right_isotone: "x \<le> y \<longrightarrow> z \<squnion> x \<le> z \<squnion> y"
  using sup.mono by blast

lemma sup_isotone: "w \<le> y \<and> x \<le> z \<longrightarrow> w \<squnion> x \<le> y \<squnion> z"
  using sup.mono by blast

lemma sup_least_upper_bound: "x \<le> z \<and> y \<le> z \<longleftrightarrow> x \<squnion> y \<le> z"
  by simp

lemma sup_left_divisibility: "x \<le> y \<longleftrightarrow> (\<exists>z . x \<squnion> z = y)"
  using sup.absorb2 sup.cobounded1 by blast

lemma sup_right_divisibility: "x \<le> y \<longleftrightarrow> (\<exists>z . z \<squnion> x = y)"
  by (metis sup.cobounded2 sup.orderE)

lemma sup_same_context:"x \<le> y \<squnion> z \<and> y \<le> x \<squnion> z \<longrightarrow> x \<squnion> z = y \<squnion> z"
  by (metis (full_types) sup.orderE sup_assoc sup_commute)

lemma sup_relative_same_increasing: "x \<le> y \<and> x \<squnion> z = x \<squnion> w \<longrightarrow> y \<squnion> z = y \<squnion> w"
  using sup_assoc sup_commute sup_left_divisibility by auto

end

sublocale bounded_semilattice_inf_top < inf!: bounded_semilattice_sup_bot where sup = inf and less_eq = "(\<lambda>x y . y \<le> x)" and less = "(\<lambda>x y . y < x)" and bot = top
  apply unfold_locales
  apply simp_all
  apply (simp add: less_le_not_le)
  done

context semilattice_inf

begin

lemma inf_same_context:"x \<le> y \<sqinter> z \<and> y \<le> x \<sqinter> z \<longrightarrow> x \<sqinter> z = y \<sqinter> z"
  by (metis inf.absorb2 inf.boundedE inf.orderE)

end

context distrib_lattice

begin

lemma relative_equality: "x \<squnion> z = y \<squnion> z \<and> x \<sqinter> z = y \<sqinter> z \<longrightarrow> x = y"
  by (metis inf.commute inf_sup_absorb inf_sup_distrib1)

end

context boolean_algebra

begin

-- {* We follow Roger Maddux's 1996 paper.

Maddux Axioms
(Ba1) @{text sup_assoc}
(Ba2) @{text sup_commute}

Maddux Theorem 3
(ii) @{text double_compl}
(vi) @{text sup_idem}
(vii) @{text inf_idem}
(viii) @{text inf_commute}
(ix) @{text inf_assoc}
(xiv) @{text sup_inf_absorb}
(xv) @{text inf_sup_distrib1}
(xvi) @{text compl_sup}
(xvii) @{text compl_inf}
(xviii) @{text sup_inf_distrib1}

Maddux Theorem 5
(i) @{text sup_compl_top}
(ii) @{text inf_compl_bot}
(iii) @{text compl_top_eq}
(iv) @{text compl_bot_eq}
(v) @{text sup_top_right}
(vi) @{text inf_bot_right}
(vii) @{text sup_bot_right}
(viii) @{text inf_top_right}

*}

lemma compl_le_swap1_iff: "x \<le> -y \<longleftrightarrow> y \<le> -x"
  using compl_le_swap1 by blast

lemma compl_le_swap2_iff: "-x \<le> y \<longleftrightarrow> -y \<le> x"
  using compl_le_swap2 by blast

lemma huntington_3: "x = -(-x \<squnion> -y) \<squnion> -(-x \<squnion> y)"
  by (metis compl_inf compl_inf_bot double_compl sup_bot_right sup_inf_distrib1)

-- {* Maddux Theorem 3 *}

lemma maddux_3_1: "x \<squnion> -x = y \<squnion> -y"
  by (simp add: sup_compl_top)

lemma maddux_3_3: "-x = -(x \<squnion> y) \<squnion> -(x \<squnion> -y)"
  by (metis huntington_3 double_compl)

lemma maddux_3_4: "x \<squnion> (y \<squnion> -y) = z \<squnion> -z"
  by (metis sup_assoc sup_idem maddux_3_1)

lemma maddux_3_5: "x \<squnion> x = x \<squnion> -(y \<squnion> -y)"
  by simp

lemma maddux_3_11: "x = (x \<sqinter> y) \<squnion> (x \<sqinter> -y)"
  by (metis inf_sup_distrib1 inf_top.right_neutral sup_compl_top)

lemma maddux_3_12: "x = (x \<squnion> -y) \<sqinter> (x \<squnion> y)"
  by (metis compl_inf_bot sup_bot.right_neutral sup_inf_distrib1)

lemma maddux_3_13: "(x \<squnion> y) \<sqinter> -x = y \<sqinter> -x"
  by (simp add: inf_compl_bot inf_sup_distrib2)

lemma maddux_3_19: "(-x \<sqinter> y) \<squnion> (x \<sqinter> z) = (x \<squnion> y) \<sqinter> (-x \<squnion> z)"
  by (smt double_compl inf.commute inf_sup_absorb sup_ge1 sup_inf_absorb sup_inf_distrib2 sup_relative_same_increasing maddux_3_11 maddux_3_13)

lemma compl_inter_eq: "x \<sqinter> y = x \<sqinter> z \<and> -x \<sqinter> y = -x \<sqinter> z \<longrightarrow> y = z"
  by (metis inf_commute maddux_3_11)

lemma maddux_3_20: "((v \<sqinter> w) \<squnion> (-v \<sqinter> x)) \<sqinter> -((v \<sqinter> y) \<squnion> (-v \<sqinter> z)) = (v \<sqinter> w \<sqinter> -y) \<squnion> (-v \<sqinter> x \<sqinter> -z)"
proof -
  have 1: "v \<sqinter> (((v \<sqinter> w) \<squnion> (-v \<sqinter> x)) \<sqinter> -((v \<sqinter> y) \<squnion> (-v \<sqinter> z))) = v \<sqinter> w \<sqinter> -y"
    by (smt compl_inf compl_sup double_compl inf.assoc inf.commute sup.left_commute sup_inf_absorb sup_inf_distrib1 maddux_3_13)
  have 2: "... = v \<sqinter> ((v \<sqinter> w \<sqinter> -y) \<squnion> (-v \<sqinter> x \<sqinter> -z))"
    by (smt inf.left_commute inf.orderE inf_bot_right inf_commute inf_compl_bot inf_le1 inf_sup_distrib1 sup_bot.right_neutral)
  have 31: "-v \<sqinter> ((v \<sqinter> w) \<squnion> (-v \<sqinter> x)) = -v \<sqinter> x" using maddux_3_11 maddux_3_13
    by (smt comp_fun_idem.fun_left_idem compl_inf_bot inf.comp_fun_idem_sup inf_bot_right inf_sup_distrib1 sup_inf_absorb)
  have 32: "-v \<sqinter> -((v \<sqinter> y) \<squnion> (-v \<sqinter> z)) = -v \<sqinter> -z" using maddux_3_13
    by (metis compl_sup double_compl inf_commute inf_idem sup_assoc sup_commute sup_inf_absorb sup_inf_distrib1 maddux_3_11)
  have 3: "-v \<sqinter> (((v \<sqinter> w) \<squnion> (-v \<sqinter> x)) \<sqinter> -((v \<sqinter> y) \<squnion> (-v \<sqinter> z))) = -v \<sqinter> x \<sqinter> -z" using 31 32
    by (smt inf_commute inf_left_commute)
  have 4: "... = -v \<sqinter> ((v \<sqinter> w \<sqinter> -y) \<squnion> (-v \<sqinter> x \<sqinter> -z))" using 1 3
    by (smt inf_assoc inf_sup_distrib2 inf_top.right_neutral sup_compl_top)
  show ?thesis using 1 2 3 4
    by (metis compl_inter_eq)
qed

lemma maddux_3_21: "x \<squnion> y = x \<squnion> (-x \<sqinter> y)"
  by (simp add: sup_compl_top sup_inf_distrib1)

-- {* Maddux Theorem 7(v) *}

lemma shunting_1: "x \<le> y \<longleftrightarrow> x \<sqinter> y ' = bot"
  apply rule
  apply (smt compl_inf_bot inf_absorb1 inf_bot_right inf_commute inf_left_commute)
  apply (metis inf_commute inf_sup_distrib1 inf_top_left le_iff_inf sup_commute sup_bot_left sup_compl_top)
  done

lemma shunting_2: "x \<le> y \<longleftrightarrow> x ' \<squnion> y = top"
  by (metis compl_bot_eq compl_inf double_compl shunting_1)

-- {* Maddux Definition 13 *}

definition conjugate :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
  where "conjugate f g \<longleftrightarrow> (\<forall>x y . f x \<sqinter> y = bot \<longleftrightarrow> x \<sqinter> g y = bot)"

-- {* Maddux Theorem 14 *}

lemma conjugate_unique: "conjugate f g \<and> conjugate f h \<longrightarrow> g = h"
proof
  assume "conjugate f g \<and> conjugate f h"
  hence "\<forall>x y . g y \<le> x ' \<longleftrightarrow> h y \<le> x '"
    by (smt double_compl inf_commute shunting_1 conjugate_def)
  hence "\<forall>y . g y = h y"
    by (metis double_compl eq_iff)
  thus "g = h"
    by (metis lifted_antisymmetric lifted_less_eq_def order_refl)
qed

lemma conjugate_symmetric: "conjugate f g \<longrightarrow> conjugate g f"
  by (smt conjugate_def inf_commute)

-- {* Maddux Definition 15(iii) *}

definition additive :: "('a \<Rightarrow> 'a) \<Rightarrow> bool"
  where "additive f \<longleftrightarrow> (\<forall>x y . f (x \<squnion> y) = f x \<squnion> f y)"

-- {* part of Maddux Theorem 17(i) *}

lemma additive_isotone: "additive f \<longrightarrow> isotone f"
  by (metis additive_def isotone_def le_iff_sup)

-- {* part of Maddux Theorem 18(ii) *}

lemma conjugate_additive: "conjugate f g \<longrightarrow> additive f"
proof
  assume 1: "conjugate f g"
  have 2: "\<forall>x y z . f (x \<squnion> y) \<le> z \<longleftrightarrow> f x \<le> z \<and> f y \<le> z"
  proof
    fix x
    show "\<forall>y z . f (x \<squnion> y) \<le> z \<longleftrightarrow> f x \<le> z \<and> f y \<le> z"
    proof
      fix y
      show "\<forall>z . f (x \<squnion> y) \<le> z \<longleftrightarrow> f x \<le> z \<and> f y \<le> z"
      proof
        fix z
        have "(f (x \<squnion> y) \<le> z) = (f (x \<squnion> y) \<sqinter> z ' = bot)"
          by (metis shunting_1)
        also have "... = ((x \<squnion> y) \<sqinter> g(z ') = bot)" using 1
          by (metis conjugate_def)
        also have "... = (x \<squnion> y \<le> (g(z '))')"
          by (metis double_compl shunting_1)
        also have "... = (x \<le> (g(z '))' \<and> y \<le> (g(z '))')"
          by (metis le_sup_iff)
        also have "... = (x \<sqinter> g(z ') = bot \<and> y \<sqinter> g(z ') = bot)"
          by (metis double_compl shunting_1)
        also have "... = (f x \<sqinter> z ' = bot \<and> f y \<sqinter> z ' = bot)" using 1
          by (metis conjugate_def)
        also have "... = (f x \<le> z \<and> f y \<le> z)"
          by (metis shunting_1)
        finally show "f (x \<squnion> y) \<le> z \<longleftrightarrow> f x \<le> z \<and> f y \<le> z"
          by metis
      qed
    qed
  qed
  have "\<forall>x y . f (x \<squnion> y) = f x \<squnion> f y"
  proof
    fix x
    show "\<forall>y . f (x \<squnion> y) = f x \<squnion> f y"
    proof
      fix y
      have "f(x \<squnion> y) \<le> f(x) \<squnion> f(y)" using 2
        by (metis sup_ge1 sup_ge2)
      thus "f (x \<squnion> y) = f x \<squnion> f y" using 2
        by (metis le_supI order_refl antisym)
    qed
  qed
  thus "additive f"
    by (metis additive_def)
qed

lemma conjugate_isotone: "conjugate f g \<longrightarrow> isotone f"
  by (metis additive_isotone conjugate_additive)

-- {* Maddux Theorem 19 *}

lemma conjugate_char_1: "conjugate f g \<longleftrightarrow> (\<forall>x y . f(x \<sqinter> (g y)') \<le> f x \<sqinter> y ' \<and> g(y \<sqinter> (f x)') \<le> g y \<sqinter> x ')"
proof
  assume 1: "conjugate f g"
  show "\<forall>x y . f(x \<sqinter> (g y)') \<le> f x \<sqinter> y ' \<and> g(y \<sqinter> (f x)') \<le> g y \<sqinter> x '"
  proof
    fix x
    show "\<forall>y . f(x \<sqinter> (g y)') \<le> f x \<sqinter> y ' \<and> g(y \<sqinter> (f x)') \<le> g y \<sqinter> x '"
    proof
      fix y
      have "f(x \<sqinter> (g y)') \<le> y '" using 1
        by (smt compl_inf_bot conjugate_def double_compl inf_assoc inf_bot_right shunting_1)
      hence 2: "f(x \<sqinter> (g y)') \<le> f x \<sqinter> y '" using 1
        by (metis conjugate_isotone inf_le1 isotone_def le_inf_iff)
      have "g(y \<sqinter> (f x)') \<le> x '" using 1
        by (smt compl_inf_bot conjugate_def double_compl inf_assoc inf_bot_right shunting_1 inf_commute)
      hence "g(y \<sqinter> (f x)') \<le> g y \<sqinter> x '" using 1
        by (metis conjugate_isotone inf_le1 isotone_def le_inf_iff conjugate_symmetric)
      thus "f(x \<sqinter> (g y)') \<le> f x \<sqinter> y ' \<and> g(y \<sqinter> (f x)') \<le> g y \<sqinter> x '" using 2
        by metis
    qed
  qed
next
  assume 2: "\<forall>x y . f(x \<sqinter> (g y)') \<le> f x \<sqinter> y ' \<and> g(y \<sqinter> (f x)') \<le> g y \<sqinter> x '"
  hence 3: "\<forall>x y . f x \<sqinter> y = bot \<longrightarrow> x \<sqinter> g y = bot"
    by (smt double_compl inf_commute inf_le2 le_iff_inf shunting_1)
  have "\<forall>x y . x \<sqinter> g y = bot \<longrightarrow> f x \<sqinter> y = bot" using 2
    by (smt double_compl inf_commute inf_le2 le_iff_inf shunting_1)
  thus "conjugate f g" using 3
    by (metis conjugate_def)
qed

lemma conjugate_char_2: "conjugate f g \<longleftrightarrow> f bot = bot \<and> g bot = bot \<and> (\<forall>x y . f x \<sqinter> y \<le> f(x \<sqinter> g y) \<and> g y \<sqinter> x \<le> g(y \<sqinter> f x))"
proof
  assume 1: "conjugate f g"
  show "f bot = bot \<and> g bot = bot \<and> (\<forall>x y . f x \<sqinter> y \<le> f(x \<sqinter> g y) \<and> g y \<sqinter> x \<le> g(y \<sqinter> f x))"
  proof
    show "f bot = bot" using 1
      by (metis conjugate_def inf_idem inf_bot_left)
  next
    show "g bot = bot \<and> (\<forall>x y . f x \<sqinter> y \<le> f(x \<sqinter> g y) \<and> g y \<sqinter> x \<le> g(y \<sqinter> f x))"
    proof
      show "g bot = bot" using 1
        by (metis conjugate_def inf_idem inf_bot_right)
    next
      show "\<forall>x y . f x \<sqinter> y \<le> f(x \<sqinter> g y) \<and> g y \<sqinter> x \<le> g(y \<sqinter> f x)"
      proof
        fix x
        show "\<forall>y . f x \<sqinter> y \<le> f(x \<sqinter> g y) \<and> g y \<sqinter> x \<le> g(y \<sqinter> f x)"
        proof
          fix y
          show "f x \<sqinter> y \<le> f(x \<sqinter> g y) \<and> g y \<sqinter> x \<le> g(y \<sqinter> f x)"
          proof
            have "f x \<sqinter> y = (f(x \<sqinter> g y) \<squnion> f(x \<sqinter> (g y)')) \<sqinter> y" using 1
              by (metis additive_def conjugate_additive inf_sup_distrib1 inf_top_right sup_compl_top)
            also have "... \<le> (f(x \<sqinter> g y) \<squnion> (f x \<sqinter> y ')) \<sqinter> y" using 1
              by (metis conjugate_char_1 inf_mono order_refl sup_mono)
            also have "... \<le> f(x \<sqinter> g y)"
              by (smt inf_idem inf_assoc inf_commute inf_compl_bot inf_sup_distrib1 le_iff_inf sup_commute sup_bot_left)
            finally show "f x \<sqinter> y \<le> f(x \<sqinter> g y)"
              by metis
          next
            have "g y \<sqinter> x = (g(y \<sqinter> f x) \<squnion> g(y \<sqinter> (f x)')) \<sqinter> x" using 1
              by (metis additive_def conjugate_additive conjugate_symmetric inf_sup_distrib1 inf_top_right sup_compl_top)
            also have "... \<le> (g(y \<sqinter> f x) \<squnion> (g y \<sqinter> x ')) \<sqinter> x" using 1
              by (metis conjugate_char_1 inf_mono order_refl sup_mono)
            also have "... \<le> g(y \<sqinter> f x)"
              by (smt inf_idem inf_assoc inf_commute inf_compl_bot inf_sup_distrib1 le_iff_inf sup_commute sup_bot_left)
            finally show "g y \<sqinter> x \<le> g(y \<sqinter> f x)"
              by metis
          qed
        qed
      qed
    qed
  qed
next
  assume "f bot = bot \<and> g bot = bot \<and> (\<forall>x y . f x \<sqinter> y \<le> f(x \<sqinter> g y) \<and> g y \<sqinter> x \<le> g(y \<sqinter> f x))"
  thus "conjugate f g"
    by (smt conjugate_def inf_commute le_bot)
qed

end

(* LatticeOrderedSemiring *)

-- {* M0-algebra *}

class lattice_ordered_pre_left_semiring = pre_left_semiring + bounded_distributive_lattice

begin

subclass bounded_pre_left_semiring
  apply unfold_locales
  apply (metis add_right_top_1)
  done

lemma top_mult_right_one: "x ; T = x ; T ; 1"
  by (metis add_commutative add_left_top less_eq_def mult_semi_associative mult_sub_right_one)

lemma mult_left_sub_dist_meet_left: "x ; (y \<frown> z) \<le> x ; y"
  by (metis meet.add_left_upper_bound mult_right_isotone)

lemma mult_left_sub_dist_meet_right: "x ; (y \<frown> z) \<le> x ; z"
  by (metis meet_commutative mult_left_sub_dist_meet_left)

lemma mult_right_sub_dist_meet_left: "(x \<frown> y) ; z \<le> x ; z"
  by (metis meet.add_left_upper_bound mult_left_isotone)

lemma mult_right_sub_dist_meet_right: "(x \<frown> y) ; z \<le> y ; z"
  by (metis meet.add_right_upper_bound mult_left_isotone)

lemma mult_right_sub_dist_meet: "(x \<frown> y) ; z \<le> x ; z \<frown> y ; z"
  by (metis meet.add_least_upper_bound mult_right_sub_dist_meet_left mult_right_sub_dist_meet_right)

-- {* Figure 1: fundamental properties *}

definition total             :: "'a \<Rightarrow> bool" where "total x \<longleftrightarrow> x ; T = T"
definition co_total          :: "'a \<Rightarrow> bool" where "co_total x \<longleftrightarrow> x ; 0 = 0"
definition transitive        :: "'a \<Rightarrow> bool" where "transitive x \<longleftrightarrow> x ; x \<le> x"
definition dense             :: "'a \<Rightarrow> bool" where "dense x \<longleftrightarrow> x \<le> x ; x"
definition reflexive         :: "'a \<Rightarrow> bool" where "reflexive x \<longleftrightarrow> 1 \<le> x"
definition co_reflexive      :: "'a \<Rightarrow> bool" where "co_reflexive x \<longleftrightarrow> x \<le> 1"
definition idempotent        :: "'a \<Rightarrow> bool" where "idempotent x \<longleftrightarrow> x ; x = x"
definition up_closed         :: "'a \<Rightarrow> bool" where "up_closed x \<longleftrightarrow> x ; 1 = x"
definition add_distributive  :: "'a \<Rightarrow> bool" where "add_distributive x \<longleftrightarrow> (\<forall>y z . x ; (y + z) = x ; y + x ; z)"
definition meet_distributive :: "'a \<Rightarrow> bool" where "meet_distributive x \<longleftrightarrow> (\<forall>y z . x ; (y \<frown> z) = x ; y \<frown> x ; z)"
definition contact           :: "'a \<Rightarrow> bool" where "contact x \<longleftrightarrow> x ; x + 1 = x"
definition kernel            :: "'a \<Rightarrow> bool" where "kernel x \<longleftrightarrow> x ; x \<frown> 1 = x ; 1"
definition add_dist_contact  :: "'a \<Rightarrow> bool" where "add_dist_contact x \<longleftrightarrow> add_distributive x \<and> contact x"
definition meet_dist_kernel  :: "'a \<Rightarrow> bool" where "meet_dist_kernel x \<longleftrightarrow> meet_distributive x \<and> kernel x"
definition test              :: "'a \<Rightarrow> bool" where "test x \<longleftrightarrow> x ; T \<frown> 1 = x"
definition co_test           :: "'a \<Rightarrow> bool" where "co_test x \<longleftrightarrow> x ; 0 + 1 = x"
definition co_vector         :: "'a \<Rightarrow> bool" where "co_vector x \<longleftrightarrow> x ; 0 = x"

-- {* Theorem 6 / Figure 2: relations between properties *}

lemma reflexive_total: "reflexive x \<longrightarrow> total x"
  by (metis eq_iff mult_isotone mult_left_one meet.zero_least reflexive_def total_def)

lemma reflexive_dense: "reflexive x \<longrightarrow> dense x"
  by (metis mult_left_isotone mult_left_one reflexive_def dense_def)

lemma reflexive_transitive_up_closed: "reflexive x \<and> transitive x \<longrightarrow> up_closed x"
  by (metis antisym_conv mult_isotone mult_sub_right_one reflexive_def reflexive_dense transitive_def dense_def up_closed_def)

lemma co_reflexive_co_total: "co_reflexive x \<longrightarrow> co_total x"
  by (metis co_reflexive_def co_total_def eq_iff mult_left_isotone mult_left_one zero_least)

lemma co_reflexive_transitive: "co_reflexive x \<longrightarrow> transitive x"
  by (metis co_reflexive_def mult_left_isotone mult_left_one transitive_def)

lemma idempotent_transitive_dense: "idempotent x \<longleftrightarrow> transitive x \<and> dense x"
  by (metis eq_iff transitive_def dense_def idempotent_def)

lemma contact_reflexive: "contact x \<longrightarrow> reflexive x"
  by (metis contact_def add_right_upper_bound reflexive_def)

lemma contact_transitive: "contact x \<longrightarrow> transitive x"
  by (metis contact_def add_left_upper_bound transitive_def)

lemma contact_dense: "contact x \<longrightarrow> dense x"
  by (metis contact_reflexive reflexive_dense)

lemma contact_idempotent: "contact x \<longrightarrow> idempotent x"
  by (metis contact_transitive contact_dense idempotent_transitive_dense)

lemma contact_up_closed: "contact x \<longrightarrow> up_closed x"
  by (metis contact_def contact_idempotent dual_order.antisym mult_left_sub_dist_add_right mult_sub_right_one idempotent_def up_closed_def)

lemma contact_reflexive_idempotent_up_closed: "contact x \<longleftrightarrow> reflexive x \<and> idempotent x \<and> up_closed x"
  by (metis contact_def contact_idempotent contact_up_closed add_commutative less_eq_def reflexive_def idempotent_def)

lemma kernel_co_reflexive: "kernel x \<longrightarrow> co_reflexive x"
  by (metis co_reflexive_def kernel_def meet.add_least_upper_bound mult_sub_right_one)

lemma kernel_transitive: "kernel x \<longrightarrow> transitive x"
  by (metis co_reflexive_transitive kernel_co_reflexive)

lemma kernel_dense: "kernel x \<longrightarrow> dense x"
  by (metis kernel_def meet.add_least_upper_bound mult_sub_right_one dense_def)

lemma kernel_idempotent: "kernel x \<longrightarrow> idempotent x"
  by (metis kernel_transitive kernel_dense idempotent_transitive_dense)

lemma kernel_up_closed: "kernel x \<longrightarrow> up_closed x"
  by (metis co_reflexive_def kernel_co_reflexive kernel_def kernel_idempotent meet_less_eq_def idempotent_def up_closed_def)

lemma kernel_co_reflexive_idempotent_up_closed: "kernel x \<longleftrightarrow> co_reflexive x \<and> idempotent x \<and> up_closed x"
  by (metis co_reflexive_def kernel_def kernel_idempotent kernel_up_closed meet.less_eq_def meet_commutative idempotent_def up_closed_def)

lemma test_co_reflexive: "test x \<longrightarrow> co_reflexive x"
  by (metis co_reflexive_def meet.add_right_upper_bound test_def)

lemma test_up_closed: "test x \<longrightarrow> up_closed x"
  by (metis eq_iff mult_left_one mult_sub_right_one mult_right_sub_dist_meet test_def top_mult_right_one up_closed_def)

lemma co_test_reflexive: "co_test x \<longrightarrow> reflexive x"
  by (metis co_test_def add_right_upper_bound reflexive_def)

lemma co_test_transitive: "co_test x \<longrightarrow> transitive x"
  by (smt co_test_def add_associative less_eq_def mult_left_one mult_left_zero mult_right_dist_add mult_semi_associative transitive_def)

lemma co_test_idempotent: "co_test x \<longrightarrow> idempotent x"
  by (metis co_test_reflexive co_test_transitive reflexive_dense idempotent_transitive_dense)

lemma co_test_up_closed: "co_test x \<longrightarrow> up_closed x"
  by (metis co_test_reflexive co_test_idempotent contact_def contact_up_closed add_commutative less_eq_def reflexive_def idempotent_def)

lemma co_test_contact: "co_test x \<longrightarrow> contact x"
  by (metis co_test_reflexive co_test_idempotent co_test_up_closed contact_reflexive_idempotent_up_closed)

lemma vector_transitive: "vector x \<longrightarrow> transitive x"
  by (metis mult_right_isotone meet.zero_least vector_def transitive_def)

lemma vector_up_closed: "vector x \<longrightarrow> up_closed x"
  by (metis vector_def top_mult_right_one up_closed_def)

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* total *}

lemma one_total: "total 1"
  by (metis mult_left_one total_def)

lemma top_total: "total T"
  by (metis top_mult_top total_def)

lemma add_total: "total x \<and> total y \<longrightarrow> total (x + y)"
  by (metis add_left_top mult_right_dist_add total_def)

-- {* co-total *}

lemma zero_co_total: "co_total 0"
  by (metis co_total_def mult_left_zero)

lemma one_co_total: "co_total 1"
  by (metis co_total_def mult_left_one)

lemma add_co_total: "co_total x \<and> co_total y \<longrightarrow> co_total (x + y)"
  by (metis co_total_def add_right_zero mult_right_dist_add)

lemma meet_co_total: "co_total x \<and> co_total y \<longrightarrow> co_total (x \<frown> y)"
  by (metis co_total_def add_left_zero antisym_conv less_eq_def mult_right_sub_dist_meet_left)

lemma comp_co_total: "co_total x \<and> co_total y \<longrightarrow> co_total (x ; y)"
  by (metis co_total_def eq_iff mult_semi_associative zero_least)

-- {* sub-transitive *}

lemma zero_transitive: "transitive 0"
  by (metis mult_left_zero zero_least transitive_def)

lemma one_transitive: "transitive 1"
  by (metis mult_left_one order_refl transitive_def)

lemma top_transitive: "transitive T"
  by (metis meet.zero_least transitive_def)

lemma meet_transitive: "transitive x \<and> transitive y \<longrightarrow> transitive (x \<frown> y)"
  by (smt meet.less_eq_def meet_associative meet_commutative mult_left_sub_dist_meet_left mult_right_sub_dist_meet_left transitive_def)

-- {* dense *}

lemma zero_dense: "dense 0"
  by (metis zero_least dense_def)

lemma one_dense: "dense 1"
  by (metis mult_sub_right_one dense_def)

lemma top_dense: "dense T"
  by (metis top_left_mult_increasing dense_def)

lemma add_dense: "dense x \<and> dense y \<longrightarrow> dense (x + y)"
proof
  assume "dense x \<and> dense y"
  hence "x \<le> x ; x \<and> y \<le> y ; y"
    by (metis dense_def)
  hence "x \<le> (x + y) ; (x + y) \<and> y \<le> (x + y) ; (x + y)"
    by (metis add_left_upper_bound dual_order.trans mult_isotone add_right_upper_bound)
  hence "x + y \<le> (x + y) ; (x + y)"
    by (metis add_least_upper_bound)
  thus "dense (x + y)"
    by (metis dense_def)
qed

-- {* reflexive *}

lemma one_reflexive: "reflexive 1"
  by (metis order_refl reflexive_def)

lemma top_reflexive: "reflexive T"
  by (metis meet.zero_least reflexive_def)

lemma add_reflexive: "reflexive x \<and> reflexive y \<longrightarrow> reflexive (x + y)"
  by (metis add_associative less_eq_def reflexive_def)

lemma meet_reflexive: "reflexive x \<and> reflexive y \<longrightarrow> reflexive (x \<frown> y)"
  by (metis meet.add_least_upper_bound reflexive_def)

lemma comp_reflexive: "reflexive x \<and> reflexive y \<longrightarrow> reflexive (x ; y)"
  by (metis mult_left_isotone mult_left_one order_trans reflexive_def)

-- {* co-reflexive *}

lemma zero_co_reflexive: "co_reflexive 0"
  by (metis co_reflexive_def zero_least)

lemma one_co_reflexive: "co_reflexive 1"
  by (metis co_reflexive_def order_refl)

lemma add_co_reflexive: "co_reflexive x \<and> co_reflexive y \<longrightarrow> co_reflexive (x + y)"
  by (metis co_reflexive_def add_least_upper_bound)

lemma meet_co_reflexive: "co_reflexive x \<and> co_reflexive y \<longrightarrow> co_reflexive (x \<frown> y)"
  by (metis co_reflexive_def meet.less_eq_def meet_associative)

lemma comp_co_reflexive: "co_reflexive x \<and> co_reflexive y \<longrightarrow> co_reflexive (x ; y)"
  by (metis co_reflexive_def mult_isotone mult_left_one)

-- {* idempotent *}

lemma zero_idempotent: "idempotent 0"
  by (metis mult_left_zero idempotent_def)

lemma one_idempotent: "idempotent 1"
  by (metis mult_left_one idempotent_def)

lemma top_idempotent: "idempotent T"
  by (metis top_mult_top idempotent_def)

-- {* up-closed *}

lemma zero_up_closed: "up_closed 0"
  by (metis mult_left_zero up_closed_def)

lemma one_up_closed: "up_closed 1"
  by (metis mult_left_one up_closed_def)

lemma top_up_closed: "up_closed T"
  by (metis top_mult_top vector_def vector_up_closed)

lemma add_up_closed: "up_closed x \<and> up_closed y \<longrightarrow> up_closed (x + y)"
  by (metis mult_right_dist_add up_closed_def)

lemma meet_up_closed: "up_closed x \<and> up_closed y \<longrightarrow> up_closed (x \<frown> y)"
  by (metis dual_order.antisym mult_sub_right_one mult_right_sub_dist_meet up_closed_def)

lemma comp_up_closed: "up_closed x \<and> up_closed y \<longrightarrow> up_closed (x ; y)"
  by (metis dual_order.antisym mult_semi_associative mult_sub_right_one up_closed_def)

-- {* add-distributive *}

lemma zero_add_distributive: "add_distributive 0"
  by (metis add_distributive_def add_idempotent mult_left_zero)

lemma one_add_distributive: "add_distributive 1"
  by (metis add_distributive_def mult_left_one)

lemma add_add_distributive: "add_distributive x \<and> add_distributive y \<longrightarrow> add_distributive (x + y)"
  by (smt add_distributive_def add_associative add_commutative mult_right_dist_add)

-- {* meet-distributive *}

lemma zero_meet_distributive: "meet_distributive 0"
  by (metis meet_left_zero mult_left_zero meet_distributive_def)

lemma one_meet_distributive: "meet_distributive 1"
  by (metis mult_left_one meet_distributive_def)

-- {* contact *}

lemma one_contact: "contact 1"
  by (metis contact_def add_idempotent mult_left_one)

lemma top_contact: "contact T"
  by (metis contact_def add_left_top top_mult_top)

lemma meet_contact: "contact x \<and> contact y \<longrightarrow> contact (x \<frown> y)"
  by (smt contact_def contact_reflexive contact_transitive contact_up_closed meet.less_eq_def meet_commutative meet_left_dist_add mult_left_sub_dist_add_right meet_transitive meet_up_closed reflexive_def transitive_def up_closed_def)

-- {* kernel *}

lemma zero_kernel: "kernel 0"
  by (metis kernel_co_reflexive_idempotent_up_closed zero_co_reflexive zero_idempotent zero_up_closed)

lemma one_kernel: "kernel 1"
  by (metis kernel_def meet_idempotent mult_left_one)

lemma add_kernel: "kernel x \<and> kernel y \<longrightarrow> kernel (x + y)"
  by (metis add_co_reflexive add_dense add_up_closed co_reflexive_transitive kernel_co_reflexive_idempotent_up_closed idempotent_transitive_dense)

-- {* add-distributive contact *}

lemma one_add_dist_contact: "add_dist_contact 1"
  by (metis add_dist_contact_def one_add_distributive one_contact)

-- {* meet-distributive kernel *}

lemma zero_meet_dist_kernel: "meet_dist_kernel 0"
  by (metis meet_dist_kernel_def zero_kernel zero_meet_distributive)

lemma one_meet_dist_kernel: "meet_dist_kernel 1"
  by (metis meet_dist_kernel_def one_kernel one_meet_distributive)

-- {* test *}

lemma zero_test: "test 0"
  by (metis meet_commutative meet_right_zero mult_left_zero test_def)

lemma one_test: "test 1"
  by (metis meet_left_top mult_left_one test_def)

lemma add_test: "test x \<and> test y \<longrightarrow> test (x + y)"
  by (metis (no_types, lifting) meet_commutative meet_left_dist_add mult_right_dist_add test_def)

lemma meet_test: "test x \<and> test y \<longrightarrow> test (x \<frown> y)"
  by (smt test_def meet_commutative meet.add_least_upper_bound meet.add_right_isotone mult_right_sub_dist_meet_left meet.add_left_upper_bound top_right_mult_increasing antisym)

-- {* co-test *}

lemma one_co_test: "co_test 1"
  by (metis co_test_def co_total_def add_left_zero one_co_total)

lemma add_co_test: "co_test x \<and> co_test y \<longrightarrow> co_test (x + y)"
  by (smt co_test_contact co_test_def contact_def add_associative add_commutative add_left_zero mult_left_one mult_right_dist_add)

-- {* vector *}

lemma zero_vector: "vector 0"
  by (metis mult_left_zero vector_def)

lemma top_vector: "vector T"
  by (metis top_mult_top vector_def)

lemma add_vector: "vector x \<and> vector y \<longrightarrow> vector (x + y)"
  by (metis mult_right_dist_add vector_def)

lemma meet_vector: "vector x \<and> vector y \<longrightarrow> vector (x \<frown> y)"
  by (metis antisym meet.add_least_upper_bound mult_right_sub_dist_meet_left mult_right_sub_dist_meet_right top_right_mult_increasing vector_def)

lemma comp_vector: "vector y \<longrightarrow> vector (x ; y)"
  by (metis antisym_conv mult_semi_associative top_right_mult_increasing vector_def)

end

class lattice_ordered_pre_left_semiring_1 = non_associative_left_semiring + bounded_distributive_lattice +
  assumes mult_associative_one: "x ; (y ; z) = (x ; (y ; 1)) ; z"
  assumes mult_right_dist_meet_one: "(x ; 1 \<frown> y ; 1) ; z = x ; z \<frown> y ; z"

begin

subclass pre_left_semiring
  apply unfold_locales
  apply (metis mult_associative_one mult_left_isotone mult_right_isotone mult_sub_right_one)
  done

subclass lattice_ordered_pre_left_semiring
  ..

lemma mult_zero_associative: "x ; 0 ; y = x ; 0"
  by (smt mult_left_zero mult_associative_one)

lemma mult_zero_add_one_dist: "(x ; 0 + 1) ; z = x ; 0 + z"
  by (metis mult_left_one mult_right_dist_add mult_zero_associative)

lemma mult_zero_add_dist: "(x ; 0 + y) ; z = x ; 0 + y ; z"
  by (metis mult_right_dist_add mult_zero_associative)

lemma vector_zero_meet_one_comp: "(x ; 0 \<frown> 1) ; y = x ; 0 \<frown> y"
  by (metis mult_left_one mult_right_dist_meet_one mult_zero_associative)

-- {* Theorem 6 / Figure 2: relations between properties *}

lemma co_test_meet_distributive: "co_test x \<longrightarrow> meet_distributive x"
  by (metis add_left_dist_meet co_test_def meet_distributive_def mult_zero_add_one_dist)

lemma co_test_add_distributive: "co_test x \<longrightarrow> add_distributive x"
  by (smt add_associative add_commutative add_distributive_def add_left_upper_bound co_test_def less_eq_def mult_zero_add_one_dist)

lemma co_test_add_dist_contact: "co_test x \<longrightarrow> add_dist_contact x"
  by (metis co_test_add_distributive add_dist_contact_def co_test_contact)

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* co-test *}

lemma meet_co_test: "co_test x \<and> co_test y \<longrightarrow> co_test (x \<frown> y)"
  by (smt add_commutative add_left_dist_meet co_test_def co_test_up_closed up_closed_def mult_right_dist_meet_one)

lemma comp_co_test: "co_test x \<and> co_test y \<longrightarrow> co_test (x ; y)"
  by (metis add_associative co_test_def mult_zero_add_dist mult_zero_add_one_dist)

end

class lattice_ordered_pre_left_semiring_2 = lattice_ordered_pre_left_semiring +
  assumes mult_sub_associative_one: "x ; (y ; z) \<le> (x ; (y ; 1)) ; z"
  assumes mult_right_dist_meet_one_sub: "x ; z \<frown> y ; z \<le> (x ; 1 \<frown> y ; 1) ; z"

begin

subclass lattice_ordered_pre_left_semiring_1
  apply unfold_locales
  apply (metis meet.eq_iff mult_sub_associative_one mult_sup_associative_one)
  apply (metis meet.antisym_conv mult_one_associative mult_right_dist_meet_one_sub mult_right_sub_dist_meet)
  done

end

class multirelation_algebra_1 = lattice_ordered_pre_left_semiring +
  assumes mult_left_top: "T ; x = T"

begin

-- {* Theorem 10 / Figure 3: closure properties *}

lemma top_add_distributive: "add_distributive T"
  by (metis add_distributive_def add_left_top mult_left_top)

lemma top_meet_distributive: "meet_distributive T"
  by (metis meet_idempotent meet_distributive_def mult_left_top)

lemma top_add_dist_contact: "add_dist_contact T"
  by (metis add_dist_contact_def top_add_distributive top_contact)

lemma top_co_test: "co_test T"
  by (metis co_test_def add_left_top mult_left_top)

end

-- {* M1-algebra *}

class multirelation_algebra_2 = multirelation_algebra_1 + lattice_ordered_pre_left_semiring_2

begin

lemma mult_top_associative: "x ; T ; y = x ; T"
  by (metis mult_left_top mult_associative_one)

lemma vector_meet_one_comp: "(x ; T \<frown> 1) ; y = x ; T \<frown> y"
  by (metis mult_left_one mult_left_top mult_associative_one mult_right_dist_meet_one)

lemma vector_left_annihilator: "vector x \<longrightarrow> x ; y = x"
  by (metis mult_left_top vector_def mult_associative_one)

-- {* properties *}

lemma test_comp_meet: "test x \<and> test y \<longrightarrow> x ; y = x \<frown> y"
  by (smt meet_associative meet_commutative meet_idempotent test_def vector_meet_one_comp)

-- {* Theorem 6 / Figure 2: relations between properties *}

lemma test_add_distributive: "test x \<longrightarrow> add_distributive x"
  by (metis add_distributive_def meet_left_dist_add test_def vector_meet_one_comp)

lemma test_meet_distributive: "test x \<longrightarrow> meet_distributive x"
  by (smt meet.less_eq_def meet_associative meet_commutative meet_distributive_def meet.add_right_upper_bound mult_left_one test_def vector_meet_one_comp)

lemma test_meet_dist_kernel: "test x \<longrightarrow> meet_dist_kernel x"
  by (metis kernel_co_reflexive_idempotent_up_closed meet_associative meet_dist_kernel_def meet_idempotent test_co_reflexive test_def test_up_closed idempotent_def vector_meet_one_comp test_meet_distributive)

lemma vector_idempotent: "vector x \<longrightarrow> idempotent x"
  by (metis idempotent_def vector_left_annihilator)

lemma vector_add_distributive: "vector x \<longrightarrow> add_distributive x"
  by (metis add_distributive_def add_idempotent vector_left_annihilator)

lemma vector_meet_distributive: "vector x \<longrightarrow> meet_distributive x"
  by (metis meet_distributive_def meet_idempotent vector_left_annihilator)

lemma vector_co_vector: "vector x \<longleftrightarrow> co_vector x"
  by (metis co_vector_def vector_def mult_zero_associative vector_left_annihilator)

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* test *}

lemma comp_test: "test x \<and> test y \<longrightarrow> test (x ; y)"
  by (metis meet_associative meet_distributive_def meet.add_right_zero test_def test_up_closed up_closed_def mult_associative_one test_meet_distributive)

end

class dual =
  fixes dual :: "'a \<Rightarrow> 'a" ("_\<^sup>d" [100] 100)

class multirelation_algebra_3 = lattice_ordered_pre_left_semiring + dual +
  assumes dual_involutive: "x\<^sup>d\<^sup>d = x"
  assumes dual_dist_add: "(x + y)\<^sup>d = x\<^sup>d \<frown> y\<^sup>d"
  assumes dual_one: "1\<^sup>d = 1"

begin

lemma dual_dist_meet: "(x \<frown> y)\<^sup>d = x\<^sup>d + y\<^sup>d"
  by (metis dual_dist_add dual_involutive)

lemma dual_antitone: "x \<le> y \<longrightarrow> y\<^sup>d \<le> x\<^sup>d"
  by (metis dual_dist_meet add_left_divisibility meet.add_left_divisibility)

lemma dual_zero: "0\<^sup>d = T"
  by (metis dual_dist_meet add_right_top dual_involutive meet_left_zero)

lemma dual_top: "T\<^sup>d = 0"
  by (metis dual_zero dual_involutive)

-- {* Theorem 10 / Figure 3: closure properties *}

lemma reflexive_co_reflexive_dual: "reflexive x \<longleftrightarrow> co_reflexive (x\<^sup>d)"
  by (metis co_reflexive_def dual_antitone dual_involutive dual_one reflexive_def)

end

class multirelation_algebra_4 = multirelation_algebra_3 +
  assumes dual_sub_dist_comp: "(x ; y)\<^sup>d \<le> x\<^sup>d ; y\<^sup>d"

begin

subclass multirelation_algebra_1
  apply unfold_locales
  apply (metis dual_zero dual_sub_dist_comp dual_involutive meet.less_eq_def meet_commutative meet_left_top mult_left_zero)
  done

lemma dual_sub_dist_comp_one: "(x ; y)\<^sup>d \<le> (x ; 1)\<^sup>d ; y\<^sup>d"
  by (metis dual_sub_dist_comp mult_one_associative)

-- {* Theorem 10 / Figure 3: closure properties *}

lemma co_total_total_dual: "co_total x \<longrightarrow> total (x\<^sup>d)"
  by (metis co_total_def dual_sub_dist_comp dual_zero meet.less_eq_def meet_commutative meet_left_top total_def)

lemma transitive_dense_dual: "transitive x \<longrightarrow> dense (x\<^sup>d)"
  by (metis dual_antitone dual_sub_dist_comp order_trans transitive_def dense_def)

end

-- {* M2-algebra *}

class multirelation_algebra_5 = multirelation_algebra_3 +
  assumes dual_dist_comp_one: "(x ; y)\<^sup>d = (x ; 1)\<^sup>d ; y\<^sup>d"

begin

subclass multirelation_algebra_4
  apply unfold_locales
  apply (metis dual_antitone mult_sub_right_one mult_left_isotone dual_dist_comp_one)
  done

lemma strong_up_closed: "x ; 1 \<le> x \<longrightarrow> x\<^sup>d ; y\<^sup>d \<le> (x ; y)\<^sup>d"
  by (metis dual_dist_comp_one eq_iff mult_sub_right_one)

lemma strong_up_closed_2: "up_closed x \<longrightarrow> (x ; y)\<^sup>d = x\<^sup>d ; y\<^sup>d"
  by (metis dual_sub_dist_comp eq_iff strong_up_closed up_closed_def)

subclass lattice_ordered_pre_left_semiring_2
  apply unfold_locales
  apply (smt comp_up_closed dual_antitone dual_dist_comp_one dual_involutive dual_one mult_left_one mult_one_associative mult_semi_associative up_closed_def strong_up_closed_2)
  apply (smt dual_dist_comp_one dual_dist_meet dual_involutive eq_refl mult_one_associative mult_right_dist_add)
  done

-- {* Theorem 8 *}

subclass multirelation_algebra_2
  ..

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* up-closed *}

lemma dual_up_closed: "up_closed x \<longleftrightarrow> up_closed (x\<^sup>d)"
  by (metis dual_involutive dual_one up_closed_def strong_up_closed_2)

-- {* contact *}

lemma contact_kernel_dual: "contact x \<longleftrightarrow> kernel (x\<^sup>d)"
  by (metis contact_def contact_up_closed dual_dist_add dual_involutive dual_one kernel_def kernel_up_closed up_closed_def strong_up_closed_2)

-- {* add-distributive contact *}

lemma add_dist_contact_meet_dist_kernel_dual: "add_dist_contact x \<longleftrightarrow> meet_dist_kernel (x\<^sup>d)"
proof
  assume 1: "add_dist_contact x"
  hence 2: "up_closed x"
    by (metis add_dist_contact_def contact_up_closed)
  have "add_distributive x" using 1
    by (metis add_dist_contact_def)
  hence "meet_distributive (x\<^sup>d)" using 2
    by (smt add_distributive_def dual_dist_comp_one dual_dist_meet dual_involutive meet_distributive_def up_closed_def)
  thus "meet_dist_kernel (x\<^sup>d)" using 1
    by (metis contact_kernel_dual add_dist_contact_def meet_dist_kernel_def)
next
  assume 3: "meet_dist_kernel (x\<^sup>d)"
  hence 2: "up_closed (x\<^sup>d)"
    by (metis kernel_up_closed meet_dist_kernel_def)
  have "meet_distributive (x\<^sup>d)" using 3
    by (metis meet_dist_kernel_def)
  hence "add_distributive (x\<^sup>d\<^sup>d)" using 2
    by (smt meet_distributive_def add_distributive_def dual_dist_add dual_involutive strong_up_closed_2)
  thus "add_dist_contact x" using 3
    by (metis contact_kernel_dual add_dist_contact_def meet_dist_kernel_def dual_involutive)
qed

-- {* test *}

lemma test_co_test_dual: "test x \<longleftrightarrow> co_test (x\<^sup>d)"
  by (smt co_test_def co_test_up_closed dual_dist_meet dual_involutive dual_one dual_top test_def test_up_closed strong_up_closed_2)

-- {* vector *}

lemma vector_dual: "vector x \<longleftrightarrow> vector (x\<^sup>d)"
  by (metis dual_dist_comp_one comp_vector dual_involutive dual_top vector_def zero_vector)

end

class multirelation_algebra_6 = multirelation_algebra_4 +
  assumes dual_sub_dist_comp_one: "(x ; 1)\<^sup>d ; y\<^sup>d \<le> (x ; y)\<^sup>d"

begin

subclass multirelation_algebra_5
  apply unfold_locales
  apply (metis dual_sub_dist_comp dual_sub_dist_comp_one meet.eq_iff mult_one_associative)
  done

(*lemma "dense x \<and> co_reflexive x \<longrightarrow> up_closed x" nitpick [expect=genuine,card=5] oops*)
(*lemma "x ; T \<frown> y ; z \<le> (x ; T \<frown> y) ; z" nitpick [expect=genuine,card=8] oops*)

end

-- {* M3-algebra *}

class up_closed_multirelation_algebra = multirelation_algebra_3 +
  assumes dual_dist_comp: "(x ; y)\<^sup>d = x\<^sup>d ; y\<^sup>d"

begin

lemma mult_right_dist_meet: "(x \<frown> y) ; z = x ; z \<frown> y ; z"
  by (metis dual_dist_add dual_dist_comp dual_involutive mult_right_dist_add)

-- {* Theorem 9 *}

subclass idempotent_left_semiring
  apply unfold_locales
  apply (metis antisym dual_antitone dual_dist_comp dual_involutive mult_semi_associative)
  apply (metis mult_left_one)
  apply (metis dual_dist_add dual_dist_comp dual_involutive dual_one less_eq_def meet_absorb mult_sub_right_one)
  done

subclass multirelation_algebra_6
  apply unfold_locales
  apply (metis dual_dist_comp eq_iff)
  apply (metis dual_dist_comp eq_iff mult_right_one)
  done

lemma vector_meet_comp: "(x ; T \<frown> y) ; z = x ; T \<frown> y ; z"
  by (metis mult_associative mult_left_top mult_right_dist_meet)

lemma vector_zero_meet_comp: "(x ; 0 \<frown> y) ; z = x ; 0 \<frown> y ; z"
  by (metis mult_associative mult_left_zero mult_right_dist_meet)

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* total *}

lemma meet_total: "total x \<and> total y \<longrightarrow> total (x \<frown> y)"
  by (metis meet_left_top total_def mult_right_dist_meet)

lemma comp_total: "total x \<and> total y \<longrightarrow> total (x ; y)"
  by (metis mult_associative total_def)

lemma total_co_total_dual: "total x \<longleftrightarrow> co_total (x\<^sup>d)"
  by (metis co_total_def dual_dist_comp dual_involutive dual_top total_def)

-- {* dense *}

lemma transitive_iff_dense_dual: "transitive x \<longleftrightarrow> dense (x\<^sup>d)"
  by (metis dense_def dual_antitone dual_dist_comp dual_involutive transitive_def)

-- {* idempotent *}

lemma idempotent_dual: "idempotent x \<longleftrightarrow> idempotent (x\<^sup>d)"
  by (metis dual_involutive idempotent_transitive_dense transitive_iff_dense_dual)

-- {* add-distributive *}

lemma comp_add_distributive: "add_distributive x \<and> add_distributive y \<longrightarrow> add_distributive (x ; y)"
  by (metis add_distributive_def mult_associative)

lemma add_meet_distributive_dual: "add_distributive x \<longleftrightarrow> meet_distributive (x\<^sup>d)"
  by (metis (no_types, hide_lams) add_distributive_def dual_dist_add dual_dist_comp dual_involutive meet_distributive_def)

-- {* meet-distributive *}

lemma meet_meet_distributive: "meet_distributive x \<and> meet_distributive y \<longrightarrow> meet_distributive (x \<frown> y)"
  by (smt meet_distributive_def meet_associative meet_commutative mult_right_dist_meet)

lemma comp_meet_distributive: "meet_distributive x \<and> meet_distributive y \<longrightarrow> meet_distributive (x ; y)"
  by (metis meet_distributive_def mult_associative)

(*lemma "co_total x \<and> transitive x \<and> up_closed x \<longrightarrow> co_reflexive x" nitpick [expect=genuine,card=5] oops*)
(*lemma "total x \<and> dense x \<and> up_closed x \<longrightarrow> reflexive x" nitpick [expect=genuine,card=5] oops*)
(*lemma "x ; T \<frown> x\<^sup>d ; 0 = 0" nitpick [expect=genuine,card=6] oops*)

end

class multirelation_algebra_7 = multirelation_algebra_4 +
  assumes vector_meet_comp: "(x ; T \<frown> y) ; z = x ; T \<frown> y ; z"

begin

lemma vector_zero_meet_comp: "(x ; 0 \<frown> y) ; z = x ; 0 \<frown> y ; z"
  by (metis vector_def comp_vector vector_meet_comp zero_vector)

lemma test_add_distributive: "test x \<longrightarrow> add_distributive x"
  by (metis add_distributive_def meet_left_dist_add mult_left_one test_def vector_meet_comp)

lemma test_meet_distributive: "test x \<longrightarrow> meet_distributive x"
  by (smt meet.less_eq_def meet_associative meet_commutative meet_distributive_def meet.add_right_upper_bound mult_left_one test_def vector_meet_comp)

lemma test_meet_dist_kernel: "test x \<longrightarrow> meet_dist_kernel x"
  by (metis kernel_co_reflexive_idempotent_up_closed meet_associative meet_dist_kernel_def meet_idempotent mult_left_one test_co_reflexive test_def test_up_closed idempotent_def vector_meet_comp test_meet_distributive)

lemma co_test_meet_distributive: "co_test x \<longrightarrow> meet_distributive x"
proof
  assume "co_test x"
  hence "x = x ; 0 + 1"
    by (metis co_test_def)
  hence "\<forall>y z . x ; y \<frown> x ; z = x ; (y \<frown> z)"
    by (metis mult_left_one mult_left_top mult_right_dist_add meet.add_right_zero vector_zero_meet_comp add_left_dist_meet)
  thus "meet_distributive x"
    by (metis meet_distributive_def)
qed

lemma co_test_add_distributive: "co_test x \<longrightarrow> add_distributive x"
proof
  assume "co_test x"
  hence 1: "x = x ; 0 + 1"
    by (metis co_test_def)
  hence "\<forall>y z . x ; (y + z) = x ; y + x ; z"
    by (metis add_associative add_commutative add_idempotent mult_left_one mult_left_top mult_right_dist_add meet.add_right_zero vector_zero_meet_comp)
  thus "add_distributive x"
    by (metis add_distributive_def)
qed

lemma co_test_add_dist_contact: "co_test x \<longrightarrow> add_dist_contact x"
  by (metis co_test_add_distributive add_dist_contact_def co_test_contact)

end

(* BooleanSemiring *)

class complemented_distributive_lattice = bounded_distributive_lattice + uminus +
  assumes meet_complement: "x \<frown> (-x) = 0"
  assumes add_complement: "x + (-x) = T"

begin

sublocale boolean_algebra where minus = "\<lambda>x y . x \<frown> (-y)" and inf = meet and sup = plus and bot = "0" and top = "T"
  apply unfold_locales
  apply (simp add: meet.add_left_upper_bound)
  apply (simp add: meet.add_right_upper_bound)
  using meet.add_least_upper_bound apply blast
  apply (simp add: add_left_upper_bound)
  apply (simp add: add_right_upper_bound)
  using add_least_upper_bound apply blast
  apply (simp add: zero_least)
  apply (simp add: meet.zero_least)
  apply (simp add: add_left_dist_meet)
  apply (simp add: meet_complement)
  apply (simp add: add_complement)
  apply simp
  done

end

-- {* M0-algebra *}

context lattice_ordered_pre_left_semiring

begin

-- {* Section 7 *}

lemma vector_1: "vector x \<longleftrightarrow> x ; T \<le> x"
  by (simp add: meet.eq_iff top_right_mult_increasing vector_def)

definition zero_vector :: "'a \<Rightarrow> bool" where "zero_vector x \<longleftrightarrow> x \<le> x ; 0"
definition one_vector :: "'a \<Rightarrow> bool" where "one_vector x \<longleftrightarrow> x ; 0 \<le> x"

lemma zero_vector_left_zero: "zero_vector x \<longrightarrow> x ; y = x ; 0"
proof -
  have "zero_vector x \<longrightarrow> x ; y \<le> x ; 0"
    using mult_isotone top_greatest vector_def vector_left_mult_closed zero_vector zero_vector_def by fastforce
  thus ?thesis
    by (simp add: meet.antisym mult_right_isotone zero_least)
qed

lemma zero_vector_1: "zero_vector x \<longleftrightarrow> (\<forall>y . x ; y = x ; 0)"
  by (metis top_right_mult_increasing zero_vector_def zero_vector_left_zero)

lemma zero_vector_2: "zero_vector x \<longleftrightarrow> (\<forall>y . x ; y \<le> x ; 0)"
  by (simp add: meet.eq_iff mult_right_isotone zero_least zero_vector_1)

lemma zero_vector_3: "zero_vector x \<longleftrightarrow> x ; 1 = x ; 0"
  by (metis mult_sub_right_one zero_vector_def zero_vector_left_zero)

lemma zero_vector_4: "zero_vector x \<longleftrightarrow> x ; 1 \<le> x ; 0"
  by (simp add: meet.eq_iff mult_right_isotone zero_least zero_vector_3)

lemma zero_vector_5: "zero_vector x \<longleftrightarrow> x ; T = x ; 0"
  by (metis top_right_mult_increasing zero_vector_def zero_vector_left_zero)

lemma zero_vector_6: "zero_vector x \<longleftrightarrow> x ; T \<le> x ; 0"
  by (simp add: meet.eq_iff mult_right_isotone top_greatest zero_vector_5)

lemma zero_vector_7: "zero_vector x \<longleftrightarrow> (\<forall>y . x ; T = x ; y)"
  by (metis zero_vector_5 zero_vector_left_zero)

lemma zero_vector_8: "zero_vector x \<longleftrightarrow> (\<forall>y . x ; T \<le> x ; y)"
  by (metis zero_vector_6 zero_vector_left_zero)

lemma zero_vector_9: "zero_vector x \<longleftrightarrow> (\<forall>y . x ; 1 = x ; y)"
  by (metis zero_vector_1)

lemma zero_vector_0: "zero_vector x \<longleftrightarrow> (\<forall>y z . x ; y = x ; z)"
  by (metis zero_vector_5 zero_vector_left_zero)

-- {* Theorem 6 / Figure 2: relations between properties *}

lemma co_vector_zero_vector_one_vector: "co_vector x \<longleftrightarrow> zero_vector x \<and> one_vector x"
  by (simp add: co_vector_def meet.eq_iff one_vector_def zero_vector_def)

lemma up_closed_one_vector: "up_closed x \<longrightarrow> one_vector x"
  by (metis mult_right_isotone up_closed_def zero_least one_vector_def)

lemma zero_vector_dense: "zero_vector x \<longrightarrow> dense x"
  by (metis dense_def zero_vector_def zero_vector_left_zero)

lemma zero_vector_add_distributive: "zero_vector x \<longrightarrow> add_distributive x"
  by (metis add_distributive_def add_idempotent zero_vector_left_zero)

lemma zero_vector_meet_distributive: "zero_vector x \<longrightarrow> meet_distributive x"
  by (metis meet_distributive_def meet_idempotent zero_vector_left_zero)

lemma up_closed_zero_vector_vector: "up_closed x \<and> zero_vector x \<longrightarrow> vector x"
  by (metis up_closed_def zero_vector_8 vector_1)

lemma zero_vector_one_vector_vector: "zero_vector x \<and> one_vector x \<longrightarrow> vector x"
  by (simp add: one_vector_def vector_1 zero_vector_5)

lemma co_vector_vector: "co_vector x \<longrightarrow> vector x"
  by (simp add: co_vector_zero_vector_one_vector zero_vector_one_vector_vector)

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* zero-vector *}

lemma zero_zero_vector: "zero_vector 0"
  by (simp add: mult_left_zero zero_vector_def)

lemma add_zero_vector: "zero_vector x \<and> zero_vector y \<longrightarrow> zero_vector (x + y)"
  by (simp add: mult_right_dist_add zero_vector_5)

lemma comp_zero_vector: "zero_vector x \<and> zero_vector y \<longrightarrow> zero_vector (x ; y)"
  by (metis mult_one_associative zero_vector_0)

-- {* one-vector *}

lemma zero_one_vector: "one_vector 0"
  by (simp add: zero_up_closed up_closed_one_vector)

lemma one_one_vector: "one_vector 1"
  by (simp add: one_up_closed up_closed_one_vector)

lemma top_one_vector: "one_vector T"
  by (simp add: top_greatest one_vector_def)

lemma add_one_vector: "one_vector x \<and> one_vector y \<longrightarrow> one_vector (x + y)"
  by (smt add_least_upper_bound add_left_upper_bound add_right_upper_bound mult_right_dist_add order_trans one_vector_def)

lemma meet_one_vector: "one_vector x \<and> one_vector y \<longrightarrow> one_vector (x \<frown> y)"
  by (meson dual_order.trans meet.add_least_upper_bound mult_right_sub_dist_meet_left mult_right_sub_dist_meet_right one_vector_def)

lemma comp_one_vector: "one_vector x \<and> one_vector y \<longrightarrow> one_vector (x ; y)"
  using mult_isotone mult_semi_associative order_lesseq_imp one_vector_def by blast

end

context multirelation_algebra_1

begin

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* zero-vector *}

lemma top_zero_vector: "zero_vector T"
  by (simp add: mult_left_top zero_vector_def)

end

-- {* M1-algebra *}

context multirelation_algebra_2

begin

-- {* Section 7 *}

lemma zero_vector_10: "zero_vector x \<longleftrightarrow> x ; T = x ; 1"
  by (metis mult_one_associative mult_top_associative zero_vector_7)

lemma zero_vector_11: "zero_vector x \<longleftrightarrow> x ; T \<le> x ; 1"
  using antisym_conv mult_right_isotone reflexive_def top_reflexive zero_vector_10 by blast

-- {* Theorem 6 / Figure 2: relations between properties *}

lemma vector_zero_vector: "vector x \<longrightarrow> zero_vector x"
  by (simp add: zero_vector_def vector_left_annihilator)

lemma vector_up_closed_zero_vector: "vector x \<longleftrightarrow> up_closed x \<and> zero_vector x"
  using up_closed_zero_vector_vector vector_up_closed vector_zero_vector by blast

lemma vector_zero_vector_one_vector: "vector x \<longleftrightarrow> zero_vector x \<and> one_vector x"
  using up_closed_one_vector zero_vector_one_vector_vector vector_up_closed_zero_vector by blast

(*lemma "(x ; 0 \<frown> y) ; 1 = x ; 0 \<frown> y ; 1" nitpick [expect=genuine,card=7] oops*)

end

-- {* M3-algebra *}

context up_closed_multirelation_algebra

begin

lemma up_closed: "up_closed x"
  by (simp add: mult_right_one up_closed_def)

lemma dedekind_1_left: "x ; 1 \<frown> y \<le> (x \<frown> y ; 1) ; 1"
  by (simp add: mult_right_one)

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* zero-vector *}

lemma zero_vector_dual: "zero_vector x \<longleftrightarrow> zero_vector (x\<^sup>d)"
  using up_closed_zero_vector_vector vector_dual vector_zero_vector up_closed by blast

end

-- {* complemented M0-algebra *}

class lattice_ordered_pre_left_semiring_b = lattice_ordered_pre_left_semiring + complemented_distributive_lattice

begin

definition down_closed :: "'a \<Rightarrow> bool" where "down_closed x \<longleftrightarrow> -x ; 1 \<le> -x"

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* down-closed *}

lemma zero_down_closed: "down_closed 0"
  by (simp add: down_closed_def)

lemma top_down_closed: "down_closed T"
  using down_closed_def up_closed_def zero_up_closed by auto

lemma complement_down_closed_up_closed: "down_closed x \<longleftrightarrow> up_closed (-x)"
  by (simp add: down_closed_def meet.eq_iff mult_sub_right_one up_closed_def)

lemma add_down_closed: "down_closed x \<and> down_closed y \<longrightarrow> down_closed (x + y)"
  by (simp add: complement_down_closed_up_closed meet_up_closed)

lemma meet_down_closed: "down_closed x \<and> down_closed y \<longrightarrow> down_closed (x \<frown> y)"
  by (simp add: complement_down_closed_up_closed add_up_closed)

end

class multirelation_algebra_1b = multirelation_algebra_1 + complemented_distributive_lattice

begin

subclass lattice_ordered_pre_left_semiring_b ..

-- {* Theorem 7.1 *}

lemma complement_mult_zero_sub: "-(x ; 0) \<le> -x ; 0"
proof -
  have "T = -x ; 0 + x ; 0"
    by (metis compl_sup_top mult_left_top mult_right_dist_add)
  thus ?thesis
    by (simp add: shunting_2 sup.commute)
qed

-- {* Theorem 7.2 *}

lemma transitive_zero_vector_complement: "transitive x \<longrightarrow> zero_vector (-x)"
  by (meson complement_mult_zero_sub compl_mono mult_right_isotone order_trans zero_vector_def transitive_def zero_least)

lemma transitive_dense_complement: "transitive x \<longrightarrow> dense (-x)"
  by (simp add: zero_vector_dense transitive_zero_vector_complement)

lemma transitive_add_distributive_complement: "transitive x \<longrightarrow> add_distributive (-x)"
  by (simp add: zero_vector_add_distributive transitive_zero_vector_complement)

lemma transitive_meet_distributive_complement: "transitive x \<longrightarrow> meet_distributive (-x)"
  by (simp add: zero_vector_meet_distributive transitive_zero_vector_complement)

lemma up_closed_zero_vector_complement: "up_closed x \<longrightarrow> zero_vector (-x)"
  by (metis complement_mult_zero_sub compl_mono mult_right_isotone order_trans zero_vector_def up_closed_def zero_least)

lemma up_closed_dense_complement: "up_closed x \<longrightarrow> dense (-x)"
  by (simp add: zero_vector_dense up_closed_zero_vector_complement)

lemma up_closed_add_distributive_complement: "up_closed x \<longrightarrow> add_distributive (-x)"
  by (simp add: zero_vector_add_distributive up_closed_zero_vector_complement)

lemma up_closed_meet_distributive_complement: "up_closed x \<longrightarrow> meet_distributive (-x)"
  by (simp add: zero_vector_meet_distributive up_closed_zero_vector_complement)

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* closure under complement *}

lemma co_total_total: "co_total x \<longrightarrow> total (-x)"
  by (metis complement_mult_zero_sub co_total_def compl_bot_eq mult_left_sub_dist_add_right sup_bot_right top_le total_def)

lemma complement_one_vector_zero_vector: "one_vector x \<longrightarrow> zero_vector (-x)"
  using compl_mono complement_mult_zero_sub one_vector_def order_trans zero_vector_def by blast

-- {* Theorem 6 / Figure 2: relations between properties *}

lemma down_closed_zero_vector: "down_closed x \<longrightarrow> zero_vector x"
  using complement_down_closed_up_closed up_closed_zero_vector_complement by force

lemma down_closed_one_vector_vector: "down_closed x \<and> one_vector x \<longrightarrow> vector x"
  by (simp add: down_closed_zero_vector zero_vector_one_vector_vector)

(*lemma complement_vector: "vector x \<longrightarrow> vector (-x)" nitpick [expect=genuine,card=8] oops*)

end

class multirelation_algebra_1c = multirelation_algebra_1b +
  assumes dedekind_T_left: "x ; T \<frown> y \<le> (x \<frown> y ; T) ; T"
  assumes comp_zero_meet: "(x ; 0 \<frown> y) ; 0 \<le> (x \<frown> y) ; 0"

begin

-- {* Theorem 7.3 *}

lemma schroeder_top_sub: "-(x ; T) ; T \<le> -x"
proof -
  have "-(x ; T) ; T \<frown> x \<le> 0"
    by (metis compl_inf_bot dedekind_T_left vector_def zero_vector)
  thus ?thesis
    by (simp add: shunting_1)
qed

-- {* Theorem 7.4 *}

lemma schroeder_top: "x ; T \<le> y \<longleftrightarrow> -y ; T \<le> -x"
  apply rule
  using compl_mono meet.order_trans mult_left_isotone schroeder_top_sub apply blast
  by (metis compl_mono double_compl mult_left_isotone order_trans schroeder_top_sub)

-- {* Theorem 7.5 *}

lemma schroeder_top_eq: "-(x ; T) ; T = -(x ; T)"
  by (metis meet.antisym_conv mult_semi_associative top_mult_top top_right_mult_increasing schroeder_top)

lemma schroeder_one_eq: "-(x ; T) ; 1 = -(x ; T)"
  by (metis top_mult_right_one schroeder_top_eq)

-- {* Theorem 7.6 *}

lemma vector_meet_comp: "x ; T \<frown> y ; z = (x ; T \<frown> y) ; z"
proof (rule antisym)
  have "x ; T \<frown> y ; z = x ; T \<frown> ((x ; T \<frown> y) + (-(x ; T) \<frown> y)) ; z"
    using inf.commute maddux_3_11 meet_left_dist_add by auto
  also have "... = x ; T \<frown> ((x ; T \<frown> y) ; z + (-(x ; T) \<frown> y) ; z)"
    by (simp add: inf_sup_distrib2 mult_right_dist_add)
  also have "... = (x ; T \<frown> (x ; T \<frown> y) ; z) + (x ; T \<frown> (-(x ; T) \<frown> y) ; z)"
    by (simp add: meet_left_dist_add)
  also have "... \<le> (x ; T \<frown> y) ; z + (x ; T \<frown> (-(x ; T) \<frown> y) ; z)"
    by (simp add: le_infI2)
  also have "... \<le> (x ; T \<frown> y) ; z + (x ; T \<frown> -(x ; T) ; z)"
    using meet.add_right_isotone meet.add_right_upper_bound meet_commutative mult_left_isotone sup_right_isotone by presburger
  also have "... \<le> (x ; T \<frown> y) ; z + (x ; T \<frown> -(x ; T) ; T)"
    using meet.add_right_isotone mult_right_isotone sup_right_isotone by auto
  also have "... = (x ; T \<frown> y) ; z"
    by (simp add: meet_complement schroeder_top_eq)
  finally show "x ; T \<frown> y ; z \<le> (x ; T \<frown> y) ; z"
    .
next
  show "(x ; T \<frown> y) ; z \<le> x ; T \<frown> y ; z"
    by (metis inf.bounded_iff mult_left_top mult_right_sub_dist_meet_left mult_right_sub_dist_meet_right mult_semi_associative order_lesseq_imp)
qed

(*
lemma dedekind_T_left: "x ; T \<frown> y \<le> (x \<frown> y ; T) ; T"
  by (metis inf.commute top_right_mult_increasing vector_meet_comp)
*)

-- {* Theorem 7.7 *}

lemma vector_zero_meet_comp: "(x ; 0 \<frown> y) ; z = x ; 0 \<frown> y ; z"
  by (metis vector_def comp_vector vector_meet_comp zero_vector)

lemma vector_zero_meet_comp_2: "(x ; 0 \<frown> y) ; z = (x ; 0 \<frown> y ; 1) ; z"
  by (simp add: mult_one_associative vector_zero_meet_comp)

-- {* Theorem 7.8 *}

lemma comp_zero_meet_2: "x ; 0 \<frown> y ; 0 = (x \<frown> y) ; 0"
  using meet.antisym mult_right_sub_dist_meet comp_zero_meet vector_zero_meet_comp by auto

lemma comp_zero_meet_3: "x ; 0 \<frown> y ; 0 = (x ; 0 \<frown> y) ; 0"
  by (simp add: vector_zero_meet_comp)

lemma comp_zero_meet_4: "x ; 0 \<frown> y ; 0 = (x ; 0 \<frown> y ; 0) ; 0"
  by (metis comp_zero_meet_2 inf.commute vector_zero_meet_comp)

lemma comp_zero_meet_5: "x ; 0 \<frown> y ; 0 = (x ; 1 \<frown> y ; 1) ; 0"
  by (metis comp_zero_meet_2 mult_one_associative)

lemma comp_zero_meet_6: "x ; 0 \<frown> y ; 0 = (x ; 1 \<frown> y ; 0) ; 0"
  using meet_commutative mult_one_associative vector_zero_meet_comp by auto

lemma comp_zero_meet_7: "x ; 0 \<frown> y ; 0 = (x ; 1 \<frown> y) ; 0"
  by (metis comp_zero_meet_2 mult_one_associative)

-- {* Theorem 10 / Figure 3: closure properties *}

-- {* zero-vector *}

lemma meet_zero_vector: "zero_vector x \<and> zero_vector y \<longrightarrow> zero_vector (x \<frown> y)"
  by (metis comp_zero_meet_2 inf.sup_mono zero_vector_def)

-- {* down-closed *}

lemma comp_down_closed: "down_closed x \<and> down_closed y \<longrightarrow> down_closed (x ; y)"
  by (metis complement_down_closed_up_closed down_closed_zero_vector up_closed_def zero_vector_0 schroeder_one_eq)

-- {* closure under complement *}

lemma complement_vector: "vector x \<longleftrightarrow> vector (-x)"
  by (metis double_compl vector_def schroeder_top_eq)

lemma complement_zero_vector_one_vector: "zero_vector x \<longrightarrow> one_vector (-x)"
  by (smt comp_zero_meet_2 idempotent_def meet.add_relative_same_increasing meet_commutative meet_complement one_vector_def shunting_1 zero_idempotent zero_vector_def)

lemma complement_zero_vector_one_vector_iff: "zero_vector x \<longleftrightarrow> one_vector (-x)"
  using complement_zero_vector_one_vector complement_one_vector_zero_vector by force

lemma complement_one_vector_zero_vector_iff: "one_vector x \<longleftrightarrow> zero_vector (-x)"
  using complement_zero_vector_one_vector complement_one_vector_zero_vector by force

-- {* Theorem 6 / Figure 2: relations between properties *}

lemma vector_down_closed: "vector x \<longrightarrow> down_closed x"
  using complement_vector complement_down_closed_up_closed vector_up_closed by blast

lemma co_vector_down_closed: "co_vector x \<longrightarrow> down_closed x"
  by (metis co_vector_def down_closed_def meet.eq_iff mult_left_zero mult_right_isotone mult_semi_associative zero_least schroeder_one_eq)

lemma vector_down_closed_one_vector: "vector x \<longleftrightarrow> down_closed x \<and> one_vector x"
  using down_closed_one_vector_vector up_closed_one_vector vector_up_closed vector_down_closed by blast

lemma vector_up_closed_down_closed: "vector x \<longleftrightarrow> up_closed x \<and> down_closed x"
  using down_closed_zero_vector up_closed_zero_vector_vector vector_up_closed vector_down_closed by blast

-- {* Section 7 *}

lemma vector_b1: "vector x \<longleftrightarrow> -x ; T = -x"
  using complement_vector vector_def by force

lemma vector_b2: "vector x \<longleftrightarrow> -x ; 0 = -x"
  by (metis double_compl up_closed_zero_vector_complement vector_left_mult_closed vector_up_closed zero_vector zero_vector_0 vector_b1)

lemma covector_b1: "co_vector x \<longleftrightarrow> -x ; T = -x"
  using co_vector_def co_vector_vector vector_b1 vector_b2 by force

lemma covector_b2: "co_vector x \<longleftrightarrow> -x ; 0 = -x"
  using covector_b1 vector_b1 vector_b2 by auto

lemma vector_co_vector_iff: "vector x \<longleftrightarrow> co_vector x"
  by (simp add: covector_b1 vector_b1)

lemma zero_vector_b: "zero_vector x \<longleftrightarrow> -x ; 0 \<le> -x"
  by (simp add: complement_zero_vector_one_vector_iff one_vector_def)

lemma one_vector_b1: "one_vector x \<longleftrightarrow> -x \<le> -x ; 0"
  by (simp add: complement_one_vector_zero_vector_iff zero_vector_def)

lemma one_vector_b0: "one_vector x \<longleftrightarrow> (\<forall>y z . -x ; y = -x ; z)"
  by (simp add: complement_one_vector_zero_vector_iff zero_vector_0)

(*lemma schroeder_one: "x ; -1 \<le> y \<longleftrightarrow> -y ; -1 \<le> -x" nitpick [expect=genuine,card=8] oops*)

end

class multirelation_algebra_2b = multirelation_algebra_2 + complemented_distributive_lattice

begin

subclass multirelation_algebra_1b ..

(*lemma "-x ; 0 \<le> -(x ; 0)" nitpick [expect=genuine,card=8] oops*)

end

-- {* complemented M1-algebra *}

class multirelation_algebra_2c = multirelation_algebra_2b + multirelation_algebra_1c

class multirelation_algebra_3b = multirelation_algebra_3 + complemented_distributive_lattice

begin

subclass lattice_ordered_pre_left_semiring_b ..

lemma dual_complement_commute: "-(x\<^sup>d) = (-x)\<^sup>d"
  by (metis compl_unique dual_dist_add dual_dist_meet dual_top dual_zero meet_complement sup_compl_top)

end

-- {* complemented M2-algebra *}

class multirelation_algebra_5b = multirelation_algebra_5 + complemented_distributive_lattice

begin

subclass multirelation_algebra_2b ..

subclass multirelation_algebra_3b ..

lemma dual_down_closed: "down_closed x \<longleftrightarrow> down_closed (x\<^sup>d)"
  using complement_down_closed_up_closed dual_complement_commute dual_up_closed by auto

end

class multirelation_algebra_5c = multirelation_algebra_5b + multirelation_algebra_1c

begin

lemma complement_mult_zero_below: "-x ; 0 \<le> -(x ; 0)"
  by (simp add: comp_zero_meet_2 mult_left_zero shunting_1)

(*lemma "x ; 1 \<frown> y ; 1 \<le> (x \<frown> y) ; 1" nitpick [expect=genuine,card=4] oops*)
(*lemma "x ; 1 \<frown> (y ; 1) \<le> (x ; 1 \<frown> y) ; 1" nitpick [expect=genuine,card=4] oops*)

end

class up_closed_multirelation_algebra_b = up_closed_multirelation_algebra + complemented_distributive_lattice

begin

subclass multirelation_algebra_5c
  apply unfold_locales
  apply (metis mult_associative mult_right_dist_meet top_mult_top top_right_mult_increasing)
  by (simp add: le_infI2 meet_commutative mult_left_isotone zero_right_mult_decreasing)

lemma complement_zero_vector: "zero_vector x \<longleftrightarrow> zero_vector (-x)"
  by (metis compl_sup_top double_compl mult_right_dist_add mult_right_one zero_vector_def zero_vector_left_zero shunting_2 top_zero_vector)

lemma down_closed: "down_closed x"
  by (simp add: down_closed_def mult_right_one)

lemma vector: "vector x"
  by (simp add: down_closed complement_one_vector_zero_vector_iff down_closed_zero_vector vector_down_closed_one_vector)

end

end