Quelle  Language.thy

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

Copyright (C) 2004-2008 Norbert Schirmer
Copyright (c) 2022 Apple Inc. All rights reserved.
*)

section ‹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
  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 c₁ b c₂ = Catch c₁ (Cond b c₂ 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_exn:: "['s==>'s,('s,'p,'f) com,'s==>'s==>'s,'s==>'s==>'s,'s==>'s==>('s,'p,'f) com]==>('s,'p,'f) com"
where
  "block_exn init bdy return result_exn c =
    DynCom (λs. (Seq (Catch (Seq (Basic init) bdy) (Seq (Basic (λt. result_exn (return s t) t)) Throw))
                            (DynCom (λt. Seq (Basic (return s)) (c s t))))
                        )"

definition
  call_exn:: "('s==>'s) ==> 'p ==> ('s ==> 's ==> 's)==> ('s ==> 's ==> 's) ==>('s==>'s==>('s,'p,'f) com)==>('s,'p,'f)com" where
  "call_exn init p return result_exn c = block_exn init (Call p) return result_exn c"

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 maybe_guard:: "'f ==> 's set ==> ('s,'p,'f) com ==> ('s,'p,'f) com"
where
"maybe_guard f g c = (if g = UNIV then c else Guard f g c)"

lemma maybe_guard_UNIV [simp]: "maybe_guard f UNIV c = c"
  by (simp add: maybe_guard_def)


definition
  dynCall_exn:: "'f ==> 's set ==> ('s ==> 's) ==> ('s ==> 'p) ==>
             ('s ==> 's ==> 's) ==> ('s ==> 's ==> 's) ==> ('s ==> 's ==> ('s,'p,'f) com) ==> ('s,'p,'f) com" where
  "dynCall_exn f g init p return result_exn c =
    maybe_guard f g (DynCom (λs. call_exn init (p s) return result_exn c))"

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 = block_exn init bdy return (λs t. s) c"


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


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)


lemma call_call_exn: "call init p return result = call_exn init p return (λs t. s) result"
  by (simp add: call_def call_exn_def block_def)

lemma dynCall_dynCall_exn: "dynCall init p return result = dynCall_exn undefined UNIV init p return (λs t. s) result"
  by (simp add: dynCall_def dynCall_exn_def call_call_exn)


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 c₁ c₂) = flatten c₁ @ flatten c₂" |
"flatten (Cond b c₁ c₂) = [Cond b c₁ c₂]" |
"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 c₁ c₂) = [Catch c₁ c₂]"

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 c₁ c₂) = sequence Seq
                            ((flatten (normalize c₁)) @ (flatten (normalize c₂)))" |
"normalize (Cond b c₁ c₂) = Cond b (normalize c₁) (normalize c₂)" |
"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 c₁ c₂) = Catch (normalize c₁) (normalize c₂)"


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_exn [simp]:
  "flatten (block_exn init bdy return result_exn result) = [block_exn init bdy return result_exn result]"
  by (simp add: block_exn_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_call_exn [simp]: "flatten (call_exn init p return result_exn result) = [call_exn init p return result_exn result]"
  by (simp add: call_exn_def)

lemma flatten_dynCall_exn [simp]: "flatten (dynCall_exn f g init p return result_exn result) = [dynCall_exn f g init p return result_exn result]"
  by (simp add: dynCall_exn_def maybe_guard_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_exn [simp]: "normalize (block_exn init bdy return result_exn c) =
                         block_exn init (normalize bdy) return result_exn (λs t. normalize (c s t))"
  apply (simp add: block_exn_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_block [simp]: "normalize (block init bdy return c) =
                         block init (normalize bdy) return (λs t. normalize (c s t))"
  by (simp add: block_def)

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_call_exn [simp]:
  "normalize (call_exn init p return result_exn c) = call_exn init p return result_exn (λi t. normalize (c i t))"
  by (simp add: call_exn_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_guards [simp]:
  "normalize (guards gs c) = guards gs (normalize c)"
  by (induct gs) auto

lemma normalize_dynCall_exn [simp]:
  "normalize (dynCall_exn f g init p return result_exn c) =
    dynCall_exn f g init p return result_exn (λs t. normalize (c s t))"
  by  (simp add: dynCall_exn_def maybe_guard_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)


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 c₁ c₂) = (Seq (strip_guards F c₁) (strip_guards F c₂))" |
"strip_guards F (Cond b c₁ c₂) = Cond b (strip_guards F c₁) (strip_guards F c₂)" |
"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 c₁ c₂) = Catch (strip_guards F c₁) (strip_guards F c₂)"

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_exn [simp]:
  "strip_guards F (block_exn init bdy return result_exn c) =
    block_exn init (strip_guards F bdy) return result_exn (λs t. strip_guards F (c s t))"
  by (simp add: block_exn_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_call_exn [simp]:
  "strip_guards F (call_exn init p return result_exn c) =
     call_exn init p return result_exn (λs t. strip_guards F (c s t))"
  by (simp add: call_exn_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_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_dynCall_exn [simp]:
  "strip_guards F (dynCall_exn f g init p return result_exn c) =
     dynCall_exn f (if f ∈ F then UNIV else g) init p return result_exn (λs t. strip_guards F (c s t))"
  by (simp add: dynCall_exn_def maybe_guard_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_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 c₁ c₂) = (Seq (mark_guards f c₁) (mark_guards f c₂))" |
"mark_guards f (Cond b c₁ c₂) = Cond b (mark_guards f c₁) (mark_guards f c₂)" |
"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 c₁ c₂) = Catch (mark_guards f c₁) (mark_guards f c₂)"

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_exn [simp]:
  "mark_guards f (block_exn init bdy return result_exn c) =
    block_exn init (mark_guards f bdy) return result_exn (λs t. mark_guards f (c s t))"
  by (simp add: block_exn_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_call_exn [simp]:
  "mark_guards f (call_exn init p return result_exn c) =
     call_exn init p return result_exn (λs t. mark_guards f (c s t))"
  by (simp add: call_exn_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_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_dynCall_exn [simp]:
  "mark_guards f (dynCall_exn f' g init p return result_exn c) =
     dynCall_exn f g init p return result_exn (λs t. mark_guards f (c s t))"
  by (simp add: dynCall_exn_def maybe_guard_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_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 (guards (pg# pgs) c) = True"
 "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_exn init bdy return result_exn cont) = 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 (call_exn init p return result_exn cont) = False"
 "is_Guard (dynCall_exn f UNIV init P return result_exn 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 block_exn_def call_def dynCall_def call_exn_def dynCall_exn_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 c₁ c₂) = (Seq (merge_guards c₁) (merge_guards c₂))" |
"merge_guards (Cond b c₁ c₂) = Cond b (merge_guards c₁) (merge_guards c₂)" |
"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' \<Rightarrow> if f=f' then Guard f (g \<inter> g') c'
                        else Guard f g (Guard f' g' c')
     | _ \<Rightarrow>  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 c₁ c₂) = Catch (merge_guards c₁) (merge_guards c₂)"

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_guards_empty: "merge_guards (guards [] c) = merge_guards c"
  by (simp)

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_exn [simp]:
  "merge_guards (block_exn init bdy return result_exn c) =
    block_exn init (merge_guards bdy) return result_exn (λs t. merge_guards (c s t))"
  by (simp add: block_exn_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_call_exn [simp]:
  "merge_guards (call_exn init p return result_exn c) =
     call_exn init p return result_exn (λs t. merge_guards (c s t))"
  by (simp add: call_exn_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_block_exn merge_guards_call_exn
  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 c₁ c₂) = (noguards c₁ ∧ noguards c₂)" |
"noguards (Cond b c₁ c₂) = (noguards c₁ ∧ noguards c₂)" |
"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 c₁ c₂) = (noguards c₁ ∧ noguards c₂)"

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 c₁ c₂) = (nothrows c₁ ∧ nothrows c₂)" |
"nothrows (Cond b c₁ c₂) = (nothrows c₁ ∧ nothrows c₂)" |
"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 c₁ c₂) = (nothrows c₁ ∧ nothrows c₂)"

subsubsection ‹Intersecting Guards: ‹c₁ ∩_g c₂››

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: ‹c₁ ⊆_g c₂››

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\<dots> *)

end