Theory Semantic

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

| GuardFault: "sg  Γ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: "Γc1,Normal s   s'; Γc2,s'   t
        
        ΓSeq c1 c2,Normal s   t"

| CondTrue: "s  b; Γc1,Normal s   t
             
             ΓCond b c1 c2,Normal s   t"

| CondFalse: "s  b; Γc2,Normal s   t
              
              ΓCond b c1 c2,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: "Γc1,Normal s   Abrupt s'; Γc2,Normal s'   t
               
               ΓCatch c1 c2,Normal s   t"
| CatchMiss: "Γc1,Normal s   t; ¬isAbr t
               
               ΓCatch c1 c2,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: "sg; Γc,Normal s =n  t
          
          ΓGuard f g c,Normal s =n  t"

| GuardFault: "sg  Γ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: "Γc1,Normal s =n  s'; Γc2,s' =n  t
        
        ΓSeq c1 c2,Normal s =n  t"

| CondTrue: "s  b; Γc1,Normal s =n  t
             
             ΓCond b c1 c2,Normal s =n  t"

| CondFalse: "s  b; Γc2,Normal s =n  t
              
              ΓCond b c1 c2,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: "Γc1,Normal s =n  Abrupt s'; Γc2,Normal s' =n t
               
               ΓCatch c1 c2,Normal s =n t"
| CatchMiss: "Γc1,Normal s =n  t; ¬isAbr t
               
               ΓCatch c1 c2,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  tT)"

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  tT)"

lemma final_notinI: "t. Γc,s  t  t  T  Γc,s ⇒∉T"
  by (simp add: final_notin_def)

lemma noFaultStuck_Call_body': "p  dom Γ 
ΓCall p,Normal s ⇒∉({Stuck}  Fault ` (-F)) =
Γ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: "tFault f"
  shows "sFault f"
using execn t by (induct) auto

lemma noFault_start:
  assumes exec: "Γc,s  t" and t: "tFault f"
  shows "sFault f"
using exec t by (induct) auto

lemma noStuck_startn:
  assumes execn: "Γc,s =n t" and t: "tStuck"
  shows "sStuck"
using execn t by (induct) auto

lemma noStuck_start:
  assumes exec: "Γc,s  t" and t: "tStuck"
  shows "sStuck"
using exec t by (induct) auto

lemma noAbrupt_startn:
  assumes execn: "Γc,s =n t" and t: "t'. tAbrupt t'"
  shows "sAbrupt s'"
using execn t by (induct) auto

lemma noAbrupt_start:
  assumes exec: "Γc,s  t" and t: "t'. tAbrupt t'"
  shows "sAbrupt 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': "tFault 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': "tFault 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': "tStuck  Γ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': "tStuck  Γ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 =nt  tFault 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 =nt  tStuck   Γ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  tFault 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  tStuck   Γ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 =nt  tFault f"
  by (simp add: nfinal_notin_def)

lemma noFault_execD: "Γc,s ⇒∉{Fault f}; Γc,s t  tFault f"
  by (simp add: final_notin_def)

lemma noFaultn_exec_startD: "Γc,s =n⇒∉{Fault f}; Γc,s =nt  sFault f"
  by (auto simp add: nfinal_notin_def dest: noFaultn_startD)

lemma noFault_exec_startD: "Γc,s ⇒∉{Fault f}; Γc,s t  sFault f"
  by (auto simp add: final_notin_def dest: noFault_startD)

lemma noStuckn_execD: "Γc,s =n⇒∉{Stuck}; Γc,s =nt  tStuck"
  by (simp add: nfinal_notin_def)

lemma noStuck_execD: "Γc,s ⇒∉{Stuck}; Γc,s t  tStuck"
  by (simp add: final_notin_def)

lemma noStuckn_exec_startD: "Γc,s =n⇒∉{Stuck}; Γc,s =nt  sStuck"
  by (auto simp add: nfinal_notin_def dest: noStuckn_startD)

lemma noStuck_exec_startD: "Γc,s ⇒∉{Stuck}; Γc,s t  sStuck"
  by (auto simp add: final_notin_def dest: noStuck_startD)

lemma noFaultStuckn_execD:
  "Γc,s =n⇒∉{Fault True,Fault False,Stuck}; Γc,s =nt 
       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 =nt
    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 "tT"
  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 "c1 g c2"}
(* ************************************************************************ *)

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)
    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)
      fix w
      assume exec_c1: "Γc1,Normal s' =n Abrupt w"
      assume exec_c2: "Γc2,Normal w =n t"
      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
qed

lemma 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)"
proof -
  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)
qed


(* ************************************************************************* *)
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: "rb" 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: "rb" 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 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'  t' = t"
        by blast
      with Normal True
      show ?thesis
        by (blast intro: execn.intros)
    next
      case False
      with Normal exec_strip
      have "Γstrip_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'  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_strip: "Γstrip_guards F (While b 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')
    {
      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: "rb" 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: "rb" 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 "fF")
      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 =nt"
    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 =nt"
    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 =nt"
    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 =nt"
    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 =nFault 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 "c1 g c2"}
(* ************************************************************************* *)

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: "sb"
    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: "sb"
    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 add: 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 "sg1  sg2"
      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|⇘A) 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|⇘dom 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|⇘A) x = m x"
  by (auto simp add: restrict_map_def)


lemma exec_restrict_to_exec:
  assumes exec_restrict: "Γ|⇘Ac,s  t"
  assumes notStuck: "tStuck"
  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: "Γ|⇘Ac,s =n t"
  assumes notStuck: "tStuck"
  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|⇘A) 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'. Γ|⇘Pc,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) p = Some bdy"
      by (simp)
    with Call show ?thesis
      by (auto intro: execn.intros)
  next
    case False
    hence "(Γ|⇘P) 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) 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: "Γ|⇘Pc1,Normal s =n t'" and
    t'_notStuck: "t'  Stuck  t' = Abrupt s'" and
    exec_res_c2: "Γ|⇘Pc2,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 "Γ|⇘PCatch 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 "Γ|⇘PCatch 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': "Γ|⇘Pc1,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'. Γ|⇘Pc,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
    "Γ|⇘Pc,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