author | wenzelm |
Mon, 25 Jul 2016 21:50:04 +0200 | |
changeset 63549 | b0d31c7def86 |
parent 62441 | e5e38e1f2dd4 |
child 63648 | f9f3006a5579 |
permissions | -rw-r--r-- |
62008 | 1 |
(* Title: HOL/HOLCF/IOA/TLS.thy |
40945 | 2 |
Author: Olaf Müller |
17233 | 3 |
*) |
4559 | 4 |
|
62002 | 5 |
section \<open>Temporal Logic of Steps -- tailored for I/O automata\<close> |
4559 | 6 |
|
17233 | 7 |
theory TLS |
8 |
imports IOA TL |
|
9 |
begin |
|
4559 | 10 |
|
36452 | 11 |
default_sort type |
4559 | 12 |
|
62005 | 13 |
type_synonym ('a, 's) ioa_temp = "('a option, 's) transition temporal" |
4559 | 14 |
|
62005 | 15 |
type_synonym ('a, 's) step_pred = "('a option, 's) transition predicate" |
4559 | 16 |
|
62005 | 17 |
type_synonym 's state_pred = "'s predicate" |
4559 | 18 |
|
62005 | 19 |
definition mkfin :: "'a Seq \<Rightarrow> 'a Seq" |
20 |
where "mkfin s = (if Partial s then SOME t. Finite t \<and> s = t @@ UU else s)" |
|
4559 | 21 |
|
62005 | 22 |
definition option_lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a option \<Rightarrow> 'b" |
23 |
where "option_lift f s y = (case y of None \<Rightarrow> s | Some x \<Rightarrow> f x)" |
|
4559 | 24 |
|
62005 | 25 |
definition plift :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" |
17233 | 26 |
(* plift is used to determine that None action is always false in |
4559 | 27 |
transition predicates *) |
62005 | 28 |
where "plift P = option_lift P False" |
4559 | 29 |
|
62005 | 30 |
definition xt1 :: "'s predicate \<Rightarrow> ('a, 's) step_pred" |
31 |
where "xt1 P tr = P (fst tr)" |
|
4559 | 32 |
|
62005 | 33 |
definition xt2 :: "'a option predicate \<Rightarrow> ('a, 's) step_pred" |
34 |
where "xt2 P tr = P (fst (snd tr))" |
|
4559 | 35 |
|
62005 | 36 |
definition ex2seqC :: "('a, 's) pairs \<rightarrow> ('s \<Rightarrow> ('a option, 's) transition Seq)" |
62192 | 37 |
where "ex2seqC = |
63549 | 38 |
(fix \<cdot> (LAM h ex. (\<lambda>s. case ex of |
62192 | 39 |
nil \<Rightarrow> (s, None, s) \<leadsto> nil |
63549 | 40 |
| x ## xs \<Rightarrow> (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (h \<cdot> xs) (snd pr)) \<cdot> x))))" |
4559 | 41 |
|
62005 | 42 |
definition ex2seq :: "('a, 's) execution \<Rightarrow> ('a option, 's) transition Seq" |
63549 | 43 |
where "ex2seq ex = (ex2seqC \<cdot> (mkfin (snd ex))) (fst ex)" |
62005 | 44 |
|
45 |
definition temp_sat :: "('a, 's) execution \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" (infixr "\<TTurnstile>" 22) |
|
46 |
where "(ex \<TTurnstile> P) \<longleftrightarrow> ((ex2seq ex) \<Turnstile> P)" |
|
4559 | 47 |
|
62005 | 48 |
definition validTE :: "('a, 's) ioa_temp \<Rightarrow> bool" |
49 |
where "validTE P \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P))" |
|
50 |
||
51 |
definition validIOA :: "('a, 's) ioa \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" |
|
52 |
where "validIOA A P \<longleftrightarrow> (\<forall>ex \<in> executions A. (ex \<TTurnstile> P))" |
|
4559 | 53 |
|
5976 | 54 |
|
62193 | 55 |
lemma IMPLIES_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<longrightarrow> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<longrightarrow> (ex \<TTurnstile> Q))" |
56 |
by (simp add: IMPLIES_def temp_sat_def satisfies_def) |
|
57 |
||
58 |
lemma AND_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<and> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<and> (ex \<TTurnstile> Q))" |
|
59 |
by (simp add: AND_def temp_sat_def satisfies_def) |
|
60 |
||
61 |
lemma OR_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<or> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<or> (ex \<TTurnstile> Q))" |
|
62 |
by (simp add: OR_def temp_sat_def satisfies_def) |
|
63 |
||
64 |
lemma NOT_temp_sat [simp]: "(ex \<TTurnstile> \<^bold>\<not> P) \<longleftrightarrow> (\<not> (ex \<TTurnstile> P))" |
|
65 |
by (simp add: NOT_def temp_sat_def satisfies_def) |
|
66 |
||
67 |
||
62005 | 68 |
axiomatization |
62192 | 69 |
where mkfin_UU [simp]: "mkfin UU = nil" |
70 |
and mkfin_nil [simp]: "mkfin nil = nil" |
|
71 |
and mkfin_cons [simp]: "mkfin (a \<leadsto> s) = a \<leadsto> mkfin s" |
|
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
72 |
|
19741 | 73 |
|
37598 | 74 |
lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex |
19741 | 75 |
|
62002 | 76 |
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close> |
19741 | 77 |
|
78 |
||
62002 | 79 |
subsection \<open>ex2seqC\<close> |
19741 | 80 |
|
62192 | 81 |
lemma ex2seqC_unfold: |
82 |
"ex2seqC = |
|
83 |
(LAM ex. (\<lambda>s. case ex of |
|
84 |
nil \<Rightarrow> (s, None, s) \<leadsto> nil |
|
85 |
| x ## xs \<Rightarrow> |
|
63549 | 86 |
(flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (ex2seqC \<cdot> xs) (snd pr)) \<cdot> x)))" |
62005 | 87 |
apply (rule trans) |
88 |
apply (rule fix_eq4) |
|
89 |
apply (rule ex2seqC_def) |
|
90 |
apply (rule beta_cfun) |
|
91 |
apply (simp add: flift1_def) |
|
92 |
done |
|
19741 | 93 |
|
63549 | 94 |
lemma ex2seqC_UU [simp]: "(ex2seqC \<cdot> UU) s = UU" |
62005 | 95 |
apply (subst ex2seqC_unfold) |
96 |
apply simp |
|
97 |
done |
|
19741 | 98 |
|
63549 | 99 |
lemma ex2seqC_nil [simp]: "(ex2seqC \<cdot> nil) s = (s, None, s) \<leadsto> nil" |
62005 | 100 |
apply (subst ex2seqC_unfold) |
101 |
apply simp |
|
102 |
done |
|
19741 | 103 |
|
63549 | 104 |
lemma ex2seqC_cons [simp]: "(ex2seqC \<cdot> ((a, t) \<leadsto> xs)) s = (s, Some a,t ) \<leadsto> (ex2seqC \<cdot> xs) t" |
62005 | 105 |
apply (rule trans) |
106 |
apply (subst ex2seqC_unfold) |
|
107 |
apply (simp add: Consq_def flift1_def) |
|
108 |
apply (simp add: Consq_def flift1_def) |
|
109 |
done |
|
19741 | 110 |
|
111 |
||
62192 | 112 |
lemma ex2seq_UU: "ex2seq (s, UU) = (s, None, s) \<leadsto> nil" |
62005 | 113 |
by (simp add: ex2seq_def) |
19741 | 114 |
|
62192 | 115 |
lemma ex2seq_nil: "ex2seq (s, nil) = (s, None, s) \<leadsto> nil" |
62005 | 116 |
by (simp add: ex2seq_def) |
19741 | 117 |
|
62192 | 118 |
lemma ex2seq_cons: "ex2seq (s, (a, t) \<leadsto> ex) = (s, Some a, t) \<leadsto> ex2seq (t, ex)" |
62005 | 119 |
by (simp add: ex2seq_def) |
19741 | 120 |
|
121 |
declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del] |
|
122 |
declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp] |
|
123 |
||
124 |
||
62192 | 125 |
lemma ex2seq_nUUnnil: "ex2seq exec \<noteq> UU \<and> ex2seq exec \<noteq> nil" |
62195 | 126 |
apply (pair exec) |
127 |
apply (Seq_case_simp x2) |
|
128 |
apply (pair a) |
|
62005 | 129 |
done |
19741 | 130 |
|
131 |
||
62002 | 132 |
subsection \<open>Interface TL -- TLS\<close> |
19741 | 133 |
|
62005 | 134 |
(* uses the fact that in executions states overlap, which is lost in |
19741 | 135 |
after the translation via ex2seq !! *) |
136 |
||
62005 | 137 |
lemma TL_TLS: |
62192 | 138 |
"\<forall>s a t. (P s) \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> (Q t) |
139 |
\<Longrightarrow> ex \<TTurnstile> (Init (\<lambda>(s, a, t). P s) \<^bold>\<and> Init (\<lambda>(s, a, t). s \<midarrow>a\<midarrow>A\<rightarrow> t) |
|
62441 | 140 |
\<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))" |
62005 | 141 |
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def) |
142 |
apply clarify |
|
62390 | 143 |
apply (simp split add: if_split) |
62192 | 144 |
text \<open>\<open>TL = UU\<close>\<close> |
62005 | 145 |
apply (rule conjI) |
62195 | 146 |
apply (pair ex) |
147 |
apply (Seq_case_simp x2) |
|
148 |
apply (pair a) |
|
149 |
apply (Seq_case_simp s) |
|
150 |
apply (pair a) |
|
62192 | 151 |
text \<open>\<open>TL = nil\<close>\<close> |
62005 | 152 |
apply (rule conjI) |
62195 | 153 |
apply (pair ex) |
154 |
apply (Seq_case x2) |
|
62005 | 155 |
apply (simp add: unlift_def) |
156 |
apply fast |
|
157 |
apply (simp add: unlift_def) |
|
158 |
apply fast |
|
159 |
apply (simp add: unlift_def) |
|
62195 | 160 |
apply (pair a) |
161 |
apply (Seq_case_simp s) |
|
162 |
apply (pair a) |
|
62192 | 163 |
text \<open>\<open>TL = cons\<close>\<close> |
62005 | 164 |
apply (simp add: unlift_def) |
62195 | 165 |
apply (pair ex) |
166 |
apply (Seq_case_simp x2) |
|
167 |
apply (pair a) |
|
168 |
apply (Seq_case_simp s) |
|
169 |
apply (pair a) |
|
62005 | 170 |
done |
4559 | 171 |
|
172 |
end |