1(* 2 Author: Norbert Schirmer 3 Maintainer: Norbert Schirmer, norbert.schirmer at web de 4 License: LGPL 5*) 6 7(* Title: Termination.thy 8 Author: Norbert Schirmer, TU Muenchen 9 10Copyright (C) 2004-2008 Norbert Schirmer 11Some rights reserved, TU Muenchen 12 13This library is free software; you can redistribute it and/or modify 14it under the terms of the GNU Lesser General Public License as 15published by the Free Software Foundation; either version 2.1 of the 16License, or (at your option) any later version. 17 18This library is distributed in the hope that it will be useful, but 19WITHOUT ANY WARRANTY; without even the implied warranty of 20MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 21Lesser General Public License for more details. 22 23You should have received a copy of the GNU Lesser General Public 24License along with this library; if not, write to the Free Software 25Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 26USA 27*) 28section \<open>Terminating Programs\<close> 29 30theory Termination imports Semantic begin 31 32subsection \<open>Inductive Characterisation: \<open>\<Gamma>\<turnstile>c\<down>s\<close>\<close> 33 34inductive "terminates"::"('s,'p,'f) body \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('s,'f) xstate \<Rightarrow> bool" 35 ("_\<turnstile>_ \<down> _" [60,20,60] 89) 36 for \<Gamma>::"('s,'p,'f) body" 37where 38 Skip: "\<Gamma>\<turnstile>Skip \<down>(Normal s)" 39 40| Basic: "\<Gamma>\<turnstile>Basic f \<down>(Normal s)" 41 42| Spec: "\<Gamma>\<turnstile>Spec r \<down>(Normal s)" 43 44| Guard: "\<lbrakk>s\<in>g; \<Gamma>\<turnstile>c\<down>(Normal s)\<rbrakk> 45 \<Longrightarrow> 46 \<Gamma>\<turnstile>Guard f g c\<down>(Normal s)" 47 48| GuardFault: "s\<notin>g 49 \<Longrightarrow> 50 \<Gamma>\<turnstile>Guard f g c\<down>(Normal s)" 51 52 53| Fault [intro,simp]: "\<Gamma>\<turnstile>c\<down>Fault f" 54 55 56| Seq: "\<lbrakk>\<Gamma>\<turnstile>c\<^sub>1\<down>Normal s; \<forall>s'. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>c\<^sub>2\<down>s'\<rbrakk> 57 \<Longrightarrow> 58 \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2\<down>(Normal s)" 59 60| CondTrue: "\<lbrakk>s \<in> b; \<Gamma>\<turnstile>c\<^sub>1\<down>(Normal s)\<rbrakk> 61 \<Longrightarrow> 62 \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2\<down>(Normal s)" 63 64 65| CondFalse: "\<lbrakk>s \<notin> b; \<Gamma>\<turnstile>c\<^sub>2\<down>(Normal s)\<rbrakk> 66 \<Longrightarrow> 67 \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2\<down>(Normal s)" 68 69 70| WhileTrue: "\<lbrakk>s \<in> b; \<Gamma>\<turnstile>c\<down>(Normal s); 71 \<forall>s'. \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>While b c\<down>s'\<rbrakk> 72 \<Longrightarrow> 73 \<Gamma>\<turnstile>While b c\<down>(Normal s)" 74 75| WhileFalse: "\<lbrakk>s \<notin> b\<rbrakk> 76 \<Longrightarrow> 77 \<Gamma>\<turnstile>While b c\<down>(Normal s)" 78 79| Call: "\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>bdy\<down>(Normal s)\<rbrakk> 80 \<Longrightarrow> 81 \<Gamma>\<turnstile>Call p\<down>(Normal s)" 82 83| CallUndefined: "\<lbrakk>\<Gamma> p = None\<rbrakk> 84 \<Longrightarrow> 85 \<Gamma>\<turnstile>Call p\<down>(Normal s)" 86 87| Stuck [intro,simp]: "\<Gamma>\<turnstile>c\<down>Stuck" 88 89| DynCom: "\<lbrakk>\<Gamma>\<turnstile>(c s)\<down>(Normal s)\<rbrakk> 90 \<Longrightarrow> 91 \<Gamma>\<turnstile>DynCom c\<down>(Normal s)" 92 93| Throw: "\<Gamma>\<turnstile>Throw\<down>(Normal s)" 94 95| Abrupt [intro,simp]: "\<Gamma>\<turnstile>c\<down>Abrupt s" 96 97| Catch: "\<lbrakk>\<Gamma>\<turnstile>c\<^sub>1\<down>Normal s; 98 \<forall>s'. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s \<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c\<^sub>2\<down>Normal s'\<rbrakk> 99 \<Longrightarrow> 100 \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2\<down>Normal s" 101 102 103inductive_cases terminates_elim_cases [cases set]: 104 "\<Gamma>\<turnstile>Skip \<down> s" 105 "\<Gamma>\<turnstile>Guard f g c \<down> s" 106 "\<Gamma>\<turnstile>Basic f \<down> s" 107 "\<Gamma>\<turnstile>Spec r \<down> s" 108 "\<Gamma>\<turnstile>Seq c1 c2 \<down> s" 109 "\<Gamma>\<turnstile>Cond b c1 c2 \<down> s" 110 "\<Gamma>\<turnstile>While b c \<down> s" 111 "\<Gamma>\<turnstile>Call p \<down> s" 112 "\<Gamma>\<turnstile>DynCom c \<down> s" 113 "\<Gamma>\<turnstile>Throw \<down> s" 114 "\<Gamma>\<turnstile>Catch c1 c2 \<down> s" 115 116inductive_cases terminates_Normal_elim_cases [cases set]: 117 "\<Gamma>\<turnstile>Skip \<down> Normal s" 118 "\<Gamma>\<turnstile>Guard f g c \<down> Normal s" 119 "\<Gamma>\<turnstile>Basic f \<down> Normal s" 120 "\<Gamma>\<turnstile>Spec r \<down> Normal s" 121 "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s" 122 "\<Gamma>\<turnstile>Cond b c1 c2 \<down> Normal s" 123 "\<Gamma>\<turnstile>While b c \<down> Normal s" 124 "\<Gamma>\<turnstile>Call p \<down> Normal s" 125 "\<Gamma>\<turnstile>DynCom c \<down> Normal s" 126 "\<Gamma>\<turnstile>Throw \<down> Normal s" 127 "\<Gamma>\<turnstile>Catch c1 c2 \<down> Normal s" 128 129lemma terminates_Skip': "\<Gamma>\<turnstile>Skip \<down> s" 130 by (cases s) (auto intro: terminates.intros) 131 132lemma terminates_Call_body: 133 "\<Gamma> p=Some bdy\<Longrightarrow>\<Gamma>\<turnstile>Call p \<down>s = \<Gamma>\<turnstile>(the (\<Gamma> p))\<down>s" 134 by (cases s) 135 (auto elim: terminates_Normal_elim_cases intro: terminates.intros) 136 137lemma terminates_Normal_Call_body: 138 "p \<in> dom \<Gamma> \<Longrightarrow> 139 \<Gamma>\<turnstile>Call p \<down>Normal s = \<Gamma>\<turnstile>(the (\<Gamma> p))\<down>Normal s" 140 by (auto elim: terminates_Normal_elim_cases intro: terminates.intros) 141 142lemma terminates_implies_exec: 143 assumes terminates: "\<Gamma>\<turnstile>c\<down>s" 144 shows "\<exists>t. \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t" 145using terminates 146proof (induct) 147 case Skip thus ?case by (iprover intro: exec.intros) 148next 149 case Basic thus ?case by (iprover intro: exec.intros) 150next 151 case (Spec r s) thus ?case 152 by (cases "\<exists>t. (s,t)\<in> r") (auto intro: exec.intros) 153next 154 case Guard thus ?case by (iprover intro: exec.intros) 155next 156 case GuardFault thus ?case by (iprover intro: exec.intros) 157next 158 case Fault thus ?case by (iprover intro: exec.intros) 159next 160 case Seq thus ?case by (iprover intro: exec_Seq') 161next 162 case CondTrue thus ?case by (iprover intro: exec.intros) 163next 164 case CondFalse thus ?case by (iprover intro: exec.intros) 165next 166 case WhileTrue thus ?case by (iprover intro: exec.intros) 167next 168 case WhileFalse thus ?case by (iprover intro: exec.intros) 169next 170 case (Call p bdy s) 171 then obtain s' where 172 "\<Gamma>\<turnstile>\<langle>bdy,Normal s \<rangle> \<Rightarrow> s'" 173 by iprover 174 moreover have "\<Gamma> p = Some bdy" by fact 175 ultimately show ?case 176 by (cases s') (iprover intro: exec.intros)+ 177next 178 case CallUndefined thus ?case by (iprover intro: exec.intros) 179next 180 case Stuck thus ?case by (iprover intro: exec.intros) 181next 182 case DynCom thus ?case by (iprover intro: exec.intros) 183next 184 case Throw thus ?case by (iprover intro: exec.intros) 185next 186 case Abrupt thus ?case by (iprover intro: exec.intros) 187next 188 case (Catch c1 s c2) 189 then obtain s' where exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'" 190 by iprover 191 thus ?case 192 proof (cases s') 193 case (Normal s'') 194 with exec_c1 show ?thesis by (auto intro!: exec.intros) 195 next 196 case (Abrupt s'') 197 with exec_c1 Catch.hyps 198 obtain t where "\<Gamma>\<turnstile>\<langle>c2,Normal s'' \<rangle> \<Rightarrow> t" 199 by auto 200 with exec_c1 Abrupt show ?thesis by (auto intro: exec.intros) 201 next 202 case Fault 203 with exec_c1 show ?thesis by (auto intro!: exec.CatchMiss) 204 next 205 case Stuck 206 with exec_c1 show ?thesis by (auto intro!: exec.CatchMiss) 207 qed 208qed 209 210lemma terminates_block: 211"\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal (init s); 212 \<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk> 213 \<Longrightarrow> \<Gamma>\<turnstile>block init bdy return c \<down> Normal s" 214apply (unfold block_def) 215apply (fastforce intro: terminates.intros elim!: exec_Normal_elim_cases 216 dest!: not_isAbrD) 217done 218 219lemma terminates_block_elim [cases set, consumes 1]: 220assumes termi: "\<Gamma>\<turnstile>block init bdy return c \<down> Normal s" 221assumes e: "\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal (init s); 222 \<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t) 223 \<rbrakk> \<Longrightarrow> P" 224shows P 225proof - 226 have "\<Gamma>\<turnstile>\<langle>Basic init,Normal s\<rangle> \<Rightarrow> Normal (init s)" 227 by (auto intro: exec.intros) 228 with termi 229 have "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" 230 apply (unfold block_def) 231 apply (elim terminates_Normal_elim_cases) 232 by simp 233 moreover 234 { 235 fix t 236 assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t" 237 have "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)" 238 proof - 239 from exec_bdy 240 have "\<Gamma>\<turnstile>\<langle>Catch (Seq (Basic init) bdy) 241 (Seq (Basic (return s)) Throw),Normal s\<rangle> \<Rightarrow> Normal t" 242 by (fastforce intro: exec.intros) 243 with termi have "\<Gamma>\<turnstile>DynCom (\<lambda>t. Seq (Basic (return s)) (c s t)) \<down> Normal t" 244 apply (unfold block_def) 245 apply (elim terminates_Normal_elim_cases) 246 by simp 247 thus ?thesis 248 apply (elim terminates_Normal_elim_cases) 249 apply (auto intro: exec.intros) 250 done 251 qed 252 } 253 ultimately show P by (iprover intro: e) 254qed 255 256 257lemma terminates_call: 258"\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>bdy \<down> Normal (init s); 259 \<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk> 260 \<Longrightarrow> \<Gamma>\<turnstile>call init p return c \<down> Normal s" 261 apply (unfold call_def) 262 apply (rule terminates_block) 263 apply (iprover intro: terminates.intros) 264 apply (auto elim: exec_Normal_elim_cases) 265 done 266 267lemma terminates_callUndefined: 268"\<lbrakk>\<Gamma> p = None\<rbrakk> 269 \<Longrightarrow> \<Gamma>\<turnstile>call init p return result \<down> Normal s" 270 apply (unfold call_def) 271 apply (rule terminates_block) 272 apply (iprover intro: terminates.intros) 273 apply (auto elim: exec_Normal_elim_cases) 274 done 275 276lemma terminates_call_elim [cases set, consumes 1]: 277assumes termi: "\<Gamma>\<turnstile>call init p return c \<down> Normal s" 278assumes bdy: "\<And>bdy. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>bdy \<down> Normal (init s); 279 \<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk> \<Longrightarrow> P" 280assumes undef: "\<lbrakk>\<Gamma> p = None\<rbrakk> \<Longrightarrow> P" 281shows P 282apply (cases "\<Gamma> p") 283apply (erule undef) 284using termi 285apply (unfold call_def) 286apply (erule terminates_block_elim) 287apply (erule terminates_Normal_elim_cases) 288apply simp 289apply (frule (1) bdy) 290apply (fastforce intro: exec.intros) 291apply assumption 292apply simp 293done 294 295lemma terminates_dynCall: 296"\<lbrakk>\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s\<rbrakk> 297 \<Longrightarrow> \<Gamma>\<turnstile>dynCall init p return c \<down> Normal s" 298 apply (unfold dynCall_def) 299 apply (auto intro: terminates.intros terminates_call) 300 done 301 302lemma terminates_dynCall_elim [cases set, consumes 1]: 303assumes termi: "\<Gamma>\<turnstile>dynCall init p return c \<down> Normal s" 304assumes "\<lbrakk>\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s\<rbrakk> \<Longrightarrow> P" 305shows P 306using termi 307apply (unfold dynCall_def) 308apply (elim terminates_Normal_elim_cases) 309apply fact 310done 311 312 313(* ************************************************************************* *) 314subsection \<open>Lemmas about @{const "sequence"}, @{const "flatten"} and 315 @{const "normalize"}\<close> 316(* ************************************************************************ *) 317 318lemma terminates_sequence_app: 319 "\<And>s. \<lbrakk>\<Gamma>\<turnstile>sequence Seq xs \<down> Normal s; 320 \<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq xs,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>sequence Seq ys \<down> s'\<rbrakk> 321\<Longrightarrow> \<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> Normal s" 322proof (induct xs) 323 case Nil 324 thus ?case by (auto intro: exec.intros) 325next 326 case (Cons x xs) 327 have termi_x_xs: "\<Gamma>\<turnstile>sequence Seq (x # xs) \<down> Normal s" by fact 328 have termi_ys: "\<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq (x # xs),Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>sequence Seq ys \<down> s'" by fact 329 show ?case 330 proof (cases xs) 331 case Nil 332 with termi_x_xs termi_ys show ?thesis 333 by (cases ys) (auto intro: terminates.intros) 334 next 335 case Cons 336 from termi_x_xs Cons 337 have "\<Gamma>\<turnstile>x \<down> Normal s" 338 by (auto elim: terminates_Normal_elim_cases) 339 moreover 340 { 341 fix s' 342 assume exec_x: "\<Gamma>\<turnstile>\<langle>x,Normal s \<rangle> \<Rightarrow> s'" 343 have "\<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> s'" 344 proof - 345 from exec_x termi_x_xs Cons 346 have termi_xs: "\<Gamma>\<turnstile>sequence Seq xs \<down> s'" 347 by (auto elim: terminates_Normal_elim_cases) 348 show ?thesis 349 proof (cases s') 350 case (Normal s'') 351 with exec_x termi_ys Cons 352 have "\<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq xs,Normal s'' \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>sequence Seq ys \<down> s'" 353 by (auto intro: exec.intros) 354 from Cons.hyps [OF termi_xs [simplified Normal] this] 355 have "\<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> Normal s''". 356 with Normal show ?thesis by simp 357 next 358 case Abrupt thus ?thesis by (auto intro: terminates.intros) 359 next 360 case Fault thus ?thesis by (auto intro: terminates.intros) 361 next 362 case Stuck thus ?thesis by (auto intro: terminates.intros) 363 qed 364 qed 365 } 366 ultimately show ?thesis 367 using Cons 368 by (auto intro: terminates.intros) 369 qed 370qed 371 372lemma terminates_sequence_appD: 373 "\<And>s. \<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> Normal s 374 \<Longrightarrow> \<Gamma>\<turnstile>sequence Seq xs \<down> Normal s \<and> 375 (\<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq xs,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>sequence Seq ys \<down> s')" 376proof (induct xs) 377 case Nil 378 thus ?case 379 by (auto elim: terminates_Normal_elim_cases exec_Normal_elim_cases 380 intro: terminates.intros) 381next 382 case (Cons x xs) 383 have termi_x_xs_ys: "\<Gamma>\<turnstile>sequence Seq ((x # xs) @ ys) \<down> Normal s" by fact 384 show ?case 385 proof (cases xs) 386 case Nil 387 with termi_x_xs_ys show ?thesis 388 by (cases ys) 389 (auto elim: terminates_Normal_elim_cases exec_Normal_elim_cases 390 intro: terminates_Skip') 391 next 392 case Cons 393 with termi_x_xs_ys 394 obtain termi_x: "\<Gamma>\<turnstile>x \<down> Normal s" and 395 termi_xs_ys: "\<forall>s'. \<Gamma>\<turnstile>\<langle>x,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>sequence Seq (xs@ys) \<down> s'" 396 by (auto elim: terminates_Normal_elim_cases) 397 398 have "\<Gamma>\<turnstile>Seq x (sequence Seq xs) \<down> Normal s" 399 proof (rule terminates.Seq [rule_format]) 400 show "\<Gamma>\<turnstile>x \<down> Normal s" by (rule termi_x) 401 next 402 fix s' 403 assume exec_x: "\<Gamma>\<turnstile>\<langle>x,Normal s \<rangle> \<Rightarrow> s'" 404 show "\<Gamma>\<turnstile>sequence Seq xs \<down> s'" 405 proof - 406 from termi_xs_ys [rule_format, OF exec_x] 407 have termi_xs_ys': "\<Gamma>\<turnstile>sequence Seq (xs@ys) \<down> s'" . 408 show ?thesis 409 proof (cases s') 410 case (Normal s'') 411 from Cons.hyps [OF termi_xs_ys' [simplified Normal]] 412 show ?thesis 413 using Normal by auto 414 next 415 case Abrupt thus ?thesis by (auto intro: terminates.intros) 416 next 417 case Fault thus ?thesis by (auto intro: terminates.intros) 418 next 419 case Stuck thus ?thesis by (auto intro: terminates.intros) 420 qed 421 qed 422 qed 423 moreover 424 { 425 fix s' 426 assume exec_x_xs: "\<Gamma>\<turnstile>\<langle>Seq x (sequence Seq xs),Normal s \<rangle> \<Rightarrow> s'" 427 have "\<Gamma>\<turnstile>sequence Seq ys \<down> s'" 428 proof - 429 from exec_x_xs obtain t where 430 exec_x: "\<Gamma>\<turnstile>\<langle>x,Normal s \<rangle> \<Rightarrow> t" and 431 exec_xs: "\<Gamma>\<turnstile>\<langle>sequence Seq xs,t \<rangle> \<Rightarrow> s'" 432 by cases 433 show ?thesis 434 proof (cases t) 435 case (Normal t') 436 with exec_x termi_xs_ys have "\<Gamma>\<turnstile>sequence Seq (xs@ys) \<down> Normal t'" 437 by auto 438 from Cons.hyps [OF this] exec_xs Normal 439 show ?thesis 440 by auto 441 next 442 case (Abrupt t') 443 with exec_xs have "s'=Abrupt t'" 444 by (auto dest: Abrupt_end) 445 thus ?thesis by (auto intro: terminates.intros) 446 next 447 case (Fault f) 448 with exec_xs have "s'=Fault f" 449 by (auto dest: Fault_end) 450 thus ?thesis by (auto intro: terminates.intros) 451 next 452 case Stuck 453 with exec_xs have "s'=Stuck" 454 by (auto dest: Stuck_end) 455 thus ?thesis by (auto intro: terminates.intros) 456 qed 457 qed 458 } 459 ultimately show ?thesis 460 using Cons 461 by auto 462 qed 463qed 464 465lemma terminates_sequence_appE [consumes 1]: 466 "\<lbrakk>\<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> Normal s; 467 \<lbrakk>\<Gamma>\<turnstile>sequence Seq xs \<down> Normal s; 468 \<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq xs,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>sequence Seq ys \<down> s'\<rbrakk> \<Longrightarrow> P\<rbrakk> 469 \<Longrightarrow> P" 470 by (auto dest: terminates_sequence_appD) 471 472lemma terminates_to_terminates_sequence_flatten: 473 assumes termi: "\<Gamma>\<turnstile>c\<down>s" 474 shows "\<Gamma>\<turnstile>sequence Seq (flatten c)\<down>s" 475using termi 476by (induct) 477 (auto intro: terminates.intros terminates_sequence_app 478 exec_sequence_flatten_to_exec) 479 480lemma terminates_to_terminates_normalize: 481 assumes termi: "\<Gamma>\<turnstile>c\<down>s" 482 shows "\<Gamma>\<turnstile>normalize c\<down>s" 483using termi 484proof induct 485 case Seq 486 thus ?case 487 by (fastforce intro: terminates.intros terminates_sequence_app 488 terminates_to_terminates_sequence_flatten 489 dest: exec_sequence_flatten_to_exec exec_normalize_to_exec) 490next 491 case WhileTrue 492 thus ?case 493 by (fastforce intro: terminates.intros terminates_sequence_app 494 terminates_to_terminates_sequence_flatten 495 dest: exec_sequence_flatten_to_exec exec_normalize_to_exec) 496next 497 case Catch 498 thus ?case 499 by (fastforce intro: terminates.intros terminates_sequence_app 500 terminates_to_terminates_sequence_flatten 501 dest: exec_sequence_flatten_to_exec exec_normalize_to_exec) 502qed (auto intro: terminates.intros) 503 504lemma terminates_sequence_flatten_to_terminates: 505 shows "\<And>s. \<Gamma>\<turnstile>sequence Seq (flatten c)\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s" 506proof (induct c) 507 case (Seq c1 c2) 508 have "\<Gamma>\<turnstile>sequence Seq (flatten (Seq c1 c2)) \<down> s" by fact 509 hence termi_app: "\<Gamma>\<turnstile>sequence Seq (flatten c1 @ flatten c2) \<down> s" by simp 510 show ?case 511 proof (cases s) 512 case (Normal s') 513 have "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s'" 514 proof (rule terminates.Seq [rule_format]) 515 from termi_app [simplified Normal] 516 have "\<Gamma>\<turnstile>sequence Seq (flatten c1) \<down> Normal s'" 517 by (cases rule: terminates_sequence_appE) 518 with Seq.hyps 519 show "\<Gamma>\<turnstile>c1 \<down> Normal s'" 520 by simp 521 next 522 fix s'' 523 assume "\<Gamma>\<turnstile>\<langle>c1,Normal s' \<rangle> \<Rightarrow> s''" 524 from termi_app [simplified Normal] exec_to_exec_sequence_flatten [OF this] 525 have "\<Gamma>\<turnstile>sequence Seq (flatten c2) \<down> s''" 526 by (cases rule: terminates_sequence_appE) auto 527 with Seq.hyps 528 show "\<Gamma>\<turnstile>c2 \<down> s''" 529 by simp 530 qed 531 with Normal show ?thesis 532 by simp 533 qed (auto intro: terminates.intros) 534qed (auto intro: terminates.intros) 535 536lemma terminates_normalize_to_terminates: 537 shows "\<And>s. \<Gamma>\<turnstile>normalize c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s" 538proof (induct c) 539 case Skip thus ?case by (auto intro: terminates_Skip') 540next 541 case Basic thus ?case by (cases s) (auto intro: terminates.intros) 542next 543 case Spec thus ?case by (cases s) (auto intro: terminates.intros) 544next 545 case (Seq c1 c2) 546 have "\<Gamma>\<turnstile>normalize (Seq c1 c2) \<down> s" by fact 547 hence termi_app: "\<Gamma>\<turnstile>sequence Seq (flatten (normalize c1) @ flatten (normalize c2)) \<down> s" 548 by simp 549 show ?case 550 proof (cases s) 551 case (Normal s') 552 have "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s'" 553 proof (rule terminates.Seq [rule_format]) 554 from termi_app [simplified Normal] 555 have "\<Gamma>\<turnstile>sequence Seq (flatten (normalize c1)) \<down> Normal s'" 556 by (cases rule: terminates_sequence_appE) 557 from terminates_sequence_flatten_to_terminates [OF this] Seq.hyps 558 show "\<Gamma>\<turnstile>c1 \<down> Normal s'" 559 by simp 560 next 561 fix s'' 562 assume "\<Gamma>\<turnstile>\<langle>c1,Normal s' \<rangle> \<Rightarrow> s''" 563 from exec_to_exec_normalize [OF this] 564 have "\<Gamma>\<turnstile>\<langle>normalize c1,Normal s' \<rangle> \<Rightarrow> s''" . 565 from termi_app [simplified Normal] exec_to_exec_sequence_flatten [OF this] 566 have "\<Gamma>\<turnstile>sequence Seq (flatten (normalize c2)) \<down> s''" 567 by (cases rule: terminates_sequence_appE) auto 568 from terminates_sequence_flatten_to_terminates [OF this] Seq.hyps 569 show "\<Gamma>\<turnstile>c2 \<down> s''" 570 by simp 571 qed 572 with Normal show ?thesis by simp 573 qed (auto intro: terminates.intros) 574next 575 case (Cond b c1 c2) 576 thus ?case 577 by (cases s) 578 (auto intro: terminates.intros elim!: terminates_Normal_elim_cases) 579next 580 case (While b c) 581 have "\<Gamma>\<turnstile>normalize (While b c) \<down> s" by fact 582 hence termi_norm_w: "\<Gamma>\<turnstile>While b (normalize c) \<down> s" by simp 583 { 584 fix t w 585 assume termi_w: "\<Gamma>\<turnstile> w \<down> t" 586 have "w=While b (normalize c) \<Longrightarrow> \<Gamma>\<turnstile>While b c \<down> t" 587 using termi_w 588 proof (induct) 589 case (WhileTrue t' b' c') 590 from WhileTrue obtain 591 t'_b: "t' \<in> b" and 592 termi_norm_c: "\<Gamma>\<turnstile>normalize c \<down> Normal t'" and 593 termi_norm_w': "\<forall>s'. \<Gamma>\<turnstile>\<langle>normalize c,Normal t' \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> s'" 594 by auto 595 from While.hyps [OF termi_norm_c] 596 have "\<Gamma>\<turnstile>c \<down> Normal t'". 597 moreover 598 from termi_norm_w' 599 have "\<forall>s'. \<Gamma>\<turnstile>\<langle>c,Normal t' \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> s'" 600 by (auto intro: exec_to_exec_normalize) 601 ultimately show ?case 602 using t'_b 603 by (auto intro: terminates.intros) 604 qed (auto intro: terminates.intros) 605 } 606 from this [OF termi_norm_w] 607 show ?case 608 by auto 609next 610 case Call thus ?case by simp 611next 612 case DynCom thus ?case 613 by (cases s) (auto intro: terminates.intros rangeI elim: terminates_Normal_elim_cases) 614next 615 case Guard thus ?case 616 by (cases s) (auto intro: terminates.intros elim: terminates_Normal_elim_cases) 617next 618 case Throw thus ?case by (cases s) (auto intro: terminates.intros) 619next 620 case Catch 621 thus ?case 622 by (cases s) 623 (auto dest: exec_to_exec_normalize elim!: terminates_Normal_elim_cases 624 intro!: terminates.Catch) 625qed 626 627lemma terminates_iff_terminates_normalize: 628"\<Gamma>\<turnstile>normalize c\<down>s = \<Gamma>\<turnstile>c\<down>s" 629 by (auto intro: terminates_to_terminates_normalize 630 terminates_normalize_to_terminates) 631 632(* ************************************************************************* *) 633subsection \<open>Lemmas about @{const "strip_guards"}\<close> 634(* ************************************************************************* *) 635 636lemma terminates_strip_guards_to_terminates: "\<And>s. \<Gamma>\<turnstile>strip_guards F c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s" 637proof (induct c) 638 case Skip thus ?case by simp 639next 640 case Basic thus ?case by simp 641next 642 case Spec thus ?case by simp 643next 644 case (Seq c1 c2) 645 hence "\<Gamma>\<turnstile>Seq (strip_guards F c1) (strip_guards F c2) \<down> s" by simp 646 thus "\<Gamma>\<turnstile>Seq c1 c2 \<down> s" 647 proof (cases) 648 fix f assume "s=Fault f" thus ?thesis by simp 649 next 650 assume "s=Stuck" thus ?thesis by simp 651 next 652 fix s' assume "s=Abrupt s'" thus ?thesis by simp 653 next 654 fix s' 655 assume s: "s=Normal s'" 656 assume "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s'" 657 hence "\<Gamma>\<turnstile>c1 \<down> Normal s'" 658 by (rule Seq.hyps) 659 moreover 660 assume c2: 661 "\<forall>s''. \<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s'\<rangle> \<Rightarrow> s'' \<longrightarrow> \<Gamma>\<turnstile>strip_guards F c2\<down>s''" 662 { 663 fix s'' assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s' \<rangle> \<Rightarrow> s''" 664 have " \<Gamma>\<turnstile>c2 \<down> s''" 665 proof (cases s'') 666 case (Normal s''') 667 with exec_c1 668 have "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s' \<rangle> \<Rightarrow> s''" 669 by (auto intro: exec_to_exec_strip_guards) 670 with c2 671 show ?thesis 672 by (iprover intro: Seq.hyps) 673 next 674 case (Abrupt s''') 675 with exec_c1 676 have "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s' \<rangle> \<Rightarrow> s''" 677 by (auto intro: exec_to_exec_strip_guards ) 678 with c2 679 show ?thesis 680 by (iprover intro: Seq.hyps) 681 next 682 case Fault thus ?thesis by simp 683 next 684 case Stuck thus ?thesis by simp 685 qed 686 } 687 ultimately show ?thesis 688 using s 689 by (iprover intro: terminates.intros) 690 qed 691next 692 case (Cond b c1 c2) 693 hence "\<Gamma>\<turnstile>Cond b (strip_guards F c1) (strip_guards F c2) \<down> s" by simp 694 thus "\<Gamma>\<turnstile>Cond b c1 c2 \<down> s" 695 proof (cases) 696 fix f assume "s=Fault f" thus ?thesis by simp 697 next 698 assume "s=Stuck" thus ?thesis by simp 699 next 700 fix s' assume "s=Abrupt s'" thus ?thesis by simp 701 next 702 fix s' 703 assume "s'\<in>b" "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s'" "s = Normal s'" 704 thus ?thesis 705 by (iprover intro: terminates.intros Cond.hyps) 706 next 707 fix s' 708 assume "s'\<notin>b" "\<Gamma>\<turnstile>strip_guards F c2 \<down> Normal s'" "s = Normal s'" 709 thus ?thesis 710 by (iprover intro: terminates.intros Cond.hyps) 711 qed 712next 713 case (While b c) 714 have hyp_c: "\<And>s. \<Gamma>\<turnstile>strip_guards F c \<down> s \<Longrightarrow> \<Gamma>\<turnstile>c \<down> s" by fact 715 have "\<Gamma>\<turnstile>While b (strip_guards F c) \<down> s" using While.prems by simp 716 moreover 717 { 718 fix sw 719 assume "\<Gamma>\<turnstile>sw\<down>s" 720 then have "sw=While b (strip_guards F c) \<Longrightarrow> 721 \<Gamma>\<turnstile>While b c \<down> s" 722 proof (induct) 723 case (WhileTrue s b' c') 724 have eqs: "While b' c' = While b (strip_guards F c)" by fact 725 with \<open>s\<in>b'\<close> have b: "s\<in>b" by simp 726 from eqs \<open>\<Gamma>\<turnstile>c' \<down> Normal s\<close> have "\<Gamma>\<turnstile>strip_guards F c \<down> Normal s" 727 by simp 728 hence term_c: "\<Gamma>\<turnstile>c \<down> Normal s" 729 by (rule hyp_c) 730 moreover 731 { 732 fix t 733 assume exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t" 734 have "\<Gamma>\<turnstile>While b c \<down> t" 735 proof (cases t) 736 case Fault 737 thus ?thesis by simp 738 next 739 case Stuck 740 thus ?thesis by simp 741 next 742 case (Abrupt t') 743 thus ?thesis by simp 744 next 745 case (Normal t') 746 with exec_c 747 have "\<Gamma>\<turnstile>\<langle>strip_guards F c,Normal s \<rangle> \<Rightarrow> Normal t'" 748 by (auto intro: exec_to_exec_strip_guards) 749 with WhileTrue.hyps eqs Normal 750 show ?thesis 751 by fastforce 752 qed 753 } 754 ultimately 755 show ?case 756 using b 757 by (auto intro: terminates.intros) 758 next 759 case WhileFalse thus ?case by (auto intro: terminates.intros) 760 qed simp_all 761 } 762 ultimately show "\<Gamma>\<turnstile>While b c \<down> s" 763 by auto 764next 765 case Call thus ?case by simp 766next 767 case DynCom thus ?case 768 by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros rangeI) 769next 770 case Guard 771 thus ?case 772 by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros 773 split: if_split_asm) 774next 775 case Throw thus ?case by simp 776next 777 case (Catch c1 c2) 778 hence "\<Gamma>\<turnstile>Catch (strip_guards F c1) (strip_guards F c2) \<down> s" by simp 779 thus "\<Gamma>\<turnstile>Catch c1 c2 \<down> s" 780 proof (cases) 781 fix f assume "s=Fault f" thus ?thesis by simp 782 next 783 assume "s=Stuck" thus ?thesis by simp 784 next 785 fix s' assume "s=Abrupt s'" thus ?thesis by simp 786 next 787 fix s' 788 assume s: "s=Normal s'" 789 assume "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s'" 790 hence "\<Gamma>\<turnstile>c1 \<down> Normal s'" 791 by (rule Catch.hyps) 792 moreover 793 assume c2: 794 "\<forall>s''. \<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s'\<rangle> \<Rightarrow> Abrupt s'' 795 \<longrightarrow> \<Gamma>\<turnstile>strip_guards F c2\<down>Normal s''" 796 { 797 fix s'' assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s' \<rangle> \<Rightarrow> Abrupt s''" 798 have " \<Gamma>\<turnstile>c2 \<down> Normal s''" 799 proof - 800 from exec_c1 801 have "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s' \<rangle> \<Rightarrow> Abrupt s''" 802 by (auto intro: exec_to_exec_strip_guards) 803 with c2 804 show ?thesis 805 by (auto intro: Catch.hyps) 806 qed 807 } 808 ultimately show ?thesis 809 using s 810 by (iprover intro: terminates.intros) 811 qed 812qed 813 814lemma terminates_strip_to_terminates: 815 assumes termi_strip: "strip F \<Gamma>\<turnstile>c\<down>s" 816 shows "\<Gamma>\<turnstile>c\<down>s" 817using termi_strip 818proof induct 819 case (Seq c1 s c2) 820 have "\<Gamma>\<turnstile>c1 \<down> Normal s" by fact 821 moreover 822 { 823 fix s' 824 assume exec: "\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> s'" 825 have "\<Gamma>\<turnstile>c2 \<down> s'" 826 proof (cases "isFault s'") 827 case True 828 thus ?thesis 829 by (auto elim: isFaultE) 830 next 831 case False 832 from exec_to_exec_strip [OF exec this] Seq.hyps 833 show ?thesis 834 by auto 835 qed 836 } 837 ultimately show ?case 838 by (auto intro: terminates.intros) 839next 840 case (WhileTrue s b c) 841 have "\<Gamma>\<turnstile>c \<down> Normal s" by fact 842 moreover 843 { 844 fix s' 845 assume exec: "\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'" 846 have "\<Gamma>\<turnstile>While b c \<down> s'" 847 proof (cases "isFault s'") 848 case True 849 thus ?thesis 850 by (auto elim: isFaultE) 851 next 852 case False 853 from exec_to_exec_strip [OF exec this] WhileTrue.hyps 854 show ?thesis 855 by auto 856 qed 857 } 858 ultimately show ?case 859 by (auto intro: terminates.intros) 860next 861 case (Catch c1 s c2) 862 have "\<Gamma>\<turnstile>c1 \<down> Normal s" by fact 863 moreover 864 { 865 fix s' 866 assume exec: "\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> Abrupt s'" 867 from exec_to_exec_strip [OF exec] Catch.hyps 868 have "\<Gamma>\<turnstile>c2 \<down> Normal s'" 869 by auto 870 } 871 ultimately show ?case 872 by (auto intro: terminates.intros) 873next 874 case Call thus ?case 875 by (auto intro: terminates.intros terminates_strip_guards_to_terminates) 876qed (auto intro: terminates.intros) 877 878(* ************************************************************************* *) 879subsection \<open>Lemmas about @{term "c\<^sub>1 \<inter>\<^sub>g c\<^sub>2"}\<close> 880(* ************************************************************************* *) 881 882lemma inter_guards_terminates: 883 "\<And>c c2 s. \<lbrakk>(c1 \<inter>\<^sub>g c2) = Some c; \<Gamma>\<turnstile>c1\<down>s \<rbrakk> 884 \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s" 885proof (induct c1) 886 case Skip thus ?case by (fastforce simp add: inter_guards_Skip) 887next 888 case (Basic f) thus ?case by (fastforce simp add: inter_guards_Basic) 889next 890 case (Spec r) thus ?case by (fastforce simp add: inter_guards_Spec) 891next 892 case (Seq a1 a2) 893 have "(Seq a1 a2 \<inter>\<^sub>g c2) = Some c" by fact 894 then obtain b1 b2 d1 d2 where 895 c2: "c2=Seq b1 b2" and 896 d1: "(a1 \<inter>\<^sub>g b1) = Some d1" and d2: "(a2 \<inter>\<^sub>g b2) = Some d2" and 897 c: "c=Seq d1 d2" 898 by (auto simp add: inter_guards_Seq) 899 have termi_c1: "\<Gamma>\<turnstile>Seq a1 a2 \<down> s" by fact 900 have "\<Gamma>\<turnstile>Seq d1 d2 \<down> s" 901 proof (cases s) 902 case Fault thus ?thesis by simp 903 next 904 case Stuck thus ?thesis by simp 905 next 906 case Abrupt thus ?thesis by simp 907 next 908 case (Normal s') 909 note Normal_s = this 910 with d1 termi_c1 911 have "\<Gamma>\<turnstile>d1 \<down> Normal s'" 912 by (auto elim: terminates_Normal_elim_cases intro: Seq.hyps) 913 moreover 914 { 915 fix t 916 assume exec_d1: "\<Gamma>\<turnstile>\<langle>d1,Normal s' \<rangle> \<Rightarrow> t" 917 have "\<Gamma>\<turnstile>d2 \<down> t" 918 proof (cases t) 919 case Fault thus ?thesis by simp 920 next 921 case Stuck thus ?thesis by simp 922 next 923 case Abrupt thus ?thesis by simp 924 next 925 case (Normal t') 926 with inter_guards_exec_noFault [OF d1 exec_d1] 927 have "\<Gamma>\<turnstile>\<langle>a1,Normal s' \<rangle> \<Rightarrow> Normal t'" 928 by simp 929 with termi_c1 Normal_s have "\<Gamma>\<turnstile>a2 \<down> Normal t'" 930 by (auto elim: terminates_Normal_elim_cases) 931 with d2 have "\<Gamma>\<turnstile>d2 \<down> Normal t'" 932 by (auto intro: Seq.hyps) 933 with Normal show ?thesis by simp 934 qed 935 } 936 ultimately have "\<Gamma>\<turnstile>Seq d1 d2 \<down> Normal s'" 937 by (fastforce intro: terminates.intros) 938 with Normal show ?thesis by simp 939 qed 940 with c show ?case by simp 941next 942 case Cond thus ?case 943 by - (cases s, 944 auto intro: terminates.intros elim!: terminates_Normal_elim_cases 945 simp add: inter_guards_Cond) 946next 947 case (While b bdy1) 948 have "(While b bdy1 \<inter>\<^sub>g c2) = Some c" by fact 949 then obtain bdy2 bdy where 950 c2: "c2=While b bdy2" and 951 bdy: "(bdy1 \<inter>\<^sub>g bdy2) = Some bdy" and 952 c: "c=While b bdy" 953 by (auto simp add: inter_guards_While) 954 have "\<Gamma>\<turnstile>While b bdy1 \<down> s" by fact 955 moreover 956 { 957 fix s w w1 w2 958 assume termi_w: "\<Gamma>\<turnstile>w \<down> s" 959 assume w: "w=While b bdy1" 960 from termi_w w 961 have "\<Gamma>\<turnstile>While b bdy \<down> s" 962 proof (induct) 963 case (WhileTrue s b' bdy1') 964 have eqs: "While b' bdy1' = While b bdy1" by fact 965 from WhileTrue have s_in_b: "s \<in> b" by simp 966 from WhileTrue have termi_bdy1: "\<Gamma>\<turnstile>bdy1 \<down> Normal s" by simp 967 show ?case 968 proof - 969 from bdy termi_bdy1 970 have "\<Gamma>\<turnstile>bdy\<down>(Normal s)" 971 by (rule While.hyps) 972 moreover 973 { 974 fix t 975 assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal s \<rangle> \<Rightarrow> t" 976 have "\<Gamma>\<turnstile>While b bdy\<down>t" 977 proof (cases t) 978 case Fault thus ?thesis by simp 979 next 980 case Stuck thus ?thesis by simp 981 next 982 case Abrupt thus ?thesis by simp 983 next 984 case (Normal t') 985 with inter_guards_exec_noFault [OF bdy exec_bdy] 986 have "\<Gamma>\<turnstile>\<langle>bdy1,Normal s \<rangle> \<Rightarrow> Normal t'" 987 by simp 988 with WhileTrue have "\<Gamma>\<turnstile>While b bdy \<down> Normal t'" 989 by simp 990 with Normal show ?thesis by simp 991 qed 992 } 993 ultimately show ?thesis 994 using s_in_b 995 by (blast intro: terminates.WhileTrue) 996 qed 997 next 998 case WhileFalse thus ?case 999 by (blast intro: terminates.WhileFalse) 1000 qed (simp_all) 1001 } 1002 ultimately 1003 show ?case using c by simp 1004next 1005 case Call thus ?case by (simp add: inter_guards_Call) 1006next 1007 case (DynCom f1) 1008 have "(DynCom f1 \<inter>\<^sub>g c2) = Some c" by fact 1009 then obtain f2 f where 1010 c2: "c2=DynCom f2" and 1011 f_defined: "\<forall>s. ((f1 s) \<inter>\<^sub>g (f2 s)) \<noteq> None" and 1012 c: "c=DynCom (\<lambda>s. the ((f1 s) \<inter>\<^sub>g (f2 s)))" 1013 by (auto simp add: inter_guards_DynCom) 1014 have termi: "\<Gamma>\<turnstile>DynCom f1 \<down> s" by fact 1015 show ?case 1016 proof (cases s) 1017 case Fault thus ?thesis by simp 1018 next 1019 case Stuck thus ?thesis by simp 1020 next 1021 case Abrupt thus ?thesis by simp 1022 next 1023 case (Normal s') 1024 from f_defined obtain f where f: "((f1 s') \<inter>\<^sub>g (f2 s')) = Some f" 1025 by auto 1026 from Normal termi 1027 have "\<Gamma>\<turnstile>f1 s'\<down> (Normal s')" 1028 by (auto elim: terminates_Normal_elim_cases) 1029 from DynCom.hyps f this 1030 have "\<Gamma>\<turnstile>f\<down> (Normal s')" 1031 by blast 1032 with c f Normal 1033 show ?thesis 1034 by (auto intro: terminates.intros) 1035 qed 1036next 1037 case (Guard f g1 bdy1) 1038 have "(Guard f g1 bdy1 \<inter>\<^sub>g c2) = Some c" by fact 1039 then obtain g2 bdy2 bdy where 1040 c2: "c2=Guard f g2 bdy2" and 1041 bdy: "(bdy1 \<inter>\<^sub>g bdy2) = Some bdy" and 1042 c: "c=Guard f (g1 \<inter> g2) bdy" 1043 by (auto simp add: inter_guards_Guard) 1044 have termi_c1: "\<Gamma>\<turnstile>Guard f g1 bdy1 \<down> s" by fact 1045 show ?case 1046 proof (cases s) 1047 case Fault thus ?thesis by simp 1048 next 1049 case Stuck thus ?thesis by simp 1050 next 1051 case Abrupt thus ?thesis by simp 1052 next 1053 case (Normal s') 1054 show ?thesis 1055 proof (cases "s' \<in> g1") 1056 case False 1057 with Normal c show ?thesis by (auto intro: terminates.GuardFault) 1058 next 1059 case True 1060 note s_in_g1 = this 1061 show ?thesis 1062 proof (cases "s' \<in> g2") 1063 case False 1064 with Normal c show ?thesis by (auto intro: terminates.GuardFault) 1065 next 1066 case True 1067 with termi_c1 s_in_g1 Normal have "\<Gamma>\<turnstile>bdy1 \<down> Normal s'" 1068 by (auto elim: terminates_Normal_elim_cases) 1069 with c bdy Guard.hyps Normal True s_in_g1 1070 show ?thesis by (auto intro: terminates.Guard) 1071 qed 1072 qed 1073 qed 1074next 1075 case Throw thus ?case 1076 by (auto simp add: inter_guards_Throw) 1077next 1078 case (Catch a1 a2) 1079 have "(Catch a1 a2 \<inter>\<^sub>g c2) = Some c" by fact 1080 then obtain b1 b2 d1 d2 where 1081 c2: "c2=Catch b1 b2" and 1082 d1: "(a1 \<inter>\<^sub>g b1) = Some d1" and d2: "(a2 \<inter>\<^sub>g b2) = Some d2" and 1083 c: "c=Catch d1 d2" 1084 by (auto simp add: inter_guards_Catch) 1085 have termi_c1: "\<Gamma>\<turnstile>Catch a1 a2 \<down> s" by fact 1086 have "\<Gamma>\<turnstile>Catch d1 d2 \<down> s" 1087 proof (cases s) 1088 case Fault thus ?thesis by simp 1089 next 1090 case Stuck thus ?thesis by simp 1091 next 1092 case Abrupt thus ?thesis by simp 1093 next 1094 case (Normal s') 1095 note Normal_s = this 1096 with d1 termi_c1 1097 have "\<Gamma>\<turnstile>d1 \<down> Normal s'" 1098 by (auto elim: terminates_Normal_elim_cases intro: Catch.hyps) 1099 moreover 1100 { 1101 fix t 1102 assume exec_d1: "\<Gamma>\<turnstile>\<langle>d1,Normal s' \<rangle> \<Rightarrow> Abrupt t" 1103 have "\<Gamma>\<turnstile>d2 \<down> Normal t" 1104 proof - 1105 from inter_guards_exec_noFault [OF d1 exec_d1] 1106 have "\<Gamma>\<turnstile>\<langle>a1,Normal s' \<rangle> \<Rightarrow> Abrupt t" 1107 by simp 1108 with termi_c1 Normal_s have "\<Gamma>\<turnstile>a2 \<down> Normal t" 1109 by (auto elim: terminates_Normal_elim_cases) 1110 with d2 have "\<Gamma>\<turnstile>d2 \<down> Normal t" 1111 by (auto intro: Catch.hyps) 1112 with Normal show ?thesis by simp 1113 qed 1114 } 1115 ultimately have "\<Gamma>\<turnstile>Catch d1 d2 \<down> Normal s'" 1116 by (fastforce intro: terminates.intros) 1117 with Normal show ?thesis by simp 1118 qed 1119 with c show ?case by simp 1120qed 1121 1122lemma inter_guards_terminates': 1123 assumes c: "(c1 \<inter>\<^sub>g c2) = Some c" 1124 assumes termi_c2: "\<Gamma>\<turnstile>c2\<down>s" 1125 shows "\<Gamma>\<turnstile>c\<down>s" 1126proof - 1127 from c have "(c2 \<inter>\<^sub>g c1) = Some c" 1128 by (rule inter_guards_sym) 1129 from this termi_c2 show ?thesis 1130 by (rule inter_guards_terminates) 1131qed 1132 1133(* ************************************************************************* *) 1134subsection \<open>Lemmas about @{const "mark_guards"}\<close> 1135(* ************************************************************************ *) 1136 1137lemma terminates_to_terminates_mark_guards: 1138 assumes termi: "\<Gamma>\<turnstile>c\<down>s" 1139 shows "\<Gamma>\<turnstile>mark_guards f c\<down>s" 1140using termi 1141proof (induct) 1142 case Skip thus ?case by (fastforce intro: terminates.intros) 1143next 1144 case Basic thus ?case by (fastforce intro: terminates.intros) 1145next 1146 case Spec thus ?case by (fastforce intro: terminates.intros) 1147next 1148 case Guard thus ?case by (fastforce intro: terminates.intros) 1149next 1150 case GuardFault thus ?case by (fastforce intro: terminates.intros) 1151next 1152 case Fault thus ?case by (fastforce intro: terminates.intros) 1153next 1154 case (Seq c1 s c2) 1155 have "\<Gamma>\<turnstile>mark_guards f c1 \<down> Normal s" by fact 1156 moreover 1157 { 1158 fix t 1159 assume exec_mark: "\<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> t" 1160 have "\<Gamma>\<turnstile>mark_guards f c2 \<down> t" 1161 proof - 1162 from exec_mark_guards_to_exec [OF exec_mark] obtain t' where 1163 exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t'" and 1164 t_Fault: "isFault t \<longrightarrow> isFault t'" and 1165 t'_Fault_f: "t' = Fault f \<longrightarrow> t' = t" and 1166 t'_Fault: "isFault t' \<longrightarrow> isFault t" and 1167 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t" 1168 by blast 1169 show ?thesis 1170 proof (cases "isFault t'") 1171 case True 1172 with t'_Fault have "isFault t" by simp 1173 thus ?thesis 1174 by (auto elim: isFaultE) 1175 next 1176 case False 1177 with t'_noFault have "t'=t" by simp 1178 with exec_c1 Seq.hyps 1179 show ?thesis 1180 by auto 1181 qed 1182 qed 1183 } 1184 ultimately show ?case 1185 by (auto intro: terminates.intros) 1186next 1187 case CondTrue thus ?case by (fastforce intro: terminates.intros) 1188next 1189 case CondFalse thus ?case by (fastforce intro: terminates.intros) 1190next 1191 case (WhileTrue s b c) 1192 have s_in_b: "s \<in> b" by fact 1193 have "\<Gamma>\<turnstile>mark_guards f c \<down> Normal s" by fact 1194 moreover 1195 { 1196 fix t 1197 assume exec_mark: "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s \<rangle> \<Rightarrow> t" 1198 have "\<Gamma>\<turnstile>mark_guards f (While b c) \<down> t" 1199 proof - 1200 from exec_mark_guards_to_exec [OF exec_mark] obtain t' where 1201 exec_c1: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t'" and 1202 t_Fault: "isFault t \<longrightarrow> isFault t'" and 1203 t'_Fault_f: "t' = Fault f \<longrightarrow> t' = t" and 1204 t'_Fault: "isFault t' \<longrightarrow> isFault t" and 1205 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t" 1206 by blast 1207 show ?thesis 1208 proof (cases "isFault t'") 1209 case True 1210 with t'_Fault have "isFault t" by simp 1211 thus ?thesis 1212 by (auto elim: isFaultE) 1213 next 1214 case False 1215 with t'_noFault have "t'=t" by simp 1216 with exec_c1 WhileTrue.hyps 1217 show ?thesis 1218 by auto 1219 qed 1220 qed 1221 } 1222 ultimately show ?case 1223 by (auto intro: terminates.intros) 1224next 1225 case WhileFalse thus ?case by (fastforce intro: terminates.intros) 1226next 1227 case Call thus ?case by (fastforce intro: terminates.intros) 1228next 1229 case CallUndefined thus ?case by (fastforce intro: terminates.intros) 1230next 1231 case Stuck thus ?case by (fastforce intro: terminates.intros) 1232next 1233 case DynCom thus ?case by (fastforce intro: terminates.intros) 1234next 1235 case Throw thus ?case by (fastforce intro: terminates.intros) 1236next 1237 case Abrupt thus ?case by (fastforce intro: terminates.intros) 1238next 1239 case (Catch c1 s c2) 1240 have "\<Gamma>\<turnstile>mark_guards f c1 \<down> Normal s" by fact 1241 moreover 1242 { 1243 fix t 1244 assume exec_mark: "\<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> Abrupt t" 1245 have "\<Gamma>\<turnstile>mark_guards f c2 \<down> Normal t" 1246 proof - 1247 from exec_mark_guards_to_exec [OF exec_mark] obtain t' where 1248 exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t'" and 1249 t'_Fault_f: "t' = Fault f \<longrightarrow> t' = Abrupt t" and 1250 t'_Fault: "isFault t' \<longrightarrow> isFault (Abrupt t)" and 1251 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = Abrupt t" 1252 by fastforce 1253 show ?thesis 1254 proof (cases "isFault t'") 1255 case True 1256 with t'_Fault have "isFault (Abrupt t)" by simp 1257 thus ?thesis by simp 1258 next 1259 case False 1260 with t'_noFault have "t'=Abrupt t" by simp 1261 with exec_c1 Catch.hyps 1262 show ?thesis 1263 by auto 1264 qed 1265 qed 1266 } 1267 ultimately show ?case 1268 by (auto intro: terminates.intros) 1269qed 1270 1271lemma terminates_mark_guards_to_terminates_Normal: 1272 "\<And>s. \<Gamma>\<turnstile>mark_guards f c\<down>Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>Normal s" 1273proof (induct c) 1274 case Skip thus ?case by (fastforce intro: terminates.intros) 1275next 1276 case Basic thus ?case by (fastforce intro: terminates.intros) 1277next 1278 case Spec thus ?case by (fastforce intro: terminates.intros) 1279next 1280 case (Seq c1 c2) 1281 have "\<Gamma>\<turnstile>mark_guards f (Seq c1 c2) \<down> Normal s" by fact 1282 then obtain 1283 termi_merge_c1: "\<Gamma>\<turnstile>mark_guards f c1 \<down> Normal s" and 1284 termi_merge_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> 1285 \<Gamma>\<turnstile>mark_guards f c2 \<down> s'" 1286 by (auto elim: terminates_Normal_elim_cases) 1287 from termi_merge_c1 Seq.hyps 1288 have "\<Gamma>\<turnstile>c1 \<down> Normal s" by iprover 1289 moreover 1290 { 1291 fix s' 1292 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'" 1293 have "\<Gamma>\<turnstile> c2 \<down> s'" 1294 proof (cases "isFault s'") 1295 case True 1296 thus ?thesis by (auto elim: isFaultE) 1297 next 1298 case False 1299 from exec_to_exec_mark_guards [OF exec_c1 False] 1300 have "\<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> s'" . 1301 from termi_merge_c2 [rule_format, OF this] Seq.hyps 1302 show ?thesis 1303 by (cases s') (auto) 1304 qed 1305 } 1306 ultimately show ?case by (auto intro: terminates.intros) 1307next 1308 case Cond thus ?case 1309 by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) 1310next 1311 case (While b c) 1312 { 1313 fix u c' 1314 assume termi_c': "\<Gamma>\<turnstile>c' \<down> Normal u" 1315 assume c': "c' = mark_guards f (While b c)" 1316 have "\<Gamma>\<turnstile>While b c \<down> Normal u" 1317 using termi_c' c' 1318 proof (induct) 1319 case (WhileTrue s b' c') 1320 have s_in_b: "s \<in> b" using WhileTrue by simp 1321 have "\<Gamma>\<turnstile>mark_guards f c \<down> Normal s" 1322 using WhileTrue by (auto elim: terminates_Normal_elim_cases) 1323 with While.hyps have "\<Gamma>\<turnstile>c \<down> Normal s" 1324 by auto 1325 moreover 1326 have hyp_w: "\<forall>w. \<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s \<rangle> \<Rightarrow> w \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> w" 1327 using WhileTrue by simp 1328 hence "\<forall>w. \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> w \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> w" 1329 apply - 1330 apply (rule allI) 1331 apply (case_tac "w") 1332 apply (auto dest: exec_to_exec_mark_guards) 1333 done 1334 ultimately show ?case 1335 using s_in_b 1336 by (auto intro: terminates.intros) 1337 next 1338 case WhileFalse thus ?case by (auto intro: terminates.intros) 1339 qed auto 1340 } 1341 with While show ?case by simp 1342next 1343 case Call thus ?case 1344 by (fastforce intro: terminates.intros ) 1345next 1346 case DynCom thus ?case 1347 by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) 1348next 1349 case (Guard f g c) 1350 thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) 1351next 1352 case Throw thus ?case 1353 by (fastforce intro: terminates.intros ) 1354next 1355 case (Catch c1 c2) 1356 have "\<Gamma>\<turnstile>mark_guards f (Catch c1 c2) \<down> Normal s" by fact 1357 then obtain 1358 termi_merge_c1: "\<Gamma>\<turnstile>mark_guards f c1 \<down> Normal s" and 1359 termi_merge_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> 1360 \<Gamma>\<turnstile>mark_guards f c2 \<down> Normal s'" 1361 by (auto elim: terminates_Normal_elim_cases) 1362 from termi_merge_c1 Catch.hyps 1363 have "\<Gamma>\<turnstile>c1 \<down> Normal s" by iprover 1364 moreover 1365 { 1366 fix s' 1367 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" 1368 have "\<Gamma>\<turnstile> c2 \<down> Normal s'" 1369 proof - 1370 from exec_to_exec_mark_guards [OF exec_c1] 1371 have "\<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" by simp 1372 from termi_merge_c2 [rule_format, OF this] Catch.hyps 1373 show ?thesis 1374 by iprover 1375 qed 1376 } 1377 ultimately show ?case by (auto intro: terminates.intros) 1378qed 1379 1380lemma terminates_mark_guards_to_terminates: 1381 "\<Gamma>\<turnstile>mark_guards f c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c\<down> s" 1382 by (cases s) (auto intro: terminates_mark_guards_to_terminates_Normal) 1383 1384 1385(* ************************************************************************* *) 1386subsection \<open>Lemmas about @{const "merge_guards"}\<close> 1387(* ************************************************************************ *) 1388 1389lemma terminates_to_terminates_merge_guards: 1390 assumes termi: "\<Gamma>\<turnstile>c\<down>s" 1391 shows "\<Gamma>\<turnstile>merge_guards c\<down>s" 1392using termi 1393proof (induct) 1394 case (Guard s g c f) 1395 have s_in_g: "s \<in> g" by fact 1396 have termi_merge_c: "\<Gamma>\<turnstile>merge_guards c \<down> Normal s" by fact 1397 show ?case 1398 proof (cases "\<exists>f' g' c'. merge_guards c = Guard f' g' c'") 1399 case False 1400 hence "merge_guards (Guard f g c) = Guard f g (merge_guards c)" 1401 by (cases "merge_guards c") (auto simp add: Let_def) 1402 with s_in_g termi_merge_c show ?thesis 1403 by (auto intro: terminates.intros) 1404 next 1405 case True 1406 then obtain f' g' c' where 1407 mc: "merge_guards c = Guard f' g' c'" 1408 by blast 1409 show ?thesis 1410 proof (cases "f=f'") 1411 case False 1412 with mc have "merge_guards (Guard f g c) = Guard f g (merge_guards c)" 1413 by (simp add: Let_def) 1414 with s_in_g termi_merge_c show ?thesis 1415 by (auto intro: terminates.intros) 1416 next 1417 case True 1418 with mc have "merge_guards (Guard f g c) = Guard f (g \<inter> g') c'" 1419 by simp 1420 with s_in_g mc True termi_merge_c 1421 show ?thesis 1422 by (cases "s \<in> g'") 1423 (auto intro: terminates.intros elim: terminates_Normal_elim_cases) 1424 qed 1425 qed 1426next 1427 case (GuardFault s g f c) 1428 have "s \<notin> g" by fact 1429 thus ?case 1430 by (cases "merge_guards c") 1431 (auto intro: terminates.intros split: if_split_asm simp add: Let_def) 1432qed (fastforce intro: terminates.intros dest: exec_merge_guards_to_exec)+ 1433 1434lemma terminates_merge_guards_to_terminates_Normal: 1435 shows "\<And>s. \<Gamma>\<turnstile>merge_guards c\<down>Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>Normal s" 1436proof (induct c) 1437 case Skip thus ?case by (fastforce intro: terminates.intros) 1438next 1439 case Basic thus ?case by (fastforce intro: terminates.intros) 1440next 1441 case Spec thus ?case by (fastforce intro: terminates.intros) 1442next 1443 case (Seq c1 c2) 1444 have "\<Gamma>\<turnstile>merge_guards (Seq c1 c2) \<down> Normal s" by fact 1445 then obtain 1446 termi_merge_c1: "\<Gamma>\<turnstile>merge_guards c1 \<down> Normal s" and 1447 termi_merge_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>merge_guards c1,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> 1448 \<Gamma>\<turnstile>merge_guards c2 \<down> s'" 1449 by (auto elim: terminates_Normal_elim_cases) 1450 from termi_merge_c1 Seq.hyps 1451 have "\<Gamma>\<turnstile>c1 \<down> Normal s" by iprover 1452 moreover 1453 { 1454 fix s' 1455 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'" 1456 have "\<Gamma>\<turnstile> c2 \<down> s'" 1457 proof - 1458 from exec_to_exec_merge_guards [OF exec_c1] 1459 have "\<Gamma>\<turnstile>\<langle>merge_guards c1,Normal s \<rangle> \<Rightarrow> s'" . 1460 from termi_merge_c2 [rule_format, OF this] Seq.hyps 1461 show ?thesis 1462 by (cases s') (auto) 1463 qed 1464 } 1465 ultimately show ?case by (auto intro: terminates.intros) 1466next 1467 case Cond thus ?case 1468 by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) 1469next 1470 case (While b c) 1471 { 1472 fix u c' 1473 assume termi_c': "\<Gamma>\<turnstile>c' \<down> Normal u" 1474 assume c': "c' = merge_guards (While b c)" 1475 have "\<Gamma>\<turnstile>While b c \<down> Normal u" 1476 using termi_c' c' 1477 proof (induct) 1478 case (WhileTrue s b' c') 1479 have s_in_b: "s \<in> b" using WhileTrue by simp 1480 have "\<Gamma>\<turnstile>merge_guards c \<down> Normal s" 1481 using WhileTrue by (auto elim: terminates_Normal_elim_cases) 1482 with While.hyps have "\<Gamma>\<turnstile>c \<down> Normal s" 1483 by auto 1484 moreover 1485 have hyp_w: "\<forall>w. \<Gamma>\<turnstile>\<langle>merge_guards c,Normal s \<rangle> \<Rightarrow> w \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> w" 1486 using WhileTrue by simp 1487 hence "\<forall>w. \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> w \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> w" 1488 by (simp add: exec_iff_exec_merge_guards [symmetric]) 1489 ultimately show ?case 1490 using s_in_b 1491 by (auto intro: terminates.intros) 1492 next 1493 case WhileFalse thus ?case by (auto intro: terminates.intros) 1494 qed auto 1495 } 1496 with While show ?case by simp 1497next 1498 case Call thus ?case 1499 by (fastforce intro: terminates.intros ) 1500next 1501 case DynCom thus ?case 1502 by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) 1503next 1504 case (Guard f g c) 1505 have termi_merge: "\<Gamma>\<turnstile>merge_guards (Guard f g c) \<down> Normal s" by fact 1506 show ?case 1507 proof (cases "\<exists>f' g' c'. merge_guards c = Guard f' g' c'") 1508 case False 1509 hence m: "merge_guards (Guard f g c) = Guard f g (merge_guards c)" 1510 by (cases "merge_guards c") (auto simp add: Let_def) 1511 from termi_merge Guard.hyps show ?thesis 1512 by (simp only: m) 1513 (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) 1514 next 1515 case True 1516 then obtain f' g' c' where 1517 mc: "merge_guards c = Guard f' g' c'" 1518 by blast 1519 show ?thesis 1520 proof (cases "f=f'") 1521 case False 1522 with mc have m: "merge_guards (Guard f g c) = Guard f g (merge_guards c)" 1523 by (simp add: Let_def) 1524 from termi_merge Guard.hyps show ?thesis 1525 by (simp only: m) 1526 (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) 1527 next 1528 case True 1529 with mc have m: "merge_guards (Guard f g c) = Guard f (g \<inter> g') c'" 1530 by simp 1531 from termi_merge Guard.hyps 1532 show ?thesis 1533 by (simp only: m mc) 1534 (auto intro: terminates.intros elim: terminates_Normal_elim_cases) 1535 qed 1536 qed 1537next 1538 case Throw thus ?case 1539 by (fastforce intro: terminates.intros ) 1540next 1541 case (Catch c1 c2) 1542 have "\<Gamma>\<turnstile>merge_guards (Catch c1 c2) \<down> Normal s" by fact 1543 then obtain 1544 termi_merge_c1: "\<Gamma>\<turnstile>merge_guards c1 \<down> Normal s" and 1545 termi_merge_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>merge_guards c1,Normal s \<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> 1546 \<Gamma>\<turnstile>merge_guards c2 \<down> Normal s'" 1547 by (auto elim: terminates_Normal_elim_cases) 1548 from termi_merge_c1 Catch.hyps 1549 have "\<Gamma>\<turnstile>c1 \<down> Normal s" by iprover 1550 moreover 1551 { 1552 fix s' 1553 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" 1554 have "\<Gamma>\<turnstile> c2 \<down> Normal s'" 1555 proof - 1556 from exec_to_exec_merge_guards [OF exec_c1] 1557 have "\<Gamma>\<turnstile>\<langle>merge_guards c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" . 1558 from termi_merge_c2 [rule_format, OF this] Catch.hyps 1559 show ?thesis 1560 by iprover 1561 qed 1562 } 1563 ultimately show ?case by (auto intro: terminates.intros) 1564qed 1565 1566lemma terminates_merge_guards_to_terminates: 1567 "\<Gamma>\<turnstile>merge_guards c\<down> s \<Longrightarrow> \<Gamma>\<turnstile>c\<down> s" 1568by (cases s) (auto intro: terminates_merge_guards_to_terminates_Normal) 1569 1570theorem terminates_iff_terminates_merge_guards: 1571 "\<Gamma>\<turnstile>c\<down> s = \<Gamma>\<turnstile>merge_guards c\<down> s" 1572 by (iprover intro: terminates_to_terminates_merge_guards 1573 terminates_merge_guards_to_terminates) 1574 1575(* ************************************************************************* *) 1576subsection \<open>Lemmas about @{term "c\<^sub>1 \<subseteq>\<^sub>g c\<^sub>2"}\<close> 1577(* ************************************************************************ *) 1578 1579lemma terminates_fewer_guards_Normal: 1580 shows "\<And>c s. \<lbrakk>\<Gamma>\<turnstile>c'\<down>Normal s; c \<subseteq>\<^sub>g c'; \<Gamma>\<turnstile>\<langle>c',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV\<rbrakk> 1581 \<Longrightarrow> \<Gamma>\<turnstile>c\<down>Normal s" 1582proof (induct c') 1583 case Skip thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD) 1584next 1585 case Basic thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD) 1586next 1587 case Spec thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD) 1588next 1589 case (Seq c1' c2') 1590 have termi: "\<Gamma>\<turnstile>Seq c1' c2' \<down> Normal s" by fact 1591 then obtain 1592 termi_c1': "\<Gamma>\<turnstile>c1'\<down> Normal s" and 1593 termi_c2': "\<forall>s'. \<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>c2'\<down> s'" 1594 by (auto elim: terminates_Normal_elim_cases) 1595 have noFault: "\<Gamma>\<turnstile>\<langle>Seq c1' c2',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact 1596 hence noFault_c1': "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1597 by (auto intro: exec.intros simp add: final_notin_def) 1598 have "c \<subseteq>\<^sub>g Seq c1' c2'" by fact 1599 from subseteq_guards_Seq [OF this] obtain c1 c2 where 1600 c: "c = Seq c1 c2" and 1601 c1_c1': "c1 \<subseteq>\<^sub>g c1'" and 1602 c2_c2': "c2 \<subseteq>\<^sub>g c2'" 1603 by blast 1604 from termi_c1' c1_c1' noFault_c1' 1605 have "\<Gamma>\<turnstile>c1\<down> Normal s" 1606 by (rule Seq.hyps) 1607 moreover 1608 { 1609 fix t 1610 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t" 1611 have "\<Gamma>\<turnstile>c2\<down> t" 1612 proof - 1613 from exec_to_exec_subseteq_guards [OF c1_c1' exec_c1] obtain t' where 1614 exec_c1': "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow> t'" and 1615 t_Fault: "isFault t \<longrightarrow> isFault t'" and 1616 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t" 1617 by blast 1618 show ?thesis 1619 proof (cases "isFault t'") 1620 case True 1621 with exec_c1' noFault_c1' 1622 have False 1623 by (fastforce elim: isFaultE dest: Fault_end simp add: final_notin_def) 1624 thus ?thesis .. 1625 next 1626 case False 1627 with t'_noFault have t': "t'=t" by simp 1628 with termi_c2' exec_c1' 1629 have termi_c2': "\<Gamma>\<turnstile>c2'\<down> t" 1630 by auto 1631 show ?thesis 1632 proof (cases t) 1633 case Fault thus ?thesis by auto 1634 next 1635 case Abrupt thus ?thesis by auto 1636 next 1637 case Stuck thus ?thesis by auto 1638 next 1639 case (Normal u) 1640 with noFault exec_c1' t' 1641 have "\<Gamma>\<turnstile>\<langle>c2',Normal u \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1642 by (auto intro: exec.intros simp add: final_notin_def) 1643 from termi_c2' [simplified Normal] c2_c2' this 1644 have "\<Gamma>\<turnstile>c2 \<down> Normal u" 1645 by (rule Seq.hyps) 1646 with Normal exec_c1 1647 show ?thesis by simp 1648 qed 1649 qed 1650 qed 1651 } 1652 ultimately show ?case using c by (auto intro: terminates.intros) 1653next 1654 case (Cond b c1' c2') 1655 have noFault: "\<Gamma>\<turnstile>\<langle>Cond b c1' c2',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact 1656 have termi: "\<Gamma>\<turnstile>Cond b c1' c2' \<down> Normal s" by fact 1657 have "c \<subseteq>\<^sub>g Cond b c1' c2'" by fact 1658 from subseteq_guards_Cond [OF this] obtain c1 c2 where 1659 c: "c = Cond b c1 c2" and 1660 c1_c1': "c1 \<subseteq>\<^sub>g c1'" and 1661 c2_c2': "c2 \<subseteq>\<^sub>g c2'" 1662 by blast 1663 thus ?case 1664 proof (cases "s \<in> b") 1665 case True 1666 with termi have termi_c1': "\<Gamma>\<turnstile>c1' \<down> Normal s" 1667 by (auto elim: terminates_Normal_elim_cases) 1668 from True noFault have "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1669 by (auto intro: exec.intros simp add: final_notin_def) 1670 from termi_c1' c1_c1' this 1671 have "\<Gamma>\<turnstile>c1 \<down> Normal s" 1672 by (rule Cond.hyps) 1673 with True c show ?thesis 1674 by (auto intro: terminates.intros) 1675 next 1676 case False 1677 with termi have termi_c2': "\<Gamma>\<turnstile>c2' \<down> Normal s" 1678 by (auto elim: terminates_Normal_elim_cases) 1679 from False noFault have "\<Gamma>\<turnstile>\<langle>c2',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1680 by (auto intro: exec.intros simp add: final_notin_def) 1681 from termi_c2' c2_c2' this 1682 have "\<Gamma>\<turnstile>c2 \<down> Normal s" 1683 by (rule Cond.hyps) 1684 with False c show ?thesis 1685 by (auto intro: terminates.intros) 1686 qed 1687next 1688 case (While b c') 1689 have noFault: "\<Gamma>\<turnstile>\<langle>While b c',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact 1690 have termi: "\<Gamma>\<turnstile>While b c' \<down> Normal s" by fact 1691 have "c \<subseteq>\<^sub>g While b c'" by fact 1692 from subseteq_guards_While [OF this] 1693 obtain c'' where 1694 c: "c = While b c''" and 1695 c''_c': "c'' \<subseteq>\<^sub>g c'" 1696 by blast 1697 { 1698 fix d u 1699 assume termi: "\<Gamma>\<turnstile>d \<down> u" 1700 assume d: "d = While b c'" 1701 assume noFault: "\<Gamma>\<turnstile>\<langle>While b c',u \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1702 have "\<Gamma>\<turnstile>While b c'' \<down> u" 1703 using termi d noFault 1704 proof (induct) 1705 case (WhileTrue u b' c''') 1706 have u_in_b: "u \<in> b" using WhileTrue by simp 1707 have termi_c': "\<Gamma>\<turnstile>c' \<down> Normal u" using WhileTrue by simp 1708 have noFault: "\<Gamma>\<turnstile>\<langle>While b c',Normal u \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" using WhileTrue by simp 1709 hence noFault_c': "\<Gamma>\<turnstile>\<langle>c',Normal u \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" using u_in_b 1710 by (auto intro: exec.intros simp add: final_notin_def) 1711 from While.hyps [OF termi_c' c''_c' this] 1712 have "\<Gamma>\<turnstile>c'' \<down> Normal u". 1713 moreover 1714 from WhileTrue 1715 have hyp_w: "\<forall>s'. \<Gamma>\<turnstile>\<langle>c',Normal u \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>\<langle>While b c',s' \<rangle> \<Rightarrow>\<notin>Fault ` UNIV 1716 \<longrightarrow> \<Gamma>\<turnstile>While b c'' \<down> s'" 1717 by simp 1718 { 1719 fix v 1720 assume exec_c'': "\<Gamma>\<turnstile>\<langle>c'',Normal u \<rangle> \<Rightarrow> v" 1721 have "\<Gamma>\<turnstile>While b c'' \<down> v" 1722 proof - 1723 from exec_to_exec_subseteq_guards [OF c''_c' exec_c''] obtain v' where 1724 exec_c': "\<Gamma>\<turnstile>\<langle>c',Normal u \<rangle> \<Rightarrow> v'" and 1725 v_Fault: "isFault v \<longrightarrow> isFault v'" and 1726 v'_noFault: "\<not> isFault v' \<longrightarrow> v' = v" 1727 by auto 1728 show ?thesis 1729 proof (cases "isFault v'") 1730 case True 1731 with exec_c' noFault u_in_b 1732 have False 1733 by (fastforce 1734 simp add: final_notin_def intro: exec.intros elim: isFaultE) 1735 thus ?thesis .. 1736 next 1737 case False 1738 with v'_noFault have v': "v'=v" 1739 by simp 1740 with noFault exec_c' u_in_b 1741 have "\<Gamma>\<turnstile>\<langle>While b c',v \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1742 by (fastforce simp add: final_notin_def intro: exec.intros) 1743 from hyp_w [rule_format, OF exec_c' [simplified v'] this] 1744 show "\<Gamma>\<turnstile>While b c'' \<down> v" . 1745 qed 1746 qed 1747 } 1748 ultimately 1749 show ?case using u_in_b 1750 by (auto intro: terminates.intros) 1751 next 1752 case WhileFalse thus ?case by (auto intro: terminates.intros) 1753 qed auto 1754 } 1755 with c noFault termi show ?case 1756 by auto 1757next 1758 case Call thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD) 1759next 1760 case (DynCom C') 1761 have termi: "\<Gamma>\<turnstile>DynCom C' \<down> Normal s" by fact 1762 hence termi_C': "\<Gamma>\<turnstile>C' s \<down> Normal s" 1763 by cases 1764 have noFault: "\<Gamma>\<turnstile>\<langle>DynCom C',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact 1765 hence noFault_C': "\<Gamma>\<turnstile>\<langle>C' s,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1766 by (auto intro: exec.intros simp add: final_notin_def) 1767 have "c \<subseteq>\<^sub>g DynCom C'" by fact 1768 from subseteq_guards_DynCom [OF this] obtain C where 1769 c: "c = DynCom C" and 1770 C_C': "\<forall>s. C s \<subseteq>\<^sub>g C' s" 1771 by blast 1772 from DynCom.hyps termi_C' C_C' [rule_format] noFault_C' 1773 have "\<Gamma>\<turnstile>C s \<down> Normal s" 1774 by fast 1775 with c show ?case 1776 by (auto intro: terminates.intros) 1777next 1778 case (Guard f' g' c') 1779 have noFault: "\<Gamma>\<turnstile>\<langle>Guard f' g' c',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact 1780 have termi: "\<Gamma>\<turnstile>Guard f' g' c' \<down> Normal s" by fact 1781 have "c \<subseteq>\<^sub>g Guard f' g' c'" by fact 1782 hence c_cases: "(c \<subseteq>\<^sub>g c') \<or> (\<exists>c''. c = Guard f' g' c'' \<and> (c'' \<subseteq>\<^sub>g c'))" 1783 by (rule subseteq_guards_Guard) 1784 thus ?case 1785 proof (cases "s \<in> g'") 1786 case True 1787 note s_in_g' = this 1788 with noFault have noFault_c': "\<Gamma>\<turnstile>\<langle>c',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1789 by (auto simp add: final_notin_def intro: exec.intros) 1790 from termi s_in_g' have termi_c': "\<Gamma>\<turnstile>c' \<down> Normal s" 1791 by cases auto 1792 from c_cases show ?thesis 1793 proof 1794 assume "c \<subseteq>\<^sub>g c'" 1795 from termi_c' this noFault_c' 1796 show "\<Gamma>\<turnstile>c \<down> Normal s" 1797 by (rule Guard.hyps) 1798 next 1799 assume "\<exists>c''. c = Guard f' g' c'' \<and> (c'' \<subseteq>\<^sub>g c')" 1800 then obtain c'' where 1801 c: "c = Guard f' g' c''" and c''_c': "c'' \<subseteq>\<^sub>g c'" 1802 by blast 1803 from termi_c' c''_c' noFault_c' 1804 have "\<Gamma>\<turnstile>c'' \<down> Normal s" 1805 by (rule Guard.hyps) 1806 with s_in_g' c 1807 show ?thesis 1808 by (auto intro: terminates.intros) 1809 qed 1810 next 1811 case False 1812 with noFault have False 1813 by (auto intro: exec.intros simp add: final_notin_def) 1814 thus ?thesis .. 1815 qed 1816next 1817 case Throw thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD) 1818next 1819 case (Catch c1' c2') 1820 have termi: "\<Gamma>\<turnstile>Catch c1' c2' \<down> Normal s" by fact 1821 then obtain 1822 termi_c1': "\<Gamma>\<turnstile>c1'\<down> Normal s" and 1823 termi_c2': "\<forall>s'. \<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c2'\<down> Normal s'" 1824 by (auto elim: terminates_Normal_elim_cases) 1825 have noFault: "\<Gamma>\<turnstile>\<langle>Catch c1' c2',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact 1826 hence noFault_c1': "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1827 by (fastforce intro: exec.intros simp add: final_notin_def) 1828 have "c \<subseteq>\<^sub>g Catch c1' c2'" by fact 1829 from subseteq_guards_Catch [OF this] obtain c1 c2 where 1830 c: "c = Catch c1 c2" and 1831 c1_c1': "c1 \<subseteq>\<^sub>g c1'" and 1832 c2_c2': "c2 \<subseteq>\<^sub>g c2'" 1833 by blast 1834 from termi_c1' c1_c1' noFault_c1' 1835 have "\<Gamma>\<turnstile>c1\<down> Normal s" 1836 by (rule Catch.hyps) 1837 moreover 1838 { 1839 fix t 1840 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt t" 1841 have "\<Gamma>\<turnstile>c2\<down> Normal t" 1842 proof - 1843 from exec_to_exec_subseteq_guards [OF c1_c1' exec_c1] obtain t' where 1844 exec_c1': "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow> t'" and 1845 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = Abrupt t" 1846 by blast 1847 show ?thesis 1848 proof (cases "isFault t'") 1849 case True 1850 with exec_c1' noFault_c1' 1851 have False 1852 by (fastforce elim: isFaultE dest: Fault_end simp add: final_notin_def) 1853 thus ?thesis .. 1854 next 1855 case False 1856 with t'_noFault have t': "t'=Abrupt t" by simp 1857 with termi_c2' exec_c1' 1858 have termi_c2': "\<Gamma>\<turnstile>c2'\<down> Normal t" 1859 by auto 1860 with noFault exec_c1' t' 1861 have "\<Gamma>\<turnstile>\<langle>c2',Normal t \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 1862 by (auto intro: exec.intros simp add: final_notin_def) 1863 from termi_c2' c2_c2' this 1864 show "\<Gamma>\<turnstile>c2 \<down> Normal t" 1865 by (rule Catch.hyps) 1866 qed 1867 qed 1868 } 1869 ultimately show ?case using c by (auto intro: terminates.intros) 1870qed 1871 1872theorem terminates_fewer_guards: 1873 shows "\<lbrakk>\<Gamma>\<turnstile>c'\<down>s; c \<subseteq>\<^sub>g c'; \<Gamma>\<turnstile>\<langle>c',s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV\<rbrakk> 1874 \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s" 1875 by (cases s) (auto intro: terminates_fewer_guards_Normal) 1876 1877lemma terminates_noFault_strip_guards: 1878 assumes termi: "\<Gamma>\<turnstile>c\<down>Normal s" 1879 shows "\<lbrakk>\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>strip_guards F c\<down>Normal s" 1880using termi 1881proof (induct) 1882 case Skip thus ?case by (auto intro: terminates.intros) 1883next 1884 case Basic thus ?case by (auto intro: terminates.intros) 1885next 1886 case Spec thus ?case by (auto intro: terminates.intros) 1887next 1888 case (Guard s g c f) 1889 have s_in_g: "s \<in> g" by fact 1890 have "\<Gamma>\<turnstile>c \<down> Normal s" by fact 1891 have "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 1892 with s_in_g have "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 1893 by (fastforce simp add: final_notin_def intro: exec.intros) 1894 with Guard.hyps have "\<Gamma>\<turnstile>strip_guards F c \<down> Normal s" by simp 1895 with s_in_g show ?case 1896 by (auto intro: terminates.intros) 1897next 1898 case GuardFault thus ?case 1899 by (auto intro: terminates.intros exec.intros simp add: final_notin_def ) 1900next 1901 case Fault thus ?case by (auto intro: terminates.intros) 1902next 1903 case (Seq c1 s c2) 1904 have noFault_Seq: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 1905 hence noFault_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 1906 by (auto simp add: final_notin_def intro: exec.intros) 1907 with Seq.hyps have "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s" by simp 1908 moreover 1909 { 1910 fix s' 1911 assume exec_strip_guards_c1: "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s \<rangle> \<Rightarrow> s'" 1912 have "\<Gamma>\<turnstile>strip_guards F c2 \<down> s'" 1913 proof (cases "isFault s'") 1914 case True 1915 thus ?thesis by (auto elim: isFaultE intro: terminates.intros) 1916 next 1917 case False 1918 with exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1 1919 have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'" 1920 by (auto simp add: final_notin_def elim!: isFaultE) 1921 with noFault_Seq have "\<Gamma>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>Fault ` F" 1922 by (auto simp add: final_notin_def intro: exec.intros) 1923 with * show ?thesis 1924 using Seq.hyps by simp 1925 qed 1926 } 1927 ultimately show ?case 1928 by (auto intro: terminates.intros) 1929next 1930 case CondTrue thus ?case 1931 by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def ) 1932next 1933 case CondFalse thus ?case 1934 by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def ) 1935next 1936 case (WhileTrue s b c) 1937 have s_in_b: "s \<in> b" by fact 1938 have noFault_while: "\<Gamma>\<turnstile>\<langle>While b c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 1939 with s_in_b have noFault_c: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 1940 by (auto simp add: final_notin_def intro: exec.intros) 1941 with WhileTrue.hyps have "\<Gamma>\<turnstile>strip_guards F c \<down> Normal s" by simp 1942 moreover 1943 { 1944 fix s' 1945 assume exec_strip_guards_c: "\<Gamma>\<turnstile>\<langle>strip_guards F c,Normal s \<rangle> \<Rightarrow> s'" 1946 have "\<Gamma>\<turnstile>strip_guards F (While b c) \<down> s'" 1947 proof (cases "isFault s'") 1948 case True 1949 thus ?thesis by (auto elim: isFaultE intro: terminates.intros) 1950 next 1951 case False 1952 with exec_strip_guards_to_exec [OF exec_strip_guards_c] noFault_c 1953 have *: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'" 1954 by (auto simp add: final_notin_def elim!: isFaultE) 1955 with s_in_b noFault_while have "\<Gamma>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>Fault ` F" 1956 by (auto simp add: final_notin_def intro: exec.intros) 1957 with * show ?thesis 1958 using WhileTrue.hyps by simp 1959 qed 1960 } 1961 ultimately show ?case 1962 using WhileTrue.hyps by (auto intro: terminates.intros) 1963next 1964 case WhileFalse thus ?case by (auto intro: terminates.intros) 1965next 1966 case Call thus ?case by (auto intro: terminates.intros) 1967next 1968 case CallUndefined thus ?case by (auto intro: terminates.intros) 1969next 1970 case Stuck thus ?case by (auto intro: terminates.intros) 1971next 1972 case DynCom thus ?case 1973 by (auto intro: terminates.intros exec.intros simp add: final_notin_def ) 1974next 1975 case Throw thus ?case by (auto intro: terminates.intros) 1976next 1977 case Abrupt thus ?case by (auto intro: terminates.intros) 1978next 1979 case (Catch c1 s c2) 1980 have noFault_Catch: "\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 1981 hence noFault_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 1982 by (fastforce simp add: final_notin_def intro: exec.intros) 1983 with Catch.hyps have "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s" by simp 1984 moreover 1985 { 1986 fix s' 1987 assume exec_strip_guards_c1: "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" 1988 have "\<Gamma>\<turnstile>strip_guards F c2 \<down> Normal s'" 1989 proof - 1990 from exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1 1991 have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" 1992 by (auto simp add: final_notin_def elim!: isFaultE) 1993 with noFault_Catch have "\<Gamma>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>Fault ` F" 1994 by (auto simp add: final_notin_def intro: exec.intros) 1995 with * show ?thesis 1996 using Catch.hyps by simp 1997 qed 1998 } 1999 ultimately show ?case 2000 using Catch.hyps by (auto intro: terminates.intros) 2001qed 2002 2003(* ************************************************************************* *) 2004subsection \<open>Lemmas about @{const "strip_guards"}\<close> 2005(* ************************************************************************* *) 2006 2007lemma terminates_noFault_strip: 2008 assumes termi: "\<Gamma>\<turnstile>c\<down>Normal s" 2009 shows "\<lbrakk>\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F\<rbrakk> \<Longrightarrow> strip F \<Gamma>\<turnstile>c\<down>Normal s" 2010using termi 2011proof (induct) 2012 case Skip thus ?case by (auto intro: terminates.intros) 2013next 2014 case Basic thus ?case by (auto intro: terminates.intros) 2015next 2016 case Spec thus ?case by (auto intro: terminates.intros) 2017next 2018 case (Guard s g c f) 2019 have s_in_g: "s \<in> g" by fact 2020 have "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 2021 with s_in_g have "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 2022 by (fastforce simp add: final_notin_def intro: exec.intros) 2023 then have "strip F \<Gamma>\<turnstile>c \<down> Normal s" by (simp add: Guard.hyps) 2024 with s_in_g show ?case 2025 by (auto intro: terminates.intros simp del: strip_simp) 2026next 2027 case GuardFault thus ?case 2028 by (auto intro: terminates.intros exec.intros simp add: final_notin_def ) 2029next 2030 case Fault thus ?case by (auto intro: terminates.intros) 2031next 2032 case (Seq c1 s c2) 2033 have noFault_Seq: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 2034 hence noFault_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 2035 by (auto simp add: final_notin_def intro: exec.intros) 2036 then have "strip F \<Gamma>\<turnstile>c1 \<down> Normal s" by (simp add: Seq.hyps) 2037 moreover 2038 { 2039 fix s' 2040 assume exec_strip_c1: "strip F \<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'" 2041 have "strip F \<Gamma>\<turnstile>c2 \<down> s'" 2042 proof (cases "isFault s'") 2043 case True 2044 thus ?thesis by (auto elim: isFaultE intro: terminates.intros) 2045 next 2046 case False 2047 with exec_strip_to_exec [OF exec_strip_c1] noFault_c1 2048 have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'" 2049 by (auto simp add: final_notin_def elim!: isFaultE) 2050 with noFault_Seq have "\<Gamma>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>Fault ` F" 2051 by (auto simp add: final_notin_def intro: exec.intros) 2052 with * show ?thesis 2053 using Seq.hyps by (simp del: strip_simp) 2054 qed 2055 } 2056 ultimately show ?case 2057 by (fastforce intro: terminates.intros) 2058next 2059 case CondTrue thus ?case 2060 by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def ) 2061next 2062 case CondFalse thus ?case 2063 by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def ) 2064next 2065 case (WhileTrue s b c) 2066 have s_in_b: "s \<in> b" by fact 2067 have noFault_while: "\<Gamma>\<turnstile>\<langle>While b c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 2068 with s_in_b have noFault_c: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 2069 by (auto simp add: final_notin_def intro: exec.intros) 2070 then have "strip F \<Gamma>\<turnstile>c \<down> Normal s" by (simp add: WhileTrue.hyps) 2071 moreover 2072 { 2073 fix s' 2074 assume exec_strip_c: "strip F \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'" 2075 have "strip F \<Gamma>\<turnstile>While b c \<down> s'" 2076 proof (cases "isFault s'") 2077 case True 2078 thus ?thesis by (auto elim: isFaultE intro: terminates.intros) 2079 next 2080 case False 2081 with exec_strip_to_exec [OF exec_strip_c] noFault_c 2082 have *: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'" 2083 by (auto simp add: final_notin_def elim!: isFaultE) 2084 with s_in_b noFault_while have "\<Gamma>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>Fault ` F" 2085 by (auto simp add: final_notin_def intro: exec.intros) 2086 with * show ?thesis 2087 using WhileTrue.hyps by (simp del: strip_simp) 2088 qed 2089 } 2090 ultimately show ?case 2091 using WhileTrue.hyps by (auto intro: terminates.intros simp del: strip_simp) 2092next 2093 case WhileFalse thus ?case by (auto intro: terminates.intros) 2094next 2095 case (Call p bdy s) 2096 have bdy: "\<Gamma> p = Some bdy" by fact 2097 have "\<Gamma>\<turnstile>\<langle>Call p,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 2098 with bdy have bdy_noFault: "\<Gamma>\<turnstile>\<langle>bdy,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 2099 by (auto intro: exec.intros simp add: final_notin_def) 2100 then have strip_bdy_noFault: "strip F \<Gamma>\<turnstile>\<langle>bdy,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 2101 by (auto simp add: final_notin_def dest!: exec_strip_to_exec elim!: isFaultE) 2102 2103 from bdy_noFault have "strip F \<Gamma>\<turnstile>bdy \<down> Normal s" by (simp add: Call.hyps) 2104 from terminates_noFault_strip_guards [OF this strip_bdy_noFault] 2105 have "strip F \<Gamma>\<turnstile>strip_guards F bdy \<down> Normal s". 2106 with bdy show ?case 2107 by (fastforce intro: terminates.Call) 2108next 2109 case CallUndefined thus ?case by (auto intro: terminates.intros) 2110next 2111 case Stuck thus ?case by (auto intro: terminates.intros) 2112next 2113 case DynCom thus ?case 2114 by (auto intro: terminates.intros exec.intros simp add: final_notin_def ) 2115next 2116 case Throw thus ?case by (auto intro: terminates.intros) 2117next 2118 case Abrupt thus ?case by (auto intro: terminates.intros) 2119next 2120 case (Catch c1 s c2) 2121 have noFault_Catch: "\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact 2122 hence noFault_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" 2123 by (fastforce simp add: final_notin_def intro: exec.intros) 2124 then have "strip F \<Gamma>\<turnstile>c1 \<down> Normal s" by (simp add: Catch.hyps) 2125 moreover 2126 { 2127 fix s' 2128 assume exec_strip_c1: "strip F \<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" 2129 have "strip F \<Gamma>\<turnstile>c2 \<down> Normal s'" 2130 proof - 2131 from exec_strip_to_exec [OF exec_strip_c1] noFault_c1 2132 have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" 2133 by (auto simp add: final_notin_def elim!: isFaultE) 2134 with * noFault_Catch have "\<Gamma>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>Fault ` F" 2135 by (auto simp add: final_notin_def intro: exec.intros) 2136 with * show ?thesis 2137 using Catch.hyps by (simp del: strip_simp) 2138 qed 2139 } 2140 ultimately show ?case 2141 using Catch.hyps by (auto intro: terminates.intros simp del: strip_simp) 2142qed 2143 2144 2145(* ************************************************************************* *) 2146subsection \<open>Miscellaneous\<close> 2147(* ************************************************************************* *) 2148 2149lemma terminates_while_lemma: 2150 assumes termi: "\<Gamma>\<turnstile>w\<down>fk" 2151 shows "\<And>k b c. \<lbrakk>fk = Normal (f k); w=While b c; 2152 \<forall>i. \<Gamma>\<turnstile>\<langle>c,Normal (f i) \<rangle> \<Rightarrow> Normal (f (Suc i))\<rbrakk> 2153 \<Longrightarrow> \<exists>i. f i \<notin> b" 2154using termi 2155proof (induct) 2156 case WhileTrue thus ?case by blast 2157next 2158 case WhileFalse thus ?case by blast 2159qed simp_all 2160 2161lemma terminates_while: 2162 "\<lbrakk>\<Gamma>\<turnstile>(While b c)\<down>Normal (f k); 2163 \<forall>i. \<Gamma>\<turnstile>\<langle>c,Normal (f i) \<rangle> \<Rightarrow> Normal (f (Suc i))\<rbrakk> 2164 \<Longrightarrow> \<exists>i. f i \<notin> b" 2165 by (blast intro: terminates_while_lemma) 2166 2167lemma wf_terminates_while: 2168 "wf {(t,s). \<Gamma>\<turnstile>(While b c)\<down>Normal s \<and> s\<in>b \<and> 2169 \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> Normal t}" 2170apply(subst wf_iff_no_infinite_down_chain) 2171apply(rule notI) 2172apply clarsimp 2173apply(insert terminates_while) 2174apply blast 2175done 2176 2177lemma terminates_restrict_to_terminates: 2178 assumes terminates_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile> c \<down> s" 2179 assumes not_Stuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,s \<rangle> \<Rightarrow>\<notin>{Stuck}" 2180 shows "\<Gamma>\<turnstile> c \<down> s" 2181using terminates_res not_Stuck 2182proof (induct) 2183 case Skip show ?case by (rule terminates.Skip) 2184next 2185 case Basic show ?case by (rule terminates.Basic) 2186next 2187 case Spec show ?case by (rule terminates.Spec) 2188next 2189 case Guard thus ?case 2190 by (auto intro: terminates.Guard dest: notStuck_GuardD) 2191next 2192 case GuardFault thus ?case by (auto intro: terminates.GuardFault) 2193next 2194 case Fault show ?case by (rule terminates.Fault) 2195next 2196 case (Seq c1 s c2) 2197 have not_Stuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>Seq c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" by fact 2198 hence c1_notStuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" 2199 by (rule notStuck_SeqD1) 2200 show "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s" 2201 proof (rule terminates.Seq,safe) 2202 from c1_notStuck 2203 show "\<Gamma>\<turnstile>c1 \<down> Normal s" 2204 by (rule Seq.hyps) 2205 next 2206 fix s' 2207 assume exec: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'" 2208 show "\<Gamma>\<turnstile>c2 \<down> s'" 2209 proof - 2210 from exec_to_exec_restrict [OF exec] obtain t' where 2211 exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t'" and 2212 t'_notStuck: "t' \<noteq> Stuck \<longrightarrow> t' = s'" 2213 by blast 2214 show ?thesis 2215 proof (cases "t'=Stuck") 2216 case True 2217 with c1_notStuck exec_res have "False" 2218 by (auto simp add: final_notin_def) 2219 thus ?thesis .. 2220 next 2221 case False 2222 with t'_notStuck have t': "t'=s'" by simp 2223 with not_Stuck exec_res 2224 have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>{Stuck}" 2225 by (auto dest: notStuck_SeqD2) 2226 with exec_res t' Seq.hyps 2227 show ?thesis 2228 by auto 2229 qed 2230 qed 2231 qed 2232next 2233 case CondTrue thus ?case 2234 by (auto intro: terminates.CondTrue dest: notStuck_CondTrueD) 2235next 2236 case CondFalse thus ?case 2237 by (auto intro: terminates.CondFalse dest: notStuck_CondFalseD) 2238next 2239 case (WhileTrue s b c) 2240 have s: "s \<in> b" by fact 2241 have not_Stuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>While b c,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" by fact 2242 with WhileTrue have c_notStuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" 2243 by (iprover intro: notStuck_WhileTrueD1) 2244 show ?case 2245 proof (rule terminates.WhileTrue [OF s],safe) 2246 from c_notStuck 2247 show "\<Gamma>\<turnstile>c \<down> Normal s" 2248 by (rule WhileTrue.hyps) 2249 next 2250 fix s' 2251 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'" 2252 show "\<Gamma>\<turnstile>While b c \<down> s'" 2253 proof - 2254 from exec_to_exec_restrict [OF exec] obtain t' where 2255 exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t'" and 2256 t'_notStuck: "t' \<noteq> Stuck \<longrightarrow> t' = s'" 2257 by blast 2258 show ?thesis 2259 proof (cases "t'=Stuck") 2260 case True 2261 with c_notStuck exec_res have "False" 2262 by (auto simp add: final_notin_def) 2263 thus ?thesis .. 2264 next 2265 case False 2266 with t'_notStuck have t': "t'=s'" by simp 2267 with not_Stuck exec_res s 2268 have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>{Stuck}" 2269 by (auto dest: notStuck_WhileTrueD2) 2270 with exec_res t' WhileTrue.hyps 2271 show ?thesis 2272 by auto 2273 qed 2274 qed 2275 qed 2276next 2277 case WhileFalse then show ?case by (iprover intro: terminates.WhileFalse) 2278next 2279 case Call thus ?case 2280 by (auto intro: terminates.Call dest: notStuck_CallD restrict_SomeD) 2281next 2282 case CallUndefined 2283 thus ?case 2284 by (auto dest: notStuck_CallDefinedD) 2285next 2286 case Stuck show ?case by (rule terminates.Stuck) 2287next 2288 case DynCom 2289 thus ?case 2290 by (auto intro: terminates.DynCom dest: notStuck_DynComD) 2291next 2292 case Throw show ?case by (rule terminates.Throw) 2293next 2294 case Abrupt show ?case by (rule terminates.Abrupt) 2295next 2296 case (Catch c1 s c2) 2297 have not_Stuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>Catch c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" by fact 2298 hence c1_notStuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" 2299 by (rule notStuck_CatchD1) 2300 show "\<Gamma>\<turnstile>Catch c1 c2 \<down> Normal s" 2301 proof (rule terminates.Catch,safe) 2302 from c1_notStuck 2303 show "\<Gamma>\<turnstile>c1 \<down> Normal s" 2304 by (rule Catch.hyps) 2305 next 2306 fix s' 2307 assume exec: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" 2308 show "\<Gamma>\<turnstile>c2 \<down> Normal s'" 2309 proof - 2310 from exec_to_exec_restrict [OF exec] obtain t' where 2311 exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t'" and 2312 t'_notStuck: "t' \<noteq> Stuck \<longrightarrow> t' = Abrupt s'" 2313 by blast 2314 show ?thesis 2315 proof (cases "t'=Stuck") 2316 case True 2317 with c1_notStuck exec_res have "False" 2318 by (auto simp add: final_notin_def) 2319 thus ?thesis .. 2320 next 2321 case False 2322 with t'_notStuck have t': "t'=Abrupt s'" by simp 2323 with not_Stuck exec_res 2324 have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>{Stuck}" 2325 by (auto dest: notStuck_CatchD2) 2326 with exec_res t' Catch.hyps 2327 show ?thesis 2328 by auto 2329 qed 2330 qed 2331 qed 2332qed 2333 2334end 2335