| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Simpl/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 114 kB |
|
Quelle SmallStep.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(* Author: Norbert Schirmer Maintainer: Norbert Schirmer, norbert.schirmer at web de Copyright (C) 2006-2008 Norbert Schirmer *) section ‹Small-Step Semantics and Infinite Computations› theory SmallStep imports Termination begin text ‹The redex of a statement is the substatement, which is actually altered the next step in the small-step semantics. › primrec redex:: "('s,'p,'f)com → ('s,'p,'f)com" where "redex Skip = Skip" | "redex (Basic f) = (Basic f)" | "redex (Spec r) = (Spec r)" | "redex (Seq c1 c2) = redex c1" | "redex (Cond b c1 c2) = (Cond b c1 c2)" | "redex (While b c) = (While b c)" | "redex (Call p) = (Call p)" | "redex (DynCom d) = (DynCom d)" | "redex (Guard f b c) = (Guard f b c)" | "redex (Throw) = Throw" | "redex (Catch c1 c2) = redex c1" subsection ‹Small-Step Computation: ‹Γ⊨(c, s) → (c', s')›› type_synonym ('s,'p,'f) config = "('s,'p,'f)com × ('s,'f) xstate" inductive "step"::"[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] → bool" (‹_⊨ (_ →/ _)› [81,81,81] 100) for Γ::"('s,'p,'f) body" where Basic: "Γ⊨(Basic f,Normal s) → (Skip,Normal (f s))" | Spec: "(s,t) ∈ r ==> Γ⊨(Spec r,Normal s) → (Skip,Normal t)" | SpecStuck: "∀t. (s,t) ∉ r ==> Γ⊨(Spec r,Normal s) → (Skip,Stuck)" | Guard: "s∈g ==> Γ⊨(Guard f g c,Normal s) → (c,Normal s)" | GuardFault: "s∉g ==> Γ⊨(Guard f g c,Normal s) → (Skip,Fault f)" | Seq: "Γ⊨(c1,s) → (c1',s') ==> Γ⊨(Seq c1 c2,s) → (Seq c1' c2, s')" | SeqSkip: "Γ⊨(Seq Skip c2,s) → (c2, s)" | SeqThrow: "Γ⊨(Seq Throw c2,Normal s) → (Throw, Normal s)" | CondTrue: "s∈b ==> Γ⊨(Cond b c1 c2,Normal s) → (c1,Normal s)" | CondFalse: "s∉b ==> Γ⊨(Cond b c1 c2,Normal s) → (c2,Normal s)" | WhileTrue: "[s∈b] ==> Γ⊨(While b c,Normal s) → (Seq c (While b c),Normal s)" | WhileFalse: "[s∉b] ==> Γ⊨(While b c,Normal s) → (Skip,Normal s)" | Call: "Γ p=Some bdy ==> Γ⊨(Call p,Normal s) → (bdy,Normal s)" | CallUndefined: "Γ p=None ==> Γ⊨(Call p,Normal s) → (Skip,Stuck)" | DynCom: "Γ⊨(DynCom c,Normal s) → (c s,Normal s)" | Catch: "[Γ⊨(c1,s) → (c1',s')] ==> Γ⊨(Catch c1 c2,s) → (Catch c1' c2,s')" | CatchThrow: "Γ⊨(Catch Throw c2,Normal s) → (c2,Normal s)" | CatchSkip: "Γ⊨(Catch Skip c2,s) → (Skip,s)" | FaultProp: "[c≠Skip; redex c = c] ==> Γ⊨(c,Fault f) → (Skip,Fault f)" | StuckProp: "[c≠Skip; redex c = c] ==> Γ⊨(c,Stuck) → (Skip,Stuck)" | AbruptProp: "[c≠Skip; redex c = c] ==> Γ⊨(c,Abrupt f) → (Skip,Abrupt f)" lemmas step_induct = step.induct [of _ "(c,s)" "(c',s')", split_format (complete), case_na Basic Spec SpecStuck Guard GuardFault Seq SeqSkip SeqThrow CondTrue CondFalse WhileTrue WhileFalse Call CallUndefined DynCom Catch CatchThrow CatchSkip FaultProp StuckProp AbruptProp, induct set] inductive_cases step_elim_cases [cases set]: "Γ⊨(Skip,s) → u" "Γ⊨(Guard f g c,s) → u" "Γ⊨(Basic f,s) → u" "Γ⊨(Spec r,s) → u" "Γ⊨(Seq c1 c2,s) → u" "Γ⊨(Cond b c1 c2,s) → u" "Γ⊨(While b c,s) → u" "Γ⊨(Call p,s) → u" "Γ⊨(DynCom c,s) → u" "Γ⊨(Throw,s) → u" "Γ⊨(Catch c1 c2,s) → u" inductive_cases step_Normal_elim_cases [cases set]: "Γ⊨(Skip,Normal s) → u" "Γ⊨(Guard f g c,Normal s) → u" "Γ⊨(Basic f,Normal s) → u" "Γ⊨(Spec r,Normal s) → u" "Γ⊨(Seq c1 c2,Normal s) → u" "Γ⊨(Cond b c1 c2,Normal s) → u" "Γ⊨(While b c,Normal s) → u" "Γ⊨(Call p,Normal s) → u" "Γ⊨(DynCom c,Normal s) → u" "Γ⊨(Throw,Normal s) → u" "Γ⊨(Catch c1 c2,Normal s) → u" text ‹The final configuration is either of the form ‹(Skip,_)› for normal , or @{term "(Throw,Normal s)"} in case the program was started in @{term "Normal"} state and terminated abruptly. The @{const "Abrupt"} state is abrupt termination, in contrast to the big-step semantics. Only if the starts in an @{const "Abrupt"} states it ends in the same @{term "Abrupt"} . definition final:: "('s,'p,'f) config → bool" where "final cfg = (fst cfg=Skip ∨ (fst cfg=Throw ∧ (∃s. snd cfg=Normal s)))" abbreviation "step_rtrancl" :: "[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] → bool" (‹_⊨ (_ →*/ _)› [81,81,81] 100) where "Γ⊨cf0 →* cf1 ≡ (CONST step Γ)** cf0 cf1" abbreviation "step_trancl" :: "[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] → bool" (‹_⊨ (_ →+/ _)› [81,81,81] 100) where "Γ⊨cf0 →+ cf1 ≡ (CONST step Γ)++ cf0 cf1" (* ************************************************************************ *) subsection ‹Structural Properties of Small Step Computations› (* ************************************************************************ *) lemma redex_not_Seq: "redex c = Seq c1 c2 ==> P" apply (induct c) apply auto done lemma no_step_final: assumes step: "Γ⊨(c,s) → (c',s')" shows "final (c,s) ==> P" using step by induct (auto simp add: final_def) lemma no_step_final': assumes step: "Γ⊨cfg → cfg'" shows "final cfg ==> P" using step by (cases cfg, cases cfg') (auto intro: no_step_final) lemma step_Abrupt: assumes step: "Γ⊨ (c, s) → (c', s')" shows "∧x. s=Abrupt x ==> s'=Abrupt x" using step by (induct) auto lemma step_Fault: assumes step: "Γ⊨ (c, s) → (c', s')" shows "∧f. s=Fault f ==> s'=Fault f" using step by (induct) auto lemma step_Stuck: assumes step: "Γ⊨ (c, s) → (c', s')" shows "∧f. s=Stuck ==> s'=Stuck" using step by (induct) auto lemma SeqSteps: assumes steps: "Γ⊨cfg1→* cfg2" shows "∧ c1 s c1' s'. [cfg1 = (c1,s);cfg2=(c1',s')] ==> Γ⊨(Seq c1 c2,s) →* (Seq c1' c2, s')" using steps proof (induct rule: converse_rtranclp_induct [case_names Refl Trans]) case Refl thus ?case by simp next case (Trans cfg1 cfg'') have step: "Γ⊨ cfg1 → cfg''" by fact have steps: "Γ⊨ cfg'' →* cfg2" by fact have cfg1: "cfg1 = (c1, s)" and cfg2: "cfg2 = (c1', s')" by fact+ obtain c1'' s'' where cfg'': "cfg''=(c1'',s'')" by (cases cfg'') auto from step cfg1 cfg'' have "Γ⊨ (c1,s) → (c1'',s'')" by simp hence "Γ⊨ (Seq c1 c2,s) → (Seq c1'' c2,s'')" by (rule step.Seq) also from Trans.hyps (3) [OF cfg'' cfg2] have "Γ⊨ (Seq c1'' c2, s'') →* (Seq c1' c2, s')" . finally show ?case . qed lemma CatchSteps: assumes steps: "Γ⊨cfg1→* cfg2" shows "∧ c1 s c1' s'. [cfg1 = (c1,s); cfg2=(c1',s')] ==> Γ⊨(Catch c1 c2,s) →* (Catch c1' c2, s')" using steps proof (induct rule: converse_rtranclp_induct [case_names Refl Trans]) case Refl thus ?case by simp next case (Trans cfg1 cfg'') have step: "Γ⊨ cfg1 → cfg''" by fact have steps: "Γ⊨ cfg'' →* cfg2" by fact have cfg1: "cfg1 = (c1, s)" and cfg2: "cfg2 = (c1', s')" by fact+ obtain c1'' s'' where cfg'': "cfg''=(c1'',s'')" by (cases cfg'') auto from step cfg1 cfg'' have s: "Γ⊨ (c1,s) → (c1'',s'')" by simp hence "Γ⊨ (Catch c1 c2,s) → (Catch c1'' c2,s'')" by (rule step.Catch) also from Trans.hyps (3) [OF cfg'' cfg2] have "Γ⊨ (Catch c1'' c2, s'') →* (Catch c1' c2, s')" . finally show ?case . qed lemma steps_Fault: "Γ⊨ (c, Fault f) →* (Skip, Fault f)" proof (induct c) case (Seq c1 c2) have steps_c1: "Γ⊨ (c1, Fault f) →* (Skip, Fault f)" by fact have steps_c2: "Γ⊨ (c2, Fault f) →* (Skip, Fault f)" by fact from SeqSteps [OF steps_c1 refl refl] have "Γ⊨ (Seq c1 c2, Fault f) →* (Seq Skip c2, Fault f)". also have "Γ⊨ (Seq Skip c2, Fault f) → (c2, Fault f)" by (rule SeqSkip) also note steps_c2 finally show ?case by simp next case (Catch c1 c2) have steps_c1: "Γ⊨ (c1, Fault f) →* (Skip, Fault f)" by fact from CatchSteps [OF steps_c1 refl refl] have "Γ⊨ (Catch c1 c2, Fault f) →* (Catch Skip c2, Fault f)". also have "Γ⊨ (Catch Skip c2, Fault f) → (Skip, Fault f)" by (rule CatchSkip) finally show ?case by simp qed (fastforce intro: step.intros)+ lemma steps_Stuck: "Γ⊨ (c, Stuck) →* (Skip, Stuck)" proof (induct c) case (Seq c1 c2) have steps_c1: "Γ⊨ (c1, Stuck) →* (Skip, Stuck)" by fact have steps_c2: "Γ⊨ (c2, Stuck) →* (Skip, Stuck)" by fact from SeqSteps [OF steps_c1 refl refl] have "Γ⊨ (Seq c1 c2, Stuck) →* (Seq Skip c2, Stuck)". also have "Γ⊨ (Seq Skip c2, Stuck) → (c2, Stuck)" by (rule SeqSkip) also note steps_c2 finally show ?case by simp next case (Catch c1 c2) have steps_c1: "Γ⊨ (c1, Stuck) →* (Skip, Stuck)" by fact from CatchSteps [OF steps_c1 refl refl] have "Γ⊨ (Catch c1 c2, Stuck) →* (Catch Skip c2, Stuck)" . also have "Γ⊨ (Catch Skip c2, Stuck) → (Skip, Stuck)" by (rule CatchSkip) finally show ?case by simp qed (fastforce intro: step.intros)+ lemma steps_Abrupt: "Γ⊨ (c, Abrupt s) →* (Skip, Abrupt s)" proof (induct c) case (Seq c1 c2) have steps_c1: "Γ⊨ (c1, Abrupt s) →* (Skip, Abrupt s)" by fact have steps_c2: "Γ⊨ (c2, Abrupt s) →* (Skip, Abrupt s)" by fact from SeqSteps [OF steps_c1 refl refl] have "Γ⊨ (Seq c1 c2, Abrupt s) →* (Seq Skip c2, Abrupt s)". also have "Γ⊨ (Seq Skip c2, Abrupt s) → (c2, Abrupt s)" by (rule SeqSkip) also note steps_c2 finally show ?case by simp next case (Catch c1 c2) have steps_c1: "Γ⊨ (c1, Abrupt s) →* (Skip, Abrupt s)" by fact from CatchSteps [OF steps_c1 refl refl] have "Γ⊨ (Catch c1 c2, Abrupt s) →* (Catch Skip c2, Abrupt s)". also have "Γ⊨ (Catch Skip c2, Abrupt s) → (Skip, Abrupt s)" by (rule CatchSkip) finally show ?case by simp qed (fastforce intro: step.intros)+ lemma step_Fault_prop: assumes step: "Γ⊨ (c, s) → (c', s')" shows "∧f. s=Fault f ==> s'=Fault f" using step by (induct) auto lemma step_Abrupt_prop: assumes step: "Γ⊨ (c, s) → (c', s')" shows "∧x. s=Abrupt x ==> s'=Abrupt x" using step by (induct) auto lemma step_Stuck_prop: assumes step: "Γ⊨ (c, s) → (c', s')" shows "s=Stuck ==> s'=Stuck" using step by (induct) auto lemma steps_Fault_prop: assumes step: "Γ⊨ (c, s) →* (c', s')" shows "s=Fault f ==> s'=Fault f" using step proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl thus ?case by simp next case (Trans c s c'' s'') thus ?case by (auto intro: step_Fault_prop) qed lemma steps_Abrupt_prop: assumes step: "Γ⊨ (c, s) →* (c', s')" shows "s=Abrupt t ==> s'=Abrupt t" using step proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl thus ?case by simp next case (Trans c s c'' s'') thus ?case by (auto intro: step_Abrupt_prop) qed lemma steps_Stuck_prop: assumes step: "Γ⊨ (c, s) →* (c', s')" shows "s=Stuck ==> s'=Stuck" using step proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl thus ?case by simp next case (Trans c s c'' s'') thus ?case by (auto intro: step_Stuck_prop) qed (* ************************************************************************ *) subsection ‹Equivalence between Small-Step and Big-Step Semantics› (* ************************************************************************ *) theorem exec_impl_steps: assumes exec: "Γ⊨⟨c,s⟩ → t" shows "∃c' t'. Γ⊨(c,s) →* (c',t') ∧ (case t of Abrupt x → if s=t then c'=Skip ∧ t'=t else c'=Throw ∧ t'=Normal x | _ → c'=Skip ∧ t'=t)" using exec proof (induct) case Skip thus ?case by simp next case Guard thus ?case by (blast intro: step.Guard rtranclp_trans) next case GuardFault thus ?case by (fastforce intro: step.GuardFault rtranclp_trans) next case FaultProp show ?case by (fastforce intro: steps_Fault) next case Basic thus ?case by (fastforce intro: step.Basic rtranclp_trans) next case Spec thus ?case by (fastforce intro: step.Spec rtranclp_trans) next case SpecStuck thus ?case by (fastforce intro: step.SpecStuck rtranclp_trans) next case (Seq c1 s s' c2 t) have exec_c1: "Γ⊨ ⟨c1,Normal s⟩ → s'" by fact have exec_c2: "Γ⊨ ⟨c2,s'⟩ → t" by fact show ?case proof (cases "∃x. s'=Abrupt x") case False from False Seq.hyps (2) have "Γ⊨ (c1, Normal s) →* (Skip, s')" by (cases s') auto hence seq_c1: "Γ⊨ (Seq c1 c2, Normal s) →* (Seq Skip c2, s')" by (rule SeqSteps) auto from Seq.hyps (4) obtain c' t' where steps_c2: "Γ⊨ (c2, s') →* (c', t')" and t: "(case t of Abrupt x → if s' = t then c' = Skip ∧ t' = t else c' = Throw ∧ t' = Normal x | _ → c' = Skip ∧ t' = t)" by auto note seq_c1 also have "Γ⊨ (Seq Skip c2, s') → (c2, s')" by (rule step.SeqSkip) also note steps_c2 finally have "Γ⊨ (Seq c1 c2, Normal s) →* (c', t')". with t False show ?thesis by (cases t) auto next case True then obtain x where s': "s'=Abrupt x" by blast from s' Seq.hyps (2) have "Γ⊨ (c1, Normal s) →* (Throw, Normal x)" by auto hence seq_c1: "Γ⊨ (Seq c1 c2, Normal s) →* (Seq Throw c2, Normal x)" by (rule SeqSteps) auto also have "Γ⊨ (Seq Throw c2, Normal x) → (Throw, Normal x)" by (rule SeqThrow) finally have "Γ⊨ (Seq c1 c2, Normal s) →* (Throw, Normal x)". moreover from exec_c2 s' have "t=Abrupt x" by (auto intro: Abrupt_end) ultimately show ?thesis by auto qed next case CondTrue thus ?case by (blast intro: step.CondTrue rtranclp_trans) next case CondFalse thus ?case by (blast intro: step.CondFalse rtranclp_trans) next case (WhileTrue s b c s' t) have exec_c: "Γ⊨ ⟨c,Normal s⟩ → s'" by fact have exec_w: "Γ⊨ ⟨While b c,s'⟩ → t" by fact have b: "s ∈ b" by fact hence step: "Γ⊨ (While b c,Normal s) → (Seq c (While b c),Normal s)" by (rule step.WhileTrue) show ?case proof (cases "∃x. s'=Abrupt x") case False from False WhileTrue.hyps (3) have "Γ⊨ (c, Normal s) →* (Skip, s')" by (cases s') auto hence seq_c: "Γ⊨ (Seq c (While b c), Normal s) →* (Seq Skip (While b c), s')" by (rule SeqSteps) auto from WhileTrue.hyps (5) obtain c' t' where steps_c2: "Γ⊨ (While b c, s') →* (c', t')" and t: "(case t of Abrupt x → if s' = t then c' = Skip ∧ t' = t else c' = Throw ∧ t' = Normal x | _ → c' = Skip ∧ t' = t)" by auto note step also note seq_c also have "Γ⊨ (Seq Skip (While b c), s') → (While b c, s')" by (rule step.SeqSkip) also note steps_c2 finally have "Γ⊨ (While b c, Normal s) →* (c', t')". with t False show ?thesis by (cases t) auto next case True then obtain x where s': "s'=Abrupt x" by blast note step also from s' WhileTrue.hyps (3) have "Γ⊨ (c, Normal s) →* (Throw, Normal x)" by auto hence seq_c: "Γ⊨ (Seq c (While b c), Normal s) →* (Seq Throw (While b c), Normal x)" by (rule SeqSteps) auto also have "Γ⊨ (Seq Throw (While b c), Normal x) → (Throw, Normal x)" by (rule SeqThrow) finally have "Γ⊨ (While b c, Normal s) →* (Throw, Normal x)". moreover from exec_w s' have "t=Abrupt x" by (auto intro: Abrupt_end) ultimately show ?thesis by auto qed next case WhileFalse thus ?case by (fastforce intro: step.WhileFalse rtrancl_trans) next case Call thus ?case by (blast intro: step.Call rtranclp_trans) next case CallUndefined thus ?case by (fastforce intro: step.CallUndefined rtranclp_trans) next case StuckProp thus ?case by (fastforce intro: steps_Stuck) next case DynCom thus ?case by (blast intro: step.DynCom rtranclp_trans) next case Throw thus ?case by simp next case AbruptProp thus ?case by (fastforce intro: steps_Abrupt) next case (CatchMatch c1 s s' c2 t) from CatchMatch.hyps (2) have "Γ⊨ (c1, Normal s) →* (Throw, Normal s')" by simp hence "Γ⊨ (Catch c1 c2, Normal s) →* (Catch Throw c2, Normal s')" by (rule CatchSteps) auto also have "Γ⊨ (Catch Throw c2, Normal s') → (c2, Normal s')" by (rule step.CatchThrow) also from CatchMatch.hyps (4) obtain c' t' where steps_c2: "Γ⊨ (c2, Normal s') →* (c', t')" and t: "(case t of Abrupt x → if Normal s' = t then c' = Skip ∧ t' = t else c' = Throw ∧ t' = Normal x | _ → c' = Skip ∧ t' = t)" by auto note steps_c2 finally show ?case using t by (auto split: xstate.splits) next case (CatchMiss c1 s t c2) have t: "¬ isAbr t" by fact with CatchMiss.hyps (2) have "Γ⊨ (c1, Normal s) →* (Skip, t)" by (cases t) auto hence "Γ⊨ (Catch c1 c2, Normal s) →* (Catch Skip c2, t)" by (rule CatchSteps) auto also have "Γ⊨ (Catch Skip c2, t) → (Skip, t)" by (rule step.CatchSkip) finally show ?case using t by (fastforce split: xstate.splits) qed corollary exec_impl_steps_Normal: assumes exec: "Γ⊨⟨c,s⟩ → Normal t" shows "Γ⊨(c,s) →* (Skip, Normal t)" using exec_impl_steps [OF exec] by auto corollary exec_impl_steps_Normal_Abrupt: assumes exec: "Γ⊨⟨c,Normal s⟩ → Abrupt t" shows "Γ⊨(c,Normal s) →* (Throw, Normal t)" using exec_impl_steps [OF exec] by auto corollary exec_impl_steps_Abrupt_Abrupt: assumes exec: "Γ⊨⟨c,Abrupt t⟩ → Abrupt t" shows "Γ⊨(c,Abrupt t) →* (Skip, Abrupt t)" using exec_impl_steps [OF exec] by auto corollary exec_impl_steps_Fault: assumes exec: "Γ⊨⟨c,s⟩ → Fault f" shows "Γ⊨(c,s) →* (Skip, Fault f)" using exec_impl_steps [OF exec] by auto corollary exec_impl_steps_Stuck: assumes exec: "Γ⊨⟨c,s⟩ → Stuck" shows "Γ⊨(c,s) →* (Skip, Stuck)" using exec_impl_steps [OF exec] by auto lemma step_Abrupt_end: assumes step: "Γ⊨ (c1, s) → (c1', s')" shows "s'=Abrupt x ==> s=Abrupt x" using step by induct auto lemma step_Stuck_end: assumes step: "Γ⊨ (c1, s) → (c1', s')" shows "s'=Stuck ==> s=Stuck ∨ (∃r x. redex c1 = Spec r ∧ s=Normal x ∧ (∀t. (x,t)∉r)) ∨ (∃p x. redex c1=Call p ∧ s=Normal x ∧ Γ p = None)" using step by induct auto lemma step_Fault_end: assumes step: "Γ⊨ (c1, s) → (c1', s')" shows "s'=Fault f ==> s=Fault f ∨ (∃g c x. redex c1 = Guard f g c ∧ s=Normal x ∧ x ∉ g)" using step by induct auto lemma exec_redex_Stuck: "Γ⊨⟨redex c,s⟩ → Stuck ==> Γ⊨⟨c,s⟩ → Stuck" proof (induct c) case Seq thus ?case by (cases s) (auto intro: exec.intros elim:exec_elim_cases) next case Catch thus ?case by (cases s) (auto intro: exec.intros elim:exec_elim_cases) qed simp_all lemma exec_redex_Fault: "Γ⊨⟨redex c,s⟩ → Fault f ==> Γ⊨⟨c,s⟩ → Fault f" proof (induct c) case Seq thus ?case by (cases s) (auto intro: exec.intros elim:exec_elim_cases) next case Catch thus ?case by (cases s) (auto intro: exec.intros elim:exec_elim_cases) qed simp_all lemma step_extend: assumes step: "Γ⊨(c,s) → (c', s')" shows "∧t. Γ⊨⟨c',s'⟩ → t ==> Γ⊨⟨c,s⟩ → t" using step proof (induct) case Basic thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case Spec thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case SpecStuck thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case Guard thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case GuardFault thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case (Seq c1 s c1' s' c2) have step: "Γ⊨ (c1, s) → (c1', s')" by fact have exec': "Γ⊨ ⟨Seq c1' c2,s'⟩ → t" by fact show ?case proof (cases s) case (Normal x) note s_Normal = this show ?thesis proof (cases s') case (Normal x') from exec' [simplified Normal] obtain s'' where exec_c1': "Γ⊨ ⟨c1',Normal x'⟩ → s''" and exec_c2: "Γ⊨ ⟨c2,s''⟩ → t" by cases from Seq.hyps (2) Normal exec_c1' s_Normal have "Γ⊨ ⟨c1,Normal x⟩ → s''" by simp from exec.Seq [OF this exec_c2] s_Normal show ?thesis by simp next case (Abrupt x') with exec' have "t=Abrupt x'" by (auto intro:Abrupt_end) moreover from step Abrupt have "s=Abrupt x'" by (auto intro: step_Abrupt_end) ultimately show ?thesis by (auto intro: exec.intros) next case (Fault f) from step_Fault_end [OF step this] s_Normal obtain g c where redex_c1: "redex c1 = Guard f g c" and fail: "x ∉ g" by auto hence "Γ⊨ ⟨redex c1,Normal x⟩ → Fault f" by (auto intro: exec.intros) from exec_redex_Fault [OF this] have "Γ⊨ ⟨c1,Normal x⟩ → Fault f". moreover from Fault exec' have "t=Fault f" by (auto intro: Fault_end) ultimately show ?thesis using s_Normal by (auto intro: exec.intros) next case Stuck from step_Stuck_end [OF step this] s_Normal have "(∃r. redex c1 = Spec r ∧ (∀t. (x, t) ∉ r)) ∨ (∃p. redex c1 = Call p ∧ Γ p = None)" by auto moreover { fix r assume "redex c1 = Spec r" and "(∀t. (x, t) ∉ r)" hence "Γ⊨ ⟨redex c1,Normal x⟩ → Stuck" by (auto intro: exec.intros) from exec_redex_Stuck [OF this] have "Γ⊨ ⟨c1,Normal x⟩ → Stuck". moreover from Stuck exec' have "t=Stuck" by (auto intro: Stuck_end) ultimately have ?thesis using s_Normal by (auto intro: exec.intros) } moreover { fix p assume "redex c1 = Call p" and "Γ p = None" hence "Γ⊨ ⟨redex c1,Normal x⟩ → Stuck" by (auto intro: exec.intros) from exec_redex_Stuck [OF this] have "Γ⊨ ⟨c1,Normal x⟩ → Stuck". moreover from Stuck exec' have "t=Stuck" by (auto intro: Stuck_end) ultimately have ?thesis using s_Normal by (auto intro: exec.intros) } ultimately show ?thesis by auto qed next case (Abrupt x) from step_Abrupt [OF step this] have "s'=Abrupt x". with exec' have "t=Abrupt x" by (auto intro: Abrupt_end) with Abrupt show ?thesis by (auto intro: exec.intros) next case (Fault f) from step_Fault [OF step this] have "s'=Fault f". with exec' have "t=Fault f" by (auto intro: Fault_end) with Fault show ?thesis by (auto intro: exec.intros) next case Stuck from step_Stuck [OF step this] have "s'=Stuck". with exec' have "t=Stuck" by (auto intro: Stuck_end) with Stuck show ?thesis by (auto intro: exec.intros) qed next case (SeqSkip c2 s t) thus ?case by (cases s) (fastforce intro: exec.intros elim: exec_elim_cases)+ next case (SeqThrow c2 s t) thus ?case by (fastforce intro: exec.intros elim: exec_elim_cases)+ next case CondTrue thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case CondFalse thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case WhileTrue thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case WhileFalse thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case Call thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case CallUndefined thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case DynCom thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case (Catch c1 s c1' s' c2 t) have step: "Γ⊨ (c1, s) → (c1', s')" by fact have exec': "Γ⊨ ⟨Catch c1' c2,s'⟩ → t" by fact show ?case proof (cases s) case (Normal x) note s_Normal = this show ?thesis proof (cases s') case (Normal x') from exec' [simplified Normal] show ?thesis proof (cases) fix s'' assume exec_c1': "Γ⊨ ⟨c1',Normal x'⟩ → Abrupt s''" assume exec_c2: "Γ⊨ ⟨c2,Normal s''⟩ → t" from Catch.hyps (2) Normal exec_c1' s_Normal have "Γ⊨ ⟨c1,Normal x⟩ → Abrupt s''" by simp from exec.CatchMatch [OF this exec_c2] s_Normal show ?thesis by simp next assume exec_c1': "Γ⊨ ⟨c1',Normal x'⟩ → t" assume t: "¬ isAbr t" from Catch.hyps (2) Normal exec_c1' s_Normal have "Γ⊨ ⟨c1,Normal x⟩ → t" by simp from exec.CatchMiss [OF this t] s_Normal show ?thesis by simp qed next case (Abrupt x') with exec' have "t=Abrupt x'" by (auto intro:Abrupt_end) moreover from step Abrupt have "s=Abrupt x'" by (auto intro: step_Abrupt_end) ultimately show ?thesis by (auto intro: exec.intros) next case (Fault f) from step_Fault_end [OF step this] s_Normal obtain g c where redex_c1: "redex c1 = Guard f g c" and fail: "x ∉ g" by auto hence "Γ⊨ ⟨redex c1,Normal x⟩ → Fault f" by (auto intro: exec.intros) from exec_redex_Fault [OF this] have "Γ⊨ ⟨c1,Normal x⟩ → Fault f". moreover from Fault exec' have "t=Fault f" by (auto intro: Fault_end) ultimately show ?thesis using s_Normal by (auto intro: exec.intros) next case Stuck from step_Stuck_end [OF step this] s_Normal have "(∃r. redex c1 = Spec r ∧ (∀t. (x, t) ∉ r)) ∨ (∃p. redex c1 = Call p ∧ Γ p = None)" by auto moreover { fix r assume "redex c1 = Spec r" and "(∀t. (x, t) ∉ r)" hence "Γ⊨ ⟨redex c1,Normal x⟩ → Stuck" by (auto intro: exec.intros) from exec_redex_Stuck [OF this] have "Γ⊨ ⟨c1,Normal x⟩ → Stuck". moreover from Stuck exec' have "t=Stuck" by (auto intro: Stuck_end) ultimately have ?thesis using s_Normal by (auto intro: exec.intros) } moreover { fix p assume "redex c1 = Call p" and "Γ p = None" hence "Γ⊨ ⟨redex c1,Normal x⟩ → Stuck" by (auto intro: exec.intros) from exec_redex_Stuck [OF this] have "Γ⊨ ⟨c1,Normal x⟩ → Stuck". moreover from Stuck exec' have "t=Stuck" by (auto intro: Stuck_end) ultimately have ?thesis using s_Normal by (auto intro: exec.intros) } ultimately show ?thesis by auto qed next case (Abrupt x) from step_Abrupt [OF step this] have "s'=Abrupt x". with exec' have "t=Abrupt x" by (auto intro: Abrupt_end) with Abrupt show ?thesis by (auto intro: exec.intros) next case (Fault f) from step_Fault [OF step this] have "s'=Fault f". with exec' have "t=Fault f" by (auto intro: Fault_end) with Fault show ?thesis by (auto intro: exec.intros) next case Stuck from step_Stuck [OF step this] have "s'=Stuck". with exec' have "t=Stuck" by (auto intro: Stuck_end) with Stuck show ?thesis by (auto intro: exec.intros) qed next case CatchThrow thus ?case by (fastforce intro: exec.intros elim: exec_Normal_elim_cases) next case CatchSkip thus ?case by (fastforce intro: exec.intros elim: exec_elim_cases) next case FaultProp thus ?case by (fastforce intro: exec.intros elim: exec_elim_cases) next case StuckProp thus ?case by (fastforce intro: exec.intros elim: exec_elim_cases) next case AbruptProp thus ?case by (fastforce intro: exec.intros elim: exec_elim_cases) qed theorem steps_Skip_impl_exec: assumes steps: "Γ⊨(c,s) →* (Skip,t)" shows "Γ⊨⟨c,s⟩ → t" using steps proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl thus ?case by (cases t) (auto intro: exec.intros) next case (Trans c s c' s') have "Γ⊨ (c, s) → (c', s')" and "Γ⊨ ⟨c',s'⟩ → t" by fact+ thus ?case by (rule step_extend) qed theorem steps_Throw_impl_exec: assumes steps: "Γ⊨(c,s) →* (Throw,Normal t)" shows "Γ⊨⟨c,s⟩ → Abrupt t" using steps proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl thus ?case by (auto intro: exec.intros) next case (Trans c s c' s') have "Γ⊨ (c, s) → (c', s')" and "Γ⊨ ⟨c',s'⟩ → Abrupt t" by fact+ thus ?case by (rule step_extend) qed (* ************************************************************************ *) subsection ‹Infinite Computations: ‹Γ⊨(c, s) → …(∞)›› (* ************************************************************************ *) definition inf:: "('s,'p,'f) body → ('s,'p,'f) config → bool" (‹_⊨ _ → …'(∞')› [60,80] 100) where "Γ⊨ cfg → …(∞) ≡ (∃f. f (0::nat) = cfg ∧ (∀i. Γ⊨f i → f (i+1)))" lemma not_infI: "[∧f. [f 0 = cfg; ∧i. Γ⊨f i → f (Suc i)] ==> False] ==> ¬Γ⊨ cfg → …(∞)" by (auto simp add: inf_def) (* ************************************************************************ *) subsection ‹Equivalence between Termination and the Absence of Infinite Computati (* ************************************************************************ *) lemma step_preserves_termination: assumes step: "Γ⊨(c,s) → (c',s')" shows "Γ⊨c↓s ==> Γ⊨c'↓s'" using step proof (induct) case Basic thus ?case by (fastforce intro: terminates.intros) next case Spec thus ?case by (fastforce intro: terminates.intros) next case SpecStuck thus ?case by (fastforce intro: terminates.intros) next case Guard thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases) next case GuardFault thus ?case by (fastforce intro: terminates.intros) next case (Seq c1 s c1' s' c2) thus ?case apply (cases s) apply (cases s') apply (fastforce intro: terminates.intros step_extend elim: terminates_Normal_elim_cases) apply (fastforce intro: terminates.intros dest: step_Abrupt_prop step_Fault_prop step_Stuck_prop)+ done next case (SeqSkip c2 s) thus ?case apply (cases s) apply (fastforce intro: terminates.intros exec.intros elim: terminates_Normal_elim_cases )+ done next case (SeqThrow c2 s) thus ?case by (fastforce intro: terminates.intros exec.intros elim: terminates_Normal_elim_cases ) next case CondTrue thus ?case by (fastforce intro: terminates.intros exec.intros elim: terminates_Normal_elim_cases ) next case CondFalse thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases ) next case WhileTrue thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases ) next case WhileFalse thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases ) next case Call thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases ) next case CallUndefined thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases ) next case DynCom thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases ) next case (Catch c1 s c1' s' c2) thus ?case apply (cases s) apply (cases s') apply (fastforce intro: terminates.intros step_extend elim: terminates_Normal_elim_cases) apply (fastforce intro: terminates.intros dest: step_Abrupt_prop step_Fault_prop step_Stuck_prop)+ done next case CatchThrow thus ?case by (fastforce intro: terminates.intros exec.intros elim: terminates_Normal_elim_cases ) next case (CatchSkip c2 s) thus ?case by (cases s) (fastforce intro: terminates.intros)+ next case FaultProp thus ?case by (fastforce intro: terminates.intros) next case StuckProp thus ?case by (fastforce intro: terminates.intros) next case AbruptProp thus ?case by (fastforce intro: terminates.intros) qed lemma steps_preserves_termination: assumes steps: "Γ⊨(c,s) →* (c',s')" shows "Γ⊨c↓s ==> Γ⊨c'↓s'" using steps proof (induct rule: rtranclp_induct2 [consumes 1, case_names Refl Trans]) case Refl thus ?case . next case Trans thus ?case by (blast dest: step_preserves_termination) qed ML ‹ ML_Thms.bind_thm ("tranclp_induct2", Split_Rule.split_rule @{context} (Rule_Insts.read_instantiate @{context} [((("a", 0), Position.none), "(aa,ab)"), ((("b", 0), Position.none), "(ba,bb)")] @{thm tranclp_induct})); lemma steps_preserves_termination': assumes steps: "Γ⊨(c,s) →+ (c',s')" shows "Γ⊨c↓s ==> Γ⊨c'↓s'" using steps proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans]) case Step thus ?case by (blast intro: step_preserves_termination) next case Trans thus ?case by (blast dest: step_preserves_termination) qed definition head_com:: "('s,'p,'f) com → ('s,'p,'f) com" where "head_com c = (case c of Seq c1 c2 → c1 | Catch c1 c2 → c1 | _ → c)" definition head:: "('s,'p,'f) config → ('s,'p,'f) config" where "head cfg = (head_com (fst cfg), snd cfg)" lemma le_Suc_cases: "[∧i. [i < k] ==> P i; P k] ==> ∀i<(Suc k). P i" apply clarify apply (case_tac "i=k") apply auto done lemma redex_Seq_False: "∧c' c''. (redex c = Seq c'' c') = False" by (induct c) auto lemma redex_Catch_False: "∧c' c''. (redex c = Catch c'' c') = False" by (induct c) auto lemma infinite_computation_extract_head_Seq: assumes inf_comp: "∀i::nat. Γ⊨f i → f (i+1)" assumes f_0: "f 0 = (Seq c1 c2,s)" assumes not_fin: "∀i<k. ¬ final (head (f i))" shows "∀i<k. (∃c' s'. f (i + 1) = (Seq c' c2, s')) ∧ Γ⊨head (f i) → head (f (i+1))" (is "∀i<k. ?P i") using not_fin proof (induct k) case 0 show ?case by simp next case (Suc k) have not_fin_Suc: "∀i<Suc k. ¬ final (head (f i))" by fact from this[rule_format] have not_fin_k: "∀i<k. ¬ final (head (f i))" apply clarify apply (subgoal_tac "i < Suc k") apply blast apply simp done from Suc.hyps [OF this] have hyp: "∀i<k. (∃c' s'. f (i + 1) = (Seq c' c2, s')) ∧ Γ⊨ head (f i) → head (f (i + 1))". show ?case proof (rule le_Suc_cases) fix i assume "i < k" then show "?P i" by (rule hyp [rule_format]) next show "?P k" proof - from hyp [rule_format, of "k - 1"] f_0 obtain c' fs' L' s' where f_k: "f k = (Seq c' c2, s')" by (cases k) auto from inf_comp [rule_format, of k] f_k have "Γ⊨(Seq c' c2, s') → f (k + 1)" by simp moreover from not_fin_Suc [rule_format, of k] f_k have "¬ final (c',s')" by (simp add: final_def head_def head_com_def) ultimately obtain c'' s'' where "Γ⊨(c', s') → (c'', s'')" and "f (k + 1) = (Seq c'' c2, s'')" by cases (auto simp add: redex_Seq_False final_def) with f_k show ?thesis by (simp add: head_def head_com_def) qed qed qed lemma infinite_computation_extract_head_Catch: assumes inf_comp: "∀i::nat. Γ⊨f i → f (i+1)" assumes f_0: "f 0 = (Catch c1 c2,s)" assumes not_fin: "∀i<k. ¬ final (head (f i))" shows "∀i<k. (∃c' s'. f (i + 1) = (Catch c' c2, s')) ∧ Γ⊨head (f i) → head (f (i+1))" (is "∀i<k. ?P i") using not_fin proof (induct k) case 0 show ?case by simp next case (Suc k) have not_fin_Suc: "∀i<Suc k. ¬ final (head (f i))" by fact from this[rule_format] have not_fin_k: "∀i<k. ¬ final (head (f i))" apply clarify apply (subgoal_tac "i < Suc k") apply blast apply simp done from Suc.hyps [OF this] have hyp: "∀i<k. (∃c' s'. f (i + 1) = (Catch c' c2, s')) ∧ Γ⊨ head (f i) → head (f (i + 1))". show ?case proof (rule le_Suc_cases) fix i assume "i < k" then show "?P i" by (rule hyp [rule_format]) next show "?P k" proof - from hyp [rule_format, of "k - 1"] f_0 obtain c' fs' L' s' where f_k: "f k = (Catch c' c2, s')" by (cases k) auto from inf_comp [rule_format, of k] f_k have "Γ⊨(Catch c' c2, s') → f (k + 1)" by simp moreover from not_fin_Suc [rule_format, of k] f_k have "¬ final (c',s')" by (simp add: final_def head_def head_com_def) ultimately obtain c'' s'' where "Γ⊨(c', s') → (c'', s'')" and "f (k + 1) = (Catch c'' c2, s'')" by cases (auto simp add: redex_Catch_False final_def)+ with f_k show ?thesis by (simp add: head_def head_com_def) qed qed qed lemma no_inf_Throw: "¬ Γ⊨(Throw,s) → …(∞)" proof assume "Γ⊨ (Throw, s) → …(∞)" then obtain f where step [rule_format]: "∀i::nat. Γ⊨f i → f (i+1)" and f_0: "f 0 = (Throw, s)" by (auto simp add: inf_def) from step [of 0, simplified f_0] step [of 1] show False by cases (auto elim: step_elim_cases) qed lemma split_inf_Seq: assumes inf_comp: "Γ⊨(Seq c1 c2,s) → …(∞)" shows "Γ⊨(c1,s) → …(∞) ∨ (∃s'. Γ⊨(c1,s) →* (Skip,s') ∧ Γ⊨(c2,s') → …(∞))" proof - from inf_comp obtain f where step: "∀i::nat. Γ⊨f i → f (i+1)" and f_0: "f 0 = (Seq c1 c2, s)" by (auto simp add: inf_def) from f_0 have head_f_0: "head (f 0) = (c1,s)" by (simp add: head_def head_com_def) show ?thesis proof (cases "∃i. final (head (f i))") case True define k where "k = (LEAST i. final (head (f i)))" have less_k: "∀i<k. ¬ final (head (f i))" apply (intro allI impI) apply (unfold k_def) apply (drule not_less_Least) apply auto done from infinite_computation_extract_head_Seq [OF step f_0 this] obtain step_head: "∀i<k. Γ⊨ head (f i) → head (f (i + 1))" and conf: "∀i<k. (∃c' s'. f (i + 1) = (Seq c' c2, s'))" by blast from True have final_f_k: "final (head (f k))" apply - apply (erule exE) apply (drule LeastI) apply (simp add: k_def) done moreover from f_0 conf [rule_format, of "k - 1"] obtain c' s' where f_k: "f k = (Seq c' c2,s')" by (cases k) auto moreover from step_head have steps_head: "Γ⊨head (f 0) →* head (f k)" proof (induct k) case 0 thus ?case by simp next case (Suc m) have step: "∀i<Suc m. Γ⊨ head (f i) → head (f (i + 1))" by fact hence "∀i<m. Γ⊨ head (f i) → head (f (i + 1))" by auto hence "Γ⊨ head (f 0) →* head (f m)" by (rule Suc.hyps) also from step [rule_format, of m] have "Γ⊨ head (f m) → head (f (m + 1))" by simp finally show ?case by simp qed { assume f_k: "f k = (Seq Skip c2, s')" with steps_head have "Γ⊨(c1,s) →* (Skip,s')" using head_f_0 by (simp add: head_def head_com_def) moreover from step [rule_format, of k] f_k obtain "Γ⊨(Seq Skip c2,s') → (c2,s')" and f_Suc_k: "f (k + 1) = (c2,s')" by (fastforce elim: step.cases intro: step.intros) define g where "g i = f (i + (k + 1))" for i from f_Suc_k have g_0: "g 0 = (c2,s')" by (simp add: g_def) from step have "∀i. Γ⊨g i → g (i + 1)" by (simp add: g_def) with g_0 have "Γ⊨(c2,s') → …(∞)" by (auto simp add: inf_def) ultimately have ?thesis by auto } moreover { fix x assume s': "s'=Normal x" and f_k: "f k = (Seq Throw c2, s')" from step [rule_format, of k] f_k s' obtain "Γ⊨(Seq Throw c2,s') → (Throw,s')" and f_Suc_k: "f (k + 1) = (Throw,s')" by (fastforce elim: step_elim_cases intro: step.intros) define g where "g i = f (i + (k + 1))" for i from f_Suc_k have g_0: "g 0 = (Throw,s')" by (simp add: g_def) from step have "∀i. Γ⊨g i → g (i + 1)" by (simp add: g_def) with g_0 have "Γ⊨(Throw,s') → …(∞)" by (auto simp add: inf_def) with no_inf_Throw have ?thesis by auto } ultimately show ?thesis by (auto simp add: final_def head_def head_com_def) next case False then have not_fin: "∀i. ¬ final (head (f i))" by blast have "∀i. Γ⊨head (f i) → head (f (i + 1))" proof fix k from not_fin have "∀i<(Suc k). ¬ final (head (f i))" by simp from infinite_computation_extract_head_Seq [OF step f_0 this ] show "Γ⊨ head (f k) → head (f (k + 1))" by simp qed with head_f_0 have "Γ⊨(c1,s) → …(∞)" by (auto simp add: inf_def) thus ?thesis by simp qed qed lemma split_inf_Catch: assumes inf_comp: "Γ⊨(Catch c1 c2,s) → …(∞)" shows "Γ⊨(c1,s) → …(∞) ∨ (∃s'. Γ⊨(c1,s) →* (Throw,Normal s') ∧ Γ⊨(c2,Normal s') → …(∞))" proof - from inf_comp obtain f where step: "∀i::nat. Γ⊨f i → f (i+1)" and f_0: "f 0 = (Catch c1 c2, s)" by (auto simp add: inf_def) from f_0 have head_f_0: "head (f 0) = (c1,s)" by (simp add: head_def head_com_def) show ?thesis proof (cases "∃i. final (head (f i))") case True define k where "k = (LEAST i. final (head (f i)))" have less_k: "∀i<k. ¬ final (head (f i))" apply (intro allI impI) apply (unfold k_def) apply (drule not_less_Least) apply auto done from infinite_computation_extract_head_Catch [OF step f_0 this] obtain step_head: "∀i<k. Γ⊨ head (f i) → head (f (i + 1))" and conf: "∀i<k. (∃c' s'. f (i + 1) = (Catch c' c2, s'))" by blast from True have final_f_k: "final (head (f k))" apply - apply (erule exE) apply (drule LeastI) apply (simp add: k_def) done moreover from f_0 conf [rule_format, of "k - 1"] obtain c' s' where f_k: "f k = (Catch c' c2,s')" by (cases k) auto moreover from step_head have steps_head: "Γ⊨head (f 0) →* head (f k)" proof (induct k) case 0 thus ?case by simp next case (Suc m) have step: "∀i<Suc m. Γ⊨ head (f i) → head (f (i + 1))" by fact hence "∀i<m. Γ⊨ head (f i) → head (f (i + 1))" by auto hence "Γ⊨ head (f 0) →* head (f m)" by (rule Suc.hyps) also from step [rule_format, of m] have "Γ⊨ head (f m) → head (f (m + 1))" by simp finally show ?case by simp qed { assume f_k: "f k = (Catch Skip c2, s')" with steps_head have "Γ⊨(c1,s) →* (Skip,s')" using head_f_0 by (simp add: head_def head_com_def) moreover from step [rule_format, of k] f_k obtain "Γ⊨(Catch Skip c2,s') → (Skip,s')" and f_Suc_k: "f (k + 1) = (Skip,s')" by (fastforce elim: step.cases intro: step.intros) from step [rule_format, of "k+1", simplified f_Suc_k] have ?thesis by (rule no_step_final') (auto simp add: final_def) } moreover { fix x assume s': "s'=Normal x" and f_k: "f k = (Catch Throw c2, s')" with steps_head have "Γ⊨(c1,s) →* (Throw,s')" using head_f_0 by (simp add: head_def head_com_def) moreover from step [rule_format, of k] f_k s' obtain "Γ⊨(Catch Throw c2,s') → (c2,s')" and f_Suc_k: "f (k + 1) = (c2,s')" by (fastforce elim: step_elim_cases intro: step.intros) define g where "g i = f (i + (k + 1))" for i from f_Suc_k have g_0: "g 0 = (c2,s')" by (simp add: g_def) from step have "∀i. Γ⊨g i → g (i + 1)" by (simp add: g_def) with g_0 have "Γ⊨(c2,s') → …(∞)" by (auto simp add: inf_def) ultimately have ?thesis using s' by auto } ultimately show ?thesis by (auto simp add: final_def head_def head_com_def) next case False then have not_fin: "∀i. ¬ final (head (f i))" by blast have "∀i. Γ⊨head (f i) → head (f (i + 1))" proof fix k from not_fin have "∀i<(Suc k). ¬ final (head (f i))" by simp from infinite_computation_extract_head_Catch [OF step f_0 this ] show "Γ⊨ head (f k) → head (f (k + 1))" by simp qed with head_f_0 have "Γ⊨(c1,s) → …(∞)" by (auto simp add: inf_def) thus ?thesis by simp qed qed lemma Skip_no_step: "Γ⊨(Skip,s) → cfg ==> P" apply (erule no_step_final') apply (simp add: final_def) done lemma not_inf_Stuck: "¬ Γ⊨(c,Stuck) → …(∞)" proof (induct c) case Skip show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Skip, Stuck)" from f_step [of 0] f_0 show False by (auto elim: Skip_no_step) qed next case (Basic g) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Basic g, Stuck)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Spec r) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Spec r, Stuck)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Seq c1 c2) show ?case proof assume "Γ⊨ (Seq c1 c2, Stuck) → …(∞)" from split_inf_Seq [OF this] Seq.hyps show False by (auto dest: steps_Stuck_prop) qed next case (Cond b c1 c2) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Cond b c1 c2, Stuck)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (While b c) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (While b c, Stuck)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Call p) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Call p, Stuck)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (DynCom d) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (DynCom d, Stuck)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Guard m g c) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Guard m g c, Stuck)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case Throw show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Throw, Stuck)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Catch c1 c2) show ?case proof assume "Γ⊨ (Catch c1 c2, Stuck) → …(∞)" from split_inf_Catch [OF this] Catch.hyps show False by (auto dest: steps_Stuck_prop) qed qed lemma not_inf_Fault: "¬ Γ⊨(c,Fault x) → …(∞)" proof (induct c) case Skip show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Skip, Fault x)" from f_step [of 0] f_0 show False by (auto elim: Skip_no_step) qed next case (Basic g) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Basic g, Fault x)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Spec r) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Spec r, Fault x)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Seq c1 c2) show ?case proof assume "Γ⊨ (Seq c1 c2, Fault x) → …(∞)" from split_inf_Seq [OF this] Seq.hyps show False by (auto dest: steps_Fault_prop) qed next case (Cond b c1 c2) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Cond b c1 c2, Fault x)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (While b c) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (While b c, Fault x)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Call p) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Call p, Fault x)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (DynCom d) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (DynCom d, Fault x)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Guard m g c) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Guard m g c, Fault x)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case Throw show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Throw, Fault x)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Catch c1 c2) show ?case proof assume "Γ⊨ (Catch c1 c2, Fault x) → …(∞)" from split_inf_Catch [OF this] Catch.hyps show False by (auto dest: steps_Fault_prop) qed qed lemma not_inf_Abrupt: "¬ Γ⊨(c,Abrupt s) → …(∞)" proof (induct c) case Skip show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Skip, Abrupt s)" from f_step [of 0] f_0 show False by (auto elim: Skip_no_step) qed next case (Basic g) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Basic g, Abrupt s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Spec r) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Spec r, Abrupt s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Seq c1 c2) show ?case proof assume "Γ⊨ (Seq c1 c2, Abrupt s) → …(∞)" from split_inf_Seq [OF this] Seq.hyps show False by (auto dest: steps_Abrupt_prop) qed next case (Cond b c1 c2) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Cond b c1 c2, Abrupt s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (While b c) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (While b c, Abrupt s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Call p) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Call p, Abrupt s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (DynCom d) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (DynCom d, Abrupt s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Guard m g c) show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Guard m g c, Abrupt s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case Throw show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Throw, Abrupt s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Catch c1 c2) show ?case proof assume "Γ⊨ (Catch c1 c2, Abrupt s) → …(∞)" from split_inf_Catch [OF this] Catch.hyps show False by (auto dest: steps_Abrupt_prop) qed qed theorem terminates_impl_no_infinite_computation: assumes termi: "Γ⊨c ↓ s" shows "¬ Γ⊨(c,s) → …(∞)" using termi proof (induct) case (Skip s) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Skip, Normal s)" from f_step [of 0] f_0 show False by (auto elim: Skip_no_step) qed next case (Basic g s) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Basic g, Normal s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Spec r s) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Spec r, Normal s)" from f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Guard s g c m) have g: "s ∈ g" by fact have hyp: "¬ Γ⊨ (c, Normal s) → …(∞)" by fact show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Guard m g c, Normal s)" from f_step [of 0] f_0 g have "f 1 = (c,Normal s)" by (fastforce elim: step_elim_cases) with f_step have "Γ⊨ (c, Normal s) → …(∞)" apply (simp add: inf_def) apply (rule_tac x="λi. f (Suc i)" in exI) by simp with hyp show False .. qed next case (GuardFault s g m c) have g: "s ∉ g" by fact show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Guard m g c, Normal s)" from g f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Fault c m) thus ?case by (rule not_inf_Fault) next case (Seq c1 s c2) show ?case proof assume "Γ⊨ (Seq c1 c2, Normal s) → …(∞)" from split_inf_Seq [OF this] Seq.hyps show False by (auto intro: steps_Skip_impl_exec) qed next case (CondTrue s b c1 c2) have b: "s ∈ b" by fact have hyp_c1: "¬ Γ⊨ (c1, Normal s) → …(∞)" by fact show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Cond b c1 c2, Normal s)" from b f_step [of 0] f_0 have "f 1 = (c1,Normal s)" by (auto elim: step_Normal_elim_cases) with f_step have "Γ⊨ (c1, Normal s) → …(∞)" apply (simp add: inf_def) apply (rule_tac x="λi. f (Suc i)" in exI) by simp with hyp_c1 show False by simp qed next case (CondFalse s b c2 c1) have b: "s ∉ b" by fact have hyp_c2: "¬ Γ⊨ (c2, Normal s) → …(∞)" by fact show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Cond b c1 c2, Normal s)" from b f_step [of 0] f_0 have "f 1 = (c2,Normal s)" by (auto elim: step_Normal_elim_cases) with f_step have "Γ⊨ (c2, Normal s) → …(∞)" apply (simp add: inf_def) apply (rule_tac x="λi. f (Suc i)" in exI) by simp with hyp_c2 show False by simp qed next case (WhileTrue s b c) have b: "s ∈ b" by fact have hyp_c: "¬ Γ⊨ (c, Normal s) → …(∞)" by fact have hyp_w: "∀s'. Γ⊨ ⟨c,Normal s⟩ → s' ⟶ Γ⊨While b c ↓ s' ∧ ¬ Γ⊨ (While b c, s') → …(∞)" by fact have not_inf_Seq: "¬ Γ⊨ (Seq c (While b c), Normal s) → …(∞)" proof assume "Γ⊨ (Seq c (While b c), Normal s) → …(∞)" from split_inf_Seq [OF this] hyp_c hyp_w show False by (auto intro: steps_Skip_impl_exec) qed show ?case proof assume "Γ⊨ (While b c, Normal s) → …(∞)" then obtain f where f_step: "∧i. Γ⊨f i → f (Suc i)" and f_0: "f 0 = (While b c, Normal s)" by (auto simp add: inf_def) from f_step [of 0] f_0 b have "f 1 = (Seq c (While b c),Normal s)" by (auto elim: step_Normal_elim_cases) with f_step have "Γ⊨ (Seq c (While b c), Normal s) → …(∞)" apply (simp add: inf_def) apply (rule_tac x="λi. f (Suc i)" in exI) by simp with not_inf_Seq show False by simp qed next case (WhileFalse s b c) have b: "s ∉ b" by fact show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (While b c, Normal s)" from b f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Call p bdy s) have bdy: "Γ p = Some bdy" by fact have hyp: "¬ Γ⊨ (bdy, Normal s) → …(∞)" by fact show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Call p, Normal s)" from bdy f_step [of 0] f_0 have "f 1 = (bdy,Normal s)" by (auto elim: step_Normal_elim_cases) with f_step have "Γ⊨ (bdy, Normal s) → …(∞)" apply (simp add: inf_def) apply (rule_tac x="λi. f (Suc i)" in exI) by simp with hyp show False by simp qed next case (CallUndefined p s) have no_bdy: "Γ p = None" by fact show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Call p, Normal s)" from no_bdy f_step [of 0] f_0 f_step [of 1] show False by (fastforce elim: Skip_no_step step_elim_cases) qed next case (Stuck c) show ?case by (rule not_inf_Stuck) next case (DynCom c s) have hyp: "¬ Γ⊨ (c s, Normal s) → …(∞)" by fact show ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (DynCom c, Normal s)" from f_step [of 0] f_0 have "f (Suc 0) = (c s, Normal s)" by (auto elim: step_elim_cases) with f_step have "Γ⊨ (c s, Normal s) → …(∞)" apply (simp add: inf_def) apply (rule_tac x="λi. f (Suc i)" in exI) by simp with hyp show False by simp qed next case (Throw s) thus ?case proof (rule not_infI) fix f assume f_step: "∧i. Γ⊨f i → f (Suc i)" assume f_0: "f 0 = (Throw, Normal s)" from f_step [of 0] f_0 show False by (auto elim: step_elim_cases) qed next case (Abrupt c) show ?case by (rule not_inf_Abrupt) next case (Catch c1 s c2) show ?case proof assume "Γ⊨ (Catch c1 c2, Normal s) → …(∞)" from split_inf_Catch [OF this] Catch.hyps show False by (auto intro: steps_Throw_impl_exec) qed qed definition termi_call_steps :: "('s,'p,'f) body → (('s × 'p) × ('s × 'p))set" where "termi_call_steps Γ = {((t,q),(s,p)). Γ⊨Call p↓Normal s ∧ (∃c. Γ⊨(Call p,Normal s) →+ (c,Normal t) ∧ redex c = Call q)}" primrec subst_redex:: "('s,'p,'f)com → ('s,'p,'f)com → ('s,'p,'f)com" where "subst_redex Skip c = c" | "subst_redex (Basic f) c = c" | "subst_redex (Spec r) c = c" | "subst_redex (Seq c1 c2) c = Seq (subst_redex c1 c) c2" | "subst_redex (Cond b c1 c2) c = c" | "subst_redex (While b c') c = c" | "subst_redex (Call p) c = c" | "subst_redex (DynCom d) c = c" | "subst_redex (Guard f b c') c = c" | "subst_redex (Throw) c = c" | "subst_redex (Catch c1 c2) c = Catch (subst_redex c1 c) c2" lemma subst_redex_redex: "subst_redex c (redex c) = c" by (induct c) auto lemma redex_subst_redex: "redex (subst_redex c r) = redex r" by (induct c) auto lemma step_redex': shows "Γ⊨(redex c,s) → (r',s') ==> Γ⊨(c,s) → (subst_redex c r',s')" by (induct c) (auto intro: step.Seq step.Catch) lemma step_redex: shows "Γ⊨(r,s) → (r',s') ==> Γ⊨(subst_redex c r,s) → (subst_redex c r',s')" by (induct c) (auto intro: step.Seq step.Catch) lemma steps_redex: assumes steps: "Γ⊨ (r, s) →* (r', s')" shows "∧c. Γ⊨(subst_redex c r,s) →* (subst_redex c r',s')" using steps proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl show "Γ⊨ (subst_redex c r', s') →* (subst_redex c r', s')" by simp next case (Trans r s r'' s'') have "Γ⊨ (r, s) → (r'', s'')" by fact from step_redex [OF this] have "Γ⊨ (subst_redex c r, s) → (subst_redex c r'', s'')". also have "Γ⊨ (subst_redex c r'', s'') →* (subst_redex c r', s')" by fact finally show ?case . qed ML ‹ ML_Thms.bind_thm ("trancl_induct2", Split_Rule.split_rule @{context} (Rule_Insts.read_instantiate @{context} [((("a", 0), Position.none), "(aa, ab)"), ((("b", 0), Position.none), "(ba, bb)" @{thm trancl_induct})); lemma steps_redex': assumes steps: "Γ⊨ (r, s) →+ (r', s')" shows "∧c. Γ⊨(subst_redex c r,s) →+ (subst_redex c r',s')" using steps proof (induct rule: tranclp_induct2 [consumes 1,case_names Step Trans]) case (Step r' s') have "Γ⊨ (r, s) → (r', s')" by fact then have "Γ⊨ (subst_redex c r, s) → (subst_redex c r', s')" by (rule step_redex) then show "Γ⊨ (subst_redex c r, s) →+ (subst_redex c r', s')".. next case (Trans r' s' r'' s'') have "Γ⊨ (subst_redex c r, s) →+ (subst_redex c r', s')" by fact also have "Γ⊨ (r', s') → (r'', s'')" by fact hence "Γ⊨ (subst_redex c r', s') → (subst_redex c r'', s'')" by (rule step_redex) finally show "Γ⊨ (subst_redex c r, s) →+ (subst_redex c r'', s'')" . qed primrec seq:: "(nat → ('s,'p,'f)com) → 'p → nat → ('s,'p,'f)com" where "seq c p 0 = Call p" | "seq c p (Suc i) = subst_redex (seq c p i) (c i)" lemma renumber': assumes f: "∀i. (a,f i) ∈ r* ∧ (f i,f(Suc i)) ∈ r" assumes a_b: "(a,b) ∈ r*" shows "b = f 0 ==> (∃f. f 0 = a ∧ (∀i. (f i, f(Suc i)) ∈ r))" using a_b proof (induct rule: converse_rtrancl_induct [consumes 1]) assume "b = f 0" with f show "∃f. f 0 = b ∧ (∀i. (f i, f (Suc i)) ∈ r)" by blast next fix a z assume a_z: "(a, z) ∈ r" and "(z, b) ∈ r*" assume "b = f 0 ==> ∃f. f 0 = z ∧ (∀i. (f i, f (Suc i)) ∈ r)" "b = f 0" then obtain f where f0: "f 0 = z" and seq: "∀i. (f i, f (Suc i)) ∈ r" by iprover { fix i have "((λi. case i of 0 → a | Suc i → f i) i, f i) ∈ r" using seq a_z f0 by (cases i) auto } then show "∃f. f 0 = a ∧ (∀i. (f i, f (Suc i)) ∈ r)" by - (rule exI [where x="λi. case i of 0 → a | Suc i → f i"],simp) qed lemma renumber: "∀i. (a,f i) ∈ r* ∧ (f i,f(Suc i)) ∈ r ==> ∃f. f 0 = a ∧ (∀i. (f i, f(Suc i)) ∈ r)" by (blast dest:renumber') lemma lem: "∀y. r++ a y ⟶ P a ⟶ P y ==> ((b,a) ∈ {(y,x). P x ∧ r x y}+) = ((b,a) ∈ {(y,x). P x ∧ r++ x y})" apply(rule iffI) apply clarify apply(erule trancl_induct) apply blast apply(blast intro:tranclp_trans) apply clarify apply(erule tranclp_induct) apply blast apply(blast intro:trancl_trans) done corollary terminates_impl_no_infinite_trans_computation: assumes terminates: "Γ⊨c↓s" shows "¬(∃f. f 0 = (c,s) ∧ (∀i. Γ⊨f i →+ f(Suc i)))" proof - have "wf({(y,x). Γ⊨(c,s) →* x ∧ Γ⊨x → y}+)" proof (rule wf_trancl) show "wf {(y, x). Γ⊨(c,s) →* x ∧ Γ⊨x → y}" proof (simp only: wf_iff_no_infinite_down_chain,clarify,simp) fix f assume "∀i. Γ⊨(c,s) →* f i ∧ Γ⊨f i → f (Suc i)" hence "∃f. f (0::nat) = (c,s) ∧ (∀i. Γ⊨f i → f (Suc i))" by (rule renumber [to_pred]) moreover from terminates_impl_no_infinite_computation [OF terminates] have "¬ (∃f. f (0::nat) = (c, s) ∧ (∀i. Γ⊨f i → f (Suc i)))" by (simp add: inf_def) ultimately show False by simp qed qed hence "¬ (∃f. ∀i. (f (Suc i), f i) ∈ {(y, x). Γ⊨(c, s) →* x ∧ Γ⊨x → y}+)" by (simp add: wf_iff_no_infinite_down_chain) thus ?thesis proof (rule contrapos_nn) assume "∃f. f (0::nat) = (c, s) ∧ (∀i. Γ⊨f i →+ f (Suc i))" then obtain f where f0: "f 0 = (c, s)" and seq: "∀i. Γ⊨f i →+ f (Suc i)" by iprover show "∃f. ∀i. (f (Suc i), f i) ∈ {(y, x). Γ⊨(c, s) →* x ∧ Γ⊨x → y}+" proof (rule exI [where x=f],rule allI) fix i show "(f (Suc i), f i) ∈ {(y, x). Γ⊨(c, s) →* x ∧ Γ⊨x → y}+" proof - { fix i have "Γ⊨(c,s) →* f i" proof (induct i) case 0 show "Γ⊨(c, s) →* f 0" by (simp add: f0) next case (Suc n) have "Γ⊨(c, s) →* f n" by fact with seq show "Γ⊨(c, s) →* f (Suc n)" by (blast intro: tranclp_into_rtranclp rtranclp_trans) qed } hence "Γ⊨(c,s) →* f i" by iprover with seq have "(f (Suc i), f i) ∈ {(y, x). Γ⊨(c, s) →* x ∧ Γ⊨x →+ y}" by clarsimp moreover have "∀y. Γ⊨f i →+ y⟶Γ⊨(c, s) →* f i⟶Γ⊨(c, s) →* y" by (blast intro: tranclp_into_rtranclp rtranclp_trans) ultimately show ?thesis by (subst lem ) qed qed qed qed theorem wf_termi_call_steps: "wf (termi_call_steps Γ)" proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain, clarify,simp) fix f assume inf: "∀i. (λ(t, q) (s, p). Γ⊨Call p ↓ Normal s ∧ (∃c. Γ⊨ (Call p, Normal s) →+ (c, Normal t) ∧ redex c = Call q)) (f (Suc i)) (f i)" define s where "s i = fst (f i)" for i :: nat define p where "p i = (snd (f i)::'b)" for i :: nat from inf have inf': "∀i. Γ⊨Call (p i) ↓ Normal (s i) ∧ (∃c. Γ⊨ (Call (p i), Normal (s i)) →+ (c, Normal (s (i+1))) ∧ redex c = Call (p (i+1)))" apply - apply (rule allI) apply (erule_tac x=i in allE) apply (auto simp add: s_def p_def) done show False proof - from inf' have "∃c. ∀i. Γ⊨Call (p i) ↓ Normal (s i) ∧ Γ⊨ (Call (p i), Normal (s i)) →+ (c i, Normal (s (i+1))) ∧ redex (c i) = Call (p (i+1))" apply - apply (rule choice) by blast then obtain c where termi_c: "∀i. Γ⊨Call (p i) ↓ Normal (s i)" and steps_c: "∀i. Γ⊨ (Call (p i), Normal (s i)) →+ (c i, Normal (s (i+1)))" and red_c: "∀i. redex (c i) = Call (p (i+1))" by auto define g where "g i = (seq c (p 0) i,Normal (s i)::('a,'c) xstate)" for i from red_c [rule_format, of 0] have "g 0 = (Call (p 0), Normal (s 0))" by (simp add: g_def) moreover { fix i have "redex (seq c (p 0) i) = Call (p i)" by (induct i) (auto simp add: redex_subst_redex red_c) from this [symmetric] have "subst_redex (seq c (p 0) i) (Call (p i)) = (seq c (p 0) i)" by (simp add: subst_redex_redex) } note subst_redex_seq = this have "∀i. Γ⊨ (g i) →+ (g (i+1))" proof fix i from steps_c [rule_format, of i] have "Γ⊨ (Call (p i), Normal (s i)) →+ (c i, Normal (s (i + 1)))". from steps_redex' [OF this, of "(seq c (p 0) i)"] have "Γ⊨ (subst_redex (seq c (p 0) i) (Call (p i)), Normal (s i)) →+ (subst_redex (seq c (p 0) i) (c i), Normal (s (i + 1)))" . hence "Γ⊨ (seq c (p 0) i, Normal (s i)) →+ (seq c (p 0) (i+1), Normal (s (i + 1)))" by (simp add: subst_redex_seq) thus "Γ⊨ (g i) →+ (g (i+1))" by (simp add: g_def) qed moreover from terminates_impl_no_infinite_trans_computation [OF termi_c [rule_format, of 0]] have "¬ (∃f. f 0 = (Call (p 0), Normal (s 0)) ∧ (∀i. Γ⊨ f i →+ f (Suc i)))" . ultimately show False by auto qed qed lemma no_infinite_computation_implies_wf: assumes not_inf: "¬ Γ⊨ (c, s) → …(∞)" shows "wf {(c2,c1). Γ ⊨ (c,s) →* c1 ∧ Γ ⊨ c1 → c2}" proof (simp only: wf_iff_no_infinite_down_chain,clarify, simp) fix f assume "∀i. Γ⊨(c, s) →* f i ∧ Γ⊨f i → f (Suc i)" hence "∃f. f 0 = (c, s) ∧ (∀i. Γ⊨f i → f (Suc i))" by (rule renumber [to_pred]) moreover from not_inf have "¬ (∃f. f 0 = (c, s) ∧ (∀i. Γ⊨f i → f (Suc i)))" by (simp add: inf_def) ultimately show False by simp qed lemma not_final_Stuck_step: "¬ final (c,Stuck) ==> ∃c' s'. Γ⊨ (c, Stuck) → (c',s')" by (induct c) (fastforce intro: step.intros simp add: final_def)+ lemma not_final_Abrupt_step: "¬ final (c,Abrupt s) ==> ∃c' s'. Γ⊨ (c, Abrupt s) → (c',s')" by (induct c) (fastforce intro: step.intros simp add: final_def)+ lemma not_final_Fault_step: "¬ final (c,Fault f) ==> ∃c' s'. Γ⊨ (c, Fault f) → (c',s')" by (induct c) (fastforce intro: step.intros simp add: final_def)+ lemma not_final_Normal_step: "¬ final (c,Normal s) ==> ∃c' s'. Γ⊨ (c, Normal s) → (c',s')" proof (induct c) case Skip thus ?case by (fastforce intro: step.intros simp add: final_def) next case Basic thus ?case by (fastforce intro: step.intros) next case (Spec r) thus ?case by (cases "∃t. (s,t) ∈ r") (fastforce intro: step.intros)+ next case (Seq c1 c2) thus ?case by (cases "final (c1,Normal s)") (fastforce intro: step.intros simp add: final_def)+ next case (Cond b c1 c2) show ?case by (cases "s ∈ b") (fastforce intro: step.intros)+ next case (While b c) show ?case by (cases "s ∈ b") (fastforce intro: step.intros)+ next case (Call p) show ?case by (cases "Γ p") (fastforce intro: step.intros)+ next case DynCom thus ?case by (fastforce intro: step.intros) next case (Guard f g c) show ?case by (cases "s ∈ g") (fastforce intro: step.intros)+ next case Throw thus ?case by (fastforce intro: step.intros simp add: final_def) next case (Catch c1 c2) thus ?case by (cases "final (c1,Normal s)") (fastforce intro: step.intros simp add: final_def)+ qed lemma final_termi: "final (c,s) ==> Γ⊨c↓s" by (cases s) (auto simp add: final_def terminates.intros) lemma split_computation: assumes steps: "Γ⊨ (c, s) →* (cf, sf)" assumes not_final: "¬ final (c,s)" assumes final: "final (cf,sf)" shows "∃c' s'. Γ⊨ (c, s) → (c',s') ∧ Γ⊨ (c', s') →* (cf, sf)" using steps not_final final proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl thus ?case by simp next case (Trans c s c' s') thus ?case by auto qed lemma wf_implies_termi_reach_step_case: assumes hyp: "∧c' s'. Γ⊨ (c, Normal s) → (c', s') ==> Γ⊨c' ↓ s'" shows "Γ⊨c ↓ Normal s" using hyp proof (induct c) case Skip show ?case by (fastforce intro: terminates.intros) next case Basic show ?case by (fastforce intro: terminates.intros) next case (Spec r) show ?case by (cases "∃t. (s,t)∈r") (fastforce intro: terminates.intros)+ next case (Seq c1 c2) have hyp: "∧c' s'. Γ⊨ (Seq c1 c2, Normal s) → (c', s') ==> Γ⊨c' ↓ s'" by fact show ?case proof (rule terminates.Seq) { fix c' s' assume step_c1: "Γ⊨ (c1, Normal s) → (c', s')" have "Γ⊨c' ↓ s'" proof - from step_c1 have "Γ⊨ (Seq c1 c2, Normal s) → (Seq c' c2, s')" by (rule step.Seq) from hyp [OF this] have "Γ⊨Seq c' c2 ↓ s'". thus "Γ⊨c'↓ s'" by cases auto qed } from Seq.hyps (1) [OF this] show "Γ⊨c1 ↓ Normal s". next show "∀s'. Γ⊨ ⟨c1,Normal s⟩ → s' ⟶ Γ⊨c2 ↓ s'" proof (intro allI impI) fix s' assume exec_c1: "Γ⊨ ⟨c1,Normal s⟩ → s'" show "Γ⊨c2 ↓ s'" proof (cases "final (c1,Normal s)") case True hence "c1=Skip ∨ c1=Throw" by (simp add: final_def) thus ?thesis proof assume Skip: "c1=Skip" have "Γ⊨(Seq Skip c2,Normal s) → (c2,Normal s)" by (rule step.SeqSkip) from hyp [simplified Skip, OF this] have "Γ⊨c2 ↓ Normal s" . moreover from exec_c1 Skip have "s'=Normal s" by (auto elim: exec_Normal_elim_cases) ultimately show ?thesis by simp next assume Throw: "c1=Throw" with exec_c1 have "s'=Abrupt s" by (auto elim: exec_Normal_elim_cases) thus ?thesis by auto qed next case False from exec_impl_steps [OF exec_c1] obtain cf t where steps_c1: "Γ⊨ (c1, Normal s) →* (cf, t)" and fin:"(case s' of Abrupt x → cf = Throw ∧ t = Normal x | _ → cf = Skip ∧ t = s')" by (fastforce split: xstate.splits) with fin have final: "final (cf,t)" by (cases s') (auto simp add: final_def) from split_computation [OF steps_c1 False this] obtain c'' s'' where first: "Γ⊨ (c1, Normal s) → (c'', s'')" and rest: "Γ⊨ (c'', s'') →* (cf, t)" by blast from step.Seq [OF first] have "Γ⊨ (Seq c1 c2, Normal s) → (Seq c'' c2, s'')". from hyp [OF this] have termi_s'': "Γ⊨Seq c'' c2 ↓ s''". show ?thesis proof (cases s'') case (Normal x) from termi_s'' [simplified Normal] have termi_c2: "∀t. Γ⊨ ⟨c'',Normal x⟩ → t ⟶ Γ⊨c2 ↓ t" by cases show ?thesis proof (cases "∃x'. s'=Abrupt x'") case False with fin obtain "cf=Skip" "t=s'" by (cases s') auto from steps_Skip_impl_exec [OF rest [simplified this]] Normal have "Γ⊨ ⟨c'',Normal x⟩ → s'" by simp from termi_c2 [rule_format, OF this] show "Γ⊨c2 ↓ s'" . next case True with fin obtain x' where s': "s'=Abrupt x'" and "cf=Throw" "t=Normal x'" by auto from steps_Throw_impl_exec [OF rest [simplified this]] Normal have "Γ⊨ ⟨c'',Normal x⟩ → Abrupt x'" by simp from termi_c2 [rule_format, OF this] s' show "Γ⊨c2 ↓ s'" by simp qed next case (Abrupt x) from steps_Abrupt_prop [OF rest this] have "t=Abrupt x" by simp with fin have "s'=Abrupt x" by (cases s') auto thus "Γ⊨c2 ↓ s'" by auto next case (Fault f) from steps_Fault_prop [OF rest this] have "t=Fault f" by simp with fin have "s'=Fault f" by (cases s') auto thus "Γ⊨c2 ↓ s'" by auto next case Stuck from steps_Stuck_prop [OF rest this] have "t=Stuck" by simp with fin have "s'=Stuck" by (cases s') auto thus "Γ⊨c2 ↓ s'" by auto qed qed qed qed next case (Cond b c1 c2) have hyp: "∧c' s'. Γ⊨ (Cond b c1 c2, Normal s) → (c', s') ==> Γ⊨c' ↓ s'" by fact show ?case proof (cases "s∈b") case True then have "Γ⊨ (Cond b c1 c2, Normal s) → (c1, Normal s)" by (rule step.CondTrue) from hyp [OF this] have "Γ⊨c1 ↓ Normal s". with True show ?thesis by (auto intro: terminates.intros) next case False then have "Γ⊨ (Cond b c1 c2, Normal s) → (c2, Normal s)" by (rule step.CondFalse) from hyp [OF this] have "Γ⊨c2 ↓ Normal s". with False show ?thesis by (auto intro: terminates.intros) qed next case (While b c) have hyp: "∧c' s'. Γ⊨ (While b c, Normal s) → (c', s') ==> Γ⊨c' ↓ s'" by fact show ?case proof (cases "s∈b") case True then have "Γ⊨ (While b c, Normal s) → (Seq c (While b c), Normal s)" by (rule step.WhileTrue) from hyp [OF this] have "Γ⊨(Seq c (While b c)) ↓ Normal s". with True show ?thesis by (auto elim: terminates_Normal_elim_cases intro: terminates.intros) next case False thus ?thesis by (auto intro: terminates.intros) qed next case (Call p) have hyp: "∧c' s'. Γ⊨ (Call p, Normal s) → (c', s') ==> Γ⊨c' ↓ s'" by fact show ?case proof (cases "Γ p") case None thus ?thesis by (auto intro: terminates.intros) next case (Some bdy) then have "Γ⊨ (Call p, Normal s) → (bdy, Normal s)" by (rule step.Call) from hyp [OF this] have "Γ⊨bdy ↓ Normal s". with Some show ?thesis by (auto intro: terminates.intros) qed next case (DynCom c) have hyp: "∧c' s'. Γ⊨ (DynCom c, Normal s) → (c', s') ==> Γ⊨c' ↓ s'" by fact have "Γ⊨ (DynCom c, Normal s) → (c s, Normal s)" by (rule step.DynCom) from hyp [OF this] have "Γ⊨c s ↓ Normal s". then show ?case by (auto intro: terminates.intros) next case (Guard f g c) have hyp: "∧c' s'. Γ⊨ (Guard f g c, Normal s) → (c', s') ==> Γ⊨c' ↓ s'" by fact show ?case proof (cases "s∈g") case True then have "Γ⊨ (Guard f g c, Normal s) → (c, Normal s)" by (rule step.Guard) from hyp [OF this] have "Γ⊨c↓ Normal s". with True show ?thesis by (auto intro: terminates.intros) next case False thus ?thesis by (auto intro: terminates.intros) qed next case Throw show ?case by (auto intro: terminates.intros) next case (Catch c1 c2) have hyp: "∧c' s'. Γ⊨ (Catch c1 c2, Normal s) → (c', s') ==> Γ⊨c' ↓ s'" by fact show ?case proof (rule terminates.Catch) { fix c' s' assume step_c1: "Γ⊨ (c1, Normal s) → (c', s')" have "Γ⊨c' ↓ s'" proof - from step_c1 have "Γ⊨ (Catch c1 c2, Normal s) → (Catch c' c2, s')" by (rule step.Catch) from hyp [OF this] have "Γ⊨Catch c' c2 ↓ s'". thus "Γ⊨c'↓ s'" by cases auto qed } from Catch.hyps (1) [OF this] show "Γ⊨c1 ↓ Normal s". next show "∀s'. Γ⊨ ⟨c1,Normal s⟩ → Abrupt s' ⟶ Γ⊨c2 ↓ Normal s'" proof (intro allI impI) fix s' assume exec_c1: "Γ⊨ ⟨c1,Normal s⟩ → Abrupt s'" show "Γ⊨c2 ↓ Normal s'" proof (cases "final (c1,Normal s)") case True with exec_c1 have Throw: "c1=Throw" by (auto simp add: final_def elim: exec_Normal_elim_cases) have "Γ⊨(Catch Throw c2,Normal s) → (c2,Normal s)" by (rule step.CatchThrow) from hyp [simplified Throw, OF this] have "Γ⊨c2 ↓ Normal s". moreover from exec_c1 Throw have "s'=s" by (auto elim: exec_Normal_elim_cases) ultimately show ?thesis by simp next case False from exec_impl_steps [OF exec_c1] obtain cf t where steps_c1: "Γ⊨ (c1, Normal s) →* (Throw, Normal s')" by (fastforce split: xstate.splits) from split_computation [OF steps_c1 False] obtain c'' s'' where first: "Γ⊨ (c1, Normal s) → (c'', s'')" and rest: "Γ⊨ (c'', s'') →* (Throw, Normal s')" by (auto simp add: final_def) from step.Catch [OF first] have "Γ⊨ (Catch c1 c2, Normal s) → (Catch c'' c2, s'')". from hyp [OF this] have "Γ⊨Catch c'' c2 ↓ s''". moreover from steps_Throw_impl_exec [OF rest] have "Γ⊨ ⟨c'',s''⟩ → Abrupt s'". moreover from rest obtain x where "s''=Normal x" by (cases s'') (auto dest: steps_Fault_prop steps_Abrupt_prop steps_Stuck_prop) ultimately show ?thesis by (fastforce elim: terminates_elim_cases) qed qed qed qed lemma wf_implies_termi_reach: assumes wf: "wf {(cfg2,cfg1). Γ ⊨ (c,s) →* cfg1 ∧ Γ ⊨ cfg1 → cfg2}" shows "∧c1 s1. [Γ ⊨ (c,s) →* cfg1; cfg1=(c1,s1)]==> Γ⊨c1↓s1" using wf proof (induct cfg1, simp) fix c1 s1 assume reach: "Γ⊨ (c, s) →* (c1, s1)" assume hyp_raw: "∧y c2 s2. [Γ⊨ (c1, s1) → (c2, s2); Γ⊨ (c, s) →* (c2, s2); y = (c2, s2)] ==> Γ⊨c2 ↓ s2" have hyp: "∧c2 s2. Γ⊨ (c1, s1) → (c2, s2) ==> Γ⊨c2 ↓ s2" apply - apply (rule hyp_raw) apply assumption using reach apply simp apply (rule refl) done show "Γ⊨c1 ↓ s1" proof (cases s1) case (Normal s1') with wf_implies_termi_reach_step_case [OF hyp [simplified Normal]] show ?thesis by auto qed (auto intro: terminates.intros) qed theorem no_infinite_computation_impl_terminates: assumes not_inf: "¬ Γ⊨ (c, s) → …(∞)" shows "Γ⊨c↓s" proof - from no_infinite_computation_implies_wf [OF not_inf] have wf: "wf {(c2, c1). Γ⊨(c, s) →* c1 ∧ Γ⊨c1 → c2}". show ?thesis by (rule wf_implies_termi_reach [OF wf]) auto qed corollary terminates_iff_no_infinite_computation: "Γ⊨c↓s = (¬ Γ⊨ (c, s) → …(∞))" apply (rule) apply (erule terminates_impl_no_infinite_computation) apply (erule no_infinite_computation_impl_terminates) done (* ************************************************************************* *) subsection ‹Generalised Redexes› (* ************************************************************************* *) text ‹ an important lemma for the completeness proof of the Hoare-logic for correctness we need a generalisation of @{const "redex"} that not only the redex itself but all the enclosing statements as well. › primrec redexes:: "('s,'p,'f)com → ('s,'p,'f)com set" where "redexes Skip = {Skip}" | "redexes (Basic f) = {Basic f}" | "redexes (Spec r) = {Spec r}" | "redexes (Seq c1 c2) = {Seq c1 c2} ∪ redexes c1" | "redexes (Cond b c1 c2) = {Cond b c1 c2}" | "redexes (While b c) = {While b c}" | "redexes (Call p) = {Call p}" | "redexes (DynCom d) = {DynCom d}" | "redexes (Guard f b c) = {Guard f b c}" | "redexes (Throw) = {Throw}" | "redexes (Catch c1 c2) = {Catch c1 c2} ∪ redexes c1" lemma root_in_redexes: "c ∈ redexes c" apply (induct c) apply auto done lemma redex_in_redexes: "redex c ∈ redexes c" apply (induct c) apply auto done lemma redex_redexes: "∧c'. [c' ∈ redexes c; redex c' = c'] ==> redex c = c'" apply (induct c) apply auto done lemma step_redexes: shows "∧r r'. [Γ⊨(r,s) → (r',s'); r ∈ redexes c] ==> ∃c'. Γ⊨(c,s) → (c',s') ∧ r' ∈ redexes c'" proof (induct c) case Skip thus ?case by (fastforce intro: step.intros elim: step_elim_cases) next case Basic thus ?case by (fastforce intro: step.intros elim: step_elim_cases) next case Spec thus ?case by (fastforce intro: step.intros elim: step_elim_cases) next case (Seq c1 c2) have "r ∈ redexes (Seq c1 c2)" by fact hence r: "r = Seq c1 c2 ∨ r ∈ redexes c1" by simp have step_r: "Γ⊨ (r, s) → (r', s')" by fact from r show ?case proof assume "r = Seq c1 c2" with step_r show ?case by (auto simp add: root_in_redexes) next assume r: "r ∈ redexes c1" from Seq.hyps (1) [OF step_r this] obtain c' where step_c1: "Γ⊨ (c1, s) → (c', s')" and r': "r' ∈ redexes c'" by blast from step.Seq [OF step_c1] have "Γ⊨ (Seq c1 c2, s) → (Seq c' c2, s')". with r' show ?case by auto qed next case Cond thus ?case by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) next case While thus ?case by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) next case Call thus ?case by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) next case DynCom thus ?case by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) next case Guard thus ?case by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) next case Throw thus ?case by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes) next case (Catch c1 c2) have "r ∈ redexes (Catch c1 c2)" by fact hence r: "r = Catch c1 c2 ∨ r ∈ redexes c1" by simp have step_r: "Γ⊨ (r, s) → (r', s')" by fact from r show ?case proof assume "r = Catch c1 c2" with step_r show ?case by (auto simp add: root_in_redexes) next assume r: "r ∈ redexes c1" from Catch.hyps (1) [OF step_r this] obtain c' where step_c1: "Γ⊨ (c1, s) → (c', s')" and r': "r' ∈ redexes c'" by blast from step.Catch [OF step_c1] have "Γ⊨ (Catch c1 c2, s) → (Catch c' c2, s')". with r' show ?case by auto qed qed lemma steps_redexes: assumes steps: "Γ⊨ (r, s) →* (r', s')" shows "∧c. r ∈ redexes c ==> ∃c'. Γ⊨(c,s) →* (c',s') ∧ r' ∈ redexes c'" using steps proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl then show "∃c'. Γ⊨ (c, s') →* (c', s') ∧ r' ∈ redexes c'" by auto next case (Trans r s r'' s'') have "Γ⊨ (r, s) → (r'', s'')" "r ∈ redexes c" by fact+ from step_redexes [OF this] obtain c' where step: "Γ⊨ (c, s) → (c', s'')" and r'': "r'' ∈ redexes c'" by blast note step also from Trans.hyps (3) [OF r''] obtain c'' where steps: "Γ⊨ (c', s'') →* (c'', s')" and r': "r' ∈ redexes c''" by blast note steps finally show ?case using r' by blast qed lemma steps_redexes': assumes steps: "Γ⊨ (r, s) →+ (r', s')" shows "∧c. r ∈ redexes c ==> ∃c'. Γ⊨(c,s) →+ (c',s') ∧ r' ∈ redexes c'" using steps proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans]) case (Step r' s' c') have "Γ⊨ (r, s) → (r', s')" "r ∈ redexes c'" by fact+ from step_redexes [OF this] show ?case by (blast intro: r_into_trancl) next case (Trans r' s' r'' s'') from Trans obtain c' where steps: "Γ⊨ (c, s) →+ (c', s')" and r': "r' ∈ redexes c'" by blast note steps moreover have "Γ⊨ (r', s') → (r'', s'')" by fact from step_redexes [OF this r'] obtain c'' where step: "Γ⊨ (c', s') → (c'', s'')" and r'': "r'' ∈ redexes c''" by blast note step finally show ?case using r'' by blast qed lemma step_redexes_Seq: assumes step: "Γ⊨(r,s) → (r',s')" assumes Seq: "Seq r c2 ∈ redexes c" shows "∃c'. Γ⊨(c,s) → (c',s') ∧ Seq r' c2 ∈ redexes c'" proof - from step.Seq [OF step] have "Γ⊨ (Seq r c2, s) → (Seq r' c2, s')". from step_redexes [OF this Seq] show ?thesis . qed lemma steps_redexes_Seq: assumes steps: "Γ⊨ (r, s) →* (r', s')" shows "∧c. Seq r c2 ∈ redexes c ==> ∃c'. Γ⊨(c,s) →* (c',s') ∧ Seq r' c2 ∈ redexes c'" using steps proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl then show ?case by (auto) next case (Trans r s r'' s'') have "Γ⊨ (r, s) → (r'', s'')" "Seq r c2 ∈ redexes c" by fact+ from step_redexes_Seq [OF this] obtain c' where step: "Γ⊨ (c, s) → (c', s'')" and r'': "Seq r'' c2 ∈ redexes c'" by blast note step also from Trans.hyps (3) [OF r''] obtain c'' where steps: "Γ⊨ (c', s'') →* (c'', s')" and r': "Seq r' c2 ∈ redexes c''" by blast note steps finally show ?case using r' by blast qed lemma steps_redexes_Seq': assumes steps: "Γ⊨ (r, s) →+ (r', s')" shows "∧c. Seq r c2 ∈ redexes c ==> ∃c'. Γ⊨(c,s) →+ (c',s') ∧ Seq r' c2 ∈ redexes c'" using steps proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans]) case (Step r' s' c') have "Γ⊨ (r, s) → (r', s')" "Seq r c2 ∈ redexes c'" by fact+ from step_redexes_Seq [OF this] show ?case by (blast intro: r_into_trancl) next case (Trans r' s' r'' s'') from Trans obtain c' where steps: "Γ⊨ (c, s) →+ (c', s')" and r': "Seq r' c2 ∈ redexes c'" by blast note steps moreover have "Γ⊨ (r', s') → (r'', s'')" by fact from step_redexes_Seq [OF this r'] obtain c'' where step: "Γ⊨ (c', s') → (c'', s'')" and r'': "Seq r'' c2 ∈ redexes c''" by blast note step finally show ?case using r'' by blast qed lemma step_redexes_Catch: assumes step: "Γ⊨(r,s) → (r',s')" assumes Catch: "Catch r c2 ∈ redexes c" shows "∃c'. Γ⊨(c,s) → (c',s') ∧ Catch r' c2 ∈ redexes c'" proof - from step.Catch [OF step] have "Γ⊨ (Catch r c2, s) → (Catch r' c2, s')". from step_redexes [OF this Catch] show ?thesis . qed lemma steps_redexes_Catch: assumes steps: "Γ⊨ (r, s) →* (r', s')" shows "∧c. Catch r c2 ∈ redexes c ==> ∃c'. Γ⊨(c,s) →* (c',s') ∧ Catch r' c2 ∈ redexes c'" using steps proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans]) case Refl then show ?case by (auto) next case (Trans r s r'' s'') have "Γ⊨ (r, s) → (r'', s'')" "Catch r c2 ∈ redexes c" by fact+ from step_redexes_Catch [OF this] obtain c' where step: "Γ⊨ (c, s) → (c', s'')" and r'': "Catch r'' c2 ∈ redexes c'" by blast note step also from Trans.hyps (3) [OF r''] obtain c'' where steps: "Γ⊨ (c', s'') →* (c'', s')" and r': "Catch r' c2 ∈ redexes c''" by blast note steps finally show ?case using r' by blast qed lemma steps_redexes_Catch': assumes steps: "Γ⊨ (r, s) →+ (r', s')" shows "∧c. Catch r c2 ∈ redexes c ==> ∃c'. Γ⊨(c,s) →+ (c',s') ∧ Catch r' c2 ∈ redexes c'" using steps proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans]) case (Step r' s' c') have "Γ⊨ (r, s) → (r', s')" "Catch r c2 ∈ redexes c'" by fact+ from step_redexes_Catch [OF this] show ?case by (blast intro: r_into_trancl) next case (Trans r' s' r'' s'') from Trans obtain c' where steps: "Γ⊨ (c, s) →+ (c', s')" and r': "Catch r' c2 ∈ redexes c'" by blast note steps moreover have "Γ⊨ (r', s') → (r'', s'')" by fact from step_redexes_Catch [OF this r'] obtain c'' where step: "Γ⊨ (c', s') → (c'', s'')" and r'': "Catch r'' c2 ∈ redexes c''" by blast note step finally show ?case using r'' by blast qed lemma redexes_subset:"∧c'. c' ∈ redexes c ==> redexes c' ⊆ redexes c" by (induct c) auto lemma redexes_preserves_termination: assumes termi: "Γ⊨c↓s" shows "∧c'. c' ∈ redexes c ==> Γ⊨c'↓s" using termi by induct (auto intro: terminates.intros) end
¤ Dauer der Verarbeitung: 0.108 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01