1(*  Title:      HOL/HOLCF/IOA/TLS.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Temporal Logic of Steps -- tailored for I/O automata\<close>
6
7theory TLS
8imports IOA TL
9begin
10
11default_sort type
12
13type_synonym ('a, 's) ioa_temp  = "('a option, 's) transition temporal"
14
15type_synonym ('a, 's) step_pred = "('a option, 's) transition predicate"
16
17type_synonym 's state_pred = "'s predicate"
18
19definition mkfin :: "'a Seq \<Rightarrow> 'a Seq"
20  where "mkfin s = (if Partial s then SOME t. Finite t \<and> s = t @@ UU else s)"
21
22definition 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)"
24
25definition plift :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
26(* plift is used to determine that None action is always false in
27   transition predicates *)
28  where "plift P = option_lift P False"
29
30definition xt1 :: "'s predicate \<Rightarrow> ('a, 's) step_pred"
31  where "xt1 P tr = P (fst tr)"
32
33definition xt2 :: "'a option predicate \<Rightarrow> ('a, 's) step_pred"
34  where "xt2 P tr = P (fst (snd tr))"
35
36definition ex2seqC :: "('a, 's) pairs \<rightarrow> ('s \<Rightarrow> ('a option, 's) transition Seq)"
37  where "ex2seqC =
38    (fix \<cdot> (LAM h ex. (\<lambda>s. case ex of
39      nil \<Rightarrow> (s, None, s) \<leadsto> nil
40    | x ## xs \<Rightarrow> (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (h \<cdot> xs) (snd pr)) \<cdot> x))))"
41
42definition ex2seq :: "('a, 's) execution \<Rightarrow> ('a option, 's) transition Seq"
43  where "ex2seq ex = (ex2seqC \<cdot> (mkfin (snd ex))) (fst ex)"
44
45definition 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)"
47
48definition validTE :: "('a, 's) ioa_temp \<Rightarrow> bool"
49  where "validTE P \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P))"
50
51definition 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))"
53
54
55lemma 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
58lemma 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
61lemma 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
64lemma 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
68axiomatization
69where 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"
72
73
74lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
75
76setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
77
78
79subsection \<open>ex2seqC\<close>
80
81lemma ex2seqC_unfold:
82  "ex2seqC =
83    (LAM ex. (\<lambda>s. case ex of
84      nil \<Rightarrow> (s, None, s) \<leadsto> nil
85    | x ## xs \<Rightarrow>
86        (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (ex2seqC \<cdot> xs) (snd pr)) \<cdot> x)))"
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
93
94lemma ex2seqC_UU [simp]: "(ex2seqC \<cdot> UU) s = UU"
95  apply (subst ex2seqC_unfold)
96  apply simp
97  done
98
99lemma ex2seqC_nil [simp]: "(ex2seqC \<cdot> nil) s = (s, None, s) \<leadsto> nil"
100  apply (subst ex2seqC_unfold)
101  apply simp
102  done
103
104lemma ex2seqC_cons [simp]: "(ex2seqC \<cdot> ((a, t) \<leadsto> xs)) s = (s, Some a,t ) \<leadsto> (ex2seqC \<cdot> xs) t"
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
110
111
112lemma ex2seq_UU: "ex2seq (s, UU) = (s, None, s) \<leadsto> nil"
113  by (simp add: ex2seq_def)
114
115lemma ex2seq_nil: "ex2seq (s, nil) = (s, None, s) \<leadsto> nil"
116  by (simp add: ex2seq_def)
117
118lemma ex2seq_cons: "ex2seq (s, (a, t) \<leadsto> ex) = (s, Some a, t) \<leadsto> ex2seq (t, ex)"
119  by (simp add: ex2seq_def)
120
121declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del]
122declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp]
123
124
125lemma ex2seq_nUUnnil: "ex2seq exec \<noteq> UU \<and> ex2seq exec \<noteq> nil"
126  apply (pair exec)
127  apply (Seq_case_simp x2)
128  apply (pair a)
129  done
130
131
132subsection \<open>Interface TL -- TLS\<close>
133
134(* uses the fact that in executions states overlap, which is lost in
135   after the translation via ex2seq !! *)
136
137lemma TL_TLS:
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)
140              \<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))"
141  apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
142  apply clarify
143  apply (simp split: if_split)
144  text \<open>\<open>TL = UU\<close>\<close>
145  apply (rule conjI)
146  apply (pair ex)
147  apply (Seq_case_simp x2)
148  apply (pair a)
149  apply (Seq_case_simp s)
150  apply (pair a)
151  text \<open>\<open>TL = nil\<close>\<close>
152  apply (rule conjI)
153  apply (pair ex)
154  apply (Seq_case x2)
155  apply (simp add: unlift_def)
156  apply fast
157  apply (simp add: unlift_def)
158  apply fast
159  apply (simp add: unlift_def)
160  apply (pair a)
161  apply (Seq_case_simp s)
162  apply (pair a)
163  text \<open>\<open>TL = cons\<close>\<close>
164  apply (simp add: unlift_def)
165  apply (pair ex)
166  apply (Seq_case_simp x2)
167  apply (pair a)
168  apply (Seq_case_simp s)
169  apply (pair a)
170  done
171
172end
173