Theory Binary_Iterings_Strict

(* Title:      Strict Binary Iterings
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

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