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