1(*  Title:      HOL/HOLCF/IOA/RefCorrectness.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Correctness of Refinement Mappings in HOLCF/IOA\<close>
6
7theory RefCorrectness
8imports RefMappings
9begin
10
11definition corresp_exC ::
12    "('a, 's2) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) pairs \<rightarrow> ('s1 \<Rightarrow> ('a, 's2) pairs)"
13  where "corresp_exC A f =
14    (fix \<cdot>
15      (LAM h ex.
16        (\<lambda>s. case ex of
17          nil \<Rightarrow> nil
18        | x ## xs \<Rightarrow>
19            flift1 (\<lambda>pr.
20              (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@ ((h \<cdot> xs) (snd pr))) \<cdot> x)))"
21
22definition corresp_ex ::
23    "('a, 's2) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
24  where "corresp_ex A f ex = (f (fst ex), (corresp_exC A f \<cdot> (snd ex)) (fst ex))"
25
26definition is_fair_ref_map ::
27    "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
28  where "is_fair_ref_map f C A \<longleftrightarrow>
29    is_ref_map f C A \<and> (\<forall>ex \<in> executions C. fair_ex C ex \<longrightarrow> fair_ex A (corresp_ex A f ex))"
30
31text \<open>
32  Axioms for fair trace inclusion proof support, not for the correctness proof
33  of refinement mappings!
34
35  Note: Everything is superseded by \<^file>\<open>LiveIOA.thy\<close>.
36\<close>
37
38axiomatization where
39  corresp_laststate:
40    "Finite ex \<Longrightarrow> laststate (corresp_ex A f (s, ex)) = f (laststate (s, ex))"
41
42axiomatization where
43  corresp_Finite: "Finite (snd (corresp_ex A f (s, ex))) = Finite ex"
44
45axiomatization where
46  FromAtoC:
47    "fin_often (\<lambda>x. P (snd x)) (snd (corresp_ex A f (s, ex))) \<Longrightarrow>
48      fin_often (\<lambda>y. P (f (snd y))) ex"
49
50axiomatization where
51  FromCtoA:
52    "inf_often (\<lambda>y. P (fst y)) ex \<Longrightarrow>
53      inf_often (\<lambda>x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
54
55
56text \<open>
57  Proof by case on \<open>inf W\<close> in ex: If so, ok. If not, only \<open>fin W\<close> in ex, ie.
58  there is an index \<open>i\<close> from which on no \<open>W\<close> in ex. But \<open>W\<close> inf enabled, ie at
59  least once after \<open>i\<close> \<open>W\<close> is enabled. As \<open>W\<close> does not occur after \<open>i\<close> and \<open>W\<close>
60  is \<open>enabling_persistent\<close>, \<open>W\<close> keeps enabled until infinity, ie. indefinitely
61\<close>
62
63axiomatization where
64  persistent:
65    "inf_often (\<lambda>x. Enabled A W (snd x)) ex \<Longrightarrow> en_persistent A W \<Longrightarrow>
66      inf_often (\<lambda>x. fst x \<in> W) ex \<or> fin_often (\<lambda>x. \<not> Enabled A W (snd x)) ex"
67
68axiomatization where
69  infpostcond:
70    "is_exec_frag A (s,ex) \<Longrightarrow> inf_often (\<lambda>x. fst x \<in> W) ex \<Longrightarrow>
71      inf_often (\<lambda>x. set_was_enabled A W (snd x)) ex"
72
73
74subsection \<open>\<open>corresp_ex\<close>\<close>
75
76lemma corresp_exC_unfold:
77  "corresp_exC A f =
78    (LAM ex.
79      (\<lambda>s.
80        case ex of
81          nil \<Rightarrow> nil
82        | x ## xs \<Rightarrow>
83            (flift1 (\<lambda>pr.
84              (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@
85              ((corresp_exC A f \<cdot> xs) (snd pr))) \<cdot> x)))"
86  apply (rule trans)
87  apply (rule fix_eq2)
88  apply (simp only: corresp_exC_def)
89  apply (rule beta_cfun)
90  apply (simp add: flift1_def)
91  done
92
93lemma corresp_exC_UU: "(corresp_exC A f \<cdot> UU) s = UU"
94  apply (subst corresp_exC_unfold)
95  apply simp
96  done
97
98lemma corresp_exC_nil: "(corresp_exC A f \<cdot> nil) s = nil"
99  apply (subst corresp_exC_unfold)
100  apply simp
101  done
102
103lemma corresp_exC_cons:
104  "(corresp_exC A f \<cdot> (at \<leadsto> xs)) s =
105     (SOME cex. move A cex (f s) (fst at) (f (snd at))) @@
106     ((corresp_exC A f \<cdot> xs) (snd at))"
107  apply (rule trans)
108  apply (subst corresp_exC_unfold)
109  apply (simp add: Consq_def flift1_def)
110  apply simp
111  done
112
113declare corresp_exC_UU [simp] corresp_exC_nil [simp] corresp_exC_cons [simp]
114
115
116subsection \<open>Properties of move\<close>
117
118lemma move_is_move:
119  "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
120    move A (SOME x. move A x (f s) a (f t)) (f s) a (f t)"
121  apply (unfold is_ref_map_def)
122  apply (subgoal_tac "\<exists>ex. move A ex (f s) a (f t) ")
123  prefer 2
124  apply simp
125  apply (erule exE)
126  apply (rule someI)
127  apply assumption
128  done
129
130lemma move_subprop1:
131  "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
132    is_exec_frag A (f s, SOME x. move A x (f s) a (f t))"
133  apply (cut_tac move_is_move)
134  defer
135  apply assumption+
136  apply (simp add: move_def)
137  done
138
139lemma move_subprop2:
140  "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
141    Finite ((SOME x. move A x (f s) a (f t)))"
142  apply (cut_tac move_is_move)
143  defer
144  apply assumption+
145  apply (simp add: move_def)
146  done
147
148lemma move_subprop3:
149  "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
150     laststate (f s, SOME x. move A x (f s) a (f t)) = (f t)"
151  apply (cut_tac move_is_move)
152  defer
153  apply assumption+
154  apply (simp add: move_def)
155  done
156
157lemma move_subprop4:
158  "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
159    mk_trace A \<cdot> ((SOME x. move A x (f s) a (f t))) =
160      (if a \<in> ext A then a \<leadsto> nil else nil)"
161  apply (cut_tac move_is_move)
162  defer
163  apply assumption+
164  apply (simp add: move_def)
165  done
166
167
168subsection \<open>TRACE INCLUSION Part 1: Traces coincide\<close>
169
170subsubsection \<open>Lemmata for \<open>\<Longleftarrow>\<close>\<close>
171
172text \<open>Lemma 1.1: Distribution of \<open>mk_trace\<close> and \<open>@@\<close>\<close>
173
174lemma mk_traceConc:
175  "mk_trace C \<cdot> (ex1 @@ ex2) = (mk_trace C \<cdot> ex1) @@ (mk_trace C \<cdot> ex2)"
176  by (simp add: mk_trace_def filter_act_def MapConc)
177
178
179text \<open>Lemma 1 : Traces coincide\<close>
180
181lemma lemma_1:
182  "is_ref_map f C A \<Longrightarrow> ext C = ext A \<Longrightarrow>
183    \<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow>
184      mk_trace C \<cdot> xs = mk_trace A \<cdot> (snd (corresp_ex A f (s, xs)))"
185  supply if_split [split del]
186  apply (unfold corresp_ex_def)
187  apply (pair_induct xs simp: is_exec_frag_def)
188  text \<open>cons case\<close>
189  apply (auto simp add: mk_traceConc)
190  apply (frule reachable.reachable_n)
191  apply assumption
192  apply (auto simp add: move_subprop4 split: if_split)
193  done
194
195
196subsection \<open>TRACE INCLUSION Part 2: corresp_ex is execution\<close>
197
198subsubsection \<open>Lemmata for \<open>==>\<close>\<close>
199
200text \<open>Lemma 2.1\<close>
201
202lemma lemma_2_1 [rule_format]:
203  "Finite xs \<longrightarrow>
204    (\<forall>s. is_exec_frag A (s, xs) \<and> is_exec_frag A (t, ys) \<and>
205      t = laststate (s, xs) \<longrightarrow> is_exec_frag A (s, xs @@ ys))"
206  apply (rule impI)
207  apply Seq_Finite_induct
208  text \<open>main case\<close>
209  apply (auto simp add: split_paired_all)
210  done
211
212
213text \<open>Lemma 2 : \<open>corresp_ex\<close> is execution\<close>
214
215lemma lemma_2:
216  "is_ref_map f C A \<Longrightarrow>
217    \<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow>
218      is_exec_frag A (corresp_ex A f (s, xs))"
219  apply (unfold corresp_ex_def)
220
221  apply simp
222  apply (pair_induct xs simp: is_exec_frag_def)
223
224  text \<open>main case\<close>
225  apply auto
226  apply (rule_tac t = "f x2" in lemma_2_1)
227
228  text \<open>\<open>Finite\<close>\<close>
229  apply (erule move_subprop2)
230  apply assumption+
231  apply (rule conjI)
232
233  text \<open>\<open>is_exec_frag\<close>\<close>
234  apply (erule move_subprop1)
235  apply assumption+
236  apply (rule conjI)
237
238  text \<open>Induction hypothesis\<close>
239  text \<open>\<open>reachable_n\<close> looping, therefore apply it manually\<close>
240  apply (erule_tac x = "x2" in allE)
241  apply simp
242  apply (frule reachable.reachable_n)
243  apply assumption
244  apply simp
245
246  text \<open>\<open>laststate\<close>\<close>
247  apply (erule move_subprop3 [symmetric])
248  apply assumption+
249  done
250
251
252subsection \<open>Main Theorem: TRACE -- INCLUSION\<close>
253
254theorem trace_inclusion:
255  "ext C = ext A \<Longrightarrow> is_ref_map f C A \<Longrightarrow> traces C \<subseteq> traces A"
256
257  apply (unfold traces_def)
258
259  apply (simp add: has_trace_def2)
260  apply auto
261
262  text \<open>give execution of abstract automata\<close>
263  apply (rule_tac x = "corresp_ex A f ex" in bexI)
264
265  text \<open>Traces coincide, Lemma 1\<close>
266  apply (pair ex)
267  apply (erule lemma_1 [THEN spec, THEN mp])
268  apply assumption+
269  apply (simp add: executions_def reachable.reachable_0)
270
271  text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
272  apply (pair ex)
273  apply (simp add: executions_def)
274  text \<open>start state\<close>
275  apply (rule conjI)
276  apply (simp add: is_ref_map_def corresp_ex_def)
277  text \<open>\<open>is_execution_fragment\<close>\<close>
278  apply (erule lemma_2 [THEN spec, THEN mp])
279  apply (simp add: reachable.reachable_0)
280  done
281
282
283subsection \<open>Corollary:  FAIR TRACE -- INCLUSION\<close>
284
285lemma fininf: "(~inf_often P s) = fin_often P s"
286  by (auto simp: fin_often_def)
287
288lemma WF_alt: "is_wfair A W (s, ex) =
289  (fin_often (\<lambda>x. \<not> Enabled A W (snd x)) ex \<longrightarrow> inf_often (\<lambda>x. fst x \<in> W) ex)"
290  by (auto simp add: is_wfair_def fin_often_def)
291
292lemma WF_persistent:
293  "is_wfair A W (s, ex) \<Longrightarrow> inf_often (\<lambda>x. Enabled A W (snd x)) ex \<Longrightarrow>
294    en_persistent A W \<Longrightarrow> inf_often (\<lambda>x. fst x \<in> W) ex"
295  apply (drule persistent)
296  apply assumption
297  apply (simp add: WF_alt)
298  apply auto
299  done
300
301lemma fair_trace_inclusion:
302  assumes "is_ref_map f C A"
303    and "ext C = ext A"
304    and "\<And>ex. ex \<in> executions C \<Longrightarrow> fair_ex C ex \<Longrightarrow>
305      fair_ex A (corresp_ex A f ex)"
306  shows "fairtraces C \<subseteq> fairtraces A"
307  apply (insert assms)
308  apply (simp add: fairtraces_def fairexecutions_def)
309  apply auto
310  apply (rule_tac x = "corresp_ex A f ex" in exI)
311  apply auto
312
313  text \<open>Traces coincide, Lemma 1\<close>
314  apply (pair ex)
315  apply (erule lemma_1 [THEN spec, THEN mp])
316  apply assumption+
317  apply (simp add: executions_def reachable.reachable_0)
318
319  text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
320  apply (pair ex)
321  apply (simp add: executions_def)
322  text \<open>start state\<close>
323  apply (rule conjI)
324  apply (simp add: is_ref_map_def corresp_ex_def)
325  text \<open>\<open>is_execution_fragment\<close>\<close>
326  apply (erule lemma_2 [THEN spec, THEN mp])
327  apply (simp add: reachable.reachable_0)
328  done
329
330lemma fair_trace_inclusion2:
331  "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_fair_ref_map f C A \<Longrightarrow>
332    fair_implements C A"
333  apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def)
334  apply auto
335  apply (rule_tac x = "corresp_ex A f ex" in exI)
336  apply auto
337
338  text \<open>Traces coincide, Lemma 1\<close>
339  apply (pair ex)
340  apply (erule lemma_1 [THEN spec, THEN mp])
341  apply (simp (no_asm) add: externals_def)
342  apply (auto)[1]
343  apply (simp add: executions_def reachable.reachable_0)
344
345  text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
346  apply (pair ex)
347  apply (simp add: executions_def)
348  text \<open>start state\<close>
349  apply (rule conjI)
350  apply (simp add: is_ref_map_def corresp_ex_def)
351  text \<open>\<open>is_execution_fragment\<close>\<close>
352  apply (erule lemma_2 [THEN spec, THEN mp])
353  apply (simp add: reachable.reachable_0)
354  done
355
356end
357