section‹\label{sec_RefinementReactive}Monotonic Property Transformers›
theory RefinementReactive
imports Temporal Refinement
begin
text‹
In this section we introduce reactive systems which are modeled as
monotonic property transformers where properties are predicates on
traces. We start with introducing some examples that uses LTL to
specify global behaviour on traces, and later we introduce property
transformers based on symbolic transition systems.
›
definition "HAVOC = [:x ↝ y . True:]"
definition "ASSERT_LIVE = {. □ ♢ (ltl x . x).}"
definition "GUARANTY_LIVE = [: □ ♢ (ltl x y . y):]"
definition "AE = ASSERT_LIVE o HAVOC"
definition "SKIP = [:x ↝ y . x = y:]"
lemma [simp]: "SKIP = id"
by (auto simp add: fun_eq_iff SKIP_def demonic_def)
definition "REQ_RESP = [: □(λ xs ys . xs (0::nat) ⟶ (♢ (λ ys . ys (0::nat))) ys) :]"
definition "FAIL = ⊥"
lemma "HAVOC o ASSERT_LIVE = FAIL"
by (auto simp add: HAVOC_def AE_def FAIL_def ASSERT_LIVE_def fun_eq_iff assert_def demonic_def always_def at_fun_def le_fun_def eventually_def LTL_def)
lemma "HAVOC o AE = FAIL"
by (auto simp add: HAVOC_def AE_def FAIL_def ASSERT_LIVE_def fun_eq_iff assert_def demonic_def always_def at_fun_def le_fun_def eventually_def LTL_def)
lemma "HAVOC o ASSERT_LIVE = FAIL"
by (auto simp add: HAVOC_def AE_def FAIL_def ASSERT_LIVE_def fun_eq_iff assert_def demonic_def always_def at_fun_def eventually_def LTL_def)
lemma "SKIP o AE = AE"
by simp
lemma "(REQ_RESP o AE) = AE"
proof (auto simp add: fun_eq_iff HAVOC_def AE_def FAIL_def REQ_RESP_def ASSERT_LIVE_def assert_def
demonic_def always_def le_fun_def eventually_def at_fun_def LTL_def)
fix x :: "'a ⇒ bool"
fix xa :: "nat ⇒ bool"
fix xb :: nat
assume "∀xb::nat ⇒ bool . (∀x. xa x ⟶ Ex (xb[x ..])) ⟶ (∀x. ∃a. xb (x + a)) ∧ All x"
then have "(∀x. xa x ⟶ Ex (xa[x ..])) ⟶ (∀x. ∃a. xa (x + a)) ∧ All x"
by auto
then show "∃x. xa (xb + x)"
by (auto, rule_tac x = 0 in exI, simp)
next
fix x :: "'a ⇒ bool"
fix xa :: "nat ⇒ bool"
fix xb :: 'a
assume "∀xb::nat ⇒ bool . (∀x. xa x ⟶ Ex (xb[x ..])) ⟶ (∀x. ∃a. xb (x + a)) ∧ All x"
from this show "x xb"
by (metis at_trace_def le0)
next
fix x :: "'a ⇒ bool" and xa :: "nat ⇒ bool" and xb :: "nat ⇒ bool" and xc :: nat
assume A: "∀x. xa x ⟶ Ex (xb[x ..])"
assume B: "∀x. ∃xb. xa (x + xb)"
have "∃x1. xc ≤ AbsNat x1" by (metis (full_types) le_add2 plus_Nat_def)
thus "∃x. xb (xc + x)" using A B by (metis AbsNat_plus add.commute at_trace_def le_Suc_ex trans_le_add2)
qed
subsection‹Symbolic transition systems›
text‹
In this section we introduce property transformers basend on symbolic
transition systems. These are systems with local state. The execution
starts in some initial state, and with some input value the system computes
a new state and an output value. Then using the current state, and a
new input value the system computes a new state, and a new output, and
so on. The system may fail if at some point the input and the current
state do not statisfy a required predicate.
In the folowing definitions the variables $u$, $x$, $y$ stand for the
state of the system, the input, and the output respectively. The $init$
is the property that the initial state should satisfy. The predicate
$p$ is the precondition of the input and the current state, and the
relation $r$ gives the next state and the output based on the
input and the current state.
›
definition "illegal_sts init p r x = (∃ n u y . init (u 0) ∧ (∀ i < n . r (u i, x i) (u (Suc i), y i)) ∧ (¬ p (u n, x n)))"
definition "run_sts r u x y = (∀ i . r (u i, x i) (u (Suc i), y i))"
definition "LocalSystem init p r q x = (¬ illegal_sts init p r x ∧ (∀ u y . (init (u 0) ∧ run_sts r u x y) ⟶ q y))"
lemma LocalSystem_not_fail_run: "LocalSystem init p r = {.- illegal_sts init p r.} o [:x ↝ y . ∃ u . init (u 0) ∧ run_sts r u x y:]"
by (simp add: fun_eq_iff LocalSystem_def demonic_def assert_def le_fun_def, auto)
definition "fail_sys_delete init p r x = (∃ n u y . u ∈ init ∧ (∀ i < n . r (u i) (u (Suc i)) (x i) (y i)) ∧ (¬ p (u n) (u (Suc n)) (x n)))"
definition "run_delete r u x y = (∀ i . r (u i) (u (Suc i)) (x i) (y i))"
definition "LocalSystem_delete init p r q x = (¬ fail_sys_delete init p r x ∧ (∀ u y . (u ∈ init ∧ run_delete r u x y) ⟶ q y))"
lemma "fail (LocalSystem init p r) = illegal_sts init p r"
by (simp add: fun_eq_iff LocalSystem_def fail_def)
definition "lift_pre p = (λ (u, x) (u', y) . p (u (0::nat), x (0::nat)))"
definition "lift_rel r = (λ (u, x) (u', y) . r (u (0::nat), x (0::nat)) (u' 0, y (0::nat)))"
definition "prec_pre_sts init p r x = (∀ u y . init (u 0) ⟶ (lift_rel r leads lift_pre p) (u, x) (u[1..], y))"
definition "rel_pre_sts init r x y = (∃ u . init (u 0) ∧ (□ lift_rel r) (u, x) (u[1..], y))"
lemma prec_pre_sts_simp: "prec_pre_sts init p r x = (∀ u y . init (u 0) ⟶ (∀n . (∀ i < n . r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n)))"
apply (simp add: prec_pre_sts_def leads_def until_def lift_rel_def lift_pre_def at_fun_def at_prod_def, safe, blast)
by blast
lemma prec_stateless_sts_simp: "prec_pre_sts ⊤ (λ (s::unit, x) . inpt r x) (λ (s::unit, x) (s'::unit, y) . r x y :: bool)
= (□ (λ x . inpt r (x 0)))"
proof (simp add: fun_eq_iff prec_pre_sts_simp always_def inpt_def at_fun_def, safe)
fix x n
assume A: "∀y n. (∀i < n. r (x i) (y i)) ⟶ Ex (r (x (n::nat)))"
have "∃ y .(∀ i ≤ n . r (x i) (y i))"
proof (induction n)
case 0
then show ?case
using A apply (drule_tac x = "Eps ⊤" in spec, drule_tac x = 0 in spec, safe)
by (rule_tac x = "(λ i . xa)" in exI, simp)
next
case (Suc n)
from this obtain y where [simp]: "⋀ i . i ≤ n ⟹ r (x i) (y i)"
by blast
obtain y' where "r (x (Suc n)) y'"
apply (cut_tac A)
apply (drule_tac x = y in spec)
apply (drule_tac x = "Suc n" in spec)
by auto
show ?case
apply (rule_tac x = "λ i . if i ≤ n then y i else y'" in exI)
apply simp
using ‹r (x (Suc n)) y'› le_SucE by blast
qed
from this show " Ex (r (x n))"
by blast
next
fix x n
assume "∀f::nat. Ex (r (x f))"
from this show "Ex (r (x n))"
by blast
qed
lemma prec_pre_sts_top[simp]: "prec_pre_sts init ⊤ r = ⊤"
by (simp add: prec_pre_sts_simp fun_eq_iff)
lemma prec_pre_sts_bot[simp]: "init a ⟹ prec_pre_sts init ⊥ r = ⊥"
apply (simp add: prec_pre_sts_simp fun_eq_iff le_fun_def, safe)
apply (rule_tac x = "λ i . a" in exI, simp)
apply (rule_tac x = undefined in exI)
by (rule_tac x = 0 in exI, simp)
lemma rel_pre_sts_simp: "rel_pre_sts init r x y = (∃ u . init (u 0) ∧ (∀ i . r (u i, x i) (u (Suc i), y i)))"
by (simp add: rel_pre_sts_def always_def lift_rel_def at_fun_def at_prod_def)
lemma LocalSystem_simp: "LocalSystem init p r = {.prec_pre_sts init p r.} o [:rel_pre_sts init r:]"
proof -
have [simp]: "- illegal_sts init p r = prec_pre_sts init p r"
by (simp add: prec_pre_sts_simp fun_eq_iff illegal_sts_def, blast)
have [simp]: "(λ x y . ∃u. init (u 0) ∧ run_sts r u x y) = rel_pre_sts init r"
by (simp add: fun_eq_iff rel_pre_sts_simp run_sts_def)
show ?thesis
by (simp add: LocalSystem_not_fail_run)
qed
definition "local_init init S = INFIMUM init S"
definition "zip_set A B = {u . ((fst o u) ∈ A) ∧ ((snd o u) ∈ B)}"
definition nzip:: "('x ⇒ 'a) ⇒ ('x ⇒ 'b) ⇒ 'x ⇒ ('a×'b)" (infixl "||" 65) where "(xs || ys) i = (xs i, ys i)"
lemma nzip_def_abs: "(a || b) = (λi. (a i, b i))"
by (simp add: fun_eq_iff nzip_def)
lemma nzip_split: "(fst o u) || (snd o u) = u"
by (simp add: fun_eq_iff nzip_def)
lemma [simp]: "fst ∘ x || y = x"
by (simp add: fun_eq_iff nzip_def)
lemma [simp]: "snd ∘ x || y = y"
by (simp add: fun_eq_iff nzip_def)
lemma [simp]: "x ∈ A ⟹ y ∈ B ⟹ (x || y) ∈ zip_set A B"
by (simp add: zip_set_def)
lemma local_demonic_init: "local_init init (λ u . {. x . p u x.} o [:x ↝ y . r u x y :]) =
[:z ↝ u, x . u ∈ init ∧ z = x:] o {.u, x . p u x.} o [:u, x ↝ y . r u x y :]"
by (auto simp add: fun_eq_iff demonic_def assert_def local_init_def le_fun_def)
term "Sup ((λx. f) ` A)"
lemma local_init_comp: "u' ∈ init' ⟹ (∀ u. sconjunctive (S u)) ⟹ (local_init init S) o (local_init init' S')
= local_init (zip_set init init') (λ u . (S (fst o u)) o (S' (snd o u)))"
proof (subst fun_eq_iff, auto)
fix x :: 'f
assume A: "u' ∈ init'"
assume "∀ u . sconjunctive (S u)"
from this have [simp]: "⋀ u . sconjunctive (S u)" by simp
from A have [simp]: "⋀ y . S y (INF y' : init'. S' y' x) = (INF y' : init' . S y (S' y' x))"
by (simp add: sconjunctive_INF_simp INF_image)
have [simp]: "(INF y : init . (INF y' : init' . S y (S' y' x))) ≤ (INF u : zip_set init init'. S (fst ∘ u) (S' (snd ∘ u) x))"
proof (rule INF_greatest, auto simp add: zip_set_def)
fix u :: "'a ⇒ 'c × 'b"
assume [simp]: "fst ∘ u ∈ init"
assume [simp]: "snd ∘ u ∈ init'"
have "(INF y : init. INF y' : init'. S y (S' y' x)) ≤ (INF y' : init'. S (fst o u) (S' y' x))"
by (rule INF_lower, simp)
also have "... ≤ S (fst o u) (S' (snd o u) x)"
by (rule INF_lower, simp)
finally show "(INF y : init. INF y' : init'. S y (S' y' x)) ≤ S (fst o u) (S' (snd o u) x)"
by simp
qed
have [simp]: "(INF u : zip_set init init'. S (fst ∘ u) (S' (snd ∘ u) x)) ≤ (INF y : init . (INF y' : init' . S y (S' y' x)))"
proof (rule INF_greatest, rule INF_greatest)
fix y :: "'a ⇒ 'c" and y':: "'a ⇒ 'b"
assume [simp]: "y ∈ init"
assume [simp]: "y' ∈ init'"
have "(INF u : zip_set init init'. S (fst ∘ u) (S' (snd ∘ u) x)) ≤ S (fst o (y || y')) (S' (snd o (y || y')) x)"
by (rule INF_lower, simp)
also have "... ≤ S y (S' y' x)"
by simp
finally show "(INF (u::'a ⇒ 'c × 'b) : zip_set init init'. S (fst ∘ u) (S' (snd ∘ u) x)) ≤ S y (S' y' x)"
by simp
qed
have "local_init init S (local_init init' S' x) = (INF y : init. S y (INF y' : init'. S' y' x)) "
by (simp add: local_init_def INF_image)
also have "... = (INF y : init . (INF y' : init' . S y (S' y' x)))"
by (simp)
also have "... = (INF u : zip_set init init'. S (fst ∘ u) ∘ S' (snd ∘ u)) x"
by (rule antisym, auto simp add: INF_image)
also have "... = local_init (zip_set init init') (λ u . (S (fst o u)) o (S' (snd o u))) x"
by (simp add: local_init_def)
finally show "local_init init S (local_init init' S' x) = local_init (zip_set init init') (λu::'a ⇒ 'c × 'b. S (fst ∘ u) ∘ S' (snd ∘ u)) x"
by simp
qed
definition "rel_comp_sts r r' = (λ ((u,v),x) ((u',v'), z) . (∃ y . r (u,x) (u',y) ∧ r' (v,y) (v',z)))"
definition "prec_comp_sts p r p' = (λ ((u,v),x) . p (u,x) ∧ (∀ y u' . r (u, x) (u',y) ⟶ p' (v,y)))"
definition "sts_comp S S' = [-(u,v),x ↝ (u,x),v -] o (S ** Skip) o [-(u,y),v ↝ (v,y),u-] o (S' ** Skip) o [-(v,z),u ↝ (u,v),z-]"
lemma sts_comp_prec_rel: "sts_comp ({.p.} o [:r:]) ({.p'.} o [:r':]) = {.prec_comp_sts p r p'.} o [:rel_comp_sts r r':]"
apply (simp add: sts_comp_def Prod_spec_Skip update_def)
apply (simp add: comp_assoc [THEN sym] assert_demonic_comp demonic_demonic demonic_assert_comp)
apply (simp add: comp_assoc demonic_demonic)
apply (simp add: comp_assoc [THEN sym] assert_demonic_comp demonic_demonic demonic_assert_comp assert_assert_comp)
apply (simp add: comp_assoc demonic_demonic)
apply (rule prec_rel_eq)
by (simp_all add: fun_eq_iff prec_comp_sts_def rel_comp_sts_def OO_def)
text‹We show next that the composition of two SymSystem $S$ and $S'$ is not equal to the SymSystem of the
compostion of local transitions of $S$ and $S'$›
definition "initS u = True"
definition "precS = (λ (u, x) . True)"
definition "relS = (λ (u::nat, x::nat) (u'::nat, y::nat) . u = 0 ∧ u' = 1)"
definition "initS' v = True"
definition "precS' = (λ (u, x) . False)"
definition "relS' = (λ (v::nat, x) (v'::nat, y::nat) . True)"
definition "symbS = LocalSystem initS precS relS"
definition "symbS' = LocalSystem initS' precS' relS'"
definition "symbS'' = LocalSystem (prod_pred initS initS') (prec_comp_sts precS relS precS') (rel_comp_sts relS relS')"
lemma [simp]: "symbS = Magic"
proof (simp add: symbS_def LocalSystem_simp)
have [simp]: "prec_pre_sts initS precS relS = ⊤"
by (simp add: prec_pre_sts_simp fun_eq_iff precS_def)
have [simp]: "rel_pre_sts initS relS = ⊥"
apply (simp add: rel_pre_sts_simp fun_eq_iff relS_def initS_def, safe)
by (metis One_nat_def less_numeral_extra(1))
show " {. prec_pre_sts initS precS relS .} ∘ [: rel_pre_sts initS relS :] = Magic"
by (simp add: assert_true_skip Magic_def)
qed
lemma [simp]: "symbS''= Fail"
proof (simp add: symbS''_def LocalSystem_simp)
have A[simp]: "prod_pred initS initS' = ⊤"
by (simp add: prod_pred_def initS_def initS'_def fun_eq_iff)
have B[simp]: "prec_comp_sts precS relS precS' = (λ ((u, v), x). (0 < u))"
apply (simp add: prec_comp_sts_def)
by (simp add: prec_comp_sts_def precS'_def fun_eq_iff precS_def relS_def)
have [simp]: "prec_pre_sts (prod_pred initS initS') (prec_comp_sts precS relS precS') (rel_comp_sts relS relS') = ⊥"
apply (simp add: prec_pre_sts_simp fun_eq_iff)
apply (simp add: rel_comp_sts_def relS_def relS'_def, safe)
by (rule_tac x = "λ i . if i = 0 then (0,0) else (1,1)" in exI, simp)
show " {. prec_pre_sts (prod_pred initS initS') (prec_comp_sts precS relS precS') (rel_comp_sts relS relS') .}
∘ [: rel_pre_sts (prod_pred initS initS') (rel_comp_sts relS relS') :] = Fail"
by (simp add: assert_false_fail Fail_def del: A B)
qed
theorem "symbS o symbS' ≠ symbS''"
by simp
lemma rel_pre_sts_comp: "rel_pre_sts init r OO rel_pre_sts init' r' = rel_pre_sts (prod_pred init init') (rel_comp_sts r r')"
apply (simp add: rel_pre_sts_simp fun_eq_iff OO_def prod_pred_def rel_comp_sts_def, safe)
apply (rule_tac x = "u || ua" in exI)
apply (simp add: nzip_def, blast)
proof -
fix x xa u xb y
assume A: "∀i. (case u i of (u, v) ⇒ λx ((u', v'), z). ∃y. r (u, x) (u', y) ∧ r' (v, y) (v', z)) (x i) (u (Suc i), xa i) "
from A have "∀i. ∃y. r (fst (u i), x i) (fst (u (Suc i)), y) ∧ r' (snd (u i), y) (snd (u (Suc i)), xa i)"
apply safe
apply (drule_tac x = i in spec)
apply (case_tac "u i", simp)
by (case_tac "u (Suc i)", simp)
from this have "∃ y . ∀ i . r (fst (u i), x i) (fst (u (Suc i)), y i) ∧ r' (snd (u i), y i) (snd (u (Suc i)), xa i)"
by (simp add: choice_iff)
from this obtain yy where [simp]: "⋀ i . r (fst (u i), x i) (fst (u (Suc i)), yy i)" and [simp]: "⋀ i . r' (snd (u i), yy i) (snd (u (Suc i)), xa i)"
by blast
assume [simp]: "init xb"
assume [simp]: "init' y"
assume [simp]: "u 0 = (xb, y)"
show "∃ yy . (∃ua. init (ua 0) ∧ (∀i. r (ua i, x i) (ua (Suc i), yy i))) ∧ (∃ua. init' (ua 0) ∧ (∀i. r' (ua i, yy i) (ua (Suc i), xa i)))"
apply (rule_tac x = yy in exI, safe)
apply (rule_tac x = "fst o u" in exI, simp)
by (rule_tac x = "snd o u" in exI, simp)
qed
theorem LocalSystem_comp: "init' a ⟹ LocalSystem init p r o LocalSystem init' p' r' =
{.x.(∀u. init (u 0) ⟶ (∀y n. (∀i<n. r (u i, x i) (u (Suc i), y i)) ⟶ p (u n, x n))) ∧
(∀y. (∃u. init (u 0) ∧ (∀i. r (u i, x i) (u (Suc i), y i))) ⟶ (∀u. init' (u 0) ⟶ (∀ya n. (∀i<n. r' (u i, y i) (u (Suc i), ya i)) ⟶ p' (u n, y n)))).} ∘
[: rel_pre_sts init r OO rel_pre_sts init' r' :]"
apply (simp add: LocalSystem_simp comp_assoc [symmetric] assert_demonic_comp)
by (simp add: prec_pre_sts_simp rel_pre_sts_simp)
lemma sts_comp_prec_aux_a: "p' ≤ inpt r' ⟹
(⋀ v y n .v 0 = b ⟹ (∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), y i)) ⟹ prec_comp_sts p r p' ((u n, v n), x n)) ⟹
∀i < n. r (u i, x i) (u (Suc i), y i) ⟹ p (u n, x n) ∧ (∃ z v . v 0 = b ∧ (∀ i < n . r' (v i, y i) (v (Suc i), z i) ∧ p' (v i, y i)))"
proof (induction n)
case 0
assume A: "(⋀v y n. v 0 = b ⟹ ∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), y i) ⟹ prec_comp_sts p r p' ((u n, v n), x n))"
have "prec_comp_sts p r p' ((u 0, (λ i . b) 0), x 0)"
by (rule A, simp_all)
from this have [simp]: "p (u 0, x 0)"
by (simp add: prec_comp_sts_def)
show ?case
apply simp
by (rule_tac x = "λ i . b" in exI, simp)
next
case (Suc n)
thm Suc(1)
have "p (u n, x n) ∧ (∃z v. v 0 = b ∧ (∀i<n. r' (v i, y i) (v (Suc i), z i) ∧ p' (v i, y i)))"
apply (rule Suc(1))
apply (rule Suc(2))
apply (rule Suc(3), simp_all)
by (cut_tac Suc(4), simp)
from this obtain z v where "p (u n, x n)" and [simp]: "v 0 = b" and [simp]: "⋀ i . i < n ⟹ r' (v i, y i) (v (Suc i), z i)" and "⋀ i . i < n ⟹ p' (v i, y i)"
by blast
have "⋀ i . i < n ⟹ rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), z i)"
apply (simp add: rel_comp_sts_def)
apply (rule_tac x = "y i" in exI, simp)
by (cut_tac Suc(4), simp)
thm Suc(2)
from this have A: "(prec_comp_sts p r p' ((u (n), v (n)), x (n)))"
by (rule_tac Suc(3), auto)
from this have " p (u n, x n) ∧ p' (v n, y n)"
apply (simp add: prec_comp_sts_def)
apply safe
apply (drule_tac x = "y n" in spec, safe, simp)
by (cut_tac Suc(4), blast)
from this have "p' (v n, y n)"
by simp
from Suc(2) obtain b' a where [simp]: "r' (v n, y n) (b', a)"
using ‹p' (v n, y n)› by (simp add: le_fun_def inpt_def, blast)
define v' where "v' = (λ i . if i ≤ n then v i else b')"
define z' where "z' = (λ i . if i < n then z i else a)"
have [simp]: "v' 0 = b"
by(simp add: v'_def)
have A': "∀i < Suc n. rel_comp_sts r r' ((u i, v' i), x i) ((u (Suc i), v' (Suc i)), z' i)
⟹ prec_comp_sts p r p' ((u (Suc n), v' (Suc n)), x (Suc n))"
by (rule Suc(3), simp_all)
have "∀i < Suc n. rel_comp_sts r r' ((u i, v' i), x i) ((u (Suc i), v' (Suc i)), z' i) "
apply (simp add: rel_comp_sts_def)
apply safe
apply (rule_tac x = "y i" in exI)
apply safe
using Suc.prems(3) apply auto[1]
apply (simp add: v'_def z'_def)
by (case_tac "i = n", simp_all)
from this have "prec_comp_sts p r p' ((u (Suc n), v' (Suc n)), x (Suc n))"
by (rule A')
from this have [simp]: " p (u (Suc n), x (Suc n))"
by (simp add: prec_comp_sts_def)
have [simp]: "(∃z v. v 0 = b ∧ (∀i<Suc n. r' (v i, y i) (v (Suc i), z i) ∧ p' (v i, y i)))"
apply (rule_tac x = z' in exI)
apply (rule_tac x = v' in exI, simp)
apply (simp add: v'_def z'_def, safe)
apply (simp add: ‹⋀i. i < n ⟹ p' (v i, y i)›)
using ‹r' (v n, y n) (b', a)› less_antisym apply blast
using ‹p' (v n, y n)› less_antisym by blast
show ?case
by simp
qed
lemma sts_comp_prec_b: "p' ≤ inpt r' ⟹ init' b ⟹ prec_pre_sts (prod_pred init init') (prec_comp_sts p r p') (rel_comp_sts r r') x ⟹
(prec_pre_sts init p r x ∧ (∀y. rel_pre_sts init r x y ⟶ prec_pre_sts init' p' r' y))"
proof (simp add: prec_pre_sts_simp rel_pre_sts_simp, safe)
fix u
fix y n
assume [simp]: "init (u (0::nat))"
assume [simp]: "init' b"
assume A: "∀u. prod_pred init init' (u 0) ⟶ (∀y n. (∀i<n. rel_comp_sts r r' (u i, x i) (u (Suc i), y i)) ⟶ prec_comp_sts p r p' (u n, x n))"
from this have [simp]: "⋀ v y n .v 0 = b ⟹ (∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), y i)) ⟹ prec_comp_sts p r p' ((u n, v n), x n)"
apply (drule_tac x = "u || v" in spec)
by (simp add: nzip_def prod_pred_def)
assume [simp]: "∀i<n. r (u i, x i) (u (Suc i), y i)"
thm sts_comp_prec_aux_a
assume [simp]: "p' ≤ inpt r'"
from this have "p (u n, x n) ∧ (∃ z v . v 0 = b ∧ (∀ i < n . r' (v i, y i) (v (Suc i), z i) ∧ p' (v i, y i)))"
apply (cut_tac p = p and b = b and r = r and p' = p' and r' = r' and u = u and n = n and x = x in sts_comp_prec_aux_a)
by simp_all
from this show "p (u n, x n)"
by simp
next
fix v ya n y u
assume [simp]: "init' (v (0::nat))"
assume [simp]: "∀i<n. r' (v i, y i) (v (Suc i), ya i)"
assume [simp]: "∀i. r (u i, x i) (u (Suc i), y i)"
assume [simp]: "init (u (0::nat))"
assume A: "∀u. prod_pred init init' (u 0) ⟶ (∀y n. (∀i<n. rel_comp_sts r r' (u i, x i) (u (Suc i), y i)) ⟶ prec_comp_sts p r p' (u n, x n))"
from this have B: "(∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), ya i)) ⟹ prec_comp_sts p r p' ((u n, v n), x n)"
apply (drule_tac x = "u || v" in spec)
by (simp add: nzip_def prod_pred_def)
have [simp]: "(∀i<n. rel_comp_sts r r' ((u i, v i), x i) ((u (Suc i), v (Suc i)), ya i))"
apply (simp add: rel_comp_sts_def, safe)
by (rule_tac x = "y i" in exI, simp)
have C: "prec_comp_sts p r p' ((u n, v n), x n) ⟹ p' (v n, y n)"
apply (simp add: prec_comp_sts_def, safe)
apply (drule_tac x = "y n" in spec, safe, simp)
by (drule_tac x = "u (Suc n)" in spec, auto)
show " p' (v n, y n)"
by (rule C, rule B, simp)
qed
primrec u_y :: "('a × 'b ⇒ 'a × 'c ⇒ bool) ⇒ 'a ⇒ (nat ⇒ 'b) ⇒ nat ⇒ 'a ×'c" where
"u_y r a x 0 = (SOME (u,y) . r (a, x 0) (u, y))" |
"u_y r a x (Suc n) = (SOME (u, y) . r (fst (u_y r a x n), x (Suc n)) (u, y))"
definition "uu r a x i = (case i of 0 ⇒ a | Suc n ⇒ fst (u_y r a x n))"
definition "yy r a x = snd o (u_y r a x)"
lemma sts_exists_aux: "p ≤ inpt r ⟹ prec_pre_sts init p r x ⟹
init a ⟹ (∀ i ≤ n . r (uu r a x i, x i) (uu r a x (Suc i), yy r a x i))"
apply (simp add: prec_pre_sts_simp)
apply (induction n)
apply (simp add: uu_def yy_def inpt_def le_fun_def)
apply (rule someI_ex)
apply (drule_tac x = "λ i . a" in spec, simp)
apply simp
apply safe
apply (case_tac "i < Suc n")
apply (drule_tac x = i in spec)
apply simp
apply simp
apply (drule_tac x = "uu r a x" in spec, safe)
apply (simp add: uu_def)
apply (drule_tac x = "yy r a x" in spec)
proof -
fix n
assume "∀n. (∀i<n. r (uu r a x i, x i) (uu r a x (Suc i), yy r a x i)) ⟶ p (uu r a x n, x n)"
from this have A: "(∀i<Suc n. r (uu r a x i, x i) (uu r a x (Suc i), yy r a x i)) ⟶ p (uu r a x (Suc n), x (Suc n))"
by simp
assume "∀i≤n. r (uu r a x i, x i) (uu r a x (Suc i), yy r a x i)"
from this and A have B: "p (uu r a x (Suc n), x (Suc n))"
by auto
assume "p ≤ inpt r"
from this and B have "inpt r (uu r a x (Suc n), x (Suc n))"
by (simp add: le_fun_def)
from this obtain b z where "r (uu r a x (Suc n), x (Suc n)) (b, z)"
by (simp add: inpt_def, blast)
from this show "r (uu r a x (Suc n), x (Suc n)) (uu r a x (Suc (Suc n)), yy r a x (Suc n))"
apply (simp add: uu_def yy_def)
by (simp add: tfl_some)
qed
lemma sts_exists: "p ≤ inpt r ⟹ prec_pre_sts init p r x ⟹ init a ⟹ r (uu r a x n, x n) (uu r a x (Suc n), yy r a x n)"
by (drule_tac p = p and init = init and n = "Suc n" in sts_exists_aux, auto)
lemma sts_prec: "p ≤ inpt r ⟹ prec_pre_sts init p r x ⟹ init a ⟹ p (uu r a x n, x n)"
proof -
assume [simp]: "init a"
assume [simp]: "p ≤ inpt r"
assume [simp]: "prec_pre_sts init p r x"
from this have A: "⋀ u y n . init (u 0) ⟹ ∀i<n. r (u i, x i) (u (Suc i), y i) ⟹ p (u n, x n)"
by (simp add: prec_pre_sts_simp)
show "p (uu r a x n, x n)"
apply (rule A)
apply (simp add: uu_def)
apply safe
by (rule_tac p = p and init = init in sts_exists, simp_all)
qed
lemma sts_exists_prec: "p ≤ inpt r ⟹ prec_pre_sts init p r x ⟹ init a ⟹ p (uu r a x n, x n) ∧ r (uu r a x n, x n) (uu r a x (Suc n), yy r a x n)"
by (simp add: sts_exists sts_prec)
lemma sts_comp_prec_a: "p ≤ inpt r ⟹ prec_pre_sts init p r x ⟹ (⋀ y. rel_pre_sts init r x y ⟹ prec_pre_sts init' p' r' y)
⟹ prec_pre_sts (prod_pred init init') (prec_comp_sts p r p') (rel_comp_sts r r') x"
proof (subst prec_pre_sts_simp, safe)
fix u y n
assume Z: "p ≤ inpt r"
assume init: "prod_pred init init' (u (0::nat))"
define a where "a = fst o u"
define b where "b = snd o u"
have [simp]: "⋀i . u i = (a i, b i)"
by (simp add: a_def b_def)
thm choice_iff
assume A: "prec_pre_sts init p r x"
assume T: "(⋀ y. rel_pre_sts init r x y ⟹ prec_pre_sts init' p' r' y)"
assume "∀i<n. rel_comp_sts r r' (u i, x i) (u (Suc i), y i)"
from this obtain z where U: "⋀ i . i < n ⟹ r (a i, x i) (a (Suc i), z i)" and G: "⋀ i . i < n ⟹ r' (b i, z i) (b (Suc i), y i)"
by (simp add: rel_comp_sts_def choice_iff', blast)
from init have [simp]: "init (a 0)" and [simp]: "init' (b 0)"
by (simp_all add: prod_pred_def)
from A have H: "⋀ y n . (∀i<n. r (a i, x i) (a (Suc i), y i)) ⟹ p (a n, x n)"
by (simp add: prec_pre_sts_simp)
have [simp]: "p(a n, x n)"
apply (rule H)
using U by auto
show "prec_comp_sts p r p' (u n, x n)"
proof (simp add: prec_comp_sts_def, safe)
fix ya u'
assume [simp]: "r (a n, x n) (u', ya)"
define a' where "a' = (λ i . if i ≤ n then a i else u')"
define y' where "y' = (λ i . if i < n then z i else ya)"
define N where "N = Suc n"
have V: "⋀ i . i < N ⟹ r (a' i, x i) (a' (Suc i), y' i)"
apply (simp add: a'_def y'_def N_def, safe)
using U apply simp
using ‹r (a n, x n) (u', ya)› less_antisym by blast
have B: "prec_pre_sts (λ c . c = a' N) p r (x[N..])"
using A apply (simp add: prec_pre_sts_simp)
apply safe
apply (drule_tac x = "λ i . if i ≤ N then a' i else u (i - N)" in spec)
apply safe
apply simp_all
apply (simp add: a'_def)
apply (drule_tac x = "(λ i . if i < N then y' i else y (i - N))" in spec)
proof -
fix u y m
define na where "na = N + m"
assume [simp]: "u (0::nat) = a' N"
assume "∀na. (∀i<na. r (if i ≤ N then a' i else u (i - N), x i) (if Suc i ≤ N then a' (Suc i) else u (Suc i - N), if i < N then y' i else y (i - N))) ⟶
p (if na ≤ N then a' na else u (na - N), x na)"
from this have C: " (∀i<na. r (if i ≤ N then a' i else u (i - N), x i) (if Suc i ≤ N then a' (Suc i) else u (Suc i - N), if i < N then y' i else y (i - N))) ⟶
p (if na ≤ N then a' na else u (na - N), x na)"
by simp
assume B: " ∀i<m. r (u i, x (N + i)) (u (Suc i), y i)"
have [simp]: "(∀i<na. r (if i ≤ N then a' i else u (i - N), x i) (if Suc i ≤ N then a' (Suc i) else u (Suc i - N), if i < N then y' i else y (i - N)))"
apply safe
apply (case_tac "i ≤ N", simp_all add: na_def, safe)
using V apply auto [1]
apply (cut_tac B)
apply (drule_tac x = 0 in spec, simp)
apply (cut_tac B)
apply (drule_tac x = "i - N" in spec, auto)
by (simp add: Suc_diff_le)
from C have D: " p (if na ≤ N then a' na else u (na - N), x na)"
by simp
show "p (u m, x (N + m))"
using D apply (simp add: na_def)
apply (case_tac "m = 0", simp_all)
by (simp_all add: na_def)
qed
have S: "⋀ k . r (uu r (a' N) (x[N..]) k, (x[N..]) k) (uu r (a' N) (x[N..]) (Suc k), yy r (a' N) (x[N..]) k)"
apply (rule_tac p = p and r = r and init = "(λc. c = a' N)" in sts_exists)
apply (rule Z)
apply (rule B)
by simp
define u' where "u' = (λ i . if i ≤ N then a' i else uu r (a' N) (x[N..]) (i - N))"
define z' where "z' = (λ i . if i < N then y' i else yy r (a' N) (x[N..]) (i - N))"
have "rel_pre_sts init r x z'"
apply (simp add: rel_pre_sts_simp)
apply (rule_tac x = u' in exI)
apply (simp add: u'_def z'_def, safe)
apply (simp add: a'_def)
using S [of 0] apply (simp add: uu_def)
using V apply simp
apply (cut_tac k = "i - N" in S, auto)
by (subgoal_tac "Suc (i - N) = Suc i - N", simp_all)
from this T have "prec_pre_sts init' p' r' z'"
by simp
from this show "p' (b n, ya)"
apply (simp add: prec_pre_sts_simp)
apply (drule_tac x = b in spec, simp)
apply (drule_tac x = y in spec)
apply (drule_tac x = n in spec, safe)
apply (simp add: G z'_def N_def y'_def)
by (simp add: z'_def N_def y'_def)
qed
qed
lemma prec_pre_sts_comp: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init' b ⟹
(prec_pre_sts init p r x ∧ (∀y. rel_pre_sts init r x y ⟶ prec_pre_sts init' p' r' y))
= prec_pre_sts (prod_pred init init') (prec_comp_sts p r p') (rel_comp_sts r r') x"
apply safe
apply (simp_all add: sts_comp_prec_b)
by (rule sts_comp_prec_a, simp_all)
lemma sts_comp: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init' b ⟹
LocalSystem init p r o LocalSystem init' p' r' = LocalSystem (prod_pred init init') (prec_comp_sts p r p') (rel_comp_sts r r')"
apply (simp add: LocalSystem_simp)
by (simp add: comp_assoc [THEN sym] assert_demonic_comp rel_pre_sts_comp prec_pre_sts_comp)
subsection‹Parallel Composition of STSs›
definition "rel_prod_sts r r' = (λ ((u,v), (x, y)) ((u', v'), (x', y')) . r (u,x) (u',x') ∧ r' (v, y) (v', y'))"
definition "prec_prod_sts p p' = (λ ((u,v), (x, y)) . p (u,x) ∧ p' (v,y))"
lemma "(prec_prod_sts (inpt r) (inpt r')) ≤ inpt (rel_prod_sts r r')"
by (simp add: prec_prod_sts_def rel_prod_sts_def inpt_def le_fun_def)
lemma "(prec_prod_sts (inpt r) (inpt r')) = inpt (rel_prod_sts r r')"
by (simp add: prec_prod_sts_def rel_prod_sts_def inpt_def fun_eq_iff)
definition "distrib_state = [:(u,v), (x, y) ↝ (u', x'), (v', y'). u'=u ∧ v'=v ∧ x'=x ∧ y'=y:]"
definition "merge_state = [:(u, x), (v, y) ↝ (u', v'), (x', y'). u'=u ∧ v'=v ∧ x'=x ∧ y'=y:]"
lemma "distrib_state o merge_state = Skip"
apply (simp add: distrib_state_def merge_state_def demonic_demonic demonic_eq_skip[THEN sym])
apply (rule_tac f = demonic in arg_cong)
apply (simp add: fun_eq_iff OO_def)
by auto
lemma "merge_state o distrib_state = Skip"
apply (simp add: distrib_state_def merge_state_def demonic_demonic demonic_eq_skip[THEN sym])
apply (rule_tac f = demonic in arg_cong)
apply (simp add: fun_eq_iff OO_def)
by auto
definition "prod_sts S S' = (distrib_state o (S ** S') o merge_state)"
lemma prod_sts: "prod_sts ({.p.} o [:r:]) ({.p'.}o[:r':]) = {.prec_prod_sts p p'.} o [:rel_prod_sts r r':]"
apply (simp add: prod_sts_def Prod_spec merge_state_def distrib_state_def)
apply (simp add: comp_assoc [THEN sym] demonic_assert_comp)
apply (simp add: comp_assoc demonic_demonic)
apply (rule prec_rel_eq)
apply (simp add: fun_eq_iff prec_prod_sts_def)
by (simp add: fun_eq_iff rel_prod_sts_def OO_def)
lemma update_demonic_update: "[-f-] o [:r:] o [-g-] = [:x ↝ y . ∃ z . r (f x) z ∧ y = g z:]"
by (simp add: demonic_def fun_eq_iff update_def le_fun_def, auto)
lemma sts_prod_prec: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init a ⟹ init' b ⟹
prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') (x || y)
= (prec_pre_sts init p r x ∧ prec_pre_sts init' p' r' y)"
proof (safe)
assume initA[simp]: "init a"
assume initB[simp]: "init' b"
assume "p' ≤ inpt r'" and "p ≤ inpt r"
from this have [simp]: "prec_prod_sts p p' ≤ inpt (rel_prod_sts r r')"
by (simp add: prec_prod_sts_def le_fun_def rel_prod_sts_def inpt_def)
assume A: "prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') (x || y)"
from this have C: "⋀ n . prec_prod_sts p p' (uu (rel_prod_sts r r') (a,b) (x || y) n, (x || y) n) ∧ rel_prod_sts r r' (uu (rel_prod_sts r r') (a,b) (x || y) n, (x || y) n)
(uu (rel_prod_sts r r') (a, b) (x || y) (Suc n), yy (rel_prod_sts r r') (a, b) (x || y) n)"
apply (cut_tac r = "(rel_prod_sts r r')" and p = "prec_prod_sts p p'" and init = "prod_pred init init'"
and a = "(a,b)" and x = "x || y" and n = n in sts_exists_prec)
apply simp_all
by (simp add: prod_pred_def)
obtain u' v' where U[simp]: "uu (rel_prod_sts r r') (a,b) (x || y) = u' || v'"
using nzip_split [symmetric] by auto
obtain s' t' where [simp]: "yy (rel_prod_sts r r') (a,b) (x || y) = s' || t'"
using nzip_split [symmetric] by auto
have [simp]: "init (u' 0)"
by (cut_tac U, simp add: fun_eq_iff del: U, drule_tac x= 0 in spec,
cut_tac initA, simp add: uu_def nzip_def del: U initA)
have [simp]: "init' (v' 0)"
by (cut_tac U, simp add: fun_eq_iff del: U, drule_tac x= 0 in spec, cut_tac initB,
simp add: uu_def nzip_def del: U initB)
from C have [simp]: "⋀ n . r (u' n, x n) (u' (Suc n), s' n)" and [simp]: "⋀ n . r' (v' n, y n) (v' (Suc n), t' n)"
by (simp_all, simp_all add: rel_prod_sts_def nzip_def)
from A have B: "⋀ u v s t n . init (u 0) ⟹ init' (v 0) ⟹ ∀i < n. r (u i, x i) (u (Suc i), s i) ⟹ ∀i<n. r' (v i, y i) (v (Suc i), t i) ⟹ p (u n, x n) ∧ p' (v n, y n)"
apply (simp add: prec_pre_sts_simp)
apply (drule_tac x = "u || v" in spec)
apply (simp add: prod_pred_def nzip_def)
apply (drule_tac x = "s || t" in spec)
by (simp add: prec_prod_sts_def rel_prod_sts_def nzip_def)
show "prec_pre_sts init p r x"
apply (simp add: prec_pre_sts_simp, safe)
by (cut_tac n = n and u = u and v = v' and s = y and t = t' in B, simp_all)
show "prec_pre_sts init' p' r' y"
apply (simp add: prec_pre_sts_simp, safe)
by (cut_tac n = n and u = u' and v = u and s = s' and t = ya in B, simp_all)
next
assume U: "prec_pre_sts init p r x"
assume V: "prec_pre_sts init' p' r' y"
show "prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') (x || y)"
proof (simp add: prec_pre_sts_simp prod_pred_def rel_prod_sts_def prec_prod_sts_def nzip_def, clarify)
fix u xa ya yaa n ua v
assume A: "∀i<n. (case u i of (u, v) ⇒ λ(x, y) ((u', v'), x', y'). r (u, x) (u', x') ∧ r' (v, y) (v', y')) (x i, y i) (u (Suc i), yaa i)"
define a where "a = fst o u"
define b where "b = snd o u"
define s where "s = fst o yaa"
define t where "t = snd o yaa"
assume "u 0 = (xa, ya) "
assume "init xa"
assume "init' ya"
assume "(ua, v) = u n"
have [simp]: "init (a 0)"
by (simp add: ‹init xa› ‹u 0 = (xa, ya)› a_def)
have [simp]: "init' (b 0)"
by (simp add: ‹b ≡ snd ∘ u› ‹init' ya› ‹u 0 = (xa, ya)›)
have [simp]: "⋀ i . i < n ⟹ r (a i, x i) (a (Suc i), s i)" and [simp]: "⋀ i . i < n ⟹ r' (b i, y i) (b (Suc i), t i)"
using A apply (drule_tac x = i in spec)
apply (case_tac "u i", case_tac "yaa i", case_tac "u (Suc i)", simp add: a_def s_def)
using A apply (drule_tac x = i in spec)
by (case_tac "u i", case_tac "yaa i", case_tac "u (Suc i)", simp add: b_def t_def)
from U have [simp]: "p (a n, x n)"
apply (simp add: prec_pre_sts_simp)
apply (drule_tac x = a in spec, simp)
by (drule_tac x = s in spec, simp)
from V have [simp]: "p' (b n, y n)"
apply (simp add: prec_pre_sts_simp)
apply (drule_tac x = b in spec, simp)
by (drule_tac x = t in spec, simp)
have [simp]: "ua = a n"
by (metis ‹(ua, v) = u n› ‹a ≡ fst ∘ u› comp_def fst_conv)
have [simp]: "v = b n"
by (metis ‹(ua, v) = u n› b_def comp_apply snd_conv)
show "p (ua, x n) ∧ p' (v, y n)"
by simp
qed
qed
lemma sts_prod_rel: "(λ x y . ∃z. rel_pre_sts (prod_pred init init') (rel_prod_sts r r') (case x of (x, xa) ⇒ x || xa) z ∧ y = (fst ∘ z, snd ∘ z))
= (λ (x, y) (u, v) . rel_pre_sts init r x u ∧ rel_pre_sts init' r' y v)"
apply (subst fun_eq_iff)
apply (subst fun_eq_iff)
apply(simp add: rel_pre_sts_simp nzip_def prod_pred_def rel_prod_sts_def, safe)
apply (rule_tac x = "fst o u" in exI)
apply clarsimp
apply (drule_tac x = i in spec)
apply (case_tac "u i", simp)
apply (case_tac "u (Suc i)", simp)
apply (case_tac "z i", simp)
apply (rule_tac x = "snd o u" in exI)
apply clarsimp
apply (drule_tac x = i in spec)
apply (case_tac "u i", simp)
apply (case_tac "u (Suc i)", simp)
apply (case_tac "z i", simp)
apply (rule_tac x = "aa || ba" in exI, safe)
apply (rule_tac x = "u || ua" in exI, safe)
by (simp_all add: nzip_def)
theorem sts_prod: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ init a ⟹ init' b ⟹
LocalSystem init p r ** LocalSystem init' p' r' =
[-x, x' ↝ x || x'-] o LocalSystem (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') o [-y ↝ fst o y, snd o y-]"
proof -
assume [simp]: "p ≤ inpt r"
assume [simp]: "p' ≤ inpt r'"
assume [simp]: "init a"
assume [simp]: "init' b"
thm sts_prod_prec
have [simp]: "prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') ∘ (λ(x, y). x || y)
= (λ (x, y) . prec_pre_sts init p r x ∧ prec_pre_sts init' p' r' y)"
apply (simp add: fun_eq_iff)
by (subst sts_prod_prec [of _ _ _ _ _ a _ b], simp_all)
have "[-x, x' ↝ x || x'-] o LocalSystem (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') o [-y ↝ fst o y, snd o y-] =
[- (x, y) ↝ x || y -] ∘ {. prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') .}
∘ [: rel_pre_sts (prod_pred init init') (rel_prod_sts r r') :] ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]"
by (simp add: LocalSystem_simp comp_assoc [symmetric])
also have "... = {. prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') ∘ (λ(x, y). x || y) .} ∘ [- (x, y) ↝ x || y -] ∘
[: rel_pre_sts (prod_pred init init') (rel_prod_sts r r') :] ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]"
by (simp add: update_assert_comp)
also have "... = {. prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') ∘ (λ(x, y). x || y) .} ∘ ([- (x, y) ↝ x || y -] ∘
[: rel_pre_sts (prod_pred init init') (rel_prod_sts r r') :] ∘ [- y ↝ (fst ∘ y, snd ∘ y) -])"
by (simp add: comp_assoc)
also have "... = {. prec_pre_sts (prod_pred init init') (prec_prod_sts p p') (rel_prod_sts r r') ∘ (λ(x, y). x || y) .} ∘
[:x↝y.∃z. rel_pre_sts (prod_pred init init') (rel_prod_sts r r') (case x of (x, xa) ⇒ x || xa) z ∧ y = (fst ∘ z, snd ∘ z):]"
by (simp add: update_demonic_update)
also have "... = {.(x, y).prec_pre_sts init p r x ∧ prec_pre_sts init' p' r' y.} ∘ [:(x, y)↝(u, v).rel_pre_sts init r x u ∧ rel_pre_sts init' r' y v:]"
by (simp add: sts_prod_rel)
also have "... = LocalSystem init p r ** LocalSystem init' p' r'"
by (simp add: LocalSystem_simp Prod_spec)
finally show ?thesis
by simp
qed
subsection‹Example: COUNTER›
text‹
In this section we introduce an example counter that counts how many times
the input variable $x$ is true. The input is a sequence of boolen values
and the output is a sequence of natural numbers. The output at some moment in
time is the number of true values seen so far in the input.
We defined the system counter in two different ways and we show that the
two definitions are equivalent. The first definition takes the entire
input sequence and it computes the corresponding output sequence. We introduce
the second version of the counter as a reactive system based on a symbolic
transition system. We use a local variable to record the number of true
values seen so far, and initially the local variable is zero. At every step
we increase the local variable if the input is true. The output of the
system at every step is equal to the local variable.
›
primrec count :: "bool trace ⇒ nat trace" where
"count x 0 = (if x 0 then 1 else 0)" |
"count x (Suc n) = (if x (Suc n) then count x n + 1 else count x n)"
definition "Counter_global n = {.x . (∀ k . count x k ≤ n).} o [:x ↝ y . y = count x:]"
definition "prec_count M = (λ (u, x) . u ≤ M)"
definition "rel_count = (λ (u,x) (u', y) . (x ⟶ u' = Suc u) ∧ (¬ x ⟶ u' = u) ∧ y = u')"
lemma counter_a_aux: "u 0 = 0 ⟹ ∀i < n. (x i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ x i ⟶ u (Suc i) = u i) ⟹ (∀ i < n . count x i = u (Suc i))"
proof (induction n)
case 0
show ?case by simp
next
case (Suc n)
{fix j::nat
assume "∀i<Suc n. (x i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ x i ⟶ u (Suc i) = u i)"
and "j < Suc n"
and "u (0::nat) = (0::nat)"
from this and Suc have "count x j = u (Suc j)"
by (case_tac j, auto)
}
from Suc and this show ?case
by auto
qed
lemma counter_b_aux: "u 0 = 0 ⟹ ∀n. (xa n ⟶ u (Suc n) = Suc (u n)) ∧ (¬ xa n ⟶ u (Suc n) = u n) ∧ xb n = u (Suc n)
⟹ count xa n = u (Suc n)"
by (induction n, simp_all)
definition "COUNTER M = LocalSystem (λ a . a = 0) (prec_count M) rel_count"
lemma "COUNTER = Counter_global"
proof -
have A:"rel_pre_sts (λ a . a = 0) rel_count = (λ x y . y = count x)"
proof (simp add: rel_pre_sts_simp rel_count_def fun_eq_iff, safe)
fix x :: "nat ⇒ bool" and xa :: "nat ⇒ nat" and u:: "nat ⇒ nat" and xb :: nat
assume A: "u 0 = 0"
assume B: "∀xb . (x xb ⟶ u (Suc xb) = Suc (u xb)) ∧ (¬ x xb ⟶ u (Suc xb) = u xb) ∧ xa xb = u (Suc xb)"
from A and this have "count x xb = xa xb"
by (drule_tac counter_b_aux, auto)
then show "xa xb = count x xb" by simp
next
fix x::"nat ⇒ bool" and xa::"nat ⇒ nat"
define u where A: "u == (λ i . if i = 0 then 0 else count x (i - 1))"
assume B: "∀xb::nat. xa xb = count x xb"
{fix xb::nat
from A and B have "u 0 = 0 ∧ ( (x xb ⟶ u (Suc xb) = Suc (u xb)) ∧ (¬ x xb ⟶ u (Suc xb) = u xb) ∧ xa xb = u (Suc xb))"
by (case_tac xb, auto)
}
then show "∃u::nat ⇒ nat. u 0 = 0 ∧ (∀xb. (x xb ⟶ u (Suc xb) = Suc (u xb)) ∧ (¬ x xb ⟶ u (Suc xb) = u xb) ∧
xa xb = u (Suc xb))"
by auto
qed
{fix x :: nat
have "(prec_pre_sts (λ a . a = 0) (prec_count x) rel_count) = (λxa::nat ⇒ bool. ∀k::nat. count xa k ≤ x)"
proof (simp add: fun_eq_iff prec_pre_sts_simp prec_count_def at_fun_def rel_count_def, safe)
fix xa::"nat ⇒ bool" and k:: nat
define uu where A: "uu == (λ i . if i = 0 then 0 else count xa (i - 1))"
assume "∀u. u 0 = 0 ⟶ (∀y n. (∀i<n. (xa i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ xa i ⟶ u (Suc i) = u i) ∧ y i = u (Suc i)) ⟶ u n ≤ x) " (is "∀ u . ?p u ⟶ ?s u")
then have "?p uu ⟶ ?s uu"
by blast
from this and A have "?s uu"
by simp
then have "∀ n. (∀i<n. (xa i ⟶ uu (Suc i) = Suc (uu i)) ∧ (¬ xa i ⟶ uu (Suc i) = uu i)) ⟶ uu n ≤ x"
apply auto
by (drule_tac x = "λ i . uu (Suc i)" in spec, simp)
from this have "(∀i < (Suc k). (xa i ⟶ uu (Suc i) = Suc (uu i)) ∧ (¬ xa i ⟶ uu (Suc i) = uu i)) ⟶ uu (Suc k)≤ x"
by simp
from this and A show "count xa k ≤ x"
apply (auto)
apply (metis (no_types, lifting) Suc_eq_plus1_left Suc_pred add.commute count.simps(2))
using not_gr_zero apply fastforce
apply (metis (no_types, lifting) Suc_eq_plus1_left Suc_pred add.commute count.simps(2))
using not_gr_zero apply fastforce
apply (metis Suc_pred count.simps(2))
by (metis Suc_pred count.simps(2))
next
fix xa:: "nat ⇒ bool" and u::"nat ⇒ nat" and n::nat
fix y
assume C: "∀k::nat. count xa k ≤ x"
assume A: "u (0::nat) = (0::nat)"
assume B: "∀i<n. (xa i ⟶ u (Suc i) = Suc (u i)) ∧ (¬ xa i ⟶ u (Suc i) = u i) ∧ y i = u (Suc i)"
have D: "∀i < n. count xa i = u (Suc i)"
apply (rule counter_a_aux)
apply (simp add: A)
by (simp add: B)
show "u n ≤ x"
apply (case_tac n, simp add: A)
apply simp
apply (cut_tac D)
apply (drule_tac x = nat in spec, simp)
apply (cut_tac C)
by (drule_tac x = "nat" in spec, simp)
qed
}
note B = this
show ?thesis
by (simp add: fun_eq_iff COUNTER_def LocalSystem_simp Counter_global_def A B)
qed
subsection‹Example: LIVE›
text‹
The last example of this formalization introduces a system which does some
local computation, and ensures some global liveness property.
We show that this example is the fusion of a symbolic transition system and a demonic
choice which ensures the liveness property of the output sequence.
We also show that asumming some liveness property for the input, we can refine
the example into an executable system that does not ensure the liveness
property of the output on its own, but relies on the liveness of the input.
›
definition "rel_ex = (λ (u, x) (u', y) . ((x ∧ u' = u + (1::int)) ∨ (¬ x ∧ u' = u - 1) ∨ u' = 0) ∧ (y = (u' = 0)))"
definition "prec_ex = (λ (u, x) . -1 ≤ u ∧ u ≤ 3)"
definition "LIVE = {. prec_pre_sts (λ a . a = 0) prec_ex rel_ex.}
o [:x ↝ y . ∃ u . u (0::nat) = 0 ∧ (□(λ u x y . rel_ex (u (0::nat), x (0::nat)) (u 1, y (0::nat)))) u x y ∧ (□ (♢ (λ y . y 0))) y :]"
thm fusion_spec_local_a
lemma LIVE_fusion: "LIVE = (LocalSystem (λ a . a = 0) prec_ex rel_ex) ∥ [:x ↝ y . (□ (♢ (λ y . y 0))) y:]"
proof-
have [simp]: "⋀ x y . rel_pre_sts (λa. a = 0) rel_ex x y = ( ∃u. u 0 = 0 ∧ (□ (λu x y. rel_ex (u 0, x 0) (u (Suc 0), y 0))) u x y)"
by (simp add: rel_pre_sts_simp always_def at_fun_def)
have [simp]: "rel_pre_sts (λa. a = 0) rel_ex ⊓ (λx. □ ♢ (λy. y 0)) = (λ x y . ∃u. u 0 = 0 ∧ (□ (λu x y. rel_ex (u 0, x 0) (u (Suc 0), y 0))) u x y ∧ (□ ♢ (λy. y 0)) y)"
by (simp add: fun_eq_iff, blast)
show "LIVE = (LocalSystem (λ a . a = 0) prec_ex rel_ex) ∥ [:x ↝ y . (□ (♢ (λ y . y 0))) y:]"
apply (simp add: LocalSystem_simp)
apply (auto simp add: LIVE_def fusion_spec_local_a at_fun_def)
apply (cut_tac p = "prec_pre_sts (λa. a = 0) prec_ex rel_ex" and p' = ⊤
and r = "rel_pre_sts (λa. a = 0) rel_ex" and r' = "λx. □ ♢ (λy. y 0)" in fusion_spec)
by (simp add: assert_true_skip)
qed
definition "preca_ex x = (x 1 = (¬x (0::nat)))"
lemma monotonic_SymSystem[simp]: "mono (LocalSystem init p r)"
by (simp add: LocalSystem_simp)
lemma event_ex_aux_a: "a 0 = (0::int) ⟹ ∀n. xa (Suc n) = (¬ xa n) ⟹
∀n. (xa n ∧ a (Suc n) = a n + 1 ∨ ¬ xa n ∧ a (Suc n) = a n - 1 ∨ a (Suc n) = 0) ⟹
(a n = -1 ⟶ xa n) ∧ (a n = 1 ⟶ ¬ xa n) ∧ -1 ≤ a n ∧ a n ≤ 1"
proof (induction n)
case 0
show ?case
by (metis "0.prems"(1) le_minus_one_simps(1) minus_zero zero_le_one zero_neq_neg_one)
next
case (Suc n)
{assume "a (Suc n) = - (1::int)" from this and Suc have "xa (Suc n)"
by (metis add.commute add_le_same_cancel2 not_one_le_zero zero_neq_neg_one)}
note A = this
{assume "a (Suc n) = (1::int)" and "xa (Suc n)" from this and Suc have "False"
by (metis eq_iff le_iff_diff_le_0 not_one_le_zero)}
note B = this
{assume "a n ≠ - (1::int)" from this and Suc have " - (1::int) ≤ a (Suc n)"
proof -
have f1: "∀x0. a x0 - 1 = - 1 + a x0"
by simp
have f2: "∀x0. a x0 + 1 = 1 + a x0"
by auto
have "∀n. (xa n ∧ a (Suc n) = 1 + a n ∨ ¬ xa n ∧ a (Suc n) = - 1 + a n ∨ a (Suc n) = 0) = (xa n ∧ a (Suc n) + - 1 * a n = 1 ∨ ¬ xa n ∧ a (Suc n) + - 1 * a n = - 1 ∨ a (Suc n) = 0)"
by force
hence f3: "(∀n. xa n ∧ a (Suc n) = a n + 1 ∨ ¬ xa n ∧ a (Suc n) = a n - 1 ∨ a (Suc n) = 0) = (∀n. xa n ∧ a (Suc n) + - 1 * a n = 1 ∨ ¬ xa n ∧ a (Suc n) + - 1 * a n = - 1 ∨ a (Suc n) = 0)"
using f2 f1 by presburger
have "a (Suc n) + - 1 * a n = 1 ∨ a (Suc n) + - 1 * a n = - 1 ∨ (¬ xa n ∨ a (Suc n) + - 1 * a n ≠ 1) ∧ (xa n ∨ a (Suc n) + - 1 * a n ≠ - 1)"
by meson
thus ?thesis
using f3 Suc.IH `∀n. xa (Suc n) = (¬ xa n)` `∀n. xa n ∧ a (Suc n) = a n + 1 ∨ ¬ xa n ∧ a (Suc n) = a n - 1 ∨ a (Suc n) = 0` `a 0 = 0` `a n ≠ - 1` by auto
qed
}
note C = this
{assume "a n = - (1::int)" from this and Suc have " - (1::int) ≤ a (Suc n)"
by (metis add.commute le_minus_one_simps(4) monoid_add_class.add.right_neutral not_le right_minus zle_add1_eq_le)}
note D = this
from C and D and Suc have E: " - (1::int) ≤ a (Suc n)" by auto
from Suc have F: "a (Suc n) ≤ (1::int)"
by (metis eq_iff int_one_le_iff_zero_less le_iff_diff_le_0 le_less not_le zle_add1_eq_le)
from A B E F show ?case by auto
qed
lemma event_ex_aux: "a 0 = (0::int) ⟹ ∀n. xa (Suc n) = (¬ xa n) ⟹
∀n. (xa n ∧ a (Suc n) = a n + 1 ∨ ¬ xa n ∧ a (Suc n) = a n - 1 ∨ a (Suc n) = 0) ⟹
(∀ n . (a n = -1 ⟶ xa n) ∧ (a n = 1 ⟶ ¬ xa n) ∧ -1 ≤ a n ∧ a n ≤ 1)"
by (clarify, drule event_ex_aux_a, auto)
thm fusion_local_refinement
lemma "{.□ preca_ex.} o LIVE ≤ LocalSystem (λ a . a = (0::int)) prec_ex rel_ex"
proof (unfold LIVE_def LocalSystem_simp comp_assoc [symmetric] assert_assert_comp)
show " {. □ preca_ex ⊓ prec_pre_sts (λa. a = 0) prec_ex rel_ex .}
∘ [:x↝y.∃u. u (0::nat) = 0 ∧ (□ (λu x y. rel_ex (u 0, x 0) (u 1, y 0))) u x y ∧ (□ ♢ (λy. y 0)) y:]
≤ {. prec_pre_sts (λa. a = 0) prec_ex rel_ex .} ∘ [: rel_pre_sts (λa. a = (0::int)) rel_ex :]"
proof (unfold assert_demonic_refinement, safe)
fix x xa
assume "(□ preca_ex) x"
then have B: "∀i::nat. x (Suc i) = (¬ x i)"
by (auto simp add: preca_ex_def always_def at_fun_def)
assume "prec_pre_sts (λa. a = 0) prec_ex rel_ex x"
assume "rel_pre_sts (λa. a = 0) rel_ex x xa"
from this obtain u where [simp]: "u 0 = 0" and [simp]: "⋀ i . rel_ex (u i, x i) (u (Suc i), xa i)"
by (simp add: rel_pre_sts_simp, blast)
then have C: "∀i . (x i ∧ u (Suc i) = u i + 1 ∨ ¬ x i ∧ u (Suc i) = u i - 1 ∨ u (Suc i) = 0) ∧ xa i = (u (Suc i) = 0)"
by (simp add: rel_ex_def)
have D: "(∀ n . (u n = -1 ⟶ x n) ∧ (u n = 1 ⟶ ¬ x n) ∧ -1 ≤ u n ∧ u n ≤ 1)"
by (cut_tac B C, rule event_ex_aux, auto)
have [simp]: "(□ (λu x y. rel_ex (u 0, x 0) (u (Suc 0), y 0))) u x xa "
by (simp add: always_def at_fun_def)
thm rel_ex_def
thm preca_ex_def
{
fix a::nat
{assume "u (Suc a) = 0" from this B C have "∃b . u (Suc (a + b)) = 0"
by (metis monoid_add_class.add.right_neutral)}
note 1 = this
{assume "u (Suc a) = -1" from this B C D have "∃b . u (Suc (a + b)) = 0"
by (metis add_Suc_right diff_minus_eq_add diff_self monoid_add_class.add.right_neutral)}
note 2 = this
{assume "u (Suc a) = 1" from this B C D have "∃b . u (Suc (a + b)) = 0"
by (metis add_Suc_right diff_self monoid_add_class.add.right_neutral)}
note 3 = this
from 1 2 3 B C D have X: "∃b . xa (a + b)"
by (simp, metis diff_0 int_one_le_iff_zero_less le_less not_le zle_diff1_eq)
}
then have [simp]: "(□ ♢ (λy. y 0)) xa"
by (simp add: always_def eventually_def preca_ex_def at_fun_def)
show "∃u. u (0::nat) = 0 ∧ (□ (λu x y. rel_ex (u 0, x 0) (u 1, y 0))) u x xa ∧ (□ ♢ (λy. y 0)) xa"
by (rule_tac x = u in exI, simp)
qed
qed
end