Theory Language

(*
    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
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_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 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_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 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_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 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_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 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_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 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: ‹c1 ∩g 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: ‹c1 ⊆g 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