1(*  Title:      HOL/HOLCF/IOA/SimCorrectness.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Correctness of Simulations in HOLCF/IOA\<close>
6
7theory SimCorrectness
8imports Simulations
9begin
10
11(*Note: s2 instead of s1 in last argument type!*)
12definition corresp_ex_simC ::
13    "('a, 's2) ioa \<Rightarrow> ('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) pairs \<rightarrow> ('s2 \<Rightarrow> ('a, 's2) pairs)"
14  where "corresp_ex_simC A R =
15    (fix \<cdot> (LAM h ex. (\<lambda>s. case ex of
16      nil \<Rightarrow> nil
17    | x ## xs \<Rightarrow>
18        (flift1
19          (\<lambda>pr.
20            let
21              a = fst pr;
22              t = snd pr;
23              T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
24            in (SOME cex. move A cex s a T') @@ ((h \<cdot> xs) T')) \<cdot> x))))"
25
26definition corresp_ex_sim ::
27    "('a, 's2) ioa \<Rightarrow> ('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
28  where "corresp_ex_sim A R ex \<equiv>
29    let S' = SOME s'. (fst ex, s') \<in> R \<and> s' \<in> starts_of A
30    in (S', (corresp_ex_simC A R \<cdot> (snd ex)) S')"
31
32
33subsection \<open>\<open>corresp_ex_sim\<close>\<close>
34
35lemma corresp_ex_simC_unfold:
36  "corresp_ex_simC A R =
37    (LAM ex. (\<lambda>s. case ex of
38      nil \<Rightarrow> nil
39    | x ## xs \<Rightarrow>
40        (flift1
41          (\<lambda>pr.
42            let
43              a = fst pr;
44              t = snd pr;
45              T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
46            in (SOME cex. move A cex s a T') @@ ((corresp_ex_simC A R \<cdot> xs) T')) \<cdot> x)))"
47  apply (rule trans)
48  apply (rule fix_eq2)
49  apply (simp only: corresp_ex_simC_def)
50  apply (rule beta_cfun)
51  apply (simp add: flift1_def)
52  done
53
54lemma corresp_ex_simC_UU [simp]: "(corresp_ex_simC A R \<cdot> UU) s = UU"
55  apply (subst corresp_ex_simC_unfold)
56  apply simp
57  done
58
59lemma corresp_ex_simC_nil [simp]: "(corresp_ex_simC A R \<cdot> nil) s = nil"
60  apply (subst corresp_ex_simC_unfold)
61  apply simp
62  done
63
64lemma corresp_ex_simC_cons [simp]:
65  "(corresp_ex_simC A R \<cdot> ((a, t) \<leadsto> xs)) s =
66    (let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
67     in (SOME cex. move A cex s a T') @@ ((corresp_ex_simC A R \<cdot> xs) T'))"
68  apply (rule trans)
69  apply (subst corresp_ex_simC_unfold)
70  apply (simp add: Consq_def flift1_def)
71  apply simp
72  done
73
74
75subsection \<open>Properties of move\<close>
76
77lemma move_is_move_sim:
78   "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
79     let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
80     in (t, T') \<in> R \<and> move A (SOME ex2. move A ex2 s' a T') s' a T'"
81  supply Let_def [simp del]
82  apply (unfold is_simulation_def)
83  (* Does not perform conditional rewriting on assumptions automatically as
84     usual. Instantiate all variables per hand. Ask Tobias?? *)
85  apply (subgoal_tac "\<exists>t' ex. (t, t') \<in> R \<and> move A ex s' a t'")
86  prefer 2
87  apply simp
88  apply (erule conjE)
89  apply (erule_tac x = "s" in allE)
90  apply (erule_tac x = "s'" in allE)
91  apply (erule_tac x = "t" in allE)
92  apply (erule_tac x = "a" in allE)
93  apply simp
94  (* Go on as usual *)
95  apply (erule exE)
96  apply (drule_tac x = "t'" and P = "\<lambda>t'. \<exists>ex. (t, t') \<in> R \<and> move A ex s' a t'" in someI)
97  apply (erule exE)
98  apply (erule conjE)
99  apply (simp add: Let_def)
100  apply (rule_tac x = "ex" in someI)
101  apply assumption
102  done
103
104lemma move_subprop1_sim:
105  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
106    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
107    in is_exec_frag A (s', SOME x. move A x s' a T')"
108  apply (cut_tac move_is_move_sim)
109  defer
110  apply assumption+
111  apply (simp add: move_def)
112  done
113
114lemma move_subprop2_sim:
115  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
116    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
117    in Finite (SOME x. move A x s' a T')"
118  apply (cut_tac move_is_move_sim)
119  defer
120  apply assumption+
121  apply (simp add: move_def)
122  done
123
124lemma move_subprop3_sim:
125  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
126    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
127    in laststate (s', SOME x. move A x s' a T') = T'"
128  apply (cut_tac move_is_move_sim)
129  defer
130  apply assumption+
131  apply (simp add: move_def)
132  done
133
134lemma move_subprop4_sim:
135  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
136    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
137    in mk_trace A \<cdot> (SOME x. move A x s' a T') = (if a \<in> ext A then a \<leadsto> nil else nil)"
138  apply (cut_tac move_is_move_sim)
139  defer
140  apply assumption+
141  apply (simp add: move_def)
142  done
143
144lemma move_subprop5_sim:
145  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
146    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
147    in (t, T') \<in> R"
148  apply (cut_tac move_is_move_sim)
149  defer
150  apply assumption+
151  apply (simp add: move_def)
152  done
153
154
155subsection \<open>TRACE INCLUSION Part 1: Traces coincide\<close>
156
157subsubsection "Lemmata for <=="
158
159text \<open>Lemma 1: Traces coincide\<close>
160
161lemma traces_coincide_sim [rule_format (no_asm)]:
162  "is_simulation R C A \<Longrightarrow> ext C = ext A \<Longrightarrow>
163    \<forall>s s'. reachable C s \<and> is_exec_frag C (s, ex) \<and> (s, s') \<in> R \<longrightarrow>
164      mk_trace C \<cdot> ex = mk_trace A \<cdot> ((corresp_ex_simC A R \<cdot> ex) s')"
165  supply if_split [split del]
166  apply (pair_induct ex simp: is_exec_frag_def)
167  text \<open>cons case\<close>
168  apply auto
169  apply (rename_tac ex a t s s')
170  apply (simp add: mk_traceConc)
171  apply (frule reachable.reachable_n)
172  apply assumption
173  apply (erule_tac x = "t" in allE)
174  apply (erule_tac x = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in allE)
175  apply (simp add: move_subprop5_sim [unfolded Let_def]
176    move_subprop4_sim [unfolded Let_def] split: if_split)
177  done
178
179text \<open>Lemma 2: \<open>corresp_ex_sim\<close> is execution\<close>
180
181lemma correspsim_is_execution [rule_format]:
182  "is_simulation R C A \<Longrightarrow>
183    \<forall>s s'. reachable C s \<and> is_exec_frag C (s, ex) \<and> (s, s') \<in> R
184      \<longrightarrow> is_exec_frag A (s', (corresp_ex_simC A R \<cdot> ex) s')"
185  apply (pair_induct ex simp: is_exec_frag_def)
186  text \<open>main case\<close>
187  apply auto
188  apply (rename_tac ex a t s s')
189  apply (rule_tac t = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in lemma_2_1)
190
191  text \<open>Finite\<close>
192  apply (erule move_subprop2_sim [unfolded Let_def])
193  apply assumption+
194  apply (rule conjI)
195
196  text \<open>\<open>is_exec_frag\<close>\<close>
197  apply (erule move_subprop1_sim [unfolded Let_def])
198  apply assumption+
199  apply (rule conjI)
200
201  text \<open>Induction hypothesis\<close>
202  text \<open>\<open>reachable_n\<close> looping, therefore apply it manually\<close>
203  apply (erule_tac x = "t" in allE)
204  apply (erule_tac x = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in allE)
205  apply simp
206  apply (frule reachable.reachable_n)
207  apply assumption
208  apply (simp add: move_subprop5_sim [unfolded Let_def])
209  text \<open>laststate\<close>
210  apply (erule move_subprop3_sim [unfolded Let_def, symmetric])
211  apply assumption+
212  done
213
214
215subsection \<open>Main Theorem: TRACE - INCLUSION\<close>
216
217text \<open>
218  Generate condition \<open>(s, S') \<in> R \<and> S' \<in> starts_of A\<close>, the first being
219  interesting for the induction cases concerning the two lemmas
220  \<open>correpsim_is_execution\<close> and \<open>traces_coincide_sim\<close>, the second for the start
221  state case.
222  \<open>S' := SOME s'. (s, s') \<in> R \<and> s' \<in> starts_of A\<close>, where \<open>s \<in> starts_of C\<close>
223\<close>
224
225lemma simulation_starts:
226  "is_simulation R C A \<Longrightarrow> s\<in>starts_of C \<Longrightarrow>
227    let S' = SOME s'. (s, s') \<in> R \<and> s' \<in> starts_of A
228    in (s, S') \<in> R \<and> S' \<in> starts_of A"
229  apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def)
230  apply (erule conjE)+
231  apply (erule ballE)
232  prefer 2 apply blast
233  apply (erule exE)
234  apply (rule someI2)
235  apply assumption
236  apply blast
237  done
238
239lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1]
240lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2]
241
242
243lemma trace_inclusion_for_simulations:
244  "ext C = ext A \<Longrightarrow> is_simulation R C A \<Longrightarrow> traces C \<subseteq> traces A"
245  apply (unfold traces_def)
246  apply (simp add: has_trace_def2)
247  apply auto
248
249  text \<open>give execution of abstract automata\<close>
250  apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
251
252  text \<open>Traces coincide, Lemma 1\<close>
253  apply (pair ex)
254  apply (rename_tac s ex)
255  apply (simp add: corresp_ex_sim_def)
256  apply (rule_tac s = "s" in traces_coincide_sim)
257  apply assumption+
258  apply (simp add: executions_def reachable.reachable_0 sim_starts1)
259
260  text \<open>\<open>corresp_ex_sim\<close> is execution, Lemma 2\<close>
261  apply (pair ex)
262  apply (simp add: executions_def)
263  apply (rename_tac s ex)
264
265  text \<open>start state\<close>
266  apply (rule conjI)
267  apply (simp add: sim_starts2 corresp_ex_sim_def)
268
269  text \<open>\<open>is_execution-fragment\<close>\<close>
270  apply (simp add: corresp_ex_sim_def)
271  apply (rule_tac s = s in correspsim_is_execution)
272  apply assumption
273  apply (simp add: reachable.reachable_0 sim_starts1)
274  done
275
276end
277