SSL Semantic.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 ‹Big-Step Semantics for Simpl›
theory Semantic imports Language begin

notation
restrict_map  (‹_|› [90, 91] 90)


datatype ('s,'f) xstate = Normal 's | Abrupt 's | Fault 'f | Stuck

definition isAbr::"('s,'f) xstate ==> bool"
  where "isAbr S = (∃s. S=Abrupt s)"

lemma isAbr_simps [simp]:
"isAbr (Normal s) = False"
"isAbr (Abrupt s) = True"
"isAbr (Fault f) = False"
"isAbr Stuck = False"
by (auto simp add: isAbr_def)

lemma isAbrE [consumes 1, elim?]: "[isAbr S; ∧s. S=Abrupt s ==> P] ==> P"
  by (auto simp add: isAbr_def)

lemma not_isAbrD:
"¬ isAbr s ==> (∃s'. s=Normal s') ∨ s = Stuck ∨ (∃f. s=Fault f)"
  by (cases s) auto

definition isFault:: "('s,'f) xstate ==> bool"
  where "isFault S = (∃f. S=Fault f)"

lemma isFault_simps [simp]:
"isFault (Normal s) = False"
"isFault (Abrupt s) = False"
"isFault (Fault f) = True"
"isFault Stuck = False"
by (auto simp add: isFault_def)

lemma isFaultE [consumes 1, elim?]: "[isFault s; ∧f. s=Fault f ==> P] ==> P"
  by (auto simp add: isFault_def)

lemma not_isFault_iff: "(¬ isFault t) = (∀f. t ≠ Fault f)"
  by (auto elim: isFaultE)

(* ************************************************************************* *)
subsection ‹Big-Step Execution: ‹Γ⊨⟨c, s⟩ ==> t››
(* ************************************************************************* *)

text ‹The procedure environment›
type_synonym ('s,'p,'f) body = "'p ==> ('s,'p,'f) com option"

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

| Guard: "[s∈g; Γ⊨⟨c,Normal s⟩ ==> t]
          ==>
          Γ⊨⟨Guard f g c,Normal s⟩ ==> t"

| GuardFault: "s∉g ==> Γ⊨⟨Guard f g c,Normal s⟩ ==> Fault f"

| FaultProp [intro,simp]: "Γ⊨⟨c,Fault f⟩ ==> Fault f"

| Basic: "Γ⊨⟨Basic f,Normal s⟩ ==> Normal (f s)"

| Spec: "(s,t) ∈ r
         ==>
         Γ⊨⟨Spec r,Normal s⟩ ==> Normal t"

| SpecStuck: "∀t. (s,t) ∉ r
              ==>
              Γ⊨⟨Spec r,Normal s⟩ ==> Stuck"

| Seq: "[Γ⊨⟨c₁,Normal s⟩ ==> s'; Γ⊨⟨c₂,s'⟩ ==> t]
        ==>
        Γ⊨⟨Seq c₁ c₂,Normal s⟩ ==> t"

| CondTrue: "[s ∈ b; Γ⊨⟨c₁,Normal s⟩ ==> t]
             ==>
             Γ⊨⟨Cond b c₁ c₂,Normal s⟩ ==> t"

| CondFalse: "[s ∉ b; Γ⊨⟨c₂,Normal s⟩ ==> t]
              ==>
              Γ⊨⟨Cond b c₁ c₂,Normal s⟩ ==> t"

| WhileTrue: "[s ∈ b; Γ⊨⟨c,Normal s⟩ ==> s'; Γ⊨⟨While b c,s'⟩ ==> t]
              ==>
              Γ⊨⟨While b c,Normal s⟩ ==> t"

| WhileFalse: "[s ∉ b]
               ==>
               Γ⊨⟨While b c,Normal s⟩ ==> Normal s"

| Call:  "[Γ p=Some bdy;Γ⊨⟨bdy,Normal s⟩ ==> t]
          ==>
          Γ⊨⟨Call p,Normal s⟩ ==> t"

| CallUndefined: "[Γ p=None]
                  ==>
                  Γ⊨⟨Call p,Normal s⟩ ==> Stuck"

| StuckProp [intro,simp]: "Γ⊨⟨c,Stuck⟩ ==> Stuck"

| DynCom:  "[Γ⊨⟨(c s),Normal s⟩ ==> t]
             ==>
             Γ⊨⟨DynCom c,Normal s⟩ ==> t"

| Throw: "Γ⊨⟨Throw,Normal s⟩ ==> Abrupt s"

| AbruptProp [intro,simp]: "Γ⊨⟨c,Abrupt s⟩ ==> Abrupt s"

| CatchMatch: "[Γ⊨⟨c₁,Normal s⟩ ==> Abrupt s'; Γ⊨⟨c₂,Normal s'⟩ ==> t]
               ==>
               Γ⊨⟨Catch c₁ c₂,Normal s⟩ ==> t"
| CatchMiss: "[Γ⊨⟨c₁,Normal s⟩ ==> t; ¬isAbr t]
               ==>
               Γ⊨⟨Catch c₁ c₂,Normal s⟩ ==> t"

inductive_cases exec_elim_cases [cases set]:
  "Γ⊨⟨c,Fault f⟩ ==> t"
  "Γ⊨⟨c,Stuck⟩ ==> t"
  "Γ⊨⟨c,Abrupt s⟩ ==> t"
  "Γ⊨⟨Skip,s⟩ ==> t"
  "Γ⊨⟨Seq c1 c2,s⟩ ==> t"
  "Γ⊨⟨Guard f g c,s⟩ ==> t"
  "Γ⊨⟨Basic f,s⟩ ==> t"
  "Γ⊨⟨Spec r,s⟩ ==> t"
  "Γ⊨⟨Cond b c1 c2,s⟩ ==> t"
  "Γ⊨⟨While b c,s⟩ ==> t"
  "Γ⊨⟨Call p,s⟩ ==> t"
  "Γ⊨⟨DynCom c,s⟩ ==> t"
  "Γ⊨⟨Throw,s⟩ ==> t"
  "Γ⊨⟨Catch c1 c2,s⟩ ==> t"


inductive_cases exec_Normal_elim_cases [cases set]:
  "Γ⊨⟨c,Fault f⟩ ==> t"
  "Γ⊨⟨c,Stuck⟩ ==> t"
  "Γ⊨⟨c,Abrupt s⟩ ==> t"
  "Γ⊨⟨Skip,Normal s⟩ ==> t"
  "Γ⊨⟨Guard f g c,Normal s⟩ ==> t"
  "Γ⊨⟨Basic f,Normal s⟩ ==> t"
  "Γ⊨⟨Spec r,Normal s⟩ ==> t"
  "Γ⊨⟨Seq c1 c2,Normal s⟩ ==> t"
  "Γ⊨⟨Cond b c1 c2,Normal s⟩ ==> t"
  "Γ⊨⟨While b c,Normal s⟩ ==> t"
  "Γ⊨⟨Call p,Normal s⟩ ==> t"
  "Γ⊨⟨DynCom c,Normal s⟩ ==> t"
  "Γ⊨⟨Throw,Normal s⟩ ==> t"
  "Γ⊨⟨Catch c1 c2,Normal s⟩ ==> t"


lemma exec_block_exn:
  "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t; Γ⊨⟨c s t,Normal (return s t)⟩ ==> u]
  ==>
  Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ ==> u"
apply (unfold block_exn_def)
  by (fastforce intro: exec.intros)

lemma exec_block:
  "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t; Γ⊨⟨c s t,Normal (return s t)⟩ ==> u]
  ==>
  Γ⊨⟨block init bdy return c,Normal s⟩ ==> u"
  unfolding block_def
  by (rule exec_block_exn)

lemma exec_block_exnAbrupt:
     "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Abrupt t]
       ==>
       Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ ==> Abrupt (result_exn (return s t) t)"
apply (unfold block_exn_def)
  by (fastforce intro: exec.intros)

lemma exec_blockAbrupt:
     "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Abrupt t]
       ==>
       Γ⊨⟨block init bdy return c,Normal s⟩ ==> Abrupt (return s t)"
  unfolding block_def
  by (rule exec_block_exnAbrupt)

lemma exec_block_exnFault:
  "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Fault f]
   ==>
  Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ ==> Fault f"
apply (unfold block_exn_def)
  by (fastforce intro: exec.intros)

lemma exec_blockFault:
  "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Fault f]
   ==>
  Γ⊨⟨block init bdy return c,Normal s⟩ ==> Fault f"
  unfolding block_def
  by (rule exec_block_exnFault)

lemma exec_block_exnStuck:
  "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Stuck]
  ==>
  Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ ==> Stuck"
apply (unfold block_exn_def)
  by (fastforce intro: exec.intros)

lemma exec_blockStuck:
  "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Stuck]
  ==>
  Γ⊨⟨block init bdy return c,Normal s⟩ ==> Stuck"
  unfolding block_def
  by (rule exec_block_exnStuck)

lemma exec_call:
 "[Γ p=Some bdy;Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t; Γ⊨⟨c s t,Normal (return s t)⟩ ==> u]
  ==>
  Γ⊨⟨call init p return c,Normal s⟩ ==> u"
apply (simp add: call_def)
apply (rule exec_block)
apply  (erule (1) Call)
apply assumption
done

lemma exec_callAbrupt:
 "[Γ p=Some bdy;Γ⊨⟨bdy,Normal (init s)⟩ ==> Abrupt t]
  ==>
  Γ⊨⟨call init p return c,Normal s⟩ ==> Abrupt (return s t)"
apply (simp add: call_def)
apply (rule exec_blockAbrupt)
apply (erule (1) Call)
done

lemma exec_callFault:
             "[Γ p=Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Fault f]
               ==>
              Γ⊨⟨call init p return c,Normal s⟩ ==> Fault f"
apply (simp add: call_def)
apply (rule exec_blockFault)
apply (erule (1) Call)
done

lemma exec_callStuck:
          "[Γ p=Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Stuck]
           ==>
           Γ⊨⟨call init p return c,Normal s⟩ ==> Stuck"
apply (simp add: call_def)
apply (rule exec_blockStuck)
apply (erule (1) Call)
done

lemma  exec_callUndefined:
       "[Γ p=None]
        ==>
        Γ⊨⟨call init p return c,Normal s⟩ ==> Stuck"
apply (simp add: call_def)
apply (rule exec_blockStuck)
apply (erule CallUndefined)
done

lemma exec_call_exn:
 "[Γ p=Some bdy;Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t; Γ⊨⟨c s t,Normal (return s t)⟩ ==> u]
  ==>
  Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ ==> u"
apply (simp add: call_exn_def)
apply (rule exec_block_exn)
apply  (erule (1) Call)
apply assumption
done

lemma exec_call_exnAbrupt:
 "[Γ p=Some bdy;Γ⊨⟨bdy,Normal (init s)⟩ ==> Abrupt t]
  ==>
  Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ ==> Abrupt (result_exn (return s t) t)"
apply (simp add: call_exn_def)
apply (rule exec_block_exnAbrupt)
apply (erule (1) Call)
done

lemma exec_call_exnFault:
             "[Γ p=Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Fault f]
               ==>
              Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ ==> Fault f"
apply (simp add: call_exn_def)
apply (rule exec_block_exnFault)
apply (erule (1) Call)
done

lemma exec_call_exnStuck:
          "[Γ p=Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Stuck]
           ==>
           Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ ==> Stuck"
apply (simp add: call_exn_def)
apply (rule exec_block_exnStuck)
apply (erule (1) Call)
done

lemma  exec_call_exnUndefined:
       "[Γ p=None]
        ==>
        Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ ==> Stuck"
apply (simp add: call_exn_def)
apply (rule exec_block_exnStuck)
apply (erule CallUndefined)
  done


lemma Fault_end: assumes exec: "Γ⊨⟨c,s⟩ ==> t" and s: "s=Fault f"
  shows "t=Fault f"
using exec s by (induct) auto

lemma Stuck_end: assumes exec: "Γ⊨⟨c,s⟩ ==> t" and s: "s=Stuck"
  shows "t=Stuck"
using exec s by (induct) auto

lemma Abrupt_end: assumes exec: "Γ⊨⟨c,s⟩ ==> t" and s: "s=Abrupt s'"
  shows "t=Abrupt s'"
using exec s by (induct) auto

lemma exec_Call_body_aux:
  "Γ p=Some bdy ==>
   Γ⊨⟨Call p,s⟩ ==> t = Γ⊨⟨bdy,s⟩ ==> t"
apply (rule)
apply (fastforce elim: exec_elim_cases )
apply (cases s)
apply   (cases t)
apply (auto intro: exec.intros dest: Fault_end Stuck_end Abrupt_end)
done

lemma exec_Call_body':
  "p ∈ dom Γ ==>
  Γ⊨⟨Call p,s⟩ ==> t = Γ⊨⟨the (Γ p),s⟩ ==> t"
  apply clarsimp
  by (rule exec_Call_body_aux)


lemma exec_block_exn_Normal_elim [consumes 1]:
assumes exec_block: "Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ ==> t"
assumes Normal:
 "∧t'.
    [Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t';
     Γ⊨⟨c s t',Normal (return s t')⟩ ==> t]
    ==> P"
assumes Abrupt:
 "∧t'.
    [Γ⊨⟨bdy,Normal (init s)⟩ ==> Abrupt t';
     t = Abrupt (result_exn (return s t') t')]
    ==> P"
assumes Fault:
 "∧f.
    [Γ⊨⟨bdy,Normal (init s)⟩ ==> Fault f;
     t = Fault f]
    ==> P"
assumes Stuck:
 "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Stuck;
     t = Stuck]
    ==> P"
assumes
 "[Γ p = None; t = Stuck] ==> P"
shows "P"
  using exec_block
apply (unfold block_exn_def)
apply (elim exec_Normal_elim_cases)
apply simp_all
apply  (case_tac s')
apply     simp_all
apply     (elim exec_Normal_elim_cases)
apply     simp
apply    (drule Abrupt_end) apply simp
apply    (erule exec_Normal_elim_cases)
apply    simp
apply    (rule Abrupt,assumption+)
apply   (drule Fault_end) apply simp
apply   (erule exec_Normal_elim_cases)
apply   simp
apply  (drule Stuck_end) apply simp
apply  (erule exec_Normal_elim_cases)
apply  simp
apply (case_tac s')
apply    simp_all
apply   (elim exec_Normal_elim_cases)
apply   simp
apply   (rule Normal, assumption+)
apply  (drule Fault_end) apply simp
apply  (rule Fault,assumption+)
apply (drule Stuck_end) apply simp
apply (rule Stuck,assumption+)
done


lemma exec_block_Normal_elim [consumes 1]:
assumes exec_block: "Γ⊨⟨block init bdy return c,Normal s⟩ ==> t"
assumes Normal:
 "∧t'.
    [Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t';
     Γ⊨⟨c s t',Normal (return s t')⟩ ==> t]
    ==> P"
assumes Abrupt:
 "∧t'.
    [Γ⊨⟨bdy,Normal (init s)⟩ ==> Abrupt t';
     t = Abrupt (return s t')]
    ==> P"
assumes Fault:
 "∧f.
    [Γ⊨⟨bdy,Normal (init s)⟩ ==> Fault f;
     t = Fault f]
    ==> P"
assumes Stuck:
 "[Γ⊨⟨bdy,Normal (init s)⟩ ==> Stuck;
     t = Stuck]
    ==> P"
assumes
 Undef: "[Γ p = None; t = Stuck] ==> P"
shows "P"
  by (rule exec_block_exn_Normal_elim [OF exec_block [simplified block_def]
  Normal Abrupt Fault Stuck Undef ])

lemma exec_call_exn_Normal_elim [consumes 1]:
assumes exec_call: "Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ ==> t"
assumes Normal:
 "∧bdy t'.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t';
     Γ⊨⟨c s t',Normal (return s t')⟩ ==> t]
    ==> P"
assumes Abrupt:
 "∧bdy t'.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Abrupt t';
     t = Abrupt (result_exn (return s t') t')]
    ==> P"
assumes Fault:
 "∧bdy f.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Fault f;
     t = Fault f]
    ==> P"
assumes Stuck:
 "∧bdy.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Stuck;
     t = Stuck]
    ==> P"
assumes Undef:
 "[Γ p = None; t = Stuck] ==> P"
shows "P"
  using exec_call
  apply (unfold call_exn_def)
  apply (cases "Γ p")
  apply  (erule exec_block_exn_Normal_elim)
  apply      (elim exec_Normal_elim_cases)
  apply       simp
  apply      simp
  apply     (elim exec_Normal_elim_cases)
  apply      simp
  apply     simp
  apply    (elim exec_Normal_elim_cases)
  apply     simp
  apply    simp
  apply   (elim exec_Normal_elim_cases)
  apply    simp
  apply   (rule Undef,assumption,assumption)
  apply  (rule Undef,assumption+)
  apply (erule exec_block_exn_Normal_elim)
  apply     (elim exec_Normal_elim_cases)
  apply      simp
  apply      (rule Normal,assumption+)
  apply     simp
  apply    (elim exec_Normal_elim_cases)
  apply     simp
  apply     (rule Abrupt,assumption+)
  apply    simp
  apply   (elim exec_Normal_elim_cases)
  apply    simp
  apply   (rule Fault, assumption+)
  apply   simp
  apply  (elim exec_Normal_elim_cases)
  apply   simp
  apply  (rule Stuck,assumption,assumption,assumption)
  apply  simp
  apply (rule Undef,assumption+)
  done

lemma exec_call_Normal_elim [consumes 1]:
assumes exec_call: "Γ⊨⟨call init p return c,Normal s⟩ ==> t"
assumes Normal:
 "∧bdy t'.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Normal t';
     Γ⊨⟨c s t',Normal (return s t')⟩ ==> t]
    ==> P"
assumes Abrupt:
 "∧bdy t'.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Abrupt t';
     t = Abrupt (return s t')]
    ==> P"
assumes Fault:
 "∧bdy f.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Fault f;
     t = Fault f]
    ==> P"
assumes Stuck:
 "∧bdy.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ ==> Stuck;
     t = Stuck]
    ==> P"
assumes Undef:
 "[Γ p = None; t = Stuck] ==> P"
shows "P"
  using exec_call [simplified call_call_exn] Normal Abrupt Fault Stuck Undef
  by (rule exec_call_exn_Normal_elim)


lemma exec_dynCall:
          "[Γ⊨⟨call init (p s) return c,Normal s⟩ ==> t]
           ==>
           Γ⊨⟨dynCall init p return c,Normal s⟩ ==> t"
apply (simp add: dynCall_def)
by (rule DynCom)

lemma exec_dynCall_exn:
          "[Γ⊨⟨call_exn init (p s) return result_exn c,Normal s⟩ ==> t]
           ==>
           Γ⊨⟨dynCall_exn f UNIV init p return result_exn c,Normal s⟩ ==> t"
apply (simp add: dynCall_exn_def)
  by (rule DynCom)

lemma exec_dynCall_Normal_elim:
  assumes exec: "Γ⊨⟨dynCall init p return c,Normal s⟩ ==> t"
  assumes call: "Γ⊨⟨call init (p s) return c,Normal s⟩ ==> t ==> P"
  shows "P"
  using exec
  apply (simp add: dynCall_def)
  apply (erule exec_Normal_elim_cases)
  apply (rule call,assumption)
  done

lemma exec_guards_Normal_elim_cases [consumes 1, case_names noFault someFault]:
  assumes exec_guards: "Γ⊨⟨guards gs c,Normal s⟩ ==> t"
  assumes noFault: "∀f g. (f, g) ∈ set gs ⟶ s ∈ g ==> Γ⊨⟨c,Normal s⟩ ==> t ==> P"
  assumes someFault: "∧f g. find (λ(f,g). s ∉ g) gs = Some (f, g) ==> t = Fault f ==> P"
  shows "P"
  using exec_guards noFault someFault
proof (induct gs)
  case Nil
  then show ?case by simp
next
  case (Cons pg gs)
  obtain f g where pg: "pg = (f, g)"
    by (cases pg) auto
  show ?thesis
  proof (cases "s ∈ g")
    case True
    from Cons.prems(1) have exec_gs: "Γ⊨ ⟨guards gs c,Normal s⟩ ==> t"
      by (simp add: pg) (meson True pg exec_Normal_elim_cases)

    from Cons.hyps [OF exec_gs] Cons.prems(2,3)
    show ?thesis
      by (simp add: pg True)
  next
    case False
    from Cons.prems(1) have t: "t = Fault f"
      by (simp add: pg) (meson False pg exec_Normal_elim_cases)

    from t Cons.prems(3)
    show ?thesis
      by (simp add: pg False)
  qed
qed

lemma exec_guards_noFault:
  assumes exec: "Γ⊨⟨c,Normal s⟩ ==> t"
  assumes noFault: "∀f g. (f, g) ∈ set gs ⟶ s ∈ g"
  shows "Γ⊨⟨guards gs c,Normal s⟩ ==> t"
  using exec noFault by (induct gs) (auto intro: exec.intros)

lemma exec_guards_Fault:
  assumes Fault: "find (λ(f,g). s ∉ g) gs = Some (f, g)"
  shows "Γ⊨⟨guards gs c,Normal s⟩ ==> Fault f"
  using Fault by (induct gs) (auto intro: exec.intros  split: prod.splits if_split_asm)

lemma exec_guards_DynCom:
  assumes exec_c: "Γ⊨⟨guards gs (c s), Normal s⟩ ==> t"
  shows "Γ⊨⟨guards gs (DynCom c), Normal s⟩ ==> t"
  using exec_c apply (induct gs)
   apply (fastforce intro: exec.intros)
  apply simp
  by (metis exec.Guard exec.GuardFault exec_Normal_elim_cases)

lemma exec_guards_DynCom_Normal_elim:
  assumes exec: "Γ⊨⟨guards gs (DynCom c), Normal s⟩ ==> t"
  assumes call: "Γ⊨⟨guards gs (c s), Normal s⟩ ==> t ==> P"
  shows "P"
  using exec call proof (induct gs)
  case Nil
  then show ?case
    apply simp
    apply (erule exec_Normal_elim_cases)
    apply simp
    done
next
  case (Cons g gs)
  then show ?case
    apply (cases g)
    apply simp
    apply (erule exec_Normal_elim_cases)
     apply simp
     apply (meson Guard)
    apply simp
    apply (meson GuardFault)
    done
qed

lemma exec_maybe_guard_DynCom:
  assumes exec_c: "Γ⊨⟨maybe_guard f g (c s), Normal s⟩ ==> t"
  shows "Γ⊨⟨maybe_guard f g (DynCom c), Normal s⟩ ==> t"
  using exec_c
  by (metis DynCom Guard GuardFault exec_Normal_elim_cases(5) maybe_guard_def)

lemma exec_maybe_guard_Normal_elim_cases [consumes 1, case_names noFault someFault]:
  assumes exec_guards: "Γ⊨⟨maybe_guard f g c,Normal s⟩ ==> t"
  assumes noFault: "s ∈ g ==> Γ⊨⟨c,Normal s⟩ ==> t ==> P"
  assumes someFault: "s ∉ g ==> t = Fault f ==> P"
  shows "P"
  using exec_guards noFault someFault
  by (metis UNIV_I exec_Normal_elim_cases(5) maybe_guard_def)

lemma exec_maybe_guard_noFault:
  assumes exec: "Γ⊨⟨c,Normal s⟩ ==> t"
  assumes noFault: "s ∈ g"
  shows "Γ⊨⟨maybe_guard f g c,Normal s⟩ ==> t"
  using exec noFault
  by (simp add: Guard maybe_guard_def)

lemma exec_maybe_guard_Fault:
  assumes Fault: "s ∉ g"
  shows "Γ⊨⟨maybe_guard f g c,Normal s⟩ ==> Fault f"
  using Fault
  by (metis GuardFault iso_tuple_UNIV_I maybe_guard_def)

lemma exec_maybe_guard_DynCom_Normal_elim:
  assumes exec: "Γ⊨⟨maybe_guard f g (DynCom c), Normal s⟩ ==> t"
  assumes call: "Γ⊨⟨maybe_guard f g (c s), Normal s⟩ ==> t ==> P"
  shows "P"
  using exec call
  apply (cases "g=UNIV")
  subgoal
    apply simp
    apply (erule exec_Normal_elim_cases)
    apply simp
    done
  subgoal
    apply (simp add: maybe_guard_def)
    apply (erule exec_Normal_elim_cases)
     apply (meson Guard exec_Normal_elim_cases(12))
    by (meson GuardFault)
  done


lemma exec_dynCall_exn_Normal_elim:
  assumes exec: "Γ⊨⟨dynCall_exn f g init p return result_exn c,Normal s⟩ ==> t"
  assumes call: "Γ⊨⟨maybe_guard f g (call_exn init (p s) return result_exn c),Normal s⟩ ==> t ==> P"
  shows "P"
  using exec
  apply (simp add: dynCall_exn_def)
  apply (erule exec_maybe_guard_DynCom_Normal_elim)
  by (rule call)


lemma exec_Call_body:
  "Γ p=Some bdy ==>
   Γ⊨⟨Call p,s⟩ ==> t = Γ⊨⟨the (Γ p),s⟩ ==> t"
apply (rule)
apply (fastforce elim: exec_elim_cases )
apply (cases s)
apply   (cases t)
apply (fastforce intro: exec.intros dest: Fault_end Abrupt_end Stuck_end)+
done

lemma exec_Seq': "[Γ⊨⟨c1,s⟩ ==> s'; Γ⊨⟨c2,s'⟩ ==> s'']
             ==>
             Γ⊨⟨Seq c1 c2,s⟩ ==> s''"
  apply (cases s)
  apply    (fastforce intro: exec.intros)
  apply   (fastforce dest: Abrupt_end)
  apply  (fastforce dest: Fault_end)
  apply (fastforce dest: Stuck_end)
  done


lemma exec_assoc: "Γ⊨⟨Seq c1 (Seq c2 c3),s⟩ ==> t = Γ⊨⟨Seq (Seq c1 c2) c3,s⟩ ==> t"
  by (blast elim!: exec_elim_cases intro: exec_Seq' )


(* ************************************************************************* *)
subsection ‹Big-Step Execution with Recursion Limit: ‹Γ⊨⟨c, s⟩ =n==> t››
(* ************************************************************************* *)

inductive "execn"::"[('s,'p,'f) body,('s,'p,'f) com,('s,'f) xstate,nat,('s,'f) xstate]
                      ==> bool" (‹_⊨ ⟨_,_⟩ =_==> _›  [60,20,98,65,98] 89)
  for Γ::"('s,'p,'f) body"
where
  Skip: "Γ⊨⟨Skip,Normal s⟩ =n==> Normal s"
| Guard: "[s∈g; Γ⊨⟨c,Normal s⟩ =n==> t]
          ==>
          Γ⊨⟨Guard f g c,Normal s⟩ =n==> t"

| GuardFault: "s∉g ==> Γ⊨⟨Guard f g c,Normal s⟩ =n==> Fault f"

| FaultProp [intro,simp]: "Γ⊨⟨c,Fault f⟩ =n==> Fault f"

| Basic: "Γ⊨⟨Basic f,Normal s⟩ =n==> Normal (f s)"

| Spec: "(s,t) ∈ r
         ==>
         Γ⊨⟨Spec r,Normal s⟩ =n==> Normal t"

| SpecStuck: "∀t. (s,t) ∉ r
              ==>
              Γ⊨⟨Spec r,Normal s⟩ =n==> Stuck"

| Seq: "[Γ⊨⟨c₁,Normal s⟩ =n==> s'; Γ⊨⟨c₂,s'⟩ =n==> t]
        ==>
        Γ⊨⟨Seq c₁ c₂,Normal s⟩ =n==> t"

| CondTrue: "[s ∈ b; Γ⊨⟨c₁,Normal s⟩ =n==> t]
             ==>
             Γ⊨⟨Cond b c₁ c₂,Normal s⟩ =n==> t"

| CondFalse: "[s ∉ b; Γ⊨⟨c₂,Normal s⟩ =n==> t]
              ==>
              Γ⊨⟨Cond b c₁ c₂,Normal s⟩ =n==> t"

| WhileTrue: "[s ∈ b; Γ⊨⟨c,Normal s⟩ =n==> s';
              Γ⊨⟨While b c,s'⟩ =n==> t]
              ==>
              Γ⊨⟨While b c,Normal s⟩ =n==> t"

| WhileFalse: "[s ∉ b]
               ==>
               Γ⊨⟨While b c,Normal s⟩ =n==> Normal s"

| Call:  "[Γ p=Some bdy;Γ⊨⟨bdy,Normal s⟩ =n==> t]
          ==>
          Γ⊨⟨Call p ,Normal s⟩ =Suc n==> t"

| CallUndefined: "[Γ p=None]
                 ==>
                 Γ⊨⟨Call p ,Normal s⟩ =Suc n==> Stuck"

| StuckProp [intro,simp]: "Γ⊨⟨c,Stuck⟩ =n==> Stuck"

| DynCom:  "[Γ⊨⟨(c s),Normal s⟩ =n==> t]
             ==>
             Γ⊨⟨DynCom c,Normal s⟩ =n==> t"

| Throw: "Γ⊨⟨Throw,Normal s⟩ =n==> Abrupt s"

| AbruptProp [intro,simp]: "Γ⊨⟨c,Abrupt s⟩ =n==> Abrupt s"

| CatchMatch: "[Γ⊨⟨c₁,Normal s⟩ =n==> Abrupt s'; Γ⊨⟨c₂,Normal s'⟩ =n==> t]
               ==>
               Γ⊨⟨Catch c₁ c₂,Normal s⟩ =n==> t"
| CatchMiss: "[Γ⊨⟨c₁,Normal s⟩ =n==> t; ¬isAbr t]
               ==>
               Γ⊨⟨Catch c₁ c₂,Normal s⟩ =n==> t"

inductive_cases execn_elim_cases [cases set]:
  "Γ⊨⟨c,Fault f⟩ =n==> t"
  "Γ⊨⟨c,Stuck⟩ =n==> t"
  "Γ⊨⟨c,Abrupt s⟩ =n==> t"
  "Γ⊨⟨Skip,s⟩ =n==> t"
  "Γ⊨⟨Seq c1 c2,s⟩ =n==> t"
  "Γ⊨⟨Guard f g c,s⟩ =n==> t"
  "Γ⊨⟨Basic f,s⟩ =n==> t"
  "Γ⊨⟨Spec r,s⟩ =n==> t"
  "Γ⊨⟨Cond b c1 c2,s⟩ =n==> t"
  "Γ⊨⟨While b c,s⟩ =n==> t"
  "Γ⊨⟨Call p ,s⟩ =n==> t"
  "Γ⊨⟨DynCom c,s⟩ =n==> t"
  "Γ⊨⟨Throw,s⟩ =n==> t"
  "Γ⊨⟨Catch c1 c2,s⟩ =n==> t"


inductive_cases execn_Normal_elim_cases [cases set]:
  "Γ⊨⟨c,Fault f⟩ =n==> t"
  "Γ⊨⟨c,Stuck⟩ =n==> t"
  "Γ⊨⟨c,Abrupt s⟩ =n==> t"
  "Γ⊨⟨Skip,Normal s⟩ =n==> t"
  "Γ⊨⟨Guard f g c,Normal s⟩ =n==> t"
  "Γ⊨⟨Basic f,Normal s⟩ =n==> t"
  "Γ⊨⟨Spec r,Normal s⟩ =n==> t"
  "Γ⊨⟨Seq c1 c2,Normal s⟩ =n==> t"
  "Γ⊨⟨Cond b c1 c2,Normal s⟩ =n==> t"
  "Γ⊨⟨While b c,Normal s⟩ =n==> t"
  "Γ⊨⟨Call p,Normal s⟩ =n==> t"
  "Γ⊨⟨DynCom c,Normal s⟩ =n==> t"
  "Γ⊨⟨Throw,Normal s⟩ =n==> t"
  "Γ⊨⟨Catch c1 c2,Normal s⟩ =n==> t"

lemma execn_Skip': "Γ⊨⟨Skip,t⟩ =n==> t"
  by (cases t) (auto intro: execn.intros)

lemma execn_Fault_end: assumes exec: "Γ⊨⟨c,s⟩ =n==> t" and s: "s=Fault f"
  shows "t=Fault f"
using exec s by (induct) auto

lemma execn_Stuck_end: assumes exec: "Γ⊨⟨c,s⟩ =n==> t" and s: "s=Stuck"
  shows "t=Stuck"
using exec s by (induct) auto

lemma execn_Abrupt_end: assumes exec: "Γ⊨⟨c,s⟩ =n==> t" and s: "s=Abrupt s'"
  shows "t=Abrupt s'"
using exec s by (induct) auto

lemma execn_block_exn:
  "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Normal t; Γ⊨⟨c s t,Normal (return s t)⟩ =n==> u]
  ==>
  Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ =n==> u"
apply (unfold block_exn_def)
  by (fastforce intro: execn.intros)

lemma execn_block:
  "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Normal t; Γ⊨⟨c s t,Normal (return s t)⟩ =n==> u]
  ==>
  Γ⊨⟨block init bdy return c,Normal s⟩ =n==> u"
  unfolding block_def
  by (rule execn_block_exn)

lemma execn_block_exnAbrupt:
     "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Abrupt t]
       ==>
       Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ =n==> Abrupt (result_exn (return s t) t)"
apply (unfold block_exn_def)
  by (fastforce intro: execn.intros)

lemma execn_blockAbrupt:
     "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Abrupt t]
       ==>
       Γ⊨⟨block init bdy return c,Normal s⟩ =n==> Abrupt (return s t)"
  unfolding block_def
  by (rule execn_block_exnAbrupt)

lemma execn_block_exnFault:
  "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Fault f]
   ==>
  Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ =n==> Fault f"
apply (unfold block_exn_def)
  by (fastforce intro: execn.intros)

lemma execn_blockFault:
  "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Fault f]
   ==>
  Γ⊨⟨block init bdy return c,Normal s⟩ =n==> Fault f"
  unfolding block_def
by (rule execn_block_exnFault)

lemma execn_block_exnStuck:
  "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Stuck]
  ==>
  Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ =n==> Stuck"
apply (unfold block_exn_def)
  by (fastforce intro: execn.intros)

lemma execn_blockStuck:
  "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Stuck]
  ==>
  Γ⊨⟨block init bdy return c,Normal s⟩ =n==> Stuck"
  unfolding block_def
by (rule execn_block_exnStuck)


lemma execn_call:
 "[Γ p=Some bdy;Γ⊨⟨bdy,Normal (init s)⟩ =n==> Normal t;
   Γ⊨⟨c s t,Normal (return s t)⟩ =Suc n==> u]
  ==>
  Γ⊨⟨call init p return c,Normal s⟩ =Suc n==> u"
apply (simp add: call_def)
apply (rule execn_block)
apply  (erule (1) Call)
apply assumption
done

lemma execn_call_exn:
 "[Γ p=Some bdy;Γ⊨⟨bdy,Normal (init s)⟩ =n==> Normal t;
   Γ⊨⟨c s t,Normal (return s t)⟩ =Suc n==> u]
  ==>
  Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ =Suc n==> u"
apply (simp add: call_exn_def)
apply (rule execn_block_exn)
apply  (erule (1) Call)
apply assumption
done


lemma execn_callAbrupt:
 "[Γ p=Some bdy;Γ⊨⟨bdy,Normal (init s)⟩ =n==> Abrupt t]
  ==>
  Γ⊨⟨call init p return c,Normal s⟩ =Suc n==> Abrupt (return s t)"
apply (simp add: call_def)
apply (rule execn_blockAbrupt)
apply (erule (1) Call)
done

lemma execn_call_exnAbrupt:
 "[Γ p=Some bdy;Γ⊨⟨bdy,Normal (init s)⟩ =n==> Abrupt t]
  ==>
  Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ =Suc n==> Abrupt (result_exn (return s t) t)"
apply (simp add: call_exn_def)
apply (rule execn_block_exnAbrupt)
apply (erule (1) Call)
  done

lemma execn_callFault:
             "[Γ p=Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =n==> Fault f]
               ==>
              Γ⊨⟨call init p return c,Normal s⟩ =Suc n==> Fault f"
apply (simp add: call_def)
apply (rule execn_blockFault)
apply (erule (1) Call)
done

lemma execn_call_exnFault:
             "[Γ p=Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =n==> Fault f]
               ==>
              Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ =Suc n==> Fault f"
apply (simp add: call_exn_def)
apply (rule execn_block_exnFault)
apply (erule (1) Call)
done

lemma execn_callStuck:
          "[Γ p=Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =n==> Stuck]
           ==>
           Γ⊨⟨call init p return c,Normal s⟩ =Suc n==> Stuck"
apply (simp add: call_def)
apply (rule execn_blockStuck)
apply (erule (1) Call)
done

lemma execn_call_exnStuck:
          "[Γ p=Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =n==> Stuck]
           ==>
           Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ =Suc n==> Stuck"
apply (simp add: call_exn_def)
apply (rule execn_block_exnStuck)
apply (erule (1) Call)
  done

lemma  execn_callUndefined:
       "[Γ p=None]
        ==>
        Γ⊨⟨call init p return c,Normal s⟩ =Suc n==> Stuck"
apply (simp add: call_def)
apply (rule execn_blockStuck)
apply (erule CallUndefined)
done

lemma  execn_call_exnUndefined:
       "[Γ p=None]
        ==>
        Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ =Suc n==> Stuck"
apply (simp add: call_exn_def)
apply (rule execn_block_exnStuck)
apply (erule CallUndefined)
done

lemma execn_block_exn_Normal_elim [consumes 1]:
assumes execn_block: "Γ⊨⟨block_exn init bdy return result_exn c,Normal s⟩ =n==> t"
assumes Normal:
 "∧t'.
    [Γ⊨⟨bdy,Normal (init s)⟩ =n==> Normal t';
     Γ⊨⟨c s t',Normal (return s t')⟩ =n==> t]
    ==> P"
assumes Abrupt:
 "∧t'.
    [Γ⊨⟨bdy,Normal (init s)⟩ =n==> Abrupt t';
     t = Abrupt (result_exn (return s t') t')]
    ==> P"
assumes Fault:
 "∧f.
    [Γ⊨⟨bdy,Normal (init s)⟩ =n==> Fault f;
     t = Fault f]
    ==> P"
assumes Stuck:
 "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Stuck;
     t = Stuck]
    ==> P"
assumes Undef:
 "[Γ p = None; t = Stuck] ==> P"
shows "P"
  using execn_block
apply (unfold block_exn_def)
apply (elim execn_Normal_elim_cases)
apply simp_all
apply  (case_tac s')
apply     simp_all
apply     (elim execn_Normal_elim_cases)
apply     simp
apply    (drule execn_Abrupt_end) apply simp
apply    (erule execn_Normal_elim_cases)
apply    simp
apply    (rule Abrupt,assumption+)
apply   (drule execn_Fault_end) apply simp
apply   (erule execn_Normal_elim_cases)
apply   simp
apply  (drule execn_Stuck_end) apply simp
apply  (erule execn_Normal_elim_cases)
apply  simp
apply (case_tac s')
apply    simp_all
apply   (elim execn_Normal_elim_cases)
apply   simp
apply   (rule Normal,assumption+)
apply  (drule execn_Fault_end) apply simp
apply  (rule Fault,assumption+)
apply (drule execn_Stuck_end) apply simp
apply (rule Stuck,assumption+)
done

lemma execn_block_Normal_elim [consumes 1]:
assumes execn_block: "Γ⊨⟨block init bdy return c,Normal s⟩ =n==> t"
assumes Normal:
 "∧t'.
    [Γ⊨⟨bdy,Normal (init s)⟩ =n==> Normal t';
     Γ⊨⟨c s t',Normal (return s t')⟩ =n==> t]
    ==> P"
assumes Abrupt:
 "∧t'.
    [Γ⊨⟨bdy,Normal (init s)⟩ =n==> Abrupt t';
     t = Abrupt (return s t')]
    ==> P"
assumes Fault:
 "∧f.
    [Γ⊨⟨bdy,Normal (init s)⟩ =n==> Fault f;
     t = Fault f]
    ==> P"
assumes Stuck:
 "[Γ⊨⟨bdy,Normal (init s)⟩ =n==> Stuck;
     t = Stuck]
    ==> P"
assumes Undef:
 "[Γ p = None; t = Stuck] ==> P"
shows "P"
  using execn_block [unfolded block_def] Normal Abrupt Fault Stuck Undef
  by (rule execn_block_exn_Normal_elim)

lemma execn_call_exn_Normal_elim [consumes 1]:
assumes exec_call: "Γ⊨⟨call_exn init p return result_exn c,Normal s⟩ =n==> t"
assumes Normal:
 "∧bdy i t'.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =i==> Normal t';
     Γ⊨⟨c s t',Normal (return s t')⟩ =Suc i==> t; n = Suc i]
    ==> P"
assumes Abrupt:
 "∧bdy i t'.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =i==> Abrupt t'; n = Suc i;
     t = Abrupt (result_exn (return s t') t')]
    ==> P"
assumes Fault:
 "∧bdy i f.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =i==> Fault f; n = Suc i;
     t = Fault f]
    ==> P"
assumes Stuck:
 "∧bdy i.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =i==> Stuck; n = Suc i;
     t = Stuck]
    ==> P"
assumes Undef:
 "∧i. [Γ p = None; n = Suc i; t = Stuck] ==> P"
shows "P"
  using exec_call
  apply (unfold call_exn_def)
  apply (cases n)
  apply  (simp only: block_exn_def)
  apply  (fastforce elim: execn_Normal_elim_cases)
  apply (cases "Γ p")
  apply  (erule execn_block_exn_Normal_elim)
  apply      (elim execn_Normal_elim_cases)
  apply       simp
  apply      simp
  apply     (elim execn_Normal_elim_cases)
  apply      simp
  apply     simp
  apply    (elim execn_Normal_elim_cases)
  apply     simp
  apply    simp
  apply   (elim execn_Normal_elim_cases)
  apply    simp
  apply   (rule Undef,assumption,assumption,assumption)
  apply  (rule Undef,assumption+)
  apply (erule execn_block_exn_Normal_elim)
  apply     (elim execn_Normal_elim_cases)
  apply      simp
  apply      (rule Normal,assumption+)
  apply     simp
  apply    (elim execn_Normal_elim_cases)
  apply     simp
  apply     (rule Abrupt,assumption+)
  apply    simp
  apply   (elim execn_Normal_elim_cases)
  apply    simp
  apply   (rule Fault,assumption+)
  apply   simp
  apply  (elim execn_Normal_elim_cases)
  apply   simp
  apply  (rule Stuck,assumption,assumption,assumption,assumption)
  apply  (rule Undef,assumption,assumption,assumption)
  apply (rule Undef,assumption+)
  done


lemma execn_call_Normal_elim [consumes 1]:
assumes exec_call: "Γ⊨⟨call init p return c,Normal s⟩ =n==> t"
assumes Normal:
 "∧bdy i t'.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =i==> Normal t';
     Γ⊨⟨c s t',Normal (return s t')⟩ =Suc i==> t; n = Suc i]
    ==> P"
assumes Abrupt:
 "∧bdy i t'.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =i==> Abrupt t'; n = Suc i;
     t = Abrupt (return s t')]
    ==> P"
assumes Fault:
 "∧bdy i f.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =i==> Fault f; n = Suc i;
     t = Fault f]
    ==> P"
assumes Stuck:
 "∧bdy i.
    [Γ p = Some bdy; Γ⊨⟨bdy,Normal (init s)⟩ =i==> Stuck; n = Suc i;
     t = Stuck]
    ==> P"
assumes Undef:
 "∧i. [Γ p = None; n = Suc i; t = Stuck] ==> P"
shows "P"
  using exec_call [simplified call_call_exn] Normal Abrupt Fault Stuck Undef
  by (rule execn_call_exn_Normal_elim)


lemma execn_dynCall:
  "[Γ⊨⟨call init (p s) return c,Normal s⟩ =n==> t]
  ==>
  Γ⊨⟨dynCall init p return c,Normal s⟩ =n==> t"
apply (simp add: dynCall_def)
by (rule DynCom)

lemma execn_dynCall_exn:
  "[Γ⊨⟨call_exn init (p s) return result_exn c,Normal s⟩ =n==> t]
  ==>
  Γ⊨⟨dynCall_exn f UNIV init p return result_exn c,Normal s⟩ =n==> t"
apply (simp add: dynCall_exn_def)
  by (rule DynCom)

lemma execn_dynCall_Normal_elim:
  assumes exec: "Γ⊨⟨dynCall init p return c,Normal s⟩ =n==> t"
  assumes "Γ⊨⟨call init (p s) return c,Normal s⟩ =n==> t ==> P"
  shows "P"
  using exec
  apply (simp add: dynCall_def)
  apply (erule execn_Normal_elim_cases)
  apply fact
  done

lemma execn_guards_Normal_elim_cases [consumes 1, case_names noFault someFault]:
  assumes exec_guards: "Γ⊨⟨guards gs c,Normal s⟩ =n==> t"
  assumes noFault: "∀f g. (f, g) ∈ set gs ⟶ s ∈ g ==> Γ⊨⟨c,Normal s⟩ =n==> t ==> P"
  assumes someFault: "∧f g. find (λ(f,g). s ∉ g) gs = Some (f, g) ==> t = Fault f ==> P"
  shows "P"
  using exec_guards noFault someFault
proof (induct gs)
  case Nil
  then show ?case by simp
next
  case (Cons pg gs)
  obtain f g where pg: "pg = (f, g)"
    by (cases pg) auto
  show ?thesis
  proof (cases "s ∈ g")
    case True
    from Cons.prems(1) have exec_gs: "Γ⊨ ⟨guards gs c,Normal s⟩ =n==> t"
      by (simp add: pg) (meson True pg execn_Normal_elim_cases)

    from Cons.hyps [OF exec_gs] Cons.prems(2,3)
    show ?thesis
      by (simp add: pg True)
  next
    case False
    from Cons.prems(1) have t: "t = Fault f"
      by (simp add: pg) (meson False pg execn_Normal_elim_cases)

    from t Cons.prems(3)
    show ?thesis
      by (simp add: pg False)
  qed
qed

lemma execn_maybe_guard_Normal_elim_cases [consumes 1, case_names noFault someFault]:
  assumes exec_guards: "Γ⊨⟨maybe_guard f g c,Normal s⟩ =n==> t"
  assumes noFault: "s ∈ g ==> Γ⊨⟨c,Normal s⟩ =n==> t ==> P"
  assumes someFault: "s ∉ g ==> t = Fault f ==> P"
  shows "P"
  using exec_guards noFault someFault
  by (metis UNIV_I execn_Normal_elim_cases(5) maybe_guard_def)

lemma execn_guards_noFault:
  assumes exec: "Γ⊨⟨c,Normal s⟩ =n==> t"
  assumes noFault: "∀f g. (f, g) ∈ set gs ⟶ s ∈ g"
  shows "Γ⊨⟨guards gs c,Normal s⟩ =n==> t"
  using exec noFault by (induct gs) (auto intro: execn.intros)

lemma execn_guards_Fault:
  assumes Fault: "find (λ(f,g). s ∉ g) gs = Some (f, g)"
  shows "Γ⊨⟨guards gs c,Normal s⟩ =n==> Fault f"
  using Fault by (induct gs) (auto intro: execn.intros  split: prod.splits if_split_asm)

lemma execn_maybe_guard_noFault:
  assumes exec: "Γ⊨⟨c,Normal s⟩ =n==> t"
  assumes noFault: "s ∈ g"
  shows "Γ⊨⟨maybe_guard f g c,Normal s⟩ =n==> t"
  using exec noFault
  by (auto intro: execn.intros simp add: maybe_guard_def)

lemma execn_maybe_guard_Fault:
  assumes Fault: "s ∉ g"
  shows "Γ⊨⟨maybe_guard f g c,Normal s⟩ =n==> Fault f"
  using Fault by (auto simp add: maybe_guard_def intro: execn.intros  split: prod.splits if_split_asm)

lemma execn_guards_DynCom_Normal_elim:
  assumes exec: "Γ⊨⟨guards gs (DynCom c), Normal s⟩ =n==> t"
  assumes call: "Γ⊨⟨guards gs (c s), Normal s⟩ =n==> t ==> P"
  shows "P"
  using exec call proof (induct gs)
  case Nil
  then show ?case
    apply simp
    apply (erule execn_Normal_elim_cases)
    apply simp
    done
next
  case (Cons g gs)
  then show ?case
    apply (cases g)
    apply simp
    apply (erule execn_Normal_elim_cases)
     apply simp
     apply (meson execn.Guard)
    apply simp
    apply (meson execn.GuardFault)
    done
qed

lemma execn_maybe_guard_DynCom_Normal_elim:
  assumes exec: "Γ⊨⟨maybe_guard f g (DynCom c), Normal s⟩ =n==> t"
  assumes call: "Γ⊨⟨maybe_guard f g (c s), Normal s⟩ =n==> t ==> P"
  shows "P"
  using exec call
  by (metis execn.Guard execn.GuardFault execn_Normal_elim_cases(12) execn_Normal_elim_cases(5) maybe_guard_def)

lemma execn_guards_DynCom:
  assumes exec_c: "Γ⊨⟨guards gs (c s), Normal s⟩ =n==> t"
  shows "Γ⊨⟨guards gs (DynCom c), Normal s⟩ =n==> t"
  using exec_c apply (induct gs)
   apply (fastforce intro: execn.intros)
  apply simp
  by (metis execn.Guard execn.GuardFault execn_Normal_elim_cases)

lemma execn_maybe_guard_DynCom:
  assumes exec_c: "Γ⊨⟨maybe_guard f g (c s), Normal s⟩ =n==> t"
  shows "Γ⊨⟨maybe_guard f g (DynCom c), Normal s⟩ =n==> t"
  using exec_c
  apply (cases "g = UNIV")
  subgoal
    apply simp
    apply (rule execn.intros)
    apply simp
    done
  subgoal
    apply (simp add: maybe_guard_def)
    by (metis execn.DynCom execn.Guard execn.GuardFault execn_Normal_elim_cases(5))
  done


lemma execn_dynCall_exn_Normal_elim:
  assumes exec: "Γ⊨⟨dynCall_exn f g init p return result_exn c,Normal s⟩ =n==> t"
  assumes "Γ⊨⟨maybe_guard f g (call_exn init (p s) return result_exn c),Normal s⟩ =n==> t ==> P"
  shows "P"
  using exec
  apply (simp add: dynCall_exn_def)
  apply (erule execn_maybe_guard_DynCom_Normal_elim)
  apply fact
  done

lemma  execn_Seq':
       "[Γ⊨⟨c1,s⟩ =n==> s'; Γ⊨⟨c2,s'⟩ =n==> s'']
        ==>
        Γ⊨⟨Seq c1 c2,s⟩ =n==> s''"
  apply (cases s)
  apply    (fastforce intro: execn.intros)
  apply   (fastforce dest: execn_Abrupt_end)
  apply  (fastforce dest: execn_Fault_end)
  apply (fastforce dest: execn_Stuck_end)
  done

lemma execn_mono:
 assumes exec: "Γ⊨⟨c,s⟩ =n==> t"
  shows "∧ m. n ≤ m ==> Γ⊨⟨c,s⟩ =m==> t"
using exec
by (induct) (auto intro: execn.intros dest: Suc_le_D)


lemma execn_Suc:
  "Γ⊨⟨c,s⟩ =n==> t ==> Γ⊨⟨c,s⟩ =Suc n==> t"
  by (rule execn_mono [OF _ le_refl [THEN le_SucI]])

lemma execn_assoc:
 "Γ⊨⟨Seq c1 (Seq c2 c3),s⟩ =n==> t = Γ⊨⟨Seq (Seq c1 c2) c3,s⟩ =n==> t"
  by (auto elim!: execn_elim_cases intro: execn_Seq')


lemma execn_to_exec:
  assumes execn: "Γ⊨⟨c,s⟩ =n==> t"
  shows "Γ⊨⟨c,s⟩ ==> t"
using execn
by induct (auto intro: exec.intros)

lemma exec_to_execn:
  assumes execn: "Γ⊨⟨c,s⟩ ==> t"
  shows "∃n. Γ⊨⟨c,s⟩ =n==> t"
using execn
proof (induct)
  case Skip thus ?case by (iprover intro: execn.intros)
next
  case Guard thus ?case by (iprover intro: execn.intros)
next
  case GuardFault thus ?case by (iprover intro: execn.intros)
next
 case FaultProp thus ?case by (iprover intro: execn.intros)
next
  case Basic thus ?case by (iprover intro: execn.intros)
next
  case Spec thus ?case by (iprover intro: execn.intros)
next
  case SpecStuck thus ?case by (iprover intro: execn.intros)
next
  case (Seq c1 s s' c2 s'')
  then obtain n m where
    "Γ⊨⟨c1,Normal s⟩ =n==> s'" "Γ⊨⟨c2,s'⟩ =m==> s''"
    by blast
  then have
    "Γ⊨⟨c1,Normal s⟩ =max n m==> s'"
    "Γ⊨⟨c2,s'⟩ =max n m==> s''"
    by (auto elim!: execn_mono intro: max.cobounded1 max.cobounded2)
  thus ?case
    by (iprover intro: execn.intros)
next
  case CondTrue thus ?case by (iprover intro: execn.intros)
next
  case CondFalse thus ?case by (iprover intro: execn.intros)
next
  case (WhileTrue s b c s' s'')
  then obtain n m where
    "Γ⊨⟨c,Normal s⟩ =n==> s'" "Γ⊨⟨While b c,s'⟩ =m==> s''"
    by blast
  then have
    "Γ⊨⟨c,Normal s⟩ =max n m==> s'" "Γ⊨⟨While b c,s'⟩ =max n m==> s''"
    by (auto elim!: execn_mono intro: max.cobounded1 max.cobounded2)
  with WhileTrue
  show ?case
    by (iprover intro: execn.intros)
next
  case WhileFalse thus ?case by (iprover intro: execn.intros)
next
  case Call thus ?case by (iprover intro: execn.intros)
next
  case CallUndefined thus ?case by (iprover intro: execn.intros)
next
  case StuckProp thus ?case by (iprover intro: execn.intros)
next
  case DynCom thus ?case by (iprover intro: execn.intros)
next
  case Throw thus ?case by (iprover intro: execn.intros)
next
  case AbruptProp thus ?case by (iprover intro: execn.intros)
next
  case (CatchMatch c1 s s' c2 s'')
  then obtain n m where
    "Γ⊨⟨c1,Normal s⟩ =n==> Abrupt s'" "Γ⊨⟨c2,Normal s'⟩ =m==> s''"
    by blast
  then have
    "Γ⊨⟨c1,Normal s⟩ =max n m==> Abrupt s'"
    "Γ⊨⟨c2,Normal s'⟩ =max n m==> s''"
    by (auto elim!: execn_mono intro: max.cobounded1 max.cobounded2)
  with CatchMatch.hyps show ?case
    by (iprover intro: execn.intros)
next
  case CatchMiss thus ?case by (iprover intro: execn.intros)
qed

theorem exec_iff_execn: "(Γ⊨⟨c,s⟩ ==> t) = (∃n. Γ⊨⟨c,s⟩ =n==> t)"
  by (iprover intro: exec_to_execn execn_to_exec)


definition nfinal_notin:: "('s,'p,'f) body ==> ('s,'p,'f) com ==> ('s,'f) xstate ==> nat
                       ==> ('s,'f) xstate set ==> bool"
  (‹_⊨ ⟨_,_⟩ =_==>∉_›  [60,20,98,65,60] 89) where
"Γ⊨ ⟨c,s⟩ =n==>∉T = (∀t. Γ⊨ ⟨c,s⟩ =n==> t ⟶ t∉T)"

definition final_notin:: "('s,'p,'f) body ==> ('s,'p,'f) com ==> ('s,'f) xstate
                       ==> ('s,'f) xstate set ==> bool"
  (‹_⊨ ⟨_,_⟩ ==>∉_›  [60,20,98,60] 89) where
"Γ⊨ ⟨c,s⟩ ==>∉T = (∀t. Γ⊨ ⟨c,s⟩ ==>t ⟶ t∉T)"

lemma final_notinI: "[∧t. Γ⊨⟨c,s⟩ ==> t ==> t ∉ T] ==> Γ⊨⟨c,s⟩ ==>∉T"
  by (simp add: final_notin_def)

lemma noFaultStuck_Call_body': "p ∈ dom Γ ==>
\<Gamma>⊨⟨Call p,Normal s⟩ ==>∉({Stuck} ∪ Fault ` (-F)) =
\<Gamma>⊨⟨the (Γ p),Normal s⟩ ==>∉({Stuck} ∪ Fault ` (-F))"
  by (clarsimp simp add: final_notin_def exec_Call_body)

lemma noFault_startn:
  assumes execn: "Γ⊨⟨c,s⟩ =n==> t" and t: "t≠Fault f"
  shows "s≠Fault f"
using execn t by (induct) auto

lemma noFault_start:
  assumes exec: "Γ⊨⟨c,s⟩ ==> t" and t: "t≠Fault f"
  shows "s≠Fault f"
using exec t by (induct) auto

lemma noStuck_startn:
  assumes execn: "Γ⊨⟨c,s⟩ =n==> t" and t: "t≠Stuck"
  shows "s≠Stuck"
using execn t by (induct) auto

lemma noStuck_start:
  assumes exec: "Γ⊨⟨c,s⟩ ==> t" and t: "t≠Stuck"
  shows "s≠Stuck"
using exec t by (induct) auto

lemma noAbrupt_startn:
  assumes execn: "Γ⊨⟨c,s⟩ =n==> t" and t: "∀t'. t≠Abrupt t'"
  shows "s≠Abrupt s'"
using execn t by (induct) auto

lemma noAbrupt_start:
  assumes exec: "Γ⊨⟨c,s⟩ ==> t" and t: "∀t'. t≠Abrupt t'"
  shows "s≠Abrupt s'"
using exec t by (induct) auto

lemma noFaultn_startD: "Γ⊨⟨c,s⟩ =n==> Normal t ==> s ≠ Fault f"
  by (auto dest: noFault_startn)

lemma noFaultn_startD': "t≠Fault f ==> Γ⊨⟨c,s⟩ =n==> t ==> s ≠ Fault f"
  by (auto dest: noFault_startn)

lemma noFault_startD: "Γ⊨⟨c,s⟩ ==> Normal t ==> s ≠ Fault f"
  by (auto dest: noFault_start)

lemma noFault_startD': "t≠Fault f==> Γ⊨⟨c,s⟩ ==> t ==> s ≠ Fault f"
  by (auto dest: noFault_start)

lemma noStuckn_startD: "Γ⊨⟨c,s⟩ =n==> Normal t ==> s ≠ Stuck"
  by (auto dest: noStuck_startn)

lemma noStuckn_startD': "t≠Stuck ==> Γ⊨⟨c,s⟩ =n==> t ==> s ≠ Stuck"
  by (auto dest: noStuck_startn)

lemma noStuck_startD: "Γ⊨⟨c,s⟩ ==> Normal t ==> s ≠ Stuck"
  by (auto dest: noStuck_start)

lemma noStuck_startD': "t≠Stuck ==> Γ⊨⟨c,s⟩ ==> t ==> s ≠ Stuck"
  by (auto dest: noStuck_start)

lemma noAbruptn_startD: "Γ⊨⟨c,s⟩ =n==> Normal t ==> s ≠ Abrupt s'"
  by (auto dest: noAbrupt_startn)

lemma noAbrupt_startD: "Γ⊨⟨c,s⟩ ==> Normal t ==> s ≠ Abrupt s'"
  by (auto dest: noAbrupt_start)

lemma noFaultnI: "[∧t. Γ⊨⟨c,s⟩ =n==>t ==> t≠Fault f] ==> Γ⊨⟨c,s⟩ =n==>∉{Fault f}"
  by (simp add: nfinal_notin_def)

lemma noFaultnI':
  assumes contr: "Γ⊨⟨c,s⟩ =n==> Fault f ==> False"
  shows "Γ⊨⟨c,s⟩ =n==>∉{Fault f}"
  proof (rule noFaultnI)
    fix t assume "Γ⊨⟨c,s⟩ =n==> t"
    with contr show "t ≠ Fault f"
      by (cases "t=Fault f") auto
  qed

lemma noFaultn_def': "Γ⊨⟨c,s⟩ =n==>∉{Fault f} = (¬Γ⊨⟨c,s⟩ =n==> Fault f)"
  apply rule
  apply  (fastforce simp add: nfinal_notin_def)
  apply (fastforce intro: noFaultnI')
  done

lemma noStucknI: "[∧t. Γ⊨⟨c,s⟩ =n==>t ==> t≠Stuck] ==> Γ⊨⟨c,s⟩ =n==>∉{Stuck}"
  by (simp add: nfinal_notin_def)

lemma noStucknI':
  assumes contr: "Γ⊨⟨c,s⟩ =n==> Stuck ==> False"
  shows "Γ⊨⟨c,s⟩ =n==>∉{Stuck}"
  proof (rule noStucknI)
    fix t assume "Γ⊨⟨c,s⟩ =n==> t"
    with contr show "t ≠ Stuck"
      by (cases t) auto
  qed

lemma noStuckn_def': "Γ⊨⟨c,s⟩ =n==>∉{Stuck} = (¬Γ⊨⟨c,s⟩ =n==> Stuck)"
  apply rule
  apply  (fastforce simp add: nfinal_notin_def)
  apply (fastforce intro: noStucknI')
  done


lemma noFaultI: "[∧t. Γ⊨⟨c,s⟩ ==>t ==> t≠Fault f] ==> Γ⊨⟨c,s⟩ ==>∉{Fault f}"
  by (simp add: final_notin_def)

lemma noFaultI':
  assumes contr: "Γ⊨⟨c,s⟩ ==> Fault f==> False"
  shows "Γ⊨⟨c,s⟩ ==>∉{Fault f}"
  proof (rule noFaultI)
    fix t assume "Γ⊨⟨c,s⟩ ==> t"
    with contr show "t ≠ Fault f"
      by (cases "t=Fault f") auto
  qed

lemma noFaultE:
  "[Γ⊨⟨c,s⟩ ==>∉{Fault f}; Γ⊨⟨c,s⟩ ==> Fault f] ==> P"
  by (auto simp add: final_notin_def)

lemma noFault_def': "Γ⊨⟨c,s⟩ ==>∉{Fault f} = (¬Γ⊨⟨c,s⟩ ==> Fault f)"
  apply rule
  apply  (fastforce simp add: final_notin_def)
  apply (fastforce intro: noFaultI')
  done


lemma noStuckI: "[∧t. Γ⊨⟨c,s⟩ ==>t ==> t≠Stuck] ==> Γ⊨⟨c,s⟩ ==>∉{Stuck}"
  by (simp add: final_notin_def)

lemma noStuckI':
  assumes contr: "Γ⊨⟨c,s⟩ ==> Stuck ==> False"
  shows "Γ⊨⟨c,s⟩ ==>∉{Stuck}"
  proof (rule noStuckI)
    fix t assume "Γ⊨⟨c,s⟩ ==> t"
    with contr show "t ≠ Stuck"
      by (cases t) auto
  qed

lemma noStuckE:
  "[Γ⊨⟨c,s⟩ ==>∉{Stuck}; Γ⊨⟨c,s⟩ ==> Stuck] ==> P"
  by (auto simp add: final_notin_def)

lemma noStuck_def': "Γ⊨⟨c,s⟩ ==>∉{Stuck} = (¬Γ⊨⟨c,s⟩ ==> Stuck)"
  apply rule
  apply  (fastforce simp add: final_notin_def)
  apply (fastforce intro: noStuckI')
  done


lemma noFaultn_execD: "[Γ⊨⟨c,s⟩ =n==>∉{Fault f}; Γ⊨⟨c,s⟩ =n==>t] ==> t≠Fault f"
  by (simp add: nfinal_notin_def)

lemma noFault_execD: "[Γ⊨⟨c,s⟩ ==>∉{Fault f}; Γ⊨⟨c,s⟩ ==>t] ==> t≠Fault f"
  by (simp add: final_notin_def)

lemma noFaultn_exec_startD: "[Γ⊨⟨c,s⟩ =n==>∉{Fault f}; Γ⊨⟨c,s⟩ =n==>t] ==> s≠Fault f"
  by (auto simp add: nfinal_notin_def dest: noFaultn_startD)

lemma noFault_exec_startD: "[Γ⊨⟨c,s⟩ ==>∉{Fault f}; Γ⊨⟨c,s⟩ ==>t] ==> s≠Fault f"
  by (auto simp add: final_notin_def dest: noFault_startD)

lemma noStuckn_execD: "[Γ⊨⟨c,s⟩ =n==>∉{Stuck}; Γ⊨⟨c,s⟩ =n==>t] ==> t≠Stuck"
  by (simp add: nfinal_notin_def)

lemma noStuck_execD: "[Γ⊨⟨c,s⟩ ==>∉{Stuck}; Γ⊨⟨c,s⟩ ==>t] ==> t≠Stuck"
  by (simp add: final_notin_def)

lemma noStuckn_exec_startD: "[Γ⊨⟨c,s⟩ =n==>∉{Stuck}; Γ⊨⟨c,s⟩ =n==>t] ==> s≠Stuck"
  by (auto simp add: nfinal_notin_def dest: noStuckn_startD)

lemma noStuck_exec_startD: "[Γ⊨⟨c,s⟩ ==>∉{Stuck}; Γ⊨⟨c,s⟩ ==>t] ==> s≠Stuck"
  by (auto simp add: final_notin_def dest: noStuck_startD)

lemma noFaultStuckn_execD:
  "[Γ⊨⟨c,s⟩ =n==>∉{Fault True,Fault False,Stuck}; Γ⊨⟨c,s⟩ =n==>t] ==>
       t∉{Fault True,Fault False,Stuck}"
  by (simp add: nfinal_notin_def)

lemma noFaultStuck_execD: "[Γ⊨⟨c,s⟩ ==>∉{Fault True,Fault False,Stuck}; Γ⊨⟨c,s⟩ ==>t]
 ==> t∉{Fault True,Fault False,Stuck}"
  by (simp add: final_notin_def)

lemma noFaultStuckn_exec_startD:
  "[Γ⊨⟨c,s⟩ =n==>∉{Fault True, Fault False,Stuck}; Γ⊨⟨c,s⟩ =n==>t]
   ==> s∉{Fault True,Fault False,Stuck}"
  by (auto simp add: nfinal_notin_def )

lemma noFaultStuck_exec_startD:
  "[Γ⊨⟨c,s⟩ ==>∉{Fault True, Fault False,Stuck}; Γ⊨⟨c,s⟩ ==>t]
  ==> s∉{Fault True,Fault False,Stuck}"
  by (auto simp add: final_notin_def )

lemma noStuck_Call:
  assumes noStuck: "Γ⊨⟨Call p,Normal s⟩ ==>∉{Stuck}"
  shows "p ∈ dom Γ"
proof (cases "p ∈ dom Γ")
  case True thus ?thesis by simp
next
  case False
  hence "Γ p = None" by auto
  hence "Γ⊨⟨Call p,Normal s⟩ ==>Stuck"
    by (rule exec.CallUndefined)
  with noStuck show ?thesis
    by (auto simp add: final_notin_def)
qed


lemma Guard_noFaultStuckD:
  assumes "Γ⊨⟨Guard f g c,Normal s⟩ ==>∉({Stuck} ∪ Fault ` (-F))"
  assumes "f ∉ F"
  shows "s ∈ g"
  using assms
  by (auto simp add: final_notin_def intro: exec.intros)


lemma final_notin_to_finaln:
  assumes notin: "Γ⊨⟨c,s⟩ ==>∉T"
  shows "Γ⊨⟨c,s⟩ =n==>∉T"
proof (clarsimp simp add: nfinal_notin_def)
  fix t assume "Γ⊨⟨c,s⟩ =n==> t" and "t∈T"
  with notin show "False"
    by (auto intro: execn_to_exec simp add: final_notin_def)
qed

lemma noFault_Call_body:
"Γ p=Some bdy==>
 Γ⊨⟨Call p ,Normal s⟩ ==>∉{Fault f} =
 Γ⊨⟨the (Γ p),Normal s⟩ ==>∉{Fault f}"
  by (simp add: noFault_def' exec_Call_body)

lemma noStuck_Call_body:
"Γ p=Some bdy==>
 Γ⊨⟨Call p,Normal s⟩ ==>∉{Stuck} =
 Γ⊨⟨the (Γ p),Normal s⟩ ==>∉{Stuck}"
  by (simp add: noStuck_def' exec_Call_body)

lemma exec_final_notin_to_execn: "Γ⊨⟨c,s⟩ ==>∉T ==> Γ⊨⟨c,s⟩ =n==>∉T"
  by (auto simp add: final_notin_def nfinal_notin_def dest: execn_to_exec)

lemma execn_final_notin_to_exec: "∀n. Γ⊨⟨c,s⟩ =n==>∉T ==> Γ⊨⟨c,s⟩ ==>∉T"
  by (auto simp add: final_notin_def nfinal_notin_def dest: exec_to_execn)

lemma exec_final_notin_iff_execn: "Γ⊨⟨c,s⟩ ==>∉T = (∀n. Γ⊨⟨c,s⟩ =n==>∉T)"
  by (auto intro: exec_final_notin_to_execn execn_final_notin_to_exec)

lemma Seq_NoFaultStuckD2:
  assumes noabort: "Γ⊨⟨Seq c1 c2,s⟩ ==>∉({Stuck} ∪ Fault ` F)"
  shows "∀t. Γ⊨⟨c1,s⟩ ==> t ⟶ t∉ ({Stuck} ∪ Fault ` F) ⟶
             Γ⊨⟨c2,t⟩ ==>∉({Stuck} ∪ Fault ` F)"
using noabort
by (auto simp add: final_notin_def intro: exec_Seq') lemma Seq_NoFaultStuckD1:
  assumes noabort: "Γ⊨⟨Seq c1 c2,s⟩ ==>∉({Stuck} ∪ Fault ` F)"
  shows "Γ⊨⟨c1,s⟩ ==>∉({Stuck} ∪ Fault ` F)"
proof (rule final_notinI)
  fix t
  assume exec_c1: "Γ⊨⟨c1,s⟩ ==> t"
  show "t ∉ {Stuck} ∪ Fault ` F"
  proof
    assume "t ∈ {Stuck} ∪ Fault ` F"
    moreover
    {
      assume "t = Stuck"
      with exec_c1
      have "Γ⊨⟨Seq c1 c2,s⟩ ==> Stuck"
        by (auto intro: exec_Seq')
      with noabort have False
        by (auto simp add: final_notin_def)
      hence False ..
    }
    moreover
    {
      assume "t ∈ Fault ` F"
      then obtain f where
      t: "t=Fault f" and f: "f ∈ F"
        by auto
      from t exec_c1
      have "Γ⊨⟨Seq c1 c2,s⟩ ==> Fault f"
        by (auto intro: exec_Seq')
      with noabort f have False
        by (auto simp add: final_notin_def)
      hence False ..
    }
    ultimately show False by auto
  qed
qed

lemma Seq_NoFaultStuckD2':
  assumes noabort: "Γ⊨⟨Seq c1 c2,s⟩ ==>∉({Stuck} ∪ Fault ` F)"
  shows "∀t. Γ⊨⟨c1,s⟩ ==> t ⟶ t∉ ({Stuck} ∪ Fault ` F) ⟶
             Γ⊨⟨c2,t⟩ ==>∉({Stuck} ∪ Fault ` F)"
using noabort
by (auto simp add: final_notin_def intro: exec_Seq')


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

lemma execn_sequence_app: "∧s s' t.
 [Γ⊨⟨sequence Seq xs,Normal s⟩ =n==> s'; Γ⊨⟨sequence Seq ys,s'⟩ =n==> t]
 ==> Γ⊨⟨sequence Seq (xs@ys),Normal s⟩ =n==> t"
proof (induct xs)
  case Nil
  thus ?case by (auto elim: execn_Normal_elim_cases)
next
  case (Cons x xs)
  have exec_x_xs: "Γ⊨⟨sequence Seq (x # xs),Normal s⟩ =n==> s'" by fact
  have exec_ys: "Γ⊨⟨sequence Seq ys,s'⟩ =n==> t" by fact
  show ?case
  proof (cases xs)
    case Nil
    with exec_x_xs have "Γ⊨⟨x,Normal s⟩ =n==> s'"
      by (auto elim: execn_Normal_elim_cases )
    with Nil exec_ys show ?thesis
      by (cases ys) (auto intro: execn.intros elim: execn_elim_cases)
  next
    case Cons
    with exec_x_xs
    obtain s'' where
      exec_x: "Γ⊨⟨x,Normal s⟩ =n==> s''" and
      exec_xs: "Γ⊨⟨sequence Seq xs,s''⟩ =n==> s'"
      by (auto elim: execn_Normal_elim_cases )
    show ?thesis
    proof (cases s'')
      case (Normal s''')
      from Cons.hyps [OF exec_xs [simplified Normal] exec_ys]
      have "Γ⊨⟨sequence Seq (xs @ ys),Normal s'''⟩ =n==> t" .
      with Cons exec_x Normal
      show ?thesis
        by (auto intro: execn.intros)
    next
      case (Abrupt s''')
      with exec_xs have "s'=Abrupt s'''"
        by (auto dest: execn_Abrupt_end)
      with exec_ys have "t=Abrupt s'''"
        by (auto dest: execn_Abrupt_end)
      with exec_x Abrupt Cons show ?thesis
        by (auto intro: execn.intros)
    next
      case (Fault f)
      with exec_xs have "s'=Fault f"
        by (auto dest: execn_Fault_end)
      with exec_ys have "t=Fault f"
        by (auto dest: execn_Fault_end)
      with exec_x Fault Cons show ?thesis
        by (auto intro: execn.intros)
    next
      case Stuck
      with exec_xs have "s'=Stuck"
        by (auto dest: execn_Stuck_end)
      with exec_ys have "t=Stuck"
        by (auto dest: execn_Stuck_end)
      with exec_x Stuck Cons show ?thesis
        by (auto intro: execn.intros)
    qed
  qed
qed

lemma execn_sequence_appD: "∧s t. Γ⊨⟨sequence Seq (xs @ ys),Normal s⟩ =n==> t ==>
         ∃s'. Γ⊨⟨sequence Seq xs,Normal s⟩ =n==> s' ∧ Γ⊨⟨sequence Seq ys,s'⟩ =n==> t"
proof (induct xs)
  case Nil
  thus ?case
    by (auto intro: execn.intros)
next
  case (Cons x xs)
  have exec_app: "Γ⊨⟨sequence Seq ((x # xs) @ ys),Normal s⟩ =n==> t" by fact
  show ?case
  proof (cases xs)
    case Nil
    with exec_app show ?thesis
      by (cases ys) (auto elim: execn_Normal_elim_cases intro: execn_Skip')
  next
    case Cons
    with exec_app obtain s' where
      exec_x: "Γ⊨⟨x,Normal s⟩ =n==> s'" and
      exec_xs_ys: "Γ⊨⟨sequence Seq (xs @ ys),s'⟩ =n==> t"
      by (auto elim: execn_Normal_elim_cases)
    show ?thesis
    proof (cases s')
      case (Normal s'')
      from Cons.hyps [OF exec_xs_ys [simplified Normal]] Normal exec_x Cons
      show ?thesis
        by (auto intro: execn.intros)
    next
      case (Abrupt s'')
      with exec_xs_ys have "t=Abrupt s''"
        by (auto dest: execn_Abrupt_end)
      with Abrupt exec_x Cons
      show ?thesis
        by (auto intro: execn.intros)
    next
      case (Fault f)
      with exec_xs_ys have "t=Fault f"
        by (auto dest: execn_Fault_end)
      with Fault exec_x Cons
      show ?thesis
        by (auto intro: execn.intros)
    next
      case Stuck
      with exec_xs_ys have "t=Stuck"
        by (auto dest: execn_Stuck_end)
      with Stuck exec_x Cons
      show ?thesis
        by (auto intro: execn.intros)
    qed
  qed
qed

lemma execn_sequence_appE [consumes 1]:
  "[Γ⊨⟨sequence Seq (xs @ ys),Normal s⟩ =n==> t;
   ∧s'. [Γ⊨⟨sequence Seq xs,Normal s⟩ =n==> s';Γ⊨⟨sequence Seq ys,s'⟩ =n==> t] ==> P
   ] ==> P"
  by (auto dest: execn_sequence_appD)

lemma execn_to_execn_sequence_flatten:
  assumes exec: "Γ⊨⟨c,s⟩ =n==> t"
  shows "Γ⊨⟨sequence Seq (flatten c),s⟩ =n==> t"
using exec
proof induct
  case (Seq c1 c2 n s s' s'') thus ?case
    by (auto intro: execn.intros execn_sequence_app)
qed (auto intro: execn.intros)

lemma execn_to_execn_normalize:
  assumes exec: "Γ⊨⟨c,s⟩ =n==> t"
  shows "Γ⊨⟨normalize c,s⟩ =n==> t"
using exec
proof induct
  case (Seq c1 c2 n s s' s'') thus ?case
    by (auto intro: execn_to_execn_sequence_flatten  execn_sequence_app )
qed (auto intro: execn.intros)



lemma execn_sequence_flatten_to_execn:
  shows "∧s t. Γ⊨⟨sequence Seq (flatten c),s⟩ =n==> t ==> Γ⊨⟨c,s⟩ =n==> t"
proof (induct c)
  case (Seq c1 c2)
  have exec_seq: "Γ⊨⟨sequence Seq (flatten (Seq c1 c2)),s⟩ =n==> t" by fact
  show ?case
  proof (cases s)
    case (Normal s')
    with exec_seq obtain s'' where
      "Γ⊨⟨sequence Seq (flatten c1),Normal s'⟩ =n==> s''" and
      "Γ⊨⟨sequence Seq (flatten c2),s''⟩ =n==> t"
      by (auto elim: execn_sequence_appE)
    with Seq.hyps Normal
    show ?thesis
      by (fastforce intro: execn.intros)
  next
    case Abrupt
    with exec_seq
    show ?thesis by (auto intro: execn.intros dest: execn_Abrupt_end)
  next
    case Fault
    with exec_seq
    show ?thesis by (auto intro: execn.intros dest: execn_Fault_end)
  next
    case Stuck
    with exec_seq
    show ?thesis by (auto intro: execn.intros dest: execn_Stuck_end)
  qed
qed auto

lemma execn_normalize_to_execn:
  shows "∧s t n. Γ⊨⟨normalize c,s⟩ =n==> t ==> Γ⊨⟨c,s⟩ =n==> t"
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)
  have "Γ⊨⟨normalize (Seq c1 c2),s⟩ =n==> t" by fact
  hence exec_norm_seq:
    "Γ⊨⟨sequence Seq (flatten (normalize c1) @ flatten (normalize c2)),s⟩ =n==> t"
    by simp
  show ?case
  proof (cases s)
    case (Normal s')
    with exec_norm_seq obtain s'' where
      exec_norm_c1: "Γ⊨⟨sequence Seq (flatten (normalize c1)),Normal s'⟩ =n==> s''" and
      exec_norm_c2: "Γ⊨⟨sequence Seq (flatten (normalize c2)),s''⟩ =n==> t"
      by (auto elim: execn_sequence_appE)
    from execn_sequence_flatten_to_execn [OF exec_norm_c1]
      execn_sequence_flatten_to_execn [OF exec_norm_c2] Seq.hyps Normal
    show ?thesis
      by (fastforce intro: execn.intros)
  next
    case (Abrupt s')
    with exec_norm_seq have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by (auto intro: execn.intros)
  next
    case (Fault f)
    with exec_norm_seq have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by (auto intro: execn.intros)
  next
    case Stuck
    with exec_norm_seq have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by (auto intro: execn.intros)
  qed
next
  case Cond thus ?case
    by (auto intro: execn.intros elim!: execn_elim_cases)
next
  case (While b c)
  have "Γ⊨⟨normalize (While b c),s⟩ =n==> t" by fact
  hence exec_norm_w: "Γ⊨⟨While b (normalize c),s⟩ =n==> t"
    by simp
  {
    fix s t w
    assume exec_w: "Γ⊨⟨w,s⟩ =n==> t"
    have "w=While b (normalize c) ==> Γ⊨⟨While b c,s⟩ =n==> t"
      using exec_w
    proof (induct)
      case (WhileTrue s b' c' n w t)
      from WhileTrue obtain
        s_in_b: "s ∈ b" and
        exec_c: "Γ⊨⟨normalize c,Normal s⟩ =n==> w" and
        hyp_w: "Γ⊨⟨While b c,w⟩ =n==> t"
        by simp
      from While.hyps [OF exec_c]
      have "Γ⊨⟨c,Normal s⟩ =n==> w"
        by simp
      with hyp_w s_in_b
      have "Γ⊨⟨While b c,Normal s⟩ =n==> t"
        by (auto intro: execn.intros)
      with WhileTrue show ?case by simp
    qed (auto intro: execn.intros)
  }
  from this [OF exec_norm_w]
  show ?case
    by simp
next
  case Call thus ?case by simp
next
  case DynCom thus ?case by (auto intro: execn.intros elim!: execn_elim_cases)
next
  case Guard thus ?case by (auto intro: execn.intros elim!: execn_elim_cases)
next
  case Throw thus ?case by simp
next
  case Catch thus ?case by (fastforce intro: execn.intros elim!: execn_elim_cases)
qed

lemma execn_normalize_iff_execn:
 "Γ⊨⟨normalize c,s⟩ =n==> t = Γ⊨⟨c,s⟩ =n==> t"
  by (auto intro: execn_to_execn_normalize execn_normalize_to_execn)

lemma exec_sequence_app:
  assumes exec_xs: "Γ⊨⟨sequence Seq xs,Normal s⟩ ==> s'"
  assumes exec_ys: "Γ⊨⟨sequence Seq ys,s'⟩ ==> t"
  shows "Γ⊨⟨sequence Seq (xs@ys),Normal s⟩ ==> t"
proof -
  from exec_to_execn [OF exec_xs]
  obtain n where
    execn_xs: "Γ⊨⟨sequence Seq xs,Normal s⟩ =n==> s'"..
  from exec_to_execn [OF exec_ys]
  obtain m where
    execn_ys: "Γ⊨⟨sequence Seq ys,s'⟩ =m==> t"..
  with execn_xs obtain
    "Γ⊨⟨sequence Seq xs,Normal s⟩ =max n m==> s'"
    "Γ⊨⟨sequence Seq ys,s'⟩ =max n m==> t"
    by (auto intro: execn_mono max.cobounded1 max.cobounded2)
  from execn_sequence_app [OF this]
  have "Γ⊨⟨sequence Seq (xs @ ys),Normal s⟩ =max n m==> t" .
  thus ?thesis
    by (rule execn_to_exec)
qed

lemma exec_sequence_appD:
  assumes exec_xs_ys: "Γ⊨⟨sequence Seq (xs @ ys),Normal s⟩ ==> t"
  shows "∃s'. Γ⊨⟨sequence Seq xs,Normal s⟩ ==> s' ∧ Γ⊨⟨sequence Seq ys,s'⟩ ==> t"
proof -
  from exec_to_execn [OF exec_xs_ys]
  obtain n where "Γ⊨⟨sequence Seq (xs @ ys),Normal s⟩ =n==> t"..
  thus ?thesis
    by (cases rule: execn_sequence_appE) (auto intro: execn_to_exec)
qed


lemma exec_sequence_appE [consumes 1]:
  "[Γ⊨⟨sequence Seq (xs @ ys),Normal s⟩ ==> t;
   ∧s'. [Γ⊨⟨sequence Seq xs,Normal s⟩ ==> s';Γ⊨⟨sequence Seq ys,s'⟩ ==> t] ==> P
   ] ==> P"
  by (auto dest: exec_sequence_appD)

lemma exec_to_exec_sequence_flatten:
  assumes exec: "Γ⊨⟨c,s⟩ ==> t"
  shows "Γ⊨⟨sequence Seq (flatten c),s⟩ ==> t"
proof -
  from exec_to_execn [OF exec]
  obtain n where "Γ⊨⟨c,s⟩ =n==> t"..
  from execn_to_execn_sequence_flatten [OF this]
  show ?thesis
    by (rule execn_to_exec)
qed

lemma exec_sequence_flatten_to_exec:
  assumes exec_seq: "Γ⊨⟨sequence Seq (flatten c),s⟩ ==> t"
  shows "Γ⊨⟨c,s⟩ ==> t"
proof -
  from exec_to_execn [OF exec_seq]
  obtain n where "Γ⊨⟨sequence Seq (flatten c),s⟩ =n==> t"..
  from execn_sequence_flatten_to_execn [OF this]
  show ?thesis
    by (rule execn_to_exec)
qed

lemma exec_to_exec_normalize:
  assumes exec: "Γ⊨⟨c,s⟩ ==> t"
  shows "Γ⊨⟨normalize c,s⟩ ==> t"
proof -
  from exec_to_execn [OF exec] obtain n where "Γ⊨⟨c,s⟩ =n==> t"..
  hence "Γ⊨⟨normalize c,s⟩ =n==> t"
    by (rule execn_to_execn_normalize)
  thus ?thesis
    by (rule execn_to_exec)
qed

lemma exec_normalize_to_exec:
  assumes exec: "Γ⊨⟨normalize c,s⟩ ==> t"
  shows "Γ⊨⟨c,s⟩ ==> t"
proof -
  from exec_to_execn [OF exec] obtain n where "Γ⊨⟨normalize c,s⟩ =n==> t"..
  hence "Γ⊨⟨c,s⟩ =n==> t"
    by (rule execn_normalize_to_execn)
  thus ?thesis
    by (rule execn_to_exec)
qed

lemma exec_normalize_iff_exec:
 "Γ⊨⟨normalize c,s⟩ ==> t = Γ⊨⟨c,s⟩ ==> t"
  by (auto intro: exec_to_exec_normalize exec_normalize_to_exec)

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

lemma execn_to_execn_subseteq_guards: "∧c s t n. [c ⊆_g c'; Γ⊨⟨c,s⟩ =n==> t]
    ==> ∃t'. Γ⊨⟨c',s⟩ =n==> t' ∧
            (isFault t ⟶ isFault t') ∧ (¬ isFault t' ⟶ t'=t)"
proof (induct c')
  case Skip thus ?case
    by (fastforce dest: subseteq_guardsD elim: execn_elim_cases)
next
  case Basic thus ?case
    by (fastforce dest: subseteq_guardsD elim: execn_elim_cases)
next
  case Spec thus ?case
    by (fastforce dest: subseteq_guardsD elim: execn_elim_cases)
next
  case (Seq c1' c2')
  have "c ⊆_g Seq c1' c2'" by fact
  from subseteq_guards_Seq [OF this]
  obtain c1 c2 where
    c: "c = Seq c1 c2" and
    c1_c1': "c1 ⊆_g c1'" and
    c2_c2': "c2 ⊆_g c2'"
    by blast
  have exec: "Γ⊨⟨c,s⟩ =n==> t" by fact
  with c obtain w where
    exec_c1: "Γ⊨⟨c1,s⟩ =n==> w" and
    exec_c2: "Γ⊨⟨c2,w⟩ =n==> t"
    by (auto elim: execn_elim_cases)
  from exec_c1 Seq.hyps c1_c1'
  obtain w' where
    exec_c1': "Γ⊨⟨c1',s⟩ =n==> w'" and
    w_Fault: "isFault w ⟶ isFault w'" and
    w'_noFault: "¬ isFault w' ⟶ w'=w"
    by blast
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    show ?thesis
    proof (cases "isFault w")
      case True
      then obtain f where w': "w=Fault f"..
      moreover with exec_c2
      have t: "t=Fault f"
        by (auto dest: execn_Fault_end)
      ultimately show ?thesis
        using Normal w_Fault exec_c1'
        by (fastforce intro: execn.intros elim: isFaultE)
    next
      case False
      note noFault_w = this
      show ?thesis
      proof (cases "isFault w'")
        case True
        then obtain f' where w': "w'=Fault f'"..
        with Normal exec_c1'
        have exec: "Γ⊨⟨Seq c1' c2',s⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        then show ?thesis
          by auto
      next
        case False
        with w'_noFault have w': "w'=w" by simp
        from Seq.hyps exec_c2 c2_c2'
        obtain t' where
          "Γ⊨⟨c2',w⟩ =n==> t'" and
          "isFault t ⟶ isFault t'" and
          "¬ isFault t' ⟶ t'=t"
          by blast
        with Normal exec_c1' w'
        show ?thesis
          by (fastforce intro: execn.intros)
      qed
    qed
  qed
next
  case (Cond b c1' c2')
  have exec: "Γ⊨⟨c,s⟩ =n==> t" by fact
  have "c ⊆_g 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 ⊆_g c1'" and
    c2_c2': "c2 ⊆_g c2'"
    by blast
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    from exec [simplified c Normal]
    show ?thesis
    proof (cases)
      assume s'_in_b: "s' ∈ b"
      assume "Γ⊨⟨c1,Normal s'⟩ =n==> t"
      with c1_c1' Normal Cond.hyps obtain t' where
        "Γ⊨⟨c1',Normal s'⟩ =n==> t'"
        "isFault t ⟶ isFault t'"
        "¬ isFault t' ⟶ t' = t"
        by blast
      with s'_in_b Normal show ?thesis
        by (fastforce intro: execn.intros)
    next
      assume s'_notin_b: "s' ∉ b"
      assume "Γ⊨⟨c2,Normal s'⟩ =n==> t"
      with c2_c2' Normal Cond.hyps obtain t' where
        "Γ⊨⟨c2',Normal s'⟩ =n==> t'"
        "isFault t ⟶ isFault t'"
        "¬ isFault t' ⟶ t' = t"
        by blast
      with s'_notin_b Normal show ?thesis
        by (fastforce intro: execn.intros)
    qed
  qed
next
  case (While b c')
  have exec: "Γ⊨⟨c,s⟩ =n==> t" 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 c r w
    assume exec: "Γ⊨⟨c,r⟩ =n==> w"
    assume c: "c=While b c''"
    have "∃w'. Γ⊨⟨While b c',r⟩ =n==> w' ∧
                 (isFault w ⟶ isFault w') ∧ (¬ isFault w' ⟶ w'=w)"
    using exec c
    proof (induct)
      case (WhileTrue r b' ca n u w)
      have eqs: "While b' ca = While b c''" by fact
      from WhileTrue have r_in_b: "r ∈ b" by simp
      from WhileTrue have exec_c'': "Γ⊨⟨c'',Normal r⟩ =n==> u" by simp
      from While.hyps [OF c''_c' exec_c''] obtain u' where
        exec_c': "Γ⊨⟨c',Normal r⟩ =n==> u'" and
        u_Fault: "isFault u ⟶ isFault u' "and
        u'_noFault: "¬ isFault u' ⟶ u' = u"
        by blast
      from WhileTrue obtain w' where
        exec_w: "Γ⊨⟨While b c',u⟩ =n==> w'" and
        w_Fault: "isFault w ⟶ isFault w'" and
        w'_noFault: "¬ isFault w' ⟶ w' = w"
        by blast
      show ?case
      proof (cases "isFault u'")
        case True
        with exec_c' r_in_b
        show ?thesis
          by (fastforce intro: execn.intros elim: isFaultE)
      next
        case False
        with exec_c' r_in_b u'_noFault exec_w w_Fault w'_noFault
        show ?thesis
          by (fastforce intro: execn.intros)
      qed
    next
      case WhileFalse thus ?case by (fastforce intro: execn.intros)
    qed auto
  }
  from this [OF exec c]
  show ?case .
next
  case Call thus ?case
    by (fastforce dest: subseteq_guardsD elim: execn_elim_cases)
next
  case (DynCom C')
  have exec: "Γ⊨⟨c,s⟩ =n==> t" by fact
  have "c ⊆_g DynCom C'" by fact
  from subseteq_guards_DynCom [OF this] obtain C where
    c: "c = DynCom C" and
    C_C': "∀s. C s ⊆_g C' s"
    by blast
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    from exec [simplified c Normal]
    have "Γ⊨⟨C s',Normal s'⟩ =n==> t"
      by cases
    from DynCom.hyps C_C' [rule_format] this obtain t' where
      "Γ⊨⟨C' s',Normal s'⟩ =n==> t'"
      "isFault t ⟶ isFault t'"
      "¬ isFault t' ⟶ t' = t"
      by blast
    with Normal show ?thesis
      by (fastforce intro: execn.intros)
  qed
next
  case (Guard f' g' c')
  have exec: "Γ⊨⟨c,s⟩ =n==> t" by fact
  have "c ⊆_g Guard f' g' c'" by fact
  hence subset_cases: "(c ⊆_g c') ∨ (∃c''. c = Guard f' g' c'' ∧ (c'' ⊆_g c'))"
    by (rule subseteq_guards_Guard)
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    from subset_cases show ?thesis
    proof
      assume c_c': "c ⊆_g c'"
      from Guard.hyps [OF this exec] Normal obtain t' where
        exec_c': "Γ⊨⟨c',Normal s'⟩ =n==> t'" and
        t_Fault: "isFault t ⟶ isFault t'" and
        t_noFault: "¬ isFault t' ⟶ t' = t"
        by blast
      with Normal
      show ?thesis
        by (cases "s' ∈ g'") (fastforce intro: execn.intros)+
    next
      assume "∃c''. c = Guard f' g' c'' ∧ (c'' ⊆_g c')"
      then obtain c'' where
        c: "c = Guard f' g' c''" and
        c''_c': "c'' ⊆_g c'"
        by blast
      from c exec Normal
      have exec_Guard': "Γ⊨⟨Guard f' g' c'',Normal s'⟩ =n==> t"
        by simp
      thus ?thesis
      proof (cases)
        assume s'_in_g': "s' ∈ g'"
        assume exec_c'': "Γ⊨⟨c'',Normal s'⟩ =n==> t"
        from Guard.hyps [OF c''_c' exec_c'']  obtain t' where
          exec_c': "Γ⊨⟨c',Normal s'⟩ =n==> t'" and
          t_Fault: "isFault t ⟶ isFault t'" and
          t_noFault: "¬ isFault t' ⟶ t' = t"
          by blast
        with Normal s'_in_g'
        show ?thesis
          by (fastforce intro: execn.intros)
      next
        assume "s' ∉ g'" "t=Fault f'"
        with Normal show ?thesis
          by (fastforce intro: execn.intros)
      qed
    qed
  qed
next
  case Throw thus ?case
    by (fastforce dest: subseteq_guardsD intro: execn.intros
         elim: execn_elim_cases)
next
  case (Catch c1' c2')
  have "c ⊆_g Catch c1' c2'" by fact
  from subseteq_guards_Catch [OF this]
  obtain c1 c2 where
    c: "c = Catch c1 c2" and
    c1_c1': "c1 ⊆_g c1'" and
    c2_c2': "c2 ⊆_g c2'"
    by blast
  have exec: "Γ⊨⟨c,s⟩ =n==> t" by fact
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    withtheory Go_Setup
      by auto
  next
    case (Abrupt (Go) "true"
    with exechavetAbrupt s'
      byoest"o_private_map_list f a = map f a"
    
      by auto
  next
    case (
    
java.lang.StringIndexOutOfBoundsException: Index 16 out of bounds for length 16
| "abs :: integer ==> (G)".Abs
      fix w
      assume exec_c1
      assume Numerald_code‹Code_Numeral.Pos›u^‹
 from Normal exec_c1 c1_c1' Catch.hyps obtain w' where
 exec_c1': "Γ⊨⟨c1',Normal s'⟩ =n==> w'" and
 w'_noFault: "¬ isFault w' ⟶ w' = Abrupt w"
 by blast
 show ?thesis
 proof (cases "isFault w'")
 case True
 with exec_c1' Normal show ?thesis
 by (fastforce intro: execn.intros elim: isFaultE)
 next
 case False
 with w'_noFault have w': "w'=Abrupt w" by simp
 from Normal exec_c2 c2_c2' Catch.hyps obtain t' where
 "Γ⊨⟨c2',Normal w⟩ =n==> t'"
 "isFault t ⟶ isFault t'"
 "¬ isFault t' ⟶ t' = t"
 by blast
 with exec_c1' w' Normal
 show ?thesis
 by (fastforce intro: execn.intros )
 qed
 next
 assume exec_c1: "Γ⊨⟨c1,Normal s'⟩ =n==> t"
 assume t: "¬ isAbr t"
 from Normal exec_c1 c1_c1' Catch.hyps obtain t' where
 exec_c1': "Γ⊨⟨c1',Normal s'⟩ =n==> 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' Normal show ?thesis
 by (fastforce intro: execn.intros elim: isFaultE)
 next
 case False
 with exec_c1' Normal t_Fault t'_noFault t
 show ?thesis
 by (fastforce intro: execn.intros)
 qed
 qed
 qed
 

  exec_to_exec_subseteq_guards:
 assumes c_c': "c ⊆_g c'"
 assumes exec: "Γ⊨⟨c,s⟩ ==> t"
 shows "∃t'. Γ⊨⟨c',s⟩ ==> t' ∧
 (isFault t ⟶ isFault t') ∧ (¬ isFault t' ⟶ t'=t)"
  -
 from exec_to_execn [OF exec] obtain n where
 "Γ⊨⟨c,s⟩ =n==> t" ..
 from execn_to_execn_subseteq_guards [OF c_c' this]
 show ?thesis
 by (blast intro: execn_to_exec)
 


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


theorem execn_to_execn_merge_guards:
 assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
 shows "Γ⊨⟨merge_guards c,s⟩ =n==> t "
using exec_c
proof (induct)
  case (Guard s g c n t f)
  have s_in_g: "s ∈ g"  by fact
  have exec_merge_c: "Γ⊨⟨merge_guards c,Normal s⟩ =n==> t" by fact
  show ?case
  proof (cases "∃f' g' c'. merge_guards c = Guard f' g' c'")
    case False
    with exec_merge_c s_in_g
    show ?thesis
      by (cases "merge_guards c") (auto intro: execn.intros simp add: Let_def)
  next
    case True
    then obtain f' g' c' where
      merge_guards_c: "merge_guards c = Guard f' g' c'"
      by iprover
    show ?thesis
    proof (cases "f=f'")
      case False
      from exec_merge_c s_in_g merge_guards_c False show ?thesis
        by (auto intro: execn.intros simp add: Let_def)
    next
      case True
      from exec_merge_c s_in_g merge_guards_c True show ?thesis
        by (fastforce intro: execn.intros elim: execn.cases)
    qed
  qed
next
  case (GuardFault s g f c n)
  have s_notin_g: "s ∉ g"  by fact
  show ?case
  proof (cases "∃f' g' c'. merge_guards c = Guard f' g' c'")
    case False
    with s_notin_g
    show ?thesis
      by (cases "merge_guards c") (auto intro: execn.intros simp add: Let_def)
  next
    case True
    then obtain f' g' c' where
      merge_guards_c: "merge_guards c = Guard f' g' c'"
      by iprover
    show ?thesis
    proof (cases "f=f'")
      case False
      from s_notin_g merge_guards_c False show ?thesis
        by (auto intro: execn.intros simp add: Let_def)
    next
      case True
      from  s_notin_g merge_guards_c True show ?thesis
        by (fastforce intro: execn.intros)
    qed
  qed
qed (fastforce intro: execn.intros)+

lemma execn_merge_guards_to_execn_Normal:
  "∧s n t. Γ⊨⟨merge_guards c,Normal s⟩ =n==> t ==> Γ⊨⟨c,Normal s⟩ =n==> t"
proof (induct c)
  case Skip thus ?case by auto
next
  case Basic thus ?case by auto
next
  case Spec thus ?case by auto
next
  case (Seq c1 c2)
  have "Γ⊨⟨merge_guards (Seq c1 c2),Normal s⟩ =n==> t" by fact
  hence exec_merge: "Γ⊨⟨Seq (merge_guards c1) (merge_guards c2),Normal s⟩ =n==> t"
    by simp
  then obtain s' where
    exec_merge_c1: "Γ⊨⟨merge_guards c1,Normal s⟩ =n==> s'" and
    exec_merge_c2: "Γ⊨⟨merge_guards c2,s'⟩ =n==> t"
    by cases
  from exec_merge_c1
  have exec_c1: "Γ⊨⟨c1,Normal s⟩ =n==> s'"
    by (rule Seq.hyps)
  show ?case
  proof (cases s')
    case (Normal s'')
    with exec_merge_c2
    have "Γ⊨⟨c2,s'⟩ =n==> t"
      by (auto intro: Seq.hyps)
    with exec_c1 show ?thesis
      by (auto intro: execn.intros)
  next
    case (Abrupt s'')
    with exec_merge_c2 have "t=Abrupt s''"
      by (auto dest: execn_Abrupt_end)
    with exec_c1 Abrupt
    show ?thesis
      by (auto intro: execn.intros)
  next
    case (Fault f)
    with exec_merge_c2 have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with exec_c1 Fault
    show ?thesis
      by (auto intro: execn.intros)
  next
    case Stuck
    with exec_merge_c2 have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with exec_c1 Stuck
    show ?thesis
      by (auto intro: execn.intros)
  qed
next
  case Cond thus ?case
    by (fastforce intro: execn.intros elim: execn_Normal_elim_cases)
next
  case (While b c)
  {
    fix c' r w
    assume exec_c': "Γ⊨⟨c',r⟩ =n==> w"
    assume c': "c'=While b (merge_guards c)"
    have "Γ⊨⟨While b c,r⟩ =n==> w"
      using exec_c' c'
    proof (induct)
      case (WhileTrue r b' c'' n u w)
      have eqs: "While b' c'' = While b (merge_guards c)" by fact
      from WhileTrue
      have r_in_b: "r ∈ b"
        by simp
      from WhileTrue While.hyps have exec_c: "Γ⊨⟨c,Normal r⟩ =n==> u"
        by simp
      from WhileTrue have exec_w: "Γ⊨⟨While b c,u⟩ =n==> w"
        by simp
      from r_in_b exec_c exec_w
      show ?case
        by (rule execn.WhileTrue)
    next
      case WhileFalse thus ?case by (auto intro: execn.WhileFalse)
    qed auto
  }
  with While.prems show ?case
    by (auto)
next
  case Call thus ?case by simp
next
  case DynCom thus ?case
    by (fastforce intro: execn.intros elim: execn_Normal_elim_cases)
next
  case (Guard f g c)
  have exec_merge: "Γ⊨⟨merge_guards (Guard f g c),Normal s⟩ =n==> t" by fact
  show ?case
  proof (cases "s ∈ g")
    case False
    with exec_merge have "t=Fault f"
      by (auto split: com.splits if_split_asm elim: execn_Normal_elim_cases
        simp add: Let_def is_Guard_def)
    with False show ?thesis
      by (auto intro: execn.intros)
  next
    case True
    note s_in_g = this
    show ?thesis
    proof (cases "∃f' g' c'. merge_guards c = Guard f' g' c'")
      case False
      then
      have "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
        by (cases "merge_guards c") (auto simp add: Let_def)
      with exec_merge s_in_g
      obtain "Γ⊨⟨merge_guards c,Normal s⟩ =n==> t"
        by (auto elim: execn_Normal_elim_cases)
      from Guard.hyps [OF this] s_in_g
      show ?thesis
        by (auto intro: execn.intros)
    next
      case True
      then obtain f' g' c' where
        merge_guards_c: "merge_guards c = Guard f' g' c'"
        by iprover
      show ?thesis
      proof (cases "f=f'")
        case False
        with merge_guards_c
        have "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
          by (simp add: Let_def)
        with exec_merge s_in_g
        obtain "Γ⊨⟨merge_guards c,Normal s⟩ =n==> t"
          by (auto elim: execn_Normal_elim_cases)
        from Guard.hyps [OF this] s_in_g
        show ?thesis
          by (auto intro: execn.intros)
      next
        case True
        note f_eq_f' = this
        with merge_guards_c have
          merge_guards_Guard: "merge_guards (Guard f g c) = Guard f (g ∩ g') c'"
          by simp
        show ?thesis
        proof (cases "s ∈ g'")
          case True
          with exec_merge merge_guards_Guard merge_guards_c s_in_g
          have "Γ⊨⟨merge_guards c,Normal s⟩ =n==> t"
            by (auto intro: execn.intros elim: execn_Normal_elim_cases)
          with Guard.hyps [OF this] s_in_g
          show ?thesis
            by (auto intro: execn.intros)
        next
          case False
          with exec_merge merge_guards_Guard
          have "t=Fault f"
            by (auto elim: execn_Normal_elim_cases)
          with merge_guards_c f_eq_f' False
          have "Γ⊨⟨merge_guards c,Normal s⟩ =n==> t"
            by (auto intro: execn.intros)
          from Guard.hyps [OF this] s_in_g
          show ?thesis
            by (auto intro: execn.intros)
        qed
      qed
    qed
  qed
next
  case Throw thus ?case by simp
next
  case (Catch c1 c2)
  have "Γ⊨⟨merge_guards (Catch c1 c2),Normal s⟩ =n==> t"  by fact
  hence "Γ⊨⟨Catch (merge_guards c1) (merge_guards c2),Normal s⟩ =n==> t" by simp
  thus ?case
    by cases (auto intro: execn.intros Catch.hyps)
qed

theorem execn_merge_guards_to_execn:
  "Γ⊨⟨merge_guards c,s⟩ =n==> t ==> Γ⊨⟨c, s⟩ =n==> t"
apply (cases s)
apply    (fastforce intro: execn_merge_guards_to_execn_Normal)
apply   (fastforce dest: execn_Abrupt_end)
apply  (fastforce dest: execn_Fault_end)
apply (fastforce dest: execn_Stuck_end)
done

corollary execn_iff_execn_merge_guards:
 "Γ⊨⟨c, s⟩ =n==> t = Γ⊨⟨merge_guards c,s⟩ =n==> t"
  by (blast intro: execn_merge_guards_to_execn execn_to_execn_merge_guards)

theorem exec_iff_exec_merge_guards:
 "Γ⊨⟨c, s⟩ ==> t = Γ⊨⟨merge_guards c,s⟩ ==> t"
  by (blast dest: exec_to_execn intro: execn_to_exec
            intro: execn_to_execn_merge_guards
                   execn_merge_guards_to_execn)

corollary exec_to_exec_merge_guards:
 "Γ⊨⟨c, s⟩ ==> t ==> Γ⊨⟨merge_guards c,s⟩ ==> t"
  by (rule iffD1 [OF exec_iff_exec_merge_guards])

corollary exec_merge_guards_to_exec:
 "Γ⊨⟨merge_guards c,s⟩ ==> t ==> Γ⊨⟨c, s⟩ ==> t"
  by (rule iffD2 [OF exec_iff_exec_merge_guards])

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

lemma execn_to_execn_mark_guards:
 assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
 assumes t_not_Fault: "¬ isFault t"
 shows "Γ⊨⟨mark_guards f c,s⟩ =n==> t "
using exec_c t_not_Fault [simplified not_isFault_iff]
by (induct) (auto intro: execn.intros dest: noFaultn_startD')

lemma execn_to_execn_mark_guards_Fault:
 assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
 shows "∧f. [t=Fault f] ==> ∃f'. Γ⊨⟨mark_guards x c,s⟩ =n==> Fault f'"
using exec_c
proof (induct)
  case Skip thus ?case by auto
next
  case Guard thus ?case by (fastforce intro: execn.intros)
next
  case GuardFault thus ?case by (fastforce intro: execn.intros)
next
  case FaultProp thus ?case by auto
next
 case Basic thus ?case by auto
next
 case Spec thus ?case by auto
next
 case SpecStuck thus ?case by auto
next
  case (Seq c1 s n w c2 t)
  have exec_c1: "Γ⊨⟨c1,Normal s⟩ =n==> w" by fact
  have exec_c2: "Γ⊨⟨c2,w⟩ =n==> t" by fact
  have t: "t=Fault f" by fact
  show ?case
  proof (cases w)
    case (Fault f')
    with exec_c2 t have "f'=f"
      by (auto dest: execn_Fault_end)
    with Fault Seq.hyps obtain f'' where
      "Γ⊨⟨mark_guards x c1,Normal s⟩ =n==> Fault f''"
      by auto
    moreover have "Γ⊨⟨mark_guards x c2,Fault f''⟩ =n==> Fault f''"
      by auto
    ultimately show ?thesis
      by (auto intro: execn.intros)
  next
    case (Normal s')
    with execn_to_execn_mark_guards [OF exec_c1]
    have exec_mark_c1: "Γ⊨⟨mark_guards x c1,Normal s⟩ =n==> w"
      by simp
    with Seq.hyps t obtain f' where
      "Γ⊨⟨mark_guards x c2,w⟩ =n==> Fault f'"
      by blast
    with exec_mark_c1 show ?thesis
      by (auto intro: execn.intros)
  next
    case (Abrupt s')
    with execn_to_execn_mark_guards [OF exec_c1]
    have exec_mark_c1: "Γ⊨⟨mark_guards x c1,Normal s⟩ =n==> w"
      by simp
    with Seq.hyps t obtain f' where
      "Γ⊨⟨mark_guards x c2,w⟩ =n==> Fault f'"
      by (auto intro: execn.intros)
    with exec_mark_c1 show ?thesis
      by (auto intro: execn.intros)
  next
    case Stuck
    with exec_c2 have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with t show ?thesis by simp
  qed
next
  case CondTrue thus ?case by (fastforce intro: execn.intros)
next
  case CondFalse thus ?case by (fastforce intro: execn.intros)
next
  case (WhileTrue s b c n w t)
  have exec_c: "Γ⊨⟨c,Normal s⟩ =n==> w" by fact
  have exec_w: "Γ⊨⟨While b c,w⟩ =n==> t" by fact
  have t: "t = Fault f" by fact
  have s_in_b: "s ∈ b" by fact
  show ?case
  proof (cases w)
    case (Fault f')
    with exec_w t have "f'=f"
      by (auto dest: execn_Fault_end)
    with Fault WhileTrue.hyps obtain f'' where
      "Γ⊨⟨mark_guards x c,Normal s⟩ =n==> Fault f''"
      by auto
    moreover have "Γ⊨⟨mark_guards x (While b c),Fault f''⟩ =n==> Fault f''"
      by auto
    ultimately show ?thesis
      using s_in_b by (auto intro: execn.intros)
  next
    case (Normal s')
    with execn_to_execn_mark_guards [OF exec_c]
    have exec_mark_c: "Γ⊨⟨mark_guards x c,Normal s⟩ =n==> w"
      by simp
    with WhileTrue.hyps t obtain f' where
      "Γ⊨⟨mark_guards x (While b c),w⟩ =n==> Fault f'"
      by blast
    with exec_mark_c s_in_b show ?thesis
      by (auto intro: execn.intros)
  next
    case (Abrupt s')
    with execn_to_execn_mark_guards [OF exec_c]
    have exec_mark_c: "Γ⊨⟨mark_guards x c,Normal s⟩ =n==> w"
      by simp
    with WhileTrue.hyps t obtain f' where
      "Γ⊨⟨mark_guards x (While b c),w⟩ =n==> Fault f'"
      by (auto intro: execn.intros)
    with exec_mark_c s_in_b show ?thesis
      by (auto intro: execn.intros)
  next
    case Stuck
    with exec_w have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with t show ?thesis by simp
  qed
next
  case WhileFalse thus ?case by (fastforce intro: execn.intros)
next
  case Call thus ?case by (fastforce intro: execn.intros)
next
  case CallUndefined thus ?case by simp
next
  case StuckProp thus ?case by simp
next
  case DynCom thus ?case by (fastforce intro: execn.intros)
next
  case Throw thus ?case by simp
next
  case AbruptProp thus ?case by simp
next
  case (CatchMatch c1 s n w c2 t)
  have exec_c1: "Γ⊨⟨c1,Normal s⟩ =n==> Abrupt w" by fact
  have exec_c2: "Γ⊨⟨c2,Normal w⟩ =n==> t" by fact
  have t: "t = Fault f" by fact
  from execn_to_execn_mark_guards [OF exec_c1]
  have exec_mark_c1: "Γ⊨⟨mark_guards x c1,Normal s⟩ =n==> Abrupt w"
    by simp
  with CatchMatch.hyps t obtain f' where
    "Γ⊨⟨mark_guards x c2,Normal w⟩ =n==> Fault f'"
    by blast
  with exec_mark_c1 show ?case
    by (auto intro: execn.intros)
next
  case CatchMiss thus ?case by (fastforce intro: execn.intros)
qed

lemma execn_mark_guards_to_execn:
  "∧s n t. Γ⊨⟨mark_guards f c,s⟩ =n==> t
  ==> ∃t'. Γ⊨⟨c,s⟩ =n==> t' ∧
            (isFault t ⟶ isFault t') ∧
            (t' = Fault f ⟶ t'=t) ∧
            (isFault t' ⟶ isFault t) ∧
            (¬ isFault t' ⟶ t'=t)"
proof (induct c)
  case Skip thus ?case by auto
next
  case Basic thus ?case by auto
next
  case Spec thus ?case by auto
next
  case (Seq c1 c2 s n t)
  have exec_mark: "Γ⊨⟨mark_guards f (Seq c1 c2),s⟩ =n==> t" by fact
  then obtain w where
    exec_mark_c1: "Γ⊨⟨mark_guards f c1,s⟩ =n==> w" and
    exec_mark_c2: "Γ⊨⟨mark_guards f c2,w⟩ =n==> t"
    by (auto elim: execn_elim_cases)
  from Seq.hyps exec_mark_c1
  obtain w' where
    exec_c1: "Γ⊨⟨c1,s⟩ =n==> w'" and
    w_Fault: "isFault w ⟶ isFault w'" and
    w'_Fault_f: "w' = Fault f ⟶ w'=w" and
    w'_Fault: "isFault w' ⟶ isFault w" and
    w'_noFault: "¬ isFault w' ⟶ w'=w"
    by blast
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec_mark have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_mark have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_mark have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    show ?thesis
    proof (cases "isFault w")
      case True
      then obtain f where w': "w=Fault f"..
      moreover with exec_mark_c2
      have t: "t=Fault f"
        by (auto dest: execn_Fault_end)
      ultimately show ?thesis
        using Normal w_Fault w'_Fault_f exec_c1
        by (fastforce intro: execn.intros elim: isFaultE)
    next
      case False
      note noFault_w = this
      show ?thesis
      proof (cases "isFault w'")
        case True
        then obtain f' where w': "w'=Fault f'"..
        with Normal exec_c1
        have exec: "Γ⊨⟨Seq c1 c2,s⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        from w'_Fault_f w' noFault_w
        have "f' ≠ f"
          by (cases w) auto
        moreover
        from w' w'_Fault exec_mark_c2 have "isFault t"
          by (auto dest: execn_Fault_end elim: isFaultE)
        ultimately
        show ?thesis
          using exec
          by auto
      next
        case False
        with w'_noFault have w': "w'=w" by simp
        from Seq.hyps exec_mark_c2
        obtain t' where
          "Γ⊨⟨c2,w⟩ =n==> t'" and
          "isFault t ⟶ isFault t'" and
          "t' = Fault f ⟶ t'=t" and
          "isFault t' ⟶ isFault t" and
          "¬ isFault t' ⟶ t'=t"
          by blast
        with Normal exec_c1 w'
        show ?thesis
          by (fastforce intro: execn.intros)
      qed
    qed
  qed
next
  case (Cond b c1 c2 s n t)
  have exec_mark: "Γ⊨⟨mark_guards f (Cond b c1 c2),s⟩ =n==> t" by fact
  show ?case
  proof (cases s)
    case (Fault f)
    with exec_mark have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_mark have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_mark have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    show ?thesis
    proof (cases "s'∈ b")
      case True
      with Normal exec_mark
      have "Γ⊨⟨mark_guards f c1 ,Normal s'⟩ =n==> t"
        by (auto elim: execn_Normal_elim_cases)
      with Normal True Cond.hyps obtain t'
        where "Γ⊨⟨c1,Normal s'⟩ =n==> t'"
            "isFault t ⟶ isFault t'"
            "t' = Fault f ⟶ t'=t"
            "isFault t' ⟶ isFault t"
            "¬ isFault t' ⟶ t' = t"
        by blast
      with Normal True
      show ?thesis
        by (blast intro: execn.intros)
    next
      case False
      with Normal exec_mark
      have "Γ⊨⟨mark_guards f c2 ,Normal s'⟩ =n==> t"
        by (auto elim: execn_Normal_elim_cases)
      with Normal False Cond.hyps obtain t'
        where "Γ⊨⟨c2,Normal s'⟩ =n==> t'"
            "isFault t ⟶ isFault t'"
            "t' = Fault f ⟶ t'=t"
            "isFault t' ⟶ isFault t"
            "¬ isFault t' ⟶ t' = t"
        by blast
      with Normal False
      show ?thesis
        by (blast intro: execn.intros)
    qed
  qed
next
  case (While b c s n t)
  have exec_mark: "Γ⊨⟨mark_guards f (While b c),s⟩ =n==> t" by fact
  show ?case
  proof (cases s)
    case (Fault f)
    with exec_mark have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_mark have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_mark have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    {
      fix c' r w
      assume exec_c': "Γ⊨⟨c',r⟩ =n==> w"
      assume c': "c'=While b (mark_guards f c)"
      have "∃w'. Γ⊨⟨While b c,r⟩ =n==> w' ∧ (isFault w ⟶ isFault w') ∧
                   (w' = Fault f ⟶ w'=w) ∧ (isFault w' ⟶ isFault w) ∧
                   (¬ isFault w' ⟶ w'=w)"
        using exec_c' c'
      proof (induct)
        case (WhileTrue r b' c'' n u w)
        have eqs: "While b' c'' = While b (mark_guards f c)" by fact
        from WhileTrue.hyps eqs
        have r_in_b: "r∈b" by simp
        from WhileTrue.hyps eqs
        have exec_mark_c: "Γ⊨⟨mark_guards f c,Normal r⟩ =n==> u" by simp
        from WhileTrue.hyps eqs
        have exec_mark_w: "Γ⊨⟨While b (mark_guards f c),u⟩ =n==> w"
          by simp
        show ?case
        proof -
          from WhileTrue.hyps eqs have "Γ⊨⟨mark_guards f c,Normal r⟩ =n==> u"
            by simp
          with While.hyps
          obtain u' where
            exec_c: "Γ⊨⟨c,Normal r⟩ =n==> u'" and
            u_Fault: "isFault u ⟶ isFault u'" and
            u'_Fault_f: "u' = Fault f ⟶ u'=u" and
            u'_Fault: "isFault u' ⟶ isFault u" and
            u'_noFault: "¬ isFault u' ⟶ u'=u"
            by blast
          show ?thesis
          proof (cases "isFault u'")
            case False
            with u'_noFault have u': "u'=u" by simp
            from WhileTrue.hyps eqs obtain w' where
              "Γ⊨⟨While b c,u⟩ =n==> w'"
              "isFault w ⟶ isFault w'"
              "w' = Fault f ⟶ w'=w"
              "isFault w' ⟶ isFault w"
              "¬ isFault w' ⟶ w' = w"
              by blast
            with u' exec_c r_in_b
            show ?thesis
              by (blast intro: execn.WhileTrue)
          next
            case True
            then obtain f' where u': "u'=Fault f'"..
            with exec_c r_in_b
            have exec: "Γ⊨⟨While b c,Normal r⟩ =n==> Fault f'"
              by (blast intro: execn.intros)
            from True u'_Fault have "isFault u"
              by simp
            then obtain f where u: "u=Fault f"..
            with exec_mark_w have "w=Fault f"
              by (auto dest: execn_Fault_end)
            with exec u' u u'_Fault_f
            show ?thesis
              by auto
          qed
        qed
      next
        case (WhileFalse r b' c'' n)
        have eqs: "While b' c'' = While b (mark_guards f c)" by fact
        from WhileFalse.hyps eqs
        have r_not_in_b: "r∉b" by simp
        show ?case
        proof -
          from r_not_in_b
          have "Γ⊨⟨While b c,Normal r⟩ =n==> Normal r"
            by (rule execn.WhileFalse)
          thus ?thesis
            by blast
        qed
      qed auto
    } note hyp_while = this
    show ?thesis
    proof (cases "s'∈b")
      case False
      with Normal exec_mark
      have "t=s"
        by (auto elim: execn_Normal_elim_cases)
      with Normal False show ?thesis
        by (auto intro: execn.intros)
    next
      case True note s'_in_b = this
      with Normal exec_mark obtain r where
        exec_mark_c: "Γ⊨⟨mark_guards f c,Normal s'⟩ =n==> r" and
        exec_mark_w: "Γ⊨⟨While b (mark_guards f c),r⟩ =n==> t"
        by (auto elim: execn_Normal_elim_cases)
      from While.hyps exec_mark_c obtain r' where
        exec_c: "Γ⊨⟨c,Normal s'⟩ =n==> r'" and
        r_Fault: "isFault r ⟶ isFault r'" and
        r'_Fault_f: "r' = Fault f ⟶ r'=r" and
        r'_Fault: "isFault r' ⟶ isFault r" and
        r'_noFault: "¬ isFault r' ⟶ r'=r"
        by blast
      show ?thesis
      proof (cases "isFault r'")
        case False
        with r'_noFault have r': "r'=r" by simp
        from hyp_while exec_mark_w
        obtain t' where
          "Γ⊨⟨While b c,r⟩ =n==> t'"
          "isFault t ⟶ isFault t'"
          "t' = Fault f ⟶ t'=t"
          "isFault t' ⟶ isFault t"
          "¬ isFault t' ⟶ t'=t"
          by blast
        with r' exec_c Normal s'_in_b
        show ?thesis
          by (blast intro: execn.intros)
      next
        case True
        then obtain f' where r': "r'=Fault f'"..
        hence "Γ⊨⟨While b c,r'⟩ =n==> Fault f'"
          by auto
        with Normal s'_in_b exec_c
        have exec: "Γ⊨⟨While b c,Normal s'⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        from True r'_Fault
        have "isFault r"
          by simp
        then obtain f where r: "r=Fault f"..
        with exec_mark_w have "t=Fault f"
          by (auto dest: execn_Fault_end)
        with Normal exec r' r r'_Fault_f
        show ?thesis
          by auto
      qed
    qed
  qed
next
  case Call thus ?case by auto
next
  case DynCom thus ?case
    by (fastforce elim!: execn_elim_cases intro: execn.intros)
next
  case (Guard f' g c s n t)
  have exec_mark: "Γ⊨⟨mark_guards f (Guard f' g c),s⟩ =n==> t" by fact
  show ?case
  proof (cases s)
    case (Fault f)
    with exec_mark have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_mark have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_mark have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    show ?thesis
    proof (cases "s'∈g")
      case False
      with Normal exec_mark have t: "t=Fault f"
        by (auto elim: execn_Normal_elim_cases)
      from False
      have "Γ⊨⟨Guard f' g c,Normal s'⟩ =n==> Fault f'"
        by (blast intro: execn.intros)
      with Normal t show ?thesis
        by auto
    next
      case True
      with exec_mark Normal
      have "Γ⊨⟨mark_guards f c,Normal s'⟩ =n==> t"
        by (auto elim: execn_Normal_elim_cases)
      with Guard.hyps obtain t' where
        "Γ⊨⟨c,Normal s'⟩ =n==> t'" and
        "isFault t ⟶ isFault t'" and
        "t' = Fault f ⟶ t'=t" and
        "isFault t' ⟶ isFault t" and
        "¬ isFault t' ⟶ t'=t"
        by blast
      with Normal True
      show ?thesis
        by (blast intro: execn.intros)
    qed
  qed
next
  case Throw thus ?case by auto
next
  case (Catch c1 c2 s n t)
  have exec_mark: "Γ⊨⟨mark_guards f (Catch c1 c2),s⟩ =n==> t" by fact
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec_mark have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_mark have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_mark have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s') note s=this
    with exec_mark have
      "Γ⊨⟨Catch (mark_guards f c1) (mark_guards f c2),Normal s'⟩ =n==> t" by simp
    thus ?thesis
    proof (cases)
      fix w
      assume exec_mark_c1: "Γ⊨⟨mark_guards f c1,Normal s'⟩ =n==> Abrupt w"
      assume exec_mark_c2: "Γ⊨⟨mark_guards f c2,Normal w⟩ =n==> t"
      from exec_mark_c1 Catch.hyps
      obtain w' where
        exec_c1: "Γ⊨⟨c1,Normal s'⟩ =n==> w'" and
        w'_Fault_f: "w' = Fault f ⟶ w'=Abrupt w" and
        w'_Fault: "isFault w' ⟶ isFault (Abrupt w)" and
        w'_noFault: "¬ isFault w' ⟶ w'=Abrupt w"
        by fastforce
      show ?thesis
      proof (cases "w'")
        case (Fault f')
        with Normal exec_c1 have "Γ⊨⟨Catch c1 c2,s⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        with w'_Fault Fault show ?thesis
          by auto
      next
        case Stuck
        with w'_noFault have False
          by simp
        thus ?thesis ..
      next
        case (Normal w'')
        with w'_noFault have False by simp thus ?thesis ..
      next
        case (Abrupt w'')
        with w'_noFault have w'': "w''=w" by simp
        from  exec_mark_c2 Catch.hyps
        obtain t' where
          "Γ⊨⟨c2,Normal w⟩ =n==> t'"
          "isFault t ⟶ isFault t'"
          "t' = Fault f ⟶ t'=t"
          "isFault t' ⟶ isFault t"
          "¬ isFault t' ⟶ t'=t"
          by blast
        with w'' Abrupt s exec_c1
        show ?thesis
          by (blast intro: execn.intros)
      qed
    next
      assume t: "¬ isAbr t"
      assume "Γ⊨⟨mark_guards f c1,Normal s'⟩ =n==> t"
      with Catch.hyps
      obtain t' where
        exec_c1: "Γ⊨⟨c1,Normal s'⟩ =n==> 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
        then obtain f' where t': "t'=Fault f'"..
        with exec_c1 have "Γ⊨⟨Catch c1 c2,Normal s'⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        with t'_Fault_f t'_Fault t' s show ?thesis
          by auto
      next
        case False
        with t'_noFault have "t'=t" by simp
        with t exec_c1 s show ?thesis
          by (blast intro: execn.intros)
      qed
    qed
  qed
qed

lemma exec_to_exec_mark_guards:
 assumes exec_c: "Γ⊨⟨c,s⟩ ==> t"
 assumes t_not_Fault: "¬ isFault t"
 shows "Γ⊨⟨mark_guards f c,s⟩ ==> t "
proof -
  from exec_to_execn [OF exec_c] obtain n where
    "Γ⊨⟨c,s⟩ =n==> t" ..
  from execn_to_execn_mark_guards [OF this t_not_Fault]
  show ?thesis
    by (blast intro: execn_to_exec)
qed

lemma exec_to_exec_mark_guards_Fault:
 assumes exec_c: "Γ⊨⟨c,s⟩ ==> Fault f"
 shows "∃f'. Γ⊨⟨mark_guards x c,s⟩ ==> Fault f'"
proof -
  from exec_to_execn [OF exec_c] obtain n where
    "Γ⊨⟨c,s⟩ =n==> Fault f" ..
  from execn_to_execn_mark_guards_Fault [OF this]
  show ?thesis
    by (blast intro: execn_to_exec)
qed


lemma exec_mark_guards_to_exec:
  assumes exec_mark: "Γ⊨⟨mark_guards f c,s⟩ ==> t"
  shows "∃t'. Γ⊨⟨c,s⟩ ==> t' ∧
            (isFault t ⟶ isFault t') ∧
            (t' = Fault f ⟶ t'=t) ∧
            (isFault t' ⟶ isFault t) ∧
            (¬ isFault t' ⟶ t'=t)"
proof -
  from exec_to_execn [OF exec_mark] obtain n where
    "Γ⊨⟨mark_guards f c,s⟩ =n==> t" ..
  from execn_mark_guards_to_execn [OF this]
  show ?thesis
    by (blast intro: execn_to_exec)
qed

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

lemma execn_to_execn_strip_guards:
 assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
 assumes t_not_Fault: "¬ isFault t"
 shows "Γ⊨⟨strip_guards F c,s⟩ =n==> t "
using exec_c t_not_Fault [simplified not_isFault_iff]
by (induct) (auto intro: execn.intros dest: noFaultn_startD')


lemma execn_to_execn_strip_guards_Fault:
 assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
 shows "∧f. [t=Fault f; f ∉ F] ==> Γ⊨⟨strip_guards F c,s⟩ =n==> Fault f"
using exec_c
proof (induct)
  case Skip thus ?case by auto
next
  case Guard thus ?case by (fastforce intro: execn.intros)
next
  case GuardFault thus ?case by (fastforce intro: execn.intros)
next
  case FaultProp thus ?case by auto
next
 case Basic thus ?case by auto
next
 case Spec thus ?case by auto
next
 case SpecStuck thus ?case by auto
next
  case (Seq c1 s n w c2 t)
  have exec_c1: "Γ⊨⟨c1,Normal s⟩ =n==> w" by fact
  have exec_c2: "Γ⊨⟨c2,w⟩ =n==> t" by fact
  have t: "t=Fault f" by fact
  have notinF: "f ∉ F" by fact
  show ?case
  proof (cases w)
    case (Fault f')
    with exec_c2 t have "f'=f"
      by (auto dest: execn_Fault_end)
    with Fault notinF Seq.hyps
    have "Γ⊨⟨strip_guards F c1,Normal s⟩ =n==> Fault f"
      by auto
    moreover have "Γ⊨⟨strip_guards F c2,Fault f⟩ =n==> Fault f"
      by auto
    ultimately show ?thesis
      by (auto intro: execn.intros)
  next
    case (Normal s')
    with execn_to_execn_strip_guards [OF exec_c1]
    have exec_strip_c1: "Γ⊨⟨strip_guards F c1,Normal s⟩ =n==> w"
      by simp
    with Seq.hyps t notinF
    have "Γ⊨⟨strip_guards F c2,w⟩ =n==> Fault f"
      by blast
    with exec_strip_c1 show ?thesis
      by (auto intro: execn.intros)
  next
    case (Abrupt s')
    with execn_to_execn_strip_guards [OF exec_c1]
    have exec_strip_c1: "Γ⊨⟨strip_guards F c1,Normal s⟩ =n==> w"
      by simp
    with Seq.hyps t notinF
    have "Γ⊨⟨strip_guards F c2,w⟩ =n==> Fault f"
      by (auto intro: execn.intros)
    with exec_strip_c1 show ?thesis
      by (auto intro: execn.intros)
  next
    case Stuck
    with exec_c2 have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with t show ?thesis by simp
  qed
next
  case CondTrue thus ?case by (fastforce intro: execn.intros)
next
  case CondFalse thus ?case by (fastforce intro: execn.intros)
next
  case (WhileTrue s b c n w t)
  have exec_c: "Γ⊨⟨c,Normal s⟩ =n==> w" by fact
  have exec_w: "Γ⊨⟨While b c,w⟩ =n==> t" by fact
  have t: "t = Fault f" by fact
  have notinF: "f ∉ F" by fact
  have s_in_b: "s ∈ b" by fact
  show ?case
  proof (cases w)
    case (Fault f')
    with exec_w t have "f'=f"
      by (auto dest: execn_Fault_end)
    with Fault notinF WhileTrue.hyps
    have "Γ⊨⟨strip_guards F c,Normal s⟩ =n==> Fault f"
      by auto
    moreover have "Γ⊨⟨strip_guards F (While b c),Fault f⟩ =n==> Fault f"
      by auto
    ultimately show ?thesis
      using s_in_b by (auto intro: execn.intros)
  next
    case (Normal s')
    with execn_to_execn_strip_guards [OF exec_c]
    have exec_strip_c: "Γ⊨⟨strip_guards F c,Normal s⟩ =n==> w"
      by simp
    with WhileTrue.hyps t notinF
    have "Γ⊨⟨strip_guards F (While b c),w⟩ =n==> Fault f"
      by blast
    with exec_strip_c s_in_b show ?thesis
      by (auto intro: execn.intros)
  next
    case (Abrupt s')
    with execn_to_execn_strip_guards [OF exec_c]
    have exec_strip_c: "Γ⊨⟨strip_guards F c,Normal s⟩ =n==> w"
      by simp
    with WhileTrue.hyps t notinF
    have "Γ⊨⟨strip_guards F (While b c),w⟩ =n==> Fault f"
      by (auto intro: execn.intros)
    with exec_strip_c s_in_b show ?thesis
      by (auto intro: execn.intros)
  next
    case Stuck
    with exec_w have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with t show ?thesis by simp
  qed
next
  case WhileFalse thus ?case by (fastforce intro: execn.intros)
next
  case Call thus ?case by (fastforce intro: execn.intros)
next
  case CallUndefined thus ?case by simp
next
  case StuckProp thus ?case by simp
next
  case DynCom thus ?case by (fastforce intro: execn.intros)
next
  case Throw thus ?case by simp
next
  case AbruptProp thus ?case by simp
next
  case (CatchMatch c1 s n w c2 t)
  have exec_c1: "Γ⊨⟨c1,Normal s⟩ =n==> Abrupt w" by fact
  have exec_c2: "Γ⊨⟨c2,Normal w⟩ =n==> t" by fact
  have t: "t = Fault f" by fact
  have notinF: "f ∉ F" by fact
  from execn_to_execn_strip_guards [OF exec_c1]
  have exec_strip_c1: "Γ⊨⟨strip_guards F c1,Normal s⟩ =n==> Abrupt w"
    by simp
  with CatchMatch.hyps t notinF
  have "Γ⊨⟨strip_guards F c2,Normal w⟩ =n==> Fault f"
    by blast
  with exec_strip_c1 show ?case
    by (auto intro: execn.intros)
next
  case CatchMiss thus ?case by (fastforce intro: execn.intros)
qed

lemma execn_to_execn_strip_guards':
 assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
 assumes t_not_Fault: "t ∉ Fault ` F"
 shows "Γ⊨⟨strip_guards F c,s⟩ =n==> t"
proof (cases t)
  case (Fault f)
  with t_not_Fault exec_c show ?thesis
    by (auto intro: execn_to_execn_strip_guards_Fault)
qed (insert exec_c, auto intro: execn_to_execn_strip_guards)

lemma execn_strip_guards_to_execn:
  "∧s n t. Γ⊨⟨strip_guards F c,s⟩ =n==> t
  ==> ∃t'. Γ⊨⟨c,s⟩ =n==> t' ∧
            (isFault t ⟶ isFault t') ∧
            (t' ∈ Fault ` (- F) ⟶ t'=t) ∧
            (¬ isFault t' ⟶ t'=t)"
proof (induct c)
  case Skip thus ?case by auto
next
  case Basic thus ?case by auto
next
  case Spec thus ?case by auto
next
  case (Seq c1 c2 s n t)
  have exec_strip: "Γ⊨⟨strip_guards F (Seq c1 c2),s⟩ =n==> t" by fact
  then obtain w where
    exec_strip_c1: "Γ⊨⟨strip_guards F c1,s⟩ =n==> w" and
    exec_strip_c2: "Γ⊨⟨strip_guards F c2,w⟩ =n==> t"
    by (auto elim: execn_elim_cases)
  from Seq.hyps exec_strip_c1
  obtain w' where
    exec_c1: "Γ⊨⟨c1,s⟩ =n==> w'" and
    w_Fault: "isFault w ⟶ isFault w'" and
    w'_Fault: "w' ∈ Fault ` (- F) ⟶ w'=w" and
    w'_noFault: "¬ isFault w' ⟶ w'=w"
    by blast
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec_strip have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_strip have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_strip have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    show ?thesis
    proof (cases "isFault w")
      case True
      then obtain f where w': "w=Fault f"..
      moreover with exec_strip_c2
      have t: "t=Fault f"
        by (auto dest: execn_Fault_end)
      ultimately show ?thesis
        using Normal w_Fault w'_Fault exec_c1
        by (fastforce intro: execn.intros elim: isFaultE)
    next
      case False
      note noFault_w = this
      show ?thesis
      proof (cases "isFault w'")
        case True
        then obtain f' where w': "w'=Fault f'"..
        with Normal exec_c1
        have exec: "Γ⊨⟨Seq c1 c2,s⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        from w'_Fault w' noFault_w
        have "f' ∈ F"
          by (cases w) auto
        with exec
        show ?thesis
          by auto
      next
        case False
        with w'_noFault have w': "w'=w" by simp
        from Seq.hyps exec_strip_c2
        obtain t' where
          "Γ⊨⟨c2,w⟩ =n==> t'" and
          "isFault t ⟶ isFault t'" and
          "t' ∈ Fault ` (-F) ⟶ t'=t" and
          "¬ isFault t' ⟶ t'=t"
          by blast
        with Normal exec_c1 w'
        show ?thesis
          by (fastforce intro: execn.intros)
      qed
    qed
  qed
next
next
  case (Cond b c1 c2 s n t)
  have exec_strip: "Γ⊨⟨strip_guards F (Cond b c1 c2),s⟩ =n==> t" by fact
  show ?case
  proof (cases s)
    case (Fault f)
    with exec_strip have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_strip have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_strip have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    show ?thesis
    proof (cases "s'∈ b")
      case True
      with Normal exec_strip
      have "Γ⊨⟨strip_guards F c1 ,Normal s'⟩ =n==> Year 020
        by (auto elim: execn_Normal_elim_cases)
      with Normal True Cond.hyps obtain t'
        where "Γ⟨ =n==>
            "isFault t ⟶
            "t' ∈ Fault t'=t"
            "¬ isFault t' ⟶ t' = t"
        by blast
      with Normal True
      show ?thesis
        by (blast intro: execn.intros)
    next
      case False
      with Norma
      have "Γ\         ncatenatedf term
        elim
      with region_addresses a si"
        where "Γ⊨⟨c2,Normal s'⟩ =n==> t'"
            "isFault t  ⟶
            in> Fault ` (-F) ⟶
            by
        byjava.lang.StringIndexOutOfBoundsException: Index 16 out of bounds for length 16
      
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
        by (blast
    qed
  qed
next
  case (Whilesjava.lang.StringIndexOutOfBoundsException: Index 24 out of bounds for length 24
  c_strip⊨ =n==>
  show ?case
  proof(
    casep: cal
    with exec_strip have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_strip have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_strip have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    {
      fix c' r w
      assume exec_c': "Γ⊨⟨c',r⟩ =n==> w"
      assume c': "c'=While b (strip_guards F c)"
      have "∃w'. Γ⊨⟨While b c,r⟩ =n==> w' ∧ (isFault w ⟶ isFault w') ∧
                   (w' ∈ Fault ` (-F) ⟶ w'=w) ∧
                   (¬ isFault w' ⟶ w'=w)"
        using exec_c' c'
      proof (induct)
        case (WhileTrue r b' c'' n u w)
        have eqs: "While b' c'' = While b (strip_guards F c)" by fact
        from WhileTrue.hyps eqs
        have r_in_b: "r∈b" by simp
        from WhileTrue.hyps eqs
        have exec_strip_c: "Γ⊨⟨strip_guards F c,Normal r⟩ =n==> u" by simp
        from WhileTrue.hyps eqs
        have exec_strip_w: "Γ⊨⟨While b (strip_guards F c),u⟩ =n==> w"
          by simp
        show ?case
        proof -
          from WhileTrue.hyps eqs have "Γ⊨⟨strip_guards F c,Normal r⟩ =n==> u"
            by simp
          with While.hyps
          obtain u' where
            exec_c: "Γ⊨⟨c,Normal r⟩ =n==> u'" and
            u_Fault: "isFault u ⟶ isFault u'" and
            u'_Fault: "u' ∈ Fault ` (-F) ⟶ u'=u" and
            u'_noFault: "¬ isFault u' ⟶ u'=u"
            by blast
          show ?thesis
          proof (cases "isFault u'")
            case False
            with u'_noFault have u': "u'=u" by simp
            from WhileTrue.hyps eqs obtain w' where
              "Γ⊨⟨While b c,u⟩ =n==> w'"
              "isFault w ⟶ isFault w'"
              "w' ∈ Fault ` (-F) ⟶ w'=w"
              "¬ isFault w' ⟶ w' = w"
              by blast
            with u' exec_c r_in_b
            show ?thesis
              by (blast intro: execn.WhileTrue)
          next
            case True
            then obtain f' where u': "u'=Fault f'"..
            with exec_c r_in_b
            have exec: "Γ⊨⟨While b c,Normal r⟩ =n==> Fault f'"
              by (blast intro: execn.intros)
            show ?thesis
            proof (cases "isFault u")
              case True
              then obtain f where u: "u=Fault f"..
              with exec_strip_w have "w=Fault f"
                by (auto dest: execn_Fault_end)
              with exec u' u u'_Fault
              show ?thesis
                by auto
            next
              case False
              with u'_Fault u' have "f' ∈ F"
                by (cases u) auto
              with exec show ?thesis
                by auto
            qed
          qed
        qed
      next
        case (WhileFalse r b' c'' n)
        have eqs: "While b' c'' = While b (strip_guards F c)" by fact
        from WhileFalse.hyps eqs
        have r_not_in_b: "r∉b" by simp
        show ?case
        proof -
          from r_not_in_b
          have "Γ⊨⟨While b c,Normal r⟩ =n==> Normal r"
            by (rule execn.WhileFalse)
          thus ?thesis
            by blast
        qed
      qed auto
    } note hyp_while = this
    show ?thesis
    proof (cases "s'∈b")
      case False
      with Normal exec_strip
      have "t=s"
        by (auto elim: execn_Normal_elim_cases)
      with Normal False show ?thesis
        by (auto intro: execn.intros)
    next
      case True note s'_in_b = this
      with Normal exec_strip obtain r where
        exec_strip_c: "Γ⊨⟨strip_guards F c,Normal s'⟩ =n==> r" and
        exec_strip_w: "Γ⊨⟨While b (strip_guards F c),r⟩ =n==> t"
        by (auto elim: execn_Normal_elim_cases)
      from While.hyps exec_strip_c obtain r' where
        exec_c: "Γ⊨⟨c,Normal s'⟩ =n==> r'" and
        r_Fault: "isFault r ⟶ isFault r'" and
        r'_Fault: "r' ∈ Fault ` (-F) ⟶ r'=r" and
        r'_noFault: "¬ isFault r' ⟶ r'=r"
        by blast
      show ?thesis
      proof (cases "isFault r'")
        case False
        with r'_noFault have r': "r'=r" by simp
        from hyp_while exec_strip_w
        obtain t' where
          "Γ⊨⟨While b c,r⟩ =n==> t'"
          "isFault t ⟶ isFault t'"
          "t' ∈ Fault ` (-F) ⟶ t'=t"
          "¬ isFault t' ⟶ t'=t"
          by blast
        with r' exec_c Normal s'_in_b
        show ?thesis
          by (blast intro: execn.intros)
      next
        case True
        then obtain f' where r': "r'=Fault f'"..
        hence "Γ⊨⟨While b c,r'⟩ =n==> Fault f'"
          by auto
        with Normal s'_in_b exec_c
        have exec: "Γ⊨⟨While b c,Normal s'⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        show ?thesis
        proof (cases "isFault r")
          case True
          then obtain f where r: "r=Fault f"..
          with exec_strip_w have "t=Fault f"
            by (auto dest: execn_Fault_end)
          with Normal exec r' r r'_Fault
          show ?thesis
            by auto
        next
          case False
          with r'_Fault r' have "f' ∈ F"
            by (cases r) auto
          with Normal exec show ?thesis
            by auto
        qed
      qed
    qed
  qed
next
  case Call thus ?case by auto
next
  case DynCom thus ?case
    by (fastforce elim!: execn_elim_cases intro: execn.intros)
next
  case (Guard f g c s n t)
  have exec_strip: "Γ⊨⟨strip_guards F (Guard f g c),s⟩ =n==> t" by fact
  show ?case
  proof (cases s)
    case (Fault f)
    with exec_strip have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_strip have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_strip have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s')
    show ?thesis
    proof (cases "f∈F")
      case True
      with exec_strip Normal
      have exec_strip_c: "Γ⊨⟨strip_guards F c,Normal s'⟩ =n==> t"
        by simp
      with Guard.hyps obtain t' where
        "Γ⊨⟨c,Normal s'⟩ =n==> t'" and
        "isFault t ⟶ isFault t'" and
        "t' ∈ Fault ` (-F) ⟶ t'=t" and
        "¬ isFault t' ⟶ t'=t"
        by blast
      with Normal True
      show ?thesis
        by (cases "s'∈ g") (fastforce intro: execn.intros)+
    next
      case False
      note f_notin_F = this
      show ?thesis
      proof (cases "s'∈g")
        case False
        with Normal exec_strip f_notin_F have t: "t=Fault f"
          by (auto elim: execn_Normal_elim_cases)
        from False
        have "Γ⊨⟨Guard f g c,Normal s'⟩ =n==> Fault f"
          by (blast intro: execn.intros)
        with False Normal t show ?thesis
          by auto
      next
        case True
        with exec_strip Normal f_notin_F
        have "Γ⊨⟨strip_guards F c,Normal s'⟩ =n==> t"
          by (auto elim: execn_Normal_elim_cases)
        with Guard.hyps obtain t' where
          "Γ⊨⟨c,Normal s'⟩ =n==> t'" and
          "isFault t ⟶ isFault t'" and
          "t' ∈ Fault ` (-F) ⟶ t'=t" and
          "¬ isFault t' ⟶ t'=t"
          by blast
        with Normal True
        show ?thesis
          by (blast intro: execn.intros)
      qed
    qed
  qed
next
  case Throw thus ?case by auto
next
  case (Catch c1 c2 s n t)
  have exec_strip: "Γ⊨⟨strip_guards F (Catch c1 c2),s⟩ =n==> t" by fact
  show ?case
  proof (cases "s")
    case (Fault f)
    with exec_strip have "t=Fault f"
      by (auto dest: execn_Fault_end)
    with Fault show ?thesis
      by auto
  next
    case Stuck
    with exec_strip have "t=Stuck"
      by (auto dest: execn_Stuck_end)
    with Stuck show ?thesis
      by auto
  next
    case (Abrupt s')
    with exec_strip have "t=Abrupt s'"
      by (auto dest: execn_Abrupt_end)
    with Abrupt show ?thesis
      by auto
  next
    case (Normal s') note s=this
    with exec_strip have
      "Γ⊨⟨Catch (strip_guards F c1) (strip_guards F c2),Normal s'⟩ =n==> t" by simp
    thus ?thesis
    proof (cases)
      fix w
      assume exec_strip_c1: "Γ⊨⟨strip_guards F c1,Normal s'⟩ =n==> Abrupt w"
      assume exec_strip_c2: "Γ⊨⟨strip_guards F c2,Normal w⟩ =n==> t"
      from exec_strip_c1 Catch.hyps
      obtain w' where
        exec_c1: "Γ⊨⟨c1,Normal s'⟩ =n==> w'" and
        w'_Fault: "w' ∈ Fault ` (-F) ⟶ w'=Abrupt w" and
        w'_noFault: "¬ isFault w' ⟶ w'=Abrupt w"
        by blast
      show ?thesis
      proof (cases "w'")
        case (Fault f')
        with Normal exec_c1 have "Γ⊨⟨Catch c1 c2,s⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        with w'_Fault Fault show ?thesis
          by auto
      next
        case Stuck
        with w'_noFault have False
          by simp
        thus ?thesis ..
      next
        case (Normal w'')
        with w'_noFault have False by simp thus ?thesis ..
      next
        case (Abrupt w'')
        with w'_noFault have w'': "w''=w" by simp
        from  exec_strip_c2 Catch.hyps
        obtain t' where
          "Γ⊨⟨c2,Normal w⟩ =n==> t'"
          "isFault t ⟶ isFault t'"
          "t' ∈ Fault ` (-F) ⟶ t'=t"
          "¬ isFault t' ⟶ t'=t"
          by blast
        with w'' Abrupt s exec_c1
        show ?thesis
          by (blast intro: execn.intros)
      qed
    next
      assume t: "¬ isAbr t"
      assume "Γ⊨⟨strip_guards F c1,Normal s'⟩ =n==> t"
      with Catch.hyps
      obtain t' where
        exec_c1: "Γ⊨⟨c1,Normal s'⟩ =n==> t'"  and
        t_Fault: "isFault t ⟶ isFault t'" and
        t'_Fault: "t' ∈ Fault ` (-F) ⟶ t'=t" and
        t'_noFault: "¬ isFault t' ⟶ t'=t"
        by blast
      show ?thesis
      proof (cases "isFault t'")
        case True
        then obtain f' where t': "t'=Fault f'"..
        with exec_c1 have "Γ⊨⟨Catch c1 c2,Normal s'⟩ =n==> Fault f'"
          by (auto intro: execn.intros)
        with t'_Fault t' s show ?thesis
          by auto
      next
        case False
        with t'_noFault have "t'=t" by simp
        with t exec_c1 s show ?thesis
          by (blast intro: execn.intros)
      qed
    qed
  qed
qed


lemma execn_strip_to_execn:
  assumes exec_strip: "strip F Γ⊨⟨c,s⟩ =n==> t"
  shows "∃t'. Γ⊨⟨c,s⟩ =n==> t' ∧
                 (isFault t ⟶ isFault t') ∧
                 (t' ∈ Fault ` (- F) ⟶ t'=t) ∧
                 (¬ isFault t' ⟶ t'=t)"
using exec_strip
proof (induct)
  case Skip thus ?case by (blast intro: execn.intros)
next
  case Guard thus ?case by (blast intro: execn.intros)
next
  case GuardFault thus ?case by (blast intro: execn.intros)
next
  case FaultProp thus ?case by (blast intro: execn.intros)
next
  case Basic thus ?case by (blast intro: execn.intros)
next
  case Spec thus ?case by (blast intro: execn.intros)
next
  case SpecStuck thus ?case by (blast intro: execn.intros)
next
  case Seq thus ?case by (blast intro: execn.intros elim: isFaultE)
next
  case CondTrue thus ?case by (blast intro: execn.intros)
next
  case CondFalse thus ?case by (blast intro: execn.intros)
next
  case WhileTrue thus ?case by (blast intro: execn.intros elim: isFaultE)
next
  case WhileFalse thus ?case by (blast intro: execn.intros)
next
  case Call thus ?case
    by simp (blast intro: execn.intros dest: execn_strip_guards_to_execn)
next
  case CallUndefined thus ?case
    by simp (blast intro: execn.intros)
next
  case StuckProp thus ?case
    by blast
next
  case DynCom thus ?case by (blast intro: execn.intros)
next
  case Throw thus ?case by (blast intro: execn.intros)
next
  case AbruptProp thus ?case by (blast intro: execn.intros)
next
  case (CatchMatch c1 s n r c2 t)
  then obtain r' t' where
    exec_c1: "Γ⊨⟨c1,Normal s⟩ =n==> r'"  and
    r'_Fault: "r' ∈ Fault ` (-F) ⟶ r' = Abrupt r" and
    r'_noFault: "¬ isFault r' ⟶ r' = Abrupt r" and
    exec_c2: "Γ⊨⟨c2,Normal r⟩ =n==> t'" and
    t_Fault: "isFault t ⟶ isFault t'" and
    t'_Fault: "t' ∈ Fault ` (-F) ⟶ t' = t" and
    t'_noFault: "¬ isFault t' ⟶ t' = t"
    by blast
  show ?case
  proof (cases "isFault r'")
    case True
    then obtain f' where r': "r'=Fault f'"..
    with exec_c1 have "Γ⊨⟨Catch c1 c2,Normal s⟩ =n==> Fault f'"
      by (auto intro: execn.intros)
    with r' r'_Fault show ?thesis
      by (auto intro: execn.intros)
  next
    case False
    with r'_noFault have "r'=Abrupt r" by simp
    with exec_c1 exec_c2 t_Fault t'_noFault t'_Fault
    show ?thesis
      by (blast intro: execn.intros)
  qed
next
  case CatchMiss thus ?case by (fastforce intro: execn.intros elim: isFaultE)
qed

lemma exec_strip_guards_to_exec:
  assumes exec_strip: "Γ⊨⟨strip_guards F c,s⟩ ==> t"
  shows "∃t'. Γ⊨⟨c,s⟩ ==> t' ∧
              (isFault t ⟶ isFault t') ∧
              (t' ∈ Fault ` (-F) ⟶ t'=t) ∧
              (¬ isFault t' ⟶ t'=t)"
proof -
  from exec_strip obtain n where
    execn_strip: "Γ⊨⟨strip_guards F c,s⟩ =n==> t"
    by (auto simp add: exec_iff_execn)
  then obtain t' where
    "Γ⊨⟨c,s⟩ =n==> t'"
    "isFault t ⟶ isFault t'" "t' ∈ Fault ` (-F) ⟶ t'=t" "¬ isFault t' ⟶ t'=t"
    by (blast dest: execn_strip_guards_to_execn)
  thus ?thesis
    by (blast intro: execn_to_exec)
qed

lemma exec_strip_to_exec:
  assumes exec_strip: "strip F Γ⊨⟨c,s⟩ ==> t"
  shows "∃t'. Γ⊨⟨c,s⟩ ==> t' ∧
              (isFault t ⟶ isFault t') ∧
              (t' ∈ Fault ` (-F) ⟶ t'=t) ∧
              (¬ isFault t' ⟶ t'=t)"
proof -
  from exec_strip obtain n where
    execn_strip: "strip F Γ⊨⟨c,s⟩ =n==> t"
    by (auto simp add: exec_iff_execn)
  then obtain t' where
    "Γ⊨⟨c,s⟩ =n==> t'"
    "isFault t ⟶ isFault t'" "t' ∈ Fault ` (-F) ⟶ t'=t" "¬ isFault t' ⟶ t'=t"
    by (blast dest: execn_strip_to_execn)
  thus ?thesis
    by (blast intro: execn_to_exec)
qed


lemma exec_to_exec_strip_guards:
 assumes exec_c: "Γ⊨⟨c,s⟩ ==> t"
 assumes t_not_Fault: "¬ isFault t"
 shows "Γ⊨⟨strip_guards F c,s⟩ ==> t"
proof -
  from exec_c obtain n where "Γ⊨⟨c,s⟩ =n==>t"
    by (auto simp add: exec_iff_execn)
  from this t_not_Fault
  have "Γ⊨⟨strip_guards F c,s⟩ =n==> t"
    by (rule execn_to_execn_strip_guards )
  thus "Γ⊨⟨strip_guards F c,s⟩ ==> t"
    by (rule execn_to_exec)
qed

lemma exec_to_exec_strip_guards':
 assumes exec_c: "Γ⊨⟨c,s⟩ ==> t"
 assumes t_not_Fault: "t ∉ Fault ` F"
 shows "Γ⊨⟨strip_guards F c,s⟩ ==> t"
proof -
  from exec_c obtain n where "Γ⊨⟨c,s⟩ =n==>t"
    by (auto simp add: exec_iff_execn)
  from this t_not_Fault
  have "Γ⊨⟨strip_guards F c,s⟩ =n==> t"
    by (rule execn_to_execn_strip_guards' )
  thus "Γ⊨⟨strip_guards F c,s⟩ ==> t"
    by (rule execn_to_exec)
qed

lemma execn_to_execn_strip:
 assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
 assumes t_not_Fault: "¬ isFault t"
 shows "strip F Γ⊨⟨c,s⟩ =n==> t"
using exec_c t_not_Fault
proof (induct)
  case (Call p bdy s n  s')
  have bdy: "Γ p = Some bdy" by fact
  from Call have "strip F Γ⊨⟨bdy,Normal s⟩ =n==> s'"
    by blast
  from execn_to_execn_strip_guards [OF this] Call
  have "strip F Γ⊨⟨strip_guards F bdy,Normal s⟩ =n==> s'"
    by simp
  moreover from bdy have "(strip F Γ) p = Some (strip_guards F bdy)"
    by simp
  ultimately
  show ?case
    by (blast intro: execn.intros)
next
  case CallUndefined thus ?case by (auto intro: execn.CallUndefined)
qed (auto intro: execn.intros dest: noFaultn_startD' simp add: not_isFault_iff)

lemma execn_to_execn_strip':
 assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
 assumes t_not_Fault: "t ∉ Fault ` F"
 shows "strip F Γ⊨⟨c,s⟩ =n==> t"
using exec_c t_not_Fault
proof (induct)
  case (Call p bdy s n s')
  have bdy: "Γ p = Some bdy" by fact
  from Call have "strip F Γ⊨⟨bdy,Normal s⟩ =n==> s'"
    by blast
  from execn_to_execn_strip_guards' [OF this] Call
  have "strip F Γ⊨⟨strip_guards F bdy,Normal s⟩ =n==> s'"
    by simp
  moreover from bdy have "(strip F Γ) p = Some (strip_guards F bdy)"
    by simp
  ultimately
  show ?case
    by (blast intro: execn.intros)
next
  case CallUndefined thus ?case by (auto intro: execn.CallUndefined)
next
  case (Seq c1 s n s' c2 t)
  show ?case
  proof (cases "isFault s'")
    case False
    with Seq show ?thesis
      by (auto intro: execn.intros simp add: not_isFault_iff)
  next
    case True
    then obtain f' where s': "s'=Fault f'" by (auto simp add: isFault_def)
    with Seq obtain "t=Fault f'" and "f' ∉ F"
      by (force dest: execn_Fault_end)
    with Seq s' show ?thesis
      by (auto intro: execn.intros)
  qed
next
  case (WhileTrue b c s n s' t)
  show ?case
  proof (cases "isFault s'")
    case False
    with WhileTrue show ?thesis
      by (auto intro: execn.intros simp add: not_isFault_iff)
  next
    case True
    then obtain f' where s': "s'=Fault f'" by (auto simp add: isFault_def)
    with WhileTrue obtain "t=Fault f'" and "f' ∉ F"
      by (force dest: execn_Fault_end)
    with WhileTrue s' show ?thesis
      by (auto intro: execn.intros)
  qed
qed (auto intro: execn.intros)

lemma exec_to_exec_strip:
 assumes exec_c: "Γ⊨⟨c,s⟩ ==> t"
 assumes t_not_Fault: "¬ isFault t"
 shows "strip F Γ⊨⟨c,s⟩ ==> t"
proof -
  from exec_c obtain n where "Γ⊨⟨c,s⟩ =n==>t"
    by (auto simp add: exec_iff_execn)
  from this t_not_Fault
  have "strip F Γ⊨⟨c,s⟩ =n==> t"
    by (rule execn_to_execn_strip)
  thus "strip F Γ⊨⟨c,s⟩ ==> t"
    by (rule execn_to_exec)
qed

lemma exec_to_exec_strip':
 assumes exec_c: "Γ⊨⟨c,s⟩ ==> t"
 assumes t_not_Fault: "t ∉ Fault ` F"
 shows "strip F Γ⊨⟨c,s⟩ ==> t"
proof -
  from exec_c obtain n where "Γ⊨⟨c,s⟩ =n==>t"
    by (auto simp add: exec_iff_execn)
  from this t_not_Fault
  have "strip F Γ⊨⟨c,s⟩ =n==> t"
    by (rule execn_to_execn_strip' )
  thus "strip F Γ⊨⟨c,s⟩ ==> t"
    by (rule execn_to_exec)
qed

lemma exec_to_exec_strip_guards_Fault:
 assumes exec_c: "Γ⊨⟨c,s⟩ ==> Fault f"
 assumes f_notin_F: "f ∉ F"
 shows"Γ⊨⟨strip_guards F c,s⟩ ==> Fault f"
proof -
  from exec_c obtain n where "Γ⊨⟨c,s⟩ =n==>Fault f"
    by (auto simp add: exec_iff_execn)
  from execn_to_execn_strip_guards_Fault [OF this _ f_notin_F]
  have "Γ⊨⟨strip_guards F c,s⟩ =n==> Fault f"
    by simp
  thus "Γ⊨⟨strip_guards F c,s⟩ ==> Fault f"
    by (rule execn_to_exec)
qed

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

lemma inter_guards_execn_Normal_noFault:
  "∧c c2 s t n. [(c1 ∩_g c2) = Some c; Γ⊨⟨c,Normal s⟩ =n==> t; ¬ isFault t]
        ==> Γ⊨⟨c1,Normal s⟩ =n==> t ∧ Γ⊨⟨c2,Normal s⟩ =n==> t"
proof (induct c1)
  case Skip
  have "(Skip ∩_g c2) = Some c" by fact
  then obtain c2: "c2=Skip" and c: "c=Skip"
    by (simp add: inter_guards_Skip)
  have "Γ⊨⟨c,Normal s⟩ =n==> t" by fact
  with c have "t=Normal s"
    by (auto elim: execn_Normal_elim_cases)
  with Skip c2
  show ?case
    by (auto intro: execn.intros)
next
  case (Basic f)
  have "(Basic f ∩_g c2) = Some c" by fact
  then obtain c2: "c2=Basic f" and c: "c=Basic f"
    by (simp add: inter_guards_Basic)
  have "Γ⊨⟨c,Normal s⟩ =n==> t" by fact
  with c have "t=Normal (f s)"
    by (auto elim: execn_Normal_elim_cases)
  with Basic c2
  show ?case
    by (auto intro: execn.intros)
next
  case (Spec r)
  have "(Spec r ∩_g c2) = Some c" by fact
  then obtain c2: "c2=Spec r" and c: "c=Spec r"
    by (simp add: inter_guards_Spec)
  have "Γ⊨⟨c,Normal s⟩ =n==> t" by fact
  with c have "Γ⊨⟨Spec r,Normal s⟩ =n==> t" by simp
  from this Spec c2 show ?case
    by (cases) (auto intro: execn.intros)
next
  case (Seq a1 a2)
  have noFault: "¬ isFault t" by fact
  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 "Γ⊨⟨c,Normal s⟩ =n==> t" by fact
  with c obtain s' where
    exec_d1: "Γ⊨⟨d1,Normal s⟩ =n==> s'" and
    exec_d2: "Γ⊨⟨d2,s'⟩ =n==> t"
    by (auto elim: execn_Normal_elim_cases)
  show ?case
  proof (cases s')
    case (Fault f')
    with exec_d2 have "t=Fault f'"
      by (auto intro: execn_Fault_end)
    with noFault show  ?thesis by simp
  next
    case (Normal s'')
    with d1 exec_d1 Seq.hyps
    obtain
      "Γ⊨⟨a1,Normal s⟩ =n==> Normal s''" and "Γ⊨⟨b1,Normal s⟩ =n==> Normal s''"
      by auto
    moreover
    from Normal d2 exec_d2 noFault Seq.hyps
    obtain "Γ⊨⟨a2,Normal s''⟩ =n==> t" and "Γ⊨⟨b2,Normal s''⟩ =n==> t"
      by auto
    ultimately
    show ?thesis
      using Normal c2 by (auto intro: execn.intros)
  next
    case (Abrupt s'')
    with exec_d2 have "t=Abrupt s''"
      by (auto simp add: execn_Abrupt_end)
    moreover
    from Abrupt d1 exec_d1 Seq.hyps
    obtain "Γ⊨⟨a1,Normal s⟩ =n==> Abrupt s''" and "Γ⊨⟨b1,Normal s⟩ =n==> Abrupt s''"
      by auto
    moreover
    obtain
      "Γ⊨⟨a2,Abrupt s''⟩ =n==> Abrupt s''" and "Γ⊨⟨b2,Abrupt s''⟩ =n==> Abrupt s''"
      by auto
    ultimately
    show ?thesis
      using Abrupt c2 by (auto intro: execn.intros)
  next
    case Stuck
    with exec_d2 have "t=Stuck"
      by (auto simp add: execn_Stuck_end)
    moreover
    from Stuck d1 exec_d1 Seq.hyps
    obtain "Γ⊨⟨a1,Normal s⟩ =n==> Stuck" and "Γ⊨⟨b1,Normal s⟩ =n==> Stuck"
      by auto
    moreover
    obtain
      "Γ⊨⟨a2,Stuck⟩ =n==> Stuck" and "Γ⊨⟨b2,Stuck⟩ =n==> Stuck"
      by auto
    ultimately
    show ?thesis
      using Stuck c2 by (auto intro: execn.intros)
  qed
next
  case (Cond b t1 e1)
  have noFault: "¬ isFault t" by fact
  have "(Cond b t1 e1 ∩_g c2) = Some c" by fact
  then obtain t2 e2 t3 e3 where
    c2: "c2=Cond b t2 e2" and
    t3: "(t1 ∩_g t2) = Some t3" and
    e3: "(e1 ∩_g e2) = Some e3" and
    c: "c=Cond b t3 e3"
    by (auto simp add: inter_guards_Cond)
  have "Γ⊨⟨c,Normal s⟩ =n==> t" by fact
  with c have "Γ⊨⟨Cond b t3 e3,Normal s⟩ =n==> t"
    by simp
  then show ?case
  proof (cases)
    assume s_in_b: "s∈b"
    assume "Γ⊨⟨t3,Normal s⟩ =n==> t"
    with Cond.hyps t3 noFault
    obtain "Γ⊨⟨t1,Normal s⟩ =n==> t" "Γ⊨⟨t2,Normal s⟩ =n==> t"
      by auto
    with s_in_b c2 show ?thesis
      by (auto intro: execn.intros)
  next
    assume s_notin_b: "s∉b"
    assume "Γ⊨⟨e3,Normal s⟩ =n==> t"
    with Cond.hyps e3 noFault
    obtain "Γ⊨⟨e1,Normal s⟩ =n==> t" "Γ⊨⟨e2,Normal s⟩ =n==> t"
      by auto
    with s_notin_b c2 show ?thesis
      by (auto intro: execn.intros)
  qed
next
  case (While b bdy1)
  have noFault: "¬ isFault t" by fact
  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 exec_c: "Γ⊨⟨c,Normal s⟩ =n==> t" by fact
  {
    fix s t n w w1 w2
    assume exec_w: "Γ⊨⟨w,Normal s⟩ =n==> t"
    assume w: "w=While b bdy"
    assume noFault: "¬ isFault t"
    from exec_w w noFault
    have "Γ⊨⟨While b bdy1,Normal s⟩ =n==> t ∧
          Γ⊨⟨While b bdy2,Normal s⟩ =n==> t"
    proof (induct)
      prefer 10
      case (WhileTrue s b' bdy' n s' s'')
      have eqs: "While b' bdy' = While b bdy" by fact
      from WhileTrue have s_in_b: "s ∈ b" by simp
      have noFault_s'': "¬ isFault s''"  by fact
      from WhileTrue
      have exec_bdy: "Γ⊨⟨bdy,Normal s⟩ =n==> s'" by simp
      from WhileTrue
      have exec_w: "Γ⊨⟨While b bdy,s'⟩ =n==> s''" by simp
      show ?case
      proof (cases s')
        case (Fault f)
        with exec_w have "s''=Fault f"
          by (auto intro: execn_Fault_end)
        with noFault_s'' show ?thesis by simp
      next
        case (Normal s''')
        with exec_bdy bdy While.hyps
        obtain "Γ⊨⟨bdy1,Normal s⟩ =n==> Normal s'''"
               "Γ⊨⟨bdy2,Normal s⟩ =n==> Normal s'''"
          by auto
        moreover
        from Normal WhileTrue
        obtain
          "Γ⊨⟨While b bdy1,Normal s'''⟩ =n==> s''"
          "Γ⊨⟨While b bdy2,Normal s'''⟩ =n==> s''"
          by simp
        ultimately show ?thesis
          using s_in_b Normal
          by (auto intro: execn.intros)
      next
        case (Abrupt s''')
        with exec_bdy bdy While.hyps
        obtain "Γ⊨⟨bdy1,Normal s⟩ =n==> Abrupt s'''"
               "Γ⊨⟨bdy2,Normal s⟩ =n==> Abrupt s'''"
          by auto
        moreover
        from Abrupt WhileTrue
        obtain
          "Γ⊨⟨While b bdy1,Abrupt s'''⟩ =n==> s''"
          "Γ⊨⟨While b bdy2,Abrupt s'''⟩ =n==> s''"
          by simp
        ultimately show ?thesis
          using s_in_b Abrupt
          by (auto intro: execn.intros)
      next
        case Stuck
        with exec_bdy bdy While.hyps
        obtain "Γ⊨⟨bdy1,Normal s⟩ =n==> Stuck"
               "Γ⊨⟨bdy2,Normal s⟩ =n==> Stuck"
          by auto
        moreover
        from Stuck WhileTrue
        obtain
          "Γ⊨⟨While b bdy1,Stuck⟩ =n==> s''"
          "Γ⊨⟨While b bdy2,Stuck⟩ =n==> s''"
          by simp
        ultimately show ?thesis
          using s_in_b Stuck
          by (auto intro: execn.intros)
      qed
    next
      case WhileFalse thus ?case by (auto intro: execn.intros)
    qed (simp_all)
  }
  with this [OF exec_c c noFault] c2
  show ?case
    by auto
next
  case Call thus ?case by (simp add: inter_guards_Call)
next
  case (DynCom f1)
  have noFault: "¬ isFault t" by fact
  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 "Γ⊨⟨c,Normal s⟩ =n==> t" by fact
  with c have "Γ⊨⟨DynCom (λs. the ((f1 s) ∩_g (f2 s))),Normal s⟩ =n==> t" by simp
  then show ?case
  proof (cases)
    assume exec_f: "Γ⊨⟨the (f1 s ∩_g f2 s),Normal s⟩ =n==> t"
    from f_defined obtain f where "(f1 s ∩_g f2 s) = Some f"
      by auto
    with DynCom.hyps this exec_f c2 noFault
    show ?thesis
      using execn.DynCom by fastforce
  qed
next
  case Guard thus ?case
    by (fastforce elim: execn_Normal_elim_cases intro: execn.intros
        simp add: inter_guards_Guard)
next
  case Throw thus ?case
    by (fastforce elim: execn_Normal_elim_cases
        simp add: inter_guards_Throw)
next
  case (Catch a1 a2)
  have noFault: "¬ isFault t" by fact
  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 "Γ⊨⟨c,Normal s⟩ =n==> t" by fact
  with c have "Γ⊨⟨Catch d1 d2,Normal s⟩ =n==> t" by simp
  then show ?case
  proof (cases)
    fix s'
    assume "Γ⊨⟨d1,Normal s⟩ =n==> Abrupt s'"
    with d1 Catch.hyps
    obtain "Γ⊨⟨a1,Normal s⟩ =n==> Abrupt s'" and "Γ⊨⟨b1,Normal s⟩ =n==> Abrupt s'"
      by auto
    moreover
    assume "Γ⊨⟨d2,Normal s'⟩ =n==> t"
    with d2 Catch.hyps noFault
    obtain "Γ⊨⟨a2,Normal s'⟩ =n==> t" and "Γ⊨⟨b2,Normal s'⟩ =n==> t"
      by auto
    ultimately
    show ?thesis
      using c2 by (auto intro: execn.intros)
  next
    assume "¬ isAbr t"
    moreover
    assume "Γ⊨⟨d1,Normal s⟩ =n==> t"
    with d1 Catch.hyps noFault
    obtain "Γ⊨⟨a1,Normal s⟩ =n==> t" and "Γ⊨⟨b1,Normal s⟩ =n==> t"
      by auto
    ultimately
    show ?thesis
      using c2 by (auto intro: execn.intros)
  qed
qed


lemma inter_guards_execn_noFault:
  assumes c: "(c1 ∩_g c2) = Some c"
  assumes exec_c: "Γ⊨⟨c,s⟩ =n==> t"
  assumes noFault: "¬ isFault t"
  shows "Γ⊨⟨c1,s⟩ =n==> t ∧ Γ⊨⟨c2,s⟩ =n==> t"
proof (cases s)
  case (Fault f)
  with exec_c have "t = Fault f"
    by (auto intro: execn_Fault_end)
    with noFault show ?thesis
    by simp
next
  case (Abrupt s')
  with exec_c have "t=Abrupt s'"
    by ((simp: execn_Abrupt_end)
  with Abrupt show ?thesis by auto
next
  case Stuck
  with exec_c have "t=Stuck"
    by (simp add: execn_Stuck_end)
  with Stuck show ?thesis by auto
next
  case (Normal s')
  with exec_c noFault inter_guards_execn_Normal_noFault [OF c]
  show ?thesis
    by blast
qed

lemma inter_guards_exec_noFault:
  assumes c: "(c1 ∩_g c2) = Some c"
  assumes exec_c: "Γ⊨⟨c,s⟩ ==> t"
  assumes noFault: "¬ isFault t"
  shows "Γ⊨⟨c1,s⟩ ==> t ∧ Γ⊨⟨c2,s⟩ ==> t"
proof -
  from exec_c obtain n where "Γ⊨⟨c,s⟩ =n==> t"
    by (auto simp add: exec_iff_execn)
  from c this noFault
  have "Γ⊨⟨c1,s⟩ =n==> t ∧ Γ⊨⟨c2,s⟩ =n==> t"
    by (rule inter_guards_execn_noFault)
  thus ?thesis
    by (auto intro: execn_to_exec)
qed


lemma inter_guards_execn_Normal_Fault:
  "∧c c2 s n. [(c1 ∩_g c2) = Some c; Γ⊨⟨c,Normal s⟩ =n==> Fault f]
        ==> (Γ⊨⟨c1,Normal s⟩ =n==> Fault f ∨ Γ⊨⟨c2,Normal s⟩ =n==> Fault f)"
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 "Γ⊨⟨c,Normal s⟩ =n==> Fault f" by fact
  with c obtain s' where
    exec_d1: "Γ⊨⟨d1,Normal s⟩ =n==> s'" and
    exec_d2: "Γ⊨⟨d2,s'⟩ =n==> Fault f"
    by (auto elim: execn_Normal_elim_cases)
  show ?case
  proof (cases s')
    case (Fault f')
    with exec_d2 have "f'=f"
      by (auto dest: execn_Fault_end)
    with Fault d1 exec_d1
    have "Γ⊨⟨a1,Normal s⟩ =n==> Fault f ∨ Γ⊨⟨b1,Normal s⟩ =n==> Fault f"
      by (auto dest: Seq.hyps)
    thus ?thesis
    proof (cases rule: disjE [consumes 1])
      assume "Γ⊨⟨a1,Normal s⟩ =n==> Fault f"
      hence "Γ⊨⟨Seq a1 a2,Normal s⟩ =n==> Fault f"
        by (auto intro: execn.intros)
      thus ?thesis
        by simp
    next
      assume "Γ⊨⟨b1,Normal s⟩ =n==> Fault f"
      hence "Γ⊨⟨Seq b1 b2,Normal s⟩ =n==> Fault f"
        by (auto intro: execn.intros)
      with c2 show ?thesis
        by simp
    qed
  next
    case Abrupt with exec_d2 show ?thesis by (auto dest: execn_Abrupt_end)
  next
    case Stuck with exec_d2 show ?thesis by (auto dest: execn_Stuck_end)
  next
    case (Normal s'')
    with inter_guards_execn_noFault [OF d1 exec_d1] obtain
      exec_a1: "Γ⊨⟨a1,Normal s⟩ =n==> Normal s''" and
      exec_b1: "Γ⊨⟨b1,Normal s⟩ =n==> Normal s''"
      by simp
    moreover from d2 exec_d2 Normal
    have "Γ⊨⟨a2,Normal s''⟩ =n==> Fault f ∨ Γ⊨⟨b2,Normal s''⟩ =n==> Fault f"
      by (auto dest: Seq.hyps)
    ultimately show ?thesis
      using c2 by (auto intro: execn.intros)
  qed
next
  case (Cond b t1 e1)
  have "(Cond b t1 e1 ∩_g c2) = Some c" by fact
  then obtain t2 e2 t e where
    c2: "c2=Cond b t2 e2" and
    t: "(t1 ∩_g t2) = Some t" and
    e: "(e1 ∩_g e2) = Some e" and
    c: "c=Cond b t e"
    by (auto simp add: inter_guards_Cond)
  have "Γ⊨⟨c,Normal s⟩ =n==> Fault f" by fact
  with c have "Γ⊨⟨Cond b t e,Normal s⟩ =n==> Fault f" by simp
  thus ?case
  proof (cases)
    assume "s ∈ b"
    moreover assume "Γ⊨⟨t,Normal s⟩ =n==> Fault f"
    with t have "Γ⊨⟨t1,Normal s⟩ =n==> Fault f ∨ Γ⊨⟨t2,Normal s⟩ =n==> Fault f"
      by (auto dest: Cond.hyps)
    ultimately show ?thesis using c2 c by (fastforce intro: execn.intros)
  next
    assume "s ∉ b"
    moreover assume "Γ⊨⟨e,Normal s⟩ =n==> Fault f"
    with e have "Γ⊨⟨e1,Normal s⟩ =n==> Fault f ∨ Γ⊨⟨e2,Normal s⟩ =n==> Fault f"
      by (auto dest: Cond.hyps)
    ultimately show ?thesis using c2 c by (fastforce intro: execn.intros)
  qed
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 exec_c: "Γ⊨⟨c,Normal s⟩ =n==> Fault f" by fact
  {
    fix s t n w w1 w2
    assume exec_w: "Γ⊨⟨w,Normal s⟩ =n==> t"
    assume w: "w=While b bdy"
    assume Fault: "t=Fault f"
    from exec_w w Fault
    have "Γ⊨⟨While b bdy1,Normal s⟩ =n==> Fault f∨
          Γ⊨⟨While b bdy2,Normal s⟩ =n==> Fault f"
    proof (induct)
      case (WhileTrue s b' bdy' n  s' s'')
      have eqs: "While b' bdy' = While b bdy" by fact
      from WhileTrue have s_in_b: "s ∈ b" by simp
      have Fault_s'': "s''=Fault f"  by fact
      from WhileTrue
      have exec_bdy: "Γ⊨⟨bdy,Normal s⟩ =n==> s'" by simp
      from WhileTrue
      have exec_w: "Γ⊨⟨While b bdy,s'⟩ =n==> s''" by simp
      show ?case
      proof (cases s')
        case (Fault f')
        with exec_w Fault_s'' have "f'=f"
          by (auto dest: execn_Fault_end)
        with Fault exec_bdy bdy While.hyps
        have "Γ⊨⟨bdy1,Normal s⟩ =n==> Fault f ∨ Γ⊨⟨bdy2,Normal s⟩ =n==> Fault f"
          by auto
        with s_in_b show ?thesis
          by (fastforce intro: execn.intros)
      next
        case (Normal s''')
        with inter_guards_execn_noFault [OF bdy exec_bdy]
        obtain "Γ⊨⟨bdy1,Normal s⟩ =n==> Normal s'''"
               "Γ⊨⟨bdy2,Normal s⟩ =n==> Normal s'''"
          by auto
        moreover
        from Normal WhileTrue
        have "Γ⊨⟨While b bdy1,Normal s'''⟩ =n==> Fault f ∨
              Γ⊨⟨While b bdy2,Normal s'''⟩ =n==> Fault f"
          by simp
        ultimately show ?thesis
          using s_in_b by (fastforce intro: execn.intros)
      next
        case (Abrupt s''')
        with exec_w Fault_s'' show ?thesis by (fastforce dest: execn_Abrupt_end)
      next
        case Stuck
        with exec_w Fault_s'' show ?thesis by (fastforce dest: execn_Stuck_end)
      qed
    next
      case WhileFalse thus ?case by (auto intro: execn.intros)
    qed (simp_all)
  }
  with this [OF exec_c c] c2
  show ?case
    by auto
next
  case Call thus ?case by (fastforce simp add: inter_guards_Call)
next
  case (DynCom f1)
  have "(DynCom f1 ∩_g c2) = Some c" by fact
  then obtain f2  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 "Γ⊨⟨c,Normal s⟩ =n==> Fault f" by fact
  with c have "Γ⊨⟨DynCom (λs. the ((f1 s) ∩_g (f2 s))),Normal s⟩ =n==> Fault f" by simp
  then show ?case
  proof (cases)
    assume exec_F: "Γ⊨⟨the (f1 s ∩_g f2 s),Normal s⟩ =n==> Fault f"
    from F_defined obtain F where "(f1 s ∩_g f2 s) = Some F"
      by auto
    with DynCom.hyps this exec_F c2
    show ?thesis
      by (fastforce intro: execn.intros)
  qed
next
  case (Guard m g1 bdy1)
  have "(Guard m g1 bdy1 ∩_g c2) = Some c" by fact
  then obtain g2 bdy2 bdy where
    c2: "c2=Guard m g2 bdy2" and
    bdy: "(bdy1 ∩_g bdy2) = Some bdy" and
    c: "c=Guard m (g1 ∩ g2) bdy"
    by (auto simp add: inter_guards_Guard)
  have "Γ⊨⟨c,Normal s⟩ =n==> Fault f" by fact
  with c have "Γ⊨⟨Guard m (g1 ∩ g2) bdy,Normal s⟩ =n==> Fault f"
    by simp
  thus ?case
  proof (cases)
    assume f_m: "Fault f = Fault m"
    assume "s ∉ g1 ∩ g2"
    hence "s∉g1 ∨ s∉g2"
      by blast
    with c2 f_m show ?thesis
      by (auto intro: execn.intros)
  next
    assume "s ∈ g1 ∩ g2"
    moreover
    assume "Γ⊨⟨bdy,Normal s⟩ =n==> Fault f"
    with bdy have "Γ⊨⟨bdy1,Normal s⟩ =n==> Fault f ∨ Γ⊨⟨bdy2,Normal s⟩ =n==> Fault f"
      by (rule Guard.hyps)
    ultimately show ?thesis
      using c2
      by (auto intro: execn.intros)
  qed
next
  case Throw thus ?case by (fastforce 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 "Γ⊨⟨c,Normal s⟩ =n==> Fault f" by fact
  with c have "Γ⊨⟨Catch d1 d2,Normal s⟩ =n==> Fault f" by simp
  thus ?case
  proof (cases)
    fix s'
    assume "Γ⊨⟨d1,Normal s⟩ =n==> Abrupt s'"
    from inter_guards_execn_noFault [OF d1 this] obtain
      exec_a1: "Γ⊨⟨a1,Normal s⟩ =n==> Abrupt s'" and
      exec_b1: "Γ⊨⟨b1,Normal s⟩ =n==> Abrupt s'"
      by simp
    moreover assume  "Γ⊨⟨d2,Normal s'⟩ =n==> Fault f"
    with d2
    have "Γ⊨⟨a2,Normal s'⟩ =n==> Fault f ∨ Γ⊨⟨b2,Normal s'⟩ =n==> Fault f"
      by (auto dest: Catch.hyps)
    ultimately show ?thesis
      using c2 by (fastforce intro: execn.intros)
  next
    assume "Γ⊨⟨d1,Normal s⟩ =n==> Fault f"
    with d1 have "Γ⊨⟨a1,Normal s⟩ =n==> Fault f ∨ Γ⊨⟨b1,Normal s⟩ =n==> Fault f"
      by (auto dest: Catch.hyps)
    with c2 show ?thesis
      by (fastforce intro: execn.intros)
  qed
qed


lemma inter_guards_execn_Fault:
  assumes c: "(c1 ∩_g c2) = Some c"
  assumes exec_c: "Γ⊨⟨c,s⟩ =n==> Fault f"
  shows "Γ⊨⟨c1,s⟩ =n==> Fault f ∨ Γ⊨⟨c2,s⟩ =n==> Fault f"
proof (cases s)
  case (Fault f)
  with exec_c show ?thesis
    by (auto dest: execn_Fault_end)
next
  case (Abrupt s')
  with exec_c show ?thesis
    by (fastforce dest: execn_Abrupt_end)
next
  case Stuck
  with exec_c show ?thesis
    by (fastforce dest: execn_Stuck_end)
next
  case (Normal s')
  with exec_c inter_guards_execn_Normal_Fault [OF c]
  show ?thesis
    by blast
qed

lemma inter_guards_exec_Fault:
  assumes c: "(c1 ∩_g c2) = Some c"
  assumes exec_c: "Γ⊨⟨c,s⟩ ==> Fault f"
  shows "Γ⊨⟨c1,s⟩ ==> Fault f ∨ Γ⊨⟨c2,s⟩ ==> Fault f"
proof -
  from exec_c obtain n where "Γ⊨⟨c,s⟩ =n==> Fault f"
    by (auto simp add: exec_iff_execn)
  from c this
  have "Γ⊨⟨c1,s⟩ =n==> Fault f ∨ Γ⊨⟨c2,s⟩ =n==> Fault f"
    by (rule inter_guards_execn_Fault)
  thus ?thesis
    by (auto intro: execn_to_exec)
qed


(* ************************************************************************* *)
subsection "Restriction of Procedure Environment"
(* ************************************************************************* *)

lemma restrict_SomeD: "(m|) x = Some y ==> m x = Some y"
  by (auto simp add: restrict_map_def split: if_split_asm)

(* fixme: To Map *)
lemma restrict_dom_same [simp]: "m| _m = m"
  apply (rule ext)
  apply (clarsimp simp add: restrict_map_def)
  apply (simp only: not_None_eq [symmetric])
  apply rule
  apply (drule sym)
  apply blast
  done

lemma restrict_in_dom: "x ∈ A ==> (m|) x = m x"
  by (auto simp add: restrict_map_def)


lemma exec_restrict_to_exec:
  assumes exec_restrict: "Γ|⊨⟨c,s⟩ ==> t"
  assumes notStuck: "t≠Stuck"
  shows "Γ⊨⟨c,s⟩ ==> t"
using exec_restrict notStuck
by (induct) (auto intro: exec.intros dest: restrict_SomeD Stuck_end)

lemma execn_restrict_to_execn:
  assumes exec_restrict: "Γ|⊨⟨c,s⟩ =n==> t"
  assumes notStuck: "t≠Stuck"
  shows "Γ⊨⟨c,s⟩ =n==> t"
using exec_restrict notStuck
by (induct) (auto intro: execn.intros dest: restrict_SomeD execn_Stuck_end)

lemma restrict_NoneD: "m x = None ==> (m|) x = None"
  by (auto simp add: restrict_map_def split: if_split_asm)

lemma execn_to_execn_restrict:
  assumes execn: "Γ⊨⟨c,s⟩ =n==> t"
  shows "∃t'. Γ|⊨⟨c,s⟩ =n==> t' ∧ (t=Stuck ⟶ t'=Stuck) ∧
                (∀f. t=Fault f ⟶ t'∈{Fault f,Stuck}) ∧ (t'≠Stuck ⟶ t'=t)"
using execn
proof (induct)
  case Skip show ?case by (blast intro: execn.Skip)
next
  case Guard thus ?case by (auto intro: execn.Guard)
next
  case GuardFault thus ?case by (auto intro: execn.GuardFault)
next
  case FaultProp thus ?case by (auto intro: execn.FaultProp)
next
  case Basic thus ?case by (auto intro: execn.Basic)
next
  case Spec thus ?case by (auto intro: execn.Spec)
next
  case SpecStuck thus ?case by (auto intro: execn.SpecStuck)
next
  case Seq thus ?case by (metis insertCI execn.Seq StuckProp)
next
  case CondTrue thus ?case by (auto intro: execn.CondTrue)
next
  case CondFalse thus ?case by (auto intro: execn.CondFalse)
next
  case WhileTrue thus ?case by (metis insertCI execn.WhileTrue StuckProp)
next
  case WhileFalse thus ?case by (auto intro: execn.WhileFalse)
next
  case (Call p bdy n s s')
  have "Γ p = Some bdy" by fact
  show ?case
  proof (cases "p ∈ P")
    case True
    with Call have "(Γ|) p = Some bdy"
      by (simp)
    with Call show ?thesis
      by (auto intro: execn.intros)
  next
    case False
    hence "(Γ|) p = None" by simp
    thus ?thesis
      by (auto intro: execn.CallUndefined)
  qed
next
  case (CallUndefined p n s)
  have "Γ p = None" by fact
  hence "(Γ|) p = None" by (rule restrict_NoneD)
  thus ?case by (auto intro: execn.CallUndefined)
next
  case StuckProp thus ?case by (auto intro: execn.StuckProp)
next
  case DynCom thus ?case by (auto intro: execn.DynCom)
next
  case Throw thus ?case by (auto intro: execn.Throw)
next
  case AbruptProp thus ?case by (auto intro: execn.AbruptProp)
next
  case (CatchMatch c1 s n s' c2 s'')
  from CatchMatch.hyps
  obtain t' t'' where
    exec_res_c1: "Γ|⊨⟨c1,Normal s⟩ =n==> t'" and
    t'_notStuck: "t' ≠ Stuck ⟶ t' = Abrupt s'" and
    exec_res_c2: "Γ|⊨⟨c2,Normal s'⟩ =n==> t''" and
    s''_Stuck: "s'' = Stuck ⟶ t'' = Stuck" and
    s''_Fault: "∀f. s'' = Fault f ⟶ t'' ∈ {Fault f, Stuck}" and
    t''_notStuck: "t'' ≠ Stuck ⟶ t'' = s''"
    by auto
  show ?case
  proof (cases "t'=Stuck")
    case True
    with exec_res_c1
    have "Γ|⊨⟨Catch c1 c2,Normal s⟩ =n==> Stuck"
      by (auto intro: execn.CatchMiss)
    thus ?thesis
      by auto
  next
    case False
    with t'_notStuck have "t'= Abrupt s'"
      by simp
    with exec_res_c1 exec_res_c2
    have "Γ|⊨⟨Catch c1 c2,Normal s⟩ =n==> t''"
      by (auto intro: execn.CatchMatch)
    with s''_Stuck s''_Fault t''_notStuck
    show ?thesis
      by blast
  qed
next
  case (CatchMiss c1 s n w c2)
  have exec_c1: "Γ⊨⟨c1,Normal s⟩ =n==> w" by fact
  from CatchMiss.hyps obtain w' where
    exec_c1': "Γ|⊨⟨c1,Normal s⟩ =n==> w'" and
    w_Stuck: "w = Stuck ⟶ w' = Stuck" and
    w_Fault: "∀f. w = Fault f ⟶ w' ∈ {Fault f, Stuck}" and
    w'_noStuck: "w' ≠ Stuck ⟶ w' = w"
    by auto
  have noAbr_w: "¬ isAbr w" by fact
  show ?case
  proof (cases w')
    case (Normal s')
    with w'_noStuck have "w'=w"
      by simp
    with exec_c1' Normal w_Stuck w_Fault w'_noStuck
    show ?thesis
      by (fastforce intro: execn.CatchMiss)
  next
    case (Abrupt s')
    with w'_noStuck have "w'=w"
      by simp
    with noAbr_w Abrupt show ?thesis by simp
  next
    case (Fault f)
    with w'_noStuck have "w'=w"
      by simp
    with exec_c1' Fault w_Stuck w_Fault w'_noStuck
    show ?thesis
      by (fastforce intro: execn.CatchMiss)
  next
    case Stuck
    with exec_c1' w_Stuck w_Fault w'_noStuck
    show ?thesis
      by (fastforce intro: execn.CatchMiss)
  qed
qed


lemma exec_to_exec_restrict:
  assumes exec: "Γ⊨⟨c,s⟩ ==> t"
  shows "∃t'. Γ|⊨⟨c,s⟩ ==> t' ∧ (t=Stuck ⟶ t'=Stuck) ∧
                (∀f. t=Fault f⟶ t'∈{Fault f,Stuck}) ∧ (t'≠Stuck ⟶ t'=t)"
proof -
  from exec obtain n where
    execn_strip: "Γ⊨⟨c,s⟩ =n==> t"
    by (auto simp add: exec_iff_execn)
  from execn_to_execn_restrict [where P=P,OF this]
  obtain t' where
    "Γ|⊨⟨c,s⟩ =n==> t'"
    "t=Stuck ⟶ t'=Stuck" "∀f. t=Fault f⟶ t'∈{Fault f,Stuck}" "t'≠Stuck ⟶ t'=t"
    by blast
  thus ?thesis
    by (blast intro: execn_to_exec)
qed

lemma notStuck_GuardD:
  "[Γ⊨⟨Guard m g c,Normal s⟩ ==>∉{Stuck}; s ∈ g] ==> Γ⊨⟨c,Normal s⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.Guard )

lemma notStuck_SeqD1:
  "[Γ⊨⟨Seq c1 c2,Normal s⟩ ==>∉{Stuck}] ==> Γ⊨⟨c1,Normal s⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.Seq )


lemma notStuck_SeqD2:
  "[Γ⊨⟨Seq c1 c2,Normal s⟩ ==>∉{Stuck}; Γ⊨⟨c1,Normal s⟩ ==>s'] ==> Γ⊨⟨c2,s'⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.Seq )

lemma notStuck_SeqD:
  "[Γ⊨⟨Seq c1 c2,Normal s⟩ ==>∉{Stuck}] ==>
     Γ⊨⟨c1,Normal s⟩ ==>∉{Stuck} ∧ (∀s'. Γ⊨⟨c1,Normal s⟩ ==>s' ⟶ Γ⊨⟨c2,s'⟩ ==>∉{Stuck})"
  by (auto simp add: final_notin_def dest: exec.Seq )

lemma notStuck_CondTrueD:
  "[Γ⊨⟨Cond b c1 c2,Normal s⟩ ==>∉{Stuck}; s ∈ b] ==> Γ⊨⟨c1,Normal s⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.CondTrue)

lemma notStuck_CondFalseD:
  "[Γ⊨⟨Cond b c1 c2,Normal s⟩ ==>∉{Stuck}; s ∉ b] ==> Γ⊨⟨c2,Normal s⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.CondFalse)

lemma notStuck_WhileTrueD1:
  "[Γ⊨⟨While b c,Normal s⟩ ==>∉{Stuck}; s ∈ b]
   ==> Γ⊨⟨c,Normal s⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.WhileTrue)

lemma notStuck_WhileTrueD2:
  "[Γ⊨⟨While b c,Normal s⟩ ==>∉{Stuck}; Γ⊨⟨c,Normal s⟩ ==>s'; s ∈ b]
   ==> Γ⊨⟨While b c,s'⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.WhileTrue)

lemma notStuck_CallD:
  "[Γ⊨⟨Call p ,Normal s⟩ ==>∉{Stuck}; Γ p = Some bdy]
   ==> Γ⊨⟨bdy,Normal s⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.Call)

lemma notStuck_CallDefinedD:
  "[Γ⊨⟨Call p,Normal s⟩ ==>∉{Stuck}]
   ==> Γ p ≠ None"
  by (cases "Γ p")
     (auto simp add: final_notin_def dest:  exec.CallUndefined)

lemma notStuck_DynComD:
  "[Γ⊨⟨DynCom c,Normal s⟩ ==>∉{Stuck}]
   ==> Γ⊨⟨(c s),Normal s⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.DynCom)

lemma notStuck_CatchD1:
  "[Γ⊨⟨Catch c1 c2,Normal s⟩ ==>∉{Stuck}] ==> Γ⊨⟨c1,Normal s⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.CatchMatch exec.CatchMiss )

lemma notStuck_CatchD2:
  "[Γ⊨⟨Catch c1 c2,Normal s⟩ ==>∉{Stuck}; Γ⊨⟨c1,Normal s⟩ ==>Abrupt s']
   ==> Γ⊨⟨c2,Normal s'⟩ ==>∉{Stuck}"
  by (auto simp add: final_notin_def dest: exec.CatchMatch)


(* ************************************************************************* *)
subsection "Miscellaneous"
(* ************************************************************************* *)

lemma execn_noguards_no_Fault:
 assumes execn: "Γ⊨⟨c,s⟩ =n==> t"
 assumes noguards_c: "noguards c"
 assumes noguards_Γ: "∀p ∈ dom Γ. noguards (the (Γ p))"
 assumes s_no_Fault: "¬ isFault s"
 shows "¬ isFault t"
  using execn noguards_c s_no_Fault
  proof (induct)
    case (Call p bdy n s t) with noguards_Γ show ?case
      apply -
      apply (drule bspec [where x=p])
      apply auto
      done
  qed (auto)

lemma exec_noguards_no_Fault:
 assumes exec: "Γ⊨⟨c,s⟩ ==> t"
 assumes noguards_c: "noguards c"
 assumes noguards_Γ: "∀p ∈ dom Γ. noguards (the (Γ p))"
 assumes s_no_Fault: "¬ isFault s"
 shows "¬ isFault t"
  using exec noguards_c s_no_Fault
  proof (induct)
    case (Call p bdy s t) with noguards_Γ show ?case
      apply -
      apply (drule bspec [where x=p])
      apply auto
      done
  qed auto

lemma execn_nothrows_no_Abrupt:
 assumes execn: "Γ⊨⟨c,s⟩ =n==> t"
 assumes nothrows_c: "nothrows c"
 assumes nothrows_Γ: "∀p ∈ dom Γ. nothrows (the (Γ p))"
 assumes s_no_Abrupt: "¬(isAbr s)"
 shows "¬(isAbr t)"
  using execn nothrows_c s_no_Abrupt
  proof (induct)
    case (Call p bdy n s t) with nothrows_Γ show ?case
      apply -
      apply (drule bspec [where x=p])
      apply auto
      done
  qed (auto)

lemma exec_nothrows_no_Abrupt:
 assumes exec: "Γ⊨⟨c,s⟩ ==> t"
 assumes nothrows_c: "nothrows c"
 assumes nothrows_Γ: "∀p ∈ dom Γ. nothrows (the (Γ p))"
 assumes s_no_Abrupt: "¬(isAbr s)"
 shows "¬(isAbr t)"
  using exec nothrows_c s_no_Abrupt
  proof (induct)
    case (Call p bdy s t) with nothrows_Γ show ?case
      apply -
      apply (drule bspec [where x=p])
      apply auto
      done
  qed (auto)

end