Session Simpl

Theory Language

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

(*  Title:      Language.thy
    Author:     Norbert Schirmer, TU Muenchen

Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹The Simpl Syntax›

theory Language imports "HOL-Library.Old_Recdef" begin

subsection ‹The Core Language›

text ‹We use a shallow embedding of boolean expressions as well as assertions
as sets of states.
›

type_synonym 's bexp = "'s set"
type_synonym 's assn = "'s set"

datatype (dead 's, 'p, 'f) com =
    Skip
  | Basic "'s  's"
  | Spec "('s × 's) set"
  | Seq "('s ,'p, 'f) com" "('s,'p, 'f) com"
  | Cond "'s bexp" "('s,'p,'f) com"  "('s,'p,'f) com"
  | While "'s bexp" "('s,'p,'f) com"
  | Call "'p"
  | DynCom "'s  ('s,'p,'f) com"
  | Guard "'f" "'s bexp" "('s,'p,'f) com"
  | Throw
  | Catch "('s,'p,'f) com" "('s,'p,'f) com"






subsection ‹Derived Language Constructs›

definition
  raise:: "('s  's)  ('s,'p,'f) com" where
  "raise f = Seq (Basic f) Throw"

definition
  condCatch:: "('s,'p,'f) com  's bexp  ('s,'p,'f) com  ('s,'p,'f) com" where
  "condCatch c1 b c2 = Catch c1 (Cond b c2 Throw)"

definition
  bind:: "('s  'v)  ('v  ('s,'p,'f) com)  ('s,'p,'f) com" where
  "bind e c = DynCom (λs. c (e s))"

definition
  bseq:: "('s,'p,'f) com  ('s,'p,'f) com  ('s,'p,'f) com" where
  "bseq = Seq"

definition
  block:: "['s's,('s,'p,'f) com,'s's's,'s's('s,'p,'f) com]('s,'p,'f) com"
where
  "block init bdy return c =
    DynCom (λs. (Seq (Catch (Seq (Basic init) bdy) (Seq (Basic (return s)) Throw))
                            (DynCom (λt. Seq (Basic (return s)) (c s t))))
                        )"

definition
  call:: "('s's)  'p  ('s  's  's)('s's('s,'p,'f) com)('s,'p,'f)com" where
  "call init p return c = block init (Call p) return c"

definition
  dynCall:: "('s  's)  ('s  'p) 
             ('s  's  's)  ('s  's  ('s,'p,'f) com)  ('s,'p,'f) com" where
  "dynCall init p return c = DynCom (λs. call init (p s) return c)"

definition
  fcall:: "('s's)  'p  ('s  's  's)('s  'v)  ('v('s,'p,'f) com)
            ('s,'p,'f)com" where
  "fcall init p return result c = call init p return (λs t. c (result t))"

definition
  lem:: "'x  ('s,'p,'f)com ('s,'p,'f)com" where
  "lem x c = c"

primrec switch:: "('s  'v)  ('v set × ('s,'p,'f) com) list  ('s,'p,'f) com"
where
"switch v [] = Skip" |
"switch v (Vc#vs) = Cond {s. v s  fst Vc} (snd Vc) (switch v vs)"

definition guaranteeStrip:: "'f  's set  ('s,'p,'f) com  ('s,'p,'f) com"
  where "guaranteeStrip f g c = Guard f g c"

definition guaranteeStripPair:: "'f  's set  ('f × 's set)"
  where "guaranteeStripPair f g = (f,g)"

primrec guards:: "('f × 's set ) list  ('s,'p,'f) com  ('s,'p,'f) com"
where
"guards [] c = c" |
"guards (g#gs) c = Guard (fst g) (snd g) (guards gs c)"

definition
  while::  "('f × 's set) list  's bexp  ('s,'p,'f) com  ('s, 'p, 'f) com"
where
  "while gs b c = guards gs (While b (Seq c (guards gs Skip)))"

definition
  whileAnno::
  "'s bexp  's assn  ('s × 's) assn  ('s,'p,'f) com  ('s,'p,'f) com" where
  "whileAnno b I V c = While b c"

definition
  whileAnnoG::
  "('f × 's set) list  's bexp  's assn  ('s × 's) assn 
     ('s,'p,'f) com  ('s,'p,'f) com" where
  "whileAnnoG gs b I V c = while gs b c"

definition
  specAnno::  "('a  's assn)  ('a  ('s,'p,'f) com) 
                         ('a  's assn)  ('a  's assn)  ('s,'p,'f) com"
  where "specAnno P c Q A = (c undefined)"

definition
  whileAnnoFix::
  "'s bexp  ('a  's assn)  ('a  ('s × 's) assn)  ('a  ('s,'p,'f) com) 
     ('s,'p,'f) com" where
  "whileAnnoFix b I V c = While b (c undefined)"

definition
  whileAnnoGFix::
  "('f × 's set) list  's bexp  ('a  's assn)  ('a  ('s × 's) assn) 
     ('a  ('s,'p,'f) com)  ('s,'p,'f) com" where
  "whileAnnoGFix gs b I V c = while gs b (c undefined)"

definition if_rel::"('s  bool)  ('s  's)  ('s  's)  ('s  's)  ('s × 's) set"
  where "if_rel b f g h = {(s,t). if b s then t = f s else t = g s  t = h s}"

lemma fst_guaranteeStripPair: "fst (guaranteeStripPair f g) = f"
  by (simp add: guaranteeStripPair_def)

lemma snd_guaranteeStripPair: "snd (guaranteeStripPair f g) = g"
  by (simp add: guaranteeStripPair_def)


subsection ‹Operations on Simpl-Syntax›


subsubsection ‹Normalisation of Sequential Composition: sequence›, flatten› and normalize›

primrec flatten:: "('s,'p,'f) com  ('s,'p,'f) com list"
where
"flatten Skip = [Skip]" |
"flatten (Basic f) = [Basic f]" |
"flatten (Spec r) = [Spec r]" |
"flatten (Seq c1 c2)  = flatten c1 @ flatten c2" |
"flatten (Cond b c1 c2) = [Cond b c1 c2]" |
"flatten (While b c) = [While b c]" |
"flatten (Call p) = [Call p]" |
"flatten (DynCom c) = [DynCom c]" |
"flatten (Guard f g c) = [Guard f g c]" |
"flatten Throw = [Throw]" |
"flatten (Catch c1 c2) = [Catch c1 c2]"

primrec sequence:: "(('s,'p,'f) com  ('s,'p,'f) com  ('s,'p,'f) com) 
                      ('s,'p,'f) com list  ('s,'p,'f) com"
where
"sequence seq [] = Skip" |
"sequence seq (c#cs) = (case cs of []  c
                        | _  seq c (sequence seq cs))"


primrec normalize:: "('s,'p,'f) com  ('s,'p,'f) com"
where
"normalize Skip = Skip" |
"normalize (Basic f) = Basic f" |
"normalize (Spec r) = Spec r" |
"normalize (Seq c1 c2)  = sequence Seq
                            ((flatten (normalize c1)) @ (flatten (normalize c2)))" |
"normalize (Cond b c1 c2) = Cond b (normalize c1) (normalize c2)" |
"normalize (While b c) = While b (normalize c)" |
"normalize (Call p) = Call p" |
"normalize (DynCom c) = DynCom (λs. (normalize (c s)))" |
"normalize (Guard f g c) = Guard f g (normalize c)" |
"normalize Throw = Throw" |
"normalize (Catch c1 c2) = Catch (normalize c1) (normalize c2)"


lemma flatten_nonEmpty: "flatten c  []"
  by (induct c) simp_all

lemma flatten_single: "c  set (flatten c'). flatten c = [c]"
apply (induct c')
apply           simp
apply          simp
apply         simp
apply        (simp (no_asm_use) )
apply        blast
apply       (simp (no_asm_use) )
apply      (simp (no_asm_use) )
apply     simp
apply    (simp (no_asm_use))
apply   (simp (no_asm_use))
apply  simp
apply (simp (no_asm_use))
done


lemma flatten_sequence_id:
  "cs[];c  set cs. flatten c = [c]  flatten (sequence Seq cs) = cs"
  apply (induct cs)
  apply  simp
  apply (case_tac cs)
  apply  simp
  apply auto
  done


lemma flatten_app:
  "flatten (sequence Seq (flatten c1 @ flatten c2)) = flatten c1 @ flatten c2"
  apply (rule flatten_sequence_id)
  apply (simp add: flatten_nonEmpty)
  apply (simp)
  apply (insert flatten_single)
  apply blast
  done



lemma flatten_sequence_flatten: "flatten (sequence Seq (flatten c)) = flatten c"
  apply (induct c)
  apply (auto simp add: flatten_app)
  done

lemma sequence_flatten_normalize: "sequence Seq (flatten (normalize c)) = normalize c"
apply (induct c)
apply (auto simp add:  flatten_app)
done


lemma flatten_normalize: "x xs. flatten (normalize c) = x#xs
        (case xs of []  normalize c = x
              | (x'#xs')  normalize c= Seq x (sequence Seq xs))"
proof (induct c)
  case (Seq c1 c2)
  have "flatten (normalize (Seq c1 c2)) = x # xs" by fact
  hence "flatten (sequence Seq (flatten (normalize c1) @ flatten (normalize c2))) =
          x#xs"
    by simp
  hence x_xs: "flatten (normalize c1) @ flatten (normalize c2) = x # xs"
    by (simp add: flatten_app)
  show ?case
  proof (cases "flatten (normalize c1)")
    case Nil
    with flatten_nonEmpty show ?thesis by auto
  next
    case (Cons x1 xs1)
    note Cons_x1_xs1 = this
    with x_xs obtain
      x_x1: "x=x1" and xs_rest: "xs=xs1@flatten (normalize c2)"
      by auto
    show ?thesis
    proof (cases xs1)
      case Nil
      from Seq.hyps (1) [OF Cons_x1_xs1] Nil
      have "normalize c1 = x1"
        by simp
      with Cons_x1_xs1 Nil x_x1 xs_rest show ?thesis
        apply (cases "flatten (normalize c2)")
        apply (fastforce simp add: flatten_nonEmpty)
        apply simp
        done
    next
      case Cons
      from Seq.hyps (1) [OF Cons_x1_xs1] Cons
      have "normalize c1 = Seq x1 (sequence Seq xs1)"
        by simp
      with Cons_x1_xs1 Nil x_x1 xs_rest show ?thesis
        apply (cases "flatten (normalize c2)")
        apply (fastforce simp add: flatten_nonEmpty)
        apply (simp split: list.splits)
        done
    qed
  qed
qed (auto)

lemma flatten_raise [simp]: "flatten (raise f) = [Basic f, Throw]"
  by (simp add: raise_def)

lemma flatten_condCatch [simp]: "flatten (condCatch c1 b c2) = [condCatch c1 b c2]"
  by (simp add: condCatch_def)

lemma flatten_bind [simp]: "flatten (bind e c) = [bind e c]"
  by (simp add: bind_def)

lemma flatten_bseq [simp]: "flatten (bseq c1 c2) = flatten c1 @ flatten c2"
  by (simp add: bseq_def)

lemma flatten_block [simp]:
  "flatten (block init bdy return result) = [block init bdy return result]"
  by (simp add: block_def)

lemma flatten_call [simp]: "flatten (call init p return result) = [call init p return result]"
  by (simp add: call_def)

lemma flatten_dynCall [simp]: "flatten (dynCall init p return result) = [dynCall init p return result]"
  by (simp add: dynCall_def)

lemma flatten_fcall [simp]: "flatten (fcall init p return result c) = [fcall init p return result c]"
  by (simp add: fcall_def)

lemma flatten_switch [simp]: "flatten (switch v Vcs) = [switch v Vcs]"
  by (cases Vcs) auto

lemma flatten_guaranteeStrip [simp]:
  "flatten (guaranteeStrip f g c) = [guaranteeStrip f g c]"
  by (simp add: guaranteeStrip_def)

lemma flatten_while [simp]: "flatten (while gs b c) = [while gs b c]"
  apply (simp add: while_def)
  apply (induct gs)
  apply  auto
  done

lemma flatten_whileAnno [simp]:
  "flatten (whileAnno b I V c) = [whileAnno b I V c]"
  by (simp add: whileAnno_def)

lemma flatten_whileAnnoG [simp]:
  "flatten (whileAnnoG gs b I V c) = [whileAnnoG gs b I V c]"
  by (simp add: whileAnnoG_def)

lemma flatten_specAnno [simp]:
  "flatten (specAnno P c Q A) = flatten (c undefined)"
  by (simp add: specAnno_def)

lemmas flatten_simps = flatten.simps flatten_raise flatten_condCatch flatten_bind
  flatten_block flatten_call flatten_dynCall flatten_fcall flatten_switch
  flatten_guaranteeStrip
  flatten_while flatten_whileAnno flatten_whileAnnoG flatten_specAnno

lemma normalize_raise [simp]:
 "normalize (raise f) = raise f"
  by (simp add: raise_def)

lemma normalize_condCatch [simp]:
 "normalize (condCatch c1 b c2) = condCatch (normalize c1) b (normalize c2)"
  by (simp add: condCatch_def)

lemma normalize_bind [simp]:
 "normalize (bind e c) = bind e (λv. normalize (c v))"
  by (simp add: bind_def)

lemma normalize_bseq [simp]:
 "normalize (bseq c1 c2) = sequence bseq
                            ((flatten (normalize c1)) @ (flatten (normalize c2)))"
  by (simp add: bseq_def)

lemma normalize_block [simp]: "normalize (block init bdy return c) =
                         block init (normalize bdy) return (λs t. normalize (c s t))"
  apply (simp add: block_def)
  apply (rule ext)
  apply (simp)
  apply (cases "flatten (normalize bdy)")
  apply  (simp add: flatten_nonEmpty)
  apply (rule conjI)
  apply  simp
  apply  (drule flatten_normalize)
  apply  (case_tac list)
  apply   simp
  apply  simp
  apply (rule ext)
  apply (case_tac "flatten (normalize (c s sa))")
  apply  (simp add: flatten_nonEmpty)
  apply  simp
  apply (thin_tac "flatten (normalize bdy) = P" for P)
  apply (drule flatten_normalize)
  apply (case_tac lista)
  apply  simp
  apply simp
  done

lemma normalize_call [simp]:
  "normalize (call init p return c) = call init p return (λi t. normalize (c i t))"
  by (simp add: call_def)

lemma normalize_dynCall [simp]:
  "normalize (dynCall init p return c) =
    dynCall init p return (λs t. normalize (c s t))"
  by (simp add: dynCall_def)

lemma normalize_fcall [simp]:
  "normalize (fcall init p return result c) =
    fcall init p return result (λv. normalize (c v))"
  by (simp add: fcall_def)

lemma normalize_switch [simp]:
  "normalize (switch v Vcs) = switch v (map (λ(V,c). (V,normalize c)) Vcs)"
apply (induct Vcs)
apply auto
done

lemma normalize_guaranteeStrip [simp]:
  "normalize (guaranteeStrip f g c) = guaranteeStrip f g (normalize c)"
  by (simp add: guaranteeStrip_def)

lemma normalize_guards [simp]:
  "normalize (guards gs c) = guards gs (normalize c)"
  by (induct gs) auto

text ‹Sequencial composition with guards in the body is not preserved by
        normalize›
lemma normalize_while [simp]:
  "normalize (while gs b c) = guards gs
      (While b (sequence Seq (flatten (normalize c) @ flatten (guards gs Skip))))"
  by (simp add: while_def)

lemma normalize_whileAnno [simp]:
  "normalize (whileAnno b I V c) = whileAnno b I V (normalize c)"
  by (simp add: whileAnno_def)

lemma normalize_whileAnnoG [simp]:
  "normalize (whileAnnoG gs b I V c) = guards gs
      (While b (sequence Seq (flatten (normalize c) @ flatten (guards gs Skip))))"
  by (simp add: whileAnnoG_def)

lemma normalize_specAnno [simp]:
  "normalize (specAnno P c Q A) = specAnno P (λs. normalize (c undefined)) Q A"
  by (simp add: specAnno_def)

lemmas normalize_simps =
  normalize.simps normalize_raise normalize_condCatch normalize_bind
  normalize_block normalize_call normalize_dynCall normalize_fcall normalize_switch
  normalize_guaranteeStrip normalize_guards
  normalize_while normalize_whileAnno normalize_whileAnnoG normalize_specAnno


subsubsection ‹Stripping Guards: strip_guards›

primrec strip_guards:: "'f set  ('s,'p,'f) com  ('s,'p,'f) com"
where
"strip_guards F Skip = Skip" |
"strip_guards F (Basic f) = Basic f" |
"strip_guards F (Spec r) = Spec r" |
"strip_guards F (Seq c1 c2)  = (Seq (strip_guards F c1) (strip_guards F c2))" |
"strip_guards F (Cond b c1 c2) = Cond b (strip_guards F c1) (strip_guards F c2)" |
"strip_guards F (While b c) = While b (strip_guards F c)" |
"strip_guards F (Call p) = Call p" |
"strip_guards F (DynCom c) = DynCom (λs. (strip_guards F (c s)))" |
"strip_guards F (Guard f g c) = (if f  F then strip_guards F c
                                  else Guard f g (strip_guards F c))" |
"strip_guards F Throw = Throw" |
"strip_guards F (Catch c1 c2) = Catch (strip_guards F c1) (strip_guards F c2)"

definition strip:: "'f set 
                   ('p  ('s,'p,'f) com option)  ('p  ('s,'p,'f) com option)"
  where "strip F Γ = (λp. map_option (strip_guards F) (Γ p))"


lemma strip_simp [simp]: "(strip F Γ) p = map_option (strip_guards F) (Γ p)"
  by (simp add: strip_def)

lemma dom_strip: "dom (strip F Γ) = dom Γ"
  by (auto)

lemma strip_guards_idem: "strip_guards F (strip_guards F c) = strip_guards F c"
  by (induct c) auto

lemma strip_idem: "strip F (strip F Γ) = strip F Γ"
  apply (rule ext)
  apply (case_tac "Γ x")
  apply (auto simp add: strip_guards_idem strip_def)
  done

lemma strip_guards_raise [simp]:
  "strip_guards F (raise f) = raise f"
  by (simp add: raise_def)

lemma strip_guards_condCatch [simp]:
  "strip_guards F (condCatch c1 b c2) =
    condCatch (strip_guards F c1) b (strip_guards F c2)"
  by (simp add: condCatch_def)

lemma strip_guards_bind [simp]:
  "strip_guards F (bind e c) = bind e (λv. strip_guards F (c v))"
  by (simp add: bind_def)

lemma strip_guards_bseq [simp]:
  "strip_guards F (bseq c1 c2) = bseq (strip_guards F c1) (strip_guards F c2)"
  by (simp add: bseq_def)

lemma strip_guards_block [simp]:
  "strip_guards F (block init bdy return c) =
    block init (strip_guards F bdy) return (λs t. strip_guards F (c s t))"
  by (simp add: block_def)

lemma strip_guards_call [simp]:
  "strip_guards F (call init p return c) =
     call init p return (λs t. strip_guards F (c s t))"
  by (simp add: call_def)

lemma strip_guards_dynCall [simp]:
  "strip_guards F (dynCall init p return c) =
     dynCall init p return (λs t. strip_guards F (c s t))"
  by (simp add: dynCall_def)

lemma strip_guards_fcall [simp]:
  "strip_guards F (fcall init p return result c) =
     fcall init p return result (λv. strip_guards F (c v))"
  by (simp add: fcall_def)

lemma strip_guards_switch [simp]:
  "strip_guards F (switch v Vc) =
    switch v (map (λ(V,c). (V,strip_guards F c)) Vc)"
  by (induct Vc) auto

lemma strip_guards_guaranteeStrip [simp]:
  "strip_guards F (guaranteeStrip f g c) =
    (if f  F then strip_guards F c
     else guaranteeStrip f g (strip_guards F c))"
  by (simp add: guaranteeStrip_def)

lemma guaranteeStripPair_split_conv [simp]: "case_prod c (guaranteeStripPair f g) = c f g"
  by (simp add: guaranteeStripPair_def)

lemma strip_guards_guards [simp]: "strip_guards F (guards gs c) =
        guards (filter (λ(f,g). f  F) gs) (strip_guards F c)"
  by (induct gs) auto

lemma strip_guards_while [simp]:
 "strip_guards F (while gs b  c) =
     while (filter (λ(f,g). f  F) gs) b (strip_guards F c)"
  by (simp add: while_def)

lemma strip_guards_whileAnno [simp]:
 "strip_guards F (whileAnno b I V c) = whileAnno b I V (strip_guards F c)"
  by (simp add: whileAnno_def  while_def)

lemma strip_guards_whileAnnoG [simp]:
 "strip_guards F (whileAnnoG gs b I V c) =
     whileAnnoG (filter (λ(f,g). f  F) gs) b I V (strip_guards F c)"
  by (simp add: whileAnnoG_def)

lemma strip_guards_specAnno [simp]:
  "strip_guards F (specAnno P c Q A) =
    specAnno P (λs. strip_guards F (c undefined)) Q A"
  by (simp add: specAnno_def)

lemmas strip_guards_simps = strip_guards.simps strip_guards_raise
  strip_guards_condCatch strip_guards_bind strip_guards_bseq strip_guards_block
  strip_guards_dynCall strip_guards_fcall strip_guards_switch
  strip_guards_guaranteeStrip guaranteeStripPair_split_conv strip_guards_guards
  strip_guards_while strip_guards_whileAnno strip_guards_whileAnnoG
  strip_guards_specAnno

subsubsection ‹Marking Guards: mark_guards›

primrec mark_guards:: "'f  ('s,'p,'g) com  ('s,'p,'f) com"
where
"mark_guards f Skip = Skip" |
"mark_guards f (Basic g) = Basic g" |
"mark_guards f (Spec r) = Spec r" |
"mark_guards f (Seq c1 c2)  = (Seq (mark_guards f c1) (mark_guards f c2))" |
"mark_guards f (Cond b c1 c2) = Cond b (mark_guards f c1) (mark_guards f c2)" |
"mark_guards f (While b c) = While b (mark_guards f c)" |
"mark_guards f (Call p) = Call p" |
"mark_guards f (DynCom c) = DynCom (λs. (mark_guards f (c s)))" |
"mark_guards f (Guard f' g c) = Guard f g (mark_guards f c)" |
"mark_guards f Throw = Throw" |
"mark_guards f (Catch c1 c2) = Catch (mark_guards f c1) (mark_guards f c2)"

lemma mark_guards_raise: "mark_guards f (raise g) = raise g"
  by (simp add: raise_def)

lemma mark_guards_condCatch [simp]:
  "mark_guards f (condCatch c1 b c2) =
    condCatch (mark_guards f c1) b (mark_guards f c2)"
  by (simp add: condCatch_def)

lemma mark_guards_bind [simp]:
  "mark_guards f (bind e c) = bind e (λv. mark_guards f (c v))"
  by (simp add: bind_def)

lemma mark_guards_bseq [simp]:
  "mark_guards f (bseq c1 c2) = bseq (mark_guards f c1) (mark_guards f c2)"
  by (simp add: bseq_def)

lemma mark_guards_block [simp]:
  "mark_guards f (block init bdy return c) =
    block init (mark_guards f bdy) return (λs t. mark_guards f (c s t))"
  by (simp add: block_def)

lemma mark_guards_call [simp]:
  "mark_guards f (call init p return c) =
     call init p return (λs t. mark_guards f (c s t))"
  by (simp add: call_def)

lemma mark_guards_dynCall [simp]:
  "mark_guards f (dynCall init p return c) =
     dynCall init p return (λs t. mark_guards f (c s t))"
  by (simp add: dynCall_def)

lemma mark_guards_fcall [simp]:
  "mark_guards f (fcall init p return result c) =
     fcall init p return result (λv. mark_guards f (c v))"
  by (simp add: fcall_def)

lemma mark_guards_switch [simp]:
  "mark_guards f (switch v vs) =
     switch v (map (λ(V,c). (V,mark_guards f c)) vs)"
  by (induct vs) auto

lemma mark_guards_guaranteeStrip [simp]:
  "mark_guards f (guaranteeStrip f' g c) = guaranteeStrip f g (mark_guards f c)"
  by (simp add: guaranteeStrip_def)

lemma mark_guards_guards [simp]:
  "mark_guards f (guards gs c) = guards (map (λ(f',g). (f,g)) gs) (mark_guards f c)"
  by (induct gs) auto

lemma mark_guards_while [simp]:
 "mark_guards f (while gs b c) =
    while (map (λ(f',g). (f,g)) gs) b (mark_guards f c)"
  by (simp add: while_def)

lemma mark_guards_whileAnno [simp]:
 "mark_guards f (whileAnno b I V c) = whileAnno b I V (mark_guards f c)"
  by (simp add: whileAnno_def while_def)

lemma mark_guards_whileAnnoG [simp]:
 "mark_guards f (whileAnnoG gs b I V c) =
    whileAnnoG (map (λ(f',g). (f,g)) gs) b I V (mark_guards f c)"
  by (simp add: whileAnno_def whileAnnoG_def while_def)

lemma mark_guards_specAnno [simp]:
  "mark_guards f (specAnno P c Q A) =
    specAnno P (λs. mark_guards f (c undefined)) Q A"
  by (simp add: specAnno_def)

lemmas mark_guards_simps = mark_guards.simps mark_guards_raise
  mark_guards_condCatch mark_guards_bind mark_guards_bseq mark_guards_block
  mark_guards_dynCall mark_guards_fcall mark_guards_switch
  mark_guards_guaranteeStrip guaranteeStripPair_split_conv mark_guards_guards
  mark_guards_while mark_guards_whileAnno mark_guards_whileAnnoG
  mark_guards_specAnno

definition is_Guard:: "('s,'p,'f) com  bool"
  where "is_Guard c = (case c of Guard f g c'  True | _  False)"
lemma is_Guard_basic_simps [simp]:
 "is_Guard Skip = False"
 "is_Guard (Basic f) = False"
 "is_Guard (Spec r) = False"
 "is_Guard (Seq c1 c2) = False"
 "is_Guard (Cond b c1 c2) = False"
 "is_Guard (While b c) = False"
 "is_Guard (Call p) = False"
 "is_Guard (DynCom C) = False"
 "is_Guard (Guard F g c) = True"
 "is_Guard (Throw) = False"
 "is_Guard (Catch c1 c2) = False"
 "is_Guard (raise f) = False"
 "is_Guard (condCatch c1 b c2) = False"
 "is_Guard (bind e cv) = False"
 "is_Guard (bseq c1 c2) = False"
 "is_Guard (block init bdy return cont) = False"
 "is_Guard (call init p return cont) = False"
 "is_Guard (dynCall init P return cont) = False"
 "is_Guard (fcall init p return result cont') = False"
 "is_Guard (whileAnno b I V c) = False"
 "is_Guard (guaranteeStrip F g c) = True"
  by (auto simp add: is_Guard_def raise_def condCatch_def bind_def bseq_def
          block_def call_def dynCall_def fcall_def whileAnno_def guaranteeStrip_def)


lemma is_Guard_switch [simp]:
 "is_Guard (switch v Vc) = False"
  by (induct Vc) auto

lemmas is_Guard_simps = is_Guard_basic_simps is_Guard_switch

primrec dest_Guard:: "('s,'p,'f) com  ('f × 's set × ('s,'p,'f) com)"
  where "dest_Guard (Guard f g c) = (f,g,c)"

lemma dest_Guard_guaranteeStrip [simp]: "dest_Guard (guaranteeStrip f g c) = (f,g,c)"
  by (simp add: guaranteeStrip_def)

lemmas dest_Guard_simps = dest_Guard.simps dest_Guard_guaranteeStrip

subsubsection ‹Merging Guards: merge_guards›

primrec merge_guards:: "('s,'p,'f) com  ('s,'p,'f) com"
where
"merge_guards Skip = Skip" |
"merge_guards (Basic g) = Basic g" |
"merge_guards (Spec r) = Spec r" |
"merge_guards (Seq c1 c2)  = (Seq (merge_guards c1) (merge_guards c2))" |
"merge_guards (Cond b c1 c2) = Cond b (merge_guards c1) (merge_guards c2)" |
"merge_guards (While b c) = While b (merge_guards c)" |
"merge_guards (Call p) = Call p" |
"merge_guards (DynCom c) = DynCom (λs. (merge_guards (c s)))" |
(*"merge_guards (Guard f g c) =
    (case (merge_guards c) of
      Guard f' g' c' ⇒ if f=f' then Guard f (g ∩ g') c'
                        else Guard f g (Guard f' g' c')
     | _ ⇒  Guard f g (merge_guards c))"*)
(* the following version works better with derived language constructs *)
"merge_guards (Guard f g c) =
    (let c' = (merge_guards c)
     in if is_Guard c'
        then let (f',g',c'') = dest_Guard c'
             in if f=f' then Guard f (g  g') c''
                        else Guard f g (Guard f' g' c'')
        else Guard f g c')" |
"merge_guards Throw = Throw" |
"merge_guards (Catch c1 c2) = Catch (merge_guards c1) (merge_guards c2)"

lemma merge_guards_res_Skip: "merge_guards c = Skip  c = Skip"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_Basic: "merge_guards c = Basic f  c = Basic f"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_Spec: "merge_guards c = Spec r  c = Spec r"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_Seq: "merge_guards c = Seq c1 c2 
    c1' c2'. c = Seq c1' c2'  merge_guards c1' = c1  merge_guards c2' = c2"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_Cond: "merge_guards c = Cond b c1 c2 
    c1' c2'. c = Cond b c1' c2'  merge_guards c1' = c1  merge_guards c2' = c2"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_While: "merge_guards c = While b c' 
    c''. c = While b c''   merge_guards c'' = c'"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_Call: "merge_guards c = Call p  c = Call p"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_DynCom: "merge_guards c = DynCom c' 
    c''. c = DynCom c''   (λs. (merge_guards (c'' s))) = c'"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_Throw: "merge_guards c = Throw  c = Throw"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_Catch: "merge_guards c = Catch c1 c2 
    c1' c2'. c = Catch c1' c2'  merge_guards c1' = c1  merge_guards c2' = c2"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemma merge_guards_res_Guard:
 "merge_guards c = Guard f g c'  c'' f' g'. c = Guard f' g' c''"
  by (cases c) (auto split: com.splits if_split_asm simp add: is_Guard_def Let_def)

lemmas merge_guards_res_simps = merge_guards_res_Skip merge_guards_res_Basic
 merge_guards_res_Spec merge_guards_res_Seq merge_guards_res_Cond
 merge_guards_res_While merge_guards_res_Call
 merge_guards_res_DynCom merge_guards_res_Throw merge_guards_res_Catch
 merge_guards_res_Guard

lemma merge_guards_raise: "merge_guards (raise g) = raise g"
  by (simp add: raise_def)

lemma merge_guards_condCatch [simp]:
  "merge_guards (condCatch c1 b c2) =
    condCatch (merge_guards c1) b (merge_guards c2)"
  by (simp add: condCatch_def)

lemma merge_guards_bind [simp]:
  "merge_guards (bind e c) = bind e (λv. merge_guards (c v))"
  by (simp add: bind_def)

lemma merge_guards_bseq [simp]:
  "merge_guards (bseq c1 c2) = bseq (merge_guards c1) (merge_guards c2)"
  by (simp add: bseq_def)

lemma merge_guards_block [simp]:
  "merge_guards (block init bdy return c) =
    block init (merge_guards bdy) return (λs t. merge_guards (c s t))"
  by (simp add: block_def)

lemma merge_guards_call [simp]:
  "merge_guards (call init p return c) =
     call init p return (λs t. merge_guards (c s t))"
  by (simp add: call_def)

lemma merge_guards_dynCall [simp]:
  "merge_guards (dynCall init p return c) =
     dynCall init p return (λs t. merge_guards (c s t))"
  by (simp add: dynCall_def)

lemma merge_guards_fcall [simp]:
  "merge_guards (fcall init p return result c) =
     fcall init p return result (λv. merge_guards (c v))"
  by (simp add: fcall_def)

lemma merge_guards_switch [simp]:
  "merge_guards (switch v vs) =
     switch v (map (λ(V,c). (V,merge_guards c)) vs)"
  by (induct vs) auto

lemma merge_guards_guaranteeStrip [simp]:
  "merge_guards (guaranteeStrip f g c) =
    (let c' = (merge_guards c)
     in if is_Guard c'
        then let (f',g',c') = dest_Guard c'
             in if f=f' then Guard f (g  g') c'
                        else Guard f g (Guard f' g' c')
        else Guard f g c')"
  by (simp add: guaranteeStrip_def)

lemma merge_guards_whileAnno [simp]:
 "merge_guards (whileAnno b I V c) = whileAnno b I V (merge_guards c)"
  by (simp add: whileAnno_def while_def)

lemma merge_guards_specAnno [simp]:
  "merge_guards (specAnno P c Q A) =
    specAnno P (λs. merge_guards (c undefined)) Q A"
  by (simp add: specAnno_def)

text @{term "merge_guards"} for guard-lists as in @{const guards}, @{const while}
 and @{const whileAnnoG} may have funny effects since the guard-list has to
 be merged with the body statement too.›

lemmas merge_guards_simps = merge_guards.simps merge_guards_raise
  merge_guards_condCatch merge_guards_bind merge_guards_bseq merge_guards_block
  merge_guards_dynCall merge_guards_fcall merge_guards_switch
  merge_guards_guaranteeStrip merge_guards_whileAnno merge_guards_specAnno

primrec noguards:: "('s,'p,'f) com  bool"
where
"noguards Skip = True" |
"noguards (Basic f) = True" |
"noguards (Spec r ) = True" |
"noguards (Seq c1 c2)  = (noguards c1  noguards c2)" |
"noguards (Cond b c1 c2) = (noguards c1  noguards c2)" |
"noguards (While b c) = (noguards c)" |
"noguards (Call p) = True" |
"noguards (DynCom c) = (s. noguards (c s))" |
"noguards (Guard f g c) = False" |
"noguards Throw = True" |
"noguards (Catch c1 c2) = (noguards c1  noguards c2)"

lemma noguards_strip_guards: "noguards (strip_guards UNIV c)"
  by (induct c) auto

primrec nothrows:: "('s,'p,'f) com  bool"
where
"nothrows Skip = True" |
"nothrows (Basic f) = True" |
"nothrows (Spec r) = True" |
"nothrows (Seq c1 c2)  = (nothrows c1  nothrows c2)" |
"nothrows (Cond b c1 c2) = (nothrows c1  nothrows c2)" |
"nothrows (While b c) = nothrows c" |
"nothrows (Call p) = True" |
"nothrows (DynCom c) = (s. nothrows (c s))" |
"nothrows (Guard f g c) = nothrows c" |
"nothrows Throw = False" |
"nothrows (Catch c1 c2) = (nothrows c1  nothrows c2)"

subsubsection ‹Intersecting Guards: c1g c2

inductive_set com_rel ::"(('s,'p,'f) com × ('s,'p,'f) com) set"
where
  "(c1, Seq c1 c2)  com_rel"
| "(c2, Seq c1 c2)  com_rel"
| "(c1, Cond b c1 c2)  com_rel"
| "(c2, Cond b c1 c2)  com_rel"
| "(c, While b c)  com_rel"
| "(c x, DynCom c)  com_rel"
| "(c, Guard f g c)  com_rel"
| "(c1, Catch c1 c2)  com_rel"
| "(c2, Catch c1 c2)  com_rel"

inductive_cases com_rel_elim_cases:
 "(c, Skip)  com_rel"
 "(c, Basic f)  com_rel"
 "(c, Spec r)  com_rel"
 "(c, Seq c1 c2)  com_rel"
 "(c, Cond b c1 c2)  com_rel"
 "(c, While b c1)  com_rel"
 "(c, Call p)  com_rel"
 "(c, DynCom c1)  com_rel"
 "(c, Guard f g c1)  com_rel"
 "(c, Throw)  com_rel"
 "(c, Catch c1 c2)  com_rel"

lemma wf_com_rel: "wf com_rel"
apply (rule wfUNIVI)
apply (induct_tac x)
apply           (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases)
apply          (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases)
apply         (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases)
apply        (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases,
               simp,simp)
apply       (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases,
              simp,simp)
apply      (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases,simp)
apply     (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases)
apply    (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases,simp)
apply   (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases,simp)
apply  (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases)
apply (erule allE, erule mp, (rule allI impI)+, erule com_rel_elim_cases,simp,simp)
done

consts inter_guards:: "('s,'p,'f) com × ('s,'p,'f) com  ('s,'p,'f) com option"

abbreviation
  inter_guards_syntax :: "('s,'p,'f) com  ('s,'p,'f) com  ('s,'p,'f) com option"
           ("_ g _" [20,20] 19)
  where "c g d == inter_guards (c,d)"

recdef inter_guards "inv_image com_rel fst"
  "(Skip g Skip) = Some Skip"
  "(Basic f1 g Basic f2) = (if f1 = f2 then Some (Basic f1) else None)"
  "(Spec r1 g Spec r2) = (if r1 = r2 then Some (Spec r1) else None)"
  "(Seq a1 a2 g Seq b1 b2) =
     (case a1 g b1 of
        None  None
      | Some c1  (case a2 g b2 of
          None  None
        | Some c2  Some (Seq c1 c2)))"
  "(Cond cnd1 t1 e1 g Cond cnd2 t2 e2) =
     (if cnd1 = cnd2
      then (case t1 g t2 of
            None  None
          | Some t  (case e1 g e2 of
              None  None
            | Some e  Some (Cond cnd1 t e)))
      else None)"
  "(While cnd1 c1 g While cnd2 c2) =
      (if cnd1 = cnd2
       then (case c1 g c2 of
           None  None
         | Some c  Some (While cnd1 c))
       else None)"
  "(Call p1 g Call p2) =
     (if p1 = p2
      then Some (Call p1)
      else None)"
  "(DynCom P1 g DynCom P2) =
     (if (s. (P1 s g P2 s)  None)
     then Some (DynCom (λs. the (P1 s g P2 s)))
     else None)"
  "(Guard m1 g1 c1 g Guard m2 g2 c2) =
     (if m1 = m2 then
       (case c1 g c2 of
          None  None
        | Some c  Some (Guard m1 (g1  g2) c))
      else None)"
  "(Throw g Throw) = Some Throw"
  "(Catch a1 a2 g Catch b1 b2) =
     (case a1 g b1 of
        None  None
      | Some c1  (case a2 g b2 of
          None  None
        | Some c2  Some (Catch c1 c2)))"
  "(c g d) = None"
(hints cong add: option.case_cong if_cong
       recdef_wf: wf_com_rel simp: com_rel.intros)

lemma inter_guards_strip_eq:
  "c. (c1 g c2) = Some c  
    (strip_guards UNIV c = strip_guards UNIV c1) 
    (strip_guards UNIV c = strip_guards UNIV c2)"
apply (induct c1 c2 rule: inter_guards.induct)
prefer 8
apply (simp split: if_split_asm)
apply hypsubst
apply simp
apply (rule ext)
apply (erule_tac x=s in allE, erule exE)
apply (erule_tac x=s in allE)
apply fastforce
apply (fastforce split: option.splits if_split_asm)+
done

lemma inter_guards_sym: "c. (c1 g c2) = Some c  (c2 g c1) = Some c"
apply (induct c1 c2 rule: inter_guards.induct)
apply (simp_all)
prefer 7
apply (simp split: if_split_asm add: not_None_eq)
apply (rule conjI)
apply  (clarsimp)
apply  (rule ext)
apply  (erule_tac x=s in allE)+
apply  fastforce
apply fastforce
apply (fastforce split: option.splits if_split_asm)+
done


lemma inter_guards_Skip: "(Skip g c2) = Some c = (c2=Skip  c=Skip)"
  by (cases c2) auto

lemma inter_guards_Basic:
  "((Basic f) g c2) = Some c = (c2=Basic f  c=Basic f)"
  by (cases c2) auto

lemma inter_guards_Spec:
  "((Spec r) g c2) = Some c = (c2=Spec r  c=Spec r)"
  by (cases c2) auto

lemma inter_guards_Seq:
  "(Seq a1 a2 g c2) = Some c =
     (b1 b2 d1 d2. c2=Seq b1 b2  (a1 g b1) = Some d1 
        (a2 g b2) = Some d2  c=Seq d1 d2)"
  by (cases c2) (auto split: option.splits)

lemma inter_guards_Cond:
  "(Cond cnd t1 e1 g c2) = Some c =
     (t2 e2 t e. c2=Cond cnd t2 e2  (t1 g t2) = Some t 
        (e1 g e2) = Some e  c=Cond cnd t e)"
  by (cases c2) (auto split: option.splits)

lemma inter_guards_While:
 "(While cnd bdy1 g c2) = Some c =
     (bdy2 bdy. c2 =While cnd bdy2  (bdy1 g bdy2) = Some bdy 
       c=While cnd bdy)"
  by (cases c2) (auto split: option.splits if_split_asm)

lemma inter_guards_Call:
  "(Call p g c2) = Some c =
     (c2=Call p  c=Call p)"
  by (cases c2) (auto split: if_split_asm)

lemma inter_guards_DynCom:
  "(DynCom f1 g c2) = Some c =
     (f2. c2=DynCom f2  (s. ((f1 s) g (f2 s))  None) 
      c=DynCom (λs. the ((f1 s) g (f2 s))))"
  by (cases c2) (auto split: if_split_asm)


lemma inter_guards_Guard:
  "(Guard f g1 bdy1 g c2) = Some c =
     (g2 bdy2 bdy. c2=Guard f g2 bdy2  (bdy1 g bdy2) = Some bdy 
       c=Guard f (g1  g2) bdy)"
  by (cases c2) (auto split: option.splits)

lemma inter_guards_Throw:
  "(Throw g c2) = Some c = (c2=Throw  c=Throw)"
  by (cases c2) auto

lemma inter_guards_Catch:
  "(Catch a1 a2 g c2) = Some c =
     (b1 b2 d1 d2. c2=Catch b1 b2  (a1 g b1) = Some d1 
        (a2 g b2) = Some d2  c=Catch d1 d2)"
  by (cases c2) (auto split: option.splits)


lemmas inter_guards_simps = inter_guards_Skip inter_guards_Basic inter_guards_Spec
  inter_guards_Seq inter_guards_Cond inter_guards_While inter_guards_Call
  inter_guards_DynCom inter_guards_Guard inter_guards_Throw
  inter_guards_Catch


subsubsection ‹Subset on Guards: c1g c2

inductive subseteq_guards :: "('s,'p,'f) com  ('s,'p,'f) com  bool"
  ("_ g _" [20,20] 19) where
  "Skip g Skip"
| "f1 = f2  Basic f1 g Basic f2"
| "r1 = r2  Spec r1 g Spec r2"
| "a1 g b1  a2 g b2  Seq a1 a2 g Seq b1 b2"
| "cnd1 = cnd2  t1 g t2  e1 g e2  Cond cnd1 t1 e1 g Cond cnd2 t2 e2"
| "cnd1 = cnd2  c1 g c2  While cnd1 c1 g While cnd2 c2"
| "p1 = p2  Call p1 g Call p2"
| "(s. P1 s g P2 s)  DynCom P1 g DynCom P2"
| "m1 = m2  g1 = g2  c1 g c2  Guard m1 g1 c1 g Guard m2 g2 c2"
| "c1 g c2  c1 g Guard m2 g2 c2"
| "Throw g Throw"
| "a1 g b1  a2 g b2  Catch a1 a2 g Catch b1 b2"

lemma subseteq_guards_Skip:
  "c = Skip" if "c g Skip"
  using that by cases

lemma subseteq_guards_Basic:
  "c = Basic f" if "c g Basic f"
  using that by cases simp

lemma subseteq_guards_Spec:
  "c = Spec r" if "c g Spec r"
  using that by cases simp

lemma subseteq_guards_Seq:
  "c1' c2'. c = Seq c1' c2'  (c1' g c1)  (c2' g c2)" if "c g Seq c1 c2"
  using that by cases simp

lemma subseteq_guards_Cond:
  "c1' c2'. c=Cond b c1' c2'  (c1' g c1)  (c2' g c2)" if "c g Cond b c1 c2"
  using that by cases simp

lemma subseteq_guards_While:
  "c''. c=While b c''  (c'' g c')" if "c g While b c'"
  using that by cases simp

lemma subseteq_guards_Call:
 "c = Call p" if "c g Call p"
  using that by cases simp

lemma subseteq_guards_DynCom:
  "C'. c=DynCom C'  (s. C' s g C s)" if "c g DynCom C"
  using that by cases simp

lemma subseteq_guards_Guard:
  "(c g c')  (c''. c = Guard f g c''  (c'' g c'))" if "c g Guard f g c'"
  using that by cases simp_all

lemma subseteq_guards_Throw:
  "c = Throw" if "c g Throw"
  using that by cases

lemma subseteq_guards_Catch:
  "c1' c2'. c = Catch c1' c2'  (c1' g c1)  (c2' g c2)" if "c g Catch c1 c2"
  using that by cases simp

lemmas subseteq_guardsD = subseteq_guards_Skip subseteq_guards_Basic
 subseteq_guards_Spec subseteq_guards_Seq subseteq_guards_Cond subseteq_guards_While
 subseteq_guards_Call subseteq_guards_DynCom subseteq_guards_Guard
 subseteq_guards_Throw subseteq_guards_Catch

lemma subseteq_guards_Guard':
  "f' b' c'. d = Guard f' b' c'" if "Guard f b c g d"
  using that by cases auto

lemma subseteq_guards_refl: "c g c"
  by (induct c) (auto intro: subseteq_guards.intros)

(* Antisymmetry and transitivity should hold as well… *)

end

Theory Semantic

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

(*  Title:      Semantic.thy
    Author:     Norbert Schirmer, TU Muenchen

Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

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:
  "Γbdy,Normal (init s)   Normal t; Γc s t,Normal (return s t)   u
  
  Γblock init bdy return c,Normal s   u"
apply (unfold block_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)"
apply (unfold block_def)
by (fastforce intro: exec.intros)

lemma exec_blockFault:
  "Γbdy,Normal (init s)   Fault f
   
  Γblock init bdy return c,Normal s   Fault f"
apply (unfold block_def)
by (fastforce intro: exec.intros)

lemma exec_blockStuck:
  "Γbdy,Normal (init s)   Stuck
  
  Γblock init bdy return c,Normal s   Stuck"
apply (unfold block_def)
by (fastforce intro: exec.intros)

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 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_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
 "Γ p = None; t = Stuck  P"
shows "P"
  using exec_block
apply (unfold block_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_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
  apply (unfold call_def)
  apply (cases "Γ p")
  apply  (erule exec_block_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_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_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_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_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:
  "Γ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"
apply (unfold block_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)"
apply (unfold block_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"
apply (unfold block_def)
by (fastforce intro: execn.intros)

lemma execn_blockStuck:
  "Γbdy,Normal (init s) =n  Stuck
  
  Γblock init bdy return c,Normal s =n  Stuck"
apply (unfold block_def)
by (fastforce intro: execn.intros)


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_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_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_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_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_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
apply (unfold block_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_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
  apply (unfold call_def)
  apply (cases n)
  apply  (simp only: block_def)
  apply  (fastforce elim: execn_Normal_elim_cases)
  apply (cases "Γ p")
  apply  (erule execn_block_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_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_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_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_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