Theory KAD.Modal_Kleene_Algebra_Applications

(* Title:      Applications of Modal Kleene Algebras
   Author:     Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
   Maintainer: Walter Guttmann <walter.guttman at canterbury.ac.nz>
               Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Applications of Modal Kleene Algebras›

theory Modal_Kleene_Algebra_Applications
imports Antidomain_Semiring
begin

text ‹This file collects some applications of the theories developed so far. These are described
 in~\<^cite>‹"guttmannstruthweber11algmeth"›.›

context antidomain_kleene_algebra
begin

subsection ‹A Reachability Result›

text ‹This example is taken from~\<^cite>‹"desharnaismoellerstruth06kad"›.›

lemma opti_iterate_var [simp]: "|(ad y ⋅ x)⇧⋆⟩ y = |x⇧⋆⟩ y"
proof (rule order.antisym)
  show "|(ad y ⋅ x)⇧⋆⟩ y ≤ |x⇧⋆⟩ y"
    by (simp add: a_subid_aux1' ds.fd_iso2 star_iso)
  have "d y + |x⟩ |(ad y ⋅ x)⇧⋆⟩ y = d y + ad y ⋅ |x⟩ |(ad y ⋅ x)⇧⋆⟩ y"
    using local.ads_d_def local.d_6 local.fdia_def by auto
  also have "... = d y + |ad y ⋅ x⟩ |(ad y ⋅ x)⇧⋆⟩ y"
    by (simp add: fdia_export_2)
  finally have "d y + |x⟩ |(ad y ⋅ x)⇧⋆⟩ y = |(ad y ⋅ x)⇧⋆⟩ y"
    by simp
  thus "|x⇧⋆⟩ y ≤ |(ad y ⋅ x)⇧⋆⟩ y"
    using local.dka.fd_def local.dka.fdia_star_induct_eq by auto
qed

lemma opti_iterate [simp]: "d y + |(x ⋅ ad y)⇧⋆⟩ |x⟩ y = |x⇧⋆⟩ y"
proof -
  have "d y + |(x ⋅ ad y)⇧⋆⟩ |x⟩ y = d y + |x⟩ |(ad y ⋅ x)⇧⋆⟩ y"
    by (metis local.conway.dagger_slide local.ds.fdia_mult)
  also have "... = d y + |x⟩ |x⇧⋆⟩ y"
    by simp
  finally show ?thesis
    by force
qed

lemma opti_iterate_var_2 [simp]: "d y + |ad y ⋅ x⟩ |x⇧⋆⟩ y = |x⇧⋆⟩ y"
  by (metis local.dka.fdia_star_unfold_var opti_iterate_var)

subsection ‹Derivation of Segerberg's Formula›

text ‹This example is taken from~\<^cite>‹"DesharnaisMoellerStruthLMCS"›.›

definition Alpha :: "'a ⇒ 'a ⇒ 'a" ("A")
  where "A x y = d (x ⋅ y) ⋅ ad y"

lemma A_dom [simp]: "d (A x y) = A x y"
  using Alpha_def local.a_d_closed local.ads_d_def local.apd_d_def by auto

lemma A_fdia: "A x y = |x⟩ y ⋅ ad y"
  by (simp add: Alpha_def local.dka.fd_def)

lemma A_fdia_var: "A x y = |x⟩ d y ⋅ ad y"
  by (simp add: A_fdia)

lemma a_A: "ad (A x (ad y)) = |x] y + ad y"
  using Alpha_def local.a_6 local.a_d_closed local.apd_d_def local.fbox_def by force

lemma fsegerberg [simp]: "d y + |x⇧⋆⟩ A x y = |x⇧⋆⟩ y"
proof (rule order.antisym)
  have "d y + |x⟩ (d y + |x⇧⋆⟩ A x y) = d y + |x⟩ y + |x⟩ |x⇧⋆⟩ ( |x⟩ y ⋅ ad y )"
    by (simp add: A_fdia add_assoc local.ds.fdia_add1)
  also have "... = d y + |x⟩ y ⋅ ad y + |x⟩ |x⇧⋆⟩ ( |x⟩ y ⋅ ad y )"
    by (metis local.am2 local.d_6 local.dka.fd_def local.fdia_def)
  finally have "d y + |x⟩ (d y + |x⇧⋆⟩ A x y) = d y + |x⇧⋆⟩ A x y"
    by (metis A_dom A_fdia add_assoc local.dka.fdia_star_unfold_var)
  thus "|x⇧⋆⟩ y ≤ d y + |x⇧⋆⟩ A x y"
    by (metis local.a_d_add_closure local.ads_d_def local.dka.fdia_star_induct_eq local.fdia_def)
  have "d y + |x⇧⋆⟩ A x y = d y + |x⇧⋆⟩ ( |x⟩ y ⋅ ad y )"
    by (simp add: A_fdia)
  also have "... ≤ d y + |x⇧⋆⟩ |x⟩ y"
    using local.dpdz.domain_1'' local.ds.fd_iso1 local.join.sup_mono by blast
  finally show "d y + |x⇧⋆⟩ A x y ≤ |x⇧⋆⟩ y"
    by simp
qed

lemma fbox_segerberg [simp]: "d y ⋅ |x⇧⋆] ( |x] y + ad y ) = |x⇧⋆] y"
proof -
  have "|x⇧⋆] ( |x] y + ad y ) = d ( |x⇧⋆] ( |x] y + ad y ) )"
    using local.a_d_closed local.ads_d_def local.apd_d_def local.fbox_def by auto
  hence f1: "|x⇧⋆] ( |x] y + ad y ) = ad ( |x⇧⋆⟩ (A x (ad y)) )"
    by (simp add: a_A local.fdia_fbox_de_morgan_2)
  have "ad y + |x⇧⋆⟩ (A x (ad y)) = |x⇧⋆⟩ ad y"
    by (metis fsegerberg local.a_d_closed local.ads_d_def local.apd_d_def)
  thus ?thesis
    by (metis f1 local.ads_d_def local.ans4 local.fbox_simp local.fdia_fbox_de_morgan_2)
qed

subsection ‹Wellfoundedness and Loeb's Formula›

text ‹This example is taken from~\<^cite>‹"DesharnaisStruthSCP"›.›

definition Omega :: "'a ⇒ 'a ⇒ 'a" ("Ω")
  where "Ω x y = d y ⋅ ad (x ⋅ y)"

text ‹If $y$ is a set, then $\Omega(x,y)$ describes those elements in $y$ from which no further $x$ transitions are possible.›

lemma omega_fdia: "Ω x y = d y ⋅ ad ( |x⟩ y )"
  using Omega_def local.a_d_closed local.ads_d_def local.apd_d_def local.dka.fd_def by auto

lemma omega_fbox: "Ω x y = d y ⋅ |x] (ad y)"
  by (simp add: fdia_fbox_de_morgan_2 omega_fdia)

lemma omega_absorb1 [simp]: "Ω x y ⋅ ad ( |x⟩ y ) = Ω x y"
  by (simp add: mult_assoc omega_fdia)

lemma omega_absorb2 [simp]: "Ω x y ⋅ ad (x ⋅ y) = Ω x y"
  by (simp add: Omega_def mult_assoc)

lemma omega_le_1: "Ω x y ≤ d y"
  by (simp add: Omega_def d_a_galois1)

lemma omega_subid: "Ω x (d y) ≤ d y"
  by (simp add: Omega_def local.a_subid_aux2)

lemma omega_le_2: "Ω x y ≤ ad ( |x⟩ y )"
  by (simp add: local.dka.dom_subid_aux2 omega_fdia)

lemma omega_dom [simp]: "d (Ω x y) = Ω x y"
  using Omega_def local.a_d_closed local.ads_d_def local.apd_d_def by auto

lemma a_omega: "ad (Ω x y) = ad y + |x⟩ y"
  by (simp add: Omega_def local.a_6 local.ds.fd_def)

lemma omega_fdia_3 [simp]: "d y ⋅ ad (Ω x y) = d y ⋅ |x⟩ y"
  using Omega_def local.ads_d_def local.fdia_def local.s4 by presburger

lemma omega_zero_equiv_1: "Ω x y = 0 ⟷ d y ≤ |x⟩ y"
  by (simp add: Omega_def local.a_gla local.ads_d_def local.fdia_def)

definition Loebian :: "'a ⇒ bool"
  where "Loebian x = (∀y. |x⟩ y ≤ |x⟩ Ω x y)"

definition PreLoebian :: "'a ⇒ bool"
  where "PreLoebian x = (∀y. d y ≤ |x⇧⋆⟩ Ω x y)"

definition Noetherian :: "'a ⇒ bool"
  where "Noetherian x = (∀y. Ω x y = 0 ⟶ d y = 0)"

lemma noetherian_alt: "Noetherian x ⟷ (∀y. d y ≤ |x⟩ y ⟶ d y = 0)"
  by (simp add: Noetherian_def omega_zero_equiv_1)

lemma Noetherian_iff_PreLoebian: "Noetherian x ⟷ PreLoebian x"
proof
  assume hyp: "Noetherian x"
  {
    fix y
    have "d y ⋅ ad ( |x⇧⋆⟩ Ω x y ) = d y ⋅ ad (Ω x y + |x⟩ |x⇧⋆⟩ Ω x y)"
      by (metis local.dka.fdia_star_unfold_var omega_dom)
    also have "... = d y ⋅ ad (Ω x y) ⋅ ad ( |x⟩ |x⇧⋆⟩ Ω x y )"
      using ans4 mult_assoc by presburger
    also have "... ≤ |x⟩ d y ⋅ ad ( |x⟩ |x⇧⋆⟩ Ω x y )"
      by (simp add: local.dka.dom_subid_aux2 local.mult_isor)
    also have "... ≤ |x⟩ (d y ⋅ ad ( |x⇧⋆⟩ Ω x y ))"
      by (simp add: local.dia_diff)
    finally have "d y ⋅ ad ( |x⇧⋆⟩ Ω x y ) ≤ |x⟩ (d y ⋅ ad ( |x⇧⋆⟩ Ω x y ))"
      by blast
    hence "d y ⋅ ad ( |x⇧⋆⟩ Ω x y ) = 0"
      by (metis hyp local.ads_d_def local.dpdz.dom_mult_closed local.fdia_def noetherian_alt)
    hence "d y ≤ |x⇧⋆⟩ Ω x y"
      by (simp add: local.a_gla local.ads_d_def local.dka.fd_def)
  }
  thus "PreLoebian x"
    using PreLoebian_def by blast
next
  assume a: "PreLoebian x"
  {
    fix y
    assume b: "Ω x y = 0"
    hence "d y ≤ |x⟩ d y"
      using omega_zero_equiv_1 by auto
    hence "d y = 0"
      by (metis (no_types) PreLoebian_def a b a_one a_zero add_zeror annir fdia_def less_eq_def)
  }
  thus "Noetherian x"
    by (simp add: Noetherian_def)
qed

lemma Loebian_imp_Noetherian: "Loebian x ⟹ Noetherian x"
proof -
  assume a: "Loebian x"
  {
    fix y
    assume b: "Ω x y = 0"
    hence "d y ≤ |x⟩ d y"
      using omega_zero_equiv_1 by auto
    also have "... ≤ |x⟩ (Ω x y)"
      using Loebian_def a by auto
    finally have "d y = 0"
      by (simp add: b order.antisym fdia_def)
  }
  thus "Noetherian x"
    by (simp add: Noetherian_def)
qed

lemma d_transitive: "(∀y. |x⟩ |x⟩ y ≤ |x⟩ y) ⟹ (∀y. |x⟩ y = |x⇧⋆⟩ |x⟩ y)"
proof -
  assume a: "∀y. |x⟩ |x⟩ y ≤ |x⟩ y"
  {
    fix y
    have "|x⟩ y + |x⟩ |x⟩ y ≤ |x⟩ y"
      by (simp add: a)
    hence "|x⇧⋆⟩ |x⟩ y ≤ |x⟩ y"
      using local.dka.fd_def local.dka.fdia_star_induct_var by auto
    have "|x⟩ y ≤ |x⇧⋆⟩ |x⟩ y"
      using local.dka.fd_def local.order_prop opti_iterate by force
  }
  thus ?thesis
    using a order.antisym dka.fd_def dka.fdia_star_induct_var by auto
qed

lemma d_transitive_var: "(∀y. |x⟩ |x⟩ y ≤ |x⟩ y) ⟹ (∀y. |x⟩ y = |x⟩ |x⇧⋆⟩ y)"
proof -
  assume "∀y. |x⟩ |x⟩ y ≤ |x⟩ y"
  then have "∀a. |x⟩ |x⇧⋆⟩ a = |x⟩ a"
    by (metis (full_types) d_transitive local.dka.fd_def local.dka.fdia_d_simp local.star_slide_var mult_assoc)
  then show ?thesis
    by presburger
qed

lemma d_transitive_PreLoebian_imp_Loebian: "(∀y. |x⟩ |x⟩ y ≤ |x⟩ y) ⟹ PreLoebian x ⟹ Loebian x"
proof -
  assume wt: "(∀y. |x⟩ |x⟩ y ≤ |x⟩ y)"
  and "PreLoebian x"
  hence "∀y. |x⟩ y ≤ |x⟩ |x⇧⋆⟩ Ω x y"
    using PreLoebian_def local.ads_d_def local.dka.fd_def local.ds.fd_iso1 by auto
  hence "∀y. |x⟩ y ≤ |x⟩ Ω x y"
    by (metis wt d_transitive_var)
  then show "Loebian x"
    using Loebian_def fdia_def by auto
qed

lemma d_transitive_Noetherian_iff_Loebian: "∀y. |x⟩ |x⟩ y ≤ |x⟩ y ⟹ Noetherian x ⟷ Loebian x"
  using Loebian_imp_Noetherian Noetherian_iff_PreLoebian d_transitive_PreLoebian_imp_Loebian by blast

lemma Loeb_iff_box_Loeb: "Loebian x ⟷ (∀y. |x] (ad ( |x] y ) + d y) ≤ |x] y)"
proof -
  have "Loebian x ⟷ (∀y. |x⟩ y ≤ |x⟩ (d y ⋅ |x] (ad y)))"
    using Loebian_def omega_fbox by auto
  also have "... ⟷ (∀y. ad ( |x⟩ (d y ⋅ |x] (ad y)) ) ≤ ad ( |x⟩ y ))"
    using a_antitone' fdia_def by fastforce
  also have "... ⟷ (∀y. |x] ad (d y ⋅ |x] (ad y)) ≤ |x] (ad y))"
    by (simp add: fdia_fbox_de_morgan_2)
  also have "... ⟷ (∀y. |x] (d (ad y) + ad ( |x] (ad y) )) ≤ |x] (ad y))"
    by (simp add: local.ads_d_def local.fbox_def)
  finally show ?thesis
    by (metis add_commute local.a_d_closed local.ads_d_def local.apd_d_def local.fbox_def)
qed

end

subsection ‹Divergence Kleene Algebras and Separation of Termination›

text ‹The notion of divergence has been added to modal Kleene algebras in~\<^cite>‹"DesharnaisMoellerStruthLMCS"›.
More facts about divergence could be added in the future. Some could be adapted from omega algebras.›

class nabla_op =
  fixes nabla :: "'a ⇒ 'a" ("∇_" [999] 1000)

class fdivergence_kleene_algebra = antidomain_kleene_algebra + nabla_op +
  assumes nabla_closure [simp]: "d ∇ x = ∇ x"
  and nabla_unfold: "∇ x ≤ |x⟩ ∇ x"
  and nabla_coinduction: "d y ≤ |x⟩ y + d z ⟹ d y ≤ ∇ x + |x⇧⋆⟩ z"

begin

lemma nabla_coinduction_var: "d y ≤ |x⟩ y ⟹ d y ≤ ∇ x"
proof -
  assume "d y ≤ |x⟩ y"
  hence "d y ≤ |x⟩ y + d 0"
    by simp
  hence "d y ≤ ∇ x + |x⇧⋆⟩ 0"
    using nabla_coinduction by blast
  thus "d y ≤ ∇ x"
    by (simp add: fdia_def)
qed

lemma nabla_unfold_eq [simp]: "|x⟩ ∇ x = ∇ x"
proof -
  have f1: "ad (ad (x ⋅ ∇x)) = ad (ad (x ⋅ ∇x)) + ∇x"
    using local.ds.fd_def local.join.sup.order_iff local.nabla_unfold by presburger
  then have "ad (ad (x ⋅ ∇x)) ⋅ ad (ad ∇x) = ∇x"
    by (metis local.ads_d_def local.dpdz.dns5 local.dpdz.dsg4 local.join.sup_commute local.nabla_closure)
  then show ?thesis
    using f1 by (metis local.ads_d_def local.ds.fd_def local.ds.fd_subdist_2 local.join.sup.order_iff local.join.sup_commute nabla_coinduction_var)
qed

lemma nabla_subdist: "∇ x ≤ ∇ (x + y)"
proof -
  have "d ∇ x ≤ ∇ (x + y)"
    by (metis local.ds.fd_iso2 local.join.sup.cobounded1 local.nabla_closure nabla_coinduction_var nabla_unfold_eq)
  thus ?thesis
    by simp
qed

lemma nabla_iso: "x ≤ y ⟹ ∇ x ≤ ∇ y"
  by (metis less_eq_def nabla_subdist)

lemma nabla_omega: "Ω x (d y) = 0 ⟹ d y ≤ ∇ x"
  using omega_zero_equiv_1 nabla_coinduction_var by fastforce

lemma nabla_noether: "∇ x = 0 ⟹ Noetherian x"
  using local.join.le_bot local.noetherian_alt nabla_coinduction_var by blast

lemma nabla_preloeb: "∇ x = 0 ⟹ PreLoebian x"
  using Noetherian_iff_PreLoebian nabla_noether by auto

lemma star_nabla_1 [simp]: "|x⇧⋆⟩ ∇ x = ∇ x"
proof (rule order.antisym)
  show "|x⇧⋆⟩ ∇ x ≤ ∇ x"
    by (metis dka.fdia_star_induct_var order.eq_iff nabla_closure nabla_unfold_eq)
  show "∇ x ≤ |x⇧⋆⟩ ∇ x"
    by (metis ds.fd_iso2 star_ext nabla_unfold_eq)
qed

lemma nabla_sum_expand [simp]: "|x⟩ ∇ (x + y) + |y⟩ ∇ (x + y) = ∇ (x + y)"
proof -
  have "d ((x + y) ⋅ ∇(x + y)) = ∇(x + y)"
    using local.dka.fd_def nabla_unfold_eq by presburger
  thus ?thesis
    by (simp add: local.dka.fd_def)
qed

lemma wagner_3:
  assumes "d z + |x⟩ ∇ (x + y) = ∇ (x + y)"
  shows "∇ (x + y) = ∇ x + |x⇧⋆⟩ z"
proof (rule order.antisym)
  have "d ∇(x + y) ≤ d z + |x⟩ ∇(x + y)"
    by (simp add: assms)
  thus "∇ (x + y) ≤ ∇ x + |x⇧⋆⟩ z"
    by (metis add_commute nabla_closure nabla_coinduction)
  have "d z + |x⟩ ∇ (x + y) ≤ ∇ (x + y)"
    using assms by auto
  hence "|x⇧⋆⟩ z ≤ ∇ (x + y)"
    by (metis local.dka.fdia_star_induct local.nabla_closure)
  thus "∇ x + |x⇧⋆⟩ z ≤ ∇ (x + y)"
    by (simp add: sup_least nabla_subdist)
qed

lemma nabla_sum_unfold [simp]: "∇ x + |x⇧⋆⟩ |y⟩ ∇ (x + y) = ∇ (x + y)"
proof -
  have "∇ (x + y) = |x⟩ ∇ (x + y) + |y⟩ ∇ (x + y)"
    by simp
  thus ?thesis
    by (metis add_commute local.dka.fd_def local.ds.fd_def local.ds.fdia_d_simp wagner_3)
qed

lemma nabla_separation: "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ ⟹ (∇ (x + y) = ∇ x + |x⇧⋆⟩ ∇ y)"
proof (rule order.antisym)
  assume quasi_comm: "y ⋅ x ≤ x ⋅ (x + y)⇧⋆"
  hence a: "y⇧⋆ ⋅ x ≤ x ⋅ (x + y)⇧⋆"
    using quasicomm_var by blast
  have "∇ (x + y) = ∇ y + |y⇧⋆⋅ x⟩ ∇ (x + y)"
    by (metis local.ds.fdia_mult local.join.sup_commute nabla_sum_unfold)
  also have "... ≤ ∇ y + |x ⋅ (x + y)⇧⋆⟩ ∇ (x + y)"
    using a local.ds.fd_iso2 local.join.sup.mono by blast
  also have "... = ∇ y + |x⟩ |(x + y)⇧⋆⟩ ∇ (x + y)"
    by (simp add: fdia_def mult_assoc)
  finally have "∇ (x + y) ≤ ∇ y + |x⟩ ∇ (x + y)"
    by (metis star_nabla_1)
  thus "∇ (x + y) ≤ ∇ x + |x⇧⋆⟩ ∇ y"
    by (metis add_commute nabla_closure nabla_coinduction)
next
  have "∇ x + |x⇧⋆⟩ ∇ y = ∇ x + |x⇧⋆⟩ |y⟩ ∇ y"
    by simp
  also have "... = ∇ x + |x⇧⋆ ⋅ y⟩ ∇ y"
    by (simp add: fdia_def mult_assoc)
  also have "... ≤ ∇ x + |x⇧⋆ ⋅ y⟩ ∇ (x + y)"
    using dpdz.dom_iso eq_refl fdia_def join.sup_ge2 join.sup_mono mult_isol nabla_iso by presburger
  also have "... = ∇ x + |x⇧⋆⟩ |y⟩ ∇ (x + y)"
    by (simp add: fdia_def mult_assoc)
  finally show "∇ x + |x⇧⋆⟩ ∇ y ≤ ∇ (x + y)"
    by (metis nabla_sum_unfold)
qed

text ‹The next lemma is a separation of termination theorem by Bachmair and Dershowitz~\<^cite>‹"bachmair86commutation"›.›

lemma bachmair_dershowitz: "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ ⟹ ∇ x + ∇ y = 0 ⟷ ∇ (x + y) = 0"
proof -
  assume quasi_comm: "y ⋅ x ≤ x ⋅ (x + y)⇧⋆"
  have "∀x. |x⟩ 0 = 0"
    by (simp add: fdia_def)
  hence "∇y = 0 ⟹ ∇x + ∇y = 0 ⟷ ∇(x + y) = 0"
    using quasi_comm nabla_separation by presburger
  thus ?thesis
    using add_commute local.join.le_bot nabla_subdist by fastforce
qed

text ‹The next lemma is a more complex separation of termination theorem by Doornbos,
Backhouse and van der Woude~\<^cite>‹"doornbos97calculational"›.›

lemma separation_of_termination:
assumes "y ⋅ x ≤ x ⋅ (x + y)⇧⋆ + y"
shows "∇ x + ∇ y = 0 ⟷ ∇ (x + y) = 0"
proof
  assume xy_wf: "∇ x + ∇ y = 0"
  hence x_preloeb: "∇ (x + y) ≤ |x⇧⋆⟩ Ω x (∇ (x + y))"
    by (metis PreLoebian_def no_trivial_inverse nabla_closure nabla_preloeb)
  hence y_div: "∇ y = 0"
    using add_commute no_trivial_inverse xy_wf by blast
  have "∇ (x + y) ≤ |y⟩ ∇ (x + y) + |x⟩ ∇ (x + y)"
    by (simp add: local.join.sup_commute)
  hence "∇ (x + y) ⋅ ad ( |x⟩ ∇ (x + y) ) ≤ |y⟩ ∇(x + y)"
    by (simp add: local.da_shunt1 local.dka.fd_def local.join.sup_commute)
  hence "Ω x ∇(x + y) ≤ |y⟩ ∇ (x + y)"
    by (simp add: fdia_def omega_fdia)
  also have "... ≤ |y⟩ |x⇧⋆⟩ (Ω x ∇(x + y))"
    using local.dpdz.dom_iso local.ds.fd_iso1 x_preloeb by blast
  also have "... = |y ⋅ x⇧⋆⟩ (Ω x ∇(x + y))"
    by (simp add: fdia_def mult_assoc)
  also have "... ≤ |x ⋅ (x + y)⇧⋆ + y⟩ (Ω x ∇(x + y))"
    using assms local.ds.fd_iso2 local.lazycomm_var by blast
  also have "... = |x ⋅ (x + y)⇧⋆⟩ (Ω x ∇(x + y)) + |y⟩ (Ω x ∇(x + y))"
    by (simp add: local.dka.fd_def)
  also have "... ≤ |(x ⋅ (x + y)⇧⋆)⟩ ∇(x + y) + |y⟩ (Ω x ∇(x + y))"
    using local.add_iso local.dpdz.domain_1'' local.ds.fd_iso1 local.omega_fdia by auto
  also have "... ≤ |x⟩ |(x + y)⇧⋆⟩ ∇(x + y) + |y⟩ (Ω x ∇(x + y))"
    by (simp add: fdia_def mult_assoc)
  finally have "Ω x ∇(x + y) ≤ |x⟩ ∇(x + y) + |y⟩ (Ω x ∇(x + y))"
    by (metis star_nabla_1)
  hence "Ω x ∇(x + y) ⋅ ad ( |x⟩ ∇(x + y) ) ≤ |y⟩ (Ω x ∇(x + y))"
    by (simp add: local.da_shunt1 local.dka.fd_def)
  hence "Ω x ∇(x + y) ≤ |y⟩ (Ω x ∇(x + y))"
    by (simp add: omega_fdia mult_assoc)
  hence "(Ω x ∇(x + y)) = 0"
    by (metis noetherian_alt omega_dom nabla_noether y_div)
  thus "∇ (x + y) = 0"
    using local.dka.fd_def local.join.le_bot x_preloeb by auto
next
  assume "∇ (x + y) = 0"
  thus "(∇ x) + (∇ y) = 0"
    by (metis local.join.le_bot local.join.sup.order_iff local.join.sup_commute nabla_subdist)
qed

text ‹The final examples can be found in~\<^cite>‹"guttmannstruthweber11algmeth"›.›

definition T :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("_ ↝ _ ↝ _" [61,61,61] 60)
  where "p↝x↝q ≡ ad p + |x] d q"

lemma T_d [simp]: "d (p↝x↝q) = p↝x↝q"
  using T_def local.a_d_add_closure local.fbox_def by auto

lemma T_p: "d p ⋅ (p↝x↝q) = d p ⋅ |x] d q"
proof -
  have "d p ⋅ (p↝x↝q) = ad (ad p + ad (p↝x↝q))"
    using T_d local.ads_d_def by auto
  thus ?thesis
    using T_def add_commute local.a_mult_add local.ads_d_def by auto
qed

lemma T_a [simp]: "ad p ⋅ (p↝x↝q) = ad p"
  by (metis T_d T_def local.a_d_closed local.ads_d_def local.apd_d_def local.dpdz.dns5 local.join.sup.left_idem)

lemma T_seq: "(p↝x↝q) ⋅ |x](q↝y↝s) ≤ p↝x ⋅ y↝s"
proof -
  have f1: "|x] q = |x] d q"
    using local.fbox_simp by auto
  have "ad p ⋅ ad (x ⋅ ad (q↝y↝s)) + |x] d q ⋅ |x] (ad q + |y] d s) ≤ ad p + |x] d q ⋅ |x] (ad q + |y] d s)"
    using local.a_subid_aux2 local.add_iso by blast
  hence "(p↝x↝q) ⋅ |x](q↝y↝s) ≤ ad p + |x](d q ⋅ (q↝y↝s))"
    by (metis T_d T_def f1 local.distrib_right' local.fbox_add1 local.fbox_def)
  also have "... = ad p + |x](d q ⋅ (ad q + |y] d s))"
    by (simp add: T_def)
  also have "... = ad p + |x](d q ⋅ |y] d s)"
    using T_def T_p by auto
  also have "... ≤ ad p + |x] |y] d s"
    by (metis (no_types, lifting) dka.dom_subid_aux2 dka.dsg3 order.eq_iff fbox_iso join.sup.mono)
  finally show ?thesis
    by (simp add: T_def fbox_mult)
qed

lemma T_square: "(p↝x↝q) ⋅ |x](q↝x↝p) ≤ p↝x⋅x↝p"
  by (simp add: T_seq)

lemma T_segerberg [simp]: "d p ⋅ |x⇧⋆](p↝x↝p) = |x⇧⋆] d p"
  using T_def add_commute local.fbox_segerberg local.fbox_simp by force

lemma lookahead [simp]: "|x⇧⋆](d p ⋅ |x] d p) = |x⇧⋆] d p"
  by (metis (full_types) local.dka.dsg3 local.fbox_add1 local.fbox_mult local.fbox_simp local.fbox_star_unfold_var local.star_slide_var local.star_trans_eq)

lemma alternation: "d p ⋅ |x⇧⋆]((p↝x↝q) ⋅ (q↝x↝p)) = |(x⋅x)⇧⋆](d p ⋅ (q↝x↝p)) ⋅ |x⋅(x⋅x)⇧⋆](d q ⋅ (p↝x↝q))"
proof -
  have fbox_simp_2: "⋀x p. |x]p = d( |x] p )"
    using local.a_d_closed local.ads_d_def local.apd_d_def local.fbox_def by fastforce
  have "|(x⋅x)⇧⋆]((p↝x↝q) ⋅ |x](q↝x↝p) ⋅ (q↝x↝p) ⋅ |x](p↝x↝q)) ≤ |(x⋅x)⇧⋆]((p↝x↝q) ⋅ |x](q↝x↝p))"
    using local.dka.domain_1'' local.fbox_iso local.order_trans by blast
  also have "... ≤ |(x⋅x)⇧⋆](p↝x⋅x↝p)"
    using T_seq local.dka.dom_iso local.fbox_iso by blast
  finally have 1: "|(x⋅x)⇧⋆]((p↝x↝q) ⋅ |x](q↝x↝p) ⋅ (q↝x↝p) ⋅ |x](p↝x↝q)) ≤ |(x⋅x)⇧⋆](p↝x⋅x↝p)".
  have "d p ⋅ |x⇧⋆]((p↝x↝q) ⋅ (q↝x↝p)) = d p ⋅ |1+x] |(x⋅x)⇧⋆]((p↝x↝q) ⋅ (q↝x↝p))"
    by (metis (full_types) fbox_mult meyer_1)
  also have "... = d p ⋅ |(x⋅x)⇧⋆]((p↝x↝q) ⋅ (q↝x↝p)) ⋅ |x⋅(x⋅x)⇧⋆]((p↝x↝q) ⋅ (q↝x↝p))"
    using fbox_simp_2 fbox_mult fbox_add2 mult_assoc by auto
  also have "... = d p ⋅ |(x⋅x)⇧⋆]((p↝x↝q) ⋅ (q↝x↝p)) ⋅ |(x⋅x)⇧⋆⋅x]((p↝x↝q) ⋅ (q↝x↝p))"
    by (simp add: star_slide)
  also have "... = d p ⋅ |(x⋅x)⇧⋆]((p↝x↝q) ⋅ (q↝x↝p)) ⋅ |(x⋅x)⇧⋆] |x]((p↝x↝q) ⋅ (q↝x↝p))"
    by (simp add: fbox_mult)
  also have "... = d p ⋅ |(x⋅x)⇧⋆]((p↝x↝q) ⋅ (q↝x↝p) ⋅ |x]((p↝x↝q) ⋅ (q↝x↝p)))"
    by (metis T_d fbox_simp_2 local.dka.dom_mult_closed local.fbox_add1 mult_assoc)
  also have "... = d p ⋅ |(x⋅x)⇧⋆]((p↝x↝q) ⋅ |x](q↝x↝p) ⋅ (q↝x↝p) ⋅ |x](p↝x↝q))"
  proof -
    have f1: "d ((q ↝ x ↝ p) ⋅ |x] (p ↝ x ↝ q)) = (q ↝ x ↝ p) ⋅ |x] (p ↝ x ↝ q)"
      by (metis (full_types) T_d fbox_simp_2 local.dka.dsg3)
    then have "|(x ⋅ x)⇧⋆] (d ( |x] (q ↝ x ↝ p)) ⋅ ((q ↝ x ↝ p) ⋅ |x] (p ↝ x ↝ q))) = |(x ⋅ x)⇧⋆] d ( |x] (q ↝ x ↝ p)) ⋅ |(x ⋅ x)⇧⋆] ((q ↝ x ↝ p) ⋅ |x] (p ↝ x ↝ q))"
      by (metis (full_types) fbox_simp_2 local.fbox_add1)
    then have f2: "|(x ⋅ x)⇧⋆] (d ( |x] (q ↝ x ↝ p)) ⋅ ((q ↝ x ↝ p) ⋅ |x] (p ↝ x ↝ q))) = ad ((x ⋅ x)⇧⋆ ⋅ ad ((q ↝ x ↝ p) ⋅ |x] (p ↝ x ↝ q)) + (x ⋅ x)⇧⋆ ⋅ ad (d ( |x] (q ↝ x ↝ p))))"
      by (simp add: add_commute local.fbox_def)
    have "d ( |x] (p ↝ x ↝ q)) ⋅ d ( |x] (q ↝ x ↝ p)) = |x] ((p ↝ x ↝ q) ⋅ (q ↝ x ↝ p))"
      by (metis (no_types) T_d fbox_simp_2 local.fbox_add1)
    then have "d ((q ↝ x ↝ p) ⋅ |x] (p ↝ x ↝ q)) ⋅ d (d ( |x] (q ↝ x ↝ p))) = (q ↝ x ↝ p) ⋅ |x] ((p ↝ x ↝ q) ⋅ (q ↝ x ↝ p))"
      using f1 fbox_simp_2 mult_assoc by force
    then have "|(x ⋅ x)⇧⋆] (d ( |x] (q ↝ x ↝ p)) ⋅ ((q ↝ x ↝ p) ⋅ |x] (p ↝ x ↝ q))) = |(x ⋅ x)⇧⋆] ((q ↝ x ↝ p) ⋅ |x] ((p ↝ x ↝ q) ⋅ (q ↝ x ↝ p)))"
      using f2 by (metis (no_types) local.ans4 local.fbox_add1 local.fbox_def)
    then show ?thesis
      by (metis (no_types) T_d fbox_simp_2 local.dka.dsg3 local.fbox_add1 mult_assoc)
  qed
  also have "... = d p ⋅ |(x⋅x)⇧⋆](p↝x⋅x↝p) ⋅ |(x⋅x)⇧⋆]((p↝x↝q) ⋅ |x](q↝x↝p) ⋅ (q↝x↝p) ⋅ |x](p↝x↝q))" using "1"
    by (metis fbox_simp_2 dka.dns5 dka.dsg4 join.sup.absorb2 mult_assoc)
  also have "... = |(x⋅x)⇧⋆](d p ⋅ (p↝x↝q) ⋅ |x](q↝x↝p) ⋅ (q↝x↝p) ⋅ |x](p↝x↝q))"
    using T_segerberg local.a_d_closed local.ads_d_def local.apd_d_def local.distrib_left local.fbox_def mult_assoc by auto
  also have "... = |(x⋅x)⇧⋆](d p ⋅ |x] d q ⋅ |x](q↝x↝p) ⋅ (q↝x↝p) ⋅ |x](p↝x↝q))"
    by (simp add: T_p)
  also have "... = |(x⋅x)⇧⋆](d p ⋅ |x] d q ⋅ |x] |x] d p ⋅ (q↝x↝p) ⋅ |x](p↝x↝q))"
    by (metis T_d T_p fbox_simp_2 fbox_add1 fbox_simp mult_assoc)
  also have "... = |(x⋅x)⇧⋆](d p ⋅ |x⋅x] d p ⋅ (q↝x↝p) ⋅ |x] d q ⋅ |x](p↝x↝q))"
  proof -
    have f1: "ad (x ⋅ ad ( |x] d p)) = |x ⋅ x] d p"
      using local.fbox_def local.fbox_mult by presburger
    have f2: "ad (d q ⋅ d (x ⋅ ad (d p))) = q ↝ x ↝ p"
      by (simp add: T_def local.a_de_morgan_var_4 local.fbox_def)
    have "ad q + |x] d p = ad (d q ⋅ d (x ⋅ ad (d p)))"
      by (simp add: local.a_de_morgan_var_4 local.fbox_def)
    then have "ad (x ⋅ ad ( |x] d p)) ⋅ ((q ↝ x ↝ p) ⋅ |x] d q) = ad (x ⋅ ad ( |x] d p)) ⋅ ad (x ⋅ ad (d q)) ⋅ (ad q + |x] d p)"
      using f2 by (metis (no_types) local.am2 local.fbox_def mult_assoc)
    then show ?thesis
      using f1 by (simp add: T_def local.am2 local.fbox_def mult_assoc)
  qed
  also have "... = |(x⋅x)⇧⋆](d p ⋅ |x⋅x] d p ⋅ (q↝x↝p) ⋅ |x](d q ⋅ (p↝x↝q)))"
    using local.a_d_closed local.ads_d_def local.apd_d_def local.distrib_left local.fbox_def mult_assoc by auto
  also have "... = |(x⋅x)⇧⋆](d p ⋅ |x⋅x] d p) ⋅ |(x⋅x)⇧⋆](q↝x↝p) ⋅ |(x⋅x)⇧⋆] |x](d q ⋅ (p↝x↝q))"
    by (metis T_d fbox_simp_2 local.dka.dom_mult_closed local.fbox_add1)
  also have "... = |(x⋅x)⇧⋆](d p ⋅ (q↝x↝p)) ⋅ |(x⋅x)⇧⋆] |x] (d q ⋅ (p↝x↝q))"
    by (metis T_d local.fbox_add1 local.fbox_simp lookahead)
  finally show ?thesis
    by (metis fbox_mult star_slide)
qed

lemma "|(x⋅x)⇧⋆] d p ⋅ |x⋅(x⋅x)⇧⋆] ad p = d p ⋅ |x⇧⋆]((p↝x↝ad p) ⋅ (ad p↝x↝p))"
  using alternation local.a_d_closed local.ads_d_def local.apd_d_def by auto

lemma "|x⇧⋆] d p = d p ⋅ |x⇧⋆](p↝x↝p)"
  by (simp add: alternation)

end

end