Theory N_Semirings_Modal

(* Title:      Modal N-Semirings
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section Modal N-Semirings

theory N_Semirings_Modal

imports N_Semirings_Boolean

begin

class n_diamond_semiring = n_semiring + diamond +
  assumes ndiamond_def: "|x>y = n(x * y * L)"
begin

lemma diamond_x_bot:
  "|x>bot = n(x)"
  using n_mult_bot ndiamond_def mult_assoc by auto

lemma diamond_x_1:
  "|x>1 = n(x * L)"
  by (simp add: ndiamond_def)

lemma diamond_x_L:
  "|x>L = n(x * L)"
  by (simp add: L_left_zero ndiamond_def mult_assoc)

lemma diamond_x_top:
  "|x>top = n(x * L)"
  by (metis mult_assoc n_top_L ndiamond_def top_mult_top)

lemma diamond_x_n:
  "|x>n(y) = n(x * y)"
  by (simp add: n_mult ndiamond_def)

lemma diamond_bot_y:
  "|bot>y = bot"
  by (simp add: n_bot ndiamond_def)

lemma diamond_1_y:
  "|1>y = n(y * L)"
  by (simp add: ndiamond_def)

lemma diamond_1_n:
  "|1>n(y) = n(y)"
  by (simp add: diamond_1_y n_n_L)

lemma diamond_L_y:
  "|L>y = 1"
  by (simp add: L_left_zero n_L ndiamond_def)

lemma diamond_top_y:
  "|top>y = 1"
  by (metis sup_left_top sup_right_top diamond_L_y mult_right_dist_sup n_dist_sup n_top ndiamond_def)

lemma diamond_n_y:
  "|n(x)>y = n(x) * n(y * L)"
  by (simp add: n_export ndiamond_def mult_assoc)

lemma diamond_n_bot:
  "|n(x)>bot = bot"
  by (simp add: n_bot n_mult_right_bot ndiamond_def)

lemma diamond_n_1:
  "|n(x)>1 = n(x)"
  using diamond_1_n diamond_1_y diamond_x_1 by auto

lemma diamond_n_n:
  "|n(x)>n(y) = n(x) * n(y)"
  by (simp add: diamond_x_n n_export)

lemma diamond_n_n_same:
  "|n(x)>n(x) = n(x)"
  by (simp add: diamond_n_n n_mult_idempotent)

text Theorem 23.1

lemma diamond_left_dist_sup:
  "|x  y>z = |x>z  |y>z"
  by (simp add: mult_right_dist_sup n_dist_sup ndiamond_def)

text Theorem 23.2

lemma diamond_right_dist_sup:
  "|x>(y  z) = |x>y  |x>z"
  by (simp add: mult_left_dist_sup n_dist_sup ndiamond_def semiring.distrib_right)

text Theorem 23.3

lemma diamond_associative:
  "|x * y>z = |x>(y * z)"
  by (simp add: ndiamond_def mult_assoc)

text Theorem 23.3

lemma diamond_left_mult:
  "|x * y>z = |x>|y>z"
  using n_mult_ni ndiamond_def ni_def mult_assoc by auto

lemma diamond_right_mult:
  "|x>(y * z) = |x>|y>z"
  using diamond_associative diamond_left_mult by force

lemma diamond_n_export:
  "|n(x) * y>z = n(x) * |y>z"
  by (simp add: n_export ndiamond_def mult_assoc)

lemma diamond_diamond_export:
  "||x>y>z = |x>y * |z>1"
  using diamond_n_y ndiamond_def by auto

lemma diamond_left_isotone:
  "x  y  |x>z  |y>z"
  by (metis diamond_left_dist_sup le_iff_sup)

lemma diamond_right_isotone:
  "y  z  |x>y  |x>z"
  by (metis diamond_right_dist_sup le_iff_sup)

lemma diamond_isotone:
  "w  y  x  z  |w>x  |y>z"
  by (meson diamond_left_isotone diamond_right_isotone order_trans)

definition ndiamond_L :: "'a  'a  'a" (" _ » _" [50,90] 95)
  where "x»y  n(x * y) * L"

lemma ndiamond_to_L:
  "x»y = |x>n(y) * L"
  by (simp add: diamond_x_n ndiamond_L_def)

lemma ndiamond_from_L:
  "|x>y = n(x»(y * L))"
  by (simp add: n_n_L ndiamond_def mult_assoc ndiamond_L_def)

lemma diamond_L_ni:
  "x»y = ni(x * y)"
  by (simp add: ni_def ndiamond_L_def)

lemma diamond_L_associative:
  "x * y»z = x»(y * z)"
  by (simp add: diamond_L_ni mult_assoc)

lemma diamond_L_left_mult:
  "x * y»z = x»y»z"
  using diamond_L_associative diamond_L_ni ni_mult by auto

lemma diamond_L_right_mult:
  "x»(y * z) = x»y»z"
  using diamond_L_associative diamond_L_left_mult by auto

lemma diamond_L_left_dist_sup:
  "x  y»z = x»z  y»z"
  by (simp add: diamond_L_ni mult_right_dist_sup ni_dist_sup)

lemma diamond_L_x_ni:
  "x»ni(y) = ni(x * y)"
  using n_mult_ni ni_def ndiamond_L_def by auto

lemma diamond_L_left_isotone:
  "x  y  x»z  y»z"
  using mult_left_isotone ni_def ni_isotone ndiamond_L_def by auto

lemma diamond_L_right_isotone:
  "y  z  x»y  x»z"
  using mult_right_isotone ni_def ni_isotone ndiamond_L_def by auto

lemma diamond_L_isotone:
  "w  y  x  z  w»x  y»z"
  using diamond_L_ni mult_isotone ni_isotone by force

end

class n_box_semiring = n_diamond_semiring + an_semiring + box +
  assumes nbox_def: "|x]y = an(x * an(y * L) * L)"
begin

text Theorem 23.8

lemma box_diamond:
  "|x]y = an( |x>an(y * L) * L)"
  by (simp add: an_n_L nbox_def ndiamond_def)

text Theorem 23.4

lemma diamond_box:
  "|x>y = an( |x]an(y * L) * L)"
  using n_an_def n_mult nbox_def ndiamond_def mult_assoc by force

lemma box_x_bot:
  "|x]bot = an(x * L)"
  by (simp add: an_bot nbox_def)

lemma box_x_1:
  "|x]1 = an(x)"
  using an_L an_mult_an nbox_def mult_assoc by auto

lemma box_x_L:
  "|x]L = an(x)"
  using box_x_1 L_left_zero nbox_def by auto

lemma box_x_top:
  "|x]top = an(x)"
  by (metis box_diamond box_x_1 box_x_bot diamond_top_y)

lemma box_x_n:
  "|x]n(y) = an(x * an(y) * L)"
  by (simp add: an_n_L nbox_def)

lemma box_x_an:
  "|x]an(y) = an(x * y)"
  using an_mult n_an_def nbox_def by auto

lemma box_bot_y:
  "|bot]y = 1"
  by (simp add: an_bot nbox_def)

lemma box_1_y:
  "|1]y = n(y * L)"
  by (simp add: n_an_def nbox_def)

lemma box_1_n:
  "|1]n(y) = n(y)"
  using box_1_y diamond_1_n diamond_1_y by auto

lemma box_1_an:
  "|1]an(y) = an(y)"
  by (simp add: box_x_an)

lemma box_L_y:
  "|L]y = bot"
  by (simp add: L_left_zero an_L nbox_def)

lemma box_top_y:
  "|top]y = bot"
  by (simp add: box_diamond an_L diamond_top_y)

lemma box_n_y:
  "|n(x)]y = an(x)  n(y * L)"
  using an_export_n n_an_def nbox_def mult_assoc by auto

lemma box_an_y:
  "|an(x)]y = n(x)  n(y * L)"
  by (metis an_n_def box_n_y n_an_def)

lemma box_n_bot:
  "|n(x)]bot = an(x)"
  by (simp add: box_x_bot an_n_L)

lemma box_an_bot:
  "|an(x)]bot = n(x)"
  by (simp add: box_x_bot n_an_def)

lemma box_n_1:
  "|n(x)]1 = 1"
  using box_x_1 ani_an_L ani_n by auto

lemma box_an_1:
  "|an(x)]1 = 1"
  using box_x_1 ani_an ani_an_L by fastforce

lemma box_n_n:
  "|n(x)]n(y) = an(x)  n(y)"
  using box_1_n box_1_y box_n_y by auto

lemma box_an_n:
  "|an(x)]n(y) = n(x)  n(y)"
  using box_x_n an_dist_sup n_an_def n_dist_sup by auto

lemma box_n_an:
  "|n(x)]an(y) = an(x)  an(y)"
  by (simp add: box_x_an an_export_n)

lemma box_an_an:
  "|an(x)]an(y) = n(x)  an(y)"
  by (simp add: box_x_an an_export)

lemma box_n_n_same:
  "|n(x)]n(x) = 1"
  by (simp add: box_n_n an_complement)

lemma box_an_an_same:
  "|an(x)]an(x) = 1"
  using box_an_bot an_bot an_complement_bot nbox_def by auto

text Theorem 23.5

lemma box_left_dist_sup:
  "|x  y]z = |x]z * |y]z"
  using an_dist_sup nbox_def semiring.distrib_right by auto

lemma box_right_dist_sup:
  "|x](y  z) = an(x * an(y * L) * an(z * L) * L)"
  by (simp add: an_dist_sup mult_right_dist_sup nbox_def mult_assoc)

lemma box_associative:
  "|x * y]z = an(x * y * an(z * L) * L)"
  by (simp add: nbox_def)

text Theorem 23.7

lemma box_left_mult:
  "|x * y]z = |x]|y]z"
  using box_x_an nbox_def mult_assoc by auto

lemma box_right_mult:
  "|x](y * z) = an(x * an(y * z * L) * L)"
  by (simp add: nbox_def)

text Theorem 23.6

lemma box_right_mult_n_n:
  "|x](n(y) * n(z)) = |x]n(y) * |x]n(z)"
  by (smt an_dist_sup an_export_n an_n_L mult_assoc mult_left_dist_sup mult_right_dist_sup nbox_def)

lemma box_right_mult_an_n:
  "|x](an(y) * n(z)) = |x]an(y) * |x]n(z)"
  by (metis an_n_def box_right_mult_n_n)

lemma box_right_mult_n_an:
  "|x](n(y) * an(z)) = |x]n(y) * |x]an(z)"
  by (simp add: box_right_mult_an_n box_x_an box_x_n an_mult_commutative n_an_mult_commutative)

lemma box_right_mult_an_an:
  "|x](an(y) * an(z)) = |x]an(y) * |x]an(z)"
  by (metis an_dist_sup box_x_an mult_left_dist_sup)

lemma box_n_export:
  "|n(x) * y]z = an(x)  |y]z"
  using box_left_mult box_n_an nbox_def by auto

lemma box_an_export:
  "|an(x) * y]z = n(x)  |y]z"
  using box_an_an box_left_mult nbox_def by auto

lemma box_left_antitone:
  "y  x  |x]z  |y]z"
  by (smt an_mult_commutative an_order box_diamond box_left_dist_sup le_iff_sup)

lemma box_right_isotone:
  "y  z  |x]y  |x]z"
  by (metis an_antitone mult_left_isotone mult_right_isotone nbox_def)

lemma box_antitone_isotone:
  "y  w  x  z  |w]x  |y]z"
  by (meson box_left_antitone box_right_isotone order.trans)

definition nbox_L :: "'a  'a  'a" (" _  _" [50,90] 95)
  where "xy  an(x * an(y) * L) * L"

lemma nbox_to_L:
  "xy = |x]n(y) * L"
  by (simp add: box_x_n nbox_L_def)

lemma nbox_from_L:
  "|x]y = n(x(y * L))"
  using an_n_def nbox_def nbox_L_def by auto

lemma diamond_x_an:
  "|x>an(y) = n(x * an(y) * L)"
  by (simp add: ndiamond_def)

lemma diamond_1_an:
  "|1>an(y) = an(y)"
  using box_1_an box_1_y diamond_1_y by auto

lemma diamond_an_y:
  "|an(x)>y = an(x) * n(y * L)"
  by (simp add: n_export_an ndiamond_def mult_assoc)

lemma diamond_an_bot:
  "|an(x)>bot = bot"
  by (simp add: an_mult_right_zero n_bot ndiamond_def)

lemma diamond_an_1:
  "|an(x)>1 = an(x)"
  using an_n_def diamond_x_1 by auto

lemma diamond_an_n:
  "|an(x)>n(y) = an(x) * n(y)"
  by (simp add: diamond_x_n n_export_an)

lemma diamond_n_an:
  "|n(x)>an(y) = n(x) * an(y)"
  using an_n_def diamond_n_y by auto

lemma diamond_an_an:
  "|an(x)>an(y) = an(x) * an(y)"
  using diamond_an_y an_n_def by auto

lemma diamond_an_an_same:
  "|an(x)>an(x) = an(x)"
  by (simp add: diamond_an_an an_mult_idempotent)

lemma diamond_an_export:
  "|an(x) * y>z = an(x) * |y>z"
  using diamond_an_an diamond_box diamond_left_mult by auto

lemma box_ani:
  "|x]y = an(x * ani(y * L))"
  by (simp add: ani_def nbox_def mult_assoc)

lemma box_x_n_ani:
  "|x]n(y) = an(x * ani(y))"
  by (simp add: box_x_n ani_def mult_assoc)

lemma box_L_ani:
  "xy = ani(x * ani(y))"
  using box_x_n_ani ani_def nbox_to_L by auto

lemma box_L_left_mult:
  "x * yz = xyz"
  using an_mult n_an_def mult_assoc nbox_L_def by auto

lemma diamond_x_an_ani:
  "|x>an(y) = n(x * ani(y))"
  by (simp add: ani_def ndiamond_def mult_assoc)

lemma box_L_left_antitone:
  "y  x  xz  yz"
  by (simp add: box_L_ani ani_antitone mult_left_isotone)

lemma box_L_right_isotone:
  "y  z  xy  xz"
  using ani_antitone ani_def mult_right_isotone mult_assoc nbox_L_def by auto

lemma box_L_antitone_isotone:
  "y  w  x  z  wx  yz"
  using ani_antitone ani_def mult_isotone mult_assoc nbox_L_def by force

end

class n_box_omega_algebra = n_box_semiring + an_omega_algebra
begin

lemma diamond_omega:
  "|xω>y = |xω>z"
  by (simp add: n_omega_mult ndiamond_def mult_assoc)

lemma box_omega:
  "|xω]y = |xω]z"
  by (metis box_diamond diamond_omega)

lemma an_box_omega_induct:
  "|x]an(y) * n(z * L)  an(y)  |xω  x]z  an(y)"
  by (smt an_dist_sup an_omega_induct an_omega_mult box_left_dist_sup box_x_an mult_assoc n_an_def nbox_def)

lemma n_box_omega_induct:
  "|x]n(y) * n(z * L)  n(y)  |xω  x]z  n(y)"
  by (simp add: an_box_omega_induct n_an_def)

lemma an_box_omega_induct_an:
  "|x]an(y) * an(z)  an(y)  |xω  x]an(z)  an(y)"
  using an_box_omega_induct an_n_def by auto

text Theorem 23.13

lemma n_box_omega_induct_n:
  "|x]n(y) * n(z)  n(y)  |xω  x]n(z)  n(y)"
  using an_box_omega_induct_an n_an_def by force

lemma n_diamond_omega_induct:
  "n(y)  |x>n(y)  n(z * L)  n(y)  |xω  x>z"
  using diamond_x_n mult_right_dist_sup n_dist_sup n_omega_induct n_omega_mult ndiamond_def mult_assoc by force

lemma an_diamond_omega_induct:
  "an(y)  |x>an(y)  n(z * L)  an(y)  |xω  x>z"
  by (metis n_diamond_omega_induct an_n_def)

text Theorem 23.9

lemma n_diamond_omega_induct_n:
  "n(y)  |x>n(y)  n(z)  n(y)  |xω  x>n(z)"
  using box_1_n box_1_y n_diamond_omega_induct by auto

lemma an_diamond_omega_induct_an:
  "an(y)  |x>an(y)  an(z)  an(y)  |xω  x>an(z)"
  using an_diamond_omega_induct an_n_def by auto

lemma box_segerberg_an:
  "|xω  x]an(y) = an(y) * |xω  x](n(y)  |x]an(y))"
proof (rule order.antisym)
  have "|xω  x]an(y)  |xω  x]|x]an(y)"
    by (smt box_left_dist_sup box_left_mult box_omega sup_right_isotone box_left_antitone mult_right_dist_sup star.right_plus_below_circ)
  hence "|xω  x]an(y)  |xω  x](n(y)  |x]an(y))"
    using box_right_isotone order_lesseq_imp sup.cobounded2 by blast
  thus"|xω  x]an(y)  an(y) * |xω  x](n(y)  |x]an(y))"
    by (metis le_sup_iff box_1_an box_left_antitone order_refl star_left_unfold_equal an_mult_least_upper_bound nbox_def)
next
  have "an(y) * |x](n(y)  |xω  x]an(y)) * (n(y)  |x]an(y)) = |x]( |xω  x]an(y) * an(y)) * an(y)"
    by (smt sup_bot_left an_export an_mult_commutative box_right_mult_an_an mult_assoc mult_right_dist_sup n_complement_bot nbox_def)
  hence 1: "an(y) * |x](n(y)  |xω  x]an(y)) * (n(y)  |x]an(y))  n(y)  |xω  x]an(y)"
    by (smt sup_assoc sup_commute sup_ge2 box_1_an box_left_dist_sup box_left_mult mult_left_dist_sup omega_unfold star_left_unfold_equal star.circ_plus_one)
  have "n(y) * |x](n(y)  |xω  x]an(y)) * (n(y)  |x]an(y))  n(y)  |xω  x]an(y)"
    by (smt sup_ge1 an_n_def mult_left_isotone n_an_mult_left_lower_bound n_mult_left_absorb_sup nbox_def order_trans)
  thus "an(y) * |xω  x](n(y)  |x]an(y))  |xω  x]an(y)"
    using 1 by (smt an_case_split_left an_shunting_an mult_assoc n_box_omega_induct_n n_dist_sup nbox_def nbox_from_L)
qed

text Theorem 23.16

lemma box_segerberg_n:
  "|xω  x]n(y) = n(y) * |xω  x](an(y)  |x]n(y))"
  using box_segerberg_an an_n_def n_an_def by force

lemma diamond_segerberg_an:
  "|xω  x>an(y) = an(y)  |xω  x>(n(y) * |x>an(y))"
  by (smt an_export an_n_L box_diamond box_segerberg_an diamond_box mult_assoc n_an_def)

text Theorem 23.12

lemma diamond_segerberg_n:
  "|xω  x>n(y) = n(y)  |xω  x>(an(y) * |x>n(y))"
  using diamond_segerberg_an an_n_L n_an_def by auto

text Theorem 23.11

lemma diamond_star_unfold_n:
  "|x>n(y) = n(y)  |an(y) * x>|x>n(y)"
proof -
  have "|x>n(y) = n(y)  n(y) * |x * x>n(y)  |an(y) * x * x>n(y)"
    by (smt sup_assoc sup_commute sup_bot_right an_complement an_complement_bot diamond_an_n diamond_left_dist_sup diamond_n_export diamond_n_n_same mult_assoc mult_left_one mult_right_dist_sup star_left_unfold_equal)
  thus ?thesis
    by (metis diamond_left_mult diamond_x_n n_sup_left_absorb_mult)
qed

lemma diamond_star_unfold_an:
  "|x>an(y) = an(y)  |n(y) * x>|x>an(y)"
  by (metis an_n_def diamond_star_unfold_n n_an_def)

text Theorem 23.15

lemma box_star_unfold_n:
  "|x]n(y) = n(y) * |n(y) * x]|x]n(y)"
  by (smt an_export an_n_L box_diamond diamond_box diamond_star_unfold_an n_an_def n_export)

lemma box_star_unfold_an:
  "|x]an(y) = an(y) * |an(y) * x]|x]an(y)"
  by (metis an_n_def box_star_unfold_n)

text Theorem 23.10

lemma diamond_omega_unfold_n:
  "|xω  x>n(y) = n(y)  |an(y) * x>|xω  x>n(y)"
  by (smt sup_assoc sup_commute diamond_an_export diamond_left_dist_sup diamond_right_dist_sup diamond_star_unfold_n diamond_x_n n_omega_mult n_plus_complement_intro_n omega_unfold)

lemma diamond_omega_unfold_an:
  "|xω  x>an(y) = an(y)  |n(y) * x>|xω  x>an(y)"
  by (metis an_n_def diamond_omega_unfold_n n_an_def)

text Theorem 23.14

lemma box_omega_unfold_n:
  "|xω  x]n(y) = n(y) * |n(y) * x]|xω  x]n(y)"
  by (smt an_export an_n_L box_diamond diamond_box diamond_omega_unfold_an n_an_def n_export)

lemma box_omega_unfold_an:
  "|xω  x]an(y) = an(y) * |an(y) * x]|xω  x]an(y)"
  by (metis an_n_def box_omega_unfold_n)

lemma box_cut_iteration_an:
  "|xω  x]an(y) = |(an(y) * x)ω  (an(y) * x)]an(y)"
  apply (rule order.antisym)
  apply (meson semiring.add_mono an_case_split_left box_left_antitone omega_isotone order_refl star.circ_isotone)
  by (smt (z3) an_box_omega_induct_an an_mult_commutative box_omega_unfold_an nbox_def order_refl)

lemma box_cut_iteration_n:
  "|xω  x]n(y) = |(n(y) * x)ω  (n(y) * x)]n(y)"
  using box_cut_iteration_an n_an_def by auto

lemma diamond_cut_iteration_an:
  "|xω  x>an(y) = |(n(y) * x)ω  (n(y) * x)>an(y)"
  using box_cut_iteration_n diamond_box n_an_def by auto

lemma diamond_cut_iteration_n:
  "|xω  x>n(y) = |(an(y) * x)ω  (an(y) * x)>n(y)"
  using box_cut_iteration_an an_n_L diamond_box by auto

lemma ni_diamond_omega_induct:
  "ni(y)  x»ni(y)  ni(z)  ni(y)  xω  x»z"
  by (metis diamond_L_left_dist_sup diamond_L_x_ni diamond_L_ni ni_dist_sup ni_omega_induct ni_omega_mult)

lemma ani_diamond_omega_induct:
  "ani(y)  x»ani(y)  ni(z)  ani(y)  xω  x»z"
  by (metis ni_ani ni_diamond_omega_induct)

lemma n_diamond_omega_L:
  "|n(xω) * L>y = |xω>y"
  using L_left_zero mult_1_right n_L n_export n_omega_mult ndiamond_def mult_assoc by auto

lemma n_diamond_loop:
  "|xΩ>y = |xω  x>y"
  by (metis Omega_def diamond_left_dist_sup n_diamond_omega_L)

text Theorem 24.1

lemma cut_iteration_loop:
  "|xΩ>n(y) = |(an(y) * x)Ω>n(y)"
  using diamond_cut_iteration_n n_diamond_loop by auto

lemma cut_iteration_while_loop:
  "|xΩ>n(y) = |(an(y) * x)Ω * n(y)>n(y)"
  using cut_iteration_loop diamond_left_mult diamond_n_n_same by auto

text Theorem 24.1

lemma cut_iteration_while_loop_2:
  "|xΩ>n(y) = |an(y)  x>n(y)"
  by (metis cut_iteration_while_loop an_uminus n_an_def while_Omega_def)

lemma modal_while:
  assumes "-q * -p * L  x * -p * L  -p  -q  -r"
    shows "-p  |n((-q * x)ω) * L  (-q * x) * --q>(-r)"
proof -
  have 1: "--q * -p  |-q * x>(-p)  --q * -r"
    using assms mult_right_isotone sup.coboundedI2 tests_dual.sup_complement_intro by auto
  have "-q * -p = n(-q * -q * -p * L)"
    using an_uminus n_export_an mult_assoc mult_1_right n_L tests_dual.sup_idempotent by auto
  also have "...  n(-q * x * -p * L)"
    by (metis assms n_isotone mult_right_isotone mult_assoc)
  also have "...  |-q * x>(-p)  --q * -r"
    by (simp add: ndiamond_def)
  finally have "-p  |-q * x>(-p)  --q * -r"
    using 1 by (smt sup_assoc le_iff_sup tests_dual.inf_cases sub_comm)
  thus ?thesis
    by (smt L_left_zero an_diamond_omega_induct_an an_uminus diamond_left_dist_sup mult_assoc n_n_L n_omega_mult ndiamond_def sub_mult_closed)
qed

lemma modal_while_loop:
  "-q * -p * L  x * -p * L  -p  -q  -r  -p  |(-q * x)Ω * --q>(-r)"
  by (metis L_left_zero Omega_def modal_while mult_assoc mult_right_dist_sup)

text Theorem 24.2

lemma modal_while_loop_2:
  "-q * -p * L  x * -p * L  -p  -q  -r  -p  |-q  x>(-r)"
  by (simp add: while_Omega_def modal_while_loop)

lemma modal_while_2:
  assumes "-p * L  x * -p * L"
    shows "-p  |n((-q * x)ω) * L  (-q * x) * --q>(--q)"
proof -
  have "-p  |-q * x>(-p)  --q"
    by (smt (verit, del_insts) assms an_uminus tests_dual.double_negation n_an_def n_isotone ndiamond_def diamond_an_export sup_assoc sup_commute le_iff_sup tests_dual.inf_complement_intro)
  thus ?thesis
    by (smt L_left_zero an_diamond_omega_induct_an an_uminus diamond_left_dist_sup mult_assoc tests_dual.sup_idempotent n_n_L n_omega_mult ndiamond_def)
qed

end

class n_modal_omega_algebra = n_box_omega_algebra +
  assumes n_star_induct: "n(x * y)  n(y)  n(x * y)  n(y)"
begin

lemma n_star_induct_sup:
  "n(z  x * y)  n(y)  n(x * z)  n(y)"
  by (metis an_dist_sup an_mult_least_upper_bound an_n_order n_mult_right_upper_bound n_star_induct star_L_split)

lemma n_star_induct_star:
  "n(x * y)  n(y)  n(x)  n(y)"
  using n_star_induct n_star_mult by auto

lemma n_star_induct_iff:
  "n(x * y)  n(y)  n(x * y)  n(y)"
  by (metis mult_left_isotone n_isotone n_star_induct order_trans star.circ_increasing)

lemma n_star_bot:
  "n(x) = bot  n(x) = bot"
  by (metis sup_bot_right le_iff_sup mult_1_right n_one n_star_induct_iff)

lemma n_diamond_star_induct:
  "|x>n(y)  n(y)  |x>n(y)  n(y)"
  by (simp add: diamond_x_n n_star_induct)

lemma n_diamond_star_induct_sup:
  "|x>n(y)  n(z)  n(y)  |x>n(z)  n(y)"
  by (simp add: diamond_x_n n_dist_sup n_star_induct_sup)

lemma n_diamond_star_induct_iff:
  "|x>n(y)  n(y)  |x>n(y)  n(y)"
  using diamond_x_n n_star_induct_iff by auto

lemma an_star_induct:
  "an(y)  an(x * y)  an(y)  an(x * y)"
  using an_n_order n_star_induct by auto

lemma an_star_induct_sup:
  "an(y)  an(z  x * y)  an(y)  an(x * z)"
  using an_n_order n_star_induct_sup by auto

lemma an_star_induct_star:
  "an(y)  an(x * y)  an(y)  an(x)"
  by (simp add: an_n_order n_star_induct_star)

lemma an_star_induct_iff:
  "an(y)  an(x * y)  an(y)  an(x * y)"
  using an_n_order n_star_induct_iff by auto

lemma an_star_one:
  "an(x) = 1  an(x) = 1"
  by (metis an_n_equal an_bot n_star_bot n_bot)

lemma an_box_star_induct:
  "an(y)  |x]an(y)  an(y)  |x]an(y)"
  by (simp add: an_star_induct box_x_an)

lemma an_box_star_induct_sup:
  "an(y)  |x]an(y) * an(z)  an(y)  |x]an(z)"
  by (simp add: an_star_induct_sup an_dist_sup an_mult_commutative box_x_an)

lemma an_box_star_induct_iff:
  "an(y)  |x]an(y)  an(y)  |x]an(y)"
  using an_star_induct_iff box_x_an by auto

lemma box_star_segerberg_an:
  "|x]an(y) = an(y) * |x](n(y)  |x]an(y))"
proof (rule order.antisym)
  show "|x]an(y)  an(y) * |x](n(y)  |x]an(y))"
    by (smt (verit) sup_ge2 box_1_an box_left_dist_sup box_left_mult box_right_isotone mult_right_isotone star.circ_right_unfold)
next
  have "an(y) * |x](n(y)  |x]an(y))  an(y) * |x]an(y)"
    by (metis sup_bot_left an_complement_bot box_an_an box_left_antitone box_x_an mult_left_dist_sup mult_left_one mult_right_isotone star.circ_reflexive)
  thus "an(y) * |x](n(y)  |x]an(y))  |x]an(y)"
    by (smt an_box_star_induct_sup an_case_split_left an_dist_sup an_mult_least_upper_bound box_left_antitone box_left_mult box_right_mult_an_an star.left_plus_below_circ nbox_def)
qed

lemma box_star_segerberg_n:
  "|x]n(y) = n(y) * |x](an(y)  |x]n(y))"
  using box_star_segerberg_an an_n_def n_an_def by auto

lemma diamond_segerberg_an:
  "|x>an(y) = an(y)  |x>(n(y) * |x>an(y))"
  by (smt an_export an_n_L box_diamond box_star_segerberg_an diamond_box mult_assoc n_an_def)

lemma diamond_star_segerberg_n:
  "|x>n(y) = n(y)  |x>(an(y) * |x>n(y))"
  using an_n_def diamond_segerberg_an n_an_def by auto

lemma box_cut_star_iteration_an:
  "|x]an(y) = |(an(y) * x)]an(y)"
  by (smt an_box_star_induct_sup an_mult_commutative an_mult_complement_intro_an order.antisym box_an_export box_star_unfold_an nbox_def order_refl)

lemma box_cut_star_iteration_n:
  "|x]n(y) = |(n(y) * x)]n(y)"
  using box_cut_star_iteration_an n_an_def by auto

lemma diamond_cut_star_iteration_an:
  "|x>an(y) = |(n(y) * x)>an(y)"
  using box_cut_star_iteration_an diamond_box n_an_def by auto

lemma diamond_cut_star_iteration_n:
  "|x>n(y) = |(an(y) * x)>n(y)"
  using box_cut_star_iteration_an an_n_L diamond_box by auto

lemma ni_star_induct:
  "ni(x * y)  ni(y)  ni(x * y)  ni(y)"
  using n_star_induct ni_n_order by auto

lemma ni_star_induct_sup:
  "ni(z  x * y)  ni(y)  ni(x * z)  ni(y)"
  by (simp add: ni_n_order n_star_induct_sup)

lemma ni_star_induct_star:
  "ni(x * y)  ni(y)  ni(x)  ni(y)"
  using ni_n_order n_star_induct_star by auto

lemma ni_star_induct_iff:
  "ni(x * y)  ni(y)  ni(x * y)  ni(y)"
  using ni_n_order n_star_induct_iff by auto

lemma ni_star_bot:
  "ni(x) = bot  ni(x) = bot"
  using ni_n_bot n_star_bot by auto

lemma ni_diamond_star_induct:
  "x»ni(y)  ni(y)  x»ni(y)  ni(y)"
  by (simp add: diamond_L_x_ni ni_star_induct)

lemma ni_diamond_star_induct_sup:
  "x»ni(y)  ni(z)  ni(y)  x»ni(z)  ni(y)"
  by (simp add: diamond_L_x_ni ni_dist_sup ni_star_induct_sup)

lemma ni_diamond_star_induct_iff:
  "x»ni(y)  ni(y)  x»ni(y)  ni(y)"
  using diamond_L_x_ni ni_star_induct_iff by auto

lemma ani_star_induct:
  "ani(y)  ani(x * y)  ani(y)  ani(x * y)"
  using an_star_induct ani_an_order by blast

lemma ani_star_induct_sup:
  "ani(y)  ani(z  x * y)  ani(y)  ani(x * z)"
  by (simp add: an_star_induct_sup ani_an_order)

lemma ani_star_induct_star:
  "ani(y)  ani(x * y)  ani(y)  ani(x)"
  using an_star_induct_star ani_an_order by auto

lemma ani_star_induct_iff:
  "ani(y)  ani(x * y)  ani(y)  ani(x * y)"
  using an_star_induct_iff ani_an_order by auto

lemma ani_star_L:
  "ani(x) = L  ani(x) = L"
  using an_star_one ani_an_L by auto

lemma ani_box_star_induct:
  "ani(y)  xani(y)  ani(y)  xani(y)"
  by (metis an_ani ani_def ani_star_induct_iff n_ani box_L_ani)

lemma ani_box_star_induct_iff:
  "ani(y)  xani(y)  ani(y)  xani(y)"
  using ani_box_star_induct box_L_left_antitone order_lesseq_imp star.circ_increasing by blast

lemma ani_box_star_induct_sup:
  "ani(y)  xani(y)  ani(y)  ani(z)  ani(y)  xani(z)"
  by (meson ani_box_star_induct_iff box_L_right_isotone order_trans)

end

end