10 |
10 |
11 default_sort type |
11 default_sort type |
12 |
12 |
13 type_synonym 'a temporal = "'a Seq predicate" |
13 type_synonym 'a temporal = "'a Seq predicate" |
14 |
14 |
15 definition validT :: "'a Seq predicate \<Rightarrow> bool" ("\<^bold>\<TTurnstile> _" [9] 8) |
15 definition validT :: "'a Seq predicate \<Rightarrow> bool" (\<open>\<^bold>\<TTurnstile> _\<close> [9] 8) |
16 where "(\<^bold>\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> P))" |
16 where "(\<^bold>\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> P))" |
17 |
17 |
18 definition unlift :: "'a lift \<Rightarrow> 'a" |
18 definition unlift :: "'a lift \<Rightarrow> 'a" |
19 where "unlift x = (case x of Def y \<Rightarrow> y)" |
19 where "unlift x = (case x of Def y \<Rightarrow> y)" |
20 |
20 |
21 definition Init :: "'a predicate \<Rightarrow> 'a temporal" ("\<langle>_\<rangle>" [0] 1000) |
21 definition Init :: "'a predicate \<Rightarrow> 'a temporal" (\<open>\<langle>_\<rangle>\<close> [0] 1000) |
22 where "Init P s = P (unlift (HD \<cdot> s))" |
22 where "Init P s = P (unlift (HD \<cdot> s))" |
23 \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close> |
23 \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close> |
24 |
24 |
25 definition Next :: "'a temporal \<Rightarrow> 'a temporal" ("\<circle>(_)" [80] 80) |
25 definition Next :: "'a temporal \<Rightarrow> 'a temporal" (\<open>\<circle>(_)\<close> [80] 80) |
26 where "(\<circle>P) s \<longleftrightarrow> (if TL \<cdot> s = UU \<or> TL \<cdot> s = nil then P s else P (TL \<cdot> s))" |
26 where "(\<circle>P) s \<longleftrightarrow> (if TL \<cdot> s = UU \<or> TL \<cdot> s = nil then P s else P (TL \<cdot> s))" |
27 |
27 |
28 definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool" |
28 definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool" |
29 where "suffix s2 s \<longleftrightarrow> (\<exists>s1. Finite s1 \<and> s = s1 @@ s2)" |
29 where "suffix s2 s \<longleftrightarrow> (\<exists>s1. Finite s1 \<and> s = s1 @@ s2)" |
30 |
30 |
31 definition tsuffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool" |
31 definition tsuffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool" |
32 where "tsuffix s2 s \<longleftrightarrow> s2 \<noteq> nil \<and> s2 \<noteq> UU \<and> suffix s2 s" |
32 where "tsuffix s2 s \<longleftrightarrow> s2 \<noteq> nil \<and> s2 \<noteq> UU \<and> suffix s2 s" |
33 |
33 |
34 definition Box :: "'a temporal \<Rightarrow> 'a temporal" ("\<box>(_)" [80] 80) |
34 definition Box :: "'a temporal \<Rightarrow> 'a temporal" (\<open>\<box>(_)\<close> [80] 80) |
35 where "(\<box>P) s \<longleftrightarrow> (\<forall>s2. tsuffix s2 s \<longrightarrow> P s2)" |
35 where "(\<box>P) s \<longleftrightarrow> (\<forall>s2. tsuffix s2 s \<longrightarrow> P s2)" |
36 |
36 |
37 definition Diamond :: "'a temporal \<Rightarrow> 'a temporal" ("\<diamond>(_)" [80] 80) |
37 definition Diamond :: "'a temporal \<Rightarrow> 'a temporal" (\<open>\<diamond>(_)\<close> [80] 80) |
38 where "\<diamond>P = (\<^bold>\<not> (\<box>(\<^bold>\<not> P)))" |
38 where "\<diamond>P = (\<^bold>\<not> (\<box>(\<^bold>\<not> P)))" |
39 |
39 |
40 definition Leadsto :: "'a temporal \<Rightarrow> 'a temporal \<Rightarrow> 'a temporal" (infixr "\<leadsto>" 22) |
40 definition Leadsto :: "'a temporal \<Rightarrow> 'a temporal \<Rightarrow> 'a temporal" (infixr \<open>\<leadsto>\<close> 22) |
41 where "(P \<leadsto> Q) = (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))" |
41 where "(P \<leadsto> Q) = (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))" |
42 |
42 |
43 |
43 |
44 lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)" |
44 lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)" |
45 by (auto simp add: Diamond_def NOT_def Box_def) |
45 by (auto simp add: Diamond_def NOT_def Box_def) |