Theory Pre_Post

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

section ‹Pre-Post Specifications›

theory Pre_Post

imports Preconditions

begin

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"
begin

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:
  "x⊔y«-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 ≤ 1⊣1"
  by (metis order.eq_iff one_def pre_below_one pre_post_galois)

text ‹Theorem 42.4›

lemma post_pre_left_dist_sup:
  "x⊔y«-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

end

class pre_post_spec_greatest_2 = pre_post_spec_greatest + precondition_test_test
begin

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)
next
  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)
qed

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)
qed

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
qed

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

end

class left_zero_pre_post_spec_greatest_2 = pre_post_spec_greatest_2 + bounded_idempotent_left_zero_semiring
begin

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)
qed

end

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"
begin

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

end

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"
begin

lemma shunting_top:
  "-p * x ≤ y ⟷ x ≤ y ⊔ --p * top"
proof
  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)
next
  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)
qed

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 ≤ x⊔y«-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)
qed

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
qed

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)
next
  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)
qed

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 ⟷ 1⊣1 ≤ 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: "x⊔y«-q = (x«-q) ⊔ (y«-q)" oops

end

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"
begin

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)

end

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

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

lemma pre_post_below_Hd:
  "1⊣1 ≤ Hd"
  using Hd_pre_one pre_post_one_one by auto

lemma Hd_pre_post:
  "Hd = 1⊣1"
  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)
qed

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)
qed

lemma pre_post_one_def:
  "1⊣-q = Hd*(-q⊔--q*top)"
proof (rule order.antisym)
  have "1 ≤ (1⊣1)*(-q⊔--q)«1"
    by (metis pre_post_pre one_def mult_1_right tests_dual.inf_complement)
  also have "... ≤ (1⊣1)*(-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
next
  show "Hd*(-q⊔--q*top) ≤ 1⊣-q"
    by (simp add: pre_post_pre_one pre_post_one_def_1)
qed

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

end

end