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 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: "sg  Γ(Guard f g c,Normal s)  (c,Normal s)"

| GuardFault: "sg  Γ(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:  "sb  Γ(Cond b c1 c2,Normal s)  (c1,Normal s)"
| CondFalse: "sb  Γ(Cond b c1 c2,Normal s)  (c2,Normal s)"

| WhileTrue: "sb
              
              Γ(While b c,Normal s)  (Seq c (While b c),Normal s)"

| WhileFalse: "sb
               
               Γ(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:  "cSkip; redex c = c  Γ(c,Fault f)  (Skip,Fault f)"
| StuckProp:  "cSkip; redex c = c  Γ(c,Stuck)  (Skip,Stuck)"
| AbruptProp: "cSkip; 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: "Γ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 Computations›
(* ************************************************************************ *)


lemma step_preserves_termination:
  assumes step: "Γ(c,s)  (c',s')"
  shows "Γcs  Γ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 "Γcs  Γ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 "Γcs  Γ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 pNormal 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: "Γcs"
 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)  Γcs"
  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 "sb")
    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 "sb")
    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 "sg")
    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) Γc1s1"
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 "Γcs"
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:
  "Γcs = (¬ Γ (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 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: "Γcs"
  shows "c'. c'  redexes c  Γc's"
using termi
by induct (auto intro: terminates.intros)


end