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

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"

lemma test_below_pre_test_2:
"--p ≤ -p«-q"

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

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"

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"

lemma test_above_pre_test_2:
"-p«-q ≤ -p"

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

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

```