Theory Pre_Post_Modal

(* Title:      Pre-Post Specifications and Modal Operators
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section Pre-Post Specifications and Modal Operators

theory Pre_Post_Modal

imports Pre_Post Hoare_Modal

begin

class pre_post_spec_whiledo = pre_post_spec_greatest + whiledo
begin

lemma nat_test_pre_post:
  "nat_test t s  -q  s  (n . x  t n*-p*-q(pSum t n*-q))  -px  -q--p*-q"
  by (smt (verit, ccfv_threshold) nat_test_def nat_test_pre pSum_test_nat pre_post_galois tests_dual.sub_sup_closed)

lemma nat_test_pre_post_2:
  "nat_test t s  -r  s  (n . x  t n*-p(pSum t n))  -px  -r1"
  by (smt (verit, ccfv_threshold) nat_test_def nat_test_pre_2 one_def pSum_test_nat pre_post_galois tests_dual.sub_sup_closed)

end

class pre_post_spec_hoare = pre_post_spec_whiledo + hoare_calculus_sound
begin

lemma pre_post_while:
  "x  -p*-q-q  -px  aL*-q-q"
  by (smt aL_test pre_post_galois sub_mult_closed while_soundness)

text Theorem 43.1

lemma while_soundness_3:
  "test_seq t  -q  Sum t  x  t 0*-p*-qaL*-q  (n>0 . x  t n*-p*-qpSum t n*-q)  -px  -q--p*-q"
  by (smt (verit, del_insts) aL_test pSum_test tests_dual.inf_closed pre_post_galois sub_mult_closed test_seq_def while_soundness_1)

text Theorem 43.2

lemma while_soundness_4:
  "test_seq t  -r  Sum t  (n . x  t n*-ppSum t n)  -px  -r1"
  by (smt one_def pSum_test pre_post_galois sub_mult_closed test_seq_def while_soundness_2)

end

class pre_post_spec_hoare_pc_2 = pre_post_spec_hoare + hoare_calculus_pc_2
begin

text Theorem 43.3

lemma pre_post_while_pc:
  "x  -p*-q-q  -px  -q--p*-q"
  by (metis pre_post_galois sub_mult_closed while_soundness_pc)

end

class pre_post_spec_hoare_pc = pre_post_spec_hoare + hoare_calculus_pc
begin

subclass pre_post_spec_hoare_pc_2 ..

lemma pre_post_one_one_top:
  "11 = top"
  using order.eq_iff pre_one_one pre_post_one_one by auto

end

class pre_post_spec_H = pre_post_spec_greatest + box_precondition + havoc +
  assumes H_zero_2: "H * bot = bot"
  assumes H_split_2: "x  x * -q * top  H * --q"
begin

subclass idempotent_left_semiring_H
  apply unfold_locales
  apply (rule H_zero_2)
  by (smt H_split_2 tests_dual.complement_bot mult_assoc mult_left_zero mult_1_right one_def)

lemma pre_post_def_iff:
  "-p * x * --q  Z  x  Z  --p * top  H * -q"
proof (rule iffI)
  assume "-p * x * --q  Z"
  hence "x * --q * top  Z  --p * top"
    by (smt (verit, ccfv_threshold) Z_left_zero_above_one case_split_left_sup mult_assoc mult_left_isotone mult_right_dist_sup mult_right_isotone top_greatest top_mult_top)
  thus "x  Z  --p * top  H * -q"
    by (metis sup_left_isotone order_trans H_split_2 tests_dual.double_negation)
next
  assume "x  Z  --p * top  H * -q"
  hence "-p * x * --q  -p * (Z * --q  --p * top * --q  H * -q * --q)"
    by (metis mult_left_isotone mult_right_dist_sup mult_right_isotone mult_assoc)
  thus "-p * x * --q  Z"
    by (metis H_zero_2 Z_mult_decreasing sup_commute sup_bot_left mult_assoc mult_right_dist_sup mult_right_isotone order_trans test_mult_left_dist_shunt test_mult_left_sub_dist_shunt tests_dual.top_def)
qed

lemma pre_post_def:
  "-p-q = Z  --p*top  H*-q"
  by (meson order.antisym order_refl pre_Z pre_post_galois pre_post_def_iff)

end

class pre_post_L = pre_post_spec_greatest + box_while + left_conway_semiring_L + left_kleene_conway_semiring +
  assumes circ_below_L_add_star: "x  L  x"
begin

text a loop does not abort if its body does not abort
text this avoids abortion from all states* alternatively from states in -r if -r is an invariant

lemma body_abort_loop:
  assumes "Z = L"
      and "x  -p1"
    shows "-px  11"
proof -
  have "-p * x * bot  L"
    by (metis assms pre_Z pre_post_galois tests_dual.sba_dual.one_def tests_dual.top_double_complement)
  hence "(-p * x) * bot  L"
    by (metis L_split le_iff_sup star_left_induct sup_bot_left)
  hence "(-p * x) * bot  L"
    by (smt L_left_zero L_split sup_commute circ_below_L_add_star le_iff_sup mult_right_dist_sup)
  thus ?thesis
    by (metis assms(1) a_restrict mult_isotone pre_pc_Z pre_post_compose_2 pre_post_one_one tests_dual.sba_dual.one_def while_def tests_dual.sup_right_zero)
qed

end

class pre_post_spec_Hd = pre_post_spec_least + diamond_precondition + idempotent_left_semiring_Hd +
  assumes d_mult_top: "d(x) * top = x * top"
begin

subclass pre_post_spec_least_Hd
  apply unfold_locales
  by (simp add: d_mult_top diamond_x_1 pre_def)

end

end