Theory Hoare_Modal

(* Title:      Hoare Calculus and Modal Operators
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section Hoare Calculus and Modal Operators

theory Hoare_Modal

imports Stone_Kleene_Relation_Algebras.Kleene_Algebras Complete_Domain Hoare Relative_Modal

begin

class box_precondition = relative_box_semiring + pre +
  assumes pre_def: "x«p = |x]p"
begin

text Theorem 47

subclass precondition
  apply unfold_locales
  apply (simp add: box_x_a pre_def)
  apply (simp add: box_left_mult pre_def)
  using box_def box_right_submult_a_a pre_def tests_dual.sba_dual.greatest_lower_bound apply fastforce
  by (simp add: box_1_a pre_def)

subclass precondition_test_test
  apply unfold_locales
  by (simp add: a_box_a_a pre_def)

subclass precondition_promote
  apply unfold_locales
  using a_mult_d box_def pre_def pre_test_test by auto

subclass precondition_test_box
  apply unfold_locales
  by (simp add: box_a_a d_def pre_def)

lemma pre_Z:
  "-p  x«-q  -p * x * --q  Z"
  by (simp add: box_demodalisation_2 pre_def)

lemma pre_left_dist_add:
  "xy«-q = (x«-q) * (y«-q)"
  by (simp add: box_left_dist_sup pre_def)

lemma pre_left_antitone:
  "x  y  y«-q  x«-q"
  by (simp add: box_antitone_isotone pre_def)

lemma pre_promote_neg:
  "(x«-q) * x * --q  Z"
  by (simp add: box_below_Z pre_def)

lemma pre_pc_Z:
  "x«1 = 1  x * bot  Z"
  by (simp add: a_strict box_x_1 pre_def)

proposition pre_sub_promote: "(x«-q) * x  (x«-q) * x * -q  Z" nitpick [expect=genuine,card=6] oops
proposition pre_promote: "(x«-q) * x  Z = (x«-q) * x * -q  Z" nitpick [expect=genuine,card=6] oops
proposition pre_mult_sub_promote: "(x*y«-q) * x  (x*y«-q) * x * (y«-q)  Z" nitpick [expect=genuine,card=6] oops
proposition pre_mult_promote: "(x*y«-q) * x * (y«-q)  Z = (x*y«-q) * x  Z" nitpick [expect=genuine,card=6] oops

end

class left_zero_box_precondition = box_precondition + relative_left_zero_antidomain_semiring
begin

lemma pre_sub_promote:
  "(x«-q) * x  (x«-q) * x * -q  Z"
  using case_split_right_sup pre_promote_neg by blast

lemma pre_promote:
  "(x«-q) * x  Z = (x«-q) * x * -q  Z"
  apply (rule sup_same_context)
  apply (simp add: pre_sub_promote)
  by (metis a_below_one le_supI1 mult_1_right mult_right_isotone)

lemma pre_mult_sub_promote:
  "(x*y«-q) * x  (x*y«-q) * x * (y«-q)  Z"
  by (metis pre_closed pre_seq pre_sub_promote)

lemma pre_mult_promote_sub:
  "(x*y«-q) * x * (y«-q)  (x*y«-q) * x"
  by (metis mult_right_isotone mult_1_right pre_below_one)

lemma pre_mult_promote:
  "(x*y«-q) * x * (y«-q)  Z = (x*y«-q) * x  Z"
  by (metis sup_ge1 sup_same_context order_trans pre_mult_sub_promote pre_mult_promote_sub)

end

class diamond_precondition = relative_box_semiring + pre +
  assumes pre_def: "x«p = |x>p"
begin

text Theorem 47

subclass precondition
  apply unfold_locales
  apply (simp add: d_def diamond_def pre_def)
  apply (simp add: diamond_left_mult pre_def)
  apply (metis a_antitone a_dist_sup box_antitone_isotone box_deMorgan_1 order.refl pre_def sup_right_divisibility)
  by (simp add: diamond_1_a pre_def)

subclass precondition_test_test
  apply unfold_locales
  by (metis diamond_a_a_same diamond_a_export diamond_associative diamond_right_mult pre_def)

subclass precondition_promote
  apply unfold_locales
  using d_def diamond_def pre_def pre_test_test tests_dual.sub_sup_closed by force

subclass precondition_test_diamond
  apply unfold_locales
  by (simp add: diamond_a_a pre_def)

lemma pre_left_dist_add:
  "xy«-q = (x«-q)  (y«-q)"
  by (simp add: diamond_left_dist_sup pre_def)

lemma pre_left_isotone:
  "x  y  x«-q  y«-q"
  by (metis diamond_left_isotone pre_def)

end

class box_while = box_precondition + bounded_left_conway_semiring + ite + while +
  assumes ite_def:   "xpy = p * x  -p * y"
  assumes while_def: "px = (p * x) * -p"
begin

subclass bounded_relative_antidomain_semiring ..

lemma Z_circ_left_zero:
  "Z * x = Z"
  using Z_left_zero_above_one circ_plus_one sup.absorb_iff2 by auto

subclass ifthenelse
  apply unfold_locales
  by (smt a_d_closed box_a_export box_left_dist_sup box_x_a tests_dual.case_duality d_def ite_def pre_def)

text Theorem 48.1

subclass whiledo
  apply unfold_locales
  apply (smt circ_loop_fixpoint ite_def ite_pre mult_assoc mult_1_right pre_one pre_seq while_def)
  using pre_mult_test_promote while_def by auto

lemma pre_while_1:
  "-p*(-px)«1 = -px«1"
proof -
  have "--p*(-p*(-px)«1) = --p*(-px«1)"
    by (metis mult_1_right pre_closed pre_seq pre_test_neg tests_dual.sba_dual.top_double_complement while_pre_else)
  thus ?thesis
    by (smt (z3) pre_closed pre_import tests_dual.sba_dual.top_double_complement tests_dual.sup_eq_cases)
qed

lemma aL_one_circ:
  "aL = a(1*bot)"
  by (metis aL_def box_left_mult box_x_a idempotent_bot_closed idempotent_one_closed pre_def tests_dual.sba_dual.one_def while_def tests_dual.one_def)

end

class diamond_while = diamond_precondition + bounded_left_conway_semiring + ite + while +
  assumes ite_def:   "xpy = p * x  -p * y"
  assumes while_def: "px = (p * x) * -p"
begin

subclass bounded_relative_antidomain_semiring ..

lemma Z_circ_left_zero:
  "Z * x = Z"
  by (simp add: Z_left_zero_above_one circ_reflexive)

subclass ifthenelse
  apply unfold_locales
  by (simp add: ite_def pre_export pre_left_dist_add)

text Theorem 48.2

subclass whiledo
  apply unfold_locales
  apply (smt circ_loop_fixpoint ite_def ite_pre mult_assoc mult_1_right pre_one pre_seq while_def)
  by (simp add: pre_mult_test_promote while_def)

lemma aL_one_circ:
  "aL = d(1*bot)"
  by (metis aL_def tests_dual.complement_bot diamond_x_1 mult_left_one pre_def while_def)

end

class box_while_program = box_while + atoms
begin

subclass while_program ..

end

class diamond_while_program = diamond_while + atoms
begin

subclass while_program ..

end

class box_hoare_calculus = box_while_program + complete_antidomain_semiring
begin

subclass hoare_calculus ..

end

class diamond_hoare_calculus = diamond_while_program + complete_antidomain_semiring
begin

subclass hoare_calculus ..

end

class box_hoare_sound = box_hoare_calculus + relative_domain_semiring_split + left_kleene_conway_semiring +
  assumes aL_circ: "aL * x  x"
begin

lemma aL_circ_ext:
  "|x]y  |aL * x]y"
  by (simp add: aL_circ box_left_antitone)

lemma box_star_induct:
  assumes "-p  |x](-p)"
    shows "-p  |x](-p)"
proof -
  have 1: "x*--p*top  Z  --p*top"
    by (metis assms Z_top sup_commute box_demodalisation_2 mult_assoc mult_left_isotone shunting_Z)
  have "x*(Z  --p*top)  x*--p*top  Z"
    using split_Z sup_monoid.add_commute mult_assoc by force
  also have "...  Z  --p*top"
    using 1 by simp
  finally have "x*(Z  --p*top)  --p  Z  --p*top"
    using le_supI2 sup.bounded_iff top_right_mult_increasing by auto
  thus ?thesis
    by (metis sup_commute box_demodalisation_2 mult_assoc shunting_Z star_left_induct)
qed

lemma box_circ_induct:
  "-p  |x](-p)  -p*aL  |x](-p)"
  by (smt aL_circ_ext aL_test box_left_mult box_star_induct order_trans tests_dual.inf_commutative pre_closed pre_def pre_test tests_dual.shunting_right)

lemma a_while_soundness:
  assumes "-p*-q  |x](-q)"
    shows "aL*-q  |(-p*x)*--p](-q)"
proof -
  have "|(-p*x)](-q)  |(-p*x)*--p](-q)"
    by (meson box_left_antitone circ_mult_upper_bound circ_reflexive order.refl order.trans tests_dual.sub_bot_least)
  thus ?thesis
    by (smt assms box_import_shunting box_circ_induct order_trans sub_comm aL_test)
qed

subclass hoare_calculus_sound
  apply unfold_locales
  by (simp add: a_while_soundness pre_def while_def)

end

class diamond_hoare_sound = diamond_hoare_calculus + left_kleene_conway_semiring +
  assumes aL_circ: "aL * x  x"
begin

lemma aL_circ_equal:
  "aL * x = aL * x"
  apply (rule order.antisym)
  using aL_circ aL_one_circ d_restrict_iff_1 apply force
  by (simp add: mult_right_isotone star_below_circ)

lemma aL_zero:
  "aL = bot"
  by (smt aL_circ_equal aL_one_circ d_export d_idempotent diamond_d_bot diamond_def mult_assoc mult_1_right star_one)

subclass hoare_calculus_sound
  apply unfold_locales
  using aL_zero by auto

end

class box_hoare_complete = box_hoare_calculus + left_kleene_conway_semiring +
  assumes box_circ_induct_2: "-p*|x](-q)  -q  |x](-p)  -qaL"
  assumes aL_zero_or_one: "aL = bot  aL = 1"
  assumes while_mult_left_dist_Prod: "x  While_program  descending_chain t  test_seq t  x*Prod t = Prod (λn . x*t n)"
begin

subclass hoare_calculus_complete
  apply unfold_locales
  apply (metis aL_zero_or_one bot_least order.eq_iff mult_1_right pre_closed tests_dual.sup_right_zero)
  subgoal
    apply (unfold pre_def box_def)
    by (metis a_ascending_chain a_dist_Prod a_dist_Sum descending_chain_left_mult while_mult_left_dist_Prod test_seq_def)
  by (smt box_circ_induct_2 tests_dual.double_negation tests_dual.greatest_lower_bound tests_dual.upper_bound_left mult_right_dist_sup pre_closed pre_def pre_import pre_seq pre_test sub_mult_closed while_def)

end

class diamond_hoare_complete = diamond_hoare_calculus + relative_domain_semiring_split + left_kleene_conway_semiring +
  assumes dL_circ: "-aL*x  x"
  assumes aL_zero_or_one: "aL = bot  aL = 1"
  assumes while_mult_left_dist_Sum: "x  While_program  ascending_chain t  test_seq t  x*Sum t = Sum (λn . x*t n)"
begin

lemma diamond_star_induct_var:
  assumes "|x>(d p)  d p"
    shows "|x>(d p)  d p"
proof -
  have "x * (d p * x  Z)  d p * x * x  Z * x  Z"
    by (metis assms sup_left_isotone d_mult_d diamond_def diamond_demodalisation_3 mult_assoc mult_left_isotone mult_right_dist_sup order_trans split_Z)
  also have "...  d p * x  Z"
    by (metis Z_mult_decreasing mult_right_isotone star.left_plus_below_circ sup.bounded_iff sup_ge1 sup_mono sup_monoid.add_commute mult_assoc)
  finally show ?thesis
    by (smt sup_commute le_sup_iff sup_ge2 d_mult_d diamond_def diamond_demodalisation_3 order_trans star.circ_back_loop_prefixpoint star_left_induct)
qed

lemma diamond_star_induct:
  "d q  |x>(d p)  d p  |x>(d q)  d p"
  by (metis le_sup_iff diamond_star_induct_var diamond_right_isotone order_trans)

lemma while_completeness_1:
  assumes "-p*(x«-q)  -q"
    shows "-px«-q  -qaL"
proof -
  have "--p*-q  |-p*x>(-q)  -q"
    using assms pre_def pre_export tests_dual.upper_bound_right by auto
  hence "|(-p*x)>(--p*-q)  -q"
    by (smt diamond_star_induct d_def sub_mult_closed tests_dual.double_negation)
  hence "|-aL*(-p*x)>(--p*-q)  -q"
    by (meson dL_circ diamond_isotone order.eq_iff order.trans)
  thus ?thesis
    by (smt aL_test diamond_a_export diamond_def mult_assoc tests_dual.inf_commutative pre_closed pre_def tests_dual.shunting while_def)
qed

subclass hoare_calculus_complete
  apply unfold_locales
  apply (metis aL_test aL_zero_or_one bot_least order.eq_iff pre_closed pre_test pre_test_one tests_dual.sup_right_zero)
  subgoal
    apply (unfold pre_def diamond_def)
    by (simp add: ascending_chain_left_mult d_dist_Sum while_mult_left_dist_Sum)
  by (simp add: while_completeness_1)

end

class box_hoare_valid = box_hoare_sound + box_hoare_complete + hoare_triple +
  assumes hoare_triple_def: "pxq  p  |x]q"
begin

text Theorem 49.2

subclass hoare_calculus_valid
  apply unfold_locales
  by (simp add: hoare_triple_def pre_def)

lemma rule_skip_valid:
  "-p1-p"
  by (simp add: rule_skip)

end

class diamond_hoare_valid = diamond_hoare_sound + diamond_hoare_complete + hoare_triple +
  assumes hoare_triple_def: "pxq  p  |x>q"
begin

lemma circ_star_equal:
  "x = x"
  by (metis aL_zero order.antisym dL_circ mult_left_one one_def star_below_circ)

text Theorem 49.1

subclass hoare_calculus_valid
  apply unfold_locales
  by (simp add: hoare_triple_def pre_def)

end

class diamond_hoare_sound_2 = diamond_hoare_calculus + left_kleene_conway_semiring +
  assumes diamond_circ_induct_2: "--p*-q  |x>(-q)   aL*-q  |x>(-p)"
begin

subclass hoare_calculus_sound
  apply unfold_locales
  by (smt a_export diamond_associative diamond_circ_induct_2 tests_dual.double_negation tests_dual.sup_complement_intro pre_def pre_import_equiv_mult sub_comm sub_mult_closed while_def)

end

class diamond_hoare_valid_2 = diamond_hoare_sound_2 + diamond_hoare_complete + hoare_triple +
  assumes hoare_triple_def: "pxq  p  |x>q"
begin

subclass hoare_calculus_valid
  apply unfold_locales
  by (simp add: hoare_triple_def pre_def)

end

end