Theory Binary_Iterings_Strict
section ‹Strict Binary Iterings›
theory Binary_Iterings_Strict
imports Stone_Kleene_Relation_Algebras.Iterings Binary_Iterings
begin
class strict_itering = itering + while +
assumes while_def: "x ⋆ y = x⇧∘ * y"
begin
text ‹Theorem 8.1›
subclass extended_binary_itering
apply unfold_locales
apply (metis circ_loop_fixpoint circ_slide_1 sup_commute while_def mult_assoc)
apply (metis circ_sup mult_assoc while_def)
apply (simp add: mult_left_dist_sup while_def)
apply (simp add: while_def mult_assoc)
apply (metis circ_simulate_left_plus mult_assoc mult_left_isotone mult_right_dist_sup mult_1_right while_def)
apply (metis circ_simulate_right_plus mult_assoc mult_left_isotone mult_right_dist_sup while_def)
by (metis circ_loop_fixpoint mult_right_sub_dist_sup_right while_def mult_assoc)
text ‹Theorem 13.1›
lemma while_associative:
"(x ⋆ y) * z = x ⋆ (y * z)"
by (simp add: while_def mult_assoc)
text ‹Theorem 13.3›
lemma while_one_mult:
"(x ⋆ 1) * x = x ⋆ x"
by (simp add: while_def)
lemma while_back_loop_is_fixpoint:
"is_fixpoint (λx . x * y ⊔ z) (z * (y ⋆ 1))"
by (simp add: circ_back_loop_is_fixpoint while_def)
text ‹Theorem 13.4›
lemma while_sumstar_var:
"(x ⊔ y) ⋆ z = ((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z)"
by (simp add: while_sumstar_3 while_associative)
text ‹Theorem 13.2›
lemma while_mult_1_assoc:
"(x ⋆ 1) * y = x ⋆ y"
by (simp add: while_def)
proposition "y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1) ⟹ (x ⊔ y) ⋆ 1 = x ⋆ (y ⋆ 1)" oops
proposition "y * x ≤ (1 ⊔ x) * (y ⋆ 1) ⟹ (x ⊔ y) ⋆ 1 = x ⋆ (y ⋆ 1)" oops
proposition while_square_1: "x ⋆ 1 = (x * x) ⋆ (x ⊔ 1)" oops
proposition while_absorb_below_one: "y * x ≤ x ⟹ y ⋆ x ≤ 1 ⋆ x" oops
end
class bounded_strict_itering = bounded_itering + strict_itering
begin
subclass bounded_extended_binary_itering ..
text ‹Theorem 13.6›
lemma while_top_2:
"top ⋆ z = top * z"
by (simp add: circ_top while_def)
text ‹Theorem 13.5›
lemma while_mult_top_2:
"(x * top) ⋆ z = z ⊔ x * top * z"
by (metis circ_left_top mult_assoc while_def while_left_unfold)
text ‹Theorem 13 counterexamples›
proposition while_one_top: "1 ⋆ x = top" nitpick [expect=genuine,card=2] oops
proposition while_top: "top ⋆ x = top" nitpick [expect=genuine,card=2] oops
proposition while_sub_mult_one: "x * (1 ⋆ y) ≤ 1 ⋆ x" oops
proposition while_unfold_below_1: "x = y * x ⟹ x ≤ y ⋆ 1" oops
proposition while_unfold_below: "x = z ⊔ y * x ⟹ x ≤ y ⋆ z" nitpick [expect=genuine,card=2] oops
proposition while_unfold_below: "x ≤ z ⊔ y * x ⟹ x ≤ y ⋆ z" nitpick [expect=genuine,card=2] oops
proposition while_mult_top: "(x * top) ⋆ z = z ⊔ x * top" nitpick [expect=genuine,card=2] oops
proposition tarski_mult_top_idempotent: "x * top = x * top * x * top" oops
proposition while_loop_is_greatest_postfixpoint: "is_greatest_postfixpoint (λx . y * x ⊔ z) (y ⋆ z)" nitpick [expect=genuine,card=2] oops
proposition while_loop_is_greatest_fixpoint: "is_greatest_fixpoint (λx . y * x ⊔ z) (y ⋆ z)" nitpick [expect=genuine,card=2] oops
proposition while_sub_while_zero: "x ⋆ z ≤ (x ⋆ y) ⋆ z" oops
proposition while_while_sub_associative: "x ⋆ (y ⋆ z) ≤ (x ⋆ y) ⋆ z" oops
proposition tarski: "x ≤ x * top * x * top" oops
proposition tarski_top_omega_below: "x * top ≤ (x * top) ⋆ bot" nitpick [expect=genuine,card=2] oops
proposition tarski_top_omega: "x * top = (x * top) ⋆ bot" nitpick [expect=genuine,card=2] oops
proposition tarski_below_top_omega: "x ≤ (x * top) ⋆ bot" nitpick [expect=genuine,card=2] oops
proposition tarski: "x = bot ∨ top * x * top = top" oops
proposition "1 = (x * bot) ⋆ 1" oops
proposition "1 ⊔ x * bot = x ⋆ 1" oops
proposition "x = x * (x ⋆ 1)" oops
proposition "x * (x ⋆ 1) = x ⋆ 1" oops
proposition "x ⋆ 1 = x ⋆ (1 ⋆ 1)" oops
proposition "(x ⊔ y) ⋆ 1 = (x ⋆ (y ⋆ 1)) ⋆ 1" oops
proposition "z ⊔ y * x = x ⟹ y ⋆ z ≤ x" oops
proposition "y * x = x ⟹ y ⋆ x ≤ x" oops
proposition "z ⊔ x * y = x ⟹ z * (y ⋆ 1) ≤ x" oops
proposition "x * y = x ⟹ x * (y ⋆ 1) ≤ x" oops
proposition "x * z = z * y ⟹ x ⋆ z ≤ z * (y ⋆ 1)" oops
end
class binary_itering_unary = extended_binary_itering + circ +
assumes circ_def: "x⇧∘ = x ⋆ 1"
begin
text ‹Theorem 50.7›
subclass left_conway_semiring
apply unfold_locales
using circ_def while_left_unfold apply simp
apply (metis circ_def mult_1_right while_one_mult_below while_slide)
using circ_def while_one_while while_sumstar_2 by auto
end
class strict_binary_itering = binary_itering + circ +
assumes while_associative: "(x ⋆ y) * z = x ⋆ (y * z)"
assumes circ_def: "x⇧∘ = x ⋆ 1"
begin
text ‹Theorem 2.8›
subclass itering
apply unfold_locales
apply (simp add: circ_def while_associative while_sumstar)
apply (metis circ_def mult_1_right while_associative while_productstar while_slide)
apply (metis circ_def mult_1_right while_associative mult_1_left while_slide while_simulate_right_plus)
by (metis circ_def mult_1_right while_associative mult_1_left while_simulate_left_plus mult_right_dist_sup)
text ‹Theorem 8.5›
subclass extended_binary_itering
apply unfold_locales
by (simp add: while_associative while_increasing mult_assoc)
end
end