Theory Stone_Kleene_Relation_Algebras.Iterings
section ‹Iterings›
text ‹
This theory introduces algebraic structures with an operation that describes iteration in various relational computation models.
An iteration describes the repeated sequential execution of a computation.
This is typically modelled by fixpoints, but different computation models use different fixpoints in the refinement order.
We therefore look at equational and simulation axioms rather than induction axioms.
Our development is based on \<^cite>‹"Guttmann2012c"› and the proposed algebras generalise Kleene algebras.
We first consider a variant of Conway semirings \<^cite>‹"BloomEsik1993a"› based on idempotent left semirings.
Conway semirings expand semirings by an iteration operation satisfying Conway's sumstar and productstar axioms \<^cite>‹"Conway1971"›.
Many properties of iteration follow already from these equational axioms.
Next we introduce iterings, which use generalised versions of simulation axioms in addition to sumstar and productstar.
Unlike the induction axioms of the Kleene star, which hold only in partial-correctness models, the simulation axioms are also valid in total and general correctness models.
They are still powerful enough to prove the correctness of complex results such as separation theorems of \<^cite>‹"Cohen2000"› and Back's atomicity refinement theorem \<^cite>‹"BackWright1999" and "Wright2004"›.
›
theory Iterings
imports Stone_Relation_Algebras.Semirings
begin
subsection ‹Conway Semirings›
text ‹
In this section, we consider equational axioms for iteration.
The algebraic structures are based on idempotent left semirings, which are expanded by a unary iteration operation.
We start with an unfold property, one inequality of the sliding rule and distributivity over joins, which is similar to Conway's sumstar.
›
class circ =
fixes circ :: "'a ⇒ 'a" ("_⇧∘" [100] 100)
class left_conway_semiring = idempotent_left_semiring + circ +
assumes circ_left_unfold: "1 ⊔ x * x⇧∘ = x⇧∘"
assumes circ_left_slide: "(x * y)⇧∘ * x ≤ x * (y * x)⇧∘"
assumes circ_sup_1: "(x ⊔ y)⇧∘ = x⇧∘ * (y * x⇧∘)⇧∘"
begin
text ‹
We obtain one inequality of Conway's productstar, as well as of the other unfold rule.
›
lemma circ_mult_sub:
"1 ⊔ x * (y * x)⇧∘ * y ≤ (x * y)⇧∘"
by (metis sup_right_isotone circ_left_slide circ_left_unfold mult_assoc mult_right_isotone)
lemma circ_right_unfold_sub:
"1 ⊔ x⇧∘ * x ≤ x⇧∘"
by (metis circ_mult_sub mult_1_left mult_1_right)
lemma circ_zero:
"bot⇧∘ = 1"
by (metis sup_monoid.add_0_right circ_left_unfold mult_left_zero)
lemma circ_increasing:
"x ≤ x⇧∘"
by (metis le_supI2 circ_left_unfold circ_right_unfold_sub mult_1_left mult_right_sub_dist_sup_left order_trans)
lemma circ_reflexive:
"1 ≤ x⇧∘"
by (metis sup_left_divisibility circ_left_unfold)
lemma circ_mult_increasing:
"x ≤ x * x⇧∘"
by (metis circ_reflexive mult_right_isotone mult_1_right)
lemma circ_mult_increasing_2:
"x ≤ x⇧∘ * x"
by (metis circ_reflexive mult_left_isotone mult_1_left)
lemma circ_transitive_equal:
"x⇧∘ * x⇧∘ = x⇧∘"
by (metis sup_idem circ_sup_1 circ_left_unfold mult_assoc)
text ‹
While iteration is not idempotent, a fixpoint is reached after applying this operation twice.
Iteration is idempotent for the unit.
›
lemma circ_circ_circ:
"x⇧∘⇧∘⇧∘ = x⇧∘⇧∘"
by (metis sup_idem circ_sup_1 circ_increasing circ_transitive_equal le_iff_sup)
lemma circ_one:
"1⇧∘ = 1⇧∘⇧∘"
by (metis circ_circ_circ circ_zero)
lemma circ_sup_sub:
"(x⇧∘ * y)⇧∘ * x⇧∘ ≤ (x ⊔ y)⇧∘"
by (metis circ_sup_1 circ_left_slide)
lemma circ_plus_one:
"x⇧∘ = 1 ⊔ x⇧∘"
by (metis le_iff_sup circ_reflexive)
text ‹
Iteration satisfies a characteristic property of reflexive transitive closures.
›
lemma circ_rtc_2:
"1 ⊔ x ⊔ x⇧∘ * x⇧∘ = x⇧∘"
by (metis sup_assoc circ_increasing circ_plus_one circ_transitive_equal le_iff_sup)
lemma mult_zero_circ:
"(x * bot)⇧∘ = 1 ⊔ x * bot"
by (metis circ_left_unfold mult_assoc mult_left_zero)
lemma mult_zero_sup_circ:
"(x ⊔ y * bot)⇧∘ = x⇧∘ * (y * bot)⇧∘"
by (metis circ_sup_1 mult_assoc mult_left_zero)
lemma circ_plus_sub:
"x⇧∘ * x ≤ x * x⇧∘"
by (metis circ_left_slide mult_1_left mult_1_right)
lemma circ_loop_fixpoint:
"y * (y⇧∘ * z) ⊔ z = y⇧∘ * z"
by (metis sup_commute circ_left_unfold mult_assoc mult_1_left mult_right_dist_sup)
lemma left_plus_below_circ:
"x * x⇧∘ ≤ x⇧∘"
by (metis sup.cobounded2 circ_left_unfold)
lemma right_plus_below_circ:
"x⇧∘ * x ≤ x⇧∘"
using circ_right_unfold_sub by auto
lemma circ_sup_upper_bound:
"x ≤ z⇧∘ ⟹ y ≤ z⇧∘ ⟹ x ⊔ y ≤ z⇧∘"
by simp
lemma circ_mult_upper_bound:
"x ≤ z⇧∘ ⟹ y ≤ z⇧∘ ⟹ x * y ≤ z⇧∘"
by (metis mult_isotone circ_transitive_equal)
lemma circ_sub_dist:
"x⇧∘ ≤ (x ⊔ y)⇧∘"
by (metis circ_sup_sub circ_plus_one mult_1_left mult_right_sub_dist_sup_left order_trans)
lemma circ_sub_dist_1:
"x ≤ (x ⊔ y)⇧∘"
using circ_increasing le_supE by blast
lemma circ_sub_dist_2:
"x * y ≤ (x ⊔ y)⇧∘"
by (metis sup_commute circ_mult_upper_bound circ_sub_dist_1)
lemma circ_sub_dist_3:
"x⇧∘ * y⇧∘ ≤ (x ⊔ y)⇧∘"
by (metis sup_commute circ_mult_upper_bound circ_sub_dist)
lemma circ_isotone:
"x ≤ y ⟹ x⇧∘ ≤ y⇧∘"
by (metis circ_sub_dist le_iff_sup)
lemma circ_sup_2:
"(x ⊔ y)⇧∘ ≤ (x⇧∘ * y⇧∘)⇧∘"
by (metis sup.bounded_iff circ_increasing circ_isotone circ_reflexive mult_isotone mult_1_left mult_1_right)
lemma circ_sup_one_left_unfold:
"1 ≤ x ⟹ x * x⇧∘ = x⇧∘"
by (metis order.antisym le_iff_sup mult_1_left mult_right_sub_dist_sup_left left_plus_below_circ)
lemma circ_sup_one_right_unfold:
"1 ≤ x ⟹ x⇧∘ * x = x⇧∘"
by (metis order.antisym le_iff_sup mult_left_sub_dist_sup_left mult_1_right right_plus_below_circ)
lemma circ_decompose_4:
"(x⇧∘ * y⇧∘)⇧∘ = x⇧∘ * (y⇧∘ * x⇧∘)⇧∘"
by (metis sup_assoc sup_commute circ_sup_1 circ_loop_fixpoint circ_plus_one circ_rtc_2 circ_transitive_equal mult_assoc)
lemma circ_decompose_5:
"(x⇧∘ * y⇧∘)⇧∘ = (y⇧∘ * x⇧∘)⇧∘"
by (metis circ_decompose_4 circ_loop_fixpoint order.antisym mult_right_sub_dist_sup_right mult_assoc)
lemma circ_decompose_6:
"x⇧∘ * (y * x⇧∘)⇧∘ = y⇧∘ * (x * y⇧∘)⇧∘"
by (metis sup_commute circ_sup_1)
lemma circ_decompose_7:
"(x ⊔ y)⇧∘ = x⇧∘ * y⇧∘ * (x ⊔ y)⇧∘"
by (metis circ_sup_1 circ_decompose_6 circ_transitive_equal mult_assoc)
lemma circ_decompose_8:
"(x ⊔ y)⇧∘ = (x ⊔ y)⇧∘ * x⇧∘ * y⇧∘"
by (metis order.antisym eq_refl mult_assoc mult_isotone mult_1_right circ_mult_upper_bound circ_reflexive circ_sub_dist_3)
lemma circ_decompose_9:
"(x⇧∘ * y⇧∘)⇧∘ = x⇧∘ * y⇧∘ * (x⇧∘ * y⇧∘)⇧∘"
by (metis circ_decompose_4 mult_assoc)
lemma circ_decompose_10:
"(x⇧∘ * y⇧∘)⇧∘ = (x⇧∘ * y⇧∘)⇧∘ * x⇧∘ * y⇧∘"
by (metis sup_ge2 circ_loop_fixpoint circ_reflexive circ_sup_one_right_unfold mult_assoc order_trans)
lemma circ_back_loop_prefixpoint:
"(z * y⇧∘) * y ⊔ z ≤ z * y⇧∘"
by (metis sup.bounded_iff circ_left_unfold mult_assoc mult_left_sub_dist_sup_left mult_right_isotone mult_1_right right_plus_below_circ)
text ‹
We obtain the fixpoint and prefixpoint properties of iteration, but not least or greatest fixpoint properties.
›
lemma circ_loop_is_fixpoint:
"is_fixpoint (λx . y * x ⊔ z) (y⇧∘ * z)"
by (metis circ_loop_fixpoint is_fixpoint_def)
lemma circ_back_loop_is_prefixpoint:
"is_prefixpoint (λx . x * y ⊔ z) (z * y⇧∘)"
by (metis circ_back_loop_prefixpoint is_prefixpoint_def)
lemma circ_circ_sup:
"(1 ⊔ x)⇧∘ = x⇧∘⇧∘"
by (metis sup_commute circ_sup_1 circ_decompose_4 circ_zero mult_1_right)
lemma circ_circ_mult_sub:
"x⇧∘ * 1⇧∘ ≤ x⇧∘⇧∘"
by (metis circ_increasing circ_isotone circ_mult_upper_bound circ_reflexive)
lemma left_plus_circ:
"(x * x⇧∘)⇧∘ = x⇧∘"
by (metis circ_left_unfold circ_sup_1 mult_1_right mult_sub_right_one sup.absorb1 mult_assoc)
lemma right_plus_circ:
"(x⇧∘ * x)⇧∘ = x⇧∘"
by (metis sup_commute circ_isotone circ_loop_fixpoint circ_plus_sub circ_sub_dist order.eq_iff left_plus_circ)
lemma circ_square:
"(x * x)⇧∘ ≤ x⇧∘"
by (metis circ_increasing circ_isotone left_plus_circ mult_right_isotone)
lemma circ_mult_sub_sup:
"(x * y)⇧∘ ≤ (x ⊔ y)⇧∘"
by (metis sup_ge1 sup_ge2 circ_isotone circ_square mult_isotone order_trans)
lemma circ_sup_mult_zero:
"x⇧∘ * y = (x ⊔ y * bot)⇧∘ * y"
proof -
have "(x ⊔ y * bot)⇧∘ * y = x⇧∘ * (1 ⊔ y * bot) * y"
by (metis mult_zero_sup_circ mult_zero_circ)
also have "... = x⇧∘ * (y ⊔ y * bot)"
by (metis mult_assoc mult_1_left mult_left_zero mult_right_dist_sup)
also have "... = x⇧∘ * y"
by (metis sup_commute le_iff_sup zero_right_mult_decreasing)
finally show ?thesis
by simp
qed
lemma troeger_1:
"(x ⊔ y)⇧∘ = x⇧∘ * (1 ⊔ y * (x ⊔ y)⇧∘)"
by (metis circ_sup_1 circ_left_unfold mult_assoc)
lemma troeger_2:
"(x ⊔ y)⇧∘ * z = x⇧∘ * (y * (x ⊔ y)⇧∘ * z ⊔ z)"
by (metis circ_sup_1 circ_loop_fixpoint mult_assoc)
lemma troeger_3:
"(x ⊔ y * bot)⇧∘ = x⇧∘ * (1 ⊔ y * bot)"
by (metis mult_zero_sup_circ mult_zero_circ)
lemma circ_sup_sub_sup_one_1:
"x ⊔ y ≤ x⇧∘ * (1 ⊔ y)"
by (metis circ_increasing circ_left_unfold mult_1_left mult_1_right mult_left_sub_dist_sup mult_right_sub_dist_sup_left order_trans sup_mono)
lemma circ_sup_sub_sup_one_2:
"x⇧∘ * (x ⊔ y) ≤ x⇧∘ * (1 ⊔ y)"
by (metis circ_sup_sub_sup_one_1 circ_transitive_equal mult_assoc mult_right_isotone)
lemma circ_sup_sub_sup_one:
"x * x⇧∘ * (x ⊔ y) ≤ x * x⇧∘ * (1 ⊔ y)"
by (metis circ_sup_sub_sup_one_2 mult_assoc mult_right_isotone)
lemma circ_square_2:
"(x * x)⇧∘ * (x ⊔ 1) ≤ x⇧∘"
by (metis sup.bounded_iff circ_increasing circ_mult_upper_bound circ_reflexive circ_square)
lemma :
"(y * x⇧∘)⇧∘ = (y * y⇧∘ * x⇧∘)⇧∘"
by (metis circ_decompose_6 circ_transitive_equal left_plus_circ mult_assoc)
lemma circ_circ_sub_mult:
"1⇧∘ * x⇧∘ ≤ x⇧∘⇧∘"
by (metis circ_increasing circ_isotone circ_mult_upper_bound circ_reflexive)
lemma circ_decompose_11:
"(x⇧∘ * y⇧∘)⇧∘ = (x⇧∘ * y⇧∘)⇧∘ * x⇧∘"
by (metis circ_decompose_10 circ_decompose_4 circ_decompose_5 circ_decompose_9 left_plus_circ)
lemma circ_mult_below_circ_circ:
"(x * y)⇧∘ ≤ (x⇧∘ * y)⇧∘ * x⇧∘"
by (metis circ_increasing circ_isotone circ_reflexive dual_order.trans mult_left_isotone mult_right_isotone mult_1_right)
lemma power_below_circ:
"power x i ≤ x⇧∘"
apply (induct rule: nat.induct)
apply (simp add: circ_reflexive)
by (simp add: circ_increasing circ_mult_upper_bound)
end
text ‹
The next class considers the interaction of iteration with a greatest element.
›
class bounded_left_conway_semiring = bounded_idempotent_left_semiring + left_conway_semiring
begin
lemma circ_top:
"top⇧∘ = top"
by (simp add: order.antisym circ_increasing)
lemma circ_right_top:
"x⇧∘ * top = top"
by (metis sup_right_top circ_loop_fixpoint)
lemma circ_left_top:
"top * x⇧∘ = top"
by (metis circ_right_top circ_top circ_decompose_11)
lemma mult_top_circ:
"(x * top)⇧∘ = 1 ⊔ x * top"
by (metis circ_left_top circ_left_unfold mult_assoc)
end
class left_zero_conway_semiring = idempotent_left_zero_semiring + left_conway_semiring
begin
lemma mult_zero_sup_circ_2:
"(x ⊔ y * bot)⇧∘ = x⇧∘ ⊔ x⇧∘ * y * bot"
by (metis mult_assoc mult_left_dist_sup mult_1_right troeger_3)
lemma circ_unfold_sum:
"(x ⊔ y)⇧∘ = x⇧∘ ⊔ x⇧∘ * y * (x ⊔ y)⇧∘"
by (metis mult_assoc mult_left_dist_sup mult_1_right troeger_1)
end
text ‹
The next class assumes the full sliding equation.
›
class left_conway_semiring_1 = left_conway_semiring +
assumes circ_right_slide: "x * (y * x)⇧∘ ≤ (x * y)⇧∘ * x"
begin
lemma circ_slide_1:
"x * (y * x)⇧∘ = (x * y)⇧∘ * x"
by (metis order.antisym circ_left_slide circ_right_slide)
text ‹
This implies the full unfold rules and Conway's productstar.
›
lemma circ_right_unfold_1:
"1 ⊔ x⇧∘ * x = x⇧∘"
by (metis circ_left_unfold circ_slide_1 mult_1_left mult_1_right)
lemma circ_mult_1:
"(x * y)⇧∘ = 1 ⊔ x * (y * x)⇧∘ * y"
by (metis circ_left_unfold circ_slide_1 mult_assoc)
lemma circ_sup_9:
"(x ⊔ y)⇧∘ = (x⇧∘ * y)⇧∘ * x⇧∘"
by (metis circ_sup_1 circ_slide_1)
lemma circ_plus_same:
"x⇧∘ * x = x * x⇧∘"
by (metis circ_slide_1 mult_1_left mult_1_right)
lemma circ_decompose_12:
"x⇧∘ * y⇧∘ ≤ (x⇧∘ * y)⇧∘ * x⇧∘"
by (metis circ_sup_9 circ_sub_dist_3)
end
class left_zero_conway_semiring_1 = left_zero_conway_semiring + left_conway_semiring_1
begin
lemma circ_back_loop_fixpoint:
"(z * y⇧∘) * y ⊔ z = z * y⇧∘"
by (metis sup_commute circ_left_unfold circ_plus_same mult_assoc mult_left_dist_sup mult_1_right)
lemma circ_back_loop_is_fixpoint:
"is_fixpoint (λx . x * y ⊔ z) (z * y⇧∘)"
by (metis circ_back_loop_fixpoint is_fixpoint_def)
lemma circ_elimination:
"x * y = bot ⟹ x * y⇧∘ ≤ x"
by (metis sup_monoid.add_0_left circ_back_loop_fixpoint circ_plus_same mult_assoc mult_left_zero order_refl)
end
subsection ‹Iterings›
text ‹
This section adds simulation axioms to Conway semirings.
We consider several classes with increasingly general simulation axioms.
›
class itering_1 = left_conway_semiring_1 +
assumes circ_simulate: "z * x ≤ y * z ⟶ z * x⇧∘ ≤ y⇧∘ * z"
begin
lemma circ_circ_mult:
"1⇧∘ * x⇧∘ = x⇧∘⇧∘"
by (metis order.antisym circ_circ_sup circ_reflexive circ_simulate circ_sub_dist_3 circ_sup_one_left_unfold circ_transitive_equal mult_1_left order_refl)
lemma sub_mult_one_circ:
"x * 1⇧∘ ≤ 1⇧∘ * x"
by (metis circ_simulate mult_1_left mult_1_right order_refl)
text ‹
The left simulation axioms is enough to prove a basic import property of tests.
›
lemma circ_import:
assumes "p ≤ p * p"
and "p ≤ 1"
and "p * x ≤ x * p"
shows "p * x⇧∘ = p * (p * x)⇧∘"
proof -
have "p * x ≤ p * (p * x * p) * p"
by (metis assms coreflexive_transitive order.eq_iff test_preserves_equation mult_assoc)
hence "p * x⇧∘ ≤ p * (p * x)⇧∘"
by (metis (no_types) assms circ_simulate circ_slide_1 test_preserves_equation)
thus ?thesis
by (metis assms(2) circ_isotone mult_left_isotone mult_1_left mult_right_isotone order.antisym)
qed
end
text ‹
Including generalisations of both simulation axioms allows us to prove separation rules.
›
class itering_2 = left_conway_semiring_1 +
assumes circ_simulate_right: "z * x ≤ y * z ⊔ w ⟶ z * x⇧∘ ≤ y⇧∘ * (z ⊔ w * x⇧∘)"
assumes circ_simulate_left: "x * z ≤ z * y ⊔ w ⟶ x⇧∘ * z ≤ (z ⊔ x⇧∘ * w) * y⇧∘"
begin
subclass itering_1
apply unfold_locales
by (metis sup_monoid.add_0_right circ_simulate_right mult_left_zero)
lemma circ_simulate_left_1:
"x * z ≤ z * y ⟹ x⇧∘ * z ≤ z * y⇧∘ ⊔ x⇧∘ * bot"
by (metis sup_monoid.add_0_right circ_simulate_left mult_assoc mult_left_zero mult_right_dist_sup)
lemma circ_separate_1:
assumes "y * x ≤ x * y"
shows "(x ⊔ y)⇧∘ = x⇧∘ * y⇧∘"
proof -
have "y⇧∘ * x ≤ x * y⇧∘ ⊔ y⇧∘ * bot"
by (metis assms circ_simulate_left_1)
hence "y⇧∘ * x * y⇧∘ ≤ x * y⇧∘ * y⇧∘ ⊔ y⇧∘ * bot * y⇧∘"
by (metis mult_assoc mult_left_isotone mult_right_dist_sup)
also have "... = x * y⇧∘ ⊔ y⇧∘ * bot"
by (metis circ_transitive_equal mult_assoc mult_left_zero)
finally have "y⇧∘ * (x * y⇧∘)⇧∘ ≤ x⇧∘ * (y⇧∘ ⊔ y⇧∘ * bot)"
using circ_simulate_right mult_assoc by fastforce
also have "... = x⇧∘ * y⇧∘"
by (simp add: sup_absorb1 zero_right_mult_decreasing)
finally have "(x ⊔ y)⇧∘ ≤ x⇧∘ * y⇧∘"
by (simp add: circ_decompose_6 circ_sup_1)
thus ?thesis
by (simp add: order.antisym circ_sub_dist_3)
qed
lemma circ_circ_mult_1:
"x⇧∘ * 1⇧∘ = x⇧∘⇧∘"
by (metis sup_commute circ_circ_sup circ_separate_1 mult_1_left mult_1_right order_refl)
end
text ‹
With distributivity, we also get Back's atomicity refinement theorem.
›
class itering_3 = itering_2 + left_zero_conway_semiring_1
begin
lemma circ_simulate_1:
assumes "y * x ≤ x * y"
shows "y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘"
proof -
have "y * x⇧∘ ≤ x⇧∘ * y"
by (metis assms circ_simulate)
hence "y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘ ⊔ y⇧∘ * bot"
by (metis circ_simulate_left_1)
thus ?thesis
by (metis sup_assoc sup_monoid.add_0_right circ_loop_fixpoint mult_assoc mult_left_zero mult_zero_sup_circ_2)
qed
lemma atomicity_refinement:
assumes "s = s * q"
and "x = q * x"
and "q * b = bot"
and "r * b ≤ b * r"
and "r * l ≤ l * r"
and "x * l ≤ l * x"
and "b * l ≤ l * b"
and "q * l ≤ l * q"
and "r⇧∘ * q ≤ q * r⇧∘"
and "q ≤ 1"
shows "s * (x ⊔ b ⊔ r ⊔ l)⇧∘ * q ≤ s * (x * b⇧∘ * q ⊔ r ⊔ l)⇧∘"
proof -
have "(x ⊔ b ⊔ r) * l ≤ l * (x ⊔ b ⊔ r)"
using assms(5-7) mult_left_dist_sup mult_right_dist_sup semiring.add_mono by presburger
hence "s * (x ⊔ b ⊔ r ⊔ l)⇧∘ * q = s * l⇧∘ * (x ⊔ b ⊔ r)⇧∘ * q"
by (metis sup_commute circ_separate_1 mult_assoc)
also have "... = s * l⇧∘ * b⇧∘ * r⇧∘ * q * (x * b⇧∘ * r⇧∘ * q)⇧∘"
proof -
have "(b ⊔ r)⇧∘ = b⇧∘ * r⇧∘"
by (simp add: assms(4) circ_separate_1)
hence "b⇧∘ * r⇧∘ * (q * (x * b⇧∘ * r⇧∘))⇧∘ = (x ⊔ b ⊔ r)⇧∘"
by (metis (full_types) assms(2) circ_sup_1 sup_assoc sup_commute mult_assoc)
thus ?thesis
by (metis circ_slide_1 mult_assoc)
qed
also have "... ≤ s * l⇧∘ * b⇧∘ * r⇧∘ * q * (x * b⇧∘ * q * r⇧∘)⇧∘"
by (metis assms(9) circ_isotone mult_assoc mult_right_isotone)
also have "... ≤ s * q * l⇧∘ * b⇧∘ * r⇧∘ * (x * b⇧∘ * q * r⇧∘)⇧∘"
by (metis assms(1,10) mult_left_isotone mult_right_isotone mult_1_right)
also have "... ≤ s * l⇧∘ * q * b⇧∘ * r⇧∘ * (x * b⇧∘ * q * r⇧∘)⇧∘"
by (metis assms(1,8) circ_simulate mult_assoc mult_left_isotone mult_right_isotone)
also have "... ≤ s * l⇧∘ * r⇧∘ * (x * b⇧∘ * q * r⇧∘)⇧∘"
by (metis assms(3,10) sup_monoid.add_0_left circ_back_loop_fixpoint circ_plus_same mult_assoc mult_left_zero mult_left_isotone mult_right_isotone mult_1_right)
also have "... ≤ s * (x * b⇧∘ * q ⊔ r ⊔ l)⇧∘"
by (metis sup_commute circ_sup_1 circ_sub_dist_3 mult_assoc mult_right_isotone)
finally show ?thesis
.
qed
end
text ‹
The following class contains the most general simulation axioms we consider.
They allow us to prove further separation properties.
›
class itering = idempotent_left_zero_semiring + circ +
assumes circ_sup: "(x ⊔ y)⇧∘ = (x⇧∘ * y)⇧∘ * x⇧∘"
assumes circ_mult: "(x * y)⇧∘ = 1 ⊔ x * (y * x)⇧∘ * y"
assumes circ_simulate_right_plus: "z * x ≤ y * y⇧∘ * z ⊔ w ⟶ z * x⇧∘ ≤ y⇧∘ * (z ⊔ w * x⇧∘)"
assumes circ_simulate_left_plus: "x * z ≤ z * y⇧∘ ⊔ w ⟶ x⇧∘ * z ≤ (z ⊔ x⇧∘ * w) * y⇧∘"
begin
lemma circ_right_unfold:
"1 ⊔ x⇧∘ * x = x⇧∘"
by (metis circ_mult mult_1_left mult_1_right)
lemma circ_slide:
"x * (y * x)⇧∘ = (x * y)⇧∘ * x"
proof -
have "x * (y * x)⇧∘ = Rf x (y * 1 ⊔ y * (x * (y * x)⇧∘ * y)) * x"
by (metis (no_types) circ_mult mult_1_left mult_1_right mult_left_dist_sup mult_right_dist_sup mult_assoc)
thus ?thesis
by (metis (no_types) circ_mult mult_1_right mult_left_dist_sup mult_assoc)
qed
subclass itering_3
apply unfold_locales
apply (metis circ_mult mult_1_left mult_1_right)
apply (metis circ_slide order_refl)
apply (metis circ_sup circ_slide)
apply (metis circ_slide order_refl)
apply (metis sup_left_isotone circ_right_unfold mult_left_isotone mult_left_sub_dist_sup_left mult_1_right order_trans circ_simulate_right_plus)
by (metis sup_commute sup_ge1 sup_right_isotone circ_mult mult_right_isotone mult_1_right order_trans circ_simulate_left_plus)
lemma circ_simulate_right_plus_1:
"z * x ≤ y * y⇧∘ * z ⟹ z * x⇧∘ ≤ y⇧∘ * z"
by (metis sup_monoid.add_0_right circ_simulate_right_plus mult_left_zero)
lemma circ_simulate_left_plus_1:
"x * z ≤ z * y⇧∘ ⟹ x⇧∘ * z ≤ z * y⇧∘ ⊔ x⇧∘ * bot"
by (metis sup_monoid.add_0_right circ_simulate_left_plus mult_assoc mult_left_zero mult_right_dist_sup)
lemma circ_simulate_2:
"y * x⇧∘ ≤ x⇧∘ * y⇧∘ ⟷ y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘"
apply (rule iffI)
apply (metis sup_assoc sup_monoid.add_0_right circ_loop_fixpoint circ_simulate_left_plus_1 mult_assoc mult_left_zero mult_zero_sup_circ_2)
by (metis circ_increasing mult_left_isotone order_trans)
lemma circ_simulate_absorb:
"y * x ≤ x ⟹ y⇧∘ * x ≤ x ⊔ y⇧∘ * bot"
by (metis circ_simulate_left_plus_1 circ_zero mult_1_right)
lemma circ_simulate_3:
"y * x⇧∘ ≤ x⇧∘ ⟹ y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘"
by (metis sup.bounded_iff circ_reflexive circ_simulate_2 le_iff_sup mult_right_isotone mult_1_right)
lemma circ_separate_mult_1:
"y * x ≤ x * y ⟹ (x * y)⇧∘ ≤ x⇧∘ * y⇧∘"
by (metis circ_mult_sub_sup circ_separate_1)
lemma circ_separate_unfold:
"(y * x⇧∘)⇧∘ = y⇧∘ ⊔ y⇧∘ * y * x * x⇧∘ * (y * x⇧∘)⇧∘"
by (metis circ_back_loop_fixpoint circ_plus_same circ_unfold_sum sup_commute mult_assoc)
lemma separation:
assumes "y * x ≤ x * y⇧∘"
shows "(x ⊔ y)⇧∘ = x⇧∘ * y⇧∘"
proof -
have "y⇧∘ * x * y⇧∘ ≤ x * y⇧∘ ⊔ y⇧∘ * bot"
by (metis assms circ_simulate_left_plus_1 circ_transitive_equal mult_assoc mult_left_isotone)
thus ?thesis
by (metis sup_commute circ_sup_1 circ_simulate_right circ_sub_dist_3 le_iff_sup mult_assoc mult_left_zero zero_right_mult_decreasing)
qed
lemma simulation:
"y * x ≤ x * y⇧∘ ⟹ y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘"
by (metis sup_ge2 circ_isotone circ_mult_upper_bound circ_sub_dist separation)
lemma circ_simulate_4:
assumes "y * x ≤ x * x⇧∘ * (1 ⊔ y)"
shows "y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘"
proof -
have "x ⊔ (x * x⇧∘ * x * x ⊔ x * x) = x * x⇧∘"
by (metis (no_types) circ_back_loop_fixpoint mult_right_dist_sup sup_commute)
hence "x ≤ x * x⇧∘ * 1 ⊔ x * x⇧∘ * y"
by (metis mult_1_right sup_assoc sup_ge1)
hence "(1 ⊔ y) * x ≤ x * x⇧∘ * (1 ⊔ y)"
using assms mult_left_dist_sup mult_right_dist_sup by force
hence "y * x⇧∘ ≤ x⇧∘ * y⇧∘"
by (metis circ_sup_upper_bound circ_increasing circ_reflexive circ_simulate_right_plus_1 mult_right_isotone mult_right_sub_dist_sup_right order_trans)
thus ?thesis
by (metis circ_simulate_2)
qed
lemma circ_simulate_5:
"y * x ≤ x * x⇧∘ * (x ⊔ y) ⟹ y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘"
by (metis circ_sup_sub_sup_one circ_simulate_4 order_trans)
lemma circ_simulate_6:
"y * x ≤ x * (x ⊔ y) ⟹ y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘"
by (metis sup_commute circ_back_loop_fixpoint circ_simulate_5 mult_right_sub_dist_sup_left order_trans)
lemma circ_separate_4:
assumes "y * x ≤ x * x⇧∘ * (1 ⊔ y)"
shows "(x ⊔ y)⇧∘ = x⇧∘ * y⇧∘"
proof -
have "y * x * x⇧∘ ≤ x * x⇧∘ * (1 ⊔ y) * x⇧∘"
by (simp add: assms mult_left_isotone)
also have "... = x * x⇧∘ ⊔ x * x⇧∘ * y * x⇧∘"
by (simp add: circ_transitive_equal mult_left_dist_sup mult_right_dist_sup mult_assoc)
also have "... ≤ x * x⇧∘ ⊔ x * x⇧∘ * x⇧∘ * y⇧∘"
by (metis assms sup_right_isotone circ_simulate_2 circ_simulate_4 mult_assoc mult_right_isotone)
finally have "y * x * x⇧∘ ≤ x * x⇧∘ * y⇧∘"
by (metis circ_reflexive circ_transitive_equal le_iff_sup mult_assoc mult_right_isotone mult_1_right)
thus ?thesis
by (metis circ_sup_1 left_plus_circ mult_assoc separation)
qed
lemma circ_separate_5:
"y * x ≤ x * x⇧∘ * (x ⊔ y) ⟹ (x ⊔ y)⇧∘ = x⇧∘ * y⇧∘"
by (metis circ_sup_sub_sup_one circ_separate_4 order_trans)
lemma circ_separate_6:
"y * x ≤ x * (x ⊔ y) ⟹ (x ⊔ y)⇧∘ = x⇧∘ * y⇧∘"
by (metis sup_commute circ_back_loop_fixpoint circ_separate_5 mult_right_sub_dist_sup_left order_trans)
end
class bounded_itering = bounded_idempotent_left_zero_semiring + itering
begin
subclass bounded_left_conway_semiring ..
end
text ‹
We finally expand Conway semirings and iterings by an element that corresponds to the endless loop.
›
class L =
fixes L :: "'a"
class left_conway_semiring_L = left_conway_semiring + L +
assumes one_circ_mult_split: "1⇧∘ * x = L ⊔ x"
assumes L_split_sup: "x * (y ⊔ L) ≤ x * y ⊔ L"
begin
lemma L_def:
"L = 1⇧∘ * bot"
by (metis sup_monoid.add_0_right one_circ_mult_split)
lemma one_circ_split:
"1⇧∘ = L ⊔ 1"
by (metis mult_1_right one_circ_mult_split)
lemma one_circ_circ_split:
"1⇧∘⇧∘ = L ⊔ 1"
by (metis circ_one one_circ_split)
lemma sub_mult_one_circ:
"x * 1⇧∘ ≤ 1⇧∘ * x"
by (metis L_split_sup sup_commute mult_1_right one_circ_mult_split)
lemma one_circ_mult_split_2:
"1⇧∘ * x = x * 1⇧∘ ⊔ L"
proof -
have 1: "x * 1⇧∘ ≤ L ⊔ x"
using one_circ_mult_split sub_mult_one_circ by presburger
have "x ⊔ x * 1⇧∘ = x * 1⇧∘"
by (meson circ_back_loop_prefixpoint le_iff_sup sup.boundedE)
thus ?thesis
using 1 by (simp add: le_iff_sup one_circ_mult_split sup_assoc sup_commute)
qed
lemma sub_mult_one_circ_split:
"x * 1⇧∘ ≤ x ⊔ L"
by (metis sup_commute one_circ_mult_split sub_mult_one_circ)
lemma sub_mult_one_circ_split_2:
"x * 1⇧∘ ≤ x ⊔ 1⇧∘"
by (metis L_def sup_right_isotone order_trans sub_mult_one_circ_split zero_right_mult_decreasing)
lemma L_split:
"x * L ≤ x * bot ⊔ L"
by (metis L_split_sup sup_monoid.add_0_left)
lemma L_left_zero:
"L * x = L"
by (metis L_def mult_assoc mult_left_zero)
lemma one_circ_L:
"1⇧∘ * L = L"
by (metis L_def circ_transitive_equal mult_assoc)
lemma mult_L_circ:
"(x * L)⇧∘ = 1 ⊔ x * L"
by (metis L_left_zero circ_left_unfold mult_assoc)
lemma mult_L_circ_mult:
"(x * L)⇧∘ * y = y ⊔ x * L"
by (metis L_left_zero mult_L_circ mult_assoc mult_1_left mult_right_dist_sup)
lemma circ_L:
"L⇧∘ = L ⊔ 1"
by (metis L_left_zero sup_commute circ_left_unfold)
lemma L_below_one_circ:
"L ≤ 1⇧∘"
by (metis L_def zero_right_mult_decreasing)
lemma circ_circ_mult_1:
"x⇧∘ * 1⇧∘ = x⇧∘⇧∘"
by (metis L_left_zero sup_commute circ_sup_1 circ_circ_sup mult_zero_circ one_circ_split)
lemma circ_circ_mult:
"1⇧∘ * x⇧∘ = x⇧∘⇧∘"
by (metis order.antisym circ_circ_mult_1 circ_circ_sub_mult sub_mult_one_circ)
lemma circ_circ_split:
"x⇧∘⇧∘ = L ⊔ x⇧∘"
by (metis circ_circ_mult one_circ_mult_split)
lemma circ_sup_6:
"L ⊔ (x ⊔ y)⇧∘ = (x⇧∘ * y⇧∘)⇧∘"
by (metis sup_assoc sup_commute circ_sup_1 circ_circ_sup circ_circ_split circ_decompose_4)
end
class itering_L = itering + L +
assumes L_def: "L = 1⇧∘ * bot"
begin
lemma one_circ_split:
"1⇧∘ = L ⊔ 1"
by (metis L_def sup_commute order.antisym circ_sup_upper_bound circ_reflexive circ_simulate_absorb mult_1_right order_refl zero_right_mult_decreasing)
lemma one_circ_mult_split:
"1⇧∘ * x = L ⊔ x"
by (metis L_def sup_commute circ_loop_fixpoint mult_assoc mult_left_zero mult_zero_circ one_circ_split)
lemma sub_mult_one_circ_split:
"x * 1⇧∘ ≤ x ⊔ L"
by (metis sup_commute one_circ_mult_split sub_mult_one_circ)
lemma sub_mult_one_circ_split_2:
"x * 1⇧∘ ≤ x ⊔ 1⇧∘"
by (metis L_def sup_right_isotone order_trans sub_mult_one_circ_split zero_right_mult_decreasing)
lemma L_split:
"x * L ≤ x * bot ⊔ L"
by (metis L_def mult_assoc mult_left_isotone mult_right_dist_sup sub_mult_one_circ_split_2)
subclass left_conway_semiring_L
apply unfold_locales
apply (metis L_def sup_commute circ_loop_fixpoint mult_assoc mult_left_zero mult_zero_circ one_circ_split)
by (metis sup_commute mult_assoc mult_left_isotone one_circ_mult_split sub_mult_one_circ)
lemma circ_left_induct_mult_L:
"L ≤ x ⟹ x * y ≤ x ⟹ x * y⇧∘ ≤ x"
by (metis circ_one circ_simulate le_iff_sup one_circ_mult_split)
lemma circ_left_induct_mult_iff_L:
"L ≤ x ⟹ x * y ≤ x ⟷ x * y⇧∘ ≤ x"
by (metis sup.bounded_iff circ_back_loop_fixpoint circ_left_induct_mult_L le_iff_sup)
lemma circ_left_induct_L:
"L ≤ x ⟹ x * y ⊔ z ≤ x ⟹ z * y⇧∘ ≤ x"
by (metis sup.bounded_iff circ_left_induct_mult_L le_iff_sup mult_right_dist_sup)
end
end