Theory Preconditions

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

section ‹Preconditions›

theory Preconditions

imports Tests

begin

class pre =
  fixes pre :: "'a ⇒ 'a ⇒ 'a" (infixr "«" 55)

class precondition = tests + pre +
  assumes pre_closed: "x«-q = --(x«-q)"
  assumes pre_seq: "x*y«-q = x«y«-q"
  assumes pre_lower_bound_right: "x«-p*-q ≤ x«-q"
  assumes pre_one_increasing: "-q ≤ 1«-q"
begin

text ‹Theorem 39.2›

lemma pre_sub_distr:
  "x«-p*-q ≤ (x«-p)*(x«-q)"
  by (smt (z3) pre_closed pre_lower_bound_right tests_dual.sub_commutative tests_dual.sub_sup_closed tests_dual.least_upper_bound)

text ‹Theorem 39.5›

lemma pre_below_one:
  "x«-p ≤ 1"
  by (metis pre_closed tests_dual.sub_bot_least)

lemma pre_lower_bound_left:
  "x«-p*-q ≤ x«-p"
  using pre_lower_bound_right tests_dual.sub_commutative by fastforce

text ‹Theorem 39.1›

lemma pre_iso:
  "-p ≤ -q ⟹ x«-p ≤ x«-q"
  by (metis leq_def pre_lower_bound_right)

text ‹Theorem 39.4 and Theorem 40.9›

lemma pre_below_pre_one:
  "x«-p ≤ x«1"
  using tests_dual.sba_dual.one_def pre_iso tests_dual.sub_bot_least by blast

text ‹Theorem 39.3›

lemma pre_seq_below_pre_one:
  "x*y«1 ≤ x«1"
  by (metis one_def pre_below_pre_one pre_closed pre_seq)

text ‹Theorem 39.6›

lemma pre_compose:
  "-p ≤ x«-q ⟹ -q ≤ y«-r ⟹ -p ≤ x*y«-r"
  by (metis pre_closed pre_iso tests_dual.transitive pre_seq)

proposition pre_test_test: "-p*(-p«-q) = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_test_promote: "-p«-q = -p«-p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = --p⊔-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_distr_mult: "x«-p*-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=4] oops
proposition pre_distr_plus: "x«-p⊔-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=2] oops

end

class precondition_test_test = precondition +
  assumes pre_test_test: "-p*(-p«-q) = -p*-q"
begin

lemma pre_one:
  "1«-p = -p"
  by (metis pre_closed pre_test_test tests_dual.sba_dual.one_def tests_dual.sup_left_unit)

lemma pre_import:
  "-p*(x«-q) = -p*(-p*x«-q)"
  by (metis pre_closed pre_seq pre_test_test)

lemma pre_import_composition:
  "-p*(-p*x*y«-q) = -p*(x«y«-q)"
  by (metis pre_closed pre_seq pre_import)

lemma pre_import_equiv:
  "-p ≤ x«-q ⟷ -p ≤ -p*x«-q"
  by (metis leq_def pre_closed pre_import)

lemma pre_import_equiv_mult:
  "-p*-q ≤ x«-s ⟷ -p*-q ≤ -q*x«-s"
  by (smt leq_def pre_closed sub_assoc sub_mult_closed pre_import)

proposition pre_test_promote: "-p«-q = -p«-p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = --p⊔-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_distr_mult: "x«-p*-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=4] oops
proposition pre_distr_plus: "x«-p⊔-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=2] oops

end

class precondition_promote = precondition +
  assumes pre_test_promote: "-p«-q = -p«-p*-q"
begin

lemma pre_mult_test_promote:
  "x*-p«-q = x*-p«-p*-q"
  by (metis pre_seq pre_test_promote sub_mult_closed)

proposition pre_test_test: "-p*(-p«-q) = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = --p⊔-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_distr_mult: "x«-p*-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=4] oops
proposition pre_distr_plus: "x«-p⊔-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=2] oops

end

class precondition_test_box = precondition +
  assumes pre_test: "-p«-q = --p⊔-q"
begin

lemma pre_test_neg:
  "--p*(-p«-q) = --p"
  by (simp add: pre_test)

lemma pre_bot:
  "bot«-q = 1"
  by (metis pre_test tests_dual.sba_dual.one_def tests_dual.sba_dual.sup_left_zero tests_dual.top_double_complement)

lemma pre_export:
  "-p*x«-q = --p⊔(x«-q)"
  by (metis pre_closed pre_seq pre_test)

lemma pre_neg_mult:
  "--p ≤ -p*x«-q"
  by (metis leq_def pre_closed pre_seq pre_test_neg)

lemma pre_test_test_same:
  "-p«-p = 1"
  using pre_test tests_dual.sba_dual.less_eq_sup_top tests_dual.sba_dual.reflexive by auto

lemma test_below_pre_test_mult:
  "-q ≤ -p«-p*-q"
  by (metis pre_test tests_dual.sba_dual.reflexive tests_dual.sba_dual.shunting tests_dual.sub_sup_closed)

lemma test_below_pre_test:
  "-q ≤ -p«-q"
  by (simp add: pre_test tests_dual.sba_dual.upper_bound_right)

lemma test_below_pre_test_2:
  "--p ≤ -p«-q"
  by (simp add: pre_test tests_dual.sba_dual.upper_bound_left)

lemma pre_test_bot:
  "-p«bot = --p"
  by (metis pre_test tests_dual.sba_dual.sup_right_unit tests_dual.top_double_complement)

lemma pre_test_one:
  "-p«1 = 1"
  by (metis pre_seq pre_bot tests_dual.sup_right_zero)

subclass precondition_test_test
  apply unfold_locales
  by (simp add: pre_test tests_dual.sup_complement_intro)

subclass precondition_promote
  apply unfold_locales
  by (metis pre_test tests_dual.sba_dual.sub_commutative tests_dual.sub_sup_closed tests_dual.inf_complement_intro)

proposition pre_test: "-p«-q = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_distr_mult: "x«-p*-q = (x«-p)*(x«-q)" oops
proposition pre_distr_plus: "x«-p⊔-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=2] oops

end

class precondition_test_diamond = precondition +
  assumes pre_test: "-p«-q = -p*-q"
begin

lemma pre_test_neg:
  "--p*(-p«-q) = bot"
  by (simp add: pre_test tests_dual.sub_associative tests_dual.sub_commutative)

lemma pre_bot:
  "bot«-q = bot"
  by (metis pre_test tests_dual.sup_left_zero tests_dual.top_double_complement)

lemma pre_export:
  "-p*x«-q = -p*(x«-q)"
  by (metis pre_closed pre_seq pre_test)

lemma pre_neg_mult:
  "-p*x«-q ≤ -p"
  by (metis pre_closed pre_export tests_dual.upper_bound_left)

lemma pre_test_test_same:
  "-p«-p = -p"
  by (simp add: pre_test)

lemma test_above_pre_test_plus:
  "--p«-p⊔-q ≤ -q"
  using pre_test tests_dual.sba_dual.inf_complement_intro tests_dual.sub_commutative tests_dual.sub_inf_def tests_dual.upper_bound_left by auto

lemma test_above_pre_test:
  "-p«-q ≤ -q"
  by (simp add: pre_test tests_dual.upper_bound_right)

lemma test_above_pre_test_2:
  "-p«-q ≤ -p"
  by (simp add: pre_test tests_dual.upper_bound_left)

lemma pre_test_bot:
  "-p«bot = bot"
  by (metis pre_test tests_dual.sup_right_zero tests_dual.top_double_complement)

lemma pre_test_one:
  "-p«1 = -p"
  by (metis pre_test tests_dual.complement_top tests_dual.sup_right_unit)

subclass precondition_test_test
  apply unfold_locales
  by (simp add: pre_test tests_dual.sub_associative)

subclass precondition_promote
  apply unfold_locales
  by (metis pre_seq pre_test tests_dual.sup_idempotent)

proposition pre_test: "-p«-q = --p⊔-q" nitpick [expect=genuine,card=2] oops
proposition pre_distr_mult: "x«-p*-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=6] oops
proposition pre_distr_plus: "x«-p⊔-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=2] oops

end

class precondition_distr_mult = precondition +
  assumes pre_distr_mult: "x«-p*-q = (x«-p)*(x«-q)"
begin

proposition pre_test_test: "-p*(-p«-q) = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_test_promote: "-p«-q = -p«-p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = --p⊔-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_distr_plus: "x«-p⊔-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=2] oops

end

class precondition_distr_plus = precondition +
  assumes pre_distr_plus: "x«-p⊔-q = (x«-p)⊔(x«-q)"
begin

proposition pre_test_test: "-p*(-p«-q) = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_test_promote: "-p«-q = -p«-p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = --p⊔-q" nitpick [expect=genuine,card=2] oops
proposition pre_test: "-p«-q = -p*-q" nitpick [expect=genuine,card=2] oops
proposition pre_distr_mult: "x«-p*-q = (x«-p)*(x«-q)" nitpick [expect=genuine,card=4] oops

end

end