1(* 2 Author: Norbert Schirmer 3 Maintainer: Norbert Schirmer, norbert.schirmer at web de 4 License: LGPL 5*) 6 7(* Title: SmallStep.thy 8 Author: Norbert Schirmer, TU Muenchen 9 10Copyright (C) 2006-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*) 28 29section \<open>Small-Step Semantics and Infinite Computations\<close> 30 31theory SmallStep imports Termination 32begin 33 34text \<open>The redex of a statement is the substatement, which is actually altered 35by the next step in the small-step semantics. 36\<close> 37 38primrec redex:: "('s,'p,'f)com \<Rightarrow> ('s,'p,'f)com" 39where 40"redex Skip = Skip" | 41"redex (Basic f) = (Basic f)" | 42"redex (Spec r) = (Spec r)" | 43"redex (Seq c\<^sub>1 c\<^sub>2) = redex c\<^sub>1" | 44"redex (Cond b c\<^sub>1 c\<^sub>2) = (Cond b c\<^sub>1 c\<^sub>2)" | 45"redex (While b c) = (While b c)" | 46"redex (Call p) = (Call p)" | 47"redex (DynCom d) = (DynCom d)" | 48"redex (Guard f b c) = (Guard f b c)" | 49"redex (Throw) = Throw" | 50"redex (Catch c\<^sub>1 c\<^sub>2) = redex c\<^sub>1" 51 52 53subsection \<open>Small-Step Computation: \<open>\<Gamma>\<turnstile>(c, s) \<rightarrow> (c', s')\<close>\<close> 54 55type_synonym ('s,'p,'f) config = "('s,'p,'f)com \<times> ('s,'f) xstate" 56inductive "step"::"[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] \<Rightarrow> bool" 57 ("_\<turnstile> (_ \<rightarrow>/ _)" [81,81,81] 100) 58 for \<Gamma>::"('s,'p,'f) body" 59where 60 61 Basic: "\<Gamma>\<turnstile>(Basic f,Normal s) \<rightarrow> (Skip,Normal (f s))" 62 63| Spec: "(s,t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile>(Spec r,Normal s) \<rightarrow> (Skip,Normal t)" 64| SpecStuck: "\<forall>t. (s,t) \<notin> r \<Longrightarrow> \<Gamma>\<turnstile>(Spec r,Normal s) \<rightarrow> (Skip,Stuck)" 65 66| Guard: "s\<in>g \<Longrightarrow> \<Gamma>\<turnstile>(Guard f g c,Normal s) \<rightarrow> (c,Normal s)" 67 68| GuardFault: "s\<notin>g \<Longrightarrow> \<Gamma>\<turnstile>(Guard f g c,Normal s) \<rightarrow> (Skip,Fault f)" 69 70 71| Seq: "\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow> (c\<^sub>1',s') 72 \<Longrightarrow> 73 \<Gamma>\<turnstile>(Seq c\<^sub>1 c\<^sub>2,s) \<rightarrow> (Seq c\<^sub>1' c\<^sub>2, s')" 74| SeqSkip: "\<Gamma>\<turnstile>(Seq Skip c\<^sub>2,s) \<rightarrow> (c\<^sub>2, s)" 75| SeqThrow: "\<Gamma>\<turnstile>(Seq Throw c\<^sub>2,Normal s) \<rightarrow> (Throw, Normal s)" 76 77| CondTrue: "s\<in>b \<Longrightarrow> \<Gamma>\<turnstile>(Cond b c\<^sub>1 c\<^sub>2,Normal s) \<rightarrow> (c\<^sub>1,Normal s)" 78| CondFalse: "s\<notin>b \<Longrightarrow> \<Gamma>\<turnstile>(Cond b c\<^sub>1 c\<^sub>2,Normal s) \<rightarrow> (c\<^sub>2,Normal s)" 79 80| WhileTrue: "\<lbrakk>s\<in>b\<rbrakk> 81 \<Longrightarrow> 82 \<Gamma>\<turnstile>(While b c,Normal s) \<rightarrow> (Seq c (While b c),Normal s)" 83 84| WhileFalse: "\<lbrakk>s\<notin>b\<rbrakk> 85 \<Longrightarrow> 86 \<Gamma>\<turnstile>(While b c,Normal s) \<rightarrow> (Skip,Normal s)" 87 88| Call: "\<Gamma> p=Some bdy \<Longrightarrow> 89 \<Gamma>\<turnstile>(Call p,Normal s) \<rightarrow> (bdy,Normal s)" 90 91| CallUndefined: "\<Gamma> p=None \<Longrightarrow> 92 \<Gamma>\<turnstile>(Call p,Normal s) \<rightarrow> (Skip,Stuck)" 93 94| DynCom: "\<Gamma>\<turnstile>(DynCom c,Normal s) \<rightarrow> (c s,Normal s)" 95 96| Catch: "\<lbrakk>\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow> (c\<^sub>1',s')\<rbrakk> 97 \<Longrightarrow> 98 \<Gamma>\<turnstile>(Catch c\<^sub>1 c\<^sub>2,s) \<rightarrow> (Catch c\<^sub>1' c\<^sub>2,s')" 99 100| CatchThrow: "\<Gamma>\<turnstile>(Catch Throw c\<^sub>2,Normal s) \<rightarrow> (c\<^sub>2,Normal s)" 101| CatchSkip: "\<Gamma>\<turnstile>(Catch Skip c\<^sub>2,s) \<rightarrow> (Skip,s)" 102 103| FaultProp: "\<lbrakk>c\<noteq>Skip; redex c = c\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>(c,Fault f) \<rightarrow> (Skip,Fault f)" 104| StuckProp: "\<lbrakk>c\<noteq>Skip; redex c = c\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>(c,Stuck) \<rightarrow> (Skip,Stuck)" 105| AbruptProp: "\<lbrakk>c\<noteq>Skip; redex c = c\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>(c,Abrupt f) \<rightarrow> (Skip,Abrupt f)" 106 107 108lemmas step_induct = step.induct [of _ "(c,s)" "(c',s')", split_format (complete), case_names 109Basic Spec SpecStuck Guard GuardFault Seq SeqSkip SeqThrow CondTrue CondFalse 110WhileTrue WhileFalse Call CallUndefined DynCom Catch CatchThrow CatchSkip 111FaultProp StuckProp AbruptProp, induct set] 112 113 114inductive_cases step_elim_cases [cases set]: 115 "\<Gamma>\<turnstile>(Skip,s) \<rightarrow> u" 116 "\<Gamma>\<turnstile>(Guard f g c,s) \<rightarrow> u" 117 "\<Gamma>\<turnstile>(Basic f,s) \<rightarrow> u" 118 "\<Gamma>\<turnstile>(Spec r,s) \<rightarrow> u" 119 "\<Gamma>\<turnstile>(Seq c1 c2,s) \<rightarrow> u" 120 "\<Gamma>\<turnstile>(Cond b c1 c2,s) \<rightarrow> u" 121 "\<Gamma>\<turnstile>(While b c,s) \<rightarrow> u" 122 "\<Gamma>\<turnstile>(Call p,s) \<rightarrow> u" 123 "\<Gamma>\<turnstile>(DynCom c,s) \<rightarrow> u" 124 "\<Gamma>\<turnstile>(Throw,s) \<rightarrow> u" 125 "\<Gamma>\<turnstile>(Catch c1 c2,s) \<rightarrow> u" 126 127inductive_cases step_Normal_elim_cases [cases set]: 128 "\<Gamma>\<turnstile>(Skip,Normal s) \<rightarrow> u" 129 "\<Gamma>\<turnstile>(Guard f g c,Normal s) \<rightarrow> u" 130 "\<Gamma>\<turnstile>(Basic f,Normal s) \<rightarrow> u" 131 "\<Gamma>\<turnstile>(Spec r,Normal s) \<rightarrow> u" 132 "\<Gamma>\<turnstile>(Seq c1 c2,Normal s) \<rightarrow> u" 133 "\<Gamma>\<turnstile>(Cond b c1 c2,Normal s) \<rightarrow> u" 134 "\<Gamma>\<turnstile>(While b c,Normal s) \<rightarrow> u" 135 "\<Gamma>\<turnstile>(Call p,Normal s) \<rightarrow> u" 136 "\<Gamma>\<turnstile>(DynCom c,Normal s) \<rightarrow> u" 137 "\<Gamma>\<turnstile>(Throw,Normal s) \<rightarrow> u" 138 "\<Gamma>\<turnstile>(Catch c1 c2,Normal s) \<rightarrow> u" 139 140 141text \<open>The final configuration is either of the form \<open>(Skip,_)\<close> for normal 142termination, or @{term "(Throw,Normal s)"} in case the program was started in 143a @{term "Normal"} state and terminated abruptly. The @{const "Abrupt"} state is not used to 144model abrupt termination, in contrast to the big-step semantics. Only if the 145program starts in an @{const "Abrupt"} states it ends in the same @{term "Abrupt"} 146state.\<close> 147 148definition final:: "('s,'p,'f) config \<Rightarrow> bool" where 149"final cfg = (fst cfg=Skip \<or> (fst cfg=Throw \<and> (\<exists>s. snd cfg=Normal s)))" 150 151 152abbreviation 153 "step_rtrancl" :: "[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] \<Rightarrow> bool" 154 ("_\<turnstile> (_ \<rightarrow>\<^sup>*/ _)" [81,81,81] 100) 155 where 156 "\<Gamma>\<turnstile>cf0 \<rightarrow>\<^sup>* cf1 \<equiv> (CONST step \<Gamma>)\<^sup>*\<^sup>* cf0 cf1" 157abbreviation 158 "step_trancl" :: "[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] \<Rightarrow> bool" 159 ("_\<turnstile> (_ \<rightarrow>\<^sup>+/ _)" [81,81,81] 100) 160 where 161 "\<Gamma>\<turnstile>cf0 \<rightarrow>\<^sup>+ cf1 \<equiv> (CONST step \<Gamma>)\<^sup>+\<^sup>+ cf0 cf1" 162 163 164 165 166 167 168 169 170(* ************************************************************************ *) 171subsection \<open>Structural Properties of Small Step Computations\<close> 172(* ************************************************************************ *) 173 174lemma redex_not_Seq: "redex c = Seq c1 c2 \<Longrightarrow> P" 175 apply (induct c) 176 apply auto 177 done 178 179lemma no_step_final: 180 assumes step: "\<Gamma>\<turnstile>(c,s) \<rightarrow> (c',s')" 181 shows "final (c,s) \<Longrightarrow> P" 182using step 183by induct (auto simp add: final_def) 184 185lemma no_step_final': 186 assumes step: "\<Gamma>\<turnstile>cfg \<rightarrow> cfg'" 187 shows "final cfg \<Longrightarrow> P" 188using step 189 by (cases cfg, cases cfg') (auto intro: no_step_final) 190 191lemma step_Abrupt: 192 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')" 193 shows "\<And>x. s=Abrupt x \<Longrightarrow> s'=Abrupt x" 194using step 195by (induct) auto 196 197lemma step_Fault: 198 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')" 199 shows "\<And>f. s=Fault f \<Longrightarrow> s'=Fault f" 200using step 201by (induct) auto 202 203lemma step_Stuck: 204 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')" 205 shows "\<And>f. s=Stuck \<Longrightarrow> s'=Stuck" 206using step 207by (induct) auto 208 209lemma SeqSteps: 210 assumes steps: "\<Gamma>\<turnstile>cfg\<^sub>1\<rightarrow>\<^sup>* cfg\<^sub>2" 211 shows "\<And> c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>1 = (c\<^sub>1,s);cfg\<^sub>2=(c\<^sub>1',s')\<rbrakk> 212 \<Longrightarrow> \<Gamma>\<turnstile>(Seq c\<^sub>1 c\<^sub>2,s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')" 213using steps 214proof (induct rule: converse_rtranclp_induct [case_names Refl Trans]) 215 case Refl 216 thus ?case 217 by simp 218next 219 case (Trans cfg\<^sub>1 cfg'') 220 have step: "\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''" by fact 221 have steps: "\<Gamma>\<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2" by fact 222 have cfg\<^sub>1: "cfg\<^sub>1 = (c\<^sub>1, s)" and cfg\<^sub>2: "cfg\<^sub>2 = (c\<^sub>1', s')" by fact+ 223 obtain c\<^sub>1'' s'' where cfg'': "cfg''=(c\<^sub>1'',s'')" 224 by (cases cfg'') auto 225 from step cfg\<^sub>1 cfg'' 226 have "\<Gamma>\<turnstile> (c\<^sub>1,s) \<rightarrow> (c\<^sub>1'',s'')" 227 by simp 228 hence "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2,s) \<rightarrow> (Seq c\<^sub>1'' c\<^sub>2,s'')" 229 by (rule step.Seq) 230 also from Trans.hyps (3) [OF cfg'' cfg\<^sub>2] 231 have "\<Gamma>\<turnstile> (Seq c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')" . 232 finally show ?case . 233qed 234 235 236lemma CatchSteps: 237 assumes steps: "\<Gamma>\<turnstile>cfg\<^sub>1\<rightarrow>\<^sup>* cfg\<^sub>2" 238 shows "\<And> c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>1 = (c\<^sub>1,s); cfg\<^sub>2=(c\<^sub>1',s')\<rbrakk> 239 \<Longrightarrow> \<Gamma>\<turnstile>(Catch c\<^sub>1 c\<^sub>2,s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')" 240using steps 241proof (induct rule: converse_rtranclp_induct [case_names Refl Trans]) 242 case Refl 243 thus ?case 244 by simp 245next 246 case (Trans cfg\<^sub>1 cfg'') 247 have step: "\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''" by fact 248 have steps: "\<Gamma>\<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2" by fact 249 have cfg\<^sub>1: "cfg\<^sub>1 = (c\<^sub>1, s)" and cfg\<^sub>2: "cfg\<^sub>2 = (c\<^sub>1', s')" by fact+ 250 obtain c\<^sub>1'' s'' where cfg'': "cfg''=(c\<^sub>1'',s'')" 251 by (cases cfg'') auto 252 from step cfg\<^sub>1 cfg'' 253 have s: "\<Gamma>\<turnstile> (c\<^sub>1,s) \<rightarrow> (c\<^sub>1'',s'')" 254 by simp 255 hence "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2,s) \<rightarrow> (Catch c\<^sub>1'' c\<^sub>2,s'')" 256 by (rule step.Catch) 257 also from Trans.hyps (3) [OF cfg'' cfg\<^sub>2] 258 have "\<Gamma>\<turnstile> (Catch c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')" . 259 finally show ?case . 260qed 261 262lemma steps_Fault: "\<Gamma>\<turnstile> (c, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)" 263proof (induct c) 264 case (Seq c\<^sub>1 c\<^sub>2) 265 have steps_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)" by fact 266 have steps_c\<^sub>2: "\<Gamma>\<turnstile> (c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)" by fact 267 from SeqSteps [OF steps_c\<^sub>1 refl refl] 268 have "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Fault f)". 269 also 270 have "\<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Fault f) \<rightarrow> (c\<^sub>2, Fault f)" by (rule SeqSkip) 271 also note steps_c\<^sub>2 272 finally show ?case by simp 273next 274 case (Catch c\<^sub>1 c\<^sub>2) 275 have steps_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Fault f) \<rightarrow>\<^sup>* (Skip, Fault f)" by fact 276 from CatchSteps [OF steps_c\<^sub>1 refl refl] 277 have "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Fault f) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Fault f)". 278 also 279 have "\<Gamma>\<turnstile> (Catch Skip c\<^sub>2, Fault f) \<rightarrow> (Skip, Fault f)" by (rule CatchSkip) 280 finally show ?case by simp 281qed (fastforce intro: step.intros)+ 282 283lemma steps_Stuck: "\<Gamma>\<turnstile> (c, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)" 284proof (induct c) 285 case (Seq c\<^sub>1 c\<^sub>2) 286 have steps_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)" by fact 287 have steps_c\<^sub>2: "\<Gamma>\<turnstile> (c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)" by fact 288 from SeqSteps [OF steps_c\<^sub>1 refl refl] 289 have "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Stuck)". 290 also 291 have "\<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Stuck) \<rightarrow> (c\<^sub>2, Stuck)" by (rule SeqSkip) 292 also note steps_c\<^sub>2 293 finally show ?case by simp 294next 295 case (Catch c\<^sub>1 c\<^sub>2) 296 have steps_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Stuck) \<rightarrow>\<^sup>* (Skip, Stuck)" by fact 297 from CatchSteps [OF steps_c\<^sub>1 refl refl] 298 have "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Stuck)" . 299 also 300 have "\<Gamma>\<turnstile> (Catch Skip c\<^sub>2, Stuck) \<rightarrow> (Skip, Stuck)" by (rule CatchSkip) 301 finally show ?case by simp 302qed (fastforce intro: step.intros)+ 303 304lemma steps_Abrupt: "\<Gamma>\<turnstile> (c, Abrupt s) \<rightarrow>\<^sup>* (Skip, Abrupt s)" 305proof (induct c) 306 case (Seq c\<^sub>1 c\<^sub>2) 307 have steps_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Abrupt s) \<rightarrow>\<^sup>* (Skip, Abrupt s)" by fact 308 have steps_c\<^sub>2: "\<Gamma>\<turnstile> (c\<^sub>2, Abrupt s) \<rightarrow>\<^sup>* (Skip, Abrupt s)" by fact 309 from SeqSteps [OF steps_c\<^sub>1 refl refl] 310 have "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Abrupt s) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, Abrupt s)". 311 also 312 have "\<Gamma>\<turnstile> (Seq Skip c\<^sub>2, Abrupt s) \<rightarrow> (c\<^sub>2, Abrupt s)" by (rule SeqSkip) 313 also note steps_c\<^sub>2 314 finally show ?case by simp 315next 316 case (Catch c\<^sub>1 c\<^sub>2) 317 have steps_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Abrupt s) \<rightarrow>\<^sup>* (Skip, Abrupt s)" by fact 318 from CatchSteps [OF steps_c\<^sub>1 refl refl] 319 have "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Abrupt s) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, Abrupt s)". 320 also 321 have "\<Gamma>\<turnstile> (Catch Skip c\<^sub>2, Abrupt s) \<rightarrow> (Skip, Abrupt s)" by (rule CatchSkip) 322 finally show ?case by simp 323qed (fastforce intro: step.intros)+ 324 325lemma step_Fault_prop: 326 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')" 327 shows "\<And>f. s=Fault f \<Longrightarrow> s'=Fault f" 328using step 329by (induct) auto 330 331lemma step_Abrupt_prop: 332 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')" 333 shows "\<And>x. s=Abrupt x \<Longrightarrow> s'=Abrupt x" 334using step 335by (induct) auto 336 337lemma step_Stuck_prop: 338 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')" 339 shows "s=Stuck \<Longrightarrow> s'=Stuck" 340using step 341by (induct) auto 342 343lemma steps_Fault_prop: 344 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>* (c', s')" 345 shows "s=Fault f \<Longrightarrow> s'=Fault f" 346using step 347proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 348 case Refl thus ?case by simp 349next 350 case (Trans c s c'' s'') 351 thus ?case 352 by (auto intro: step_Fault_prop) 353qed 354 355lemma steps_Abrupt_prop: 356 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>* (c', s')" 357 shows "s=Abrupt t \<Longrightarrow> s'=Abrupt t" 358using step 359proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 360 case Refl thus ?case by simp 361next 362 case (Trans c s c'' s'') 363 thus ?case 364 by (auto intro: step_Abrupt_prop) 365qed 366 367lemma steps_Stuck_prop: 368 assumes step: "\<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>* (c', s')" 369 shows "s=Stuck \<Longrightarrow> s'=Stuck" 370using step 371proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 372 case Refl thus ?case by simp 373next 374 case (Trans c s c'' s'') 375 thus ?case 376 by (auto intro: step_Stuck_prop) 377qed 378 379(* ************************************************************************ *) 380subsection \<open>Equivalence between Small-Step and Big-Step Semantics\<close> 381(* ************************************************************************ *) 382 383theorem exec_impl_steps: 384 assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t" 385 shows "\<exists>c' t'. \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (c',t') \<and> 386 (case t of 387 Abrupt x \<Rightarrow> if s=t then c'=Skip \<and> t'=t else c'=Throw \<and> t'=Normal x 388 | _ \<Rightarrow> c'=Skip \<and> t'=t)" 389using exec 390proof (induct) 391 case Skip thus ?case 392 by simp 393next 394 case Guard thus ?case by (blast intro: step.Guard rtranclp_trans) 395next 396 case GuardFault thus ?case by (fastforce intro: step.GuardFault rtranclp_trans) 397next 398 case FaultProp show ?case by (fastforce intro: steps_Fault) 399next 400 case Basic thus ?case by (fastforce intro: step.Basic rtranclp_trans) 401next 402 case Spec thus ?case by (fastforce intro: step.Spec rtranclp_trans) 403next 404 case SpecStuck thus ?case by (fastforce intro: step.SpecStuck rtranclp_trans) 405next 406 case (Seq c\<^sub>1 s s' c\<^sub>2 t) 407 have exec_c\<^sub>1: "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'" by fact 408 have exec_c\<^sub>2: "\<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t" by fact 409 show ?case 410 proof (cases "\<exists>x. s'=Abrupt x") 411 case False 412 from False Seq.hyps (2) 413 have "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow>\<^sup>* (Skip, s')" 414 by (cases s') auto 415 hence seq_c\<^sub>1: "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow>\<^sup>* (Seq Skip c\<^sub>2, s')" 416 by (rule SeqSteps) auto 417 from Seq.hyps (4) obtain c' t' where 418 steps_c\<^sub>2: "\<Gamma>\<turnstile> (c\<^sub>2, s') \<rightarrow>\<^sup>* (c', t')" and 419 t: "(case t of 420 Abrupt x \<Rightarrow> if s' = t then c' = Skip \<and> t' = t 421 else c' = Throw \<and> t' = Normal x 422 | _ \<Rightarrow> c' = Skip \<and> t' = t)" 423 by auto 424 note seq_c\<^sub>1 425 also have "\<Gamma>\<turnstile> (Seq Skip c\<^sub>2, s') \<rightarrow> (c\<^sub>2, s')" by (rule step.SeqSkip) 426 also note steps_c\<^sub>2 427 finally have "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow>\<^sup>* (c', t')". 428 with t False show ?thesis 429 by (cases t) auto 430 next 431 case True 432 then obtain x where s': "s'=Abrupt x" 433 by blast 434 from s' Seq.hyps (2) 435 have "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow>\<^sup>* (Throw, Normal x)" 436 by auto 437 hence seq_c\<^sub>1: "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow>\<^sup>* (Seq Throw c\<^sub>2, Normal x)" 438 by (rule SeqSteps) auto 439 also have "\<Gamma>\<turnstile> (Seq Throw c\<^sub>2, Normal x) \<rightarrow> (Throw, Normal x)" 440 by (rule SeqThrow) 441 finally have "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow>\<^sup>* (Throw, Normal x)". 442 moreover 443 from exec_c\<^sub>2 s' have "t=Abrupt x" 444 by (auto intro: Abrupt_end) 445 ultimately show ?thesis 446 by auto 447 qed 448next 449 case CondTrue thus ?case by (blast intro: step.CondTrue rtranclp_trans) 450next 451 case CondFalse thus ?case by (blast intro: step.CondFalse rtranclp_trans) 452next 453 case (WhileTrue s b c s' t) 454 have exec_c: "\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'" by fact 455 have exec_w: "\<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t" by fact 456 have b: "s \<in> b" by fact 457 hence step: "\<Gamma>\<turnstile> (While b c,Normal s) \<rightarrow> (Seq c (While b c),Normal s)" 458 by (rule step.WhileTrue) 459 show ?case 460 proof (cases "\<exists>x. s'=Abrupt x") 461 case False 462 from False WhileTrue.hyps (3) 463 have "\<Gamma>\<turnstile> (c, Normal s) \<rightarrow>\<^sup>* (Skip, s')" 464 by (cases s') auto 465 hence seq_c: "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow>\<^sup>* (Seq Skip (While b c), s')" 466 by (rule SeqSteps) auto 467 from WhileTrue.hyps (5) obtain c' t' where 468 steps_c\<^sub>2: "\<Gamma>\<turnstile> (While b c, s') \<rightarrow>\<^sup>* (c', t')" and 469 t: "(case t of 470 Abrupt x \<Rightarrow> if s' = t then c' = Skip \<and> t' = t 471 else c' = Throw \<and> t' = Normal x 472 | _ \<Rightarrow> c' = Skip \<and> t' = t)" 473 by auto 474 note step also note seq_c 475 also have "\<Gamma>\<turnstile> (Seq Skip (While b c), s') \<rightarrow> (While b c, s')" 476 by (rule step.SeqSkip) 477 also note steps_c\<^sub>2 478 finally have "\<Gamma>\<turnstile> (While b c, Normal s) \<rightarrow>\<^sup>* (c', t')". 479 with t False show ?thesis 480 by (cases t) auto 481 next 482 case True 483 then obtain x where s': "s'=Abrupt x" 484 by blast 485 note step 486 also 487 from s' WhileTrue.hyps (3) 488 have "\<Gamma>\<turnstile> (c, Normal s) \<rightarrow>\<^sup>* (Throw, Normal x)" 489 by auto 490 hence 491 seq_c: "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow>\<^sup>* (Seq Throw (While b c), Normal x)" 492 by (rule SeqSteps) auto 493 also have "\<Gamma>\<turnstile> (Seq Throw (While b c), Normal x) \<rightarrow> (Throw, Normal x)" 494 by (rule SeqThrow) 495 finally have "\<Gamma>\<turnstile> (While b c, Normal s) \<rightarrow>\<^sup>* (Throw, Normal x)". 496 moreover 497 from exec_w s' have "t=Abrupt x" 498 by (auto intro: Abrupt_end) 499 ultimately show ?thesis 500 by auto 501 qed 502next 503 case WhileFalse thus ?case by (fastforce intro: step.WhileFalse rtrancl_trans) 504next 505 case Call thus ?case by (blast intro: step.Call rtranclp_trans) 506next 507 case CallUndefined thus ?case by (fastforce intro: step.CallUndefined rtranclp_trans) 508next 509 case StuckProp thus ?case by (fastforce intro: steps_Stuck) 510next 511 case DynCom thus ?case by (blast intro: step.DynCom rtranclp_trans) 512next 513 case Throw thus ?case by simp 514next 515 case AbruptProp thus ?case by (fastforce intro: steps_Abrupt) 516next 517 case (CatchMatch c\<^sub>1 s s' c\<^sub>2 t) 518 from CatchMatch.hyps (2) 519 have "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow>\<^sup>* (Throw, Normal s')" 520 by simp 521 hence "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow>\<^sup>* (Catch Throw c\<^sub>2, Normal s')" 522 by (rule CatchSteps) auto 523 also have "\<Gamma>\<turnstile> (Catch Throw c\<^sub>2, Normal s') \<rightarrow> (c\<^sub>2, Normal s')" 524 by (rule step.CatchThrow) 525 also 526 from CatchMatch.hyps (4) obtain c' t' where 527 steps_c\<^sub>2: "\<Gamma>\<turnstile> (c\<^sub>2, Normal s') \<rightarrow>\<^sup>* (c', t')" and 528 t: "(case t of 529 Abrupt x \<Rightarrow> if Normal s' = t then c' = Skip \<and> t' = t 530 else c' = Throw \<and> t' = Normal x 531 | _ \<Rightarrow> c' = Skip \<and> t' = t)" 532 by auto 533 note steps_c\<^sub>2 534 finally show ?case 535 using t 536 by (auto split: xstate.splits) 537next 538 case (CatchMiss c\<^sub>1 s t c\<^sub>2) 539 have t: "\<not> isAbr t" by fact 540 with CatchMiss.hyps (2) 541 have "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow>\<^sup>* (Skip, t)" 542 by (cases t) auto 543 hence "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow>\<^sup>* (Catch Skip c\<^sub>2, t)" 544 by (rule CatchSteps) auto 545 also 546 have "\<Gamma>\<turnstile> (Catch Skip c\<^sub>2, t) \<rightarrow> (Skip, t)" 547 by (rule step.CatchSkip) 548 finally show ?case 549 using t 550 by (fastforce split: xstate.splits) 551qed 552 553corollary exec_impl_steps_Normal: 554 assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> Normal t" 555 shows "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (Skip, Normal t)" 556using exec_impl_steps [OF exec] 557by auto 558 559corollary exec_impl_steps_Normal_Abrupt: 560 assumes exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t" 561 shows "\<Gamma>\<turnstile>(c,Normal s) \<rightarrow>\<^sup>* (Throw, Normal t)" 562using exec_impl_steps [OF exec] 563by auto 564 565corollary exec_impl_steps_Abrupt_Abrupt: 566 assumes exec: "\<Gamma>\<turnstile>\<langle>c,Abrupt t\<rangle> \<Rightarrow> Abrupt t" 567 shows "\<Gamma>\<turnstile>(c,Abrupt t) \<rightarrow>\<^sup>* (Skip, Abrupt t)" 568using exec_impl_steps [OF exec] 569by auto 570 571corollary exec_impl_steps_Fault: 572 assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> Fault f" 573 shows "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (Skip, Fault f)" 574using exec_impl_steps [OF exec] 575by auto 576 577corollary exec_impl_steps_Stuck: 578 assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> Stuck" 579 shows "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (Skip, Stuck)" 580using exec_impl_steps [OF exec] 581by auto 582 583 584lemma step_Abrupt_end: 585 assumes step: "\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1', s')" 586 shows "s'=Abrupt x \<Longrightarrow> s=Abrupt x" 587using step 588by induct auto 589 590lemma step_Stuck_end: 591 assumes step: "\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1', s')" 592 shows "s'=Stuck \<Longrightarrow> 593 s=Stuck \<or> 594 (\<exists>r x. redex c\<^sub>1 = Spec r \<and> s=Normal x \<and> (\<forall>t. (x,t)\<notin>r)) \<or> 595 (\<exists>p x. redex c\<^sub>1=Call p \<and> s=Normal x \<and> \<Gamma> p = None)" 596using step 597by induct auto 598 599lemma step_Fault_end: 600 assumes step: "\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1', s')" 601 shows "s'=Fault f \<Longrightarrow> 602 s=Fault f \<or> 603 (\<exists>g c x. redex c\<^sub>1 = Guard f g c \<and> s=Normal x \<and> x \<notin> g)" 604using step 605by induct auto 606 607lemma exec_redex_Stuck: 608"\<Gamma>\<turnstile>\<langle>redex c,s\<rangle> \<Rightarrow> Stuck \<Longrightarrow> \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> Stuck" 609proof (induct c) 610 case Seq 611 thus ?case 612 by (cases s) (auto intro: exec.intros elim:exec_elim_cases) 613next 614 case Catch 615 thus ?case 616 by (cases s) (auto intro: exec.intros elim:exec_elim_cases) 617qed simp_all 618 619lemma exec_redex_Fault: 620"\<Gamma>\<turnstile>\<langle>redex c,s\<rangle> \<Rightarrow> Fault f \<Longrightarrow> \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> Fault f" 621proof (induct c) 622 case Seq 623 thus ?case 624 by (cases s) (auto intro: exec.intros elim:exec_elim_cases) 625next 626 case Catch 627 thus ?case 628 by (cases s) (auto intro: exec.intros elim:exec_elim_cases) 629qed simp_all 630 631lemma step_extend: 632 assumes step: "\<Gamma>\<turnstile>(c,s) \<rightarrow> (c', s')" 633 shows "\<And>t. \<Gamma>\<turnstile>\<langle>c',s'\<rangle> \<Rightarrow> t \<Longrightarrow> \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t" 634using step 635proof (induct) 636 case Basic thus ?case 637 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 638next 639 case Spec thus ?case 640 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 641next 642 case SpecStuck thus ?case 643 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 644next 645 case Guard thus ?case 646 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 647next 648 case GuardFault thus ?case 649 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 650next 651 case (Seq c\<^sub>1 s c\<^sub>1' s' c\<^sub>2) 652 have step: "\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1', s')" by fact 653 have exec': "\<Gamma>\<turnstile> \<langle>Seq c\<^sub>1' c\<^sub>2,s'\<rangle> \<Rightarrow> t" by fact 654 show ?case 655 proof (cases s) 656 case (Normal x) 657 note s_Normal = this 658 show ?thesis 659 proof (cases s') 660 case (Normal x') 661 from exec' [simplified Normal] obtain s'' where 662 exec_c\<^sub>1': "\<Gamma>\<turnstile> \<langle>c\<^sub>1',Normal x'\<rangle> \<Rightarrow> s''" and 663 exec_c\<^sub>2: "\<Gamma>\<turnstile> \<langle>c\<^sub>2,s''\<rangle> \<Rightarrow> t" 664 by cases 665 from Seq.hyps (2) Normal exec_c\<^sub>1' s_Normal 666 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> s''" 667 by simp 668 from exec.Seq [OF this exec_c\<^sub>2] s_Normal 669 show ?thesis by simp 670 next 671 case (Abrupt x') 672 with exec' have "t=Abrupt x'" 673 by (auto intro:Abrupt_end) 674 moreover 675 from step Abrupt 676 have "s=Abrupt x'" 677 by (auto intro: step_Abrupt_end) 678 ultimately 679 show ?thesis 680 by (auto intro: exec.intros) 681 next 682 case (Fault f) 683 from step_Fault_end [OF step this] s_Normal 684 obtain g c where 685 redex_c\<^sub>1: "redex c\<^sub>1 = Guard f g c" and 686 fail: "x \<notin> g" 687 by auto 688 hence "\<Gamma>\<turnstile> \<langle>redex c\<^sub>1,Normal x\<rangle> \<Rightarrow> Fault f" 689 by (auto intro: exec.intros) 690 from exec_redex_Fault [OF this] 691 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> Fault f". 692 moreover from Fault exec' have "t=Fault f" 693 by (auto intro: Fault_end) 694 ultimately 695 show ?thesis 696 using s_Normal 697 by (auto intro: exec.intros) 698 next 699 case Stuck 700 from step_Stuck_end [OF step this] s_Normal 701 have "(\<exists>r. redex c\<^sub>1 = Spec r \<and> (\<forall>t. (x, t) \<notin> r)) \<or> 702 (\<exists>p. redex c\<^sub>1 = Call p \<and> \<Gamma> p = None)" 703 by auto 704 moreover 705 { 706 fix r 707 assume "redex c\<^sub>1 = Spec r" and "(\<forall>t. (x, t) \<notin> r)" 708 hence "\<Gamma>\<turnstile> \<langle>redex c\<^sub>1,Normal x\<rangle> \<Rightarrow> Stuck" 709 by (auto intro: exec.intros) 710 from exec_redex_Stuck [OF this] 711 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> Stuck". 712 moreover from Stuck exec' have "t=Stuck" 713 by (auto intro: Stuck_end) 714 ultimately 715 have ?thesis 716 using s_Normal 717 by (auto intro: exec.intros) 718 } 719 moreover 720 { 721 fix p 722 assume "redex c\<^sub>1 = Call p" and "\<Gamma> p = None" 723 hence "\<Gamma>\<turnstile> \<langle>redex c\<^sub>1,Normal x\<rangle> \<Rightarrow> Stuck" 724 by (auto intro: exec.intros) 725 from exec_redex_Stuck [OF this] 726 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> Stuck". 727 moreover from Stuck exec' have "t=Stuck" 728 by (auto intro: Stuck_end) 729 ultimately 730 have ?thesis 731 using s_Normal 732 by (auto intro: exec.intros) 733 } 734 ultimately show ?thesis 735 by auto 736 qed 737 next 738 case (Abrupt x) 739 from step_Abrupt [OF step this] 740 have "s'=Abrupt x". 741 with exec' 742 have "t=Abrupt x" 743 by (auto intro: Abrupt_end) 744 with Abrupt 745 show ?thesis 746 by (auto intro: exec.intros) 747 next 748 case (Fault f) 749 from step_Fault [OF step this] 750 have "s'=Fault f". 751 with exec' 752 have "t=Fault f" 753 by (auto intro: Fault_end) 754 with Fault 755 show ?thesis 756 by (auto intro: exec.intros) 757 next 758 case Stuck 759 from step_Stuck [OF step this] 760 have "s'=Stuck". 761 with exec' 762 have "t=Stuck" 763 by (auto intro: Stuck_end) 764 with Stuck 765 show ?thesis 766 by (auto intro: exec.intros) 767 qed 768next 769 case (SeqSkip c\<^sub>2 s t) thus ?case 770 by (cases s) (fastforce intro: exec.intros elim: exec_elim_cases)+ 771next 772 case (SeqThrow c\<^sub>2 s t) thus ?case 773 by (fastforce intro: exec.intros elim: exec_elim_cases)+ 774next 775 case CondTrue thus ?case 776 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 777next 778 case CondFalse thus ?case 779 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 780next 781 case WhileTrue thus ?case 782 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 783next 784 case WhileFalse thus ?case 785 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 786next 787 case Call thus ?case 788 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 789next 790 case CallUndefined thus ?case 791 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 792next 793 case DynCom thus ?case 794 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 795next 796 case (Catch c\<^sub>1 s c\<^sub>1' s' c\<^sub>2 t) 797 have step: "\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1', s')" by fact 798 have exec': "\<Gamma>\<turnstile> \<langle>Catch c\<^sub>1' c\<^sub>2,s'\<rangle> \<Rightarrow> t" by fact 799 show ?case 800 proof (cases s) 801 case (Normal x) 802 note s_Normal = this 803 show ?thesis 804 proof (cases s') 805 case (Normal x') 806 from exec' [simplified Normal] 807 show ?thesis 808 proof (cases) 809 fix s'' 810 assume exec_c\<^sub>1': "\<Gamma>\<turnstile> \<langle>c\<^sub>1',Normal x'\<rangle> \<Rightarrow> Abrupt s''" 811 assume exec_c\<^sub>2: "\<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s''\<rangle> \<Rightarrow> t" 812 from Catch.hyps (2) Normal exec_c\<^sub>1' s_Normal 813 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> Abrupt s''" 814 by simp 815 from exec.CatchMatch [OF this exec_c\<^sub>2] s_Normal 816 show ?thesis by simp 817 next 818 assume exec_c\<^sub>1': "\<Gamma>\<turnstile> \<langle>c\<^sub>1',Normal x'\<rangle> \<Rightarrow> t" 819 assume t: "\<not> isAbr t" 820 from Catch.hyps (2) Normal exec_c\<^sub>1' s_Normal 821 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> t" 822 by simp 823 from exec.CatchMiss [OF this t] s_Normal 824 show ?thesis by simp 825 qed 826 next 827 case (Abrupt x') 828 with exec' have "t=Abrupt x'" 829 by (auto intro:Abrupt_end) 830 moreover 831 from step Abrupt 832 have "s=Abrupt x'" 833 by (auto intro: step_Abrupt_end) 834 ultimately 835 show ?thesis 836 by (auto intro: exec.intros) 837 next 838 case (Fault f) 839 from step_Fault_end [OF step this] s_Normal 840 obtain g c where 841 redex_c\<^sub>1: "redex c\<^sub>1 = Guard f g c" and 842 fail: "x \<notin> g" 843 by auto 844 hence "\<Gamma>\<turnstile> \<langle>redex c\<^sub>1,Normal x\<rangle> \<Rightarrow> Fault f" 845 by (auto intro: exec.intros) 846 from exec_redex_Fault [OF this] 847 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> Fault f". 848 moreover from Fault exec' have "t=Fault f" 849 by (auto intro: Fault_end) 850 ultimately 851 show ?thesis 852 using s_Normal 853 by (auto intro: exec.intros) 854 next 855 case Stuck 856 from step_Stuck_end [OF step this] s_Normal 857 have "(\<exists>r. redex c\<^sub>1 = Spec r \<and> (\<forall>t. (x, t) \<notin> r)) \<or> 858 (\<exists>p. redex c\<^sub>1 = Call p \<and> \<Gamma> p = None)" 859 by auto 860 moreover 861 { 862 fix r 863 assume "redex c\<^sub>1 = Spec r" and "(\<forall>t. (x, t) \<notin> r)" 864 hence "\<Gamma>\<turnstile> \<langle>redex c\<^sub>1,Normal x\<rangle> \<Rightarrow> Stuck" 865 by (auto intro: exec.intros) 866 from exec_redex_Stuck [OF this] 867 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> Stuck". 868 moreover from Stuck exec' have "t=Stuck" 869 by (auto intro: Stuck_end) 870 ultimately 871 have ?thesis 872 using s_Normal 873 by (auto intro: exec.intros) 874 } 875 moreover 876 { 877 fix p 878 assume "redex c\<^sub>1 = Call p" and "\<Gamma> p = None" 879 hence "\<Gamma>\<turnstile> \<langle>redex c\<^sub>1,Normal x\<rangle> \<Rightarrow> Stuck" 880 by (auto intro: exec.intros) 881 from exec_redex_Stuck [OF this] 882 have "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal x\<rangle> \<Rightarrow> Stuck". 883 moreover from Stuck exec' have "t=Stuck" 884 by (auto intro: Stuck_end) 885 ultimately 886 have ?thesis 887 using s_Normal 888 by (auto intro: exec.intros) 889 } 890 ultimately show ?thesis 891 by auto 892 qed 893 next 894 case (Abrupt x) 895 from step_Abrupt [OF step this] 896 have "s'=Abrupt x". 897 with exec' 898 have "t=Abrupt x" 899 by (auto intro: Abrupt_end) 900 with Abrupt 901 show ?thesis 902 by (auto intro: exec.intros) 903 next 904 case (Fault f) 905 from step_Fault [OF step this] 906 have "s'=Fault f". 907 with exec' 908 have "t=Fault f" 909 by (auto intro: Fault_end) 910 with Fault 911 show ?thesis 912 by (auto intro: exec.intros) 913 next 914 case Stuck 915 from step_Stuck [OF step this] 916 have "s'=Stuck". 917 with exec' 918 have "t=Stuck" 919 by (auto intro: Stuck_end) 920 with Stuck 921 show ?thesis 922 by (auto intro: exec.intros) 923 qed 924next 925 case CatchThrow thus ?case 926 by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) 927next 928 case CatchSkip thus ?case 929 by (fastforce intro: exec.intros elim: exec_elim_cases) 930next 931 case FaultProp thus ?case 932 by (fastforce intro: exec.intros elim: exec_elim_cases) 933next 934 case StuckProp thus ?case 935 by (fastforce intro: exec.intros elim: exec_elim_cases) 936next 937 case AbruptProp thus ?case 938 by (fastforce intro: exec.intros elim: exec_elim_cases) 939qed 940 941theorem steps_Skip_impl_exec: 942 assumes steps: "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (Skip,t)" 943 shows "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t" 944using steps 945proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 946 case Refl thus ?case 947 by (cases t) (auto intro: exec.intros) 948next 949 case (Trans c s c' s') 950 have "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')" and "\<Gamma>\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t" by fact+ 951 thus ?case 952 by (rule step_extend) 953qed 954 955theorem steps_Throw_impl_exec: 956 assumes steps: "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (Throw,Normal t)" 957 shows "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> Abrupt t" 958using steps 959proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 960 case Refl thus ?case 961 by (auto intro: exec.intros) 962next 963 case (Trans c s c' s') 964 have "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')" and "\<Gamma>\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> Abrupt t" by fact+ 965 thus ?case 966 by (rule step_extend) 967qed 968 969(* ************************************************************************ *) 970subsection \<open>Infinite Computations: \<open>\<Gamma>\<turnstile>(c, s) \<rightarrow> \<dots>(\<infinity>)\<close>\<close> 971(* ************************************************************************ *) 972 973definition inf:: "('s,'p,'f) body \<Rightarrow> ('s,'p,'f) config \<Rightarrow> bool" 974 ("_\<turnstile> _ \<rightarrow> \<dots>'(\<infinity>')" [60,80] 100) where 975"\<Gamma>\<turnstile> cfg \<rightarrow> \<dots>(\<infinity>) \<equiv> (\<exists>f. f (0::nat) = cfg \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (i+1)))" 976 977lemma not_infI: "\<lbrakk>\<And>f. \<lbrakk>f 0 = cfg; \<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False\<rbrakk> 978 \<Longrightarrow> \<not>\<Gamma>\<turnstile> cfg \<rightarrow> \<dots>(\<infinity>)" 979 by (auto simp add: inf_def) 980 981(* ************************************************************************ *) 982subsection \<open>Equivalence between Termination and the Absence of Infinite Computations\<close> 983(* ************************************************************************ *) 984 985 986lemma step_preserves_termination: 987 assumes step: "\<Gamma>\<turnstile>(c,s) \<rightarrow> (c',s')" 988 shows "\<Gamma>\<turnstile>c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c'\<down>s'" 989using step 990proof (induct) 991 case Basic thus ?case by (fastforce intro: terminates.intros) 992next 993 case Spec thus ?case by (fastforce intro: terminates.intros) 994next 995 case SpecStuck thus ?case by (fastforce intro: terminates.intros) 996next 997 case Guard thus ?case 998 by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) 999next 1000 case GuardFault thus ?case by (fastforce intro: terminates.intros) 1001next 1002 case (Seq c\<^sub>1 s c\<^sub>1' s' c\<^sub>2) thus ?case 1003 apply (cases s) 1004 apply (cases s') 1005 apply (fastforce intro: terminates.intros step_extend 1006 elim: terminates_Normal_elim_cases) 1007 apply (fastforce intro: terminates.intros dest: step_Abrupt_prop 1008 step_Fault_prop step_Stuck_prop)+ 1009 done 1010next 1011 case (SeqSkip c\<^sub>2 s) 1012 thus ?case 1013 apply (cases s) 1014 apply (fastforce intro: terminates.intros exec.intros 1015 elim: terminates_Normal_elim_cases )+ 1016 done 1017next 1018 case (SeqThrow c\<^sub>2 s) 1019 thus ?case 1020 by (fastforce intro: terminates.intros exec.intros 1021 elim: terminates_Normal_elim_cases ) 1022next 1023 case CondTrue 1024 thus ?case 1025 by (fastforce intro: terminates.intros exec.intros 1026 elim: terminates_Normal_elim_cases ) 1027next 1028 case CondFalse 1029 thus ?case 1030 by (fastforce intro: terminates.intros 1031 elim: terminates_Normal_elim_cases ) 1032next 1033 case WhileTrue 1034 thus ?case 1035 by (fastforce intro: terminates.intros 1036 elim: terminates_Normal_elim_cases ) 1037next 1038 case WhileFalse 1039 thus ?case 1040 by (fastforce intro: terminates.intros 1041 elim: terminates_Normal_elim_cases ) 1042next 1043 case Call 1044 thus ?case 1045 by (fastforce intro: terminates.intros 1046 elim: terminates_Normal_elim_cases ) 1047next 1048 case CallUndefined 1049 thus ?case 1050 by (fastforce intro: terminates.intros 1051 elim: terminates_Normal_elim_cases ) 1052next 1053 case DynCom 1054 thus ?case 1055 by (fastforce intro: terminates.intros 1056 elim: terminates_Normal_elim_cases ) 1057next 1058 case (Catch c\<^sub>1 s c\<^sub>1' s' c\<^sub>2) thus ?case 1059 apply (cases s) 1060 apply (cases s') 1061 apply (fastforce intro: terminates.intros step_extend 1062 elim: terminates_Normal_elim_cases) 1063 apply (fastforce intro: terminates.intros dest: step_Abrupt_prop 1064 step_Fault_prop step_Stuck_prop)+ 1065 done 1066next 1067 case CatchThrow 1068 thus ?case 1069 by (fastforce intro: terminates.intros exec.intros 1070 elim: terminates_Normal_elim_cases ) 1071next 1072 case (CatchSkip c\<^sub>2 s) 1073 thus ?case 1074 by (cases s) (fastforce intro: terminates.intros)+ 1075next 1076 case FaultProp thus ?case by (fastforce intro: terminates.intros) 1077next 1078 case StuckProp thus ?case by (fastforce intro: terminates.intros) 1079next 1080 case AbruptProp thus ?case by (fastforce intro: terminates.intros) 1081qed 1082 1083lemma steps_preserves_termination: 1084 assumes steps: "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (c',s')" 1085 shows "\<Gamma>\<turnstile>c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c'\<down>s'" 1086using steps 1087proof (induct rule: rtranclp_induct2 [consumes 1, case_names Refl Trans]) 1088 case Refl thus ?case . 1089next 1090 case Trans 1091 thus ?case 1092 by (blast dest: step_preserves_termination) 1093qed 1094 1095ML \<open> 1096 ML_Thms.bind_thm ("tranclp_induct2", Split_Rule.split_rule @{context} 1097 (Rule_Insts.read_instantiate @{context} 1098 [((("a", 0), Position.none), "(aa,ab)"), ((("b", 0), Position.none), "(ba,bb)")] [] 1099 @{thm tranclp_induct})); 1100\<close> 1101 1102lemma steps_preserves_termination': 1103 assumes steps: "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>+ (c',s')" 1104 shows "\<Gamma>\<turnstile>c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c'\<down>s'" 1105using steps 1106proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans]) 1107 case Step thus ?case by (blast intro: step_preserves_termination) 1108next 1109 case Trans 1110 thus ?case 1111 by (blast dest: step_preserves_termination) 1112qed 1113 1114 1115 1116definition head_com:: "('s,'p,'f) com \<Rightarrow> ('s,'p,'f) com" 1117where 1118"head_com c = 1119 (case c of 1120 Seq c\<^sub>1 c\<^sub>2 \<Rightarrow> c\<^sub>1 1121 | Catch c\<^sub>1 c\<^sub>2 \<Rightarrow> c\<^sub>1 1122 | _ \<Rightarrow> c)" 1123 1124 1125definition head:: "('s,'p,'f) config \<Rightarrow> ('s,'p,'f) config" 1126 where "head cfg = (head_com (fst cfg), snd cfg)" 1127 1128lemma le_Suc_cases: "\<lbrakk>\<And>i. \<lbrakk>i < k\<rbrakk> \<Longrightarrow> P i; P k\<rbrakk> \<Longrightarrow> \<forall>i<(Suc k). P i" 1129 apply clarify 1130 apply (case_tac "i=k") 1131 apply auto 1132 done 1133 1134lemma redex_Seq_False: "\<And>c' c''. (redex c = Seq c'' c') = False" 1135 by (induct c) auto 1136 1137lemma redex_Catch_False: "\<And>c' c''. (redex c = Catch c'' c') = False" 1138 by (induct c) auto 1139 1140 1141lemma infinite_computation_extract_head_Seq: 1142 assumes inf_comp: "\<forall>i::nat. \<Gamma>\<turnstile>f i \<rightarrow> f (i+1)" 1143 assumes f_0: "f 0 = (Seq c\<^sub>1 c\<^sub>2,s)" 1144 assumes not_fin: "\<forall>i<k. \<not> final (head (f i))" 1145 shows "\<forall>i<k. (\<exists>c' s'. f (i + 1) = (Seq c' c\<^sub>2, s')) \<and> 1146 \<Gamma>\<turnstile>head (f i) \<rightarrow> head (f (i+1))" 1147 (is "\<forall>i<k. ?P i") 1148using not_fin 1149proof (induct k) 1150 case 0 1151 show ?case by simp 1152next 1153 case (Suc k) 1154 have not_fin_Suc: 1155 "\<forall>i<Suc k. \<not> final (head (f i))" by fact 1156 from this[rule_format] have not_fin_k: 1157 "\<forall>i<k. \<not> final (head (f i))" 1158 apply clarify 1159 apply (subgoal_tac "i < Suc k") 1160 apply blast 1161 apply simp 1162 done 1163 1164 from Suc.hyps [OF this] 1165 have hyp: "\<forall>i<k. (\<exists>c' s'. f (i + 1) = (Seq c' c\<^sub>2, s')) \<and> 1166 \<Gamma>\<turnstile> head (f i) \<rightarrow> head (f (i + 1))". 1167 show ?case 1168 proof (rule le_Suc_cases) 1169 fix i 1170 assume "i < k" 1171 then show "?P i" 1172 by (rule hyp [rule_format]) 1173 next 1174 show "?P k" 1175 proof - 1176 from hyp [rule_format, of "k - 1"] f_0 1177 obtain c' fs' L' s' where f_k: "f k = (Seq c' c\<^sub>2, s')" 1178 by (cases k) auto 1179 from inf_comp [rule_format, of k] f_k 1180 have "\<Gamma>\<turnstile>(Seq c' c\<^sub>2, s') \<rightarrow> f (k + 1)" 1181 by simp 1182 moreover 1183 from not_fin_Suc [rule_format, of k] f_k 1184 have "\<not> final (c',s')" 1185 by (simp add: final_def head_def head_com_def) 1186 ultimately 1187 obtain c'' s'' where 1188 "\<Gamma>\<turnstile>(c', s') \<rightarrow> (c'', s'')" and 1189 "f (k + 1) = (Seq c'' c\<^sub>2, s'')" 1190 by cases (auto simp add: redex_Seq_False final_def) 1191 with f_k 1192 show ?thesis 1193 by (simp add: head_def head_com_def) 1194 qed 1195 qed 1196qed 1197 1198lemma infinite_computation_extract_head_Catch: 1199 assumes inf_comp: "\<forall>i::nat. \<Gamma>\<turnstile>f i \<rightarrow> f (i+1)" 1200 assumes f_0: "f 0 = (Catch c\<^sub>1 c\<^sub>2,s)" 1201 assumes not_fin: "\<forall>i<k. \<not> final (head (f i))" 1202 shows "\<forall>i<k. (\<exists>c' s'. f (i + 1) = (Catch c' c\<^sub>2, s')) \<and> 1203 \<Gamma>\<turnstile>head (f i) \<rightarrow> head (f (i+1))" 1204 (is "\<forall>i<k. ?P i") 1205using not_fin 1206proof (induct k) 1207 case 0 1208 show ?case by simp 1209next 1210 case (Suc k) 1211 have not_fin_Suc: 1212 "\<forall>i<Suc k. \<not> final (head (f i))" by fact 1213 from this[rule_format] have not_fin_k: 1214 "\<forall>i<k. \<not> final (head (f i))" 1215 apply clarify 1216 apply (subgoal_tac "i < Suc k") 1217 apply blast 1218 apply simp 1219 done 1220 1221 from Suc.hyps [OF this] 1222 have hyp: "\<forall>i<k. (\<exists>c' s'. f (i + 1) = (Catch c' c\<^sub>2, s')) \<and> 1223 \<Gamma>\<turnstile> head (f i) \<rightarrow> head (f (i + 1))". 1224 show ?case 1225 proof (rule le_Suc_cases) 1226 fix i 1227 assume "i < k" 1228 then show "?P i" 1229 by (rule hyp [rule_format]) 1230 next 1231 show "?P k" 1232 proof - 1233 from hyp [rule_format, of "k - 1"] f_0 1234 obtain c' fs' L' s' where f_k: "f k = (Catch c' c\<^sub>2, s')" 1235 by (cases k) auto 1236 from inf_comp [rule_format, of k] f_k 1237 have "\<Gamma>\<turnstile>(Catch c' c\<^sub>2, s') \<rightarrow> f (k + 1)" 1238 by simp 1239 moreover 1240 from not_fin_Suc [rule_format, of k] f_k 1241 have "\<not> final (c',s')" 1242 by (simp add: final_def head_def head_com_def) 1243 ultimately 1244 obtain c'' s'' where 1245 "\<Gamma>\<turnstile>(c', s') \<rightarrow> (c'', s'')" and 1246 "f (k + 1) = (Catch c'' c\<^sub>2, s'')" 1247 by cases (auto simp add: redex_Catch_False final_def)+ 1248 with f_k 1249 show ?thesis 1250 by (simp add: head_def head_com_def) 1251 qed 1252 qed 1253qed 1254 1255lemma no_inf_Throw: "\<not> \<Gamma>\<turnstile>(Throw,s) \<rightarrow> \<dots>(\<infinity>)" 1256proof 1257 assume "\<Gamma>\<turnstile> (Throw, s) \<rightarrow> \<dots>(\<infinity>)" 1258 then obtain f where 1259 step [rule_format]: "\<forall>i::nat. \<Gamma>\<turnstile>f i \<rightarrow> f (i+1)" and 1260 f_0: "f 0 = (Throw, s)" 1261 by (auto simp add: inf_def) 1262 from step [of 0, simplified f_0] step [of 1] 1263 show False 1264 by cases (auto elim: step_elim_cases) 1265qed 1266 1267lemma split_inf_Seq: 1268 assumes inf_comp: "\<Gamma>\<turnstile>(Seq c\<^sub>1 c\<^sub>2,s) \<rightarrow> \<dots>(\<infinity>)" 1269 shows "\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow> \<dots>(\<infinity>) \<or> 1270 (\<exists>s'. \<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow>\<^sup>* (Skip,s') \<and> \<Gamma>\<turnstile>(c\<^sub>2,s') \<rightarrow> \<dots>(\<infinity>))" 1271proof - 1272 from inf_comp obtain f where 1273 step: "\<forall>i::nat. \<Gamma>\<turnstile>f i \<rightarrow> f (i+1)" and 1274 f_0: "f 0 = (Seq c\<^sub>1 c\<^sub>2, s)" 1275 by (auto simp add: inf_def) 1276 from f_0 have head_f_0: "head (f 0) = (c\<^sub>1,s)" 1277 by (simp add: head_def head_com_def) 1278 show ?thesis 1279 proof (cases "\<exists>i. final (head (f i))") 1280 case True 1281 define k where "k = (LEAST i. final (head (f i)))" 1282 have less_k: "\<forall>i<k. \<not> final (head (f i))" 1283 apply (intro allI impI) 1284 apply (unfold k_def) 1285 apply (drule not_less_Least) 1286 apply auto 1287 done 1288 from infinite_computation_extract_head_Seq [OF step f_0 this] 1289 obtain step_head: "\<forall>i<k. \<Gamma>\<turnstile> head (f i) \<rightarrow> head (f (i + 1))" and 1290 conf: "\<forall>i<k. (\<exists>c' s'. f (i + 1) = (Seq c' c\<^sub>2, s'))" 1291 by blast 1292 from True 1293 have final_f_k: "final (head (f k))" 1294 apply - 1295 apply (erule exE) 1296 apply (drule LeastI) 1297 apply (simp add: k_def) 1298 done 1299 moreover 1300 from f_0 conf [rule_format, of "k - 1"] 1301 obtain c' s' where f_k: "f k = (Seq c' c\<^sub>2,s')" 1302 by (cases k) auto 1303 moreover 1304 from step_head have steps_head: "\<Gamma>\<turnstile>head (f 0) \<rightarrow>\<^sup>* head (f k)" 1305 proof (induct k) 1306 case 0 thus ?case by simp 1307 next 1308 case (Suc m) 1309 have step: "\<forall>i<Suc m. \<Gamma>\<turnstile> head (f i) \<rightarrow> head (f (i + 1))" by fact 1310 hence "\<forall>i<m. \<Gamma>\<turnstile> head (f i) \<rightarrow> head (f (i + 1))" 1311 by auto 1312 hence "\<Gamma>\<turnstile> head (f 0) \<rightarrow>\<^sup>* head (f m)" 1313 by (rule Suc.hyps) 1314 also from step [rule_format, of m] 1315 have "\<Gamma>\<turnstile> head (f m) \<rightarrow> head (f (m + 1))" by simp 1316 finally show ?case by simp 1317 qed 1318 { 1319 assume f_k: "f k = (Seq Skip c\<^sub>2, s')" 1320 with steps_head 1321 have "\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow>\<^sup>* (Skip,s')" 1322 using head_f_0 1323 by (simp add: head_def head_com_def) 1324 moreover 1325 from step [rule_format, of k] f_k 1326 obtain "\<Gamma>\<turnstile>(Seq Skip c\<^sub>2,s') \<rightarrow> (c\<^sub>2,s')" and 1327 f_Suc_k: "f (k + 1) = (c\<^sub>2,s')" 1328 by (fastforce elim: step.cases intro: step.intros) 1329 define g where "g i = f (i + (k + 1))" for i 1330 from f_Suc_k 1331 have g_0: "g 0 = (c\<^sub>2,s')" 1332 by (simp add: g_def) 1333 from step 1334 have "\<forall>i. \<Gamma>\<turnstile>g i \<rightarrow> g (i + 1)" 1335 by (simp add: g_def) 1336 with g_0 have "\<Gamma>\<turnstile>(c\<^sub>2,s') \<rightarrow> \<dots>(\<infinity>)" 1337 by (auto simp add: inf_def) 1338 ultimately 1339 have ?thesis 1340 by auto 1341 } 1342 moreover 1343 { 1344 fix x 1345 assume s': "s'=Normal x" and f_k: "f k = (Seq Throw c\<^sub>2, s')" 1346 from step [rule_format, of k] f_k s' 1347 obtain "\<Gamma>\<turnstile>(Seq Throw c\<^sub>2,s') \<rightarrow> (Throw,s')" and 1348 f_Suc_k: "f (k + 1) = (Throw,s')" 1349 by (fastforce elim: step_elim_cases intro: step.intros) 1350 define g where "g i = f (i + (k + 1))" for i 1351 from f_Suc_k 1352 have g_0: "g 0 = (Throw,s')" 1353 by (simp add: g_def) 1354 from step 1355 have "\<forall>i. \<Gamma>\<turnstile>g i \<rightarrow> g (i + 1)" 1356 by (simp add: g_def) 1357 with g_0 have "\<Gamma>\<turnstile>(Throw,s') \<rightarrow> \<dots>(\<infinity>)" 1358 by (auto simp add: inf_def) 1359 with no_inf_Throw 1360 have ?thesis 1361 by auto 1362 } 1363 ultimately 1364 show ?thesis 1365 by (auto simp add: final_def head_def head_com_def) 1366 next 1367 case False 1368 then have not_fin: "\<forall>i. \<not> final (head (f i))" 1369 by blast 1370 have "\<forall>i. \<Gamma>\<turnstile>head (f i) \<rightarrow> head (f (i + 1))" 1371 proof 1372 fix k 1373 from not_fin 1374 have "\<forall>i<(Suc k). \<not> final (head (f i))" 1375 by simp 1376 1377 from infinite_computation_extract_head_Seq [OF step f_0 this ] 1378 show "\<Gamma>\<turnstile> head (f k) \<rightarrow> head (f (k + 1))" by simp 1379 qed 1380 with head_f_0 have "\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow> \<dots>(\<infinity>)" 1381 by (auto simp add: inf_def) 1382 thus ?thesis 1383 by simp 1384 qed 1385qed 1386 1387lemma split_inf_Catch: 1388 assumes inf_comp: "\<Gamma>\<turnstile>(Catch c\<^sub>1 c\<^sub>2,s) \<rightarrow> \<dots>(\<infinity>)" 1389 shows "\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow> \<dots>(\<infinity>) \<or> 1390 (\<exists>s'. \<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow>\<^sup>* (Throw,Normal s') \<and> \<Gamma>\<turnstile>(c\<^sub>2,Normal s') \<rightarrow> \<dots>(\<infinity>))" 1391proof - 1392 from inf_comp obtain f where 1393 step: "\<forall>i::nat. \<Gamma>\<turnstile>f i \<rightarrow> f (i+1)" and 1394 f_0: "f 0 = (Catch c\<^sub>1 c\<^sub>2, s)" 1395 by (auto simp add: inf_def) 1396 from f_0 have head_f_0: "head (f 0) = (c\<^sub>1,s)" 1397 by (simp add: head_def head_com_def) 1398 show ?thesis 1399 proof (cases "\<exists>i. final (head (f i))") 1400 case True 1401 define k where "k = (LEAST i. final (head (f i)))" 1402 have less_k: "\<forall>i<k. \<not> final (head (f i))" 1403 apply (intro allI impI) 1404 apply (unfold k_def) 1405 apply (drule not_less_Least) 1406 apply auto 1407 done 1408 from infinite_computation_extract_head_Catch [OF step f_0 this] 1409 obtain step_head: "\<forall>i<k. \<Gamma>\<turnstile> head (f i) \<rightarrow> head (f (i + 1))" and 1410 conf: "\<forall>i<k. (\<exists>c' s'. f (i + 1) = (Catch c' c\<^sub>2, s'))" 1411 by blast 1412 from True 1413 have final_f_k: "final (head (f k))" 1414 apply - 1415 apply (erule exE) 1416 apply (drule LeastI) 1417 apply (simp add: k_def) 1418 done 1419 moreover 1420 from f_0 conf [rule_format, of "k - 1"] 1421 obtain c' s' where f_k: "f k = (Catch c' c\<^sub>2,s')" 1422 by (cases k) auto 1423 moreover 1424 from step_head have steps_head: "\<Gamma>\<turnstile>head (f 0) \<rightarrow>\<^sup>* head (f k)" 1425 proof (induct k) 1426 case 0 thus ?case by simp 1427 next 1428 case (Suc m) 1429 have step: "\<forall>i<Suc m. \<Gamma>\<turnstile> head (f i) \<rightarrow> head (f (i + 1))" by fact 1430 hence "\<forall>i<m. \<Gamma>\<turnstile> head (f i) \<rightarrow> head (f (i + 1))" 1431 by auto 1432 hence "\<Gamma>\<turnstile> head (f 0) \<rightarrow>\<^sup>* head (f m)" 1433 by (rule Suc.hyps) 1434 also from step [rule_format, of m] 1435 have "\<Gamma>\<turnstile> head (f m) \<rightarrow> head (f (m + 1))" by simp 1436 finally show ?case by simp 1437 qed 1438 { 1439 assume f_k: "f k = (Catch Skip c\<^sub>2, s')" 1440 with steps_head 1441 have "\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow>\<^sup>* (Skip,s')" 1442 using head_f_0 1443 by (simp add: head_def head_com_def) 1444 moreover 1445 from step [rule_format, of k] f_k 1446 obtain "\<Gamma>\<turnstile>(Catch Skip c\<^sub>2,s') \<rightarrow> (Skip,s')" and 1447 f_Suc_k: "f (k + 1) = (Skip,s')" 1448 by (fastforce elim: step.cases intro: step.intros) 1449 from step [rule_format, of "k+1", simplified f_Suc_k] 1450 have ?thesis 1451 by (rule no_step_final') (auto simp add: final_def) 1452 } 1453 moreover 1454 { 1455 fix x 1456 assume s': "s'=Normal x" and f_k: "f k = (Catch Throw c\<^sub>2, s')" 1457 with steps_head 1458 have "\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow>\<^sup>* (Throw,s')" 1459 using head_f_0 1460 by (simp add: head_def head_com_def) 1461 moreover 1462 from step [rule_format, of k] f_k s' 1463 obtain "\<Gamma>\<turnstile>(Catch Throw c\<^sub>2,s') \<rightarrow> (c\<^sub>2,s')" and 1464 f_Suc_k: "f (k + 1) = (c\<^sub>2,s')" 1465 by (fastforce elim: step_elim_cases intro: step.intros) 1466 define g where "g i = f (i + (k + 1))" for i 1467 from f_Suc_k 1468 have g_0: "g 0 = (c\<^sub>2,s')" 1469 by (simp add: g_def) 1470 from step 1471 have "\<forall>i. \<Gamma>\<turnstile>g i \<rightarrow> g (i + 1)" 1472 by (simp add: g_def) 1473 with g_0 have "\<Gamma>\<turnstile>(c\<^sub>2,s') \<rightarrow> \<dots>(\<infinity>)" 1474 by (auto simp add: inf_def) 1475 ultimately 1476 have ?thesis 1477 using s' 1478 by auto 1479 } 1480 ultimately 1481 show ?thesis 1482 by (auto simp add: final_def head_def head_com_def) 1483 next 1484 case False 1485 then have not_fin: "\<forall>i. \<not> final (head (f i))" 1486 by blast 1487 have "\<forall>i. \<Gamma>\<turnstile>head (f i) \<rightarrow> head (f (i + 1))" 1488 proof 1489 fix k 1490 from not_fin 1491 have "\<forall>i<(Suc k). \<not> final (head (f i))" 1492 by simp 1493 1494 from infinite_computation_extract_head_Catch [OF step f_0 this ] 1495 show "\<Gamma>\<turnstile> head (f k) \<rightarrow> head (f (k + 1))" by simp 1496 qed 1497 with head_f_0 have "\<Gamma>\<turnstile>(c\<^sub>1,s) \<rightarrow> \<dots>(\<infinity>)" 1498 by (auto simp add: inf_def) 1499 thus ?thesis 1500 by simp 1501 qed 1502qed 1503 1504lemma Skip_no_step: "\<Gamma>\<turnstile>(Skip,s) \<rightarrow> cfg \<Longrightarrow> P" 1505 apply (erule no_step_final') 1506 apply (simp add: final_def) 1507 done 1508 1509lemma not_inf_Stuck: "\<not> \<Gamma>\<turnstile>(c,Stuck) \<rightarrow> \<dots>(\<infinity>)" 1510proof (induct c) 1511 case Skip 1512 show ?case 1513 proof (rule not_infI) 1514 fix f 1515 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1516 assume f_0: "f 0 = (Skip, Stuck)" 1517 from f_step [of 0] f_0 1518 show False 1519 by (auto elim: Skip_no_step) 1520 qed 1521next 1522 case (Basic g) 1523 thus ?case 1524 proof (rule not_infI) 1525 fix f 1526 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1527 assume f_0: "f 0 = (Basic g, Stuck)" 1528 from f_step [of 0] f_0 f_step [of 1] 1529 show False 1530 by (fastforce elim: Skip_no_step step_elim_cases) 1531 qed 1532next 1533 case (Spec r) 1534 thus ?case 1535 proof (rule not_infI) 1536 fix f 1537 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1538 assume f_0: "f 0 = (Spec r, Stuck)" 1539 from f_step [of 0] f_0 f_step [of 1] 1540 show False 1541 by (fastforce elim: Skip_no_step step_elim_cases) 1542 qed 1543next 1544 case (Seq c\<^sub>1 c\<^sub>2) 1545 show ?case 1546 proof 1547 assume "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow> \<dots>(\<infinity>)" 1548 from split_inf_Seq [OF this] Seq.hyps 1549 show False 1550 by (auto dest: steps_Stuck_prop) 1551 qed 1552next 1553 case (Cond b c\<^sub>1 c\<^sub>2) 1554 show ?case 1555 proof (rule not_infI) 1556 fix f 1557 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1558 assume f_0: "f 0 = (Cond b c\<^sub>1 c\<^sub>2, Stuck)" 1559 from f_step [of 0] f_0 f_step [of 1] 1560 show False 1561 by (fastforce elim: Skip_no_step step_elim_cases) 1562 qed 1563next 1564 case (While b c) 1565 show ?case 1566 proof (rule not_infI) 1567 fix f 1568 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1569 assume f_0: "f 0 = (While b c, Stuck)" 1570 from f_step [of 0] f_0 f_step [of 1] 1571 show False 1572 by (fastforce elim: Skip_no_step step_elim_cases) 1573 qed 1574next 1575 case (Call p) 1576 show ?case 1577 proof (rule not_infI) 1578 fix f 1579 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1580 assume f_0: "f 0 = (Call p, Stuck)" 1581 from f_step [of 0] f_0 f_step [of 1] 1582 show False 1583 by (fastforce elim: Skip_no_step step_elim_cases) 1584 qed 1585next 1586 case (DynCom d) 1587 show ?case 1588 proof (rule not_infI) 1589 fix f 1590 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1591 assume f_0: "f 0 = (DynCom d, Stuck)" 1592 from f_step [of 0] f_0 f_step [of 1] 1593 show False 1594 by (fastforce elim: Skip_no_step step_elim_cases) 1595 qed 1596next 1597 case (Guard m g c) 1598 show ?case 1599 proof (rule not_infI) 1600 fix f 1601 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1602 assume f_0: "f 0 = (Guard m g c, Stuck)" 1603 from f_step [of 0] f_0 f_step [of 1] 1604 show False 1605 by (fastforce elim: Skip_no_step step_elim_cases) 1606 qed 1607next 1608 case Throw 1609 show ?case 1610 proof (rule not_infI) 1611 fix f 1612 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1613 assume f_0: "f 0 = (Throw, Stuck)" 1614 from f_step [of 0] f_0 f_step [of 1] 1615 show False 1616 by (fastforce elim: Skip_no_step step_elim_cases) 1617 qed 1618next 1619 case (Catch c\<^sub>1 c\<^sub>2) 1620 show ?case 1621 proof 1622 assume "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Stuck) \<rightarrow> \<dots>(\<infinity>)" 1623 from split_inf_Catch [OF this] Catch.hyps 1624 show False 1625 by (auto dest: steps_Stuck_prop) 1626 qed 1627qed 1628 1629lemma not_inf_Fault: "\<not> \<Gamma>\<turnstile>(c,Fault x) \<rightarrow> \<dots>(\<infinity>)" 1630proof (induct c) 1631 case Skip 1632 show ?case 1633 proof (rule not_infI) 1634 fix f 1635 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1636 assume f_0: "f 0 = (Skip, Fault x)" 1637 from f_step [of 0] f_0 1638 show False 1639 by (auto elim: Skip_no_step) 1640 qed 1641next 1642 case (Basic g) 1643 thus ?case 1644 proof (rule not_infI) 1645 fix f 1646 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1647 assume f_0: "f 0 = (Basic g, Fault x)" 1648 from f_step [of 0] f_0 f_step [of 1] 1649 show False 1650 by (fastforce elim: Skip_no_step step_elim_cases) 1651 qed 1652next 1653 case (Spec r) 1654 thus ?case 1655 proof (rule not_infI) 1656 fix f 1657 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1658 assume f_0: "f 0 = (Spec r, Fault x)" 1659 from f_step [of 0] f_0 f_step [of 1] 1660 show False 1661 by (fastforce elim: Skip_no_step step_elim_cases) 1662 qed 1663next 1664 case (Seq c\<^sub>1 c\<^sub>2) 1665 show ?case 1666 proof 1667 assume "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Fault x) \<rightarrow> \<dots>(\<infinity>)" 1668 from split_inf_Seq [OF this] Seq.hyps 1669 show False 1670 by (auto dest: steps_Fault_prop) 1671 qed 1672next 1673 case (Cond b c\<^sub>1 c\<^sub>2) 1674 show ?case 1675 proof (rule not_infI) 1676 fix f 1677 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1678 assume f_0: "f 0 = (Cond b c\<^sub>1 c\<^sub>2, Fault x)" 1679 from f_step [of 0] f_0 f_step [of 1] 1680 show False 1681 by (fastforce elim: Skip_no_step step_elim_cases) 1682 qed 1683next 1684 case (While b c) 1685 show ?case 1686 proof (rule not_infI) 1687 fix f 1688 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1689 assume f_0: "f 0 = (While b c, Fault x)" 1690 from f_step [of 0] f_0 f_step [of 1] 1691 show False 1692 by (fastforce elim: Skip_no_step step_elim_cases) 1693 qed 1694next 1695 case (Call p) 1696 show ?case 1697 proof (rule not_infI) 1698 fix f 1699 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1700 assume f_0: "f 0 = (Call p, Fault x)" 1701 from f_step [of 0] f_0 f_step [of 1] 1702 show False 1703 by (fastforce elim: Skip_no_step step_elim_cases) 1704 qed 1705next 1706 case (DynCom d) 1707 show ?case 1708 proof (rule not_infI) 1709 fix f 1710 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1711 assume f_0: "f 0 = (DynCom d, Fault x)" 1712 from f_step [of 0] f_0 f_step [of 1] 1713 show False 1714 by (fastforce elim: Skip_no_step step_elim_cases) 1715 qed 1716next 1717 case (Guard m g c) 1718 show ?case 1719 proof (rule not_infI) 1720 fix f 1721 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1722 assume f_0: "f 0 = (Guard m g c, Fault x)" 1723 from f_step [of 0] f_0 f_step [of 1] 1724 show False 1725 by (fastforce elim: Skip_no_step step_elim_cases) 1726 qed 1727next 1728 case Throw 1729 show ?case 1730 proof (rule not_infI) 1731 fix f 1732 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1733 assume f_0: "f 0 = (Throw, Fault x)" 1734 from f_step [of 0] f_0 f_step [of 1] 1735 show False 1736 by (fastforce elim: Skip_no_step step_elim_cases) 1737 qed 1738next 1739 case (Catch c\<^sub>1 c\<^sub>2) 1740 show ?case 1741 proof 1742 assume "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Fault x) \<rightarrow> \<dots>(\<infinity>)" 1743 from split_inf_Catch [OF this] Catch.hyps 1744 show False 1745 by (auto dest: steps_Fault_prop) 1746 qed 1747qed 1748 1749lemma not_inf_Abrupt: "\<not> \<Gamma>\<turnstile>(c,Abrupt s) \<rightarrow> \<dots>(\<infinity>)" 1750proof (induct c) 1751 case Skip 1752 show ?case 1753 proof (rule not_infI) 1754 fix f 1755 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1756 assume f_0: "f 0 = (Skip, Abrupt s)" 1757 from f_step [of 0] f_0 1758 show False 1759 by (auto elim: Skip_no_step) 1760 qed 1761next 1762 case (Basic g) 1763 thus ?case 1764 proof (rule not_infI) 1765 fix f 1766 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1767 assume f_0: "f 0 = (Basic g, Abrupt s)" 1768 from f_step [of 0] f_0 f_step [of 1] 1769 show False 1770 by (fastforce elim: Skip_no_step step_elim_cases) 1771 qed 1772next 1773 case (Spec r) 1774 thus ?case 1775 proof (rule not_infI) 1776 fix f 1777 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1778 assume f_0: "f 0 = (Spec r, Abrupt s)" 1779 from f_step [of 0] f_0 f_step [of 1] 1780 show False 1781 by (fastforce elim: Skip_no_step step_elim_cases) 1782 qed 1783next 1784 case (Seq c\<^sub>1 c\<^sub>2) 1785 show ?case 1786 proof 1787 assume "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Abrupt s) \<rightarrow> \<dots>(\<infinity>)" 1788 from split_inf_Seq [OF this] Seq.hyps 1789 show False 1790 by (auto dest: steps_Abrupt_prop) 1791 qed 1792next 1793 case (Cond b c\<^sub>1 c\<^sub>2) 1794 show ?case 1795 proof (rule not_infI) 1796 fix f 1797 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1798 assume f_0: "f 0 = (Cond b c\<^sub>1 c\<^sub>2, Abrupt s)" 1799 from f_step [of 0] f_0 f_step [of 1] 1800 show False 1801 by (fastforce elim: Skip_no_step step_elim_cases) 1802 qed 1803next 1804 case (While b c) 1805 show ?case 1806 proof (rule not_infI) 1807 fix f 1808 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1809 assume f_0: "f 0 = (While b c, Abrupt s)" 1810 from f_step [of 0] f_0 f_step [of 1] 1811 show False 1812 by (fastforce elim: Skip_no_step step_elim_cases) 1813 qed 1814next 1815 case (Call p) 1816 show ?case 1817 proof (rule not_infI) 1818 fix f 1819 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1820 assume f_0: "f 0 = (Call p, Abrupt s)" 1821 from f_step [of 0] f_0 f_step [of 1] 1822 show False 1823 by (fastforce elim: Skip_no_step step_elim_cases) 1824 qed 1825next 1826 case (DynCom d) 1827 show ?case 1828 proof (rule not_infI) 1829 fix f 1830 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1831 assume f_0: "f 0 = (DynCom d, Abrupt s)" 1832 from f_step [of 0] f_0 f_step [of 1] 1833 show False 1834 by (fastforce elim: Skip_no_step step_elim_cases) 1835 qed 1836next 1837 case (Guard m g c) 1838 show ?case 1839 proof (rule not_infI) 1840 fix f 1841 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1842 assume f_0: "f 0 = (Guard m g c, Abrupt s)" 1843 from f_step [of 0] f_0 f_step [of 1] 1844 show False 1845 by (fastforce elim: Skip_no_step step_elim_cases) 1846 qed 1847next 1848 case Throw 1849 show ?case 1850 proof (rule not_infI) 1851 fix f 1852 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1853 assume f_0: "f 0 = (Throw, Abrupt s)" 1854 from f_step [of 0] f_0 f_step [of 1] 1855 show False 1856 by (fastforce elim: Skip_no_step step_elim_cases) 1857 qed 1858next 1859 case (Catch c\<^sub>1 c\<^sub>2) 1860 show ?case 1861 proof 1862 assume "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Abrupt s) \<rightarrow> \<dots>(\<infinity>)" 1863 from split_inf_Catch [OF this] Catch.hyps 1864 show False 1865 by (auto dest: steps_Abrupt_prop) 1866 qed 1867qed 1868 1869 1870theorem terminates_impl_no_infinite_computation: 1871 assumes termi: "\<Gamma>\<turnstile>c \<down> s" 1872 shows "\<not> \<Gamma>\<turnstile>(c,s) \<rightarrow> \<dots>(\<infinity>)" 1873using termi 1874proof (induct) 1875 case (Skip s) thus ?case 1876 proof (rule not_infI) 1877 fix f 1878 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1879 assume f_0: "f 0 = (Skip, Normal s)" 1880 from f_step [of 0] f_0 1881 show False 1882 by (auto elim: Skip_no_step) 1883 qed 1884next 1885 case (Basic g s) 1886 thus ?case 1887 proof (rule not_infI) 1888 fix f 1889 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1890 assume f_0: "f 0 = (Basic g, Normal s)" 1891 from f_step [of 0] f_0 f_step [of 1] 1892 show False 1893 by (fastforce elim: Skip_no_step step_elim_cases) 1894 qed 1895next 1896 case (Spec r s) 1897 thus ?case 1898 proof (rule not_infI) 1899 fix f 1900 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1901 assume f_0: "f 0 = (Spec r, Normal s)" 1902 from f_step [of 0] f_0 f_step [of 1] 1903 show False 1904 by (fastforce elim: Skip_no_step step_elim_cases) 1905 qed 1906next 1907 case (Guard s g c m) 1908 have g: "s \<in> g" by fact 1909 have hyp: "\<not> \<Gamma>\<turnstile> (c, Normal s) \<rightarrow> \<dots>(\<infinity>)" by fact 1910 show ?case 1911 proof (rule not_infI) 1912 fix f 1913 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1914 assume f_0: "f 0 = (Guard m g c, Normal s)" 1915 from f_step [of 0] f_0 g 1916 have "f 1 = (c,Normal s)" 1917 by (fastforce elim: step_elim_cases) 1918 with f_step 1919 have "\<Gamma>\<turnstile> (c, Normal s) \<rightarrow> \<dots>(\<infinity>)" 1920 apply (simp add: inf_def) 1921 apply (rule_tac x="\<lambda>i. f (Suc i)" in exI) 1922 by simp 1923 with hyp show False .. 1924 qed 1925next 1926 case (GuardFault s g m c) 1927 have g: "s \<notin> g" by fact 1928 show ?case 1929 proof (rule not_infI) 1930 fix f 1931 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1932 assume f_0: "f 0 = (Guard m g c, Normal s)" 1933 from g f_step [of 0] f_0 f_step [of 1] 1934 show False 1935 by (fastforce elim: Skip_no_step step_elim_cases) 1936 qed 1937next 1938 case (Fault c m) 1939 thus ?case 1940 by (rule not_inf_Fault) 1941next 1942 case (Seq c\<^sub>1 s c\<^sub>2) 1943 show ?case 1944 proof 1945 assume "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> \<dots>(\<infinity>)" 1946 from split_inf_Seq [OF this] Seq.hyps 1947 show False 1948 by (auto intro: steps_Skip_impl_exec) 1949 qed 1950next 1951 case (CondTrue s b c1 c2) 1952 have b: "s \<in> b" by fact 1953 have hyp_c1: "\<not> \<Gamma>\<turnstile> (c1, Normal s) \<rightarrow> \<dots>(\<infinity>)" by fact 1954 show ?case 1955 proof (rule not_infI) 1956 fix f 1957 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1958 assume f_0: "f 0 = (Cond b c1 c2, Normal s)" 1959 from b f_step [of 0] f_0 1960 have "f 1 = (c1,Normal s)" 1961 by (auto elim: step_Normal_elim_cases) 1962 with f_step 1963 have "\<Gamma>\<turnstile> (c1, Normal s) \<rightarrow> \<dots>(\<infinity>)" 1964 apply (simp add: inf_def) 1965 apply (rule_tac x="\<lambda>i. f (Suc i)" in exI) 1966 by simp 1967 with hyp_c1 show False by simp 1968 qed 1969next 1970 case (CondFalse s b c2 c1) 1971 have b: "s \<notin> b" by fact 1972 have hyp_c2: "\<not> \<Gamma>\<turnstile> (c2, Normal s) \<rightarrow> \<dots>(\<infinity>)" by fact 1973 show ?case 1974 proof (rule not_infI) 1975 fix f 1976 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 1977 assume f_0: "f 0 = (Cond b c1 c2, Normal s)" 1978 from b f_step [of 0] f_0 1979 have "f 1 = (c2,Normal s)" 1980 by (auto elim: step_Normal_elim_cases) 1981 with f_step 1982 have "\<Gamma>\<turnstile> (c2, Normal s) \<rightarrow> \<dots>(\<infinity>)" 1983 apply (simp add: inf_def) 1984 apply (rule_tac x="\<lambda>i. f (Suc i)" in exI) 1985 by simp 1986 with hyp_c2 show False by simp 1987 qed 1988next 1989 case (WhileTrue s b c) 1990 have b: "s \<in> b" by fact 1991 have hyp_c: "\<not> \<Gamma>\<turnstile> (c, Normal s) \<rightarrow> \<dots>(\<infinity>)" by fact 1992 have hyp_w: "\<forall>s'. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s' \<longrightarrow> 1993 \<Gamma>\<turnstile>While b c \<down> s' \<and> \<not> \<Gamma>\<turnstile> (While b c, s') \<rightarrow> \<dots>(\<infinity>)" by fact 1994 have not_inf_Seq: "\<not> \<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow> \<dots>(\<infinity>)" 1995 proof 1996 assume "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow> \<dots>(\<infinity>)" 1997 from split_inf_Seq [OF this] hyp_c hyp_w show False 1998 by (auto intro: steps_Skip_impl_exec) 1999 qed 2000 show ?case 2001 proof 2002 assume "\<Gamma>\<turnstile> (While b c, Normal s) \<rightarrow> \<dots>(\<infinity>)" 2003 then obtain f where 2004 f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" and 2005 f_0: "f 0 = (While b c, Normal s)" 2006 by (auto simp add: inf_def) 2007 from f_step [of 0] f_0 b 2008 have "f 1 = (Seq c (While b c),Normal s)" 2009 by (auto elim: step_Normal_elim_cases) 2010 with f_step 2011 have "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow> \<dots>(\<infinity>)" 2012 apply (simp add: inf_def) 2013 apply (rule_tac x="\<lambda>i. f (Suc i)" in exI) 2014 by simp 2015 with not_inf_Seq show False by simp 2016 qed 2017next 2018 case (WhileFalse s b c) 2019 have b: "s \<notin> b" by fact 2020 show ?case 2021 proof (rule not_infI) 2022 fix f 2023 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 2024 assume f_0: "f 0 = (While b c, Normal s)" 2025 from b f_step [of 0] f_0 f_step [of 1] 2026 show False 2027 by (fastforce elim: Skip_no_step step_elim_cases) 2028 qed 2029next 2030 case (Call p bdy s) 2031 have bdy: "\<Gamma> p = Some bdy" by fact 2032 have hyp: "\<not> \<Gamma>\<turnstile> (bdy, Normal s) \<rightarrow> \<dots>(\<infinity>)" by fact 2033 show ?case 2034 proof (rule not_infI) 2035 fix f 2036 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 2037 assume f_0: "f 0 = (Call p, Normal s)" 2038 from bdy f_step [of 0] f_0 2039 have "f 1 = (bdy,Normal s)" 2040 by (auto elim: step_Normal_elim_cases) 2041 with f_step 2042 have "\<Gamma>\<turnstile> (bdy, Normal s) \<rightarrow> \<dots>(\<infinity>)" 2043 apply (simp add: inf_def) 2044 apply (rule_tac x="\<lambda>i. f (Suc i)" in exI) 2045 by simp 2046 with hyp show False by simp 2047 qed 2048next 2049 case (CallUndefined p s) 2050 have no_bdy: "\<Gamma> p = None" by fact 2051 show ?case 2052 proof (rule not_infI) 2053 fix f 2054 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 2055 assume f_0: "f 0 = (Call p, Normal s)" 2056 from no_bdy f_step [of 0] f_0 f_step [of 1] 2057 show False 2058 by (fastforce elim: Skip_no_step step_elim_cases) 2059 qed 2060next 2061 case (Stuck c) 2062 show ?case 2063 by (rule not_inf_Stuck) 2064next 2065 case (DynCom c s) 2066 have hyp: "\<not> \<Gamma>\<turnstile> (c s, Normal s) \<rightarrow> \<dots>(\<infinity>)" by fact 2067 show ?case 2068 proof (rule not_infI) 2069 fix f 2070 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 2071 assume f_0: "f 0 = (DynCom c, Normal s)" 2072 from f_step [of 0] f_0 2073 have "f (Suc 0) = (c s, Normal s)" 2074 by (auto elim: step_elim_cases) 2075 with f_step have "\<Gamma>\<turnstile> (c s, Normal s) \<rightarrow> \<dots>(\<infinity>)" 2076 apply (simp add: inf_def) 2077 apply (rule_tac x="\<lambda>i. f (Suc i)" in exI) 2078 by simp 2079 with hyp 2080 show False by simp 2081 qed 2082next 2083 case (Throw s) thus ?case 2084 proof (rule not_infI) 2085 fix f 2086 assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 2087 assume f_0: "f 0 = (Throw, Normal s)" 2088 from f_step [of 0] f_0 2089 show False 2090 by (auto elim: step_elim_cases) 2091 qed 2092next 2093 case (Abrupt c) 2094 show ?case 2095 by (rule not_inf_Abrupt) 2096next 2097 case (Catch c\<^sub>1 s c\<^sub>2) 2098 show ?case 2099 proof 2100 assume "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> \<dots>(\<infinity>)" 2101 from split_inf_Catch [OF this] Catch.hyps 2102 show False 2103 by (auto intro: steps_Throw_impl_exec) 2104 qed 2105qed 2106 2107 2108definition 2109 termi_call_steps :: "('s,'p,'f) body \<Rightarrow> (('s \<times> 'p) \<times> ('s \<times> 'p))set" 2110where 2111"termi_call_steps \<Gamma> = 2112 {((t,q),(s,p)). \<Gamma>\<turnstile>Call p\<down>Normal s \<and> 2113 (\<exists>c. \<Gamma>\<turnstile>(Call p,Normal s) \<rightarrow>\<^sup>+ (c,Normal t) \<and> redex c = Call q)}" 2114 2115 2116primrec subst_redex:: "('s,'p,'f)com \<Rightarrow> ('s,'p,'f)com \<Rightarrow> ('s,'p,'f)com" 2117where 2118"subst_redex Skip c = c" | 2119"subst_redex (Basic f) c = c" | 2120"subst_redex (Spec r) c = c" | 2121"subst_redex (Seq c\<^sub>1 c\<^sub>2) c = Seq (subst_redex c\<^sub>1 c) c\<^sub>2" | 2122"subst_redex (Cond b c\<^sub>1 c\<^sub>2) c = c" | 2123"subst_redex (While b c') c = c" | 2124"subst_redex (Call p) c = c" | 2125"subst_redex (DynCom d) c = c" | 2126"subst_redex (Guard f b c') c = c" | 2127"subst_redex (Throw) c = c" | 2128"subst_redex (Catch c\<^sub>1 c\<^sub>2) c = Catch (subst_redex c\<^sub>1 c) c\<^sub>2" 2129 2130lemma subst_redex_redex: 2131 "subst_redex c (redex c) = c" 2132 by (induct c) auto 2133 2134lemma redex_subst_redex: "redex (subst_redex c r) = redex r" 2135 by (induct c) auto 2136 2137lemma step_redex': 2138 shows "\<Gamma>\<turnstile>(redex c,s) \<rightarrow> (r',s') \<Longrightarrow> \<Gamma>\<turnstile>(c,s) \<rightarrow> (subst_redex c r',s')" 2139by (induct c) (auto intro: step.Seq step.Catch) 2140 2141 2142lemma step_redex: 2143 shows "\<Gamma>\<turnstile>(r,s) \<rightarrow> (r',s') \<Longrightarrow> \<Gamma>\<turnstile>(subst_redex c r,s) \<rightarrow> (subst_redex c r',s')" 2144by (induct c) (auto intro: step.Seq step.Catch) 2145 2146lemma steps_redex: 2147 assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>* (r', s')" 2148 shows "\<And>c. \<Gamma>\<turnstile>(subst_redex c r,s) \<rightarrow>\<^sup>* (subst_redex c r',s')" 2149using steps 2150proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 2151 case Refl 2152 show "\<Gamma>\<turnstile> (subst_redex c r', s') \<rightarrow>\<^sup>* (subst_redex c r', s')" 2153 by simp 2154next 2155 case (Trans r s r'' s'') 2156 have "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r'', s'')" by fact 2157 from step_redex [OF this] 2158 have "\<Gamma>\<turnstile> (subst_redex c r, s) \<rightarrow> (subst_redex c r'', s'')". 2159 also 2160 have "\<Gamma>\<turnstile> (subst_redex c r'', s'') \<rightarrow>\<^sup>* (subst_redex c r', s')" by fact 2161 finally show ?case . 2162qed 2163 2164ML \<open> 2165 ML_Thms.bind_thm ("trancl_induct2", Split_Rule.split_rule @{context} 2166 (Rule_Insts.read_instantiate @{context} 2167 [((("a", 0), Position.none), "(aa, ab)"), ((("b", 0), Position.none), "(ba, bb)")] [] 2168 @{thm trancl_induct})); 2169\<close> 2170 2171lemma steps_redex': 2172 assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>+ (r', s')" 2173 shows "\<And>c. \<Gamma>\<turnstile>(subst_redex c r,s) \<rightarrow>\<^sup>+ (subst_redex c r',s')" 2174using steps 2175proof (induct rule: tranclp_induct2 [consumes 1,case_names Step Trans]) 2176 case (Step r' s') 2177 have "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r', s')" by fact 2178 then have "\<Gamma>\<turnstile> (subst_redex c r, s) \<rightarrow> (subst_redex c r', s')" 2179 by (rule step_redex) 2180 then show "\<Gamma>\<turnstile> (subst_redex c r, s) \<rightarrow>\<^sup>+ (subst_redex c r', s')".. 2181next 2182 case (Trans r' s' r'' s'') 2183 have "\<Gamma>\<turnstile> (subst_redex c r, s) \<rightarrow>\<^sup>+ (subst_redex c r', s')" by fact 2184 also 2185 have "\<Gamma>\<turnstile> (r', s') \<rightarrow> (r'', s'')" by fact 2186 hence "\<Gamma>\<turnstile> (subst_redex c r', s') \<rightarrow> (subst_redex c r'', s'')" 2187 by (rule step_redex) 2188 finally show "\<Gamma>\<turnstile> (subst_redex c r, s) \<rightarrow>\<^sup>+ (subst_redex c r'', s'')" . 2189qed 2190 2191primrec seq:: "(nat \<Rightarrow> ('s,'p,'f)com) \<Rightarrow> 'p \<Rightarrow> nat \<Rightarrow> ('s,'p,'f)com" 2192where 2193"seq c p 0 = Call p" | 2194"seq c p (Suc i) = subst_redex (seq c p i) (c i)" 2195 2196 2197lemma renumber': 2198 assumes f: "\<forall>i. (a,f i) \<in> r\<^sup>* \<and> (f i,f(Suc i)) \<in> r" 2199 assumes a_b: "(a,b) \<in> r\<^sup>*" 2200 shows "b = f 0 \<Longrightarrow> (\<exists>f. f 0 = a \<and> (\<forall>i. (f i, f(Suc i)) \<in> r))" 2201using a_b 2202proof (induct rule: converse_rtrancl_induct [consumes 1]) 2203 assume "b = f 0" 2204 with f show "\<exists>f. f 0 = b \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)" 2205 by blast 2206next 2207 fix a z 2208 assume a_z: "(a, z) \<in> r" and "(z, b) \<in> r\<^sup>*" 2209 assume "b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)" 2210 "b = f 0" 2211 then obtain f where f0: "f 0 = z" and seq: "\<forall>i. (f i, f (Suc i)) \<in> r" 2212 by iprover 2213 { 2214 fix i have "((\<lambda>i. case i of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i) i, f i) \<in> r" 2215 using seq a_z f0 2216 by (cases i) auto 2217 } 2218 then 2219 show "\<exists>f. f 0 = a \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)" 2220 by - (rule exI [where x="\<lambda>i. case i of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i"],simp) 2221qed 2222 2223lemma renumber: 2224 "\<forall>i. (a,f i) \<in> r\<^sup>* \<and> (f i,f(Suc i)) \<in> r 2225 \<Longrightarrow> \<exists>f. f 0 = a \<and> (\<forall>i. (f i, f(Suc i)) \<in> r)" 2226 by (blast dest:renumber') 2227 2228lemma lem: 2229 "\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y 2230 \<Longrightarrow> ((b,a) \<in> {(y,x). P x \<and> r x y}\<^sup>+) = ((b,a) \<in> {(y,x). P x \<and> r\<^sup>+\<^sup>+ x y})" 2231apply(rule iffI) 2232 apply clarify 2233 apply(erule trancl_induct) 2234 apply blast 2235 apply(blast intro:tranclp_trans) 2236apply clarify 2237apply(erule tranclp_induct) 2238 apply blast 2239apply(blast intro:trancl_trans) 2240done 2241 2242corollary terminates_impl_no_infinite_trans_computation: 2243 assumes terminates: "\<Gamma>\<turnstile>c\<down>s" 2244 shows "\<not>(\<exists>f. f 0 = (c,s) \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow>\<^sup>+ f(Suc i)))" 2245proof - 2246 have "wf({(y,x). \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* x \<and> \<Gamma>\<turnstile>x \<rightarrow> y}\<^sup>+)" 2247 proof (rule wf_trancl) 2248 show "wf {(y, x). \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* x \<and> \<Gamma>\<turnstile>x \<rightarrow> y}" 2249 proof (simp only: wf_iff_no_infinite_down_chain,clarify,simp) 2250 fix f 2251 assume "\<forall>i. \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 2252 hence "\<exists>f. f (0::nat) = (c,s) \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i))" 2253 by (rule renumber [to_pred]) 2254 moreover from terminates_impl_no_infinite_computation [OF terminates] 2255 have "\<not> (\<exists>f. f (0::nat) = (c, s) \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)))" 2256 by (simp add: inf_def) 2257 ultimately show False 2258 by simp 2259 qed 2260 qed 2261 hence "\<not> (\<exists>f. \<forall>i. (f (Suc i), f i) 2262 \<in> {(y, x). \<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* x \<and> \<Gamma>\<turnstile>x \<rightarrow> y}\<^sup>+)" 2263 by (simp add: wf_iff_no_infinite_down_chain) 2264 thus ?thesis 2265 proof (rule contrapos_nn) 2266 assume "\<exists>f. f (0::nat) = (c, s) \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow>\<^sup>+ f (Suc i))" 2267 then obtain f where 2268 f0: "f 0 = (c, s)" and 2269 seq: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow>\<^sup>+ f (Suc i)" 2270 by iprover 2271 show 2272 "\<exists>f. \<forall>i. (f (Suc i), f i) \<in> {(y, x). \<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* x \<and> \<Gamma>\<turnstile>x \<rightarrow> y}\<^sup>+" 2273 proof (rule exI [where x=f],rule allI) 2274 fix i 2275 show "(f (Suc i), f i) \<in> {(y, x). \<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* x \<and> \<Gamma>\<turnstile>x \<rightarrow> y}\<^sup>+" 2276 proof - 2277 { 2278 fix i have "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* f i" 2279 proof (induct i) 2280 case 0 show "\<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* f 0" 2281 by (simp add: f0) 2282 next 2283 case (Suc n) 2284 have "\<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* f n" by fact 2285 with seq show "\<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* f (Suc n)" 2286 by (blast intro: tranclp_into_rtranclp rtranclp_trans) 2287 qed 2288 } 2289 hence "\<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* f i" 2290 by iprover 2291 with seq have 2292 "(f (Suc i), f i) \<in> {(y, x). \<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* x \<and> \<Gamma>\<turnstile>x \<rightarrow>\<^sup>+ y}" 2293 by clarsimp 2294 moreover 2295 have "\<forall>y. \<Gamma>\<turnstile>f i \<rightarrow>\<^sup>+ y\<longrightarrow>\<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* f i\<longrightarrow>\<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* y" 2296 by (blast intro: tranclp_into_rtranclp rtranclp_trans) 2297 ultimately 2298 show ?thesis 2299 by (subst lem ) 2300 qed 2301 qed 2302 qed 2303qed 2304 2305theorem wf_termi_call_steps: "wf (termi_call_steps \<Gamma>)" 2306proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, 2307 clarify,simp) 2308 fix f 2309 assume inf: "\<forall>i. (\<lambda>(t, q) (s, p). 2310 \<Gamma>\<turnstile>Call p \<down> Normal s \<and> 2311 (\<exists>c. \<Gamma>\<turnstile> (Call p, Normal s) \<rightarrow>\<^sup>+ (c, Normal t) \<and> redex c = Call q)) 2312 (f (Suc i)) (f i)" 2313 define s where "s i = fst (f i)" for i :: nat 2314 define p where "p i = (snd (f i)::'b)" for i :: nat 2315 from inf 2316 have inf': "\<forall>i. \<Gamma>\<turnstile>Call (p i) \<down> Normal (s i) \<and> 2317 (\<exists>c. \<Gamma>\<turnstile> (Call (p i), Normal (s i)) \<rightarrow>\<^sup>+ (c, Normal (s (i+1))) \<and> 2318 redex c = Call (p (i+1)))" 2319 apply - 2320 apply (rule allI) 2321 apply (erule_tac x=i in allE) 2322 apply (auto simp add: s_def p_def) 2323 done 2324 show False 2325 proof - 2326 from inf' 2327 have "\<exists>c. \<forall>i. \<Gamma>\<turnstile>Call (p i) \<down> Normal (s i) \<and> 2328 \<Gamma>\<turnstile> (Call (p i), Normal (s i)) \<rightarrow>\<^sup>+ (c i, Normal (s (i+1))) \<and> 2329 redex (c i) = Call (p (i+1))" 2330 apply - 2331 apply (rule choice) 2332 by blast 2333 then obtain c where 2334 termi_c: "\<forall>i. \<Gamma>\<turnstile>Call (p i) \<down> Normal (s i)" and 2335 steps_c: "\<forall>i. \<Gamma>\<turnstile> (Call (p i), Normal (s i)) \<rightarrow>\<^sup>+ (c i, Normal (s (i+1)))" and 2336 red_c: "\<forall>i. redex (c i) = Call (p (i+1))" 2337 by auto 2338 define g where "g i = (seq c (p 0) i,Normal (s i)::('a,'c) xstate)" for i 2339 from red_c [rule_format, of 0] 2340 have "g 0 = (Call (p 0), Normal (s 0))" 2341 by (simp add: g_def) 2342 moreover 2343 { 2344 fix i 2345 have "redex (seq c (p 0) i) = Call (p i)" 2346 by (induct i) (auto simp add: redex_subst_redex red_c) 2347 from this [symmetric] 2348 have "subst_redex (seq c (p 0) i) (Call (p i)) = (seq c (p 0) i)" 2349 by (simp add: subst_redex_redex) 2350 } note subst_redex_seq = this 2351 have "\<forall>i. \<Gamma>\<turnstile> (g i) \<rightarrow>\<^sup>+ (g (i+1))" 2352 proof 2353 fix i 2354 from steps_c [rule_format, of i] 2355 have "\<Gamma>\<turnstile> (Call (p i), Normal (s i)) \<rightarrow>\<^sup>+ (c i, Normal (s (i + 1)))". 2356 from steps_redex' [OF this, of "(seq c (p 0) i)"] 2357 have "\<Gamma>\<turnstile> (subst_redex (seq c (p 0) i) (Call (p i)), Normal (s i)) \<rightarrow>\<^sup>+ 2358 (subst_redex (seq c (p 0) i) (c i), Normal (s (i + 1)))" . 2359 hence "\<Gamma>\<turnstile> (seq c (p 0) i, Normal (s i)) \<rightarrow>\<^sup>+ 2360 (seq c (p 0) (i+1), Normal (s (i + 1)))" 2361 by (simp add: subst_redex_seq) 2362 thus "\<Gamma>\<turnstile> (g i) \<rightarrow>\<^sup>+ (g (i+1))" 2363 by (simp add: g_def) 2364 qed 2365 moreover 2366 from terminates_impl_no_infinite_trans_computation [OF termi_c [rule_format, of 0]] 2367 have "\<not> (\<exists>f. f 0 = (Call (p 0), Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i)))" . 2368 ultimately show False 2369 by auto 2370 qed 2371qed 2372 2373 2374lemma no_infinite_computation_implies_wf: 2375 assumes not_inf: "\<not> \<Gamma>\<turnstile> (c, s) \<rightarrow> \<dots>(\<infinity>)" 2376 shows "wf {(c2,c1). \<Gamma> \<turnstile> (c,s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma> \<turnstile> c1 \<rightarrow> c2}" 2377proof (simp only: wf_iff_no_infinite_down_chain,clarify, simp) 2378 fix f 2379 assume "\<forall>i. \<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)" 2380 hence "\<exists>f. f 0 = (c, s) \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i))" 2381 by (rule renumber [to_pred]) 2382 moreover from not_inf 2383 have "\<not> (\<exists>f. f 0 = (c, s) \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)))" 2384 by (simp add: inf_def) 2385 ultimately show False 2386 by simp 2387qed 2388 2389lemma not_final_Stuck_step: "\<not> final (c,Stuck) \<Longrightarrow> \<exists>c' s'. \<Gamma>\<turnstile> (c, Stuck) \<rightarrow> (c',s')" 2390by (induct c) (fastforce intro: step.intros simp add: final_def)+ 2391 2392lemma not_final_Abrupt_step: 2393 "\<not> final (c,Abrupt s) \<Longrightarrow> \<exists>c' s'. \<Gamma>\<turnstile> (c, Abrupt s) \<rightarrow> (c',s')" 2394by (induct c) (fastforce intro: step.intros simp add: final_def)+ 2395 2396lemma not_final_Fault_step: 2397 "\<not> final (c,Fault f) \<Longrightarrow> \<exists>c' s'. \<Gamma>\<turnstile> (c, Fault f) \<rightarrow> (c',s')" 2398by (induct c) (fastforce intro: step.intros simp add: final_def)+ 2399 2400lemma not_final_Normal_step: 2401 "\<not> final (c,Normal s) \<Longrightarrow> \<exists>c' s'. \<Gamma>\<turnstile> (c, Normal s) \<rightarrow> (c',s')" 2402proof (induct c) 2403 case Skip thus ?case by (fastforce intro: step.intros simp add: final_def) 2404next 2405 case Basic thus ?case by (fastforce intro: step.intros) 2406next 2407 case (Spec r) 2408 thus ?case 2409 by (cases "\<exists>t. (s,t) \<in> r") (fastforce intro: step.intros)+ 2410next 2411 case (Seq c\<^sub>1 c\<^sub>2) 2412 thus ?case 2413 by (cases "final (c\<^sub>1,Normal s)") (fastforce intro: step.intros simp add: final_def)+ 2414next 2415 case (Cond b c1 c2) 2416 show ?case 2417 by (cases "s \<in> b") (fastforce intro: step.intros)+ 2418next 2419 case (While b c) 2420 show ?case 2421 by (cases "s \<in> b") (fastforce intro: step.intros)+ 2422next 2423 case (Call p) 2424 show ?case 2425 by (cases "\<Gamma> p") (fastforce intro: step.intros)+ 2426next 2427 case DynCom thus ?case by (fastforce intro: step.intros) 2428next 2429 case (Guard f g c) 2430 show ?case 2431 by (cases "s \<in> g") (fastforce intro: step.intros)+ 2432next 2433 case Throw 2434 thus ?case by (fastforce intro: step.intros simp add: final_def) 2435next 2436 case (Catch c\<^sub>1 c\<^sub>2) 2437 thus ?case 2438 by (cases "final (c\<^sub>1,Normal s)") (fastforce intro: step.intros simp add: final_def)+ 2439qed 2440 2441lemma final_termi: 2442"final (c,s) \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s" 2443 by (cases s) (auto simp add: final_def terminates.intros) 2444 2445 2446lemma split_computation: 2447assumes steps: "\<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>* (c\<^sub>f, s\<^sub>f)" 2448assumes not_final: "\<not> final (c,s)" 2449assumes final: "final (c\<^sub>f,s\<^sub>f)" 2450shows "\<exists>c' s'. \<Gamma>\<turnstile> (c, s) \<rightarrow> (c',s') \<and> \<Gamma>\<turnstile> (c', s') \<rightarrow>\<^sup>* (c\<^sub>f, s\<^sub>f)" 2451using steps not_final final 2452proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 2453 case Refl thus ?case by simp 2454next 2455 case (Trans c s c' s') 2456 thus ?case by auto 2457qed 2458 2459lemma wf_implies_termi_reach_step_case: 2460assumes hyp: "\<And>c' s'. \<Gamma>\<turnstile> (c, Normal s) \<rightarrow> (c', s') \<Longrightarrow> \<Gamma>\<turnstile>c' \<down> s'" 2461shows "\<Gamma>\<turnstile>c \<down> Normal s" 2462using hyp 2463proof (induct c) 2464 case Skip show ?case by (fastforce intro: terminates.intros) 2465next 2466 case Basic show ?case by (fastforce intro: terminates.intros) 2467next 2468 case (Spec r) 2469 show ?case 2470 by (cases "\<exists>t. (s,t)\<in>r") (fastforce intro: terminates.intros)+ 2471next 2472 case (Seq c\<^sub>1 c\<^sub>2) 2473 have hyp: "\<And>c' s'. \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (c', s') \<Longrightarrow> \<Gamma>\<turnstile>c' \<down> s'" by fact 2474 show ?case 2475 proof (rule terminates.Seq) 2476 { 2477 fix c' s' 2478 assume step_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow> (c', s')" 2479 have "\<Gamma>\<turnstile>c' \<down> s'" 2480 proof - 2481 from step_c\<^sub>1 2482 have "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (Seq c' c\<^sub>2, s')" 2483 by (rule step.Seq) 2484 from hyp [OF this] 2485 have "\<Gamma>\<turnstile>Seq c' c\<^sub>2 \<down> s'". 2486 thus "\<Gamma>\<turnstile>c'\<down> s'" 2487 by cases auto 2488 qed 2489 } 2490 from Seq.hyps (1) [OF this] 2491 show "\<Gamma>\<turnstile>c\<^sub>1 \<down> Normal s". 2492 next 2493 show "\<forall>s'. \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 \<down> s'" 2494 proof (intro allI impI) 2495 fix s' 2496 assume exec_c\<^sub>1: "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'" 2497 show "\<Gamma>\<turnstile>c\<^sub>2 \<down> s'" 2498 proof (cases "final (c\<^sub>1,Normal s)") 2499 case True 2500 hence "c\<^sub>1=Skip \<or> c\<^sub>1=Throw" 2501 by (simp add: final_def) 2502 thus ?thesis 2503 proof 2504 assume Skip: "c\<^sub>1=Skip" 2505 have "\<Gamma>\<turnstile>(Seq Skip c\<^sub>2,Normal s) \<rightarrow> (c\<^sub>2,Normal s)" 2506 by (rule step.SeqSkip) 2507 from hyp [simplified Skip, OF this] 2508 have "\<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s" . 2509 moreover from exec_c\<^sub>1 Skip 2510 have "s'=Normal s" 2511 by (auto elim: exec_Normal_elim_cases) 2512 ultimately show ?thesis by simp 2513 next 2514 assume Throw: "c\<^sub>1=Throw" 2515 with exec_c\<^sub>1 have "s'=Abrupt s" 2516 by (auto elim: exec_Normal_elim_cases) 2517 thus ?thesis 2518 by auto 2519 qed 2520 next 2521 case False 2522 from exec_impl_steps [OF exec_c\<^sub>1] 2523 obtain c\<^sub>f t where 2524 steps_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow>\<^sup>* (c\<^sub>f, t)" and 2525 fin:"(case s' of 2526 Abrupt x \<Rightarrow> c\<^sub>f = Throw \<and> t = Normal x 2527 | _ \<Rightarrow> c\<^sub>f = Skip \<and> t = s')" 2528 by (fastforce split: xstate.splits) 2529 with fin have final: "final (c\<^sub>f,t)" 2530 by (cases s') (auto simp add: final_def) 2531 from split_computation [OF steps_c\<^sub>1 False this] 2532 obtain c'' s'' where 2533 first: "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow> (c'', s'')" and 2534 rest: "\<Gamma>\<turnstile> (c'', s'') \<rightarrow>\<^sup>* (c\<^sub>f, t)" 2535 by blast 2536 from step.Seq [OF first] 2537 have "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (Seq c'' c\<^sub>2, s'')". 2538 from hyp [OF this] 2539 have termi_s'': "\<Gamma>\<turnstile>Seq c'' c\<^sub>2 \<down> s''". 2540 show ?thesis 2541 proof (cases s'') 2542 case (Normal x) 2543 from termi_s'' [simplified Normal] 2544 have termi_c\<^sub>2: "\<forall>t. \<Gamma>\<turnstile> \<langle>c'',Normal x\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 \<down> t" 2545 by cases 2546 show ?thesis 2547 proof (cases "\<exists>x'. s'=Abrupt x'") 2548 case False 2549 with fin obtain "c\<^sub>f=Skip" "t=s'" 2550 by (cases s') auto 2551 from steps_Skip_impl_exec [OF rest [simplified this]] Normal 2552 have "\<Gamma>\<turnstile> \<langle>c'',Normal x\<rangle> \<Rightarrow> s'" 2553 by simp 2554 from termi_c\<^sub>2 [rule_format, OF this] 2555 show "\<Gamma>\<turnstile>c\<^sub>2 \<down> s'" . 2556 next 2557 case True 2558 with fin obtain x' where s': "s'=Abrupt x'" and "c\<^sub>f=Throw" "t=Normal x'" 2559 by auto 2560 from steps_Throw_impl_exec [OF rest [simplified this]] Normal 2561 have "\<Gamma>\<turnstile> \<langle>c'',Normal x\<rangle> \<Rightarrow> Abrupt x'" 2562 by simp 2563 from termi_c\<^sub>2 [rule_format, OF this] s' 2564 show "\<Gamma>\<turnstile>c\<^sub>2 \<down> s'" by simp 2565 qed 2566 next 2567 case (Abrupt x) 2568 from steps_Abrupt_prop [OF rest this] 2569 have "t=Abrupt x" by simp 2570 with fin have "s'=Abrupt x" 2571 by (cases s') auto 2572 thus "\<Gamma>\<turnstile>c\<^sub>2 \<down> s'" 2573 by auto 2574 next 2575 case (Fault f) 2576 from steps_Fault_prop [OF rest this] 2577 have "t=Fault f" by simp 2578 with fin have "s'=Fault f" 2579 by (cases s') auto 2580 thus "\<Gamma>\<turnstile>c\<^sub>2 \<down> s'" 2581 by auto 2582 next 2583 case Stuck 2584 from steps_Stuck_prop [OF rest this] 2585 have "t=Stuck" by simp 2586 with fin have "s'=Stuck" 2587 by (cases s') auto 2588 thus "\<Gamma>\<turnstile>c\<^sub>2 \<down> s'" 2589 by auto 2590 qed 2591 qed 2592 qed 2593 qed 2594next 2595 case (Cond b c\<^sub>1 c\<^sub>2) 2596 have hyp: "\<And>c' s'. \<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (c', s') \<Longrightarrow> \<Gamma>\<turnstile>c' \<down> s'" by fact 2597 show ?case 2598 proof (cases "s\<in>b") 2599 case True 2600 then have "\<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (c\<^sub>1, Normal s)" 2601 by (rule step.CondTrue) 2602 from hyp [OF this] have "\<Gamma>\<turnstile>c\<^sub>1 \<down> Normal s". 2603 with True show ?thesis 2604 by (auto intro: terminates.intros) 2605 next 2606 case False 2607 then have "\<Gamma>\<turnstile> (Cond b c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (c\<^sub>2, Normal s)" 2608 by (rule step.CondFalse) 2609 from hyp [OF this] have "\<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s". 2610 with False show ?thesis 2611 by (auto intro: terminates.intros) 2612 qed 2613next 2614 case (While b c) 2615 have hyp: "\<And>c' s'. \<Gamma>\<turnstile> (While b c, Normal s) \<rightarrow> (c', s') \<Longrightarrow> \<Gamma>\<turnstile>c' \<down> s'" by fact 2616 show ?case 2617 proof (cases "s\<in>b") 2618 case True 2619 then have "\<Gamma>\<turnstile> (While b c, Normal s) \<rightarrow> (Seq c (While b c), Normal s)" 2620 by (rule step.WhileTrue) 2621 from hyp [OF this] have "\<Gamma>\<turnstile>(Seq c (While b c)) \<down> Normal s". 2622 with True show ?thesis 2623 by (auto elim: terminates_Normal_elim_cases intro: terminates.intros) 2624 next 2625 case False 2626 thus ?thesis 2627 by (auto intro: terminates.intros) 2628 qed 2629next 2630 case (Call p) 2631 have hyp: "\<And>c' s'. \<Gamma>\<turnstile> (Call p, Normal s) \<rightarrow> (c', s') \<Longrightarrow> \<Gamma>\<turnstile>c' \<down> s'" by fact 2632 show ?case 2633 proof (cases "\<Gamma> p") 2634 case None 2635 thus ?thesis 2636 by (auto intro: terminates.intros) 2637 next 2638 case (Some bdy) 2639 then have "\<Gamma>\<turnstile> (Call p, Normal s) \<rightarrow> (bdy, Normal s)" 2640 by (rule step.Call) 2641 from hyp [OF this] have "\<Gamma>\<turnstile>bdy \<down> Normal s". 2642 with Some show ?thesis 2643 by (auto intro: terminates.intros) 2644 qed 2645next 2646 case (DynCom c) 2647 have hyp: "\<And>c' s'. \<Gamma>\<turnstile> (DynCom c, Normal s) \<rightarrow> (c', s') \<Longrightarrow> \<Gamma>\<turnstile>c' \<down> s'" by fact 2648 have "\<Gamma>\<turnstile> (DynCom c, Normal s) \<rightarrow> (c s, Normal s)" 2649 by (rule step.DynCom) 2650 from hyp [OF this] have "\<Gamma>\<turnstile>c s \<down> Normal s". 2651 then show ?case 2652 by (auto intro: terminates.intros) 2653next 2654 case (Guard f g c) 2655 have hyp: "\<And>c' s'. \<Gamma>\<turnstile> (Guard f g c, Normal s) \<rightarrow> (c', s') \<Longrightarrow> \<Gamma>\<turnstile>c' \<down> s'" by fact 2656 show ?case 2657 proof (cases "s\<in>g") 2658 case True 2659 then have "\<Gamma>\<turnstile> (Guard f g c, Normal s) \<rightarrow> (c, Normal s)" 2660 by (rule step.Guard) 2661 from hyp [OF this] have "\<Gamma>\<turnstile>c\<down> Normal s". 2662 with True show ?thesis 2663 by (auto intro: terminates.intros) 2664 next 2665 case False 2666 thus ?thesis 2667 by (auto intro: terminates.intros) 2668 qed 2669next 2670 case Throw show ?case by (auto intro: terminates.intros) 2671next 2672 case (Catch c\<^sub>1 c\<^sub>2) 2673 have hyp: "\<And>c' s'. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (c', s') \<Longrightarrow> \<Gamma>\<turnstile>c' \<down> s'" by fact 2674 show ?case 2675 proof (rule terminates.Catch) 2676 { 2677 fix c' s' 2678 assume step_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow> (c', s')" 2679 have "\<Gamma>\<turnstile>c' \<down> s'" 2680 proof - 2681 from step_c\<^sub>1 2682 have "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (Catch c' c\<^sub>2, s')" 2683 by (rule step.Catch) 2684 from hyp [OF this] 2685 have "\<Gamma>\<turnstile>Catch c' c\<^sub>2 \<down> s'". 2686 thus "\<Gamma>\<turnstile>c'\<down> s'" 2687 by cases auto 2688 qed 2689 } 2690 from Catch.hyps (1) [OF this] 2691 show "\<Gamma>\<turnstile>c\<^sub>1 \<down> Normal s". 2692 next 2693 show "\<forall>s'. \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s'" 2694 proof (intro allI impI) 2695 fix s' 2696 assume exec_c\<^sub>1: "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'" 2697 show "\<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s'" 2698 proof (cases "final (c\<^sub>1,Normal s)") 2699 case True 2700 with exec_c\<^sub>1 2701 have Throw: "c\<^sub>1=Throw" 2702 by (auto simp add: final_def elim: exec_Normal_elim_cases) 2703 have "\<Gamma>\<turnstile>(Catch Throw c\<^sub>2,Normal s) \<rightarrow> (c\<^sub>2,Normal s)" 2704 by (rule step.CatchThrow) 2705 from hyp [simplified Throw, OF this] 2706 have "\<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s". 2707 moreover from exec_c\<^sub>1 Throw 2708 have "s'=s" 2709 by (auto elim: exec_Normal_elim_cases) 2710 ultimately show ?thesis by simp 2711 next 2712 case False 2713 from exec_impl_steps [OF exec_c\<^sub>1] 2714 obtain c\<^sub>f t where 2715 steps_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow>\<^sup>* (Throw, Normal s')" 2716 by (fastforce split: xstate.splits) 2717 from split_computation [OF steps_c\<^sub>1 False] 2718 obtain c'' s'' where 2719 first: "\<Gamma>\<turnstile> (c\<^sub>1, Normal s) \<rightarrow> (c'', s'')" and 2720 rest: "\<Gamma>\<turnstile> (c'', s'') \<rightarrow>\<^sup>* (Throw, Normal s')" 2721 by (auto simp add: final_def) 2722 from step.Catch [OF first] 2723 have "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, Normal s) \<rightarrow> (Catch c'' c\<^sub>2, s'')". 2724 from hyp [OF this] 2725 have "\<Gamma>\<turnstile>Catch c'' c\<^sub>2 \<down> s''". 2726 moreover 2727 from steps_Throw_impl_exec [OF rest] 2728 have "\<Gamma>\<turnstile> \<langle>c'',s''\<rangle> \<Rightarrow> Abrupt s'". 2729 moreover 2730 from rest obtain x where "s''=Normal x" 2731 by (cases s'') 2732 (auto dest: steps_Fault_prop steps_Abrupt_prop steps_Stuck_prop) 2733 ultimately show ?thesis 2734 by (fastforce elim: terminates_elim_cases) 2735 qed 2736 qed 2737 qed 2738qed 2739 2740lemma wf_implies_termi_reach: 2741assumes wf: "wf {(cfg2,cfg1). \<Gamma> \<turnstile> (c,s) \<rightarrow>\<^sup>* cfg1 \<and> \<Gamma> \<turnstile> cfg1 \<rightarrow> cfg2}" 2742shows "\<And>c1 s1. \<lbrakk>\<Gamma> \<turnstile> (c,s) \<rightarrow>\<^sup>* cfg1; cfg1=(c1,s1)\<rbrakk>\<Longrightarrow> \<Gamma>\<turnstile>c1\<down>s1" 2743using wf 2744proof (induct cfg1, simp) 2745 fix c1 s1 2746 assume reach: "\<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>* (c1, s1)" 2747 assume hyp_raw: "\<And>y c2 s2. 2748 \<lbrakk>\<Gamma>\<turnstile> (c1, s1) \<rightarrow> (c2, s2); \<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>* (c2, s2); y = (c2, s2)\<rbrakk> 2749 \<Longrightarrow> \<Gamma>\<turnstile>c2 \<down> s2" 2750 have hyp: "\<And>c2 s2. \<Gamma>\<turnstile> (c1, s1) \<rightarrow> (c2, s2) \<Longrightarrow> \<Gamma>\<turnstile>c2 \<down> s2" 2751 apply - 2752 apply (rule hyp_raw) 2753 apply assumption 2754 using reach 2755 apply simp 2756 apply (rule refl) 2757 done 2758 2759 show "\<Gamma>\<turnstile>c1 \<down> s1" 2760 proof (cases s1) 2761 case (Normal s1') 2762 with wf_implies_termi_reach_step_case [OF hyp [simplified Normal]] 2763 show ?thesis 2764 by auto 2765 qed (auto intro: terminates.intros) 2766qed 2767 2768theorem no_infinite_computation_impl_terminates: 2769 assumes not_inf: "\<not> \<Gamma>\<turnstile> (c, s) \<rightarrow> \<dots>(\<infinity>)" 2770 shows "\<Gamma>\<turnstile>c\<down>s" 2771proof - 2772 from no_infinite_computation_implies_wf [OF not_inf] 2773 have wf: "wf {(c2, c1). \<Gamma>\<turnstile>(c, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile>c1 \<rightarrow> c2}". 2774 show ?thesis 2775 by (rule wf_implies_termi_reach [OF wf]) auto 2776qed 2777 2778corollary terminates_iff_no_infinite_computation: 2779 "\<Gamma>\<turnstile>c\<down>s = (\<not> \<Gamma>\<turnstile> (c, s) \<rightarrow> \<dots>(\<infinity>))" 2780 apply (rule) 2781 apply (erule terminates_impl_no_infinite_computation) 2782 apply (erule no_infinite_computation_impl_terminates) 2783 done 2784 2785(* ************************************************************************* *) 2786subsection \<open>Generalised Redexes\<close> 2787(* ************************************************************************* *) 2788 2789text \<open> 2790For an important lemma for the completeness proof of the Hoare-logic for 2791total correctness we need a generalisation of @{const "redex"} that not only 2792yield the redex itself but all the enclosing statements as well. 2793\<close> 2794 2795primrec redexes:: "('s,'p,'f)com \<Rightarrow> ('s,'p,'f)com set" 2796where 2797"redexes Skip = {Skip}" | 2798"redexes (Basic f) = {Basic f}" | 2799"redexes (Spec r) = {Spec r}" | 2800"redexes (Seq c\<^sub>1 c\<^sub>2) = {Seq c\<^sub>1 c\<^sub>2} \<union> redexes c\<^sub>1" | 2801"redexes (Cond b c\<^sub>1 c\<^sub>2) = {Cond b c\<^sub>1 c\<^sub>2}" | 2802"redexes (While b c) = {While b c}" | 2803"redexes (Call p) = {Call p}" | 2804"redexes (DynCom d) = {DynCom d}" | 2805"redexes (Guard f b c) = {Guard f b c}" | 2806"redexes (Throw) = {Throw}" | 2807"redexes (Catch c\<^sub>1 c\<^sub>2) = {Catch c\<^sub>1 c\<^sub>2} \<union> redexes c\<^sub>1" 2808 2809lemma root_in_redexes: "c \<in> redexes c" 2810 apply (induct c) 2811 apply auto 2812 done 2813 2814lemma redex_in_redexes: "redex c \<in> redexes c" 2815 apply (induct c) 2816 apply auto 2817 done 2818 2819lemma redex_redexes: "\<And>c'. \<lbrakk>c' \<in> redexes c; redex c' = c'\<rbrakk> \<Longrightarrow> redex c = c'" 2820 apply (induct c) 2821 apply auto 2822 done 2823 2824lemma step_redexes: 2825 shows "\<And>r r'. \<lbrakk>\<Gamma>\<turnstile>(r,s) \<rightarrow> (r',s'); r \<in> redexes c\<rbrakk> 2826 \<Longrightarrow> \<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow> (c',s') \<and> r' \<in> redexes c'" 2827proof (induct c) 2828 case Skip thus ?case by (fastforce intro: step.intros elim: step_elim_cases) 2829next 2830 case Basic thus ?case by (fastforce intro: step.intros elim: step_elim_cases) 2831next 2832 case Spec thus ?case by (fastforce intro: step.intros elim: step_elim_cases) 2833next 2834 case (Seq c\<^sub>1 c\<^sub>2) 2835 have "r \<in> redexes (Seq c\<^sub>1 c\<^sub>2)" by fact 2836 hence r: "r = Seq c\<^sub>1 c\<^sub>2 \<or> r \<in> redexes c\<^sub>1" 2837 by simp 2838 have step_r: "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r', s')" by fact 2839 from r show ?case 2840 proof 2841 assume "r = Seq c\<^sub>1 c\<^sub>2" 2842 with step_r 2843 show ?case 2844 by (auto simp add: root_in_redexes) 2845 next 2846 assume r: "r \<in> redexes c\<^sub>1" 2847 from Seq.hyps (1) [OF step_r this] 2848 obtain c' where 2849 step_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c', s')" and 2850 r': "r' \<in> redexes c'" 2851 by blast 2852 from step.Seq [OF step_c\<^sub>1] 2853 have "\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow> (Seq c' c\<^sub>2, s')". 2854 with r' 2855 show ?case 2856 by auto 2857 qed 2858next 2859 case Cond 2860 thus ?case 2861 by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) 2862next 2863 case While 2864 thus ?case 2865 by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) 2866next 2867 case Call thus ?case 2868 by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) 2869next 2870 case DynCom thus ?case 2871 by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) 2872next 2873 case Guard thus ?case 2874 by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) 2875next 2876 case Throw thus ?case 2877 by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) 2878next 2879 case (Catch c\<^sub>1 c\<^sub>2) 2880 have "r \<in> redexes (Catch c\<^sub>1 c\<^sub>2)" by fact 2881 hence r: "r = Catch c\<^sub>1 c\<^sub>2 \<or> r \<in> redexes c\<^sub>1" 2882 by simp 2883 have step_r: "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r', s')" by fact 2884 from r show ?case 2885 proof 2886 assume "r = Catch c\<^sub>1 c\<^sub>2" 2887 with step_r 2888 show ?case 2889 by (auto simp add: root_in_redexes) 2890 next 2891 assume r: "r \<in> redexes c\<^sub>1" 2892 from Catch.hyps (1) [OF step_r this] 2893 obtain c' where 2894 step_c\<^sub>1: "\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c', s')" and 2895 r': "r' \<in> redexes c'" 2896 by blast 2897 from step.Catch [OF step_c\<^sub>1] 2898 have "\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow> (Catch c' c\<^sub>2, s')". 2899 with r' 2900 show ?case 2901 by auto 2902 qed 2903qed 2904 2905lemma steps_redexes: 2906 assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>* (r', s')" 2907 shows "\<And>c. r \<in> redexes c \<Longrightarrow> \<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (c',s') \<and> r' \<in> redexes c'" 2908using steps 2909proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 2910 case Refl 2911 then 2912 show "\<exists>c'. \<Gamma>\<turnstile> (c, s') \<rightarrow>\<^sup>* (c', s') \<and> r' \<in> redexes c'" 2913 by auto 2914next 2915 case (Trans r s r'' s'') 2916 have "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r'', s'')" "r \<in> redexes c" by fact+ 2917 from step_redexes [OF this] 2918 obtain c' where 2919 step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s'')" and 2920 r'': "r'' \<in> redexes c'" 2921 by blast 2922 note step 2923 also 2924 from Trans.hyps (3) [OF r''] 2925 obtain c'' where 2926 steps: "\<Gamma>\<turnstile> (c', s'') \<rightarrow>\<^sup>* (c'', s')" and 2927 r': "r' \<in> redexes c''" 2928 by blast 2929 note steps 2930 finally 2931 show ?case 2932 using r' 2933 by blast 2934qed 2935 2936 2937 2938lemma steps_redexes': 2939 assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>+ (r', s')" 2940 shows "\<And>c. r \<in> redexes c \<Longrightarrow> \<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>+ (c',s') \<and> r' \<in> redexes c'" 2941using steps 2942proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans]) 2943 case (Step r' s' c') 2944 have "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r', s')" "r \<in> redexes c'" by fact+ 2945 from step_redexes [OF this] 2946 show ?case 2947 by (blast intro: r_into_trancl) 2948next 2949 case (Trans r' s' r'' s'') 2950 from Trans obtain c' where 2951 steps: "\<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>+ (c', s')" and 2952 r': "r' \<in> redexes c'" 2953 by blast 2954 note steps 2955 moreover 2956 have "\<Gamma>\<turnstile> (r', s') \<rightarrow> (r'', s'')" by fact 2957 from step_redexes [OF this r'] obtain c'' where 2958 step: "\<Gamma>\<turnstile> (c', s') \<rightarrow> (c'', s'')" and 2959 r'': "r'' \<in> redexes c''" 2960 by blast 2961 note step 2962 finally show ?case 2963 using r'' by blast 2964qed 2965 2966lemma step_redexes_Seq: 2967 assumes step: "\<Gamma>\<turnstile>(r,s) \<rightarrow> (r',s')" 2968 assumes Seq: "Seq r c\<^sub>2 \<in> redexes c" 2969 shows "\<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow> (c',s') \<and> Seq r' c\<^sub>2 \<in> redexes c'" 2970proof - 2971 from step.Seq [OF step] 2972 have "\<Gamma>\<turnstile> (Seq r c\<^sub>2, s) \<rightarrow> (Seq r' c\<^sub>2, s')". 2973 from step_redexes [OF this Seq] 2974 show ?thesis . 2975qed 2976 2977lemma steps_redexes_Seq: 2978 assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>* (r', s')" 2979 shows "\<And>c. Seq r c\<^sub>2 \<in> redexes c \<Longrightarrow> 2980 \<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (c',s') \<and> Seq r' c\<^sub>2 \<in> redexes c'" 2981using steps 2982proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 2983 case Refl 2984 then show ?case 2985 by (auto) 2986 2987next 2988 case (Trans r s r'' s'') 2989 have "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r'', s'')" "Seq r c\<^sub>2 \<in> redexes c" by fact+ 2990 from step_redexes_Seq [OF this] 2991 obtain c' where 2992 step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s'')" and 2993 r'': "Seq r'' c\<^sub>2 \<in> redexes c'" 2994 by blast 2995 note step 2996 also 2997 from Trans.hyps (3) [OF r''] 2998 obtain c'' where 2999 steps: "\<Gamma>\<turnstile> (c', s'') \<rightarrow>\<^sup>* (c'', s')" and 3000 r': "Seq r' c\<^sub>2 \<in> redexes c''" 3001 by blast 3002 note steps 3003 finally 3004 show ?case 3005 using r' 3006 by blast 3007qed 3008 3009lemma steps_redexes_Seq': 3010 assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>+ (r', s')" 3011 shows "\<And>c. Seq r c\<^sub>2 \<in> redexes c 3012 \<Longrightarrow> \<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>+ (c',s') \<and> Seq r' c\<^sub>2 \<in> redexes c'" 3013using steps 3014proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans]) 3015 case (Step r' s' c') 3016 have "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r', s')" "Seq r c\<^sub>2 \<in> redexes c'" by fact+ 3017 from step_redexes_Seq [OF this] 3018 show ?case 3019 by (blast intro: r_into_trancl) 3020next 3021 case (Trans r' s' r'' s'') 3022 from Trans obtain c' where 3023 steps: "\<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>+ (c', s')" and 3024 r': "Seq r' c\<^sub>2 \<in> redexes c'" 3025 by blast 3026 note steps 3027 moreover 3028 have "\<Gamma>\<turnstile> (r', s') \<rightarrow> (r'', s'')" by fact 3029 from step_redexes_Seq [OF this r'] obtain c'' where 3030 step: "\<Gamma>\<turnstile> (c', s') \<rightarrow> (c'', s'')" and 3031 r'': "Seq r'' c\<^sub>2 \<in> redexes c''" 3032 by blast 3033 note step 3034 finally show ?case 3035 using r'' by blast 3036qed 3037 3038lemma step_redexes_Catch: 3039 assumes step: "\<Gamma>\<turnstile>(r,s) \<rightarrow> (r',s')" 3040 assumes Catch: "Catch r c\<^sub>2 \<in> redexes c" 3041 shows "\<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow> (c',s') \<and> Catch r' c\<^sub>2 \<in> redexes c'" 3042proof - 3043 from step.Catch [OF step] 3044 have "\<Gamma>\<turnstile> (Catch r c\<^sub>2, s) \<rightarrow> (Catch r' c\<^sub>2, s')". 3045 from step_redexes [OF this Catch] 3046 show ?thesis . 3047qed 3048 3049lemma steps_redexes_Catch: 3050 assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>* (r', s')" 3051 shows "\<And>c. Catch r c\<^sub>2 \<in> redexes c \<Longrightarrow> 3052 \<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>* (c',s') \<and> Catch r' c\<^sub>2 \<in> redexes c'" 3053using steps 3054proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) 3055 case Refl 3056 then show ?case 3057 by (auto) 3058 3059next 3060 case (Trans r s r'' s'') 3061 have "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r'', s'')" "Catch r c\<^sub>2 \<in> redexes c" by fact+ 3062 from step_redexes_Catch [OF this] 3063 obtain c' where 3064 step: "\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s'')" and 3065 r'': "Catch r'' c\<^sub>2 \<in> redexes c'" 3066 by blast 3067 note step 3068 also 3069 from Trans.hyps (3) [OF r''] 3070 obtain c'' where 3071 steps: "\<Gamma>\<turnstile> (c', s'') \<rightarrow>\<^sup>* (c'', s')" and 3072 r': "Catch r' c\<^sub>2 \<in> redexes c''" 3073 by blast 3074 note steps 3075 finally 3076 show ?case 3077 using r' 3078 by blast 3079qed 3080 3081lemma steps_redexes_Catch': 3082 assumes steps: "\<Gamma>\<turnstile> (r, s) \<rightarrow>\<^sup>+ (r', s')" 3083 shows "\<And>c. Catch r c\<^sub>2 \<in> redexes c 3084 \<Longrightarrow> \<exists>c'. \<Gamma>\<turnstile>(c,s) \<rightarrow>\<^sup>+ (c',s') \<and> Catch r' c\<^sub>2 \<in> redexes c'" 3085using steps 3086proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans]) 3087 case (Step r' s' c') 3088 have "\<Gamma>\<turnstile> (r, s) \<rightarrow> (r', s')" "Catch r c\<^sub>2 \<in> redexes c'" by fact+ 3089 from step_redexes_Catch [OF this] 3090 show ?case 3091 by (blast intro: r_into_trancl) 3092next 3093 case (Trans r' s' r'' s'') 3094 from Trans obtain c' where 3095 steps: "\<Gamma>\<turnstile> (c, s) \<rightarrow>\<^sup>+ (c', s')" and 3096 r': "Catch r' c\<^sub>2 \<in> redexes c'" 3097 by blast 3098 note steps 3099 moreover 3100 have "\<Gamma>\<turnstile> (r', s') \<rightarrow> (r'', s'')" by fact 3101 from step_redexes_Catch [OF this r'] obtain c'' where 3102 step: "\<Gamma>\<turnstile> (c', s') \<rightarrow> (c'', s'')" and 3103 r'': "Catch r'' c\<^sub>2 \<in> redexes c''" 3104 by blast 3105 note step 3106 finally show ?case 3107 using r'' by blast 3108qed 3109 3110lemma redexes_subset:"\<And>c'. c' \<in> redexes c \<Longrightarrow> redexes c' \<subseteq> redexes c" 3111 by (induct c) auto 3112 3113lemma redexes_preserves_termination: 3114 assumes termi: "\<Gamma>\<turnstile>c\<down>s" 3115 shows "\<And>c'. c' \<in> redexes c \<Longrightarrow> \<Gamma>\<turnstile>c'\<down>s" 3116using termi 3117by induct (auto intro: terminates.intros) 3118 3119 3120end 3121