Theory Pre_Post

(* Title:      Pre-Post Specifications
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at>

section Pre-Post Specifications

theory Pre_Post

imports Preconditions


class pre_post =
  fixes pre_post :: "'a  'a  'a" (infix "" 55)

class pre_post_spec_greatest = bounded_idempotent_left_semiring + precondition + pre_post +
  assumes pre_post_galois: "-p  x«-q  x  -p-q"

text Theorem 42.1

lemma post_pre_left_antitone:
  "x  y  y«-q  x«-q"
  by (smt order_refl order_trans pre_closed pre_post_galois)

lemma pre_left_sub_dist:
  "xy«-q  x«-q"
  by (simp add: post_pre_left_antitone)

text Theorem 42.2

lemma pre_post_left_antitone:
  "-p  -q  -q-r  -p-r"
  using order_lesseq_imp pre_post_galois by blast

lemma pre_post_left_sub_dist:
  "-p-q-r  -p-r"
  by (metis sup.cobounded1 tests_dual.sba_dual.sub_sup_closed pre_post_left_antitone)

lemma pre_post_left_sup_dist:
  "-p-r  -p*-q-r"
  by (metis tests_dual.sba_dual.sub_inf_def pre_post_left_sub_dist tests_dual.inf_absorb)

text Theorem 42.5

lemma pre_pre_post:
  "x  (x«-p)-p"
  by (metis order_refl pre_closed pre_post_galois)

text Theorem 42.6

lemma pre_post_pre:
  "-p  (-p-q)«-q"
  by (simp add: pre_post_galois)

text Theorem 42.8

lemma pre_post_zero_top:
  "bot-q = top"
  by (metis order.eq_iff pre_post_galois sup.cobounded2 sup_monoid.add_0_right top_greatest tests_dual.top_double_complement)

text Theorem 42.7

lemma pre_post_pre_one:
  "(1-q)«-q = 1"
  by (metis order.eq_iff pre_below_one tests_dual.sba_dual.top_double_complement pre_post_pre)

text Theorem 42.3

lemma pre_post_right_isotone:
  "-p  -q  -r-p  -r-q"
  using order_lesseq_imp pre_iso pre_post_galois by blast

lemma pre_post_right_sub_dist:
  "-r-p  -r-p-q"
  by (metis sup.cobounded1 tests_dual.sba_dual.sub_sup_closed pre_post_right_isotone)

lemma pre_post_right_sup_dist:
  "-r-p*-q  -r-p"
  by (metis tests_dual.sub_sup_closed pre_post_right_isotone tests_dual.upper_bound_left)

text Theorem 42.7

lemma pre_post_reflexive:
  "1  -p-p"
  using pre_one_increasing pre_post_galois by auto

text Theorem 42.9

lemma pre_post_compose:
  "-q  -r  (-p-q)*(-r-s)  -p-s"
  using order_lesseq_imp pre_compose pre_post_galois by blast

text Theorem 42.10

lemma pre_post_compose_1:
  "(-p-q)*(-q-r)  -p-r"
  by (simp add: pre_post_compose)

text Theorem 42.11

lemma pre_post_compose_2:
  "(-p-p)*(-p-q) = -p-q"
  by (meson case_split_left order.eq_iff le_supI1 pre_post_compose_1 pre_post_reflexive)

text Theorem 42.12

lemma pre_post_compose_3:
  "(-p-q)*(-q-q) = -p-q"
  by (meson order.eq_iff order.trans mult_right_isotone mult_sub_right_one pre_post_compose_1 pre_post_reflexive)

text Theorem 42.13

lemma pre_post_compose_4:
  "(-p-p)*(-p-p) = -p-p"
  by (simp add: pre_post_compose_3)

text Theorem 42.14

lemma pre_post_one_one:
  "x«1 = 1  x  11"
  by (metis order.eq_iff one_def pre_below_one pre_post_galois)

text Theorem 42.4

lemma post_pre_left_dist_sup:
  "xy«-q = (x«-q)*(y«-q)"
  apply (rule order.antisym)
  apply (metis mult_isotone pre_closed sup_commute tests_dual.sup_idempotent pre_left_sub_dist)
  by (smt (z3) order.refl pre_closed pre_post_galois sup.boundedI tests_dual.sba_dual.greatest_lower_bound tests_dual.sub_sup_closed)

proposition pre_post_right_dist_sup: "-p-q-r = (-p-q)  (-p-r)" nitpick [expect=genuine,card=4] oops


class pre_post_spec_greatest_2 = pre_post_spec_greatest + precondition_test_test

subclass precondition_test_box
  apply unfold_locales
  by (smt (verit) sup_commute mult_1_right tests_dual.double_negation order.eq_iff mult_left_one mult_right_dist_sup one_def tests_dual.inf_complement tests_dual.inf_complement_intro pre_below_one pre_import pre_post_galois pre_test_test tests_dual.top_def bot_least)

lemma pre_post_seq_sub_associative:
  "(-p-q)*-r  -p-q*-r"
  by (smt (z3) pre_compose pre_post_galois pre_post_pre sub_comm test_below_pre_test_mult tests_dual.sub_sup_closed)

lemma pre_post_right_import_mult:
  "(-p-q)*-r = (-p-q*-r)*-r"
  by (metis order.antisym mult_assoc tests_dual.sup_idempotent mult_left_isotone pre_post_right_sup_dist pre_post_seq_sub_associative)

lemma seq_pre_post_sub_associative:
  "-r*(-p-q)  --r-p-q"
  by (smt (z3) pre_compose pre_post_galois pre_post_pre pre_test tests_dual.sba_dual.reflexive tests_dual.sba_dual.sub_sup_closed)

lemma pre_post_left_import_sup:
  "-r*(-p-q) = -r*(--r-p-q)"
  by (metis sup_commute order.antisym mult_assoc tests_dual.sup_idempotent mult_right_isotone pre_post_left_sub_dist seq_pre_post_sub_associative)

lemma pre_post_import_same:
  "-p*(-p-q) = -p*(1-q)"
  using pre_test pre_test_test_same pre_post_left_import_sup by auto

lemma pre_post_import_complement:
  "--p*(-p-q) = --p*top"
  by (metis tests_dual.sup_idempotent tests_dual.inf_cases tests_dual.inf_closed pre_post_left_import_sup pre_post_zero_top tests_dual.top_def tests_dual.top_double_complement)

lemma pre_post_export:
  "-p-q = (1-q)  --p*top"
proof (rule order.antisym)
  have 1: "-p*(-p-q)  (1-q)  --p*top"
    by (metis le_supI1 pre_test pre_test_test_same seq_pre_post_sub_associative)
  have "--p*(-p-q)  (1-q)  --p*top"
    by (simp add: pre_post_import_complement)
  thus "-p-q  (1-q)  --p*top"
    using 1 by (smt case_split_left eq_refl tests_dual.inf_complement)
  show "(1-q)  --p*top  -p-q"
    by (metis le_sup_iff tests_dual.double_negation tests_dual.sub_bot_least pre_neg_mult pre_post_galois pre_post_pre_one)

lemma pre_post_left_dist_mult:
  "-p*-q-r = (-p-r)  (-q-r)"
proof -
  have "p q . -p*(-p*-q-r) = -p*(-q-r)"
    using sup_monoid.add_commute tests_dual.sba_dual.sub_inf_def pre_post_left_import_sup tests_dual.inf_complement_intro by auto
  hence 1: "(-p-q)*(-p*-q-r)  (-p-r)  (-q-r)"
    by (metis sup_commute le_sup_iff sup_ge2 mult_left_one mult_right_dist_sup tests_dual.inf_left_unit sub_comm)
  have "-(-p-q)*(-p*-q-r) = -(-p-q)*top"
    by (smt (z3) sup.left_commute sup_commute tests_dual.sba_dual.sub_sup_closed tests_dual.sub_sup_closed pre_post_import_complement pre_post_left_import_sup tests_dual.inf_absorb)
  hence "-(-p-q)*(-p*-q-r)  (-p-r)  (-q-r)"
    by (smt (z3) order.trans le_supI1 pre_post_left_sub_dist tests_dual.sba_dual.sub_sup_closed tests_dual.sub_sup_closed seq_pre_post_sub_associative)
  thus ?thesis
    using 1 by (smt (z3) le_sup_iff order.antisym case_split_left order_refl tests_dual.inf_closed tests_dual.inf_complement pre_post_left_sup_dist sub_comm)

lemma pre_post_left_import_mult:
  "-r*(-p-q) = -r*(-r*-p-q)"
  by (metis sup_commute tests_dual.inf_complement_intro pre_post_left_import_sup sub_mult_closed)

lemma pre_post_right_import_sup:
  "(-p-q)*-r = (-p-q--r)*-r"
  by (smt (z3) sup_monoid.add_commute tests_dual.sba_dual.inf_cases_2 tests_dual.sba_dual.inf_complement_intro tests_dual.sub_complement tests_dual.sub_inf_def pre_post_right_import_mult)

lemma pre_post_shunting:
  "x  -p*-q-r  -p*x  -q-r"
proof -
  have "--p*x  -p*-q-r"
    by (metis tests_dual.double_negation order_trans pre_neg_mult pre_post_galois pre_post_left_sup_dist)
  hence 1: "-p*x  -q-r  x  -p*-q-r"
    by (smt case_split_left eq_refl order_trans tests_dual.inf_complement pre_post_left_sup_dist sub_comm)
  have "-p*(-p*-q-r)  -q-r"
    by (metis mult_left_isotone mult_left_one tests_dual.sub_bot_least pre_post_left_import_mult)
  thus ?thesis
    using 1 mult_right_isotone order_lesseq_imp by blast

proposition pre_post_right_dist_sup: "-p-q-r = (-p-q)  (-p-r)" oops


class left_zero_pre_post_spec_greatest_2 = pre_post_spec_greatest_2 + bounded_idempotent_left_zero_semiring

lemma pre_post_right_dist_sup:
  "-p-q-r = (-p-q)  (-p-r)"
proof -
  have 1: "(-p-q-r)*-q  (-p-q)  (-p-r)"
    by (metis le_supI1 pre_post_seq_sub_associative tests_dual.sba_dual.inf_absorb tests_dual.sba_dual.sub_sup_closed)
  have "(-p-q-r)*--q = (-p-r)*--q"
    by (simp add: pre_post_right_import_sup sup_commute)
  hence "(-p-q-r)*--q  (-p-q)  (-p-r)"
    by (metis sup_ge2 mult_left_sub_dist_sup_right mult_1_right order_trans tests_dual.inf_left_unit)
  thus ?thesis
    using 1 by (metis le_sup_iff order.antisym case_split_right tests_dual.sub_bot_least tests_dual.inf_commutative tests_dual.inf_complement pre_post_right_sub_dist)


class havoc =
  fixes H :: "'a"

class idempotent_left_semiring_H = bounded_idempotent_left_semiring + havoc +
  assumes H_zero : "H * bot = bot"
  assumes H_split: "x  x * bot  H"

lemma H_galois:
  "x * bot  y  x  y  H"
  apply (rule iffI)
  using H_split order_lesseq_imp sup_mono apply blast
  by (smt (verit, ccfv_threshold) H_zero mult_right_dist_sup sup.cobounded2 sup.orderE sup_assoc sup_bot_left sup_commute zero_right_mult_decreasing)

lemma H_greatest_finite:
  "x * bot = bot  x  H"
  by (metis H_galois le_iff_sup sup_bot_left sup_monoid.add_0_right)

lemma H_reflexive:
  "1  H"
  using H_greatest_finite mult_left_one by blast

lemma H_transitive:
  "H = H * H"
  by (metis H_greatest_finite H_reflexive H_zero preorder_idempotent mult_assoc)

lemma T_split_H:
  "top * bot  H = top"
  by (simp add: H_split order.antisym)

proposition "H * (x  y) = H * x  H * y" nitpick [expect=genuine,card=6] oops


class pre_post_spec_least = bounded_idempotent_left_semiring + precondition_test_test + precondition_promote + pre_post +
  assumes test_mult_right_distr_sup: "-p * (x  y) = -p * x  -p * y"
  assumes pre_post_galois: "-p  x«-q  -p-q  x"

lemma shunting_top:
  "-p * x  y  x  y  --p * top"
  assume "-p * x  y"
  thus "x  y  --p * top"
    by (smt (verit, ccfv_SIG) case_split_left eq_refl le_supI1 le_supI2 mult_right_isotone tests_dual.sba_dual.top_def top_greatest)
  assume "x  y  --p * top"
  hence "-p * x  -p * y"
    by (metis sup_bot_right mult_assoc tests_dual.sup_complement mult_left_zero mult_right_isotone test_mult_right_distr_sup)
  thus "-p * x  y"
    by (metis mult_left_isotone mult_left_one tests_dual.sub_bot_least order_trans)

lemma post_pre_left_isotone:
  "x  y  x«-q  y«-q"
  by (smt order_refl order_trans pre_closed pre_post_galois)

lemma pre_left_sub_dist:
  "x«-q  xy«-q"
  by (simp add: post_pre_left_isotone)

lemma pre_post_left_isotone:
  "-p  -q  -p-r  -q-r"
  using order_lesseq_imp pre_post_galois by blast

lemma pre_post_left_sub_dist:
  "-p-r  -p-q-r"
  by (metis sup_ge1 tests_dual.inf_closed pre_post_left_isotone)

lemma pre_post_left_sup_dist:
  "-p*-q-r  -p-r"
  by (metis tests_dual.upper_bound_left pre_post_left_isotone sub_mult_closed)

lemma pre_pre_post:
  "(x«-p)-p  x"
  by (metis order_refl pre_closed pre_post_galois)

lemma pre_post_pre:
  "-p  (-p-q)«-q"
  by (simp add: pre_post_galois)

lemma pre_post_zero_top:
  "bot-q = bot"
  using bot_least order.eq_iff pre_post_galois tests_dual.sba_dual.sub_bot_def by blast

lemma pre_post_pre_one:
  "(1-q)«-q = 1"
  by (metis order.eq_iff pre_below_one pre_post_pre tests_dual.sba_dual.top_double_complement)

lemma pre_post_right_antitone:
  "-p  -q  -r-q  -r-p"
  using order_lesseq_imp pre_iso pre_post_galois by blast

lemma pre_post_right_sub_dist:
  "-r-p-q  -r-p"
  by (metis sup_ge1 tests_dual.inf_closed pre_post_right_antitone)

lemma pre_post_right_sup_dist:
  "-r-p  -r-p*-q"
  by (metis tests_dual.upper_bound_left pre_post_right_antitone sub_mult_closed)

lemma pre_top:
  "top«-q = 1"
  using order.eq_iff pre_below_one pre_post_galois tests_dual.sba_dual.one_def top_greatest by blast

lemma pre_mult_top_increasing:
  "-p  -p*top«-q"
  using pre_import_equiv pre_top tests_dual.sub_bot_least by auto

lemma pre_post_below_mult_top:
  "-p-q  -p*top"
  using pre_import_equiv pre_post_galois by auto

lemma pre_post_import_complement:
  "--p*(-p-q) = bot"
proof -
  have "--p*(-p-q)  --p*(-p*top)"
    by (simp add: mult_right_isotone pre_post_below_mult_top)
  thus ?thesis
    by (metis mult_assoc mult_left_zero sub_comm tests_dual.top_def order.antisym bot_least)

lemma pre_post_import_same:
  "-p*(-p-q) = -p-q"
proof -
  have "-p-q = -p*(-p-q)  --p*(-p-q)"
    by (metis mult_left_one mult_right_dist_sup tests_dual.inf_complement)
  thus ?thesis
    using pre_post_import_complement by auto

lemma pre_post_export:
  "-p-q = -p*(1-q)"
proof (rule order.antisym)
  show "-p-q  -p*(1-q)"
    by (metis tests_dual.sub_bot_least pre_import_equiv pre_post_galois pre_post_pre_one)
  have 1: "-p  ((-p-q)  --p*top)«-q"
    by (simp add: pre_post_galois)
  have "--p  ((-p-q)  --p*top)«-q"
    by (simp add: le_supI2 pre_post_galois pre_post_below_mult_top)
  hence "-p  --p  ((-p-q)  --p*top)«-q"
    using 1 le_supI by blast
  hence "1  ((-p-q)  --p*top)«-q"
    by simp
  hence "1-q  (-p-q)  --p*top"
    using pre_post_galois tests_dual.sba_dual.one_def by blast
  thus "-p*(1-q)  -p-q"
    by (simp add: shunting_top)

lemma pre_post_seq_associative:
  "-r*(-p-q) = -r*-p-q"
  by (metis pre_post_export tests_dual.sub_sup_closed mult_assoc)

lemma pre_post_left_import_mult:
  "-r*(-p-q) = -r*(-r*-p-q)"
  by (metis mult_assoc tests_dual.sup_idempotent pre_post_seq_associative)

lemma seq_pre_post_sub_associative:
  "-r*(-p-q)  --r-p-q"
  by (metis le_supI1 pre_post_left_sub_dist sup_commute shunting_top)

lemma pre_post_left_import_sup:
  "-r*(-p-q) = -r*(--r-p-q)"
  by (metis tests_dual.sba_dual.sub_sup_closed pre_post_seq_associative tests_dual.sup_complement_intro)

lemma pre_post_left_dist_sup:
  "-p-q-r = (-p-r)  (-q-r)"
  by (metis mult_right_dist_sup tests_dual.inf_closed pre_post_export)

lemma pre_post_reflexive:
  "-p-p  1"
  using pre_one_increasing pre_post_galois by auto

lemma pre_post_compose:
  "-q  -r  -p-s  (-p-q)*(-r-s)"
  by (meson pre_compose pre_post_galois pre_post_pre pre_post_right_antitone)

lemma pre_post_compose_1:
  "-p-r  (-p-q)*(-q-r)"
  by (simp add: pre_post_compose)

lemma pre_post_compose_2:
  "(-p-p)*(-p-q) = -p-q"
  using order.eq_iff mult_left_isotone pre_post_compose_1 pre_post_reflexive by fastforce

lemma pre_post_compose_3:
  "(-p-q)*(-q-q) = -p-q"
  by (metis order.antisym mult_right_isotone mult_1_right pre_post_compose_1 pre_post_reflexive)

lemma pre_post_compose_4:
  "(-p-p)*(-p-p) = -p-p"
  by (simp add: pre_post_compose_3)

lemma pre_post_one_one:
  "x«1 = 1  11  x"
  using order.eq_iff pre_below_one pre_post_galois tests_dual.sub_bot_def by force

lemma pre_one_right:
  "-p«1 = -p"
  by (metis order.antisym mult_1_right one_def tests_dual.inf_complement pre_left_sub_dist pre_mult_top_increasing pre_one pre_seq pre_test_promote pre_top)

lemma pre_pre_one:
  "x«-q = x*-q«1"
  by (metis one_def pre_one_right pre_seq)

subclass precondition_test_diamond
  apply unfold_locales
  using tests_dual.sba_dual.sub_inf_def pre_one_right pre_pre_one by auto

proposition pre_post_shunting: "x  -p*-q-r  -p*x  -q-r" nitpick [expect=genuine,card=3] oops
proposition "(-p-q)*-r = (-p-q-r)*-r" nitpick [expect=genuine,card=3] oops
proposition "(-p-q)*-r = (-p-q--r)*-r" nitpick [expect=genuine,card=3] oops
proposition "(-p-q)*-r = (-p-q*-r)*-r" nitpick [expect=genuine,card=3] oops
proposition "(-p-q)*-r = (-p-q*--r)*-r" nitpick [expect=genuine,card=3] oops
proposition "-p-q-r = (-p-q)  (-p-r)" nitpick [expect=genuine,card=3] oops
proposition "-p-q-r = (-p-q) * (-p-r)" nitpick [expect=genuine,card=3] oops
proposition pre_post_right_dist_mult: "-p-q*-r = (-p-q) * (-p-r)" oops
proposition pre_post_right_dist_mult: "-p-q*-r = (-p-q)  (-p-r)" oops
proposition post_pre_left_dist_sup: "xy«-q = (x«-q)  (y«-q)" oops


class havoc_dual =
  fixes Hd :: "'a"

class idempotent_left_semiring_Hd = bounded_idempotent_left_semiring + havoc_dual +
  assumes Hd_total: "Hd * top = top"
  assumes Hd_least: "x * top = top  Hd  x"

lemma Hd_least_total:
  "x * top = top  Hd  x"
  by (metis Hd_least Hd_total order.antisym mult_left_isotone top_greatest)

lemma Hd_reflexive:
  "Hd  1"
  by (simp add: Hd_least)

lemma Hd_transitive:
  "Hd = Hd * Hd"
  by (simp add: Hd_least Hd_total order.antisym coreflexive_transitive total_mult_closed)


class pre_post_spec_least_Hd = idempotent_left_semiring_Hd + pre_post_spec_least +
  assumes pre_one_mult_top: "(x«1)*top = x*top"

lemma Hd_pre_one:
  "Hd«1 = 1"
  by (metis Hd_total pre_seq pre_top)

lemma pre_post_below_Hd:
  "11  Hd"
  using Hd_pre_one pre_post_one_one by auto

lemma Hd_pre_post:
  "Hd = 11"
  by (metis Hd_least Hd_pre_one Hd_total order.eq_iff pre_one_mult_top pre_post_one_one)

lemma top_left_zero:
  "top*x = top"
  by (metis mult_assoc mult_left_one mult_left_zero pre_closed pre_one_mult_top pre_seq pre_top)

lemma test_dual_test:
  "(-p--p*top)*-p = -p--p*top"
  by (simp add: top_left_zero mult_right_dist_sup mult_assoc)

lemma pre_zero_mult_top:
  "(x«bot)*top = x*bot"
  by (metis mult_assoc mult_left_zero one_def pre_one_mult_top pre_seq pre_bot)

lemma pre_one_mult_Hd:
  "(x«1)*Hd  x"
  by (metis Hd_pre_post one_def pre_closed pre_post_export pre_pre_post)

lemma Hd_mult_pre_one:
  "Hd*(x«1)  x"
proof -
  have 1: "-(x«1)*Hd*(x«1)  x"
    by (metis Hd_pre_post le_iff_sup mult_left_isotone pre_closed pre_one_right pre_post_export pre_pre_post sup_commute sup_monoid.add_0_right tests_dual.sba_dual.one_def tests_dual.top_def)
  have "(x«1)*Hd*(x«1)  x"
    by (metis mult_isotone mult_1_right one_def pre_below_one pre_one_mult_Hd)
  thus ?thesis
    using 1 by (metis case_split_left pre_closed reflexive_one_closed tests_dual.sba_dual.one_def tests_dual.sba_dual.top_def mult_assoc)

lemma pre_post_one_def_1:
  assumes "1  x«-q"
    shows "Hd*(-q--q*top)  x"
proof -
  have "Hd*(-q--q*top)  x*-q*(-q--q*top)"
    by (metis assms Hd_pre_post order.antisym pre_below_one pre_post_one_one pre_pre_one mult_left_isotone)
  thus ?thesis
    by (metis mult_assoc tests_dual.sup_complement mult_left_sub_dist_sup_left mult_left_zero mult_1_right tests_dual.inf_complement test_mult_right_distr_sup order_trans)

lemma pre_post_one_def:
  "1-q = Hd*(-q--q*top)"
proof (rule order.antisym)
  have "1  (11)*(-q--q)«1"
    by (metis pre_post_pre one_def mult_1_right tests_dual.inf_complement)
  also have "...  (11)*(-q--q*top)«-q"
    by (metis sup_right_isotone mult_right_isotone mult_1_right one_def post_pre_left_isotone pre_seq pre_test_promote test_dual_test top_right_mult_increasing)
  finally show "1-q  Hd*(-q--q*top)"
    using Hd_pre_post pre_post_galois tests_dual.sub_bot_def by blast
  show "Hd*(-q--q*top)  1-q"
    by (simp add: pre_post_pre_one pre_post_one_def_1)

lemma pre_post_def:
  "-p-q = -p*Hd*(-q--q*top)"
  by (simp add: pre_post_export mult_assoc pre_post_one_def)