Quelle  Termination.thy

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2004-2008 Norbert Schirmer
Copyright (c) 2022 Apple Inc. All rights reserved.
*)
section ‹Terminating Programs›

theory Termination imports Semantic begin

subsection ‹Inductive Characterisation: ‹Γ⊨c↓s››

inductive "terminates"::"('s,'p,'f) body ==> ('s,'p,'f) com ==> ('s,'f) xstate ==> bool"
  (‹_⊨_ ↓ _› [60,20,60] 89)
  for  Γ::"('s,'p,'f) body"
where
  Skip: "Γ⊨Skip ↓(Normal s)"

| Basic: "Γ⊨Basic f ↓(Normal s)"

| Spec: "Γ⊨Spec r ↓(Normal s)"

| Guard: "[s∈g; Γ⊨c↓(Normal s)]
          ==>
          Γ⊨Guard f g c↓(Normal s)"

| GuardFault: "s∉g
               ==>
               Γ⊨Guard f g c↓(Normal s)"


| Fault [intro,simp]: "Γ⊨c↓Fault f"


| Seq: "[Γ⊨c₁↓Normal s; ∀s'. Γ⊨⟨c₁,Normal s⟩ ==> s' ⟶ Γ⊨c₂↓s']
        ==>
        Γ⊨Seq c₁ c₂↓(Normal s)"

| CondTrue: "[s ∈ b; Γ⊨c₁↓(Normal s)]
             ==>
             Γ⊨Cond b c₁ c₂↓(Normal s)"


| CondFalse: "[s ∉ b; Γ⊨c₂↓(Normal s)]
             ==>
             Γ⊨Cond b c₁ c₂↓(Normal s)"


| WhileTrue: "[s ∈ b; Γ⊨c↓(Normal s);
               ∀s'. Γ⊨⟨c,Normal s ⟩ ==> s' ⟶ Γ⊨While b c↓s']
              ==>
              Γ⊨While b c↓(Normal s)"

| WhileFalse: "[s ∉ b]
               ==>
               Γ⊨While b c↓(Normal s)"

| Call:  "[Γ p=Some bdy;Γ⊨bdy↓(Normal s)]
          ==>
          Γ⊨Call p↓(Normal s)"

| CallUndefined:  "[Γ p = None]
                   ==>
                   Γ⊨Call p↓(Normal s)"

| Stuck [intro,simp]: "Γ⊨c↓Stuck"

| DynCom:  "[Γ⊨(c s)↓(Normal s)]
             ==>
             Γ⊨DynCom c↓(Normal s)"

| Throw: "Γ⊨Throw↓(Normal s)"

| Abrupt [intro,simp]: "Γ⊨c↓Abrupt s"

| Catch: "[Γ⊨c₁↓Normal s;
           ∀s'. Γ⊨⟨c₁,Normal s ⟩ ==> Abrupt s' ⟶ Γ⊨c₂↓Normal s']
          ==>
          Γ⊨Catch c₁ c₂↓Normal s"


inductive_cases terminates_elim_cases [cases set]:
  "Γ⊨Skip ↓ s"
  "Γ⊨Guard f g c ↓ s"
  "Γ⊨Basic f ↓ s"
  "Γ⊨Spec r ↓ s"
  "Γ⊨Seq c1 c2 ↓ s"
  "Γ⊨Cond b c1 c2 ↓ s"
  "Γ⊨While b c ↓ s"
  "Γ⊨Call p ↓ s"
  "Γ⊨DynCom c ↓ s"
  "Γ⊨Throw ↓ s"
  "Γ⊨Catch c1 c2 ↓ s"

inductive_cases terminates_Normal_elim_cases [cases set]:
  "Γ⊨Skip ↓ Normal s"
  "Γ⊨Guard f g c ↓ Normal s"
  "Γ⊨Basic f ↓ Normal s"
  "Γ⊨Spec r ↓ Normal s"
  "Γ⊨Seq c1 c2 ↓ Normal s"
  "Γ⊨Cond b c1 c2 ↓ Normal s"
  "Γ⊨While b c ↓ Normal s"
  "Γ⊨Call p ↓ Normal s"
  "Γ⊨DynCom c ↓ Normal s"
  "Γ⊨Throw ↓ Normal s"
  "Γ⊨Catch c1 c2 ↓ Normal s"

lemma terminates_Skip': "Γ⊨Skip ↓ s"
  by (cases s) (auto intro: terminates.intros)

lemma terminates_Call_body:
 "Γ p=Some bdy==>Γ⊨Call p ↓s = Γ⊨(the (Γ p))↓s"
  by (cases s)
     (auto elim: terminates_Normal_elim_cases intro: terminates.intros)

lemma terminates_Normal_Call_body:
 "p ∈ dom Γ ==>
  Γ⊨Call p ↓Normal s = Γ⊨(the (Γ p))↓Normal s"
  by (auto elim: terminates_Normal_elim_cases intro: terminates.intros)

lemma terminates_implies_exec:
  assumes terminates: "Γ⊨c↓s"
  shows "∃t. Γ⊨⟨c,s⟩ ==> t"
using terminates
proof (induct)
  case Skip thus ?case by (iprover intro: exec.intros)
next
  case Basic thus ?case by (iprover intro: exec.intros)
next
  case (Spec r s) thus ?case
    by (cases "∃t. (s,t)∈ r") (auto intro: exec.intros)
next
  case Guard thus ?case by (iprover intro: exec.intros)
next
  case GuardFault thus ?case by (iprover intro: exec.intros)
next
  case Fault thus ?case by (iprover intro: exec.intros)
next
  case Seq thus ?case by (iprover intro: exec_Seq')
next
  case CondTrue thus ?case by (iprover intro: exec.intros)
next
  case CondFalse thus ?case by (iprover intro: exec.intros)
next
  case WhileTrue thus ?case by (iprover intro: exec.intros)
next
  case WhileFalse thus ?case by (iprover intro: exec.intros)
next
  case (Call p bdy s)
  then obtain s' where
    "Γ⊨⟨bdy,Normal s ⟩ ==> s'"
    by iprover
  moreover have "Γ p = Some bdy" by fact
  ultimately show ?case
    by (cases s') (iprover intro: exec.intros)+
next
  case CallUndefined thus ?case by (iprover intro: exec.intros)
next
  case Stuck thus ?case by (iprover intro: exec.intros)
next
  case DynCom thus ?case by (iprover intro: exec.intros)
next
  case Throw thus ?case by (iprover intro: exec.intros)
next
  case Abrupt thus ?case by (iprover intro: exec.intros)
next
  case (Catch c1 s c2)
  then obtain s' where exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> s'"
    by iprover
  thus ?case
  proof (cases s')
    case (Normal s'')
    with exec_c1 show ?thesis by (auto intro!: exec.intros)
  next
    case (Abrupt s'')
    with exec_c1 Catch.hyps
    obtain t where "Γ⊨⟨c2,Normal s'' ⟩ ==> t"
      by auto
    with exec_c1 Abrupt show ?thesis by (auto intro: exec.intros)
  next
    case Fault
    with exec_c1 show ?thesis by (auto intro!: exec.CatchMiss)
  next
    case Stuck
    with exec_c1 show ?thesis by (auto intro!: exec.CatchMiss)
  qed
qed

lemma terminates_block_exn:
"[Γ⊨bdy ↓ Normal (init s);
  ∀t. Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t ⟶ Γ⊨c s t ↓ Normal (return s t)]
 ==> Γ⊨block_exn init bdy return result_exn c ↓ Normal s"
apply (unfold block_exn_def)
apply (fastforce intro: terminates.intros elim!: exec_Normal_elim_cases
        dest!: not_isAbrD)
  done

lemma terminates_block:
"[Γ⊨bdy ↓ Normal (init s);
  ∀t. Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t ⟶ Γ⊨c s t ↓ Normal (return s t)]
 ==> Γ⊨block init bdy return c ↓ Normal s"
  unfolding block_def
  by (rule terminates_block_exn)

lemma terminates_block_exn_elim [cases set, consumes 1]:
assumes termi: "Γ⊨block_exn init bdy return result_exn c ↓ Normal s"
assumes e: "[Γ⊨bdy ↓ Normal (init s);
          ∀t. Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t ⟶ Γ⊨c s t ↓ Normal (return s t)
         ] ==> P"
shows P
proof -
  have "Γ⊨⟨Basic init,Normal s⟩ ==> Normal (init s)"
    by (auto intro: exec.intros)
  with termi
  have "Γ⊨bdy ↓ Normal (init s)"
    apply (unfold block_exn_def)
    apply (elim terminates_Normal_elim_cases)
    by simp
  moreover
  {
    fix t
    assume exec_bdy: "Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t"
    have "Γ⊨c s t ↓ Normal (return s t)"
    proof -
      from exec_bdy
      have "Γ⊨⟨Catch (Seq (Basic init) bdy)
                               (Seq (Basic (λt. result_exn (return s t) t)) Throw),Normal s⟩ ==> Normal t"
        by (fastforce intro: exec.intros)
      with termi have "Γ⊨DynCom (λt. Seq (Basic (return s)) (c s t)) ↓ Normal t"
        apply (unfold block_exn_def)
        apply (elim terminates_Normal_elim_cases)
        by simp
      thus ?thesis
        apply (elim terminates_Normal_elim_cases)
        apply (auto intro: exec.intros)
        done
    qed
  }
  ultimately show P by (iprover intro: e)
qed

lemma terminates_block_elim [cases set, consumes 1]:
assumes termi: "Γ⊨block init bdy return c ↓ Normal s"
assumes e: "[Γ⊨bdy ↓ Normal (init s);
          ∀t. Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t ⟶ Γ⊨c s t ↓ Normal (return s t)
         ] ==> P"
shows P
  using termi e unfolding block_def by (rule terminates_block_exn_elim)


lemma terminates_call:
"[Γ p = Some bdy; Γ⊨bdy ↓ Normal (init s);
  ∀t. Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t ⟶ Γ⊨c s t ↓ Normal (return s t)]
 ==> Γ⊨call init p return c ↓ Normal s"
  apply (unfold call_def)
  apply (rule terminates_block)
  apply  (iprover intro: terminates.intros)
  apply (auto elim: exec_Normal_elim_cases)
  done

lemma terminates_call_exn:
"[Γ p = Some bdy; Γ⊨bdy ↓ Normal (init s);
  ∀t. Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t ⟶ Γ⊨c s t ↓ Normal (return s t)]
 ==> Γ⊨call_exn init p return result_exn c ↓ Normal s"
  apply (unfold call_exn_def)
  apply (rule terminates_block_exn)
  apply  (iprover intro: terminates.intros)
  apply (auto elim: exec_Normal_elim_cases)
  done

lemma terminates_callUndefined:
"[Γ p = None]
 ==> Γ⊨call init p return result ↓ Normal s"
  apply (unfold call_def)
  apply (rule terminates_block)
  apply  (iprover intro: terminates.intros)
  apply (auto elim: exec_Normal_elim_cases)
  done

lemma terminates_call_exnUndefined:
"[Γ p = None]
 ==> Γ⊨call_exn init p return result_exn result ↓ Normal s"
  apply (unfold call_exn_def)
  apply (rule terminates_block_exn)
  apply  (iprover intro: terminates.intros)
  apply (auto elim: exec_Normal_elim_cases)
  done

lemma terminates_call_exn_elim [cases set, consumes 1]:
assumes termi: "Γ⊨call_exn init p return result_exn c ↓ Normal s"
assumes bdy: "∧bdy. [Γ p = Some bdy; Γ⊨bdy ↓ Normal (init s);
     ∀t. Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t ⟶ Γ⊨c s t ↓ Normal (return s t)] ==> P"
assumes undef: "[Γ p = None] ==> P"
shows P
apply (cases "Γ p")
apply  (erule undef)
using termi
apply (unfold call_exn_def)
apply (erule terminates_block_exn_elim)
apply (erule terminates_Normal_elim_cases)
apply  simp
apply  (frule (1) bdy)
apply   (fastforce intro: exec.intros)
apply  assumption
apply simp
done

lemma terminates_call_elim [cases set, consumes 1]:
assumes termi: "Γ⊨call init p return c ↓ Normal s"
assumes bdy: "∧bdy. [Γ p = Some bdy; Γ⊨bdy ↓ Normal (init s);
     ∀t. Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t ⟶ Γ⊨c s t ↓ Normal (return s t)] ==> P"
assumes undef: "[Γ p = None] ==> P"
shows P
  using termi bdy undef unfolding call_call_exn by (rule terminates_call_exn_elim)


lemma terminates_dynCall:
"[Γ⊨call init (p s) return c ↓ Normal s]
 ==> Γ⊨dynCall init p return c ↓ Normal s"
  apply (unfold dynCall_def)
  apply (auto intro: terminates.intros terminates_call)
  done

lemma terminates_guards: "Γ⊨c ↓ Normal s ==> Γ⊨guards gs c ↓ Normal s"
  by (induct gs) (auto intro: terminates.intros)

lemma terminates_guards_Fault: "find (λ(f, g). s ∉ g) gs = Some (f, g) ==> Γ⊨guards gs c ↓ Normal s"
 by (induct gs) (auto intro: terminates.intros split: if_split_asm prod.splits)

lemma terminates_maybe_guard_Fault: "s ∉ g ==> Γ⊨maybe_guard f g c ↓ Normal s"
  by (metis UNIV_I maybe_guard_def terminates.GuardFault)

lemma terminates_guards_DynCom: "Γ⊨(c s) ↓ Normal s ==> Γ⊨guards gs (DynCom c) ↓ Normal s"
  by (induct gs) (auto intro: terminates.intros)

lemma terminates_maybe_guard_DynCom: "Γ⊨(c s) ↓ Normal s ==> Γ⊨maybe_guard f g (DynCom c) ↓ Normal s"
  by (metis maybe_guard_def terminates.DynCom terminates.Guard terminates.GuardFault)


lemma terminates_dynCall_exn:
"[Γ⊨call_exn init (p s) return result_exn c ↓ Normal s]
 ==> Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s"
  apply (unfold dynCall_exn_def)
  by (rule terminates_maybe_guard_DynCom)

lemma terminates_dynCall_elim [cases set, consumes 1]:
assumes termi: "Γ⊨dynCall init p return c ↓ Normal s"
assumes "[Γ⊨call init (p s) return c ↓ Normal s] ==> P"
shows P
using termi
apply (unfold dynCall_def)
apply (elim terminates_Normal_elim_cases)
apply fact
done

lemma terminates_guards_elim [cases set, consumes 1, case_names noFault someFault]:
  assumes termi: "Γ⊨guards gs c ↓ Normal s"
  assumes noFault: "[∀f g. (f, g) ∈ set gs ⟶ s ∈ g; Γ⊨c ↓ Normal s] ==> P"
  assumes someFault: "∧f g. find (λ(f,g). s ∉ g) gs = Some (f, g) ==> P"
  shows P
  using termi noFault someFault
  by (induct gs)
     (auto elim: terminates_Normal_elim_cases split: if_split_asm prod.splits)

lemma terminates_maybe_guard_elim [cases set, consumes 1, case_names noFault someFault]:
  assumes termi: "Γ⊨maybe_guard f g c ↓ Normal s"
  assumes noFault: "[s ∈ g; Γ⊨c ↓ Normal s] ==> P"
  assumes someFault: "s ∉ g ==> P"
  shows P
  using termi noFault someFault
  by (metis maybe_guard_def terminates_Normal_elim_cases(2))

lemma terminates_dynCall_exn_elim [cases set, consumes 1, case_names noFault someFault]:
assumes termi: "Γ⊨dynCall_exn f g init p return result_exn c ↓ Normal s"
assumes noFault: "[s ∈ g;
 Γ⊨call_exn init (p s) return result_exn c ↓ Normal s] ==> P"
assumes someFault: "s ∉ g ==> P"
shows P
using termi noFault someFault
  apply (unfold dynCall_exn_def)
  apply (erule terminates_maybe_guard_elim)
  apply (auto elim: terminates_Normal_elim_cases)
  done

(* ************************************************************************* *)
subsection ‹Lemmas about @{const "sequence"}, @{const "flatten"} and
 @{const "normalize"}›
(* ************************************************************************ *)

lemma terminates_sequence_app:
  "∧s. [Γ⊨sequence Seq xs ↓ Normal s;
        ∀s'. Γ⊨⟨sequence Seq xs,Normal s ⟩ ==> s' ⟶ Γ⊨sequence Seq ys ↓ s']
\<Longrightarrow> Γ⊨sequence Seq (xs @ ys) ↓ Normal s"
proof (induct xs)
  case Nil
  thus ?case by (auto intro: exec.intros)
next
  case (Cons x xs)
  have termi_x_xs: "Γ⊨sequence Seq (x # xs) ↓ Normal s" by fact
  have termi_ys: "∀s'. Γ⊨⟨sequence Seq (x # xs),Normal s ⟩ ==> s' ⟶ Γ⊨sequence Seq ys ↓ s'" by fact
  show ?case
  proof (cases xs)
    case Nil
    with termi_x_xs termi_ys show ?thesis
      by (cases ys) (auto intro: terminates.intros)
  next
    case Cons
    from termi_x_xs Cons
    have "Γ⊨x ↓ Normal s"
      by (auto elim: terminates_Normal_elim_cases)
    moreover
    {
      fix s'
      assume exec_x: "Γ⊨⟨x,Normal s ⟩ ==> s'"
      have "Γ⊨sequence Seq (xs @ ys) ↓ s'"
      proof -
        from exec_x termi_x_xs Cons
        have termi_xs: "Γ⊨sequence Seq xs ↓ s'"
          by (auto elim: terminates_Normal_elim_cases)
        show ?thesis
        proof (cases s')
          case (Normal s'')
          with exec_x termi_ys Cons
          have "∀s'. Γ⊨⟨sequence Seq xs,Normal s'' ⟩ ==> s' ⟶ Γ⊨sequence Seq ys ↓ s'"
            by (auto intro: exec.intros)
          from Cons.hyps [OF termi_xs [simplified Normal] this]
          have "Γ⊨sequence Seq (xs @ ys) ↓ Normal s''".
          with Normal show ?thesis by simp
        next
          case Abrupt thus ?thesis by (auto intro: terminates.intros)
        next
          case Fault thus ?thesis by (auto intro: terminates.intros)
        next
          case Stuck thus ?thesis by (auto intro: terminates.intros)
        qed
      qed
    }
    ultimately show ?thesis
      using Cons
      by (auto intro: terminates.intros)
  qed
qed

lemma terminates_sequence_appD:
  "∧s. Γ⊨sequence Seq (xs @ ys) ↓ Normal s
   ==> Γ⊨sequence Seq xs ↓ Normal s ∧
       (∀s'. Γ⊨⟨sequence Seq xs,Normal s ⟩ ==> s' ⟶ Γ⊨sequence Seq ys ↓ s')"
proof (induct xs)
  case Nil
  thus ?case
    by (auto elim: terminates_Normal_elim_cases exec_Normal_elim_cases
         intro: terminates.intros)
next
  case (Cons x xs)
  have termi_x_xs_ys: "Γ⊨sequence Seq ((x # xs) @ ys) ↓ Normal s" by fact
  show ?case
  proof (cases xs)
    case Nil
    with termi_x_xs_ys show ?thesis
      by (cases ys)
         (auto elim: terminates_Normal_elim_cases exec_Normal_elim_cases
           intro:  terminates_Skip')
  next
    case Cons
    with termi_x_xs_ys
    obtain termi_x: "Γ⊨x ↓ Normal s" and
           termi_xs_ys: "∀s'. Γ⊨⟨x,Normal s ⟩ ==> s' ⟶ Γ⊨sequence Seq (xs@ys) ↓ s'"
      by (auto elim: terminates_Normal_elim_cases)

    have "Γ⊨Seq x (sequence Seq xs) ↓ Normal s"
    proof (rule terminates.Seq [rule_format])
      show "Γ⊨x ↓ Normal s" by (rule termi_x)
    next
      fix s'
      assume exec_x: "Γ⊨⟨x,Normal s ⟩ ==> s'"
      show "Γ⊨sequence Seq xs ↓ s'"
      proof -
        from termi_xs_ys [rule_format, OF exec_x]
        have termi_xs_ys': "Γ⊨sequence Seq (xs@ys) ↓ s'" .
        show ?thesis
        proof (cases s')
          case (Normal s'')
          from Cons.hyps [OF termi_xs_ys' [simplified Normal]]
          show ?thesis
            using Normal by auto
        next
          case Abrupt thus ?thesis by (auto intro: terminates.intros)
        next
          case Fault thus ?thesis by (auto intro: terminates.intros)
        next
          case Stuck thus ?thesis by (auto intro: terminates.intros)
        qed
      qed
    qed
    moreover
    {
      fix s'
      assume exec_x_xs: "Γ⊨⟨Seq x (sequence Seq xs),Normal s ⟩ ==> s'"
      have "Γ⊨sequence Seq ys ↓ s'"
      proof -
        from exec_x_xs obtain t where
          exec_x: "Γ⊨⟨x,Normal s ⟩ ==> t" and
          exec_xs: "Γ⊨⟨sequence Seq xs,t ⟩ ==> s'"
          by cases
        show ?thesis
        proof (cases t)
          case (Normal t')
          with exec_x termi_xs_ys have "Γ⊨sequence Seq (xs@ys) ↓ Normal t'"
            by auto
          from Cons.hyps [OF this] exec_xs Normal
          show ?thesis
            by auto
        next
          case (Abrupt t')
          with exec_xs have "s'=Abrupt t'"
            by (auto dest: Abrupt_end)
          thus ?thesis by (auto intro: terminates.intros)
        next
          case (Fault f)
          with exec_xs have "s'=Fault f"
            by (auto dest: Fault_end)
          thus ?thesis by (auto intro: terminates.intros)
        next
          case Stuck
          with exec_xs have "s'=Stuck"
            by (auto dest: Stuck_end)
          thus ?thesis by (auto intro: terminates.intros)
        qed
      qed
    }
    ultimately show ?thesis
      using Cons
      by auto
  qed
qed

lemma terminates_sequence_appE [consumes 1]:
  "[Γ⊨sequence Seq (xs @ ys) ↓ Normal s;
    [Γ⊨sequence Seq xs ↓ Normal s;
     ∀s'. Γ⊨⟨sequence Seq xs,Normal s ⟩ ==> s' ⟶ Γ⊨sequence Seq ys ↓ s'] ==> P]
   ==> P"
  by (auto dest: terminates_sequence_appD)

lemma terminates_to_terminates_sequence_flatten:
  assumes termi: "Γ⊨c↓s"
  shows "Γ⊨sequence Seq (flatten c)↓s"
using termi
by (induct)
   (auto intro: terminates.intros terminates_sequence_app
     exec_sequence_flatten_to_exec)

lemma terminates_to_terminates_normalize:
  assumes termi: "Γ⊨c↓s"
  shows "Γ⊨normalize c↓s"
using termi
proof induct
  case Seq
  thus ?case
    by (fastforce intro: terminates.intros terminates_sequence_app
                 terminates_to_terminates_sequence_flatten
        dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
next
  case WhileTrue
  thus ?case
    by (fastforce intro: terminates.intros terminates_sequence_app
                 terminates_to_terminates_sequence_flatten
        dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
next
  case Catch
  thus ?case
    by (fastforce intro: terminates.intros terminates_sequence_app
                 terminates_to_terminates_sequence_flatten
        dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
qed (auto intro: terminates.intros)

lemma terminates_sequence_flatten_to_terminates:
  shows "∧s. Γ⊨sequence Seq (flatten c)↓s ==> Γ⊨c↓s"
proof (induct c)
  case (Seq c1 c2)
  have "Γ⊨sequence Seq (flatten (Seq c1 c2)) ↓ s" by fact
  hence termi_app: "Γ⊨sequence Seq (flatten c1 @ flatten c2) ↓ s" by simp
  show ?case
  proof (cases s)
    case (Normal s')
    have "Γ⊨Seq c1 c2 ↓ Normal s'"
    proof (rule terminates.Seq [rule_format])
      from termi_app [simplified Normal]
      have "Γ⊨sequence Seq (flatten c1) ↓ Normal s'"
        by (cases rule: terminates_sequence_appE)
      with Seq.hyps
      show "Γ⊨c1 ↓ Normal s'"
        by simp
    next
      fix s''
      assume "Γ⊨⟨c1,Normal s' ⟩ ==> s''"
      from termi_app [simplified Normal] exec_to_exec_sequence_flatten [OF this]
      have "Γ⊨sequence Seq (flatten c2) ↓ s''"
        by (cases rule: terminates_sequence_appE) auto
      with Seq.hyps
      show "Γ⊨c2 ↓ s''"
        by simp
    qed
    with Normal show ?thesis
      by simp
  qed (auto intro: terminates.intros)
qed (auto intro: terminates.intros)

lemma terminates_normalize_to_terminates:
  shows "∧s. Γ⊨normalize c↓s ==> Γ⊨c↓s"
proof (induct c)
  case Skip thus ?case by (auto intro:  terminates_Skip')
next
  case Basic thus ?case by (cases s) (auto intro: terminates.intros)
next
  case Spec thus ?case by (cases s) (auto intro: terminates.intros)
next
  case (Seq c1 c2)
  have "Γ⊨normalize (Seq c1 c2) ↓ s" by fact
  hence termi_app: "Γ⊨sequence Seq (flatten (normalize c1) @ flatten (normalize c2)) ↓ s"
    by simp
  show ?case
  proof (cases s)
    case (Normal s')
    have "Γ⊨Seq c1 c2 ↓ Normal s'"
    proof (rule terminates.Seq [rule_format])
      from termi_app [simplified Normal]
      have "Γ⊨sequence Seq (flatten (normalize c1)) ↓ Normal s'"
        by (cases rule: terminates_sequence_appE)
      from terminates_sequence_flatten_to_terminates [OF this] Seq.hyps
      show "Γ⊨c1 ↓ Normal s'"
        by simp
    next
      fix s''
      assume "Γ⊨⟨c1,Normal s' ⟩ ==> s''"
      from exec_to_exec_normalize [OF this]
      have "Γ⊨⟨normalize c1,Normal s' ⟩ ==> s''" .
      from termi_app [simplified Normal] exec_to_exec_sequence_flatten [OF this]
      have "Γ⊨sequence Seq (flatten (normalize c2)) ↓ s''"
        by (cases rule: terminates_sequence_appE) auto
      from terminates_sequence_flatten_to_terminates [OF this] Seq.hyps
      show "Γ⊨c2 ↓ s''"
        by simp
    qed
    with Normal show ?thesis by simp
  qed (auto intro: terminates.intros)
next
  case (Cond b c1 c2)
  thus ?case
    by (cases s)
       (auto intro: terminates.intros elim!: terminates_Normal_elim_cases)
next
  case (While b c)
  have "Γ⊨normalize (While b c) ↓ s" by fact
  hence termi_norm_w: "Γ⊨While b (normalize c) ↓ s" by simp
  {
    fix t w
    assume termi_w: "Γ⊨ w ↓ t"
    have "w=While b (normalize c) ==> Γ⊨While b c ↓ t"
      using termi_w
    proof (induct)
      case (WhileTrue t' b' c')
      from WhileTrue obtain
        t'_b: "t' ∈ b" and
        termi_norm_c: "Γ⊨normalize c ↓ Normal t'" and
        termi_norm_w': "∀s'. Γ⊨⟨normalize c,Normal t' ⟩ ==> s' ⟶ Γ⊨While b c ↓ s'"
        by auto
      from While.hyps [OF termi_norm_c]
      have "Γ⊨c ↓ Normal t'".
      moreover
      from termi_norm_w'
      have "∀s'. Γ⊨⟨c,Normal t' ⟩ ==> s' ⟶ Γ⊨While b c ↓ s'"
        by (auto intro: exec_to_exec_normalize)
      ultimately show ?case
        using t'_b
        by (auto intro: terminates.intros)
    qed (auto intro: terminates.intros)
  }
  from this [OF termi_norm_w]
  show ?case
    by auto
next
  case Call thus ?case by simp
next
  case DynCom thus ?case
    by (cases s) (auto intro: terminates.intros rangeI elim: terminates_Normal_elim_cases)
next
  case Guard thus ?case
    by (cases s) (auto intro: terminates.intros elim: terminates_Normal_elim_cases)
next
  case Throw thus ?case by (cases s) (auto intro: terminates.intros)
next
  case Catch
  thus ?case
    by (cases s)
       (auto dest: exec_to_exec_normalize elim!: terminates_Normal_elim_cases
         intro!: terminates.Catch)
qed

lemma terminates_iff_terminates_normalize:
"Γ⊨normalize c↓s = Γ⊨c↓s"
  by (auto intro: terminates_to_terminates_normalize
    terminates_normalize_to_terminates)

(* ************************************************************************* *)
subsection ‹Lemmas about @{const "strip_guards"}›
(* ************************************************************************* *)

lemma terminates_strip_guards_to_terminates: "∧s. Γ⊨strip_guards F c↓s ==> Γ⊨c↓s"
proof (induct c)
  case Skip thus ?case by simp
next
  case Basic thus ?case by simp
next
  case Spec thus ?case by simp
next
  case (Seq c1 c2)
  hence "Γ⊨Seq (strip_guards F c1) (strip_guards F c2) ↓ s" by simp
  thus "Γ⊨Seq c1 c2 ↓ s"
  proof (cases)
    fix f assume "s=Fault f" thus ?thesis by simp
  next
    assume "s=Stuck" thus ?thesis by simp
  next
    fix s' assume "s=Abrupt s'" thus ?thesis by simp
  next
    fix s'
    assume s: "s=Normal s'"
    assume "Γ⊨strip_guards F c1 ↓ Normal s'"
    hence "Γ⊨c1 ↓ Normal s'"
      by (rule Seq.hyps)
    moreover
    assume c2:
      "∀s''. Γ⊨⟨strip_guards F c1,Normal s'⟩ ==> s'' ⟶ Γ⊨strip_guards F c2↓s''"
    {
      fix s'' assume exec_c1: "Γ⊨⟨c1,Normal s' ⟩ ==> s''"
      have " Γ⊨c2 ↓ s''"
      proof (cases s'')
        case (Normal s''')
        with exec_c1
        have "Γ⊨⟨strip_guards F c1,Normal s' ⟩ ==> s''"
          by (auto intro: exec_to_exec_strip_guards)
        with c2
        show ?thesis
          by (iprover intro: Seq.hyps)
      next
        case (Abrupt s''')
        with exec_c1
        have "Γ⊨⟨strip_guards F c1,Normal s' ⟩ ==> s''"
          by (auto intro: exec_to_exec_strip_guards )
        with c2
        show ?thesis
          by (iprover intro: Seq.hyps)
      next
        case Fault thus ?thesis by simp
      next
        case Stuck thus ?thesis by simp
      qed
    }
    ultimately show ?thesis
      using s
      by (iprover intro: terminates.intros)
  qed
next
  case (Cond b c1 c2)
  hence "Γ⊨Cond b (strip_guards F c1) (strip_guards F c2) ↓ s" by simp
  thus "Γ⊨Cond b c1 c2 ↓ s"
  proof (cases)
    fix f assume "s=Fault f" thus ?thesis by simp
  next
    assume "s=Stuck" thus ?thesis by simp
  next
    fix s' assume "s=Abrupt s'" thus ?thesis by simp
  next
    fix s'
    assume "s'∈b" "Γ⊨strip_guards F c1 ↓ Normal s'" "s = Normal s'"
    thus ?thesis
      by (iprover intro: terminates.intros Cond.hyps)
  next
    fix s'
    assume "s'∉b" "Γ⊨strip_guards F c2 ↓ Normal s'" "s = Normal s'"
    thus ?thesis
      by (iprover intro: terminates.intros Cond.hyps)
  qed
next
  case (While b c)
  have hyp_c: "∧s. Γ⊨strip_guards F c ↓ s ==> Γ⊨c ↓ s" by fact
  have "Γ⊨While b (strip_guards F c) ↓ s" using While.prems by simp
  moreover
  {
    fix sw
    assume "Γ⊨sw↓s"
    then have "sw=While b (strip_guards F c) ==>
      Γ⊨While b c ↓ s"
    proof (induct)
      case (WhileTrue s b' c')
      have eqs: "While b' c' = While b (strip_guards F c)" by fact
      with ‹s∈b'› have b: "s∈b" by simp
      from eqs ‹Γ⊨c' ↓ Normal s› have "Γ⊨strip_guards F c ↓ Normal s"
        by simp
      hence term_c: "Γ⊨c ↓ Normal s"
        by (rule hyp_c)
      moreover
      {
        fix t
        assume exec_c: "Γ⊨⟨c,Normal s ⟩ ==> t"
        have "Γ⊨While b c ↓ t"
        proof (cases t)
          case Fault
          thus ?thesis by simp
        next
          case Stuck
          thus ?thesis by simp
        next
          case (Abrupt t')
          thus ?thesis by simp
        next
          case (Normal t')
          with exec_c
          have "Γ⊨⟨strip_guards F c,Normal s ⟩ ==> Normal t'"
            by (auto intro: exec_to_exec_strip_guards)
          with WhileTrue.hyps eqs Normal
          show ?thesis
            by fastforce
        qed
      }
      ultimately
      show ?case
        using b
        by (auto intro: terminates.intros)
    next
      case WhileFalse thus ?case by (auto intro: terminates.intros)
    qed simp_all
  }
  ultimately show "Γ⊨While b c ↓ s"
    by auto
next
  case Call thus ?case by simp
next
  case DynCom thus ?case
     by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros rangeI)
next
  case Guard
  thus ?case
    by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros
                  split: if_split_asm)
next
  case Throw thus ?case by simp
next
  case (Catch c1 c2)
  hence "Γ⊨Catch (strip_guards F c1) (strip_guards F c2) ↓ s" by simp
  thus "Γ⊨Catch c1 c2 ↓ s"
  proof (cases)
    fix f assume "s=Fault f" thus ?thesis by simp
  next
    assume "s=Stuck" thus ?thesis by simp
  next
    fix s' assume "s=Abrupt s'" thus ?thesis by simp
  next
    fix s'
    assume s: "s=Normal s'"
    assume "Γ⊨strip_guards F c1 ↓ Normal s'"
    hence "Γ⊨c1 ↓ Normal s'"
      by (rule Catch.hyps)
    moreover
    assume c2:
      "∀s''. Γ⊨⟨strip_guards F c1,Normal s'⟩ ==> Abrupt s''
             ⟶ Γ⊨strip_guards F c2↓Normal s''"
    {
      fix s'' assume exec_c1: "Γ⊨⟨c1,Normal s' ⟩ ==> Abrupt s''"
      have " Γ⊨c2 ↓ Normal s''"
      proof -
        from exec_c1
        have "Γ⊨⟨strip_guards F c1,Normal s' ⟩ ==> Abrupt s''"
          by (auto intro: exec_to_exec_strip_guards)
        with c2
        show ?thesis
          by (auto intro: Catch.hyps)
      qed
    }
    ultimately show ?thesis
      using s
      by (iprover intro: terminates.intros)
  qed
qed

lemma terminates_strip_to_terminates:
  assumes termi_strip: "strip F Γ⊨c↓s"
  shows "Γ⊨c↓s"
using termi_strip
proof induct
  case (Seq c1 s c2)
  have "Γ⊨c1 ↓ Normal s" by fact
  moreover
  {
    fix s'
    assume exec: "Γ⊨ ⟨c1,Normal s⟩ ==> s'"
    have "Γ⊨c2 ↓ s'"
    proof (cases "isFault s'")
      case True
      thus ?thesis
        by (auto elim: isFaultE)
    next
      case False
      from exec_to_exec_strip [OF exec this] Seq.hyps
      show ?thesis
        by auto
    qed
  }
  ultimately show ?case
    by (auto intro: terminates.intros)
next
  case (WhileTrue s b c)
  have "Γ⊨c ↓ Normal s" by fact
  moreover
  {
    fix s'
    assume exec: "Γ⊨ ⟨c,Normal s⟩ ==> s'"
    have "Γ⊨While b c ↓ s'"
    proof (cases "isFault s'")
      case True
      thus ?thesis
        by (auto elim: isFaultE)
    next
      case False
      from exec_to_exec_strip [OF exec this] WhileTrue.hyps
      show ?thesis
        by auto
    qed
  }
  ultimately show ?case
    by (auto intro: terminates.intros)
next
  case (Catch c1 s c2)
  have "Γ⊨c1 ↓ Normal s" by fact
  moreover
  {
    fix s'
    assume exec: "Γ⊨ ⟨c1,Normal s⟩ ==> Abrupt s'"
    from exec_to_exec_strip [OF exec] Catch.hyps
    have "Γ⊨c2 ↓ Normal s'"
      by auto
  }
  ultimately show ?case
    by (auto intro: terminates.intros)
next
  case Call thus ?case
    by (auto intro: terminates.intros terminates_strip_guards_to_terminates)
qed (auto intro: terminates.intros)

(* ************************************************************************* *)
subsection ‹Lemmas about @{term "c₁ ∩_g c₂"}›
(* ************************************************************************* *)

lemma inter_guards_terminates:
  "∧c c2 s. [(c1 ∩_g c2) = Some c; Γ⊨c1↓s ]
        ==> Γ⊨c↓s"
proof (induct c1)
  case Skip thus ?case by (fastforce simp add: inter_guards_Skip)
next
  case (Basic f) thus ?case by (fastforce simp add: inter_guards_Basic)
next
  case (Spec r) thus ?case by (fastforce simp add: inter_guards_Spec)
next
  case (Seq a1 a2)
  have "(Seq a1 a2 ∩_g c2) = Some c" by fact
  then obtain b1 b2 d1 d2 where
    c2: "c2=Seq b1 b2" and
    d1: "(a1 ∩_g b1) = Some d1" and d2: "(a2 ∩_g b2) = Some d2" and
    c: "c=Seq d1 d2"
    by (auto simp add: inter_guards_Seq)
  have termi_c1: "Γ⊨Seq a1 a2 ↓ s" by fact
  have "Γ⊨Seq d1 d2 ↓ s"
  proof (cases s)
    case Fault thus ?thesis by simp
  next
    case Stuck thus ?thesis by simp
  next
    case Abrupt thus ?thesis by simp
  next
    case (Normal s')
    note Normal_s = this
    with d1 termi_c1
    have "Γ⊨d1 ↓ Normal s'"
      by (auto elim: terminates_Normal_elim_cases intro: Seq.hyps)
    moreover
    {
      fix t
      assume exec_d1: "Γ⊨⟨d1,Normal s' ⟩ ==> t"
      have "Γ⊨d2 ↓ t"
      proof (cases t)
        case Fault thus ?thesis by simp
      next
        case Stuck thus ?thesis by simp
      next
        case Abrupt thus ?thesis by simp
      next
        case (Normal t')
        with inter_guards_exec_noFault [OF d1 exec_d1]
        have "Γ⊨⟨a1,Normal s' ⟩ ==> Normal t'"
          by simp
        with termi_c1 Normal_s have "Γ⊨a2 ↓ Normal t'"
          by (auto elim: terminates_Normal_elim_cases)
        with d2 have "Γ⊨d2 ↓ Normal t'"
          by (auto intro: Seq.hyps)
        with Normal show ?thesis by simp
      qed
    }
    ultimately have "Γ⊨Seq d1 d2 ↓ Normal s'"
      by (fastforce intro: terminates.intros)
    with Normal show ?thesis by simp
  qed
  with c show ?case by simp
next
  case Cond thus ?case
    by - (cases s,
          auto intro: terminates.intros elim!: terminates_Normal_elim_cases
               simp add: inter_guards_Cond)
next
  case (While b bdy1)
  have "(While b bdy1 ∩_g c2) = Some c" by fact
  then obtain bdy2 bdy where
    c2: "c2=While b bdy2" and
    bdy: "(bdy1 ∩_g bdy2) = Some bdy" and
    c: "c=While b bdy"
    by (auto simp add: inter_guards_While)
  have "Γ⊨While b bdy1 ↓ s" by fact
  moreover
  {
    fix s w w1 w2
    assume termi_w:  "Γ⊨w ↓ s"
    assume w: "w=While b bdy1"
    from termi_w w
    have "Γ⊨While b bdy ↓ s"
    proof (induct)
      case (WhileTrue s b' bdy1')
      have eqs: "While b' bdy1' = While b bdy1" by fact
      from WhileTrue have s_in_b: "s ∈ b" by simp
      from WhileTrue have termi_bdy1: "Γ⊨bdy1 ↓ Normal s" by simp
      show ?case
      proof -
        from bdy termi_bdy1
        have "Γ⊨bdy↓(Normal s)"
          by (rule While.hyps)
        moreover
        {
          fix t
          assume exec_bdy: "Γ⊨⟨bdy,Normal s ⟩ ==> t"
          have "Γ⊨While b bdy↓t"
          proof (cases t)
            case Fault thus ?thesis by simp
          next
            case Stuck thus ?thesis by simp
          next
            case Abrupt thus ?thesis by simp
          next
            case (Normal t')
            with inter_guards_exec_noFault [OF bdy exec_bdy]
            have "Γ⊨⟨bdy1,Normal s ⟩ ==> Normal t'"
              by simp
            with WhileTrue have "Γ⊨While b bdy ↓ Normal t'"
              by simp
            with Normal show ?thesis by simp
          qed
        }
        ultimately show ?thesis
          using s_in_b
          by (blast intro: terminates.WhileTrue)
      qed
    next
      case WhileFalse thus ?case
        by (blast intro: terminates.WhileFalse)
    qed (simp_all)
  }
  ultimately
  show ?case using c by simp
next
  case Call thus ?case by (simp add: inter_guards_Call)
next
  case (DynCom f1)
  have "(DynCom f1 ∩_g c2) = Some c" by fact
  then obtain f2 f where
    c2: "c2=DynCom f2" and
    f_defined: "∀s. ((f1 s) ∩_g (f2 s)) ≠ None" and
    c: "c=DynCom (λs. the ((f1 s) ∩_g (f2 s)))"
    by (auto simp add: inter_guards_DynCom)
  have termi: "Γ⊨DynCom f1 ↓ s" by fact
  show ?case
  proof (cases s)
    case Fault thus ?thesis by simp
  next
    case Stuck thus ?thesis by simp
  next
    case Abrupt thus ?thesis by simp
  next
    case (Normal s')
    from f_defined obtain f where f: "((f1 s') ∩_g (f2 s')) = Some f"
      by auto
    from Normal termi
    have "Γ⊨f1 s'↓ (Normal s')"
      by (auto elim: terminates_Normal_elim_cases)
    from DynCom.hyps f this
    have "Γ⊨f↓ (Normal s')"
      by blast
    with c f Normal
    show ?thesis
      by (auto intro: terminates.intros)
  qed
next
  case (Guard f g1 bdy1)
  have "(Guard f g1 bdy1 ∩_g c2) = Some c" by fact
  then obtain g2 bdy2 bdy where
    c2: "c2=Guard f g2 bdy2" and
    bdy: "(bdy1 ∩_g bdy2) = Some bdy" and
    c: "c=Guard f (g1 ∩ g2) bdy"
    by (auto simp add: inter_guards_Guard)
  have termi_c1: "Γ⊨Guard f g1 bdy1 ↓ s" by fact
  show ?case
  proof (cases s)
    case Fault thus ?thesis by simp
  next
    case Stuck thus ?thesis by simp
  next
    case Abrupt thus ?thesis by simp
  next
    case (Normal s')
    show ?thesis
    proof (cases "s' ∈ g1")
      case False
      with Normal c show ?thesis by (auto intro: terminates.GuardFault)
    next
      case True
      note s_in_g1 = this
      show ?thesis
      proof (cases "s' ∈ g2")
        case False
        with Normal c show ?thesis by (auto intro: terminates.GuardFault)
      next
        case True
        with termi_c1 s_in_g1 Normal have "Γ⊨bdy1 ↓ Normal s'"
          by (auto elim: terminates_Normal_elim_cases)
        with c bdy Guard.hyps Normal True s_in_g1
        show ?thesis by (auto intro: terminates.Guard)
      qed
    qed
  qed
next
  case Throw thus ?case
    by (auto simp add: inter_guards_Throw)
next
  case (Catch a1 a2)
  have "(Catch a1 a2 ∩_g c2) = Some c" by fact
  then obtain b1 b2 d1 d2 where
    c2: "c2=Catch b1 b2" and
    d1: "(a1 ∩_g b1) = Some d1" and d2: "(a2 ∩_g b2) = Some d2" and
    c: "c=Catch d1 d2"
    by (auto simp add: inter_guards_Catch)
  have termi_c1: "Γ⊨Catch a1 a2 ↓ s" by fact
  have "Γ⊨Catch d1 d2 ↓ s"
  proof (cases s)
    case Fault thus ?thesis by simp
  next
    case Stuck thus ?thesis by simp
  next
    case Abrupt thus ?thesis by simp
  next
    case (Normal s')
    note Normal_s = this
    with d1 termi_c1
    have "Γ⊨d1 ↓ Normal s'"
      by (auto elim: terminates_Normal_elim_cases intro: Catch.hyps)
    moreover
    {
      fix t
      assume exec_d1: "Γ⊨⟨d1,Normal s' ⟩ ==> Abrupt t"
      have "Γ⊨d2 ↓ Normal t"
      proof -
        from inter_guards_exec_noFault [OF d1 exec_d1]
        have "Γ⊨⟨a1,Normal s' ⟩ ==> Abrupt t"
          by simp
        with termi_c1 Normal_s have "Γ⊨a2 ↓ Normal t"
          by (auto elim: terminates_Normal_elim_cases)
        with d2 have "Γ⊨d2 ↓ Normal t"
          by (auto intro: Catch.hyps)
        with Normal show ?thesis by simp
      qed
    }
    ultimately have "Γ⊨Catch d1 d2 ↓ Normal s'"
      by (fastforce intro: terminates.intros)
    with Normal show ?thesis by simp
  qed
  with c show ?case by simp
qed

lemma inter_guards_terminates':
  assumes c: "(c1 ∩_g c2) = Some c"
  assumes termi_c2: "Γ⊨c2↓s"
  shows "Γ⊨c↓s"
proof -
  from c have "(c2 ∩_g c1) = Some c"
    by (rule inter_guards_sym)
  from this termi_c2 show ?thesis
    by (rule inter_guards_terminates)
qed

(* ************************************************************************* *)
subsection ‹Lemmas about @{const "mark_guards"}›
(* ************************************************************************ *)

lemma terminates_to_terminates_mark_guards:
  assumes termi: "Γ⊨c↓s"
  shows "Γ⊨mark_guards f c↓s"
using termi
proof (induct)
  case Skip thus ?case by (fastforce intro: terminates.intros)
next
  case Basic thus ?case by (fastforce intro: terminates.intros)
next
  case Spec thus ?case by (fastforce intro: terminates.intros)
next
  case Guard thus ?case by (fastforce intro: terminates.intros)
next
  case GuardFault thus ?case by (fastforce intro: terminates.intros)
next
  case Fault thus ?case by (fastforce intro: terminates.intros)
next
  case (Seq c1 s c2)
  have "Γ⊨mark_guards f c1 ↓ Normal s" by fact
  moreover
  {
    fix t
    assume exec_mark: "Γ⊨⟨mark_guards f c1,Normal s ⟩ ==> t"
    have "Γ⊨mark_guards f c2 ↓ t"
    proof -
      from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
        exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> t'" and
        t_Fault: "isFault t ⟶ isFault t'" and
        t'_Fault_f: "t' = Fault f ⟶ t' = t" and
        t'_Fault: "isFault t' ⟶ isFault t" and
        t'_noFault: "¬ isFault t' ⟶ t' = t"
        by blast
      show ?thesis
      proof (cases "isFault t'")
        case True
        with t'_Fault have "isFault t" by simp
        thus ?thesis
          by (auto elim: isFaultE)
      next
        case False
        with t'_noFault have "t'=t" by simp
        with exec_c1 Seq.hyps
        show ?thesis
          by auto
      qed
    qed
  }
  ultimately show ?case
    by (auto intro: terminates.intros)
next
  case CondTrue thus ?case by (fastforce intro: terminates.intros)
next
  case CondFalse thus ?case by (fastforce intro: terminates.intros)
next
  case (WhileTrue s b c)
  have s_in_b: "s ∈ b" by fact
  have "Γ⊨mark_guards f c ↓ Normal s" by fact
  moreover
  {
    fix t
    assume exec_mark: "Γ⊨⟨mark_guards f c,Normal s ⟩ ==> t"
    have "Γ⊨mark_guards f (While b c) ↓ t"
    proof -
      from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
        exec_c1: "Γ⊨⟨c,Normal s ⟩ ==> t'" and
        t_Fault: "isFault t ⟶ isFault t'" and
        t'_Fault_f: "t' = Fault f ⟶ t' = t" and
        t'_Fault: "isFault t' ⟶ isFault t" and
        t'_noFault: "¬ isFault t' ⟶ t' = t"
        by blast
      show ?thesis
      proof (cases "isFault t'")
        case True
        with t'_Fault have "isFault t" by simp
        thus ?thesis
          by (auto elim: isFaultE)
      next
        case False
        with t'_noFault have "t'=t" by simp
        with exec_c1 WhileTrue.hyps
        show ?thesis
          by auto
      qed
    qed
  }
  ultimately show ?case
    by (auto intro: terminates.intros)
next
  case WhileFalse thus ?case by (fastforce intro: terminates.intros)
next
  case Call thus ?case by (fastforce intro: terminates.intros)
next
  case CallUndefined thus ?case by (fastforce intro: terminates.intros)
next
  case Stuck thus ?case by (fastforce intro: terminates.intros)
next
  case DynCom thus ?case by (fastforce intro: terminates.intros)
next
  case Throw thus ?case by (fastforce intro: terminates.intros)
next
  case Abrupt thus ?case by (fastforce intro: terminates.intros)
next
  case (Catch c1 s c2)
  have "Γ⊨mark_guards f c1 ↓ Normal s" by fact
  moreover
  {
    fix t
    assume exec_mark: "Γ⊨⟨mark_guards f c1,Normal s ⟩ ==> Abrupt t"
    have "Γ⊨mark_guards f c2 ↓ Normal t"
    proof -
      from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
        exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> t'" and
        t'_Fault_f: "t' = Fault f ⟶ t' = Abrupt t" and
        t'_Fault: "isFault t' ⟶ isFault (Abrupt t)" and
        t'_noFault: "¬ isFault t' ⟶ t' = Abrupt t"
        by fastforce
      show ?thesis
      proof (cases "isFault t'")
        case True
        with t'_Fault have "isFault (Abrupt t)" by simp
        thus ?thesis by simp
      next
        case False
        with t'_noFault have "t'=Abrupt t" by simp
        with exec_c1 Catch.hyps
        show ?thesis
          by auto
      qed
    qed
  }
  ultimately show ?case
    by (auto intro: terminates.intros)
qed

lemma terminates_mark_guards_to_terminates_Normal:
  "∧s. Γ⊨mark_guards f c↓Normal s ==> Γ⊨c↓Normal s"
proof (induct c)
  case Skip thus ?case by (fastforce intro: terminates.intros)
next
  case Basic thus ?case by (fastforce intro: terminates.intros)
next
  case Spec thus ?case by (fastforce intro: terminates.intros)
next
  case (Seq c1 c2)
  have "Γ⊨mark_guards f (Seq c1 c2) ↓ Normal s" by fact
  then obtain
    termi_merge_c1: "Γ⊨mark_guards f c1 ↓ Normal s" and
    termi_merge_c2: "∀s'. Γ⊨⟨mark_guards f c1,Normal s ⟩ ==> s' ⟶
                           Γ⊨mark_guards f c2 ↓ s'"
    by (auto elim: terminates_Normal_elim_cases)
  from termi_merge_c1 Seq.hyps
  have "Γ⊨c1 ↓ Normal s" by iprover
  moreover
  {
    fix s'
    assume exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> s'"
    have "Γ⊨ c2 ↓ s'"
    proof (cases "isFault s'")
      case True
      thus ?thesis by (auto elim: isFaultE)
    next
      case False
      from exec_to_exec_mark_guards [OF exec_c1 False]
      have "Γ⊨⟨mark_guards f c1,Normal s ⟩ ==> s'" .
      from termi_merge_c2 [rule_format, OF this] Seq.hyps
      show ?thesis
        by (cases s') (auto)
    qed
  }
  ultimately show ?case by (auto intro: terminates.intros)
next
  case Cond thus ?case
    by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
  case (While b c)
  {
    fix u c'
    assume termi_c': "Γ⊨c' ↓ Normal u"
    assume c': "c' = mark_guards f (While b c)"
    have "Γ⊨While b c ↓ Normal u"
      using termi_c' c'
    proof (induct)
      case (WhileTrue s b' c')
      have s_in_b: "s ∈ b" using WhileTrue by simp
      have "Γ⊨mark_guards f c ↓ Normal s"
        using WhileTrue by (auto elim: terminates_Normal_elim_cases)
      with While.hyps have "Γ⊨c ↓ Normal s"
        by auto
      moreover
      have hyp_w: "∀w. Γ⊨⟨mark_guards f c,Normal s ⟩ ==> w ⟶ Γ⊨While b c ↓ w"
        using WhileTrue by simp
      hence "∀w. Γ⊨⟨c,Normal s ⟩ ==> w ⟶ Γ⊨While b c ↓ w"
        apply -
        apply (rule allI)
        apply (case_tac "w")
        apply (auto dest: exec_to_exec_mark_guards)
        done
      ultimately show ?case
        using s_in_b
        by (auto intro: terminates.intros)
    next
      case WhileFalse thus ?case by (auto intro: terminates.intros)
    qed auto
  }
  with While show ?case by simp
next
  case Call thus ?case
    by (fastforce intro: terminates.intros )
next
  case DynCom thus ?case
    by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
  case (Guard f g c)
  thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
  case Throw thus ?case
    by (fastforce intro: terminates.intros )
next
  case (Catch c1 c2)
  have "Γ⊨mark_guards f (Catch c1 c2) ↓ Normal s" by fact
  then obtain
    termi_merge_c1: "Γ⊨mark_guards f c1 ↓ Normal s" and
    termi_merge_c2: "∀s'. Γ⊨⟨mark_guards f c1,Normal s ⟩ ==> Abrupt s' ⟶
                           Γ⊨mark_guards f c2 ↓ Normal s'"
    by (auto elim: terminates_Normal_elim_cases)
  from termi_merge_c1 Catch.hyps
  have "Γ⊨c1 ↓ Normal s" by iprover
  moreover
  {
    fix s'
    assume exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> Abrupt s'"
    have "Γ⊨ c2 ↓ Normal s'"
    proof -
      from exec_to_exec_mark_guards [OF exec_c1]
      have "Γ⊨⟨mark_guards f c1,Normal s ⟩ ==> Abrupt s'" by simp
      from termi_merge_c2 [rule_format, OF this] Catch.hyps
      show ?thesis
        by iprover
    qed
  }
  ultimately show ?case by (auto intro: terminates.intros)
qed

lemma terminates_mark_guards_to_terminates:
  "Γ⊨mark_guards f c↓s ==> Γ⊨c↓ s"
  by (cases s) (auto intro: terminates_mark_guards_to_terminates_Normal)


(* ************************************************************************* *)
subsection ‹Lemmas about @{const "merge_guards"}›
(* ************************************************************************ *)

lemma terminates_to_terminates_merge_guards:
  assumes termi: "Γ⊨c↓s"
  shows "Γ⊨merge_guards c↓s"
using termi
proof (induct)
  case (Guard s g c f)
  have s_in_g: "s ∈ g" by fact
  have termi_merge_c: "Γ⊨merge_guards c ↓ Normal s" by fact
  show ?case
  proof (cases "∃f' g' c'. merge_guards c = Guard f' g' c'")
    case False
    hence "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
      by (cases "merge_guards c") (auto simp add: Let_def)
    with s_in_g termi_merge_c show ?thesis
      by (auto intro: terminates.intros)
  next
    case True
    then obtain f' g' c' where
      mc: "merge_guards c = Guard f' g' c'"
      by blast
    show ?thesis
    proof (cases "f=f'")
      case False
      with mc have "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
        by (simp add: Let_def)
      with s_in_g termi_merge_c show ?thesis
        by (auto intro: terminates.intros)
    next
      case True
      with mc have "merge_guards (Guard f g c) = Guard f (g ∩ g') c'"
        by simp
      with s_in_g mc True termi_merge_c
      show ?thesis
        by (cases "s ∈ g'")
           (auto intro: terminates.intros elim: terminates_Normal_elim_cases)
    qed
  qed
next
  case (GuardFault s g f c)
  have "s ∉ g" by fact
  thus ?case
    by (cases "merge_guards c")
       (auto intro: terminates.intros split: if_split_asm simp add: Let_def)
qed (fastforce intro: terminates.intros dest: exec_merge_guards_to_exec)+

lemma terminates_merge_guards_to_terminates_Normal:
  shows "∧s. Γ⊨merge_guards c↓Normal s ==> Γ⊨c↓Normal s"
proof (induct c)
  case Skip thus ?case by (fastforce intro: terminates.intros)
next
  case Basic thus ?case by (fastforce intro: terminates.intros)
next
  case Spec thus ?case by (fastforce intro: terminates.intros)
next
  case (Seq c1 c2)
  have "Γ⊨merge_guards (Seq c1 c2) ↓ Normal s" by fact
  then obtain
    termi_merge_c1: "Γ⊨merge_guards c1 ↓ Normal s" and
    termi_merge_c2: "∀s'. Γ⊨⟨merge_guards c1,Normal s ⟩ ==> s' ⟶
                           Γ⊨merge_guards c2 ↓ s'"
    by (auto elim: terminates_Normal_elim_cases)
  from termi_merge_c1 Seq.hyps
  have "Γ⊨c1 ↓ Normal s" by iprover
  moreover
  {
    fix s'
    assume exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> s'"
    have "Γ⊨ c2 ↓ s'"
    proof -
      from exec_to_exec_merge_guards [OF exec_c1]
      have "Γ⊨⟨merge_guards c1,Normal s ⟩ ==> s'" .
      from termi_merge_c2 [rule_format, OF this] Seq.hyps
      show ?thesis
        by (cases s') (auto)
    qed
  }
  ultimately show ?case by (auto intro: terminates.intros)
next
  case Cond thus ?case
    by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
  case (While b c)
  {
    fix u c'
    assume termi_c': "Γ⊨c' ↓ Normal u"
    assume c': "c' = merge_guards (While b c)"
    have "Γ⊨While b c ↓ Normal u"
      using termi_c' c'
    proof (induct)
      case (WhileTrue s b' c')
      have s_in_b: "s ∈ b" using WhileTrue by simp
      have "Γ⊨merge_guards c ↓ Normal s"
        using WhileTrue by (auto elim: terminates_Normal_elim_cases)
      with While.hyps have "Γ⊨c ↓ Normal s"
        by auto
      moreover
      have hyp_w: "∀w. Γ⊨⟨merge_guards c,Normal s ⟩ ==> w ⟶ Γ⊨While b c ↓ w"
        using WhileTrue by simp
      hence "∀w. Γ⊨⟨c,Normal s ⟩ ==> w ⟶ Γ⊨While b c ↓ w"
        by (simp add: exec_iff_exec_merge_guards [symmetric])
      ultimately show ?case
        using s_in_b
        by (auto intro: terminates.intros)
    next
      case WhileFalse thus ?case by (auto intro: terminates.intros)
    qed auto
  }
  with While show ?case by simp
next
  case Call thus ?case
    by (fastforce intro: terminates.intros )
next
  case DynCom thus ?case
    by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
  case (Guard f g c)
  have termi_merge: "Γ⊨merge_guards (Guard f g c) ↓ Normal s" by fact
  show ?case
  proof (cases "∃f' g' c'. merge_guards c = Guard f' g' c'")
    case False
    hence m: "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
      by (cases "merge_guards c") (auto simp add: Let_def)
    from termi_merge Guard.hyps show ?thesis
      by (simp only: m)
         (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
  next
    case True
    then obtain f' g' c' where
      mc: "merge_guards c = Guard f' g' c'"
      by blast
    show ?thesis
    proof (cases "f=f'")
      case False
      with mc have m: "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
        by (simp add: Let_def)
      from termi_merge Guard.hyps show ?thesis
      by (simp only: m)
         (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
    next
      case True
      with mc have m: "merge_guards (Guard f g c) = Guard f (g ∩ g') c'"
        by simp
      from termi_merge Guard.hyps
      show ?thesis
        by (simp only: m mc)
           (auto intro: terminates.intros elim: terminates_Normal_elim_cases)
    qed
  qed
next
  case Throw thus ?case
    by (fastforce intro: terminates.intros )
next
  case (Catch c1 c2)
  have "Γ⊨merge_guards (Catch c1 c2) ↓ Normal s" by fact
  then obtain
    termi_merge_c1: "Γ⊨merge_guards c1 ↓ Normal s" and
    termi_merge_c2: "∀s'. Γ⊨⟨merge_guards c1,Normal s ⟩ ==> Abrupt s' ⟶
                           Γ⊨merge_guards c2 ↓ Normal s'"
    by (auto elim: terminates_Normal_elim_cases)
  from termi_merge_c1 Catch.hyps
  have "Γ⊨c1 ↓ Normal s" by iprover
  moreover
  {
    fix s'
    assume exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> Abrupt s'"
    have "Γ⊨ c2 ↓ Normal s'"
    proof -
      from exec_to_exec_merge_guards [OF exec_c1]
      have "Γ⊨⟨merge_guards c1,Normal s ⟩ ==> Abrupt s'" .
      from termi_merge_c2 [rule_format, OF this] Catch.hyps
      show ?thesis
        by iprover
    qed
  }
  ultimately show ?case by (auto intro: terminates.intros)
qed

lemma terminates_merge_guards_to_terminates:
   "Γ⊨merge_guards c↓ s ==> Γ⊨c↓ s"
by (cases s) (auto intro: terminates_merge_guards_to_terminates_Normal)

theorem terminates_iff_terminates_merge_guards:
  "Γ⊨c↓ s = Γ⊨merge_guards c↓ s"
  by (iprover intro: terminates_to_terminates_merge_guards
    terminates_merge_guards_to_terminates)

(* ************************************************************************* *)
subsection ‹Lemmas about @{term "c₁ ⊆_g c₂"}›
(* ************************************************************************ *)

lemma terminates_fewer_guards_Normal:
  shows "∧c s. [Γ⊨c'↓Normal s; c ⊆_g c'; Γ⊨⟨c',Normal s ⟩ ==>∉Fault ` UNIV]
              ==> Γ⊨c↓Normal s"
proof (induct c')
  case Skip thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
  case Basic thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
  case Spec thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
  case (Seq c1' c2')
  have termi: "Γ⊨Seq c1' c2' ↓ Normal s" by fact
  then obtain
    termi_c1': "Γ⊨c1'↓ Normal s" and
    termi_c2': "∀s'. Γ⊨⟨c1',Normal s ⟩ ==> s' ⟶ Γ⊨c2'↓ s'"
    by (auto elim: terminates_Normal_elim_cases)
  have noFault: "Γ⊨⟨Seq c1' c2',Normal s ⟩ ==>∉Fault ` UNIV" by fact
  hence noFault_c1': "Γ⊨⟨c1',Normal s ⟩ ==>∉Fault ` UNIV"
    by (auto intro: exec.intros simp add: final_notin_def)
  have "c ⊆<sub>g</sub> Seq c1' c2'" by fact
  from subseteq_guards_Seq [OF this] obtain c1 c2 where
    c: "c = Seq c1 c2" and
    c1_c1': "c1 ⊆<sub>g</sub> c1'" and
    c2_c2': "c2 ⊆<sub>g</sub> c2'"
    by blast
  from termi_c1' c1_c1' noFault_c1'
  have "Γ⊨c1↓ Normal s"
    by (rule Seq.hyps)
  moreover
  {
    fix t
    assume exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> t"
    have "Γ⊨c2↓ t"
    proof -
      from exec_to_exec_subseteq_guards [OF c1_c1' exec_c1] obtain t' where
        exec_c1': "Γ⊨⟨c1',Normal s ⟩ ==> t'" and
        t_Fault: "isFault t ⟶ isFault t'" and
        t'_noFault: "¬ isFault t' ⟶ t' = t"
        by blast
      show ?thesis
      proof (cases "isFault t'")
        case True
        with exec_c1' noFault_c1'
        have False
          by (fastforce elim: isFaultE dest: Fault_end simp add: final_notin_def)
        thus ?thesis ..
      next
        case False
        with t'_noFault have t': "t'=t" by simp
        with termi_c2' exec_c1'
        have termi_c2': "Γ⊨c2'↓ t"
          by auto
        show ?thesis
        proof (cases t)
          case Fault thus ?thesis by auto
        next
          case Abrupt thus ?thesis by auto
        next
          case Stuck thus ?thesis by auto
        next
          case (Normal u)
          with noFault exec_c1' t'
          have "Γ⊨⟨c2',Normal u ⟩ ==>∉Fault ` UNIV"
            by (auto intro: exec.intros simp add: final_notin_def)
          from termi_c2' [simplified Normal] c2_c2' this
          have "Γ⊨c2 ↓ Normal u"
            by (rule Seq.hyps)
          with Normal exec_c1
          show ?thesis by simp
        qed
      qed
    qed
  }
  ultimately show ?case using c by (auto intro: terminates.intros)
next
  case (Cond b c1' c2')
  have noFault: "Γ⊨⟨Cond b c1' c2',Normal s ⟩ ==>∉Fault ` UNIV" by fact
  have termi: "Γ⊨Cond b c1' c2' ↓ Normal s" by fact
  have "c ⊆<sub>g</sub> Cond b c1' c2'" by fact
  from subseteq_guards_Cond [OF this] obtain c1 c2 where
    c: "c = Cond b c1 c2" and
    c1_c1': "c1 ⊆<sub>g</sub> c1'" and
    c2_c2': "c2 ⊆<sub>g</sub> c2'"
    by blast
  thus ?case
  proof (cases "s ∈ b")
    case True
    with termi have termi_c1': "Γ⊨c1' ↓ Normal s"
      by (auto elim: terminates_Normal_elim_cases)
    from True noFault have "Γ⊨⟨c1',Normal s ⟩ ==>∉Fault ` UNIV"
      by (auto intro: exec.intros simp add: final_notin_def)
    from termi_c1' c1_c1' this
    have "Γ⊨c1 ↓ Normal s"
      by (rule Cond.hyps)
    with True c show ?thesis
      by (auto intro: terminates.intros)
  next
    case False
    with termi have termi_c2': "Γ⊨c2' ↓ Normal s"
      by (auto elim: terminates_Normal_elim_cases)
    from False noFault have "Γ⊨⟨c2',Normal s ⟩ ==>∉Fault ` UNIV"
      by (auto intro: exec.intros simp add: final_notin_def)
    from termi_c2' c2_c2' this
    have "Γ⊨c2 ↓ Normal s"
      by (rule Cond.hyps)
    with False c show ?thesis
      by (auto intro: terminates.intros)
  qed
next
  case (While b c')
  have noFault: "Γ⊨⟨While b c',Normal s ⟩ ==>∉Fault ` UNIV" by fact
  have termi: "Γ⊨While b c' ↓ Normal s" by fact
  have "c ⊆_g While b c'" by fact
  from subseteq_guards_While [OF this]
  obtain c'' where
    c: "c = While b c''" and
    c''_c': "c'' ⊆_g c'"
    by blast
  {
    fix d u
    assume termi: "Γ⊨d ↓ u"
    assume d: "d = While b c'"
    assume noFault: "Γ⊨⟨While b c',u ⟩ ==>∉Fault ` UNIV"
    have "Γ⊨While b c'' ↓ u"
    using termi d noFault
    proof (induct)
      case (WhileTrue u b' c''')
      have u_in_b: "u ∈ b" using WhileTrue by simp
      have termi_c': "Γ⊨c' ↓ Normal u" using WhileTrue by simp
      have noFault: "Γ⊨⟨While b c',Normal u ⟩ ==>∉Fault ` UNIV" using WhileTrue by simp
      hence noFault_c': "Γ⊨⟨c',Normal u ⟩ ==>∉Fault ` UNIV" using u_in_b
        by (auto intro: exec.intros simp add: final_notin_def)
      from While.hyps [OF termi_c' c''_c' this]
      have "Γ⊨c'' ↓ Normal u".
      moreover
      from WhileTrue
      have hyp_w: "∀s'. Γ⊨⟨c',Normal u ⟩ ==> s' ⟶ Γ⊨⟨While b c',s' ⟩ ==>∉Fault ` UNIV
                        ⟶ Γ⊨While b c'' ↓ s'"
        by simp
      {
        fix v
        assume exec_c'': "Γ⊨⟨c'',Normal u ⟩ ==> v"
        have "Γ⊨While b c'' ↓ v"
        proof -
          from exec_to_exec_subseteq_guards [OF c''_c' exec_c''] obtain v' where
            exec_c': "Γ⊨⟨c',Normal u ⟩ ==> v'" and
            v_Fault: "isFault v ⟶ isFault v'" and
            v'_noFault: "¬ isFault v' ⟶ v' = v"
            by auto
          show ?thesis
          proof (cases "isFault v'")
            case True
            with exec_c' noFault u_in_b
            have False
              by (fastforce
                   simp add: final_notin_def intro: exec.intros elim: isFaultE)
            thus ?thesis ..
          next
            case False
            with v'_noFault have v': "v'=v"
              by simp
            with noFault exec_c' u_in_b
            have "Γ⊨⟨While b c',v ⟩ ==>∉Fault ` UNIV"
              by (fastforce simp add: final_notin_def intro: exec.intros)
            from hyp_w [rule_format, OF exec_c' [simplified v'] this]
            show "Γ⊨While b c'' ↓ v" .
          qed
        qed
      }
      ultimately
      show ?case using u_in_b
        by (auto intro: terminates.intros)
    next
      case WhileFalse thus ?case by (auto intro: terminates.intros)
    qed auto
  }
  with c noFault termi show ?case
    by auto
next
  case Call thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
  case (DynCom C')
  have termi: "Γ⊨DynCom C' ↓ Normal s" by fact
  hence termi_C': "Γ⊨C' s ↓ Normal s"
    by cases
  have noFault: "Γ⊨⟨DynCom C',Normal s ⟩ ==>∉Fault ` UNIV" by fact
  hence noFault_C': "Γ⊨⟨C' s,Normal s ⟩ ==>∉Fault ` UNIV"
    by (auto intro: exec.intros simp add: final_notin_def)
  have "c ⊆<sub>g</sub> DynCom C'" by fact
  from subseteq_guards_DynCom [OF this] obtain C where
    c: "c = DynCom C" and
    C_C': "∀s. C s ⊆<sub>g</sub> C' s"
    by blast
  from DynCom.hyps termi_C' C_C' [rule_format] noFault_C'
  have "Γ⊨C s ↓ Normal s"
    by fast
  with c show ?case
    by (auto intro: terminates.intros)
next
  case (Guard f' g' c')
  have noFault: "Γ⊨⟨Guard f' g' c',Normal s ⟩ ==>∉Fault ` UNIV" by fact
  have termi: "Γ⊨Guard f' g' c' ↓ Normal s" by fact
  have "c ⊆_g Guard f' g' c'" by fact
  hence c_cases: "(c ⊆_g c') ∨ (∃c''. c = Guard f' g' c'' ∧ (c'' ⊆_g c'))"
    by (rule subseteq_guards_Guard)
  thus ?case
  proof (cases "s ∈ g'")
    case True
    note s_in_g' = this
    with noFault have noFault_c': "Γ⊨⟨c',Normal s ⟩ ==>∉Fault ` UNIV"
      by (auto simp add: final_notin_def intro: exec.intros)
    from termi s_in_g' have termi_c': "Γ⊨c' ↓ Normal s"
      by cases auto
    from c_cases show ?thesis
    proof
      assume "c ⊆<sub>g</sub> c'"
      from termi_c' this noFault_c'
      show "Γ⊨c ↓ Normal s"
        by (rule Guard.hyps)
    next
      assume "∃c''. c = Guard f' g' c'' ∧ (c'' ⊆<sub>g</sub> c')"
      then obtain c'' where
        c: "c = Guard f' g' c''" and c''_c': "c'' ⊆<sub>g</sub> c'"
        by blast
      from termi_c' c''_c' noFault_c'
      have "Γ⊨c'' ↓ Normal s"
        by (rule Guard.hyps)
      with s_in_g' c
      show ?thesis
        by (auto intro: terminates.intros)
    qed
  next
    case False
    with noFault have False
      by (auto intro: exec.intros simp add: final_notin_def)
    thus ?thesis ..
  qed
next
  case Throw thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
  case (Catch c1' c2')
  have termi: "Γ⊨Catch c1' c2' ↓ Normal s" by fact
  then obtain
    termi_c1': "Γ⊨c1'↓ Normal s" and
    termi_c2': "∀s'. Γ⊨⟨c1',Normal s ⟩ ==> Abrupt s' ⟶ Γ⊨c2'↓ Normal s'"
    by (auto elim: terminates_Normal_elim_cases)
  have noFault: "Γ⊨⟨Catch c1' c2',Normal s ⟩ ==>∉Fault ` UNIV" by fact
  hence noFault_c1': "Γ⊨⟨c1',Normal s ⟩ ==>∉Fault ` UNIV"
    by (fastforce intro: exec.intros simp add: final_notin_def)
  have "c ⊆<sub>g</sub> Catch c1' c2'"  by fact
  from subseteq_guards_Catch [OF this] obtain c1 c2 where
    c: "c = Catch c1 c2" and
    c1_c1': "c1 ⊆<sub>g</sub> c1'" and
    c2_c2': "c2 ⊆<sub>g</sub> c2'"
    by blast
  from termi_c1' c1_c1' noFault_c1'
  have "Γ⊨c1↓ Normal s"
    by (rule Catch.hyps)
  moreover
  {
    fix t
    assume exec_c1: "Γ⊨⟨c1,Normal s ⟩ ==> Abrupt t"
    have "Γ⊨c2↓ Normal t"
    proof -
      from exec_to_exec_subseteq_guards [OF c1_c1' exec_c1] obtain t' where
        exec_c1': "Γ⊨⟨c1',Normal s ⟩ ==> t'" and
        t'_noFault: "¬ isFault t' ⟶ t' = Abrupt t"
        by blast
      show ?thesis
      proof (cases "isFault t'")
        case True
        with exec_c1' noFault_c1'
        have False
          by (fastforce elim: isFaultE dest: Fault_end simp add: final_notin_def)
        thus ?thesis ..
      next
        case False
        with t'_noFault have t': "t'=Abrupt t" by simp
        with termi_c2' exec_c1'
        have termi_c2': "Γ⊨c2'↓ Normal t"
          by auto
        with noFault exec_c1' t'
        have "Γ⊨⟨c2',Normal t ⟩ ==>∉Fault ` UNIV"
          by (auto intro: exec.intros simp add: final_notin_def)
        from termi_c2' c2_c2' this
        show "Γ⊨c2 ↓ Normal t"
          by (rule Catch.hyps)
      qed
    qed
  }
  ultimately show ?case using c by (auto intro: terminates.intros)
qed

theorem terminates_fewer_guards:
  shows "[Γ⊨c'↓s; c ⊆_g c'; Γ⊨⟨c',s ⟩ ==>∉Fault ` UNIV]
         ==> Γ⊨c↓s"
  by (cases s) (auto intro: terminates_fewer_guards_Normal)

lemma terminates_noFault_strip_guards:
  assumes termi: "Γ⊨c↓Normal s"
  shows "[Γ⊨⟨c,Normal s ⟩ ==>∉Fault ` F] ==> Γ⊨strip_guards F c↓Normal s"
using termi
proof (induct)
  case Skip thus ?case by (auto intro: terminates.intros)
next
  case Basic thus ?case by (auto intro: terminates.intros)
next
  case Spec thus ?case by (auto intro: terminates.intros)
next
  case (Guard s g c f)
  have s_in_g: "s ∈ g" by fact
  have "Γ⊨c ↓ Normal s" by fact
  have "Γ⊨⟨Guard f g c,Normal s ⟩ ==>∉Fault ` F" by fact
  with s_in_g have "Γ⊨⟨c,Normal s ⟩ ==>∉Fault ` F"
    by (fastforce simp add: final_notin_def intro: exec.intros)
  with Guard.hyps have "Γ⊨strip_guards F c ↓ Normal s" by simp
  with s_in_g show ?case
    by (auto intro: terminates.intros)
next
  case GuardFault thus ?case
    by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
next
  case Fault thus ?case by (auto intro: terminates.intros)
next
  case (Seq c1 s c2)
  have noFault_Seq: "Γ⊨⟨Seq c1 c2,Normal s ⟩ ==>∉Fault ` F" by fact
  hence noFault_c1: "Γ⊨⟨c1,Normal s ⟩ ==>∉Fault ` F"
    by (auto simp add: final_notin_def intro: exec.intros)
  with Seq.hyps have "Γ⊨strip_guards F c1 ↓ Normal s" by simp
  moreover
  {
    fix s'
    assume exec_strip_guards_c1: "Γ⊨⟨strip_guards F c1,Normal s ⟩ ==> s'"
    have "Γ⊨strip_guards F c2 ↓ s'"
    proof (cases "isFault s'")
      case True
      thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
    next
      case False
      with exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1
      have *: "Γ⊨⟨c1,Normal s ⟩ ==> s'"
        by (auto simp add: final_notin_def elim!: isFaultE)
      with noFault_Seq have "Γ⊨⟨c2,s' ⟩ ==>∉Fault ` F"
        by (auto simp add: final_notin_def intro: exec.intros)
      with * show ?thesis
        using Seq.hyps by simp
    qed
  }
  ultimately show ?case
    by (auto intro: terminates.intros)
next
  case CondTrue thus ?case
    by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
next
  case CondFalse thus ?case
    by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
next
  case (WhileTrue s b c)
  have s_in_b: "s ∈ b" by fact
  have noFault_while: "Γ⊨⟨While b c,Normal s ⟩ ==>∉Fault ` F" by fact
  with s_in_b have noFault_c: "Γ⊨⟨c,Normal s ⟩ ==>∉Fault ` F"
    by (auto simp add: final_notin_def intro: exec.intros)
  with WhileTrue.hyps have "Γ⊨strip_guards F c ↓ Normal s" by simp
  moreover
  {
    fix s'
    assume exec_strip_guards_c: "Γ⊨⟨strip_guards F c,Normal s ⟩ ==> s'"
    have "Γ⊨strip_guards F (While b c) ↓ s'"
    proof (cases "isFault s'")
      case True
      thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
    next
      case False
      with exec_strip_guards_to_exec [OF exec_strip_guards_c] noFault_c
      have *: "Γ⊨⟨c,Normal s ⟩ ==> s'"
        by (auto simp add: final_notin_def elim!: isFaultE)
      with s_in_b noFault_while have "Γ⊨⟨While b c,s' ⟩ ==>∉Fault ` F"
        by (auto simp add: final_notin_def intro: exec.intros)
      with * show ?thesis
        using WhileTrue.hyps by simp
    qed
  }
  ultimately show ?case
    using WhileTrue.hyps by (auto intro: terminates.intros)
next
  case WhileFalse thus ?case by (auto intro: terminates.intros)
next
  case Call thus ?case by (auto intro: terminates.intros)
next
  case CallUndefined thus ?case by (auto intro: terminates.intros)
next
  case Stuck thus ?case by (auto intro: terminates.intros)
next
  case DynCom thus ?case
    by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
next
  case Throw thus ?case by (auto intro: terminates.intros)
next
  case Abrupt thus ?case by (auto intro: terminates.intros)
next
  case (Catch c1 s c2)
  have noFault_Catch: "Γ⊨⟨Catch c1 c2,Normal s ⟩ ==>∉Fault ` F" by fact
  hence noFault_c1: "Γ⊨⟨c1,Normal s ⟩ ==>∉Fault ` F"
    by (fastforce simp add: final_notin_def intro: exec.intros)
  with Catch.hyps have "Γ⊨strip_guards F c1 ↓ Normal s" by simp
  moreover
  {
    fix s'
    assume exec_strip_guards_c1: "Γ⊨⟨strip_guards F c1,Normal s ⟩ ==> Abrupt s'"
    have "Γ⊨strip_guards F c2 ↓ Normal s'"
    proof -
      from exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1
      have *: "Γ⊨⟨c1,Normal s ⟩ ==> Abrupt s'"
        by (auto simp add: final_notin_def elim!: isFaultE)
      with noFault_Catch have "Γ⊨⟨c2,Normal s' ⟩ ==>∉Fault ` F"
        by (auto simp add: final_notin_def intro: exec.intros)
      with * show ?thesis
        using Catch.hyps by simp
    qed
  }
  ultimately show ?case
    using Catch.hyps by (auto intro: terminates.intros)
qed

(* ************************************************************************* *)
subsection ‹Lemmas about @{const "strip_guards"}›
(* ************************************************************************* *)

lemma terminates_noFault_strip:
  assumes termi: "Γ⊨c↓Normal s"
  shows "[Γ⊨⟨c,Normal s ⟩ ==>∉Fault ` F] ==> strip F Γ⊨c↓Normal s"
using termi
proof (induct)
  case Skip thus ?case by (auto intro: terminates.intros)
next
  case Basic thus ?case by (auto intro: terminates.intros)
next
  case Spec thus ?case by (auto intro: terminates.intros)
next
  case (Guard s g c f)
  have s_in_g: "s ∈ g" by fact
  have "Γ⊨⟨Guard f g c,Normal s ⟩ ==>∉Fault ` F" by fact
  with s_in_g have "Γ⊨⟨c,Normal s ⟩ ==>∉Fault ` F"
    by (fastforce simp add: final_notin_def intro: exec.intros)
  then have "strip F Γ⊨c ↓ Normal s" by (simp add: Guard.hyps)
  with s_in_g show ?case
    by (auto intro: terminates.intros simp del: strip_simp)
next
  case GuardFault thus ?case
    by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
next
  case Fault thus ?case by (auto intro: terminates.intros)
next
  case (Seq c1 s c2)
  have noFault_Seq: "Γ⊨⟨Seq c1 c2,Normal s ⟩ ==>∉Fault ` F" by fact
  hence noFault_c1: "Γ⊨⟨c1,Normal s ⟩ ==>∉Fault ` F"
    by (auto simp add: final_notin_def intro: exec.intros)
  then have "strip F Γ⊨c1 ↓ Normal s" by (simp add: Seq.hyps)
  moreover
  {
    fix s'
    assume exec_strip_c1: "strip F Γ⊨⟨c1,Normal s ⟩ ==> s'"
    have "strip F Γ⊨c2 ↓ s'"
    proof (cases "isFault s'")
      case True
      thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
    next
      case False
      with exec_strip_to_exec [OF exec_strip_c1] noFault_c1
      have *: "Γ⊨⟨c1,Normal s ⟩ ==> s'"
        by (auto simp add: final_notin_def elim!: isFaultE)
      with noFault_Seq have "Γ⊨⟨c2,s' ⟩ ==>∉Fault ` F"
        by (auto simp add: final_notin_def intro: exec.intros)
      with * show ?thesis
        using Seq.hyps by (simp del: strip_simp)
    qed
  }
  ultimately show ?case
    by (fastforce intro: terminates.intros)
next
  case CondTrue thus ?case
    by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
next
  case CondFalse thus ?case
    by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
next
  case (WhileTrue s b c)
  have s_in_b: "s ∈ b" by fact
  have noFault_while: "Γ⊨⟨While b c,Normal s ⟩ ==>∉Fault ` F" by fact
  with s_in_b have noFault_c: "Γ⊨⟨c,Normal s ⟩ ==>∉Fault ` F"
    by (auto simp add: final_notin_def intro: exec.intros)
  then have "strip F Γ⊨c ↓ Normal s" by (simp add: WhileTrue.hyps)
  moreover
  {
    fix s'
    assume exec_strip_c: "strip F Γ⊨⟨c,Normal s ⟩ ==> s'"
    have "strip F Γ⊨While b c ↓ s'"
    proof (cases "isFault s'")
      case True
      thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
    next
      case False
      with exec_strip_to_exec [OF exec_strip_c] noFault_c
      have *: "Γ⊨⟨c,Normal s ⟩ ==> s'"
        by (auto simp add: final_notin_def elim!: isFaultE)
      with s_in_b noFault_while have "Γ⊨⟨While b c,s' ⟩ ==>∉Fault ` F"
        by (auto simp add: final_notin_def intro: exec.intros)
      with * show ?thesis
        using WhileTrue.hyps by (simp del: strip_simp)
    qed
  }
  ultimately show ?case
    using WhileTrue.hyps by (auto intro: terminates.intros simp del: strip_simp)
next
  case WhileFalse thus ?case by (auto intro: terminates.intros)
next
  case (Call p bdy s)
  have bdy: "Γ p = Some bdy" by fact
  have "Γ⊨⟨Call p,Normal s ⟩ ==>∉Fault ` F" by fact
  with bdy have bdy_noFault: "Γ⊨⟨bdy,Normal s ⟩ ==>∉Fault ` F"
    by (auto intro: exec.intros simp add: final_notin_def)
  then have strip_bdy_noFault: "strip F Γ⊨⟨bdy,Normal s ⟩ ==>∉Fault ` F"
    by (auto simp add: final_notin_def dest!: exec_strip_to_exec elim!: isFaultE)

  from bdy_noFault have "strip F Γ⊨bdy ↓ Normal s" by (simp add: Call.hyps)
  from terminates_noFault_strip_guards [OF this strip_bdy_noFault]
  have "strip F Γ⊨strip_guards F bdy ↓ Normal s".
  with bdy show ?case
    by (fastforce intro: terminates.Call)
next
  case CallUndefined thus ?case by (auto intro: terminates.intros)
next
  case Stuck thus ?case by (auto intro: terminates.intros)
next
  case DynCom thus ?case
    by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
next
  case Throw thus ?case by (auto intro: terminates.intros)
next
  case Abrupt thus ?case by (auto intro: terminates.intros)
next
  case (Catch c1 s c2)
  have noFault_Catch: "Γ⊨⟨Catch c1 c2,Normal s ⟩ ==>∉Fault ` F" by fact
  hence noFault_c1: "Γ⊨⟨c1,Normal s ⟩ ==>∉Fault ` F"
    by (fastforce simp add: final_notin_def intro: exec.intros)
  then have "strip F Γ⊨c1 ↓ Normal s" by (simp add: Catch.hyps)
  moreover
  {
    fix s'
    assume exec_strip_c1: "strip F Γ⊨⟨c1,Normal s ⟩ ==> Abrupt s'"
    have "strip F Γ⊨c2 ↓ Normal s'"
    proof -
      from exec_strip_to_exec [OF exec_strip_c1] noFault_c1
      have *: "Γ⊨⟨c1,Normal s ⟩ ==> Abrupt s'"
        by (auto simp add: final_notin_def elim!: isFaultE)
      with * noFault_Catch have "Γ⊨⟨c2,Normal s' ⟩ ==>∉Fault ` F"
        by (auto simp add: final_notin_def intro: exec.intros)
      with * show ?thesis
        using Catch.hyps by (simp del: strip_simp)
    qed
  }
  ultimately show ?case
    using Catch.hyps by (auto intro: terminates.intros simp del: strip_simp)
qed


(* ************************************************************************* *)
subsection ‹Miscellaneous›
(* ************************************************************************* *)

lemma terminates_while_lemma:
  assumes termi: "Γ⊨w↓fk"
  shows "∧k b c. [fk = Normal (f k); w=While b c;
                       ∀i. Γ⊨⟨c,Normal (f i) ⟩ ==> Normal (f (Suc i))]
         ==> ∃i. f i ∉ b"
using termi
proof (induct)
  case WhileTrue thus ?case by blast
next
  case WhileFalse thus ?case by blast
qed simp_all

lemma terminates_while:
  "[Γ⊨(While b c)↓Normal (f k);
    ∀i. Γ⊨⟨c,Normal (f i) ⟩ ==> Normal (f (Suc i))]
         ==> ∃i. f i ∉ b"
  by (blast intro: terminates_while_lemma)

lemma wf_terminates_while:
 "wf {(t,s). Γ⊨(While b c)↓Normal s ∧ s∈b ∧
             Γ⊨⟨c,Normal s ⟩ ==> Normal t}"
apply(subst wf_iff_no_infinite_down_chain)
apply(rule notI)
apply clarsimp
apply(insert terminates_while)
apply blast
done

lemma terminates_restrict_to_terminates:
  assumes terminates_res: "Γ|⊨ c ↓ s"
  assumes not_Stuck: "Γ|⊨⟨c,s ⟩ ==>∉{Stuck}"
  shows "Γ⊨ c ↓ s"
using terminates_res not_Stuck
proof (induct)
  case Skip show ?case by (rule terminates.Skip)
next
  case Basic show ?case by (rule terminates.Basic)
next
  case Spec show ?case by (rule terminates.Spec)
next
  case Guard thus ?case
    by (auto intro: terminates.Guard dest: notStuck_GuardD)
next
  case GuardFault thus ?case by (auto intro: terminates.GuardFault)
next
  case Fault show ?case by (rule terminates.Fault)
next
  case (Seq c1 s c2)
  have not_Stuck: "Γ|⊨⟨Seq c1 c2,Normal s ⟩ ==>∉{Stuck}" by fact
  hence c1_notStuck: "Γ|⊨⟨c1,Normal s ⟩ ==>∉{Stuck}"
    by (rule notStuck_SeqD1)
  show "Γ⊨Seq c1 c2 ↓ Normal s"
  proof (rule terminates.Seq,safe)
    from c1_notStuck
    show "Γ⊨c1 ↓ Normal s"
      by (rule Seq.hyps)
  next
    fix s'
    assume exec: "Γ⊨⟨c1,Normal s ⟩ ==> s'"
    show "Γ⊨c2 ↓ s'"
    proof -
      from exec_to_exec_restrict [OF exec] obtain t' where
        exec_res: "Γ|⊨⟨c1,Normal s ⟩ ==> t'" and
        t'_notStuck: "t' ≠ Stuck ⟶ t' = s'"
        by blast
      show ?thesis
      proof (cases "t'=Stuck")
        case True
        with c1_notStuck exec_res have "False"
          by (auto simp add: final_notin_def)
        thus ?thesis ..
      next
        case False
        with t'_notStuck have t': "t'=s'" by simp
        with not_Stuck exec_res
        have "Γ|⊨⟨c2,s' ⟩ ==>∉{Stuck}"
          by (auto dest: notStuck_SeqD2)
        with exec_res t' Seq.hyps
        show ?thesis
          by auto
      qed
    qed
  qed
next
  case CondTrue thus ?case
    by (auto intro: terminates.CondTrue dest: notStuck_CondTrueD)
next
  case CondFalse thus ?case
    by (auto intro: terminates.CondFalse dest: notStuck_CondFalseD)
next
  case (WhileTrue s b c)
  have s: "s ∈ b" by fact
  have not_Stuck: "Γ|⊨⟨While b c,Normal s ⟩ ==>∉{Stuck}" by fact
  with WhileTrue have c_notStuck: "Γ|⊨⟨c,Normal s ⟩ ==>∉{Stuck}"
    by (iprover intro:  notStuck_WhileTrueD1)
  show ?case
  proof (rule terminates.WhileTrue [OF s],safe)
    from c_notStuck
    show "Γ⊨c ↓ Normal s"
      by (rule WhileTrue.hyps)
  next
    fix s'
    assume exec: "Γ⊨⟨c,Normal s ⟩ ==> s'"
    show "Γ⊨While b c ↓ s'"
    proof -
      from exec_to_exec_restrict [OF exec] obtain t' where
        exec_res: "Γ|⊨⟨c,Normal s ⟩ ==> t'" and
        t'_notStuck: "t' ≠ Stuck ⟶ t' = s'"
        by blast
      show ?thesis
      proof (cases "t'=Stuck")
        case True
        with c_notStuck exec_res have "False"
          by (auto simp add: final_notin_def)
        thus ?thesis ..
      next
        case False
        with t'_notStuck have t': "t'=s'" by simp
        with not_Stuck exec_res s
        have "Γ|⊨⟨While b c,s' ⟩ ==>∉{Stuck}"
          by (auto dest: notStuck_WhileTrueD2)
        with exec_res t' WhileTrue.hyps
        show ?thesis
          by auto
      qed
    qed
  qed
next
  case WhileFalse then show ?case by (iprover intro: terminates.WhileFalse)
next
  case Call thus ?case
    by (auto intro: terminates.Call dest: notStuck_CallD restrict_SomeD)
next
  case CallUndefined
  thus ?case
    by (auto dest: notStuck_CallDefinedD)
next
  case Stuck show ?case by (rule terminates.Stuck)
next
  case DynCom
  thus ?case
    by (auto intro: terminates.DynCom dest: notStuck_DynComD)
next
  case Throw show ?case by (rule terminates.Throw)
next
  case Abrupt show ?case by (rule terminates.Abrupt)
next
  case (Catch c1 s c2)
  have not_Stuck: "Γ|⊨⟨Catch c1 c2,Normal s ⟩ ==>∉{Stuck}" by fact
  hence c1_notStuck: "Γ|⊨⟨c1,Normal s ⟩ ==>∉{Stuck}"
    by (rule notStuck_CatchD1)
  show "Γ⊨Catch c1 c2 ↓ Normal s"
  proof (rule terminates.Catch,safe)
    from c1_notStuck
    show "Γ⊨c1 ↓ Normal s"
      by (rule Catch.hyps)
  next
    fix s'
    assume exec: "Γ⊨⟨c1,Normal s ⟩ ==> Abrupt s'"
    show "Γ⊨c2 ↓ Normal s'"
    proof -
      from exec_to_exec_restrict [OF exec] obtain t' where
        exec_res: "Γ|⊨⟨c1,Normal s ⟩ ==> t'" and
        t'_notStuck: "t' ≠ Stuck ⟶ t' = Abrupt s'"
        by blast
      show ?thesis
      proof (cases "t'=Stuck")
        case True
        with c1_notStuck exec_res have "False"
          by (auto simp add: final_notin_def)
        thus ?thesis ..
      next
        case False
        with t'_notStuck have t': "t'=Abrupt s'" by simp
        with not_Stuck exec_res
        have "Γ|⊨⟨c2,Normal s' ⟩ ==>∉{Stuck}"
          by (auto dest: notStuck_CatchD2)
        with exec_res t' Catch.hyps
        show ?thesis
          by auto
      qed
    qed
  qed
qed

end