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