Theory SmallStep

(*
    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
by 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 c⇩1 c⇩2) = redex c⇩1" |
"redex (Cond b c⇩1 c⇩2) = (Cond b c⇩1 c⇩2)" |
"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 c⇩1 c⇩2) = redex c⇩1"


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: "Γ⊢(c⇩1,s) → (c⇩1',s')
        ⟹
        Γ⊢(Seq c⇩1 c⇩2,s) → (Seq c⇩1' c⇩2, s')"
| SeqSkip: "Γ⊢(Seq Skip c⇩2,s) → (c⇩2, s)"
| SeqThrow: "Γ⊢(Seq Throw c⇩2,Normal s) → (Throw, Normal s)"

| CondTrue:  "s∈b ⟹ Γ⊢(Cond b c⇩1 c⇩2,Normal s) → (c⇩1,Normal s)"
| CondFalse: "s∉b ⟹ Γ⊢(Cond b c⇩1 c⇩2,Normal s) → (c⇩2,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: "⟦Γ⊢(c⇩1,s) → (c⇩1',s')⟧
          ⟹
          Γ⊢(Catch c⇩1 c⇩2,s) → (Catch c⇩1' c⇩2,s')"

| CatchThrow: "Γ⊢(Catch Throw c⇩2,Normal s) → (c⇩2,Normal s)"
| CatchSkip: "Γ⊢(Catch Skip c⇩2,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_names
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
termination, or @{term "(Throw,Normal s)"} in case the program was started in
a @{term "Normal"} state and terminated abruptly. The @{const "Abrupt"} state is not used to
model abrupt termination, in contrast to the big-step semantics. Only if the
program starts in an @{const "Abrupt"} states it ends in the same @{term "Abrupt"}
state.›

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: "Γ⊢cfg⇩1→⇧* cfg⇩2"
  shows "⋀ c⇩1 s c⇩1' s'. ⟦cfg⇩1 = (c⇩1,s);cfg⇩2=(c⇩1',s')⟧
          ⟹ Γ⊢(Seq c⇩1 c⇩2,s) →⇧* (Seq c⇩1' c⇩2, s')"
using steps
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
  case Refl
  thus ?case
    by simp
next
  case (Trans cfg⇩1 cfg'')
  have step: "Γ⊢ cfg⇩1 → cfg''" by fact
  have steps: "Γ⊢ cfg'' →⇧* cfg⇩2" by fact
  have cfg⇩1: "cfg⇩1 = (c⇩1, s)" and cfg⇩2: "cfg⇩2 = (c⇩1', s')"  by fact+
  obtain c⇩1'' s'' where cfg'': "cfg''=(c⇩1'',s'')"
    by (cases cfg'') auto
  from step cfg⇩1 cfg''
  have "Γ⊢ (c⇩1,s) → (c⇩1'',s'')"
    by simp
  hence "Γ⊢ (Seq c⇩1 c⇩2,s) → (Seq c⇩1'' c⇩2,s'')"
    by (rule step.Seq)
  also from Trans.hyps (3) [OF cfg'' cfg⇩2]
  have "Γ⊢ (Seq c⇩1'' c⇩2, s'') →⇧* (Seq c⇩1' c⇩2, s')" .
  finally show ?case .
qed


lemma CatchSteps:
  assumes steps: "Γ⊢cfg⇩1→⇧* cfg⇩2"
  shows "⋀ c⇩1 s c⇩1' s'. ⟦cfg⇩1 = (c⇩1,s); cfg⇩2=(c⇩1',s')⟧
          ⟹ Γ⊢(Catch c⇩1 c⇩2,s) →⇧* (Catch c⇩1' c⇩2, s')"
using steps
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
  case Refl
  thus ?case
    by simp
next
  case (Trans cfg⇩1 cfg'')
  have step: "Γ⊢ cfg⇩1 → cfg''" by fact
  have steps: "Γ⊢ cfg'' →⇧* cfg⇩2" by fact
  have cfg⇩1: "cfg⇩1 = (c⇩1, s)" and cfg⇩2: "cfg⇩2 = (c⇩1', s')"  by fact+
  obtain c⇩1'' s'' where cfg'': "cfg''=(c⇩1'',s'')"
    by (cases cfg'') auto
  from step cfg⇩1 cfg''
  have s: "Γ⊢ (c⇩1,s) → (c⇩1'',s'')"
    by simp
  hence "Γ⊢ (Catch c⇩1 c⇩2,s) → (Catch c⇩1'' c⇩2,s'')"
    by (rule step.Catch)
  also from Trans.hyps (3) [OF cfg'' cfg⇩2]
  have "Γ⊢ (Catch c⇩1'' c⇩2, s'') →⇧* (Catch c⇩1' c⇩2, s')" .
  finally show ?case .
qed

lemma steps_Fault: "Γ⊢ (c, Fault f) →⇧* (Skip, Fault f)"
proof (induct c)
  case (Seq c⇩1 c⇩2)
  have steps_c⇩1: "Γ⊢ (c⇩1, Fault f) →⇧* (Skip, Fault f)" by fact
  have steps_c⇩2: "Γ⊢ (c⇩2, Fault f) →⇧* (Skip, Fault f)" by fact
  from SeqSteps [OF steps_c⇩1 refl refl]
  have "Γ⊢ (Seq c⇩1 c⇩2, Fault f) →⇧* (Seq Skip c⇩2, Fault f)".
  also
  have "Γ⊢ (Seq Skip c⇩2, Fault f) → (c⇩2, Fault f)" by (rule SeqSkip)
  also note steps_c⇩2
  finally show ?case by simp
next
  case (Catch c⇩1 c⇩2)
  have steps_c⇩1: "Γ⊢ (c⇩1, Fault f) →⇧* (Skip, Fault f)" by fact
  from CatchSteps [OF steps_c⇩1 refl refl]
  have "Γ⊢ (Catch c⇩1 c⇩2, Fault f) →⇧* (Catch Skip c⇩2, Fault f)".
  also
  have "Γ⊢ (Catch Skip c⇩2, 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 c⇩1 c⇩2)
  have steps_c⇩1: "Γ⊢ (c⇩1, Stuck) →⇧* (Skip, Stuck)" by fact
  have steps_c⇩2: "Γ⊢ (c⇩2, Stuck) →⇧* (Skip, Stuck)" by fact
  from SeqSteps [OF steps_c⇩1 refl refl]
  have "Γ⊢ (Seq c⇩1 c⇩2, Stuck) →⇧* (Seq Skip c⇩2, Stuck)".
  also
  have "Γ⊢ (Seq Skip c⇩2, Stuck) → (c⇩2, Stuck)" by (rule SeqSkip)
  also note steps_c⇩2
  finally show ?case by simp
next
  case (Catch c⇩1 c⇩2)
  have steps_c⇩1: "Γ⊢ (c⇩1, Stuck) →⇧* (Skip, Stuck)" by fact
  from CatchSteps [OF steps_c⇩1 refl refl]
  have "Γ⊢ (Catch c⇩1 c⇩2, Stuck) →⇧* (Catch Skip c⇩2, Stuck)" .
  also
  have "Γ⊢ (Catch Skip c⇩2, 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 c⇩1 c⇩2)
  have steps_c⇩1: "Γ⊢ (c⇩1, Abrupt s) →⇧* (Skip, Abrupt s)" by fact
  have steps_c⇩2: "Γ⊢ (c⇩2, Abrupt s) →⇧* (Skip, Abrupt s)" by fact
  from SeqSteps [OF steps_c⇩1 refl refl]
  have "Γ⊢ (Seq c⇩1 c⇩2, Abrupt s) →⇧* (Seq Skip c⇩2, Abrupt s)".
  also
  have "Γ⊢ (Seq Skip c⇩2, Abrupt s) → (c⇩2, Abrupt s)" by (rule SeqSkip)
  also note steps_c⇩2
  finally show ?case by simp
next
  case (Catch c⇩1 c⇩2)
  have steps_c⇩1: "Γ⊢ (c⇩1, Abrupt s) →⇧* (Skip, Abrupt s)" by fact
  from CatchSteps [OF steps_c⇩1 refl refl]
  have "Γ⊢ (Catch c⇩1 c⇩2, Abrupt s) →⇧* (Catch Skip c⇩2, Abrupt s)".
  also
  have "Γ⊢ (Catch Skip c⇩2, 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 c⇩1 s s' c⇩2 t)
  have exec_c⇩1: "Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ s'" by fact
  have exec_c⇩2: "Γ⊢ ⟨c⇩2,s'⟩ ⇒ t" by fact
  show ?case
  proof (cases "∃x. s'=Abrupt x")
    case False
    from False Seq.hyps (2)
    have "Γ⊢ (c⇩1, Normal s) →⇧* (Skip, s')"
      by (cases s') auto
    hence seq_c⇩1: "Γ⊢ (Seq c⇩1 c⇩2, Normal s) →⇧* (Seq Skip c⇩2, s')"
      by (rule SeqSteps) auto
    from Seq.hyps (4) obtain c' t' where
      steps_c⇩2: "Γ⊢ (c⇩2, 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_c⇩1
    also have "Γ⊢ (Seq Skip c⇩2, s') → (c⇩2, s')" by (rule step.SeqSkip)
    also note steps_c⇩2
    finally have "Γ⊢ (Seq c⇩1 c⇩2, 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 "Γ⊢ (c⇩1, Normal s) →⇧* (Throw, Normal x)"
      by auto
    hence seq_c⇩1: "Γ⊢ (Seq c⇩1 c⇩2, Normal s) →⇧* (Seq Throw c⇩2, Normal x)"
      by (rule SeqSteps) auto
    also have "Γ⊢ (Seq Throw c⇩2, Normal x) → (Throw, Normal x)"
      by (rule SeqThrow)
    finally have "Γ⊢ (Seq c⇩1 c⇩2, Normal s) →⇧* (Throw, Normal x)".
    moreover
    from exec_c⇩2 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_c⇩2: "Γ⊢ (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_c⇩2
    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 c⇩1 s s' c⇩2 t)
  from CatchMatch.hyps (2)
  have "Γ⊢ (c⇩1, Normal s) →⇧* (Throw, Normal s')"
    by simp
  hence "Γ⊢ (Catch c⇩1 c⇩2, Normal s) →⇧* (Catch Throw c⇩2, Normal s')"
    by (rule CatchSteps) auto
  also have "Γ⊢ (Catch Throw c⇩2, Normal s') → (c⇩2, Normal s')"
    by (rule step.CatchThrow)
  also
  from CatchMatch.hyps (4) obtain c' t' where
      steps_c⇩2: "Γ⊢ (c⇩2, 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_c⇩2
  finally show ?case
    using t
    by (auto split: xstate.splits)
next
  case (CatchMiss c⇩1 s t c⇩2)
  have t: "¬ isAbr t" by fact
  with CatchMiss.hyps (2)
  have "Γ⊢ (c⇩1, Normal s) →⇧* (Skip, t)"
    by (cases t) auto
  hence "Γ⊢ (Catch c⇩1 c⇩2, Normal s) →⇧* (Catch Skip c⇩2, t)"
    by (rule CatchSteps) auto
  also
  have "Γ⊢ (Catch Skip c⇩2, 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: "Γ⊢ (c⇩1, s) → (c⇩1', s')"
  shows "s'=Abrupt x ⟹ s=Abrupt x"
using step
by induct auto

lemma step_Stuck_end:
  assumes step: "Γ⊢ (c⇩1, s) → (c⇩1', s')"
  shows "s'=Stuck ⟹
          s=Stuck ∨
          (∃r x. redex c⇩1 = Spec r ∧ s=Normal x ∧ (∀t. (x,t)∉r)) ∨
          (∃p x. redex c⇩1=Call p ∧ s=Normal x ∧ Γ p = None)"
using step
by induct auto

lemma step_Fault_end:
  assumes step: "Γ⊢ (c⇩1, s) → (c⇩1', s')"
  shows "s'=Fault f ⟹
          s=Fault f ∨
          (∃g c x. redex c⇩1 = 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 c⇩1 s c⇩1' s' c⇩2)
  have step: "Γ⊢ (c⇩1, s) → (c⇩1', s')" by fact
  have exec': "Γ⊢ ⟨Seq c⇩1' c⇩2,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_c⇩1': "Γ⊢ ⟨c⇩1',Normal x'⟩ ⇒ s''" and
        exec_c⇩2: "Γ⊢ ⟨c⇩2,s''⟩ ⇒ t"
        by cases
      from Seq.hyps (2) Normal exec_c⇩1' s_Normal
      have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ s''"
        by simp
      from exec.Seq [OF this exec_c⇩2] 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_c⇩1: "redex c⇩1 = Guard f g c" and
        fail: "x ∉ g"
        by auto
      hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Fault f"
        by (auto intro: exec.intros)
      from exec_redex_Fault [OF this]
      have "Γ⊢ ⟨c⇩1,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 c⇩1 = Spec r ∧ (∀t. (x, t) ∉ r)) ∨
            (∃p. redex c⇩1 = Call p ∧ Γ p = None)"
        by auto
      moreover
      {
        fix r
        assume "redex c⇩1 = Spec r" and "(∀t. (x, t) ∉ r)"
        hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Stuck"
          by (auto intro: exec.intros)
        from exec_redex_Stuck [OF this]
        have "Γ⊢ ⟨c⇩1,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 c⇩1 = Call p" and "Γ p = None"
        hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Stuck"
          by (auto intro: exec.intros)
        from exec_redex_Stuck [OF this]
        have "Γ⊢ ⟨c⇩1,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 c⇩2 s t) thus ?case
    by (cases s) (fastforce intro: exec.intros elim: exec_elim_cases)+
next
  case (SeqThrow c⇩2 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 c⇩1 s c⇩1' s' c⇩2 t)
  have step: "Γ⊢ (c⇩1, s) → (c⇩1', s')" by fact
  have exec': "Γ⊢ ⟨Catch c⇩1' c⇩2,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_c⇩1': "Γ⊢ ⟨c⇩1',Normal x'⟩ ⇒ Abrupt s''"
        assume exec_c⇩2: "Γ⊢ ⟨c⇩2,Normal s''⟩ ⇒ t"
        from Catch.hyps (2) Normal exec_c⇩1' s_Normal
        have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ Abrupt s''"
          by simp
        from exec.CatchMatch [OF this exec_c⇩2] s_Normal
        show ?thesis by simp
      next
        assume exec_c⇩1': "Γ⊢ ⟨c⇩1',Normal x'⟩ ⇒ t"
        assume t: "¬ isAbr t"
        from Catch.hyps (2) Normal exec_c⇩1' s_Normal
        have "Γ⊢ ⟨c⇩1,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_c⇩1: "redex c⇩1 = Guard f g c" and
        fail: "x ∉ g"
        by auto
      hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Fault f"
        by (auto intro: exec.intros)
      from exec_redex_Fault [OF this]
      have "Γ⊢ ⟨c⇩1,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 c⇩1 = Spec r ∧ (∀t. (x, t) ∉ r)) ∨
            (∃p. redex c⇩1 = Call p ∧ Γ p = None)"
        by auto
      moreover
      {
        fix r
        assume "redex c⇩1 = Spec r" and "(∀t. (x, t) ∉ r)"
        hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Stuck"
          by (auto intro: exec.intros)
        from exec_redex_Stuck [OF this]
        have "Γ⊢ ⟨c⇩1,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 c⇩1 = Call p" and "Γ p = None"
        hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Stuck"
          by (auto intro: exec.intros)
        from exec_redex_Stuck [OF this]
        have "Γ⊢ ⟨c⇩1,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 Computations›
(* ************************************************************************ *)


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 c⇩1 s c⇩1' s' c⇩2) 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 c⇩2 s)
  thus ?case
    apply (cases s)
    apply (fastforce intro: terminates.intros exec.intros
            elim: terminates_Normal_elim_cases )+
    done
next
  case (SeqThrow c⇩2 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 c⇩1 s c⇩1' s' c⇩2) 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 c⇩2 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 c⇩1 c⇩2 ⇒ c⇩1
   | Catch c⇩1 c⇩2 ⇒ c⇩1
   | _ ⇒ 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 c⇩1 c⇩2,s)"
  assumes not_fin: "∀i<k. ¬ final (head (f i))"
  shows "∀i<k. (∃c' s'. f (i + 1) = (Seq c' c⇩2, 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' c⇩2, 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' c⇩2, s')"
        by (cases k) auto
      from inf_comp [rule_format, of k] f_k
      have "Γ⊢(Seq c' c⇩2, 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'' c⇩2, 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 c⇩1 c⇩2,s)"
  assumes not_fin: "∀i<k. ¬ final (head (f i))"
  shows "∀i<k. (∃c' s'. f (i + 1) = (Catch c' c⇩2, 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' c⇩2, 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' c⇩2, s')"
        by (cases k) auto
      from inf_comp [rule_format, of k] f_k
      have "Γ⊢(Catch c' c⇩2, 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'' c⇩2, 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 c⇩1 c⇩2,s) → …(∞)"
  shows "Γ⊢(c⇩1,s) → …(∞) ∨
         (∃s'. Γ⊢(c⇩1,s) →⇧* (Skip,s') ∧ Γ⊢(c⇩2,s') → …(∞))"
proof -
  from inf_comp obtain f where
    step: "∀i::nat. Γ⊢f i → f (i+1)" and
    f_0: "f 0 = (Seq c⇩1 c⇩2, s)"
    by (auto simp add: inf_def)
  from f_0 have head_f_0: "head (f 0) = (c⇩1,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' c⇩2, 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' c⇩2,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 c⇩2, s')"
      with steps_head
      have "Γ⊢(c⇩1,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 c⇩2,s') → (c⇩2,s')" and
        f_Suc_k: "f (k + 1) = (c⇩2,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 = (c⇩2,s')"
        by (simp add: g_def)
      from step
      have "∀i. Γ⊢g i → g (i + 1)"
        by (simp add: g_def)
      with g_0 have "Γ⊢(c⇩2,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 c⇩2, s')"
      from step [rule_format, of k] f_k s'
      obtain "Γ⊢(Seq Throw c⇩2,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 "Γ⊢(c⇩1,s) → …(∞)"
      by (auto simp add: inf_def)
    thus ?thesis
      by simp
  qed
qed

lemma split_inf_Catch:
  assumes inf_comp: "Γ⊢(Catch c⇩1 c⇩2,s) → …(∞)"
  shows "Γ⊢(c⇩1,s) → …(∞) ∨
         (∃s'. Γ⊢(c⇩1,s) →⇧* (Throw,Normal s') ∧ Γ⊢(c⇩2,Normal s') → …(∞))"
proof -
  from inf_comp obtain f where
    step: "∀i::nat. Γ⊢f i → f (i+1)" and
    f_0: "f 0 = (Catch c⇩1 c⇩2, s)"
    by (auto simp add: inf_def)
  from f_0 have head_f_0: "head (f 0) = (c⇩1,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' c⇩2, 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' c⇩2,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 c⇩2, s')"
      with steps_head
      have "Γ⊢(c⇩1,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 c⇩2,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 c⇩2, s')"
      with steps_head
      have "Γ⊢(c⇩1,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 c⇩2,s') → (c⇩2,s')" and
        f_Suc_k: "f (k + 1) = (c⇩2,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 = (c⇩2,s')"
        by (simp add: g_def)
      from step
      have "∀i. Γ⊢g i → g (i + 1)"
        by (simp add: g_def)
      with g_0 have "Γ⊢(c⇩2,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 "Γ⊢(c⇩1,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 c⇩1 c⇩2)
  show ?case
  proof
    assume "Γ⊢ (Seq c⇩1 c⇩2, Stuck) → …(∞)"
    from split_inf_Seq [OF this] Seq.hyps
    show False
      by (auto dest: steps_Stuck_prop)
  qed
next
  case (Cond b c⇩1 c⇩2)
  show ?case
  proof (rule not_infI)
    fix f
    assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
    assume f_0: "f 0 = (Cond b c⇩1 c⇩2, 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 c⇩1 c⇩2)
  show ?case
  proof
    assume "Γ⊢ (Catch c⇩1 c⇩2, 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 c⇩1 c⇩2)
  show ?case
  proof
    assume "Γ⊢ (Seq c⇩1 c⇩2, Fault x) → …(∞)"
    from split_inf_Seq [OF this] Seq.hyps
    show False
      by (auto dest: steps_Fault_prop)
  qed
next
  case (Cond b c⇩1 c⇩2)
  show ?case
  proof (rule not_infI)
    fix f
    assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
    assume f_0: "f 0 = (Cond b c⇩1 c⇩2, 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 c⇩1 c⇩2)
  show ?case
  proof
    assume "Γ⊢ (Catch c⇩1 c⇩2, 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 c⇩1 c⇩2)
  show ?case
  proof
    assume "Γ⊢ (Seq c⇩1 c⇩2, Abrupt s) → …(∞)"
    from split_inf_Seq [OF this] Seq.hyps
    show False
      by (auto dest: steps_Abrupt_prop)
  qed
next
  case (Cond b c⇩1 c⇩2)
  show ?case
  proof (rule not_infI)
    fix f
    assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
    assume f_0: "f 0 = (Cond b c⇩1 c⇩2, 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 c⇩1 c⇩2)
  show ?case
  proof
    assume "Γ⊢ (Catch c⇩1 c⇩2, 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 c⇩1 s c⇩2)
  show ?case
  proof
    assume "Γ⊢ (Seq c⇩1 c⇩2, 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 c⇩1 s c⇩2)
  show ?case
  proof
    assume "Γ⊢ (Catch c⇩1 c⇩2, 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 c⇩1 c⇩2) c  = Seq (subst_redex c⇩1 c) c⇩2" |
"subst_redex (Cond b c⇩1 c⇩2) 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 c⇩1 c⇩2) c = Catch (subst_redex c⇩1 c) c⇩2"

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 c⇩1 c⇩2)
  thus ?case
    by (cases "final (c⇩1,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 c⇩1 c⇩2)
  thus ?case
    by (cases "final (c⇩1,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) →⇧* (c⇩f, s⇩f)"
assumes not_final: "¬ final (c,s)"
assumes final: "final (c⇩f,s⇩f)"
shows "∃c' s'. Γ⊢ (c, s) → (c',s') ∧ Γ⊢ (c', s') →⇧* (c⇩f, s⇩f)"
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 c⇩1 c⇩2)
  have hyp: "⋀c' s'. Γ⊢ (Seq c⇩1 c⇩2, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
  show ?case
  proof (rule terminates.Seq)
    {
      fix c' s'
      assume step_c⇩1: "Γ⊢ (c⇩1, Normal s) → (c', s')"
      have "Γ⊢c' ↓ s'"
      proof -
        from step_c⇩1
        have "Γ⊢ (Seq c⇩1 c⇩2, Normal s) → (Seq c' c⇩2, s')"
          by (rule step.Seq)
        from hyp [OF this]
        have "Γ⊢Seq c' c⇩2 ↓ s'".
        thus "Γ⊢c'↓ s'"
          by cases auto
      qed
    }
    from Seq.hyps (1) [OF this]
    show "Γ⊢c⇩1 ↓ Normal s".
  next
    show "∀s'. Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ s' ⟶ Γ⊢c⇩2 ↓ s'"
    proof (intro allI impI)
      fix s'
      assume exec_c⇩1: "Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ s'"
      show "Γ⊢c⇩2 ↓ s'"
      proof (cases "final (c⇩1,Normal s)")
        case True
        hence "c⇩1=Skip ∨ c⇩1=Throw"
          by (simp add: final_def)
        thus ?thesis
        proof
          assume Skip: "c⇩1=Skip"
          have "Γ⊢(Seq Skip c⇩2,Normal s) → (c⇩2,Normal s)"
            by (rule step.SeqSkip)
          from hyp [simplified Skip, OF this]
          have "Γ⊢c⇩2 ↓ Normal s" .
          moreover from exec_c⇩1 Skip
          have "s'=Normal s"
            by (auto elim: exec_Normal_elim_cases)
          ultimately show ?thesis by simp
        next
          assume Throw: "c⇩1=Throw"
          with exec_c⇩1 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_c⇩1]
        obtain c⇩f t where
          steps_c⇩1: "Γ⊢ (c⇩1, Normal s) →⇧* (c⇩f, t)" and
          fin:"(case s' of
                 Abrupt x ⇒ c⇩f = Throw ∧ t = Normal x
                | _ ⇒ c⇩f = Skip ∧ t = s')"
          by (fastforce split: xstate.splits)
        with fin have final: "final (c⇩f,t)"
          by (cases s') (auto simp add: final_def)
        from split_computation [OF steps_c⇩1 False this]
        obtain c'' s'' where
          first: "Γ⊢ (c⇩1, Normal s) → (c'', s'')" and
          rest: "Γ⊢ (c'', s'') →⇧* (c⇩f, t)"
          by blast
        from step.Seq [OF first]
        have "Γ⊢ (Seq c⇩1 c⇩2, Normal s) → (Seq c'' c⇩2, s'')".
        from hyp [OF this]
        have termi_s'': "Γ⊢Seq c'' c⇩2 ↓ s''".
        show ?thesis
        proof (cases s'')
          case (Normal x)
          from termi_s'' [simplified Normal]
          have termi_c⇩2: "∀t. Γ⊢ ⟨c'',Normal x⟩ ⇒ t ⟶ Γ⊢c⇩2 ↓ t"
            by cases
          show ?thesis
          proof (cases "∃x'. s'=Abrupt x'")
            case False
            with fin obtain "c⇩f=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_c⇩2 [rule_format, OF this]
            show "Γ⊢c⇩2 ↓ s'" .
          next
            case True
            with fin obtain x' where s': "s'=Abrupt x'" and "c⇩f=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_c⇩2 [rule_format, OF this] s'
            show "Γ⊢c⇩2 ↓ 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 "Γ⊢c⇩2 ↓ 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 "Γ⊢c⇩2 ↓ 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 "Γ⊢c⇩2 ↓ s'"
            by auto
        qed
      qed
    qed
  qed
next
  case (Cond b c⇩1 c⇩2)
  have hyp: "⋀c' s'. Γ⊢ (Cond b c⇩1 c⇩2, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
  show ?case
  proof (cases "s∈b")
    case True
    then have "Γ⊢ (Cond b c⇩1 c⇩2, Normal s) → (c⇩1, Normal s)"
      by (rule step.CondTrue)
    from hyp [OF this] have "Γ⊢c⇩1 ↓ Normal s".
    with True show ?thesis
      by (auto intro: terminates.intros)
  next
    case False
    then have "Γ⊢ (Cond b c⇩1 c⇩2, Normal s) → (c⇩2, Normal s)"
      by (rule step.CondFalse)
    from hyp [OF this] have "Γ⊢c⇩2 ↓ 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 c⇩1 c⇩2)
  have hyp: "⋀c' s'. Γ⊢ (Catch c⇩1 c⇩2, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
  show ?case
  proof (rule terminates.Catch)
    {
      fix c' s'
      assume step_c⇩1: "Γ⊢ (c⇩1, Normal s) → (c', s')"
      have "Γ⊢c' ↓ s'"
      proof -
        from step_c⇩1
        have "Γ⊢ (Catch c⇩1 c⇩2, Normal s) → (Catch c' c⇩2, s')"
          by (rule step.Catch)
        from hyp [OF this]
        have "Γ⊢Catch c' c⇩2 ↓ s'".
        thus "Γ⊢c'↓ s'"
          by cases auto
      qed
    }
    from Catch.hyps (1) [OF this]
    show "Γ⊢c⇩1 ↓ Normal s".
  next
    show "∀s'. Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ Abrupt s' ⟶ Γ⊢c⇩2 ↓ Normal s'"
    proof (intro allI impI)
      fix s'
      assume exec_c⇩1: "Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ Abrupt s'"
      show "Γ⊢c⇩2 ↓ Normal s'"
      proof (cases "final (c⇩1,Normal s)")
        case True
        with exec_c⇩1
        have Throw: "c⇩1=Throw"
          by (auto simp add: final_def elim: exec_Normal_elim_cases)
        have "Γ⊢(Catch Throw c⇩2,Normal s) → (c⇩2,Normal s)"
          by (rule step.CatchThrow)
        from hyp [simplified Throw, OF this]
        have "Γ⊢c⇩2 ↓ Normal s".
        moreover from exec_c⇩1 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_c⇩1]
        obtain c⇩f t where
          steps_c⇩1: "Γ⊢ (c⇩1, Normal s) →⇧* (Throw, Normal s')"
          by (fastforce split: xstate.splits)
        from split_computation [OF steps_c⇩1 False]
        obtain c'' s'' where
          first: "Γ⊢ (c⇩1, Normal s) → (c'', s'')" and
          rest: "Γ⊢ (c'', s'') →⇧* (Throw, Normal s')"
          by (auto simp add: final_def)
        from step.Catch [OF first]
        have "Γ⊢ (Catch c⇩1 c⇩2, Normal s) → (Catch c'' c⇩2, s'')".
        from hyp [OF this]
        have "Γ⊢Catch c'' c⇩2 ↓ 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 ‹
For an important lemma for the completeness proof of the Hoare-logic for
total correctness we need a generalisation of @{const "redex"} that not only
yield 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 c⇩1 c⇩2) = {Seq c⇩1 c⇩2} ∪ redexes c⇩1" |
"redexes (Cond b c⇩1 c⇩2) = {Cond b c⇩1 c⇩2}" |
"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 c⇩1 c⇩2) = {Catch c⇩1 c⇩2} ∪ redexes c⇩1"

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 c⇩1 c⇩2)
  have "r ∈ redexes (Seq c⇩1 c⇩2)" by fact
  hence r: "r = Seq c⇩1 c⇩2 ∨ r ∈ redexes c⇩1"
    by simp
  have step_r: "Γ⊢ (r, s) → (r', s')" by fact
  from r show ?case
  proof
    assume "r = Seq c⇩1 c⇩2"
    with step_r
    show ?case
      by (auto simp add: root_in_redexes)
  next
    assume r: "r ∈ redexes c⇩1"
    from Seq.hyps (1) [OF step_r this]
    obtain c' where
      step_c⇩1: "Γ⊢ (c⇩1, s) → (c', s')" and
      r': "r' ∈ redexes c'"
      by blast
    from step.Seq [OF step_c⇩1]
    have "Γ⊢ (Seq c⇩1 c⇩2, s) → (Seq c' c⇩2, 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 c⇩1 c⇩2)
  have "r ∈ redexes (Catch c⇩1 c⇩2)" by fact
  hence r: "r = Catch c⇩1 c⇩2 ∨ r ∈ redexes c⇩1"
    by simp
  have step_r: "Γ⊢ (r, s) → (r', s')" by fact
  from r show ?case
  proof
    assume "r = Catch c⇩1 c⇩2"
    with step_r
    show ?case
      by (auto simp add: root_in_redexes)
  next
    assume r: "r ∈ redexes c⇩1"
    from Catch.hyps (1) [OF step_r this]
    obtain c' where
      step_c⇩1: "Γ⊢ (c⇩1, s) → (c', s')" and
      r': "r' ∈ redexes c'"
      by blast
    from step.Catch [OF step_c⇩1]
    have "Γ⊢ (Catch c⇩1 c⇩2, s) → (Catch c' c⇩2, 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 c⇩2 ∈ redexes c"
  shows "∃c'. Γ⊢(c,s) → (c',s') ∧ Seq r' c⇩2 ∈ redexes c'"
proof -
  from step.Seq [OF step]
  have "Γ⊢ (Seq r c⇩2, s) → (Seq r' c⇩2, s')".
  from step_redexes [OF this Seq]
  show ?thesis .
qed

lemma steps_redexes_Seq:
  assumes steps: "Γ⊢ (r, s) →⇧* (r', s')"
  shows "⋀c. Seq r c⇩2 ∈ redexes c ⟹
              ∃c'. Γ⊢(c,s) →⇧* (c',s') ∧ Seq r' c⇩2 ∈ 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 c⇩2 ∈ redexes c" by fact+
  from step_redexes_Seq [OF this]
  obtain c' where
    step: "Γ⊢ (c, s) → (c', s'')" and
    r'': "Seq r'' c⇩2 ∈ 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' c⇩2 ∈ 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 c⇩2 ∈ redexes c
             ⟹ ∃c'. Γ⊢(c,s) →⇧+ (c',s') ∧ Seq r' c⇩2 ∈ 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 c⇩2 ∈ 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' c⇩2 ∈ 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'' c⇩2 ∈ 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 c⇩2 ∈ redexes c"
  shows "∃c'. Γ⊢(c,s) → (c',s') ∧ Catch r' c⇩2 ∈ redexes c'"
proof -
  from step.Catch [OF step]
  have "Γ⊢ (Catch r c⇩2, s) → (Catch r' c⇩2, s')".
  from step_redexes [OF this Catch]
  show ?thesis .
qed

lemma steps_redexes_Catch:
  assumes steps: "Γ⊢ (r, s) →⇧* (r', s')"
  shows "⋀c. Catch r c⇩2 ∈ redexes c ⟹
              ∃c'. Γ⊢(c,s) →⇧* (c',s') ∧ Catch r' c⇩2 ∈ 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 c⇩2 ∈ redexes c" by fact+
  from step_redexes_Catch [OF this]
  obtain c' where
    step: "Γ⊢ (c, s) → (c', s'')" and
    r'': "Catch r'' c⇩2 ∈ 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' c⇩2 ∈ 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 c⇩2 ∈ redexes c
             ⟹ ∃c'. Γ⊢(c,s) →⇧+ (c',s') ∧ Catch r' c⇩2 ∈ 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 c⇩2 ∈ 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' c⇩2 ∈ 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'' c⇩2 ∈ 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