section{*\label{sec_Overview}Overview of the Refinement Calculus of Reactive Systems (RCRS) *}
theory RCRS_Overview imports "Feedback/ReactiveFeedback" Complex_Main
begin
text{*This theory file refers to the results presented in the paper "The Refinement Calculus of Reactive Systems",
by Preoteasa, Dragomir, and Tripakis, on arxiv.org, 2017, and under submission to a journal.*}
text{*The section, subsection, etc., numbers and titles below refer to those in the aforementioned paper.*}
subsection{*Section 3: Language*}
subsubsection{*Section 3.1: An Algebra of Components*}
text{*The grammar of components defined in Section 3.1 is not explicitly formalized in this theory.
However, GEN\_STS, STATELESS\_STS, DET\_STS, DET\_STATELESS\_STS, and QLTL components can be defined as
semantic objects as they are given in Section 4.3*}
subsubsection{*Section 3.2: Symbolic Transition System Components*}
subsubsection{*Section 3.2.1: General STS Components*}
text{*The semantics version of an STS component is given by the next definition which matches equation (6) from the paper.
Another difference between the semantic sts defined here and the syntactic version from the paper is that init
and r are functions in the semantic version.*}
definition "sts init r = {. -illegal_sts init (inpt r) r .} o [: x ↝ y . ∃ s . (init (s 0) ∧ run_sts r s x y) :]"
definition "C1_sts = sts (λ s . s > 0) (λ (s,(n,x)) (s', y) . s' > s ∧ y + s = x ^ n)"
definition "C2_sts = sts (λ s . s > 0) (λ (s,z) (s', y) . s'> s ∧ y + s = (snd z) ^ (fst z))"
lemma "C1_sts = C2_sts"
by (simp add: C1_sts_def C2_sts_def split_def)
definition "UnitDelay = sts (λ s . s = 0) (λ (s,x) (s',y) . y = s ∧ s' = x)"
definition "Sum_sts = sts (λ s . s = (0::nat)) (λ (s,x) (s',y) . y = s ∧ s' = s + x)"
definition "C_sts = sts (λ s . s = 0) (λ (s, x) (s', y) . x + s ≤ y )"
definition "Div_sts = sts ⊤ (λ (s::unit,(x,y)) (s'::unit, z) . y ≠ 0 ∧ z = x / y)"
definition "Integrator dt = sts (λ s . s = 0) (λ (s,x) (s',y) . y = s ∧ s' = s + x * dt)"
definition "TransferFcn dt = sts (λ (s,t) . s = 0 ∧ t = 0) (λ ((s,t),x) ((s',t'), y) .
y = -8 * s + 2 * x ∧ s' = s + (-4 * s - 2 * t + x) * dt ∧ t' = t + s * dt)"
subsubsection{*Section 3.2.2: Variable Name Scope*}
definition "A_sts = sts (λ s. s > 0) (λ (s, (x,y)) (s', z). z > s + x + y)"
definition "B_sts = sts (λ t. t > 0) (λ (t, (u, v)) (t', w). w > t + u + v)"
lemma "A_sts = B_sts"
by (simp add: A_sts_def B_sts_def)
subsubsection{*Section 3.2.3: Stateless STS Components*}
text{*The semantic version of the stateless STS component is defined using the mapping stateless2sts from the paper.*}
definition "stateless_sts r = sts ⊤ (λ (u::unit,x) (v::unit, y) . r x y)"
definition "Id_sts = stateless_sts (λ x y . y = x)"
definition "Add_sts = stateless_sts (λ (x,y) z . z = x + y)"
definition "Split_sts = stateless_sts (λ x (y,z) . y = x ∧ z = x)"
text{*Div components can also be defined as sts component*}
lemma Div_stateless: "Div_sts = stateless_sts (λ (x,y) z . y ≠ 0 ∧ z = x / y)"
by (simp add: Div_sts_def stateless_sts_def split_def)
subsubsection{*Section 3.2.3: Deterministic STS Components*}
text{*The semantic version of the deterministic STS component is defined using the mapping det2sts from the paper.*}
definition "det_sts s0 p state out = sts (λ s . s = s0) (λ (s,x) (s',y) . p (s, x) ∧ s' = state (s,x) ∧ y = out (s, x))"
lemma UnitDelay_det: "UnitDelay = det_sts 0 ⊤ (λ (s::'a::zero, x) . x) (λ (s, x) . s)"
apply (simp add: UnitDelay_def det_sts_def)
by (rule_tac f = "sts (λs. s = 0)" in arg_cong, auto)
lemma Id_sts_det: "Id_sts = det_sts () ⊤ (λ (s::unit, x) . ()) (λ (s::unit, x) . x)"
by (simp add: Id_sts_def det_sts_def stateless_sts_def split_def top_fun_def)
lemma Add_sts_det: "Add_sts = det_sts () ⊤ (λ (s::unit, (x,y)) . ()) (λ (s::unit, (x,y)) . x + y)"
by (simp add: Add_sts_def det_sts_def stateless_sts_def split_def top_fun_def)
lemma Div_sts_det: "Div_sts = det_sts () (λ (s::unit, (x,y)) . y ≠ 0) (λ (s::unit, (x,y)) . ()) (λ (s::unit, (x,y)) . x / y)"
by (simp add: Div_sts_def det_sts_def stateless_sts_def split_def top_fun_def)
lemma Split_sts_det: "Split_sts = det_sts () ⊤ (λ (s::unit, x) . ()) (λ (s::unit, x) . (x, x))"
apply (simp add: Split_sts_def det_sts_def stateless_sts_def split_def top_fun_def)
apply (rule_tac f = " sts (λx. True)" in arg_cong)
by (simp add: fun_eq_iff)
lemma Sum_sts_det: "Sum_sts = det_sts 0 ⊤ (λ (s, x) . s + x) (λ (s, x) . s)"
apply (simp add: Sum_sts_def det_sts_def stateless_sts_def split_def)
apply (rule_tac f = "sts (λs. s = 0)" in arg_cong)
by (auto simp add: fun_eq_iff)
subsubsection{*Section 3.2.3: Stateless Deterministic STS Components*}
text{*The semantic version of the stateless deterministic STS component is defined using the mapping stateless\_det2det from the paper.*}
definition "stateless_det_sts p out = det_sts () (λ (s::unit, x) . p x) (λ (s::unit, x) . ()) (λ (s::unit, x) . out x)"
text{*Many of the examples introduced above are both deterministic and stateless*}
lemma Id_sts_stateless_det: "Id_sts = stateless_det_sts ⊤ (λ x . x)"
by (simp add: Id_sts_det stateless_det_sts_def top_fun_def split_def)
lemma Add_sts_stateless_det: "Add_sts = stateless_det_sts ⊤ (λ (x, y) . x + y)"
by (simp add: Add_sts_det stateless_det_sts_def top_fun_def split_def)
lemma Split_sts_stateless_det: "Split_sts = stateless_det_sts ⊤ (λ x . (x, x))"
by (simp add: Split_sts_det stateless_det_sts_def top_fun_def split_def)
lemma Div_sts_stateless_det: "Div_sts = stateless_det_sts (λ (x, y) . y ≠ 0) (λ (x, y) . x / y)"
by (simp add: Div_sts_det stateless_det_sts_def top_fun_def split_def)
text{*fdbk is similar to Feedback but it requires the argument to have as input and output traces of pairs, while
Feedback has as input and output pairs of traces.*}
definition "fdbk S = Feedback ([- u, x ↝ u || x -] o S o [- uy ↝ fst o uy, snd o uy -])"
text{*Here is how the "Sum" composite component is defined (Simulink diagram in Fig.2).*}
definition "Sum_comp = fdbk (Add_sts o UnitDelay o Split_sts)"
text{*We can prove later that Sum\_sts = Sum\_comp*}
thm Sum_sts_def
thm sts_def
subsubsection{*Section 3.3: Quantified Linear Temporal Logic Components*}
subsubsection{*Section 3.3.1: QLTL*}
text{*For details on how QLTL is formalized in RCRS/Isabelle, see Temporal.thy*}
text{*Lemma 1.*}
text{*1. $top\_dep\ p$ is the semantic equivalent of $p$ does not contain temporal operators.*}
definition "EXISTS = SUPREMUM UNIV"
definition "FORALL = INFIMUM UNIV"
text{*The functions EXISTS and FORALL model the existential and universal quantifiers for QLTL formulas.
If $p:A \to B \to bool$ is a predicate with two parameters, then $EXISTS p : B \to bool$ is a predicate
with one parameter and $EXISTS p b = (\exists a . p\ a \ b)$.
*}
lemma lemma_1_1: "top_dep p ⟹ EXISTS (□ p) = □ (EXISTS p)"
apply (unfold EXISTS_def)
by (rule SUP_Always)
text {*2.*}
lemma lemma_1_2: "p leads p = □ p"
by (rule leads_always)
text {*3.*}
lemma lemma_1_3: "⊤ leads p = □ p"
by (rule top_leads_always)
text {*4.*}
lemma lemma_1_4: "p leads ⊤ = ⊤"
by (rule leads_top)
text {*5.*}
lemma lemma_1_5: "p leads ⊥ = ⊥"
by (rule leads_bot)
text {*6.*}
lemma lemma_1_6: "top_dep p ⟹ FORALL (p leads (λ y . q)) = ((EXISTS p) leads q)"
apply (unfold EXISTS_def FORALL_def)
by (rule top_dep_all_leadsto)
subsubsection{*Section 3.3.2: QLTL Components*}
text{*Semantically a QLTL component is a guarded property transformer on input output traces defined by a QLTL property.
If $\alpha \ x\ y$ is a QLTL property then the QLTL component of $\alpha$ is:
*}
definition "qltl α = {: α :]"
text{*However, for QLTL components, we use the syntax $\{: \alpha :]$ and its variant $\{: x \leadsto y . expr :]$,
where $expr$ is a QLTL expression on $x$ and $y$ *}
text{*For example the oven QLTL component is defined by *}
definition "thermostat = □ (ltl t . 180 ≤ t ∧ t ≤ 220)"
definition "oven = (ltl t . t = (20::nat)) ⊓ ((λ t . t 0 < t 1 ∧ t 0 < 180) until thermostat)"
definition "theromstat_liveness = ♢ (ltl t . t > 200)"
definition "Oven_qltl = {:x::(nat ⇒ unit) ↝ t . oven t:]"
subsubsection{*Section 3.4: Well Formed Components*}
text{*Since in Isabelle the components are semantic objects, they are well formed if they type check in Isabelle*}
text{*Next definition introduced a variant of the parallel composition closer to the parallel composition from the paper.
In the paper we assume that traces of pairs are equivalent to pair of traces $(x,y) = (\lambda i . (x\ i, y \ i))$.
The input of the new parallel composition variant is a trace of pairs, and the output is also a trace of pairs.*}
definition parallel_component :: "(((nat⇒'a) ⇒ bool) ⇒ ((nat ⇒ 'b) ⇒ bool)) ⇒ (((nat ⇒ 'c) ⇒ bool) ⇒ ((nat ⇒ 'd) ⇒ bool))
⇒ (((nat ⇒ 'a × 'c) ⇒ bool) ⇒ ((nat ⇒ 'b × 'd) ⇒ bool))"
(infixr "***" 70)
where
"(S *** T) = [-uv ↝ fst o uv, snd o uv -] o (S ** T) o [-x,y ↝ x || y -]"
definition "Switch1 = stateless_det_sts ⊤ (λ (x,y). ((x,y),x))"
definition "Switch2 = stateless_det_sts ⊤ (λ ((u,v),x). ((u,x),v))"
definition "Fig3 A B C = A o Switch1 o (B *** Id_sts) o Switch2 o (C *** Id_sts)"
subsection{*Section 4: Semantics*}
subsubsection{*Section 4.1: Monotonic Property Transformers*}
text{*Definition 8 (Skip) can be found in Refinement.thy. You can see the definition by placing
your cursor on the line "thm Skip\_def". You can also control-click on "Skip\_def" to be taken
automatically to the definition.*}
thm Skip_def
text{*Definition 9 (Fail) can be found in Refinement.thy.*}
thm Fail_def
text{*Definition 10 (Assert) can be found in Refinement.thy.*}
thm assert_def
text{*Definition 11 (Demonic update) can be found in Refinement.thy.*}
thm demonic_def
definition "DemonicEx1 = [:x, y ↝ z. (∀ i. z i = x i + y i) :]"
definition "DemonicEx3 = [: x ↝ y. y = (λ i. x i + 1) :]"
text{*Lemma 2. The first equality is proved below; the second and third are proved in Refinement.thy
by lemmas assert\_true\_skip and assert\_rel\_skip, whose definitions are repeated below.*}
lemma skip_demonic_rel: "Skip = [: x ↝ x'. x'=x :]"
by (simp add: Skip_def demonic_def fun_eq_iff le_fun_def)
thm assert_true_skip
thm assert_rel_skip
text{*Definition 12 (Angelic update) can be found in Refinement.thy.*}
thm angelic_def
text{*Lemma 3.*}
lemma assert_angelic_upd: "{.p.} = {: x ↝ x'. p x ∧ x' = x:}"
by (simp add: assert_def angelic_def fun_eq_iff)
text{*Results for serial composition. These results are proved in Refinement.thy by mono\_comp\_a, comp\_skip and skip\_comp.*}
thm mono_comp_a
thm comp_skip
thm skip_comp
text{*Definition 13 (Product) can be found in Refinement.thy.
Instead of the product notation $\otimes$ used in the paper, the notation ** is used in RCRS/Isabelle.
That is, product corresponds to parallel composition.*}
thm Prod_def
text{*Lemma 4 is proved in Refinement.thy by lemma mono\_prod.*}
thm mono_prod
text{*Skip with Unit as input and output type is the neutral element for product.*}
lemma "[:x ↝ y. r x y:] ** (Skip::(unit ⇒ bool) ⇒ (unit ⇒ bool)) = [: (x, u::unit) ↝ (y, v::unit). r x y :]"
by (simp add: Prod_demonic skip_demonic_rel)
lemma "(Skip::(unit ⇒ bool) ⇒ (unit ⇒ bool)) ** [:r:] = [: (u::unit, x) ↝ (v::unit, y). r x y :]"
by (simp add: Prod_demonic skip_demonic_rel)
text{*Definition 14 (Fusion) can be found in Refinement.thy.*}
thm Fusion_def
text{*Lemma 5 is proved in Refinement.thy by lemma Fusion\_spec.*}
thm Fusion_spec
text{*Definition 15 (IterateOmega) can be found in DelayFeedback.thy.*}
thm IterateOmegaA_def
text{*Definition 16 (Feedback) can be found in DelayFeedback.thy.*}
thm Feedback_def
thm IterateOmegaA_def
thm IterateMaskA_def
thm Mask_def
text{*Computing feedback of delayed sum.*}
definition "S_comp = [- λ (u, x). ((λi. if i = 0 then 0 else x(i - 1) + u(i - 1)), (λi. if i = 0 then 0 else x(i - 1) + u(i - 1)))-]"
definition "T_comp = [-(u, (y::nat ⇒ nat)), x ↝ ((u::nat ⇒ nat), x), x-] ∘ S_comp ** Skip"
lemma T_comp_simp: "T_comp
= [-(u,y), x ↝ ((λi. if i = 0 then 0 else x(i - 1) + u(i - 1)),(λi. if i = 0 then 0 else x(i - 1) + u(i - 1))), x -]"
apply (simp add: T_comp_def S_comp_def prod_update_skip update_comp)
apply (rule_tac f = update in arg_cong)
by auto
thm Summ.simps
lemma Summ_Suc: "Summ (λa. b (Suc a)) n + b 0 = Summ b n + b n"
by (induction n, auto)
lemma Summ_at_Suc: "⋀ b . Summ (b[Suc k ..]) n + b k = Summ (b[k..]) n + b (n + k)"
apply (cut_tac b = "b[k..]" and n = n in Summ_Suc)
apply simp
apply (subgoal_tac "(λa. b (Suc (k + a))) = (b[Suc k ..])")
apply simp
apply (simp add: add.commute)
by (simp add: fun_eq_iff)
lemma T_comp_power: "T_comp ^^ (Suc n) =
[-(u,y), x ↝ ((λi. if i ≤ n then Summ x i else Summ (x[i - Suc n..]) (Suc n) + u (i - Suc n)),
(λi. if i ≤ n then Summ x i else Summ (x[i - Suc n..]) (Suc n) + u (i - Suc n))), x -]"
proof (induction n)
case 0
then show ?case
apply (simp add: T_comp_simp)
apply (rule_tac f = update in arg_cong)
by (simp add: fun_eq_iff)
next
case (Suc n)
have [simp]: "⋀ b nata . ¬ Suc nata ≤ n ⟹ Summ (b[Suc nata - n ..]) n + b (nata - n) = Summ (b[Suc (nata - n) ..]) n + b (nata - n)"
by (simp add: Suc_diff_le)
have [simp]: "⋀ b nata . ¬ Suc nata ≤ n ⟹ Summ (b[Suc (nata - n) ..]) n + b (nata - n) = Summ (b[nata - n ..]) n + b nata"
by (simp add: Summ_at_Suc)
have "T_comp ^^ Suc (Suc n) = T_comp o (T_comp ^^ (Suc n))"
by simp
also have "... = T_comp o [- a ↝ case a of
(a, b) ⇒
(case a of
(u, y) ⇒
λx. ((λi. if i ≤ n then Summ x i else Summ (x[i - Suc n ..]) (Suc n) + u (i - Suc n),
λi. if i ≤ n then Summ x i else Summ (x[i - Suc n ..]) (Suc n) + u (i - Suc n)),
x))
b -]"
by (subst Suc, simp)
also have "... = [- a ↝ case a of
(a, b) ⇒
(case a of
(u, y) ⇒
λx. ((λi. if i ≤ Suc n then Summ x i else Summ (x[i - Suc (Suc n) ..]) (Suc (Suc n)) + u (i - Suc (Suc n)),
λi. if i ≤ Suc n then Summ x i else Summ (x[i - Suc (Suc n) ..]) (Suc (Suc n)) + u (i - Suc (Suc n))),
x))
b -]"
apply (simp add: T_comp_simp update_comp)
apply (rule_tac f = update in arg_cong)
apply (simp add: fun_eq_iff, auto)
apply (simp add: le_Suc_eq)
apply (case_tac x, simp_all)
by (case_tac nat, simp_all)
finally show ?case by simp
qed
lemma T_comp_IterateMaskA: "IterateMaskA T_comp n = [:(u, y), x ↝ (u', y'), x' .
(∀ i < n - 1 . x' i = x i ∧ y' i = Summ x i ∧ u' i = y' i):]"
apply (simp add: IterateMaskA_def Mask_def)
apply (case_tac n, simp)
apply (simp add: Havoc_def)
apply (rule_tac f = demonic in arg_cong)
apply auto [1]
apply (cut_tac n = nat in T_comp_power)
apply (simp)
apply (drule drop_assumption, simp)
apply (drule drop_assumption, simp)
apply (simp add: SkipTop_def update_def demonic_demonic OO_def)
apply (rule_tac f = demonic in arg_cong)
apply (simp add: fun_eq_iff)
by (simp add: eqtop_prod_def, auto)
text{*Next lemma proves relation (1) from the paper.*}
lemma Feedback_S_comp: "Feedback S_comp = [-Summ-]"
proof -
have [simp]: "Feedback S_comp
= {:x ↝ ((u, y), x').x = x':} ∘ IterateOmegaA (T_comp) ∘ [- ((u, y), x) ↝ y -]"
by (simp add: Feedback_def T_comp_def)
have "IterateMaskA T_comp = (λ n . [:(u, y), x ↝ (u', y'), x' .
(∀ i < n - 1 . x' i = x i ∧ y' i = Summ x i ∧ u' i = y' i):])"
by (simp add: T_comp_IterateMaskA fun_eq_iff)
from this have [simp]: "IterateOmegaA (T_comp) = (Fusion (λ n . [:(u, y), x ↝ (u', y'), x' .
(∀ i < n - 1 . x' i = x i ∧ y' i = Summ x i ∧ u' i = y' i):]))"
by (simp add: IterateOmegaA_def)
have [simp]: "Fusion (λn. [:((u, y), x)↝((u', y'), x').∀i<n - Suc 0. x' i = x i ∧ y' i = Summ x i ∧ u' i = y' i:])
= [:(u, y), x ↝ (u', y'), x' . (∀ i . x' i = x i ∧ y' i = Summ x i ∧ u' i = y' i):]"
apply (simp add: Fusion_demonic)
apply (rule_tac f = demonic in arg_cong)
apply (simp add: fun_eq_iff, auto)
by (metis add_diff_cancel_right' lessI)+
have "Feedback S_comp = {:x ↝ ((u, y), x').x = x':}
∘ [:(u::(nat ⇒ nat), (y::nat ⇒ nat)), x ↝ (u', y'), x' . (∀ i . x' i = x i ∧ y' i = Summ x i ∧ u' i = y' i):]∘ [- ((u, y), x) ↝ y -]"
by auto
also have "... = [-Summ-]"
apply (simp add: demonic_def fun_eq_iff update_def angelic_def le_fun_def)
apply safe
using ext apply blast
by metis
finally show ?thesis
by simp
qed
text{*Definition 17 (Refinement) is part of the Isabelle libraries (Orderings.thy).
Since MPTs are functions, refinement is simply an ordering on functions:*}
thm le_fun_def
text{*Theorem 1*}
text{*Theorem 1.1. These results are proved in Refinement.thy by lemmas mono\_comp,
prod\_mono1, prod\_mono2, and fusion\_mono1.*}
thm mono_comp
thm prod_mono1
thm prod_mono2
thm Fusion_refinement
thm fusion_mono1
text{*Theorem 1.2.*}
lemma theorem_1_2: "mono S ⟹ S ≤ T ⟹ IterateOmegaA S ≤ IterateOmegaA T"
by (rule IterateOmegaA_refin)
text{*Theorem 1.3.*}
lemma theorem_1_3: "S ≤ T ⟹ Feedback S ≤ Feedback T"
by (rule Feedback_refin)
subsubsection{*Section 4.2: Subclasses of MPTs*}
text{*Def.18 simply defines the terminology RPT.
Note that Property Transformers are instances of Predicate Transformers
(and predicate transformers are themselves instances of functions).
A predicate transformer is a function of type ('a $\rightarrow$ bool) $\rightarrow$ ('b $\rightarrow$ bool)
where types 'a and 'b are arbitrary. When these types are types of infinite
sequences, we get a property transformer, which is a function of type:
((nat $\rightarrow$ 'a) $\rightarrow$ bool) $\rightarrow$ ((nat $\rightarrow$ 'b) $\rightarrow$ bool).
Much of the RCRS formalization in Isabelle is done in terms of predicate transformers,
in order to establish more general results. Results that hold for (general) predicate
transformers automatically hold also for (the more specific) property transformers.
We sometimes wish to work with property transformers directly. Below, we define
the construct "sts init r", which produces a property transformer of type
((nat $\rightarrow$ 'a) $\rightarrow$ bool) $\rightarrow$ ((nat $\rightarrow$ 'b) $\rightarrow$ bool)
where init is of type ('c $\rightarrow$ bool) and r of type ('c $\times$ 'b $\rightarrow$ 'c $\times$ 'a $\rightarrow$ bool).*}
text{*A series of small RPT examples after Def.18, stated as lemmas:*}
lemma Fail_is_a_RPT: "Fail = {. x . False .} o [: x ↝ y . True :]"
by (simp add: fun_eq_iff assert_def Fail_def)
lemma Skip_is_a_RPT: "Skip = {. x. True.} o [: x ↝ y. y = x :]"
by (simp add: Skip_def fun_eq_iff assert_def demonic_def le_fun_def)
lemma Assert_is_a_RPT: "{.p.} = {.p.} o [: x ↝ y. y=x:]"
by (simp add: fun_eq_iff assert_def demonic_def le_fun_def)
lemma Demonic_is_a_RPT: "[:r:] = {.⊤.} o [:r:]"
by(simp add: fun_eq_iff demonic_def assert_def)
definition "RPT_S1 = {. ⊤ .} o [: (x, y) ↝ z . y ≠ 0 ∧ z = x / y :]"
definition "RPT_S2 = {. (x, y) . y ≠ 0 .} o [: (x, y) ↝ z . z = x / y :]"
text{*Theorem 2 is proved in Refinement.thy by lemmas assert\_demonic\_comp, Prod\_spec, fusion\_spec*}
thm assert_demonic_comp
thm Prod_spec
thm Fusion_spec
text{*The theorem 2 in the paper uses Fusion applied to two RPTs, but Fusion\_spec is proved for an arbitrary
number of RPTs.*}
text{*RPTs are not closed under Feedback operation.*}
lemma "Feedback [-u::nat ⇒ 'a, x::nat ⇒'b ↝ u, u-] = {:⊤:}"
by (rule Feedback_example)
text{*Theorem 3 is proved in Refinement.thy by lemma assert\_demonic\_refinement*}
thm assert_demonic_refinement
subsubsection{*Section 4.2.2: Guarded MPTs*}
text{*Definition 19 is given in Refinement.thy by the definition of $trs$*}
thm trs_def
thm Magic_def
lemma MagicAlternativeDef: "Magic = [: x ↝ y . False :]"
apply (simp add: fun_eq_iff)
apply (unfold Magic_def demonic_def le_fun_def)
by simp
lemma Fail_is_a_GPT: "Fail = {: ⊥ :]"
by (simp add: trs_def Fail_def fun_eq_iff assert_def inpt_def)
lemma Skip_is_s_GPT: "Skip = {: x ↝ y. y = x :]"
by (simp add: trs_def fun_eq_iff assert_def inpt_def demonic_def le_fun_def)
lemma Assert_is_a_GPT: "{.p.} = {: x ↝ y. p x ∧ y = x :]"
apply (simp add: trs_def fun_eq_iff assert_def inpt_def demonic_def le_fun_def)
by blast
lemma "inpt r = ⊤ ⟹ [:r:] = {:r:]"
by (simp add: trs_def fun_eq_iff demonic_def assert_def)
lemma "[:r:] = {: r:] ⟹ inpt r = ⊤"
by (metis Demonic_is_a_RPT prec_spec trs_def)
text{*Theorem 4 is proved in Refinement.thy by lemmas trs\_trs and trs\_prod.*}
thm trs_trs
thm trs_prod
text{*Corollary 1 is proved in Refinement.thy by lemmas trs\_refinement.*}
thm trs_refinement
subsubsection{*Section 4.3: Semantics of Components as MPTs*}
text{*As mentioned already, the components are semantic objects. The semantics of qltl component, relation (2),
is the definition qltl\_def. The semantics of the serial composition, relation (3), is the function composition of
property transformers. The semantics of the parallel composition, relation (4), is the definition
parallel\_component\_def. The semantics of the feedback composition, relation (5), is the definition
fdbk\_def*}
thm qltl_def
thm parallel_component_def
thm fdbk_def
text{*Lemma 6.*}
lemma lemma_6: "{: x ↝ y. inpt r x ∧ r x y :] = {: x ↝ y. r x y:]"
by (simp add: fun_eq_iff trs_def assert_def demonic_def inpt_def le_fun_def, auto)
text{*The semantics of the sts components, relation (6), is given by sts\_def*}
thm sts_def
text{*The semantics of the other components are given by their definitions:*}
thm stateless_sts_def
thm det_sts_def
thm stateless_det_sts_def
text{*Next lemma is an auxiliary results that links the definition oo sts to LocalSystem defined
in RefinementReactive.thy.*}
lemma sts_LocalSystem: "sts init r = LocalSystem init (inpt r) r"
by (auto simp add: sts_def fun_eq_iff demonic_def assert_def le_fun_def LocalSystem_def)
lemma sts_inpt_top: "inpt r = ⊤ ⟹ sts init r = [:rel_pre_sts init r:]"
by (simp add: sts_LocalSystem LocalSystem_prec_top)
lemma stateless2LocalSystem: "stateless_sts r = LocalSystem (⊤::unit⇒bool) (λ (s::unit, x) . inpt r x) (λ (s::unit, x) (s'::unit, y) . r x y)"
apply (simp add: stateless_sts_def sts_LocalSystem)
apply (subgoal_tac "(inpt (λ(u::unit, x) (v::unit, y). r x y)) = (λ(s, x). inpt r x)")
apply simp_all
by (simp add: fun_eq_iff inpt_def)
lemma det2LocalSystem: "det_sts s0 p state out = LocalSystem (λ s . s = s0) p (λ (s,x) (s',y) . s' = state (s,x) ∧ y = out (s, x) )"
apply (simp add: det_sts_def sts_LocalSystem)
apply (simp add: DelayFeedback_LocalSystem [symmetric])
apply (subgoal_tac "({. p .} ∘ [:(s, x)↝(s', y).s' = state (s, x) ∧ y = out (s, x):])
= ({. inpt (λ(s, x) ab. p (s, x) ∧ (case ab of (s', y) ⇒ s' = state (s, x) ∧ y = out (s, x))) .} ∘
[:(s, x)↝ab . p (s, x) ∧ (case ab of (s', y) ⇒ s' = state (s, x) ∧ y = out (s, x)):])")
apply simp
by (simp add: fun_eq_iff demonic_def assert_def le_fun_def inpt_def, auto)
lemma stateless_det2LocalSystem: "stateless_det_sts p out = LocalSystem (⊤::unit⇒bool) (λ (s::unit, x) . p x) (λ (s::unit, x) (s'::unit, y) . y = out x)"
by (simp add: stateless_det_sts_def det2LocalSystem top_fun_def)
text{*Lemma 7.*}
theorem stateless_det2stateless: "stateless_det_sts p out = stateless_sts (λ x y . p x ∧ y = out x)"
apply (simp add: stateless_det2LocalSystem stateless2LocalSystem)
apply (simp add: DelayFeedback_LocalSystem [symmetric])
apply (subgoal_tac "({.(s::unit, y).p y.} ∘ [:(s::unit, x)↝(s', y).y = out x:]) =
({.(s::unit, x).p x ∧ inpt (λx y. y = out x) x.} ∘ [:(s::unit, x)↝ab . p x ∧ (case ab of (s'::unit, y) ⇒ y = out x):])")
apply simp
by (simp add: fun_eq_iff demonic_def assert_def _le_fun_def inpt_def, auto)
thm Sum_comp_def
subsubsection{*Section 4.3.1: Example: Two Alternative Derivations of the Semantics of Diagram Sum*}
lemma Add_sts_simp: "Add_sts = [-ux ↝ (λ i . fst (ux i) + snd (ux i))-]"
proof (simp add: Add_sts_def stateless_sts_def sts_def illegal_sts_def)
have [simp]: "- illegal_sts ⊤ (inpt (λ(u, x) (v, y). (case x of (x, y) ⇒ λz. z = x + y) y))
(λ(u, x) (v, y). (case x of (x, y) ⇒ λz. z = x + y) y) = ⊤"
by (simp add: fun_eq_iff illegal_sts_def split_def inpt_def)
show " {. - illegal_sts ⊤ (inpt (λ(u, x) (v, y). (case x of (x, y) ⇒ λz. z = x + y) y))
(λ(u, x) (v, y). (case x of (x, y) ⇒ λz. z = x + y) y) .} ∘
[:x↝y.∃s. run_sts (λ(u, x) (v, y). (case x of (x, y) ⇒ λz. z = x + y) y) s x y:] =
[- ux ↝ λi. fst (ux i) + snd (ux i) -]"
apply (simp add: assert_true_skip update_def)
apply (rule_tac f = demonic in arg_cong)
by (simp add: run_sts_def split_def, auto)
qed
lemma UnitDelay_simp: "UnitDelay = [-x ↝ (λ i . if i = 0 then 0 else x (i - 1))-]"
proof (simp add: UnitDelay_def stateless_sts_def sts_def illegal_sts_def)
have [simp]: "- illegal_sts (λs. s = 0) (inpt (λ(s, x) (s', y). y = s ∧ s' = x)) (λ(s, x) (s', y). y = s ∧ s' = x) = ⊤"
by (simp add: fun_eq_iff illegal_sts_def split_def inpt_def)
show " {. - illegal_sts (λs. s = 0) (inpt (λ(s, x) (s', y). y = s ∧ s' = x)) (λ(s, x) (s', y). y = s ∧ s' = x) .} ∘
[:x↝y.∃s. s 0 = 0 ∧ run_sts (λ(s, x) (s', y). y = s ∧ s' = x) s x y:] =
[- x ↝ λi. if i = 0 then 0 else x (i - 1) -]"
apply (simp add: assert_true_skip update_def)
apply (rule_tac f = demonic in arg_cong)
apply (simp add: run_sts_def split_def fun_eq_iff, auto)
by (case_tac xb, auto)
qed
lemma Split_sts_simp: "Split_sts = [-x ↝ (λ i . (x i, x i))-]"
proof (simp add: Split_sts_def stateless_sts_def sts_def illegal_sts_def)
have [simp]: "- illegal_sts ⊤ (inpt (λ(u, x) (v, y, z). y = x ∧ z = x)) (λ(u, x) (v, y, z). y = x ∧ z = x) = ⊤"
by (simp add: fun_eq_iff illegal_sts_def split_def inpt_def)
show "{. - illegal_sts ⊤ (inpt (λ(u, x) (v, y, z). y = x ∧ z = x)) (λ(u, x) (v, y, z). y = x ∧ z = x) .} ∘
[:x↝y.∃s. run_sts (λ(u, x) (v, y, z). y = x ∧ z = x) s x y:] =
[- x ↝ λi. (x i, x i) -]"
apply (simp add: assert_true_skip update_def)
apply (rule_tac f = demonic in arg_cong)
apply (simp add: run_sts_def split_def fun_eq_iff, auto)
by (simp add: prod_eq_iff)
qed
lemma Sum_comp_simp: "Sum_comp = [-Summ-]"
proof -
have [simp]: "[- (u, (x::nat ⇒ nat)) ↝ u || x -] ∘ (Add_sts ∘ UnitDelay ∘ Split_sts) ∘ [- uy ↝ (fst ∘ uy, snd ∘ uy) -] = S_comp"
apply (simp add: Add_sts_simp UnitDelay_simp Split_sts_simp update_comp S_comp_def)
apply (rule_tac f = update in arg_cong)
by (simp add: fun_eq_iff nzip_def)
have "Sum_comp = fdbk (Add_sts ∘ UnitDelay ∘ Split_sts)"
by (simp add: Sum_comp_def)
also have "... = [-Summ-]"
by (simp add: fdbk_def Feedback_S_comp)
finally show ?thesis
by simp
qed
text{*The SumAtomic sts is the same as Sum\_sts defined above*}
thm Sum_sts_def
lemma Sum_sts_simp: "Sum_sts = [: x ↝ y . ∃ s . s 0 = 0 ∧ (∀ i . y i = s i ∧ s (Suc i) = s i + x i) :]"
proof (simp add: Sum_sts_def stateless_sts_def sts_def illegal_sts_def)
have [simp]: "- illegal_sts (λs. s = 0) (inpt (λ(s, x) (s', y). y = s ∧ s' = s + x)) (λ(s, x) (s', y). y = s ∧ s' = s + x) = ⊤"
by (simp add: fun_eq_iff illegal_sts_def split_def inpt_def)
show "{. - illegal_sts (λs. s = 0) (inpt (λ(s, x) (s', y). y = s ∧ s' = s + x)) (λ(s, x) (s', y). y = s ∧ s' = s + x) .} ∘
[:x↝y.∃s. s 0 = 0 ∧ run_sts (λ(s, x) (s', y). y = s ∧ s' = s + x) s x y:] =
[:x↝y.∃s. s 0 = 0 ∧ (∀i. y i = s i ∧ s (Suc i) = s i + x i):]"
apply (simp add: assert_true_skip)
apply (rule_tac f = demonic in arg_cong)
by (simp add: run_sts_def split_def fun_eq_iff)
qed
lemma Sum_comp_Sum_sts: "Sum_comp = Sum_sts"
apply (simp add: Sum_sts_simp Sum_comp_simp update_def)
apply (rule_tac f = demonic in arg_cong)
apply (simp add: fun_eq_iff, safe)
using Summ.simps(1) Summ.simps(2) apply blast
by (metis Nat.add_0_right sum_suc)
lemmas ex1 = Sum_comp_Sum_sts
subsubsection{*Section 4.3.2: Characterization of Legal Input Traces*}
text{*The function legal from the paper is implemented by the function prec in the Isabelle theories*}
definition "legal S = S ⊤"
lemma legal_prec: "legal S = ((prec S)::'a::boolean_algebra)"
by (simp add: legal_def prec_def fail_def)
text{*Lemma 8 is proved below.*}
lemma legal_RPT: "legal ({.p.} o [:r::'a ⇒ 'b ⇒ bool:]) = p"
by (simp add: legal_prec)
lemma legal_GPT: "legal ({:r:]) = (inpt r)"
by (simp add: trs_def legal_prec)
lemma legal_sts_1: "legal (sts init r) = (-illegal_sts init (inpt r) r)"
by (simp add: sts_def legal_prec)
lemma legal_sts_2: "legal (sts init r) = (prec_pre_sts init (inpt r) r)"
by (simp add: sts_LocalSystem LocalSystem_simp legal_prec)
lemma legal_qltl: "legal (qltl r) = (inpt r)"
by (simp add: qltl_def legal_GPT)
lemmas lemma_8 = legal_RPT legal_GPT legal_sts_1 legal_sts_2 legal_qltl
text{*Theorem 5. The first result is the associativity of function composition.
The second item cannot be expressed as clean as in the paper. In the paper we assume concatenation
of tuples that cannot be defined in Isabelle
*}
thm comp_assoc
theorem theorem_5_2: "S ** (S' ** S'') = [-x,y,z ↝ (x,y), z-] o ((S ** S') ** S'') o [-(x,y),z ↝ x,y,z-]"
apply (simp add: fun_eq_iff Prod_def le_fun_def prod_pred_def update_def demonic_def, safe)
apply (rule_tac x = "(λ (a, b) . p a ∧ pa b)" in exI, simp)
apply (rule_tac x = "p'a" in exI, simp)
apply auto [1]
apply (rule_tac x = pa in exI, simp)
apply (rule_tac x = "(λ (b,c) . p'a b ∧ p' c)" in exI, simp)
by auto [1]
text{*Theorem 5. The third item is proved next*}
lemma "(Skip ** Magic) o (Fail ** Fail) ≠ (Skip o Fail) ** (Magic o Fail)"
by simp
theorem theorem_5_3_aux: "p ≤ inpt r ⟹ p' ≤ inpt r' ⟹ (({.p.} o [:r:]) ** ({.p'.} o [:r':])) o (({.q.} o [:s:]) ** ({.q'.} o [:s':]))
= (({.p.} o [:r:]) o ({.q.} o [:s:])) ** (({.p'.} o [:r':]) o ({.q'.} o [:s':]))"
proof (simp add: Prod_spec assert_demonic_comp OO_def comp_assoc [THEN sym] )
have [simp]: "(λ x z . ∃a b. (case x of (x, y) ⇒ λ(u, v). r x u ∧ r' y v) (a, b) ∧ (case z of (u, v) ⇒ s a u ∧ s' b v)) =
(λ (x, y) (u, v).(∃y. r x y ∧ s y u) ∧ (∃ya. r' y ya ∧ s' ya v))"
by (simp add: fun_eq_iff, auto)
assume "p' ≤ inpt r'"
assume "p ≤ inpt r"
have [simp]: "(λ x.(case x of (x, y) ⇒ p x ∧ p' y) ∧ (∀a b. (case x of (x, y) ⇒ λ(u, v). r x u ∧ r' y v) (a, b) ⟶ q a ∧ q' b))
= (λ (x, y).p x ∧ (∀y. r x y ⟶ q y) ∧ p' y ∧ (∀ya. r' y ya ⟶ q' ya))"
apply (simp add: fun_eq_iff, auto)
apply (meson ‹p' ≤ inpt r'› inpt_def predicate1D)
by (metis ‹p ≤ inpt r› inpt_def predicate1D)
show "{.x.(case x of (x, y) ⇒ p x ∧ p' y) ∧ (∀a b. (case x of (x, y) ⇒ λ(u, v). r x u ∧ r' y v) (a, b) ⟶ q a ∧ q' b).} ∘
[:x↝z.∃a b. (case x of (x, y) ⇒ λ(u, v). r x u ∧ r' y v) (a, b) ∧ (case z of (u, v) ⇒ s a u ∧ s' b v):] =
{.(x, y).p x ∧ (∀y. r x y ⟶ q y) ∧ p' y ∧ (∀ya. r' y ya ⟶ q' ya).} ∘ [:(x, y)↝(u, v).(∃y. r x y ∧ s y u) ∧ (∃ya. r' y ya ∧ s' ya v):]"
by simp
qed
theorem theorem_5_3: "({:r:] ** {:r':]) o (({.q.} o [:s:]) ** ({.q'.} o [:s':]))
= (({:r:]) o ({.q.} o [:s:])) ** (({:r':]) o ({.q'.} o [:s':]))"
apply (simp add: trs_def)
by (subst theorem_5_3_aux [THEN sym], simp_all)
text{*Theorem 5. The fourth result is proved by in Refinement.thy by lemma mono\_comp, by lemma prod\_ref below and in ReactiveRefinement.thy by lemma Feedback\_refin, respectively.*}
thm mono_comp
lemma prod_ref: "S≤S' ⟹ T≤T' ⟹ S ** T ≤ S' ** T'"
apply (simp add: le_fun_def mono_def Prod_def prod_pred_def)
by blast
lemma theorem_5_4_c: "mono S ⟹ S ≤ T ⟹ fdbk S ≤ fdbk T"
apply (simp add: fdbk_def)
apply (rule Feedback_refin)
apply (rule mono_comp, simp_all)
by (rule mono_comp, simp_all)
lemmas theorem_5 = comp_assoc theorem_5_2 theorem_5_3
mono_comp prod_ref theorem_5_4_c
lemma theorem_6: "(S ≤ T) = (∀ p q . Hoare p S q ⟶ Hoare p T q)"
by (rule refinement_hoare_iff)
subsection{*Section 5: Symbolic Reasoning*}
text{*Theorem 7.*}
definition "sts2qltl init r = (λ x y . prec_pre_sts init (inpt r) r x ∧ rel_pre_sts init r x y)"
thm prec_pre_sts_def
thm rel_pre_sts_def
theorem theorem_7_sts_a: "init a ⟹ sts init r = {:sts2qltl init r:]"
apply (simp add: sts_LocalSystem LocalSystem_simp sts2qltl_def qltl_def)
apply (subst prec_inpt_equiv [of , THEN sym], simp_all)
by (simp add: prec_pre_sts_inpt)
theorem theorem_7_sts: "init a ⟹ sts init r = qltl (sts2qltl init r)"
by (simp add: theorem_7_sts_a qltl_def)
lemma stateless_sts_simp: "stateless_sts r = {.(□ (λ x . inpt r (x 0))).} o [: (□ (λ x y. r (x 0) (y 0))):]"
proof -
have [simp]: "rel_pre_sts ⊤ (λ(s, x) (s', y). r x y) = (□ (λ x y. r (x 0) (y 0)))"
by (simp add: fun_eq_iff always_def at_fun_def rel_pre_sts_simp)
show "stateless_sts r = {. □ (λx. inpt r (x 0)) .} ∘ [: □ (λx y. r (x 0) (y 0)) :]"
by (simp add: stateless2LocalSystem LocalSystem_simp prec_stateless_sts_simp)
qed
theorem theorem_7_stateless_sts_a: "stateless_sts r = {: (□ (λ x y. r (x (0::nat)) (y (0::nat)))):]"
apply (simp add: stateless_sts_simp trs_def)
apply (subgoal_tac "(□ (λx. inpt r (x (0::nat)))) = inpt (□ (λx y. r (x (0::nat)) (y (0::nat))))", simp)
by (simp add: fun_eq_iff always_def inpt_def at_fun_def choice_iff)
theorem theorem_7_stateless_sts: "stateless_sts r = qltl (□ (λ x y. r ( x (0::nat)) (y (0::nat))))"
by (simp add: theorem_7_stateless_sts_a qltl_def)
lemmas theorem_7 = theorem_7_sts theorem_7_stateless_sts
lemma "stateless_sts (λ x y . y > x) = qltl (□ (λ x y . y (0::nat) > x (0::nat)))"
by(rule theorem_7_stateless_sts)
lemma "stateless_sts (λ x (y::unit) . x > 0) = qltl (□ (λ x y . x (0::nat) > 0))"
by(rule theorem_7_stateless_sts)
lemma "UnitDelay = qltl (λ x y . y 0 = 0 ∧ (□ (λ x y . y (1::nat) = x (0::nat))) x y)"
apply (simp add: UnitDelay_def theorem_7_sts sts2qltl_def prec_pre_sts_def rel_pre_sts_def)
apply (rule_tac f = qltl in arg_cong)
apply (simp add: fun_eq_iff always_def lift_rel_def at_fun_def at_prod_def lift_pre_def inpt_def leads_def until_def)
apply safe
apply auto [2]
apply (rule_tac x = "λ i::nat . if i = 0 then 0 else x (i - 1)" in exI)
apply simp
by (safe, case_tac f, simp_all)
subsubsection{*Section 5.3: Symbolic Computation of Serial Composition.*}
text{*Theorem 8 for Equation 13.*}
theorem qltl_serial_a: "r'' = (λ x z . (∀ y . r x y ⟶ inpt r' y) ∧ (∃ y . r x y ∧ r' y z))
⟹ {:r:] o {:r':] = {:r'':]"
apply (simp add: fun_eq_iff demonic_def assert_def le_fun_def inpt_def trs_def, auto)
by (drule_tac x = xb in spec, auto)
theorem qltl_serial: "r'' = (λ x z . (∀ y . r x y ⟶ inpt r' y) ∧ (∃ y . r x y ∧ r' y z))
⟹ qltl r o qltl r' = qltl r''"
by (simp add: qltl_def qltl_serial_a)
text{*Theorem 8 for Equation 14.*}
definition "sts_comp_rel r r' = (λ ((u,v), x) ((u',v'), z) . inpt r (u,x) ∧ (∀ y u' . r (u, x) (u',y)
⟶ inpt r' (v,y)) ∧ (∃ y . r (u,x) (u',y) ∧ r' (v,y) (v',z)) ) "
theorem sts_serial: "init' a ⟹ sts init r o sts init' r' = sts (prod_pred init init') (sts_comp_rel r r')"
apply (simp add: sts_LocalSystem DelayFeedback_LocalSystem [symmetric])
apply (subst DelayFeedback_comp, simp_all)
apply (subgoal_tac " ({. prec_comp_sts (inpt r) r (inpt r') .} ∘ [: rel_comp_sts r r' :]) = ({. inpt (sts_comp_rel r r') .} ∘ [: sts_comp_rel r r' :])")
apply simp_all
apply (subst prec_inpt_equiv, simp_all)
apply (simp add: prec_comp_sts_def le_fun_def rel_comp_sts_def inpt_def)
apply auto [1]
apply (drule_tac x = bb in spec, safe)
apply simp
apply auto [1]
by (simp add: trs_def prec_comp_sts_def le_fun_def rel_comp_sts_def inpt_def sts_comp_rel_def fun_eq_iff demonic_def assert_def)
text{*Theorem 8 for Equation 15.*}
theorem stateless_serial: "stateless_sts r o stateless_sts r'
= stateless_sts (λ x z . (∀ y . r x y ⟶ inpt r' y) ∧ (∃ y . r x y ∧ r' y z))"
apply (simp add: stateless_sts_def sts_serial)
apply (simp add: sts_LocalSystem sts_def LocalSystem_def fun_eq_iff illegal_sts_def sts_comp_rel_def prod_pred_def run_sts_def inpt_def, auto)
by blast+
text{*Theorem 8 for Equation 16.*}
theorem det_serial: "det_sts s0 p state out o det_sts s0' p' state' out'
= det_sts (s0, s0') (λ ((s,s'),x) . p (s, x) ∧ p' (s', out (s, x))) (λ ((s,s'),x) . (state (s,x), state' (s', out(s,x))))
(λ ((s,s'),x) . (out' (s', out(s,x))))"
apply (simp add: det_sts_def sts_serial)
apply (subgoal_tac "(prod_pred (λs. s = s0) (λs. s = s0')) = (λs. s = (s0, s0'))")
apply simp
apply (subgoal_tac " (sts_comp_rel (λ(s, x) ab. p (s, x) ∧ (case ab of (s', y) ⇒ s' = state (s, x) ∧ y = out (s, x)))
(λ(s, x) ab. p' (s, x) ∧ (case ab of (s', y) ⇒ s' = state' (s, x) ∧ y = out' (s, x)))) =
(λ(s, x) ab.
(case s of (s, s') ⇒ λx. p (s, x) ∧ p' (s', out (s, x))) x ∧
(case ab of (s', y) ⇒ s' = (case s of (s, s') ⇒ λx. (state (s, x), state' (s', out (s, x)))) x ∧
y = (case s of (s, s') ⇒ λx. out' (s', out (s, x))) x))")
apply simp
apply (simp add: fun_eq_iff sts_comp_rel_def inpt_def, auto)
by (simp add: prod_pred_def fun_eq_iff)
text{*Theorem 8 for Equation 17.*}
theorem stateless_det_serial: "stateless_det_sts p out o stateless_det_sts p' out' =
stateless_det_sts (p ⊓ (p' o out)) (out' o out)"
apply (simp add: stateless_det2stateless stateless_serial)
apply (subgoal_tac "(λx z. (p x ⟶ p' (out x) ∧ inpt (λx y. y = out' x) (out x)) ∧ p x ∧ p' (out x) ∧ z = out' (out x))
= (λx y. p x ∧ p' (out x) ∧ y = out' (out x))")
apply simp
by (simp add: fun_eq_iff inpt_def, auto)
lemmas theorem_8 = qltl_serial sts_serial stateless_serial det_serial stateless_det_serial
definition "C1_comp = stateless_sts ⊤"
definition "C2_comp = stateless_det_sts (λ (x, y) . y ≠ (0::real)) (λ (x, y) . x / y)"
lemma "C1_comp o C2_comp = stateless_sts ⊥"
apply (simp add: C1_comp_def C2_comp_def stateless_det2stateless stateless_serial)
apply (rule_tac f = stateless_sts in arg_cong)
by (simp add: fun_eq_iff inpt_def)
lemma assumes x: "x = (λ x y . x (0::nat))" and y: "y = (λ x y . y (0::nat))"
shows "qltl (□ (x → ♢ y)) o qltl (□ ♢ x) = qltl (□ ♢ x)"
proof -
have [simp]: "⋀ xa xb. (∃ya. (□ (x → ♢ y)) xa ya ∧ (□ ♢ x) ya xb)"
by (simp add: always_def impl_def x y eventually_def at_fun_def, auto)
have [simp]: "⋀xa xb. (∀ya. (□ (x → ♢ y)) xa ya ⟶ Ex ((□ ♢ x) ya)) = (□ ♢ x) xa xb"
apply (simp_all add: fun_eq_iff inpt_def always_def eventually_def at_fun_def x y impl_def )
apply safe
apply (drule_tac x = "xa" in spec)
apply safe
apply (rule_tac x = 0 in exI, simp)
apply simp
apply (simp add: Inf_fun_def, safe)
apply (drule_tac x = f in spec, safe)
apply (drule_tac x = "f + fa" in spec, safe)
apply (rule_tac x = "fa + fb" in exI)
by (simp add: add.assoc)
show "qltl (□ (x → ♢ y)) o qltl (□ ♢ x ) = qltl (□ ♢ x)"
apply (simp add: qltl_serial)
apply (rule_tac f = qltl in arg_cong)
by (simp add: fun_eq_iff inpt_def)
qed
subsubsection{*Section 5.4: Symbolic Computation of Parallel composition*}
text{*Theorem 9 for Equation 18.*}
theorem qltl_parallel_a: "{:r:] ** {:r':] = {: (x,x') ↝ (y,y') . r x y ∧ r' x' y':]"
by (rule trs_prod)
theorem qltl_parallel_b: "{:r:] *** {:r':] = {: x ↝ y . r (fst o x) (fst o y) ∧ r' (snd o x) (snd o y):]"
apply (simp add: parallel_component_def trs_prod update_def)
apply (simp add: trs_def fun_eq_iff nzip_def demonic_def assert_def le_fun_def inpt_def split_def, auto)
apply (metis fst_convol snd_convol)
apply (drule_tac x = xb in spec, auto)
apply (subgoal_tac "a = (fst ∘ xb)")
apply simp_all
apply (subgoal_tac "b = (snd ∘ xb)")
by simp_all
theorem qltl_parallel: "qltl r ** qltl r' = qltl (λ (x, x') (y, y'). r x y ∧ r' x' y')"
by (simp add: qltl_def qltl_parallel_a)
text{*Theorem 9 for Equation 19.*}
theorem sts_parallel_a: "init a ⟹ init' b ⟹ sts init r ** sts init' r' =
[- (x, x') ↝ x || x' -] ∘ sts (prod_pred init init') (rel_prod_sts r r') o [- y ↝ (fst ∘ y, snd ∘ y) -]"
apply (simp add: sts_LocalSystem sts_prod)
apply (subgoal_tac " (prec_prod_sts (inpt r) (inpt r')) = (inpt (rel_prod_sts r r'))")
apply simp
by (simp add: prec_prod_sts_def inpt_def fun_eq_iff rel_prod_sts_def)
lemma split_nzip: "[- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘ [- (x, x') ↝ x || x' -] = [-id-]"
apply (simp add: update_comp)
apply (rule_tac f = update in arg_cong)
by (simp add: fun_eq_iff nzip_def)
theorem sts_parallel: "init a ⟹ init' b ⟹ sts init r *** sts init' r' = sts (prod_pred init init') (rel_prod_sts r r')"
proof (simp add: parallel_component_def sts_parallel_a)
have "[- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
([- (x, x') ↝ x || x' -] ∘ sts (prod_pred init init') (rel_prod_sts r r') ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]) ∘
[- (x, y) ↝ x || y -] =
([- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
[- (x, x') ↝ x || x' -]) ∘ sts (prod_pred init init') (rel_prod_sts r r') ∘ ([- y ↝ (fst ∘ y, snd ∘ y) -] ∘
[- (x, y) ↝ x || y -])"
by (simp add: comp_assoc)
also have "... = sts (prod_pred init init') (rel_prod_sts r r')"
by (simp add: split_nzip update_id_Skip)
finally show "[- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
([- (x, x') ↝ x || x' -] ∘ sts (prod_pred init init') (rel_prod_sts r r') ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]) ∘
[- (x, y) ↝ x || y -] = sts (prod_pred init init') (rel_prod_sts r r')"
by simp
qed
text{*Theorem 9 for Equation 20.*}
theorem stateless_parallel_a: "stateless_sts r ** stateless_sts r' =
[- (x, x') ↝ x || x' -] ∘ stateless_sts (λ (x,x') (y,y') . r x y ∧ r' x' y') o [- y ↝ (fst ∘ y, snd ∘ y) -]"
apply (simp add: stateless_sts_def sts_parallel_a)
apply (subgoal_tac "sts (prod_pred ⊤ ⊤) (rel_prod_sts (λ(u::unit, x) (v::unit, y). r x y) (λ(u::unit, x) (v::unit, y). r' x y))
= sts ⊤ (λ(u::unit, x) (v::unit, y). (case x of (x, x') ⇒ λ(y, y'). r x y ∧ r' x' y') y)")
apply simp
apply (simp add: theorem_7)
apply (subst theorem_7)
apply (simp add: prod_pred_def)
apply (simp add: qltl_def)
apply (rule_tac f = trs in arg_cong)
proof -
have[simp]: "⋀ x xa . rel_pre_sts (prod_pred ⊤ ⊤) (λ((u::unit, v::unit), x, y) ((u'::unit, v'::unit), x', y'). r x x' ∧ r' y y') x xa
= rel_pre_sts ⊤ (λ(u::unit, x) (v::unit, y). (case x of (x, x') ⇒ λ(y, y'). r x y ∧ r' x' y') y) x xa"
apply (simp add: rel_pre_sts_simp prod_pred_def, safe)
apply (drule_tac x = i in spec)
apply (case_tac "x i", simp)
apply (drule_tac x = i in spec)
apply (case_tac "x i", simp)
apply (rule_tac x = "λ i. ((),())" in exI, safe)
apply (drule_tac x = i in spec)
apply (case_tac "x i", simp)
apply (drule_tac x = i in spec)
by (case_tac "x i", simp)
have [simp]: "⋀ x . (prec_pre_sts (prod_pred ⊤ ⊤) (inpt (λ((u::unit, v::unit), x, y) ((u'::unit, v'::unit), x', y'). r x x' ∧ r' y y'))
(λ((u::unit, v::unit), x, y) ((u'::unit, v'::unit), x', y'). r x x' ∧ r' y y') x)
= (prec_pre_sts ⊤ (inpt (λ(u::unit, x) (v::unit, y). (case x of (x, x') ⇒ λ(y, y'). r x y ∧ r' x' y') y))
(λ(u::unit, x) (v::unit, y). (case x of (x, x') ⇒ λ(y, y'). r x y ∧ r' x' y') y) x)"
apply (simp add: prec_pre_sts_simp inpt_def prod_pred_def, safe)
apply (drule_tac x = "λ i. ((),())" in spec)
apply (drule_tac x = y in spec)
apply (drule move_down)
apply (drule_tac x = n in spec)
apply auto[1]
apply (drule_tac x = y in spec)
apply (drule move_down)
apply (drule_tac x = n in spec)
by auto[1]
show "sts2qltl (prod_pred ⊤ ⊤) (rel_prod_sts (λ(u::unit, x) (v::unit, y). r x y) (λ(u::unit, x) (v::unit, y). r' x y)) =
sts2qltl ⊤ (λ(u::unit, x) (v::unit, y). (case x of (x, x') ⇒ λ(y, y'). r x y ∧ r' x' y') y)"
by (simp add: sts2qltl_def fun_eq_iff rel_prod_sts_def)
qed
theorem stateless_parallel: "stateless_sts r *** stateless_sts r' = stateless_sts (λ (x,x') (y,y') . r x y ∧ r' x' y')"
proof (simp add: parallel_component_def stateless_parallel_a)
have "[- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
([- (x, x') ↝ x || x' -] ∘ stateless_sts (λ(x, x') (y, y'). r x y ∧ r' x' y') ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]) ∘
[- (x, y) ↝ x || y -] =
([- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
[- (x, x') ↝ x || x' -]) ∘ stateless_sts (λ(x, x') (y, y'). r x y ∧ r' x' y') ∘ ([- y ↝ (fst ∘ y, snd ∘ y) -] ∘
[- (x, y) ↝ x || y -])"
by (simp add: comp_assoc)
also have "... = stateless_sts (λ(x, x') (y, y'). r x y ∧ r' x' y')"
by (simp add: split_nzip update_id_Skip)
finally show "[- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
([- (x, x') ↝ x || x' -] ∘ stateless_sts (λ(x, x') (y, y'). r x y ∧ r' x' y') ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]) ∘
[- (x, y) ↝ x || y -] = stateless_sts (λ(x, x') (y, y'). r x y ∧ r' x' y')"
by simp
qed
text{*Theorem 9 for Equation 21.*}
theorem det_parallel_a: "(det_sts s0 p state out) ** (det_sts s0' p' state' out')
= [- (x, x') ↝ x || x' -] ∘ det_sts (s0, s0') (prec_prod_sts p p') (λ ((s,s'), (x,x') ) . (state (s,x), state' (s',x')) )
(λ ((s,s'), (x,x') ) . (out (s,x), out' (s',x')) ) o [- y ↝ (fst ∘ y, snd ∘ y) -]"
proof -
have [simp]: "(prod_pred (λs. s = s0) (λs. s = s0')) = (λs. s = (s0, s0'))"
by (simp add: prod_pred_def fun_eq_iff)
have [simp]: "(rel_prod_sts (λ(s, x) ab. p (s, x) ∧ (case ab of (s', y) ⇒ s' = state (s, x) ∧ y = out (s, x)))
(λ(s, x) ab. p' (s, x) ∧ (case ab of (s', y) ⇒ s' = state' (s, x) ∧ y = out' (s, x))))
= (λ(s, x) ab. prec_prod_sts p p' (s, x) ∧ (case ab of
(s', y) ⇒ s' = (case s of (s, s') ⇒ λ(x, x'). (state (s, x), state' (s', x'))) x ∧ y = (case s of (s, s') ⇒ λ(x, x'). (out (s, x), out' (s', x'))) x))"
by (simp add: prec_prod_sts_def fun_eq_iff rel_prod_sts_def, auto)
show ?thesis
by (simp add: det_sts_def sts_parallel_a)
qed
theorem det_parallel: "(det_sts s0 p state out) *** (det_sts s0' p' state' out')
= det_sts (s0, s0') (prec_prod_sts p p') (λ ((s,s'), (x,x') ) . (state (s,x), state' (s',x')) )
(λ ((s,s'), (x,x') ) . (out (s,x), out' (s',x')) )"
proof (simp add: parallel_component_def det_parallel_a)
have "[- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
([- (x, x') ↝ x || x' -] ∘
det_sts (s0, s0') (prec_prod_sts p p') (λ((s, s'), x, x'). (state (s, x), state' (s', x')))
(λ((s, s'), x, x'). (out (s, x), out' (s', x'))) ∘
[- y ↝ (fst ∘ y, snd ∘ y) -]) ∘
[- (x, y) ↝ x || y -]
= ([- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
[- (x, x') ↝ x || x' -]) ∘
det_sts (s0, s0') (prec_prod_sts p p') (λ((s, s'), x, x'). (state (s, x), state' (s', x')))
(λ((s, s'), x, x'). (out (s, x), out' (s', x'))) ∘
([- y ↝ (fst ∘ y, snd ∘ y) -] ∘
[- (x, y) ↝ x || y -])"
by (simp add: comp_assoc)
also have "... = det_sts (s0, s0') (prec_prod_sts p p') (λ((s, s'), x, x'). (state (s, x), state' (s', x')))
(λ((s, s'), x, x'). (out (s, x), out' (s', x')))"
by (simp add: split_nzip update_id_Skip)
finally show "[- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
([- (x, x') ↝ x || x' -] ∘
det_sts (s0, s0') (prec_prod_sts p p') (λ((s, s'), x, x'). (state (s, x), state' (s', x')))
(λ((s, s'), x, x'). (out (s, x), out' (s', x'))) ∘
[- y ↝ (fst ∘ y, snd ∘ y) -]) ∘
[- (x, y) ↝ x || y -] = det_sts (s0, s0') (prec_prod_sts p p') (λ((s, s'), x, x'). (state (s, x), state' (s', x')))
(λ((s, s'), x, x'). (out (s, x), out' (s', x')))"
by simp
qed
text{*Theorem 9 for Equation 22.*}
theorem stateless_det_parallel_a: "stateless_det_sts p out ** stateless_det_sts p' out' =
[- (x, x') ↝ x || x' -] ∘ stateless_det_sts (prod_pred p p') (λ (x,x') . (out x, out' x')) o [- y ↝ (fst ∘ y, snd ∘ y) -]"
apply (simp add: stateless_det2stateless stateless_parallel_a)
apply (subgoal_tac "(λ(x, x') ab. p x ∧ (case ab of (y, y') ⇒ y = out x ∧ p' x' ∧ y' = out' x')) = (λx y. prod_pred p p' x ∧ y = (case x of (x, x') ⇒ (out x, out' x')))")
apply simp
by (simp add: fun_eq_iff prod_pred_def, auto)
theorem stateless_det_parallel: "stateless_det_sts p out *** stateless_det_sts p' out' =
stateless_det_sts (prod_pred p p') (λ (x,x') . (out x, out' x'))"
proof (simp add: parallel_component_def stateless_det_parallel_a)
have " [- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
([- (x, x') ↝ x || x' -] ∘ stateless_det_sts (prod_pred p p') (λ(x, x'). (out x, out' x')) ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]) ∘
[- (x, y) ↝ x || y -]
= ([- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
[- (x, x') ↝ x || x' -]) ∘ stateless_det_sts (prod_pred p p') (λ(x, x'). (out x, out' x')) ∘ ([- y ↝ (fst ∘ y, snd ∘ y) -] ∘
[- (x, y) ↝ x || y -])"
by (simp add: comp_assoc)
also have "... = stateless_det_sts (prod_pred p p') (λ(x, x'). (out x, out' x'))"
by (simp add: split_nzip update_id_Skip)
finally show "[- uv ↝ (fst ∘ uv, snd ∘ uv) -] ∘
([- (x, x') ↝ x || x' -] ∘ stateless_det_sts (prod_pred p p') (λ(x, x'). (out x, out' x')) ∘ [- y ↝ (fst ∘ y, snd ∘ y) -]) ∘
[- (x, y) ↝ x || y -] = stateless_det_sts (prod_pred p p') (λ(x, x'). (out x, out' x'))"
by simp
qed
lemmas theorem_9 = qltl_parallel sts_parallel stateless_parallel det_parallel stateless_det_parallel
text{*5.5 Symbolic Computation of Feedback Composition*}
text{*Theorem 10 for Equation 23.*}
theorem det_decomposable_feedback: "Feedback ([- u, x ↝ u || x -] o det_sts s0 p state (λ (s, (u,x)) . (f s x, g u s x) ) o [- uy ↝ fst o uy, snd o uy -])
= det_sts s0 (λ (s,x) . p (s, (f s x, x))) (λ (s,x) . state (s, (f s x, x))) (λ (s,x) . g (f s x) s x)"
proof -
have DelayFeedback_det_sts: "⋀ f g s . det_sts s0 p state (λ (s, (u,x)) . (f s x, g s u x) ) =
DelayFeedback (λs. s = s0) ({. p .} ∘ [- s, u, x ↝ state (s, u, x), f s x, g s u x -])"
apply (simp add: det2LocalSystem update_def DelayFeedback_LocalSystem)
apply (subgoal_tac "(λ (s, x) (s', y) . s' = state (s, x) ∧ y = (case x of (u, x) ⇒ (f s x, g s u x))) =
(λ x y . y = (case x of (s, u, xa) ⇒ (state (s, u, xa), f s xa, g s u xa)))")
apply simp
by (simp add: fun_eq_iff)
have FeedbackB_deterministic_a: "⋀ init a . init = (λ x . x = a) ⟹
DelayFeedback init (feedback({.(u, s, x). p (s, u, x).} ∘ [- u, s, x ↝ f s x, state (s, u, x), g u s x -])) =
Feedback ([- u,x ↝ u || x -] o (DelayFeedback init ({. p .} ∘ [- s, u, x ↝ state (s, u, x), f s x, g u s x -])) o [- z ↝ fst o z, snd o z -])"
apply (cut_tac p = "λ (u,s,x) . p (s, u, x)" and f = f and g = "λ u s x . state (s, u, x)"
and h = "g" and a = a and init = init in Feedback_deterministic, simp_all)
apply (subgoal_tac " ([-s, u, x ↝ u, s, x-] ∘ ({.(u, s, x).p (s, u, x).} ∘ [-u, s, x ↝ f s x, state (s, u, x), g u s x-])∘ [-v, s, y ↝ s, v, y-])
= ({. p .} ∘ [- s, u, x ↝ state (s, u, x), f s x, g u s x-])")
apply simp
by (simp add: fun_eq_iff update_def demonic_def le_fun_def assert_def)
have [simp]: "(λx y. y = (case x of (s, x) ⇒ (state (s, f s x, x), g (f s x) s x)))
= (λ(s, x) (s', y). s' = state (s, f s x, x) ∧ y = g (f s x) s x)"
by auto
show ?thesis
apply (simp add: DelayFeedback_det_sts FeedbackB_deterministic_a [symmetric] feedback_update_simp_c)
by (simp add: update_def DelayFeedback_LocalSystem [symmetric] det2LocalSystem)
qed
theorem det_decomposable_feedback_a: "fdbk (det_sts s0 p state (λ (s, (u,x)) . (f s x, g u s x) ))
= det_sts s0 (λ (s,x) . p (s, (f s x, x))) (λ (s,x) . state (s, (f s x, x))) (λ (s,x) . g (f s x) s x)"
by (simp add: fdbk_def det_decomposable_feedback)
text{*Theorem 10 for Equation 24.*}
theorem stateless_det_decomposable_feedback: "Feedback ([- u, x ↝ u || x -] o stateless_det_sts p (λ (u,x) . (f x, g u x) ) o [- uy ↝ fst o uy, snd o uy -])
= stateless_det_sts (λ x . p (f x, x)) (λ x . g (f x) x)"
proof -
define fa where "fa = (λ (s::unit) x . f x)"
define ga where "ga = (λ u (s::unit) x . g u x)"
have [simp]: "(λ(s, x). case x of (u, x) ⇒ (f x, g u x)) = (λ (s, (u,x)) . (fa s x, ga u s x))"
by (simp add: fun_eq_iff fa_def ga_def)
have [simp]: "(λ(s, x). p (f x, x)) = (λ (s,x) . (λ(s, x). p x) (s, (fa s x, x)))"
by (simp add: fun_eq_iff fa_def ga_def)
have [simp]: "(λ(s, x). g (f x) x) = (λ (s,x) . ga (fa s x) s x)"
by (simp add: fun_eq_iff fa_def ga_def)
show ?thesis
by (simp add: stateless_det_sts_def det_decomposable_feedback)
qed
theorem stateless_det_decomposable_feedback_a: "fdbk (stateless_det_sts p (λ (u,x) . (f x, g u x) ))
= stateless_det_sts (λ x . p (f x, x)) (λ x . g (f x) x)"
by (simp add: fdbk_def stateless_det_decomposable_feedback)
lemmas theorem_10 = det_decomposable_feedback_a stateless_det_decomposable_feedback_a
lemma "Sum_comp = det_sts (0::nat) ⊤ (λ (s, y) . s + y) (λ (s, x) . s)"
by (simp add: Sum_comp_Sum_sts Sum_sts_det)
lemma illegal_sts_top: "illegal_sts init ⊤ = ⊥"
by (simp add: fun_eq_iff illegal_sts_def)
lemma illegal_sts_top_a: "illegal_sts init (λ x . True) = ⊥"
by (simp add: fun_eq_iff illegal_sts_def)
definition "Nondet_sts = sts (λ s . s = (0::nat)) (λ (s, (x,a::unit)) (s', (y,z)) . z = x ∧ y = s ∧ (s' = s ∨ s' = s + 1))"
lemma Nondet_sts_simp: "Nondet_sts = [:xa ↝ yz . snd o yz = fst o xa ∧ (fst o yz) 0 = 0 ∧ (∀ i . fst (yz (Suc i)) = fst (yz i) ∨ fst (yz (Suc i)) = fst (yz i) + 1):]"
proof -
have [simp]: "⋀ xa yz . (∃s. s 0 = 0 ∧ run_sts (λ(s, x, a) (s', y, z). z = x ∧ y = s ∧ (s' = s ∨ s' = Suc s)) s xa yz)
= (snd ∘ yz = fst ∘ xa ∧ fst (yz 0) = 0 ∧ (∀i. fst (yz (Suc i)) = fst (yz i) ∨ fst (yz (Suc i)) = Suc (fst (yz i))))"
apply (simp add: fun_eq_iff run_sts_def, safe)
apply (drule_tac x = x in spec)
apply (simp add: split_def)
apply (simp add: split_def)
apply (simp add: split_def)
apply blast
apply (simp add: split_def)
apply (rule_tac x = "fst o yz" in exI)
by auto
have [simp]: " (inpt (λ(s, x, a) (s', y, z). z = x ∧ y = s ∧ (s' = s ∨ s' = Suc s))) = ⊤"
by (simp add: fun_eq_iff inpt_def, blast)
show ?thesis
by (simp add: Nondet_sts_def sts_def illegal_sts_top assert_true_skip)
qed
lemma "fdbk Nondet_sts = {:x ↝ ((u, y), x').True:} ∘
[: INF x. (λ((u::nat ⇒ nat, y::nat⇒nat), x::nat ⇒ unit) ((y', z), x'::nat ⇒ unit). z = u ∧ y' 0 = 0 ∧ (∀i. y' (Suc i) = y' i ∨ y' (Suc i) = Suc (y' i))) ^^ x OO eqtop (x - Suc 0) :] ∘
[- ((u, y), x) ↝ y -]"
proof -
have [simp]: "[- (u, x) ↝ u || x -] ∘ Nondet_sts ∘ [- uy ↝ (fst ∘ uy, snd ∘ uy) -] =
[:(x, a::nat ⇒ unit) ↝ (y, z) . z = x ∧ y 0 = 0 ∧ (∀ i .y (Suc i) = y i ∨ y (Suc i) = y i + 1):]"
apply (simp add: Nondet_sts_simp demonic_demonic update_def OO_def)
apply (rule_tac f = demonic in arg_cong)
apply (subst (2) fun_eq_iff)
apply (subst (2) fun_eq_iff)
apply safe
apply (simp_all add: split_def)
apply blast
apply (rule_tac x = "aa || a" in exI)
by (simp_all add: split_def nzip_def)
have [simp]: "[- ((u, y::nat ⇒ nat), x) ↝ ((u, x), x::nat⇒unit) -] ∘ [:(u::nat⇒nat, x)↝(v, z).z = u ∧ v 0 = 0 ∧ (∀i. v (Suc i) = v i ∨ v (Suc i) = Suc (v i)):] ** Skip
= [:(u,y), x ↝ (v,z), x' . z = u ∧ v 0 = 0 ∧ (∀i. v (Suc i) = v i ∨ v (Suc i) = Suc (v i)) ∧ x' = x:]"
apply (simp add: Prod_demonic_skip update_def demonic_demonic)
apply (rule_tac f = demonic in arg_cong)
apply (subst fun_eq_iff)
apply (subst fun_eq_iff)
by auto
show ?thesis
by (simp add: fdbk_def Feedback_def IterateOmegaA_demonic)
qed
definition "AND_sts = stateless_det_sts ⊤ (λ (x,y) . (x ∧ y, x ∧ y))"
lemma AND_sts_simp: "AND_sts = [:ux ↝ vy . (∀ i . fst (vy i) = (fst (ux i) ∧ snd (ux i)) ∧ snd (vy i) = (fst (ux i) ∧ snd (ux i))) :]"
proof -
have [simp]: "(inpt (λ(s, x) (s', y). y = (case x of (x, y) ⇒ (x ∧ y, x ∧ y)))) = ⊤"
by (simp add: fun_eq_iff inpt_def)
show ?thesis
apply (simp add: sts_def stateless_det_sts_def det_sts_def illegal_sts_top assert_true_skip AND_sts_def)
apply (rule_tac f = demonic in arg_cong)
apply (simp add: fun_eq_iff run_sts_def)
apply safe
apply (simp_all add: split_def)
apply (case_tac "xa i")
by (drule_tac x = i in spec, simp)
qed
lemma AND_power_simp: "n > 0 ⟹ (λ((u::nat ⇒ bool, y::nat ⇒ bool), x::nat ⇒ bool) ((v, z), x'). (∀i. v i = (u i ∧ x i) ∧ z i = (u i ∧ x i)) ∧ x' = x) ^^ n
= (λ((u, y::nat ⇒ bool), x) ((v, z), x'). (∀i. v i = (u i ∧ x i) ∧ z i = (u i ∧ x i)) ∧ x' = x)"
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
show ?case
apply (case_tac "n = 0")
apply (simp add: OO_def fun_eq_iff)
apply simp
apply (simp add: Suc(1))
apply (simp add: OO_def fun_eq_iff)
apply safe
apply simp_all
by blast
qed
lemma fdbk_AND_sts: "fdbk AND_sts = {:x ↝ u, x' . x = x':} ∘ [: u, x ↝ z. (∀i. z i = (u i ∧ x i)) :]"
proof -
have [simp]: "[- (x, y) ↝ x || y -] ∘ AND_sts ∘ [- uy ↝ (fst ∘ uy, snd ∘ uy) -] =
[:(u, x) ↝ (v, y) . (∀ i . v i = (u i ∧ x i) ∧ y i = (u i ∧ x i)):]"
apply (simp add: AND_sts_simp demonic_demonic update_def OO_def)
apply (rule_tac f = demonic in arg_cong)
apply (subst fun_eq_iff)
apply (subst fun_eq_iff)
apply safe
apply (simp_all add: split_def nzip_def)
apply (rule_tac x = "aa || ba" in exI)
by (simp_all add: split_def nzip_def)
have [simp]: "([- ((u, y), x) ↝ ((u, x), x) -] ∘ [:(u, x)↝(v, y).∀i. v i = (u i ∧ x i) ∧ y i = (u i ∧ x i):] ** Skip)
= [:(u, y::nat ⇒ bool), x ↝ (v, z), x' . (∀ i . v i = (u i ∧ x i) ∧ z i = (u i ∧ x i)) ∧ x' = x:]"
apply (simp add: Prod_demonic_skip update_def demonic_demonic)
apply (rule_tac f = demonic in arg_cong)
apply (simp add: fun_eq_iff)
by auto
have [simp]: "⋀ n . (λ((u::nat ⇒ bool, y::nat ⇒ bool), x) ((v, z), x'). (∀i. v i = (u i ∧ x i) ∧ z i = (u i ∧ x i)) ∧ x' = x) ^^ n OO eqtop (n - Suc 0)
= (λ((u, y::nat ⇒ bool), x) ((v, z), x'). (∀i. v i = (u i ∧ x i) ∧ z i = (u i ∧ x i)) ∧ x' = x) OO eqtop (n - Suc 0)"
apply (case_tac "n > 0")
apply (simp add: AND_power_simp)
apply (simp add: fun_eq_iff OO_def)
apply safe
apply (rule_tac x = "λ i . (a i ∧ b i)" in exI, simp)
apply (rule_tac x = "λ i . (a i ∧ b i)" in exI, simp)
by (rule_tac x = "λ i . ( b i)" in exI, simp)
have [simp]: "(INF n. (λ((u::nat ⇒ bool, y::nat ⇒ bool), x) ((v, z), x'). (∀i. v i = (u i ∧ x i) ∧ z i = (u i ∧ x i)) ∧ x' = x) OO eqtop (n - Suc 0))
= (λ((u, y::nat ⇒ bool), x) ((v, z), x'). (∀i. v i = (u i ∧ x i) ∧ z i = (u i ∧ x i)) ∧ x' = x)"
apply (simp add: fun_eq_iff OO_def eqtop_prod_def , safe)
apply (drule_tac x = "Suc (Suc i)" in spec, simp, safe, simp)
apply blast
apply (drule_tac x = "Suc (Suc i)" in spec, simp, safe, simp)
apply blast
apply (drule_tac x = "Suc (Suc i)" in spec, simp, safe, simp)
apply blast
apply (drule_tac x = "Suc (Suc i)" in spec, simp, safe, simp)
apply blast
apply (drule_tac x = "Suc (Suc i)" in spec, simp, safe, simp)
apply blast
apply (drule_tac x = "Suc (Suc i)" in spec, simp, safe, simp)
apply blast
apply (drule_tac x = "Suc (Suc x)" in spec, simp, safe, simp)
apply (drule_tac x = "Suc (Suc x)" in spec, simp, safe, simp)
by blast
have [simp]: "[: (λ((u, y::nat ⇒ bool), x) ((v, z), x'). (∀i. v i = (u i ∧ x i) ∧ z i = (u i ∧ x i)) ∧ x' = x) :] ∘
[- ((u, y), x) ↝ y -]
= [: ((u::nat ⇒ bool, y::nat ⇒ bool), x) ↝ z. (∀i. z i = (u i ∧ x i)) :]"
apply (simp add: update_def demonic_demonic)
apply (rule_tac f = demonic in arg_cong)
by (simp add: fun_eq_iff OO_def, blast)
have [simp]: "{:x ↝ ((u, y), x').x = x':} ∘[: ((u::nat ⇒ bool, y::nat ⇒ bool), x) ↝ z. (∀i. z i = (u i ∧ x i)) :]
= {:x ↝ (u, x').x = x':} ∘[: (u::nat ⇒ bool, x) ↝ z. (∀i. z i = (u i ∧ x i)) :]"
by (simp add: fun_eq_iff demonic_def angelic_def)
show ?thesis
apply (simp add: fdbk_def Feedback_def IterateOmegaA_demonic)
by (simp add: comp_assoc)
qed
lemma False_fdbk_AND_sts: "[-x ↝ ⊥-] o fdbk AND_sts = [-x ↝ ⊥-]"
apply (simp add: fdbk_AND_sts)
apply (simp add: update_def angelic_def fun_eq_iff demonic_def le_fun_def)
apply safe
apply blast
apply blast
apply (rule_tac x = "xa" in exI, simp, safe)
apply (rule_tac x = "xa" in exI, simp)
by blast
subsubsection{*Section 5.8: Checking Validity*}
text{*Theorem 12 for QLTL components.*}
theorem theorem_12_qltl_a: "({:r:] = Fail) = (r = ⊥)"
by (simp add: fun_eq_iff trs_def Fail_def demonic_def assert_def inpt_def le_fun_def, auto)
theorem theorem_12_qltl: "(qltl r = Fail) = (r = ⊥)"
by (simp add: qltl_def theorem_12_qltl_a)
text{*Theorem 12 for stateless STS components.*}
theorem theorem_12_stateless_sts: "(stateless_sts r = Fail) = (r = ⊥)"
apply (simp add: theorem_7_stateless_sts theorem_12_qltl_a qltl_def)
by (simp add: fun_eq_iff always_def at_fun_def, auto)
lemmas theorem_12 = theorem_12_qltl theorem_12_stateless_sts
text{*Legal inputs*}
text{*Theorem 13 for Equation 25.*}
thm legal_qltl
text{*Theorem 13 for Equation 26.*}
lemma legal_sts: "init a ⟹ legal (sts init r) = prec_pre_sts init (inpt r) r"
by (simp add: sts_LocalSystem LocalSystem_simp legal_prec)
text{*Theorem 13 for Equation 27.*}
lemma legal_stateless: "legal (stateless_sts r) = (□ (λx . inpt r (x (0::nat))))"
apply (simp add: theorem_7_stateless_sts trs_def legal_prec qltl_def)
apply (simp add: fun_eq_iff inpt_def always_def at_fun_def)
apply safe
apply blast
by (simp add: choice_iff)
text{*Theorem 13 for Equation 28.*}
lemma legal_det: "legal (det_sts s0 p state out) =
prec_pre_sts (λs. s = s0) p (λ(s, x) (s', y). (s' = state (s, x) ∧ y = out (s, x)))"
proof -
have A: "(inpt (λ(s, x) (s', y). p (s, x) ∧ (s' = state (s, x) ∧ y = out (s, x)))) = p"
by (simp add: fun_eq_iff inpt_def)
have "legal (det_sts s0 p state out) =
prec_pre_sts (λs. s = s0) (inpt (λ(s, x) (s', y). p (s, x) ∧ (s' = state (s, x) ∧ y = out (s, x))))
(λ(s, x) (s', y). p (s, x) ∧ (s' = state (s, x) ∧ y = out (s, x)))"
by (simp add: det_sts_def legal_sts)
also have "... = prec_pre_sts (λs. s = s0) p
(λ(s, x) (s', y). p (s, x) ∧ (s' = state (s, x) ∧ y = out (s, x)))"
by (subst A, simp)
also have "... = prec_pre_sts (λs. s = s0) p
(λ(s, x) (s', y). (s' = state (s, x) ∧ y = out (s, x)))"
apply (rule prec_pre_sts_prec_rel)
by (simp add: inpt_def)
finally show ?thesis
by simp
qed
text{*Theorem 13 for Equation 29.*}
lemma legal_stateless_det: "legal (stateless_det_sts p out) = □ (λ x . p (x 0))"
apply (simp add: stateless_det2stateless legal_stateless)
by (simp add: fun_eq_iff always_def inpt_def at_fun_def)
lemmas theorem_13 = legal_qltl legal_sts legal_det legal_stateless legal_stateless_det
subsubsection{*Section 5.10: Checking Refinement Symbolically*}
lemma refinement_LocalSystem: "init' ≤ init ⟹ p ≤ p' ⟹ (⋀ x . p x ⟹ r' x ≤ r x) ⟹ LocalSystem init p r ≤ LocalSystem init' p' r'"
apply (simp add: DelayFeedback_LocalSystem [symmetric])
apply (rule DelayFeedback_refinement, simp_all)
by (simp add: assert_demonic_refinement)
text{*Theorem 14 for STS components.*}
theorem refinement_sts: "init' ≤ init ⟹ inpt r ≤ inpt r' ⟹ (⋀ x . inpt r x ⟹ r' x ≤ r x) ⟹ sts init r ≤ sts init' r'"
by (simp add: sts_LocalSystem refinement_LocalSystem)
text{*Theorem 14 for stateless STS components.*}
theorem refinement_stateless: "(stateless_sts r ≤ stateless_sts r') = ((inpt r ≤ inpt r') ∧ ((∀ x . inpt r x ⟶ r' x ≤ r x)))"
proof -
have [simp]: "(□ (λx. inpt r (x 0)) ≤ □ (λx. inpt r' (x (0::nat)))) = (inpt r ≤ inpt r')"
apply (simp add: le_fun_def always_def at_fun_def)
apply safe
apply (drule_tac x = "λ i . x" in spec, simp)
by simp
have [simp]: "(∀x. (□ (λx. inpt r (x 0))) x ⟶ (□ (λx y. r' (x (0::nat)) (y (0::nat)))) x ≤ (□ (λx y. r (x 0) (y 0))) x)
= (∀ x . inpt r x ⟶ r' x ≤ r x)"
apply (simp add: always_def fun_eq_iff at_fun_def le_fun_def, safe, simp_all)
apply (drule_tac x = "λ i . x" in spec, simp)
by (drule_tac x = "λ i . xa" in spec, simp)
show "stateless_sts r ≤ stateless_sts r' = ((inpt r ≤ inpt r') ∧ ((∀ x . inpt r x ⟶ r' x ≤ r x)))"
apply (simp add: stateless_sts_simp)
by (simp add: assert_demonic_refinement)
qed
text{*Theorem 14 for QLTL components.*}
theorem refinement_qltl_a: "({:r:] ≤ {:r':]) = ((∀ x . inpt r x ⟶ inpt r' x) ∧ (∀ x y . inpt r x ∧ r' x y ⟶ r x y))"
by (simp add: trs_def le_fun_def demonic_def assert_def, blast)
theorem refinement_qltl: "(qltl r ≤ qltl r') = ((∀ x . inpt r x ⟶ inpt r' x) ∧ (∀ x y . inpt r x ∧ r' x y ⟶ r x y))"
by (simp add: qltl_def refinement_qltl_a)
lemmas theorem_14 = refinement_sts refinement_stateless refinement_qltl
text{*Data refinement*}
text{*Theorem 15.*}
theorem theorem_15:
assumes A: "(⋀ t . init' t ⟹ ∃ s . d t s ∧ init s)"
and B: "⋀ t x s. d t s ⟹ inpt r (s, x) ⟹ inpt r' (t, x)"
and C: "⋀ t x s t' y. d t s ⟹ inpt r (s, x) ⟹ r' (t, x) (t', y) ⟹ (∃s'. d t' s' ∧ r (s, x) (s', y))"
shows "sts init r ≤ sts init' r'"
apply (simp add: sts_LocalSystem)
apply (rule data_refinement_sts)
apply (rule A, simp)
using B C by (simp add: data_refin_sts_simp, auto)
text{*Example of stateless sts refinement*}
lemma "stateless_sts (λ x y . x ≥ 0 ∧ y ≥ (x::nat)) ≤ stateless_sts (λ x y . x ≤ y ∧ y ≤ x + 10)"
apply (unfold refinement_stateless inpt_def)
by auto
subsubsection{*Proof of refinement for the Oven example*}
datatype oven_state = on | off
definition "oven_trs = (λ ((s::nat,sw), x::unit) ((s',sw'),t) . (t = s) ∧
(if sw = on then s < s' ∧ s' < s + 5 else (if s > 10 then s - 5 < s' ∧ s' < s else s' = s)) ∧
(if sw = on ∧ s > 210 then sw' = off else
(if sw = off ∧ s < 190 then sw' = on else sw' = sw)) )"
definition "oven_init = (λ (s, sw) . s = (20::nat) ∧ sw = on)"
lemma oven_refinement: "Oven_qltl ≤ sts oven_init oven_trs"
proof -
have [simp]: "inpt oven_trs = ⊤"
apply (auto simp add: inpt_def oven_trs_def fun_eq_iff)
by (rule_tac x = "if b = on then Suc a else (if a > 10 then a - 1 else a)" in exI, auto)
have [simp]: "inpt (λ x t . oven t) = ⊤"
apply (simp add: inpt_def fun_eq_iff oven_def)
apply (rule_tac x = "λ n . if n = 0 then 20 else 190" in exI)
apply (simp add: until_def thermostat_def at_fun_def always_def LTL_def)
by (rule_tac x = "Suc 0" in exI, auto)
have [simp]: "[: λx. oven :] ≤ [: rel_pre_sts oven_init oven_trs :]"
proof (rule demonic_refinement, safe, simp add: rel_pre_sts_simp, safe)
fix x y u
assume A: "oven_init (u (0::nat))"
assume B: "∀i. oven_trs (u i, ()) (u (Suc i), y i)"
define s where "s = fst o u"
define sw where "sw = snd o u"
have C: "u = s || sw"
by (simp add: s_def sw_def nzip_def)
from this and A have [simp]: "s 0 = 20" and [simp]: "sw 0 = on"
by (simp_all add: oven_init_def nzip_def)
from B and C have D: "⋀ n . oven_trs ((s n, sw n), ()) ((s (Suc n), sw (Suc n)), y n)"
by (simp add: always_def at_fun_def nzip_def)
from D have [simp]: "y = s "
and a: "⋀ n . sw n = on ⟹ s n < s (Suc n) ∧ s (Suc n) < s n + 5"
and b: "⋀ n . sw n = off ⟹ 10 < s n ⟹ s n - 5 < s (Suc n) ∧ s (Suc n) < s n"
and c: "⋀ n . sw n = off ⟹ 10 ≥ s n ⟹ s (Suc n) = s n"
and d: "⋀ n . sw n = on ∧ 210 < s n ⟹ sw (Suc n) = off"
and e: "⋀ n . 210 ≥ s n ∧ sw n = off ∧ s n < 190 ⟹ sw (Suc n) = on"
and f: "⋀ n. (sw n = off ∨ 210 ≥ s n) ∧ (sw n = on ∨ s n ≥ 190) ⟹ sw (Suc n) = sw n"
by (auto simp add: oven_trs_def)
have D: "⋀ n . s n < 180 ∧ sw n = on ⟹ s n < s (Suc n) ∧ s (Suc n) < s n + 5 ∧ sw (Suc n) = on"
by (simp add: a f)
have E: "⋀ a . ∃ k . (∀ i < k . sw i = on ∧ s i < 180 ∧ s i < s (Suc i))
∧ (20 ≤ a ∧ a ≤ 180 ⟶ a ≤ s k ∧ s k < a + 4)"
proof -
fix a
show " ∃k. (∀i<k. sw i = on ∧ s i < 180 ∧ s i < s (Suc i)) ∧ (20 ≤ a ∧ a ≤ 180 ⟶ a ≤ s k ∧ s k < a + 4)"
proof (induction a)
case 0
then show ?case
apply simp
by (rule_tac x = 0 in exI, simp)
next
case (Suc a)
from this obtain k where
[simp]: "⋀ i . i<k ⟹ sw i = on" "⋀ i . i<k ⟹ s i < 180"
"⋀ i . i<k ⟹ s i < s (Suc i)"
and A: "20 ≤ a ⟹ a ≤ 180 ⟹ a ≤ s k ∧ s k < a + 4"
by blast
show ?case
apply (case_tac "Suc a > 180")
using Suc apply auto [1]
apply simp
apply (case_tac "a = 19", simp_all)
apply (rule_tac x = 0 in exI, simp_all)
apply (case_tac "a < s k")
apply (rule_tac x = k in exI)
apply simp
using A apply linarith
apply (case_tac "a = s k", simp_all)
apply (rule_tac x = "Suc k" in exI, safe)
apply (case_tac "i < k", simp_all)
using D less_Suc_eq_0_disj apply auto[1]
apply (metis Suc_le_lessD Suc_numeral ‹⋀i. i < k ⟹ s i < 180› less_antisym not_less semiring_norm(5) semiring_norm(8))
apply (metis D ‹⋀i. i < k ⟹ s i < 180› ‹⋀i. i < k ⟹ sw i = on› ‹sw 0 = on› a less_Suc_eq_0_disj)
apply (metis D Suc_leI ‹⋀i. i < k ⟹ s i < 180› ‹⋀i. i < k ⟹ sw i = on› ‹sw 0 = on› a lessI less_Suc_eq_0_disj)
using D [of k] apply simp
apply (metis (full_types) add.commute add.right_neutral b c nat_add_left_cancel_less not_less oven_state.exhaust trans_less_add2 zero_less_numeral)
using A ‹⋀i. i < k ⟹ s i < s (Suc i)› by auto[1]
qed
qed
have "∃ n . (∀i < n. sw i = on ∧ s i < 180 ∧ s i < s (Suc i)) ∧ s n ≥ 180 ∧ s n < 184"
by (cut_tac E[of 180], simp)
from this obtain n where U: "(∀i < n. sw i = on ∧ s i < 180 ∧ s i < s (Suc i)) ∧ s n ≥ 180 ∧ s n < 184"
by blast
have [simp]: "sw n = on"
using U
by (metis D ‹sw 0 = on› lessI less_Suc_eq_0_disj)
have K: "∀ k . (sw (n + k) = on ⟶ 180 ≤ s (n + k) ∧ s (n + k) ≤ 214)
∧ (sw (n + k) = off ⟶ 186 ≤ s (n + k) ∧ s (n + k) ≤ 220)"
proof
fix k
show "(sw (n + k) = on ⟶ 180 ≤ s (n + k) ∧ s (n + k) ≤ 214) ∧
(sw (n + k) = off ⟶ 186 ≤ s (n + k) ∧ s (n + k) ≤ 220)"
proof (induction k)
case 0
then show ?case
using U by simp
next
case (Suc k)
have A: "sw (n + k) = on ⟹ 180 ≤ s (n + k) ∧ s (n + k) ≤ 214"
using Suc by blast
have B: "sw (n + k) = off ⟹ 186 ≤ s (n + k) ∧ s (n + k) ≤ 220"
using Suc by blast
have W:"sw (Suc (n + k)) = on ⟹ sw (n + k) = on ⟹ 180 ≤ s (Suc (n + k)) ∧ s (Suc (n + k)) ≤ 214"
using A apply (frule_tac a[of "n+k"], simp, safe, simp, safe)
apply (case_tac "s (n+k) ≤ 210")
apply (subgoal_tac " s (n + k) + 5 ≤ 215", simp_all)
by (cut_tac d [of "n + k"], simp_all)
have X: "sw (Suc (n + k)) = on ⟹ sw (n + k) = off ⟹ 180 ≤ s (Suc (n + k)) ∧ s (Suc (n + k)) ≤ 214"
apply (frule B, clarsimp)
apply (frule b, simp_all, clarsimp)
apply safe
apply (rule_tac y = "s (n + k) - 4" in order_trans, simp_all)
apply (case_tac "s (Suc (n + k)) > 214")
by (cut_tac f [of "n + k"], simp_all)
have Y: "sw (Suc (n + k)) = off ⟹ sw (n + k) = on ⟹ 186 ≤ s (Suc (n + k)) ∧ s (Suc (n + k)) ≤ 220"
apply (frule A, clarsimp)
apply (frule a, clarsimp)
apply (case_tac "186 > s (Suc (n + k))")
by (cut_tac f [of "n + k"], simp_all)
have Z: "sw (Suc (n + k)) = off ⟹ sw (n + k) = off ⟹ 186 ≤ s (Suc (n + k)) ∧ s (Suc (n + k)) ≤ 220"
apply (frule B, clarsimp)
apply (frule b, clarsimp, clarsimp)
apply (case_tac "s (n + k) < 190")
by (cut_tac e [of "n +k"], simp_all)
show ?case
apply (case_tac "sw (Suc (n + k))", simp_all)
apply (case_tac "sw (n + k)")
using W apply simp
using X apply simp
apply (case_tac "sw (n + k)")
using Y apply simp
using Z by simp
qed
qed
from this have [simp]: "thermostat (s[n ..])"
apply (simp add: thermostat_def always_def at_fun_def LTL_def, clarify)
by (case_tac "sw (n + f)", auto)
show "oven y"
apply (simp add: oven_def)
apply (simp add: until_def at_fun_def LTL_def)
apply (rule_tac x = n in exI, simp)
using U by simp
qed
show ?thesis
by (simp add: Oven_qltl_def trs_inpt_top sts_inpt_top)
qed
end