section‹\label{sec_Temporal}Linear Temporal Logic›
theory Temporal imports Main
begin
text‹
In this section we introduce an algebraic axiomatization of Linear Temporal Logic (LTL).
We model LTL formulas semantically as predicates on traces. For example the LTL formula
$\alpha = \Box\; \diamondsuit\; (x = 1)$ is modeled as a predicate
$\alpha : (nat \Rightarrow nat) \Rightarrow bool$, where
$\alpha \;x = True$ if $x\;i=1$ for infinitely many $i:nat$. In this formula $\Box$
and $\diamondsuit$ denote the always and eventually operators, respectively.
Formulas with multiple variables are modeled similarly. For example a formula $\alpha$ in two
variables is modeled as $\alpha : (nat \Rightarrow \tv a) \Rightarrow (nat \Rightarrow \tv b) \Rightarrow bool$,
and for example $(\Box\; \alpha) \; x\; y$ is defined as $(\forall i . \alpha \; x[i..]\; y[i..])$,
where $x[i..]\;j = x\;(i+j)$. We would like to construct an algebraic structure (Isabelle class)
which has the temporal operators as operations, and which has instatiations to
$(nat \Rightarrow \tv a) \Rightarrow bool$, $(nat \Rightarrow \tv a) \Rightarrow (nat \Rightarrow \tv b) \Rightarrow bool$,
and so on. Ideally our structure should be such that if we have this structure on a type $\tv a::temporal$,
then we could extend it to $(nat \Rightarrow \tv b) \Rightarrow \tv a$ in a way similar to the
way Boolean algebras are extended from a type $\tv a::boolean\_algebra$ to $\tv b\Rightarrow \tv a$.
Unfortunately, if we use for example $\Box$ as primitive operation on our temporal structure,
then we cannot extend $\Box$ from $\tv a::temporal$ to $(nat \Rightarrow \tv b) \Rightarrow \tv a$. A
possible extension of $\Box$ could be
$$(\Box\; \alpha)\;x = \bigwedge_{i:nat} \Box (\alpha\; x[i..]) \mbox{ and } \Box \; b = b$$
where $\alpha: (nat \Rightarrow \tv b) \Rightarrow \tv a$ and $b:bool$. However, if we apply this
definition to $\alpha : (nat \Rightarrow \tv a) \Rightarrow (nat \Rightarrow \tv b) \Rightarrow bool$,
then we get
$$(\Box\; \alpha) \; x\; y = (\forall i\;j. \alpha \; x[i..]\; y[j..])$$
which is not correct.
To overcome this problem we introduce as a primitive operation $!!:\tv a \Rightarrow nat \Rightarrow \tv a$,
where $\tv a$ is the type of temporal formulas, and $\alpha !! i$ is the formula $\alpha$ at time point $i$.
If $\alpha$ is a formula in two variables as before, then
$$(\alpha !! i)\; x\;y = \alpha\; x[i..]\;y[i..].$$
and we define for example the the operator always by
$$\Box \alpha = \bigwedge_{i:nat} \alpha !! i$$
›
notation
bot ("⊥") and
top ("⊤") and
inf (infixl "⊓" 70)
and sup (infixl "⊔" 65)
class temporal = complete_boolean_algebra + complete_distrib_lattice +
fixes at :: "'a ⇒ nat ⇒ 'a" (infixl "!!" 150)
assumes [simp]: "a !! i !! j = a !! (i + j)"
assumes [simp]: "a !! 0 = a"
assumes [simp]: "-(a !! i) = (-a) !! i"
assumes Inf_at[simp]: "(Inf X) !! i = (INFIMUM X (λ x . at x i))"
begin
lemma [simp]: "⊤ !! i = ⊤"
apply (cut_tac X = "{}" in Inf_at)
by auto
lemma Sup_at: "(Sup X) !! i = (SUPREMUM X (λ x . x !! i))"
apply (subst compl_eq_compl_iff [THEN sym], simp add: uminus_Sup image_def)
by (rule_tac f = Inf in arg_cong, auto)
lemma [simp]: "(a ⊓ b) !! i = (a !! i) ⊓ (b !! i)"
apply (cut_tac X = "{a,b}" in Inf_at)
by auto
lemma [simp]: "(INF x:X. f x) !! i = (INF x:X. f x !! i)"
apply (unfold Inf_at image_def)
by (rule_tac f = Inf in arg_cong, auto)
definition always :: "'a ⇒ 'a" ("□ (_)" [900] 900) where
"□ p = (INF i . p !! i)"
definition eventually_bounded :: "nat set ⇒ 'a ⇒ 'a" ("♢b (_) (_)" [900,900] 900) where
"♢b b p = (SUP i: b . p !! i)"
definition always_bounded :: "nat set ⇒ 'a ⇒ 'a" ("□b (_) (_)" [900,900] 900) where
"□b b p = (INF i: b . p !! i)"
lemma "(□b b p) ⊓ (□b b' p) = (□b (b ∪ b') p)"
apply (simp add: always_bounded_def)
apply (rule antisym, simp_all, auto)
apply (rule_tac INF_greatest, safe)
apply (rule_tac y = "(INF i:b. p !! i)" in order_trans, simp_all)
apply (rule INF_lower, simp)
apply (rule_tac y = "(INF i:b'. p !! i)" in order_trans, simp_all)
apply (rule INF_lower, simp)
apply (rule_tac INF_greatest)
apply (rule INF_lower, simp)
apply (rule_tac INF_greatest)
by (rule INF_lower, simp)
definition eventually :: "'a ⇒ 'a" ("♢ (_)" [900] 900) where
"♢ p = (SUP i . p !! i)"
definition "next" :: "'a ⇒ 'a" ("⨀ (_)" [900] 900) where
"⨀ p = p !! (Suc 0)"
definition until :: "'a ⇒ 'a ⇒ 'a" (infix "until" 65) where
"(p until q) = (SUP n . (INFIMUM {i . i < n} (at p)) ⊓ (q !! n))"
lemma until2: "(p until q) = (SUP n . (INF i : {i . i < n} . p !! i) ⊓ (q !! n))"
by (simp add: until_def)
definition leads :: "'a ⇒ 'a ⇒ 'a" (infix "leads" 65) where
"(p leads q) = -(p until -q)"
lemma leads2: "(p leads q) = (INF n . (SUP i : {i . i < n} . -p !! i) ⊔ (q !! n))"
proof (simp add: leads_def until2 uminus_Sup image_def)
have "{y. ∃x. (∃xa. x = Inf {y. ∃x<xa. y = p !! x} ⊓ (- q) !! xa) ∧ y = - x} = {y. ∃x. y = Sup {y. ∃xa<x. y = (- p) !! xa} ⊔ q !! x}"
proof(auto simp add: uminus_Inf image_def)
fix xaa
have "{y. ∃x. (∃xa<xaa. x = p !! xa) ∧ y = - x} = {y. ∃xa< xaa. y = (- p) !! xa}"
by auto
from this show "∃x. Sup {y. ∃x. (∃xa<xaa. x = p !! xa) ∧ y = - x} ⊔ q !! xaa = Sup {y. ∃xa<x. y = (- p) !! xa} ⊔ q !! x"
by auto
next
fix xa
define x where "x = Inf {y. ∃x<xa. y = p !! x} ⊓ (- q) !! xa"
from this have [simp]: "(∃xa. x = Inf {y. ∃x<xa. y = p !! x} ⊓ (- q) !! xa)"
by auto
have "{y. ∃xaa<xa. y = (- p) !! xaa} = {y. ∃x. (∃xb<xa. x = p !! xb) ∧ y = - x}"
by auto
from this have [simp]: "Sup {y. ∃xaa<xa. y = (- p) !! xaa} ⊔ q !! xa = - x"
by (simp add: x_def uminus_Inf image_def)
have "(∃xa. x = Inf {y. ∃x<xa. y = p !! x} ⊓ (- q) !! xa) ∧ Sup {y. ∃xaa<xa. y = (- p) !! xaa} ⊔ q !! xa = - x"
by simp
from this show " ∃x. (∃xa. x = Inf {y. ∃x<xa. y = p !! x} ⊓ (- q) !! xa) ∧ Sup {y. ∃xaa<xa. y = (- p) !! xaa} ⊔ q !! xa = - x"
by simp
qed
from this show "Inf {y. ∃x. (∃xa. x = Inf {y. ∃x<xa. y = p !! x} ⊓ (- q) !! xa) ∧ y = - x} = Inf {y. ∃x. y = Sup {y. ∃xa<x. y = (- p) !! xa} ⊔ q !! x}"
by simp
qed
definition impl :: "'a ⇒ 'a ⇒ 'a" (infix "impl" 65) where
"(p impl q) = (-p ⊔ q)"
lemma leads3: "(p leads q) = (INF n . (INF i : {i . i < n} . p !! i) impl (q !! n))"
apply (simp add: leads2 impl_def uminus_Inf image_def)
apply (subgoal_tac "⋀ x . {y. ∃xa<x. y = (- p) !! xa} = {y. ∃xa. (∃xb<x. xa = p !! xb) ∧ y = - xa}")
by auto
lemma iterate_next: "(next ^^ n) p = p !! n"
proof (induction n)
show "(next ^^ 0) p = p !! 0" by simp
next
fix n
assume [simp]: "(next ^^ n) p = p !! n"
show "(next ^^ Suc n) p = p !! Suc n"
by (simp add: next_def)
qed
lemma always_next: "□ p = p ⊓ (□ (⨀ p))"
apply (simp add: always_def next_def)
apply (rule antisym, simp_all, safe)
apply (rule_tac x = "p" in Inf_lower)
apply (simp add: image_def, rule_tac x = 0 in exI, simp)
apply (rule INF_greatest, simp)
apply (rule_tac x = "p !! Suc x" in Inf_lower)
apply (simp add: image_def, auto)[1]
apply (rule INF_greatest, simp)
apply (case_tac i, simp_all)
apply (rule_tac y = "(INF x. p !! Suc x)" in order_trans, simp_all)
apply (rule_tac x = "p !! Suc nat" in Inf_lower)
by (auto simp add: image_def)
end
text‹
Next lemma, in the context of complete boolean algebras, will be used
to prove $-(p\ until\ -p) = \Box\; p$.
›
context complete_boolean_algebra
begin
lemma until_always: "(INF n. (SUP i : {i. i < n} . - p i) ⊔ ((p :: nat ⇒ 'a) n)) ≤ p n"
proof -
have "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i:{i. i ≤ n}. p i)"
proof (induction n)
have "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (SUP i:{i. i < 0}. - p i) ⊔ p 0"
by (rule INF_lower, simp)
also have "... ≤ (INF i:{i. i ≤ 0}. p i)"
by simp
finally show "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i:{i. i ≤ 0}. p i)"
by simp
next
fix n::nat assume "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i : {i. i ≤ n}. p i)"
also have "⋀ i . i ≤ n ⟹ ... ≤ p i" by (rule INF_lower, simp)
finally have [simp]: "⋀ i . i ≤ n ⟹ (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ p i"
by simp
show "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i : {i. i ≤ Suc n}. p i)"
proof (rule INF_greatest, safe, cases)
fix i::nat
assume "i ≤ n" from this show "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ p i" by simp
next
fix i::nat
have A: "{i. i ≤ n} = {i . i < Suc n}" by auto
have B: "(SUP i:{i. i ≤ n}. - p i) ≤ - (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n)"
by (metis (lifting, mono_tags) `(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF i:{i. i ≤ n}. p i)` compl_mono uminus_INF)
assume "i ≤ Suc n" and "¬ i ≤ n"
from this have [simp]: "i = Suc n" by simp
have "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ⊓ ((SUP i:{i. i ≤ n}. - p i) ⊔ p (Suc n))"
by (simp add: A, rule INF_lower, simp)
also have "... ≤ ((INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ⊓ ((- (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n)) ⊔ p (Suc n)))"
by (rule inf_mono, simp_all, rule_tac y = "- (INF n. (SUP i:{i. i < n}. - p i) ⊔ p n)" in order_trans, simp_all add: B)
also have "... ≤ p i"
by (simp add: inf_sup_distrib1)
finally show "(INF n. (SUP i:{i. i < n}. - p i) ⊔ p n) ≤ p i" by simp
qed
qed
also have "(INF i:{i. i ≤ n}. p i) ≤ p n" by (rule INF_lower, auto)
finally show "(INF n. (SUP i : {i. i < n} . - p i) ⊔ ((p :: nat ⇒ 'a) n)) ≤ p n" by simp
qed
end
text‹
We prove now a number of results of the temporal class.
›
context temporal
begin
lemma [simp]: "(a ⊔ b) !! i = (a !! i) ⊔ (b !! i)"
by (subst compl_eq_compl_iff [THEN sym], simp)
lemma always_less [simp]: "□ p ≤ p"
proof -
have "□ p ≤ p !! 0"
by (unfold always_def, rule INF_lower, simp)
also have "p !! 0 = p" by simp
finally show "□ p ≤ p" by simp
qed
thm INF_greatest
lemma always_always: "□ □ x = □ x"
apply (rule antisym, simp_all)
apply (auto simp add: le_fun_def always_def)
apply (rule INF_greatest, simp add: image_def)
apply (rule Inf_greatest, simp)
by (rule Inf_lower, auto)
lemma always_and: "□ (p ⊓ q) = (□ p) ⊓ (□ q)"
by (simp add: always_def INF_inf_distrib)
lemma eventually_or: "♢ (p ⊔ q) = (♢ p) ⊔ (♢ q)"
by (simp add: eventually_def SUP_sup_distrib)
lemma neg_until_always: "-(p until -p) = □ p"
proof (rule antisym)
show "- (p until - p) ≤ □ p"
by (simp add: until_def always_def uminus_SUP uminus_INF, rule INF_greatest, cut_tac p = "λ n . p !! n" in until_always, simp)
next
have "⋀ n . □ p ≤ p !! n"
by (simp add: always_def INF_lower)
also have "⋀ n . p !! n ≤ (SUP x:{i. i < n}. (- p) !! x) ⊔ p !! n"
by simp
finally show "□ p ≤ -(p until -p)"
apply (simp add: until_def uminus_SUP uminus_INF)
by (rule INF_greatest, simp)
qed
lemma leads_always: "p leads p = □ p"
by (simp add: neg_until_always leads_def)
lemma neg_always_eventually: "□ p = - ♢ (- p)"
by (simp add: fun_eq_iff always_def eventually_def until_def uminus_SUP)
lemma neg_true_until_always: "-(⊤ until -p) = □ p"
by (simp add: fun_eq_iff always_def until_def uminus_SUP uminus_INF)
lemma top_leads_always: "⊤ leads p = □ p"
by (simp add: neg_true_until_always leads_def)
lemma neg_until_true: "-(p until -⊤) = ⊤"
by (simp add: fun_eq_iff always_def until_def uminus_SUP uminus_INF)
lemma leads_top: "p leads ⊤ = ⊤"
using neg_until_true by (simp add: leads_def)
lemma neg_until_false: "-(p until -⊥) = ⊥"
proof (simp add: fun_eq_iff always_def until_def uminus_SUP uminus_INF)
have "⋀f. (⊥::'a) ∈ range (λn. SUPREMUM {na. (na::nat) < n} f)"
by auto
then have "⋀f. (INF n. SUPREMUM {na. (na::nat) < n} f) ≤ (⊥::'a)"
by (meson local.Inf_lower)
then show "(INF n. SUPREMUM {na. na < n} ((!!) (- p))) = ⊥"
by (simp add: local.le_iff_inf)
qed
lemma leads_bot: "p leads ⊥ = ⊥"
using neg_until_false by (simp add: leads_def)
lemma true_until_eventually: "(⊤ until p) = ♢ p"
by (cut_tac p = "-p" in neg_always_eventually, cut_tac p = "-p" in neg_true_until_always, simp)
end
text‹
Boolean algebras with $b!!i = b$ form a temporal class.
›
instantiation bool :: temporal
begin
definition at_bool_def [simp]: "(p::bool) !! i = p"
instance proof
qed (auto)
end
type_synonym 'a trace = "nat ⇒ 'a"
text‹
Asumming that $\tv a::temporal$ is a type of class $temporal$, and $\tv b$ is an arbitrary type,
we would like to create the instantiation of $\tv b\ trace \Rightarrow \tv a$ as a temporal
class. However Isabelle allows only instatiations of functions from a class to another
class. To solve this problem we introduce a new class called trace with an operation
$\mathit{suffix}::\tv a \Rightarrow nat \Rightarrow \tv a$ where
$\mathit{suffix}\;a\;i\;j = (a[i..])\; j = a\;(i+j)$ when
$a$ is a trace with elements of some type $\tv b$ ($\tv a = nat \Rightarrow \tv b$).
›
class trace =
fixes suffix :: "'a ⇒ nat ⇒ 'a" ("_[_ ..]" [80, 15] 80)
fixes eqtop :: "nat ⇒ 'a ⇒ 'a ⇒ bool"
fixes cat :: "nat ⇒ 'a ⇒ 'a ⇒ 'a"
fixes Cat :: "(nat ⇒ 'a) ⇒ 'a"
assumes suffix_suffix[simp]: "a[i..][j..] = a[i + j..]"
assumes [simp]: "a[0..] = a"
assumes [simp]: "eqtop 0 a b = True"
assumes [simp]: "eqtop n a a = True"
assumes all_eqtop[simp]: "∀ n . eqtop n a b ⟹ a = b"
assumes eqtop_sym: "eqtop n a b = eqtop n b a"
assumes eqtop_tran: "eqtop n a b ⟹ eqtop n b c ⟹ eqtop n a c"
assumes [simp]: "eqtop n (cat n x y) z = eqtop n x z"
assumes cat_at_eq[simp]: "(cat n x y)[n..] = y"
assumes eqtop_Suc: "eqtop (Suc n) x y = (eqtop n x y ∧ eqtop (Suc 0) (x[n..]) (y[n..]))"
assumes Cat_Suc: "Cat u = cat (Suc 0) (u 0) (Cat (λ i . u (Suc i)))"
assumes cat_Suc: "cat (Suc n) x y = cat (Suc 0) x (cat n (x[Suc 0..]) y)"
assumes cat_Zero[simp]: "cat 0 x y = y"
begin
definition "next_trace" :: "'a ⇒ 'a" ("⊙ (_)" [900] 900) where
"⊙ p = p[Suc 0..]"
lemma eq_le[simp]: "⋀ a b . n ≤ m ⟹ eqtop m a b ⟹ eqtop n a b"
apply (induction m, simp)
apply (case_tac "n = Suc m", simp)
apply (subst (asm) eqtop_Suc)
by auto
lemma eqtop_Suc_Cat: "⋀ u . eqtop (Suc 0) ((Cat u)[n..]) (u n)"
proof (induction n)
case 0
then show ?case
apply simp
apply (subst Cat_Suc)
by simp
next
case (Suc n)
have "(cat (Suc 0) (u 0) (Cat (λi. u (Suc i)))[Suc n ..]) = (cat (Suc 0) (u 0) (Cat (λi. u (Suc i)))[Suc 0 ..][n..])"
by (simp del: cat_at_eq)
also have "... = Cat (λi. u (Suc i))[n ..]"
by simp
finally have [simp]: "(cat (Suc 0) (u 0) (Cat (λi. u (Suc i)))[Suc n ..]) = Cat (λi. u (Suc i))[n ..]"
by simp
show ?case
apply (subst Cat_Suc, simp)
by (rule Suc)
qed
lemma eqtop_tail_eqtop: "eqtop n x y ⟹ x[n ..] = y[n ..] ⟹ eqtop na x y"
apply (case_tac "na ≤ n", simp_all)
apply (induction na, simp_all)
apply (subst eqtop_Suc)
apply (case_tac "n = na", simp_all)
apply (cut_tac i = n and j = "na - n" and a = x in suffix_suffix)
apply (simp del: suffix_suffix)
by simp
lemma [simp]: "eqtop n z (cat n x y) = eqtop n z x"
by (subst eqtop_sym, simp, subst eqtop_sym, simp)
lemma eqtop_tail: "eqtop n x y ⟹ x[n..] = y[n..] ⟹ x = y"
apply (rule all_eqtop, safe)
by (rule eqtop_tail_eqtop, simp_all)
definition "cons x = cat (Suc 0) x x"
lemma [simp]: "(cons a)[Suc 0..] = a"
by (simp add: cons_def)
lemma [simp]: "eqtop 0 = ⊤"
by (simp add: fun_eq_iff)
lemma [simp]: "eqtop n x (cat n x y)"
by (subst eqtop_sym, simp)
lemma [simp]: "∃y. x = y[Suc 0 ..]"
by (rule_tac x = "cons x" in exI, simp)
lemma eqtop_plus: "⋀ x y . (eqtop n x y ∧ (eqtop m (x[n..]) (y[n..]))) = eqtop (n + m) x y"
apply (induction m, simp)
apply (subst eqtop_Suc)
apply simp
apply (subst (2) eqtop_Suc)
by auto
lemma [simp]: "cat n (cat n x y) z = cat n x z"
by (rule_tac n = n in eqtop_tail, simp_all)
lemma [simp]: "cat n x (x[n..]) = x"
by (rule_tac n = n in eqtop_tail, simp_all)
lemma eqtop_Suc_a: "eqtop (Suc n) x y = (eqtop (Suc 0) x y ∧ eqtop n (x[Suc 0 ..]) (y[Suc 0 ..]))"
by (cut_tac n = "Suc 0" and m = "n" in eqtop_plus, auto)
lemma cat_Suc_b: "⋀ x y . cat (Suc n) x y = cat n x (cat (Suc 0) (x[n..]) y)"
apply (induction n, simp_all)
apply (subst cat_Suc)
apply simp
apply (subst cat_Suc[THEN sym])
by simp
lemma cat_at: "⋀ i x y . i ≤ n ⟹ (cat n x y[i..]) = cat (n - i) (x[i..]) y"
proof (induction n)
case 0
then show ?case
by simp
next
case (Suc n)
then show ?case
apply (case_tac "i = Suc n", simp_all)
apply (subst cat_Suc_b)
apply (case_tac "i ≤ n", simp_all)
apply (subgoal_tac "x[n ..] = x[i..][n-i..]")
apply (simp del: suffix_suffix add: cat_Suc_b[THEN sym])
apply simp_all
apply (subgoal_tac "(Suc (n - i)) = Suc n - i")
by auto
qed
lemma eqtop_cat_le: "⋀ m x y z . m ≤ n ⟹ eqtop m (cat n x y) z = eqtop m x z"
proof (induction n)
case 0
then show ?case
by simp
next
case (Suc n)
then show ?case
apply (case_tac "m = Suc n")
apply simp
apply (subst cat_Suc_b)
by (subst Suc, simp_all)
qed
lemma eqtop_cat_aux: "i < n ⟹ eqtop (Suc 0) (cat n x y[i..]) (x[i..])"
by (simp add: cat_at eqtop_cat_le)
end
instantiation "prod" :: (trace, trace) trace
begin
definition at_prod_def: "x[i..] ≡ ((fst x)[i..], (snd x)[i..])"
definition eqtop_prod_def: "eqtop n x y ≡ eqtop n (fst x) (fst y) ∧ eqtop n (snd x) (snd y)"
definition cat_prod_def: "cat n x y ≡ (cat n (fst x) (fst y), cat n (snd x) (snd y))"
definition Cat_prod_def: "Cat u ≡ (Cat (fst o u), Cat (snd o u))"
instance proof
fix n:: nat fix a b c:: "'a × 'b"
assume "eqtop n a b" and " eqtop n b c"
from this show "eqtop n a c"
apply (simp add: eqtop_prod_def, safe)
apply (rule_tac b = "fst b" in eqtop_tran, simp_all)
by (rule_tac b = "snd b" in eqtop_tran, simp_all)
next
fix n:: nat fix x y:: "'a × 'b"
show "cat (Suc n) x y = cat (Suc 0) x (cat n (x[Suc 0..]) y)"
apply (simp add: cat_prod_def at_prod_def)
apply (subst cat_Suc)
apply simp
apply (subst cat_Suc)
by simp
next
qed (auto simp add: at_prod_def eqtop_prod_def all_conj_distrib cat_prod_def Cat_prod_def, simp_all add: eqtop_sym eqtop_tail,
metis eqtop_Suc, metis eqtop_Suc, metis eqtop_Suc, metis eqtop_Suc, metis eqtop_Suc, metis eqtop_Suc,
subst Cat_Suc, simp add: comp_def, subst Cat_Suc, simp add: comp_def)
end
instantiation "fun" :: (trace, temporal) temporal
begin
definition at_fun_def: "(P:: 'a ⇒ 'b) !! i = (λ x . (P (x[i..])) !! i)"
lemma aux: "{y. ∃xa. (∃xb∈X. xa = xb (x[i ..])) ∧ y = xa !! i} = {y. ∃xa. (∃x∈X. ∀xb. xa xb = x (xb[i ..]) !! i) ∧ y = xa x}"
by auto
instance proof qed (simp_all add: at_fun_def add.commute fun_eq_iff le_fun_def image_def aux)
end
lemma SUP_Suc: "(SUP x:{i. i < Suc n}. p x) = (SUP x:{i. i < n}. p x) ⊔ ((p n)::'a::complete_lattice)"
apply (rule antisym)
apply (rule SUP_least, safe)
apply (case_tac "x = n", simp_all)
apply (simp add: SUP_upper le_supI1)
apply auto
apply (rule SUP_least, auto)
by (simp_all add: SUP_upper)
definition "top_dep p = (∀ x x' . eqtop (Suc 0) x x' ⟶ p x = p x')"
lemma INF_distrib: "(INF x y. p x ⊔ ((q y)::'a::complete_distrib_lattice)) = (INF x . p x) ⊔ (INF y . q y)"
apply (simp add: sup_INF Inf_sup)
apply (subst (2) INF_commute)
apply (simp add: image_def)
by (rule_tac f = Inf in arg_cong, auto)
lemma top_dep_INF_SUP: "top_dep p ⟹ (INF x. (SUP xa:{i. i < n}. (- p (x[xa ..])) !! xa) ⊔ (- p (x[n ..])) !! n) =
(INF x y. (SUP xa:{i. i < n}. (- p (x[xa ..])) !! xa) ⊔ (- p y) !! n)"
apply (rule antisym)
apply (rule INF_greatest,simp)
apply (rule INF_greatest,simp)
apply (rule_tac y = "(SUP xa:{i. i < n}. (- p ((cat n x y)[xa ..])) !! xa) ⊔ (- p ((cat n x y)[n ..])) !! n" in order_trans)
apply(rule_tac i = "(cat n x y)" in INF_lower, simp_all)
apply (subgoal_tac "⋀ xa . xa < n ⟹ p (cat n x y[xa ..]) = p (x[xa ..])")
apply simp
apply (simp add: top_dep_def)
apply (drule_tac x = "(cat n x y[xa ..])" in spec)
apply (drule_tac x = "(x[xa ..])" in spec)
apply auto
apply (simp add: eqtop_cat_aux)
apply (rule INF_greatest,simp)
apply (rule_tac y = " (INF y. (SUP xa:{i. i < n}. (- p (x[xa ..])) !! xa) ⊔ (- p y) !! n) " in order_trans)
apply(rule_tac i = "x" in INF_lower, simp_all)
apply (rule_tac y = "(SUP xa:{i. i < n}. (- p (x[xa ..])) !! xa) ⊔ (- p (x[n ..])) !! n " in order_trans)
by(rule_tac i = "x[n ..]" in INF_lower, simp_all)
lemma top_dep_all_leadsto_aux: "top_dep p ⟹ (INF b. SUP x:{i. i < n}. (- p (b[x ..])) !! x) ≤ (SUP x:{i. i < n}. INF xa. (- p xa) !! x)"
proof (induction n)
case 0
then show ?case
by simp
next
case (Suc n)
then show ?case
apply (simp add: SUP_Suc)
apply (rule_tac y = "(INF b. SUP x:{i. i < n}. (- p (b[x ..])) !! x) ⊔ (INF xa. (- p xa) !! n)" in order_trans)
apply simp_all
apply (simp add: top_dep_INF_SUP)
apply (simp add: INF_distrib)
by (rule_tac y = "(SUP x:{i. i < n}. INF xa. (- p xa) !! x)" in order_trans, simp_all)
qed
thm INF_SUP
thm SUP_INF
thm SUP_INF_set
theorem top_dep_all_leadsto: "top_dep p ⟹ INFIMUM UNIV (p leads (λ y . q)) = ((SUPREMUM UNIV p) leads q)"
apply (simp add: until_def leads_def)
apply (simp add: until_def uminus_SUP uminus_INF at_fun_def)
apply (rule antisym)
prefer 2
apply (simp add: image_def at_fun_def)
apply (rule Inf_greatest, simp_all, auto)
apply (rule Inf_greatest, simp_all, auto)
apply (simp add: uminus_INF )
apply (simp add: image_def)
apply (rule_tac y = "Sup {y::'b. ∃xa<xc. y = Inf {y::'b. ∃x::'b. (∃xa::'a. x = - p xa) ∧ y = x !! xa}} ⊔ q !! xc" in order_trans)
apply (rule Inf_lower, auto)
apply (rule_tac y = "Sup {y::'b. ∃x::'a ⇒ 'b. (∃xa<xc. x = (λx::'a. p (x[xa ..]) !! xa)) ∧ y = - x xa}" in order_trans, simp_all)
apply(rule Sup_least, auto)
apply (rule_tac y = " - (λx::'a. p (x[xaa ..]) !! xaa) xa" in order_trans)
apply auto
apply (metis (mono_tags, lifting) Inf_lower mem_Collect_eq)
apply (rule Sup_upper, auto)
apply (rule INF_greatest, simp_all)
apply (subst INF_commute)
apply (simp add: image_def)
apply (rule_tac y = "(INF z. (SUP x:{i. i < x}. (- p (z[x ..])) !! x) ⊔ q !! x)" in order_trans)
apply (simp add: image_def)
apply (rule Inf_lower, auto)
apply (rule_tac x ="Inf {y::'a ⇒ 'b. ∃xa<x. y = (λx::'a. p (x[xa ..]) !! xa)} ⊓ (λxa::'a. (- q) !! x)" in exI)
apply auto
apply (simp add: uminus_INF)
apply (simp add: image_def)
apply (rule_tac f = Inf in arg_cong)
apply auto
apply (rule_tac x ="xb" in exI)
apply (subgoal_tac "Sup {y::'b. ∃xa<x. y = (- p (xb[xa ..])) !! xa} = Sup {y::'b. ∃xa::'a ⇒ 'b. (∃xaa<x. xa = (λx::'a. p (x[xaa ..]) !! xaa)) ∧ y = - xa xb}")
apply simp_all
apply (rule_tac f = Sup in arg_cong)
apply auto
apply (rule_tac x ="xb" in exI)
apply (subgoal_tac "Sup {y::'b. ∃xa<x. y = (- p (xb[xa ..])) !! xa} = Sup {y::'b. ∃xa::'a ⇒ 'b. (∃xaa<x. xa = (λx::'a. p (x[xaa ..]) !! xaa)) ∧ y = - xa xb}")
apply auto
apply (rule_tac f = Sup in arg_cong)
apply auto
apply (subst INF_sup [THEN sym], simp)
apply (rule_tac y = "(SUP x:{i. i < x}. INF xa. (- p xa) !! x)" in order_trans)
apply (simp add: top_dep_all_leadsto_aux)
apply (simp add: image_def)
apply (subgoal_tac "Sup {y::'b. ∃xa<x. y = Inf {y::'b. ∃x::'a. y = (- p x) !! xa}} = Sup {y::'b. ∃xa<x. y = Inf {y::'b. ∃x::'b. (∃xa::'a. x = - p xa) ∧ y = x !! xa}}")
apply auto
apply (rule_tac f = Sup in arg_cong)
apply auto
apply (rule_tac x ="xaa" in exI)
apply auto
apply (rule_tac f = Inf in arg_cong)
apply auto
apply (rule_tac x ="xaa" in exI)
apply auto
apply (rule_tac f = Inf in arg_cong)
by auto
lemma INF_SUP_range: "(INF x. SUP xa∈range p. xa !! x) = (INF x. SUP xa. p xa !! x)"
by (metis (mono_tags, lifting) SUP_cong range_composition)
lemma SUP_INF_range: "(SUP x. INF f∈range (λx xa. p (xa[x ..]) !! x). f x) = (SUP x. INF xa. p (x[xa ..]) !! xa)"
by (metis (mono_tags, lifting) INF_apply INF_cong Inf_fun_def)
theorem SUP_Always: "top_dep p ⟹ SUPREMUM UNIV (□ p) = □ (SUPREMUM UNIV (p::('b::trace) ⇒ 'a::temporal))"
proof (simp add: always_def Sup_at at_fun_def INF_SUP INF_SUP_range SUP_INF_range)
assume A: "top_dep p"
have "⋀x. (INF n. p (x[n ..]) !! n) ≤ (SUP x. INF n. p (x n) !! n)"
by (rule_tac i = "(λ i . x[i ..])" in SUP_upper2, simp_all)
from this have [simp]: "(SUP x. INF n. p (x[n ..]) !! n) ≤ (SUP x. INF n. p (x n) !! n)"
by (rule SUP_least)
have "⋀x. (INF n. p (x n) !! n) ≤ (SUP x. INF n. p (x[n ..]) !! n)"
apply (rule_tac y = "INF n. p ((Cat x)[n ..]) !! n" in order_trans)
apply (rule INF_greatest, simp)
apply (rule_tac y = "p (x n) !! n" in order_trans)
apply (rule INF_lower, simp)
using A apply (simp add: top_dep_def)
apply (drule_tac x = "Cat x[n ..]" in spec)
apply (drule_tac x = "x n" in spec)
apply (simp add: eqtop_Suc_Cat)
by (rule SUP_upper, simp)
from this have [simp]: "(SUP x. INF n. p (x n) !! n) ≤ (SUP x. INF n. p (x[n ..]) !! n)"
by (rule SUP_least)
show " (SUP x. INF xa. p (x[xa ..]) !! xa) = (SUP x. INF xa. p (x xa) !! xa)"
by (rule antisym, simp_all)
qed
text‹
In the last part of our formalization, we need to instantiate the functions
from $nat$ to some arbitrary type $\tv a$ as a trace class. However, this again is not
possible using the instatiation mechanism of Isabelle. We solve this problem
by creating another class called $nat$, and then we instatiate the functions
from $\tv a::nat$ to $\tv b$ as traces. The class $nat$ is defined such that if we
have a type $\tv a::nat$, then $\tv a$ is isomorphic to the type $nat$.
›
class nat = zero + plus + minus + one +
fixes RepNat :: "'a ⇒ nat"
fixes AbsNat :: "nat ⇒ 'a"
assumes RepAbsNat[simp]: "RepNat (AbsNat n) = n"
and AbsRepNat[simp]: "AbsNat (RepNat x) = x"
and zero_Nat_def: "0 = AbsNat 0"
and one_Nat_def: "1 = AbsNat 1"
and plus_Nat_def: "a + b = AbsNat (RepNat a + RepNat b)"
and minus_Nat_def: "a - b = AbsNat (RepNat a - RepNat b)"
begin
lemma AbsNat_plus: "AbsNat (i + j) = AbsNat i + AbsNat j"
by (simp add: plus_Nat_def)
lemma AbsNat_minus: "AbsNat (i - j) = AbsNat i - AbsNat j"
by (simp add: minus_Nat_def)
lemma AbsNat_zero [simp]: "AbsNat 0 + i = i"
by (simp add: plus_Nat_def)
lemma [simp]: "(AbsNat (Suc 0) + x = 0) = False"
apply (simp add: plus_Nat_def zero_Nat_def)
apply (rule notI)
apply (subgoal_tac "RepNat (AbsNat (Suc (RepNat x))) = RepNat (AbsNat 0)")
apply (unfold RepAbsNat) [1]
by simp_all
subclass comm_monoid_diff
apply (unfold_locales)
apply (simp_all add: plus_Nat_def zero_Nat_def minus_Nat_def add.assoc)
by (simp add: add.commute)
end
text‹
The type natural numbers is an instantiation of the class $nat$.
›
instantiation nat :: nat
begin
definition RepNat_nat_def [simp]: "(RepNat:: nat ⇒ nat) = id"
definition AbsNat_nat_def [simp]: "(AbsNat:: nat ⇒ nat) = id"
instance proof
qed auto
end
text‹
Finally, functions from $\tv a::nat$ to some arbitrary type $\tv b$ are instatiated
as a trace class.
›
instantiation "fun" :: (nat, type) trace
begin
definition at_trace_def [simp]: "((t :: 'a ⇒ 'b)[i..]) j = (t (AbsNat i + j))"
definition eqtop_trace_def [simp]: "eqtop n a b = (∀ i < n . a (AbsNat i) = b (AbsNat i))"
definition cat_trace_def [simp]: "cat n a b i = (if RepNat i < n then a i else b (i - AbsNat n))"
definition Cat_trace_def [simp]: "Cat y i = (y (RepNat i) 0)"
lemma eqtop_trace_eq: "∀n i. i < n ⟶ (a::'a⇒'b) (AbsNat i) = b (AbsNat i) ⟹ a = b"
proof (simp add: fun_eq_iff, safe)
fix x:: "'a"
assume " ∀n i. i < n ⟶ a (AbsNat i) = b (AbsNat i)"
from this have "∀ i < Suc (RepNat x) . a (AbsNat i) = b (AbsNat i)" by blast
from this have "a (AbsNat (RepNat x)) = b (AbsNat (RepNat x))" by blast
from this show "a x = b x" by simp
qed
lemma [simp]: "(RepNat (AbsNat n + xa) < n) = False"
by (subst plus_Nat_def, simp)
lemma [simp]: "AbsNat n + AbsNat 0 = AbsNat n"
by (subst plus_Nat_def, simp)
lemma trace_eqtop_tail: "∀i<n. x (AbsNat i) = y (AbsNat i) ⟹ ∀xa. x (AbsNat n + xa) = y (AbsNat n + xa) ⟹ x xa = y xa"
by (metis AbsNat_plus AbsRepNat add_diff_inverse)
lemma trace_eqtop_Suc: "∀i<n. x (AbsNat i) = y (AbsNat i) ⟹ x (AbsNat n) = y (AbsNat n) ⟹ i < Suc n ⟹ x (AbsNat i) = y (AbsNat i)"
by (metis less_antisym)
lemma RepNat_is_zero: "RepNat x = 0 ⟹ x = 0"
proof -
assume "RepNat x = 0"
from this have "AbsNat (RepNat x) = AbsNat(0)" by simp
from this show "x = 0" apply (subst zero_Nat_def)
by (subst (asm) AbsRepNat, simp)
qed
lemma RepNat_zero: "RepNat x = 0 ⟹ u 0 x = u 0 0"
by (drule RepNat_is_zero, simp)
lemma [simp]: "0 < RepNat x ⟹ (Suc (RepNat (x - AbsNat (Suc 0)))) = RepNat x"
by (subst minus_Nat_def, simp)
instance proof
fix n::nat fix x y :: "'a ⇒ 'b"
show "cat (Suc n) x y = cat (Suc 0) x (cat n (x[Suc 0..]) y)"
apply (simp add: fun_eq_iff)
apply auto
apply (metis (no_types, lifting) AbsRepNat RepAbsNat Suc_pred add.left_neutral add_Suc_shift minus_Nat_def plus_Nat_def)
using not_less_eq apply auto[1]
using less_Suc_eq_0_disj apply auto[1]
by (metis (no_types, lifting) One_nat_def RepAbsNat diff_Suc_eq_diff_pred minus_Nat_def)
next
fix x y :: "'a ⇒ 'b"
show "cat 0 x y = y"
apply (auto simp add: fun_eq_iff)
by (metis diff_zero zero_Nat_def)
next
qed (auto simp add: fun_eq_iff AbsNat_plus add.assoc AbsNat_minus one_Nat_def RepNat_zero, drule eqtop_trace_eq,
simp_all, drule trace_eqtop_Suc)
end
text‹
By putting together all class definitions and instatiations introduced so far, we obtain the
temporal class structure for predicates on traces with arbitrary number of parameters.
For example in the next lemma $r$ and $r'$ are predicate relations, and the operator
always is available for them as a consequence of the above construction.
›
lemma "(□ r) OO (□ r') ≤ (□ (r OO r'))"
by (simp add: le_fun_def always_def at_fun_def, auto)
lemma [simp]: "(next ^^ n) ⊤ = ⊤"
apply (induction n, simp)
by (simp add: next_def)
lemma "r (u[1..]) = (∃ y . (⨀ (λ v . v = y ∧ r y)) u)"
apply safe
apply (rule_tac x = "u[1..]" in exI)
apply (simp add: next_def at_fun_def)
by (simp add: next_def at_fun_def)
lemma "r (u[1..]) = ( (⨀ (λ v . ∃ y . v = y ∧ r y)) u)"
apply safe
apply (simp add: next_def at_fun_def)
by (simp add: next_def at_fun_def)
lemma "(r (u[1..])::bool) = ( (⨀ r) u)"
apply safe
apply (simp add: next_def at_fun_def)
by (simp add: next_def at_fun_def)
lemma "((□ r) u (u[1..]) x y ::bool) = ( (⨀ (λ u' . (□ r) u u' x y)) u)"
apply safe
apply (simp add: next_def at_fun_def)
by (simp add: next_def at_fun_def)
lemma "r (u[1..]) = (∃ y . (⨀ (λ v y . v = y ∧ r y)) u y)"
apply safe
apply (rule_tac x = "u" in exI)
apply (simp add: next_def at_fun_def)
by (simp add: next_def at_fun_def)
subsection‹Propositional Temporal Logic›
definition "prop P σ = (P ∈ σ (0::nat))"
definition "Exists P f σ = (∃ σ' . (∀ i . σ i - {P} = σ' i - {P}) ∧ f σ')"
definition "Forall P f σ = (∀ σ' . (∀ i . σ i - {P} = σ' i - {P}) ⟶ f σ')"
definition impl:: "'a ⇒ 'a ⇒ ('a::boolean_algebra)" (infixl "→" 60)
where "x → y = ((-x) ⊔ y)"
lemma "x ≠ y ⟹ (Exists y ((□ (prop x → (♢ prop y))) ⊓ □ ♢ prop y)) = ⊤"
apply (auto simp add: fun_eq_iff)
apply (simp add: Exists_def)
apply (rule_tac x = "λ i . xa i ∪ {y}" in exI, simp, safe)
apply (simp add: always_def at_fun_def impl_def, safe)
apply (simp add: eventually_def at_fun_def)
apply (rule_tac x = 0 in exI)
apply (simp add: prop_def)
apply (simp add: always_def at_fun_def impl_def eventually_def, safe)
apply (rule_tac x = 0 in exI)
by (simp add: prop_def)
lemma "x ≠ y ⟹ (Forall y ((□ (prop x → (♢ prop y))) → □ ♢ prop y)) = (□ ♢ (prop x))"
apply (auto simp add: fun_eq_iff)
apply (simp add: Forall_def impl_def sup_fun_def)
apply (subst always_def)
apply (subst eventually_def)
apply (simp add: at_fun_def, safe)
apply (subst prop_def, simp)
apply (drule_tac x = "λ i . if i < f then xa i ∪ {y} else xa i - {y}" in spec)
apply safe
apply auto [1]
apply (case_tac "i < f")
apply auto [2]
apply (simp add: always_def eventually_def at_fun_def prop_def, safe)
apply (case_tac "fa < f", simp_all)
apply (drule_tac x = 0 in spec, simp)
apply (rule_tac x = "fa - f" in exI, simp)
apply (simp add: always_def eventually_def at_fun_def prop_def)
apply (drule_tac x = f in spec, simp)
apply (simp add: Forall_def impl_def, safe)
apply (simp add: always_def eventually_def at_fun_def prop_def, safe)
apply (drule_tac x = f in spec, safe)
apply (drule_tac x = "f + fa" in spec)
apply (drule_tac x = "f + fa" in spec, safe)
apply auto[1]
apply (rule_tac x = "fa + fb" in exI)
by (simp add: add.assoc)
definition LTL :: "('a ⇒ 'b) ⇒ ((nat ⇒ 'a) ⇒ 'b)" (binder "ltl " 10)
where "LTL P x = (P (x 0))"
end