Theory Language
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 c⇩1 b c⇩2 = Catch c⇩1 (Cond b c⇩2 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 c⇩1 c⇩2) = flatten c⇩1 @ flatten c⇩2" |
"flatten (Cond b c⇩1 c⇩2) = [Cond b c⇩1 c⇩2]" |
"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⇩1 c⇩2) = [Catch c⇩1 c⇩2]"
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⇩1 c⇩2) = sequence Seq
((flatten (normalize c⇩1)) @ (flatten (normalize c⇩2)))" |
"normalize (Cond b c⇩1 c⇩2) = Cond b (normalize c⇩1) (normalize c⇩2)" |
"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⇩1 c⇩2) = Catch (normalize c⇩1) (normalize c⇩2)"
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 c⇩1 c⇩2) = (Seq (strip_guards F c⇩1) (strip_guards F c⇩2))" |
"strip_guards F (Cond b c⇩1 c⇩2) = Cond b (strip_guards F c⇩1) (strip_guards F c⇩2)" |
"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⇩1 c⇩2) = Catch (strip_guards F c⇩1) (strip_guards F c⇩2)"
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 c⇩1 c⇩2) = (Seq (mark_guards f c⇩1) (mark_guards f c⇩2))" |
"mark_guards f (Cond b c⇩1 c⇩2) = Cond b (mark_guards f c⇩1) (mark_guards f c⇩2)" |
"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⇩1 c⇩2) = Catch (mark_guards f c⇩1) (mark_guards f c⇩2)"
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 c⇩1 c⇩2) = (Seq (merge_guards c⇩1) (merge_guards c⇩2))" |
"merge_guards (Cond b c⇩1 c⇩2) = Cond b (merge_guards c⇩1) (merge_guards c⇩2)" |
"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) =
(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⇩1 c⇩2) = Catch (merge_guards c⇩1) (merge_guards c⇩2)"
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 c⇩1 c⇩2) = (noguards c⇩1 ∧ noguards c⇩2)" |
"noguards (Cond b c⇩1 c⇩2) = (noguards c⇩1 ∧ noguards c⇩2)" |
"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⇩1 c⇩2) = (noguards c⇩1 ∧ noguards c⇩2)"
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⇩1 c⇩2) = (nothrows c⇩1 ∧ nothrows c⇩2)" |
"nothrows (Cond b c⇩1 c⇩2) = (nothrows c⇩1 ∧ nothrows c⇩2)" |
"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⇩1 c⇩2) = (nothrows c⇩1 ∧ nothrows c⇩2)"
subsubsection ‹Intersecting Guards: ‹c⇩1 ∩⇩g c⇩2››
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⇩1 ⊆⇩g c⇩2››
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)
end
Theory Semantic
section ‹Big-Step Semantics for Simpl›
theory Semantic imports Language begin
notation
restrict_map ("_|⇘_⇙" [90, 91] 90)
datatype ('s,'f) xstate = Normal 's | Abrupt 's | Fault 'f | Stuck
definition isAbr::"('s,'f) xstate ⇒ bool"
where "isAbr S = (∃s. S=Abrupt s)"
lemma isAbr_simps [simp]:
"isAbr (Normal s) = False"
"isAbr (Abrupt s) = True"
"isAbr (Fault f) = False"
"isAbr Stuck = False"
by (auto simp add: isAbr_def)
lemma isAbrE [consumes 1, elim?]: "⟦isAbr S; ⋀s. S=Abrupt s ⟹ P⟧ ⟹ P"
by (auto simp add: isAbr_def)
lemma not_isAbrD:
"¬ isAbr s ⟹ (∃s'. s=Normal s') ∨ s = Stuck ∨ (∃f. s=Fault f)"
by (cases s) auto
definition isFault:: "('s,'f) xstate ⇒ bool"
where "isFault S = (∃f. S=Fault f)"
lemma isFault_simps [simp]:
"isFault (Normal s) = False"
"isFault (Abrupt s) = False"
"isFault (Fault f) = True"
"isFault Stuck = False"
by (auto simp add: isFault_def)
lemma isFaultE [consumes 1, elim?]: "⟦isFault s; ⋀f. s=Fault f ⟹ P⟧ ⟹ P"
by (auto simp add: isFault_def)
lemma not_isFault_iff: "(¬ isFault t) = (∀f. t ≠ Fault f)"
by (auto elim: isFaultE)
subsection ‹Big-Step Execution: ‹Γ⊢⟨c, s⟩ ⇒ t››
text ‹The procedure environment›
type_synonym ('s,'p,'f) body = "'p ⇒ ('s,'p,'f) com option"
inductive
"exec"::"[('s,'p,'f) body,('s,'p,'f) com,('s,'f) xstate,('s,'f) xstate]
⇒ bool" ("_⊢ ⟨_,_⟩ ⇒ _" [60,20,98,98] 89)
for Γ::"('s,'p,'f) body"
where
Skip: "Γ⊢⟨Skip,Normal s⟩ ⇒ Normal s"
| Guard: "⟦s∈g; Γ⊢⟨c,Normal s⟩ ⇒ t⟧
⟹
Γ⊢⟨Guard f g c,Normal s⟩ ⇒ t"
| GuardFault: "s∉g ⟹ Γ⊢⟨Guard f g c,Normal s⟩ ⇒ Fault f"
| FaultProp [intro,simp]: "Γ⊢⟨c,Fault f⟩ ⇒ Fault f"
| Basic: "Γ⊢⟨Basic f,Normal s⟩ ⇒ Normal (f s)"
| Spec: "(s,t) ∈ r
⟹
Γ⊢⟨Spec r,Normal s⟩ ⇒ Normal t"
| SpecStuck: "∀t. (s,t) ∉ r
⟹
Γ⊢⟨Spec r,Normal s⟩ ⇒ Stuck"
| Seq: "⟦Γ⊢⟨c⇩1,Normal s⟩ ⇒ s'; Γ⊢⟨c⇩2,s'⟩ ⇒ t⟧
⟹
Γ⊢⟨Seq c⇩1 c⇩2,Normal s⟩ ⇒ t"
| CondTrue: "⟦s ∈ b; Γ⊢⟨c⇩1,Normal s⟩ ⇒ t⟧
⟹
Γ⊢⟨Cond b c⇩1 c⇩2,Normal s⟩ ⇒ t"
| CondFalse: "⟦s ∉ b; Γ⊢⟨c⇩2,Normal s⟩ ⇒ t⟧
⟹
Γ⊢⟨Cond b c⇩1 c⇩2,Normal s⟩ ⇒ t"
| WhileTrue: "⟦s ∈ b; Γ⊢⟨c,Normal s⟩ ⇒ s'; Γ⊢⟨While b c,s'⟩ ⇒ t⟧
⟹
Γ⊢⟨While b c,Normal s⟩ ⇒ t"
| WhileFalse: "⟦s ∉ b⟧
⟹
Γ⊢⟨While b c,Normal s⟩ ⇒ Normal s"
| Call: "⟦Γ p=Some bdy;Γ⊢⟨bdy,Normal s⟩ ⇒ t⟧
⟹
Γ⊢⟨Call p,Normal s⟩ ⇒ t"
| CallUndefined: "⟦Γ p=None⟧
⟹
Γ⊢⟨Call p,Normal s⟩ ⇒ Stuck"
| StuckProp [intro,simp]: "Γ⊢⟨c,Stuck⟩ ⇒ Stuck"
| DynCom: "⟦Γ⊢⟨(c s),Normal s⟩ ⇒ t⟧
⟹
Γ⊢⟨DynCom c,Normal s⟩ ⇒ t"
| Throw: "Γ⊢⟨Throw,Normal s⟩ ⇒ Abrupt s"
| AbruptProp [intro,simp]: "Γ⊢⟨c,Abrupt s⟩ ⇒ Abrupt s"
| CatchMatch: "⟦Γ⊢⟨c⇩1,Normal s⟩ ⇒ Abrupt s'; Γ⊢⟨c⇩2,Normal s'⟩ ⇒ t⟧
⟹
Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒ t"
| CatchMiss: "⟦Γ⊢⟨c⇩1,Normal s⟩ ⇒ t; ¬isAbr t⟧
⟹
Γ⊢⟨Catch c⇩1 c⇩2,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: "⟦s∈g; Γ⊢⟨c,Normal s⟩ =n⇒ t⟧
⟹
Γ⊢⟨Guard f g c,Normal s⟩ =n⇒ t"
| GuardFault: "s∉g ⟹ Γ⊢⟨Guard f g c,Normal s⟩ =n⇒ Fault f"
| FaultProp [intro,simp]: "Γ⊢⟨c,Fault f⟩ =n⇒ Fault f"
| Basic: "Γ⊢⟨Basic f,Normal s⟩ =n⇒ Normal (f s)"
| Spec: "(s,t) ∈ r
⟹
Γ⊢⟨Spec r,Normal s⟩ =n⇒ Normal t"
| SpecStuck: "∀t. (s,t) ∉ r
⟹
Γ⊢⟨Spec r,Normal s⟩ =n⇒ Stuck"
| Seq: "⟦Γ⊢⟨c⇩1,Normal s⟩ =n⇒ s'; Γ⊢⟨c⇩2,s'⟩ =n⇒ t⟧
⟹
Γ⊢⟨Seq c⇩1 c⇩2,Normal s⟩ =n⇒ t"
| CondTrue: "⟦s ∈ b; Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t⟧
⟹
Γ⊢⟨Cond b c⇩1 c⇩2,Normal s⟩ =n⇒ t"
| CondFalse: "⟦s ∉ b; Γ⊢⟨c⇩2,Normal s⟩ =n⇒ t⟧
⟹
Γ⊢⟨Cond b c⇩1 c⇩2,Normal s⟩ =n⇒ t"
| WhileTrue: "⟦s ∈ b; Γ⊢⟨c,Normal s⟩ =n⇒ s';
Γ⊢⟨While b c,s'⟩ =n⇒ t⟧
⟹
Γ⊢⟨While b c,Normal s⟩ =n⇒ t"
| WhileFalse: "⟦s ∉ b⟧
⟹
Γ⊢⟨While b c,Normal s⟩ =n⇒ Normal s"
| Call: "⟦Γ p=Some bdy;Γ⊢⟨bdy,Normal s⟩ =n⇒ t⟧
⟹
Γ⊢⟨Call p ,Normal s⟩ =Suc n⇒ t"
| CallUndefined: "⟦Γ p=None⟧
⟹
Γ⊢⟨Call p ,Normal s⟩ =Suc n⇒ Stuck"
| StuckProp [intro,simp]: "Γ⊢⟨c,Stuck⟩ =n⇒ Stuck"
| DynCom: "⟦Γ⊢⟨(c s),Normal s⟩ =n⇒ t⟧
⟹
Γ⊢⟨DynCom c,Normal s⟩ =n⇒ t"
| Throw: "Γ⊢⟨Throw,Normal s⟩ =n⇒ Abrupt s"
| AbruptProp [intro,simp]: "Γ⊢⟨c,Abrupt s⟩ =n⇒ Abrupt s"
| CatchMatch: "⟦Γ⊢⟨c⇩1,Normal s⟩ =n⇒ Abrupt s'; Γ⊢⟨c⇩2,Normal s'⟩ =n⇒ t⟧
⟹
Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ =n⇒ t"
| CatchMiss: "⟦Γ⊢⟨c⇩1,Normal s⟩ =n⇒ t; ¬isAbr t⟧
⟹
Γ⊢⟨Catch c⇩1 c⇩2,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 ⟶ t∉T)"
definition final_notin:: "('s,'p,'f) body ⇒ ('s,'p,'f) com ⇒ ('s,'f) xstate
⇒ ('s,'f) xstate set ⇒ bool"
("_⊢ ⟨_,_⟩ ⇒∉_" [60,20,98,60] 89) where
"Γ⊢ ⟨c,s⟩ ⇒∉T = (∀t. Γ⊢ ⟨c,s⟩ ⇒t ⟶ t∉T)"
lemma final_notinI: "⟦⋀t. Γ⊢⟨c,s⟩ ⇒ t ⟹ t ∉ T⟧ ⟹ Γ⊢⟨c,s⟩ ⇒∉T"
by (simp add: final_notin_def)
lemma noFaultStuck_Call_body': "p ∈ dom Γ ⟹
Γ⊢⟨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: "t≠Fault f"
shows "s≠Fault f"
using execn t by (induct) auto
lemma noFault_start:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ t" and t: "t≠Fault f"
shows "s≠Fault f"
using exec t by (induct) auto
lemma noStuck_startn:
assumes execn: "Γ⊢⟨c,s⟩ =n⇒ t" and t: "t≠Stuck"
shows "s≠Stuck"
using execn t by (induct) auto
lemma noStuck_start:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ t" and t: "t≠Stuck"
shows "s≠Stuck"
using exec t by (induct) auto
lemma noAbrupt_startn:
assumes execn: "Γ⊢⟨c,s⟩ =n⇒ t" and t: "∀t'. t≠Abrupt t'"
shows "s≠Abrupt s'"
using execn t by (induct) auto
lemma noAbrupt_start:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ t" and t: "∀t'. t≠Abrupt t'"
shows "s≠Abrupt s'"
using exec t by (induct) auto
lemma noFaultn_startD: "Γ⊢⟨c,s⟩ =n⇒ Normal t ⟹ s ≠ Fault f"
by (auto dest: noFault_startn)
lemma noFaultn_startD': "t≠Fault f ⟹ Γ⊢⟨c,s⟩ =n⇒ t ⟹ s ≠ Fault f"
by (auto dest: noFault_startn)
lemma noFault_startD: "Γ⊢⟨c,s⟩ ⇒ Normal t ⟹ s ≠ Fault f"
by (auto dest: noFault_start)
lemma noFault_startD': "t≠Fault f⟹ Γ⊢⟨c,s⟩ ⇒ t ⟹ s ≠ Fault f"
by (auto dest: noFault_start)
lemma noStuckn_startD: "Γ⊢⟨c,s⟩ =n⇒ Normal t ⟹ s ≠ Stuck"
by (auto dest: noStuck_startn)
lemma noStuckn_startD': "t≠Stuck ⟹ Γ⊢⟨c,s⟩ =n⇒ t ⟹ s ≠ Stuck"
by (auto dest: noStuck_startn)
lemma noStuck_startD: "Γ⊢⟨c,s⟩ ⇒ Normal t ⟹ s ≠ Stuck"
by (auto dest: noStuck_start)
lemma noStuck_startD': "t≠Stuck ⟹ Γ⊢⟨c,s⟩ ⇒ t ⟹ s ≠ Stuck"
by (auto dest: noStuck_start)
lemma noAbruptn_startD: "Γ⊢⟨c,s⟩ =n⇒ Normal t ⟹ s ≠ Abrupt s'"
by (auto dest: noAbrupt_startn)
lemma noAbrupt_startD: "Γ⊢⟨c,s⟩ ⇒ Normal t ⟹ s ≠ Abrupt s'"
by (auto dest: noAbrupt_start)
lemma noFaultnI: "⟦⋀t. Γ⊢⟨c,s⟩ =n⇒t ⟹ t≠Fault f⟧ ⟹ Γ⊢⟨c,s⟩ =n⇒∉{Fault f}"
by (simp add: nfinal_notin_def)
lemma noFaultnI':
assumes contr: "Γ⊢⟨c,s⟩ =n⇒ Fault f ⟹ False"
shows "Γ⊢⟨c,s⟩ =n⇒∉{Fault f}"
proof (rule noFaultnI)
fix t assume "Γ⊢⟨c,s⟩ =n⇒ t"
with contr show "t ≠ Fault f"
by (cases "t=Fault f") auto
qed
lemma noFaultn_def': "Γ⊢⟨c,s⟩ =n⇒∉{Fault f} = (¬Γ⊢⟨c,s⟩ =n⇒ Fault f)"
apply rule
apply (fastforce simp add: nfinal_notin_def)
apply (fastforce intro: noFaultnI')
done
lemma noStucknI: "⟦⋀t. Γ⊢⟨c,s⟩ =n⇒t ⟹ t≠Stuck⟧ ⟹ Γ⊢⟨c,s⟩ =n⇒∉{Stuck}"
by (simp add: nfinal_notin_def)
lemma noStucknI':
assumes contr: "Γ⊢⟨c,s⟩ =n⇒ Stuck ⟹ False"
shows "Γ⊢⟨c,s⟩ =n⇒∉{Stuck}"
proof (rule noStucknI)
fix t assume "Γ⊢⟨c,s⟩ =n⇒ t"
with contr show "t ≠ Stuck"
by (cases t) auto
qed
lemma noStuckn_def': "Γ⊢⟨c,s⟩ =n⇒∉{Stuck} = (¬Γ⊢⟨c,s⟩ =n⇒ Stuck)"
apply rule
apply (fastforce simp add: nfinal_notin_def)
apply (fastforce intro: noStucknI')
done
lemma noFaultI: "⟦⋀t. Γ⊢⟨c,s⟩ ⇒t ⟹ t≠Fault f⟧ ⟹ Γ⊢⟨c,s⟩ ⇒∉{Fault f}"
by (simp add: final_notin_def)
lemma noFaultI':
assumes contr: "Γ⊢⟨c,s⟩ ⇒ Fault f⟹ False"
shows "Γ⊢⟨c,s⟩ ⇒∉{Fault f}"
proof (rule noFaultI)
fix t assume "Γ⊢⟨c,s⟩ ⇒ t"
with contr show "t ≠ Fault f"
by (cases "t=Fault f") auto
qed
lemma noFaultE:
"⟦Γ⊢⟨c,s⟩ ⇒∉{Fault f}; Γ⊢⟨c,s⟩ ⇒ Fault f⟧ ⟹ P"
by (auto simp add: final_notin_def)
lemma noFault_def': "Γ⊢⟨c,s⟩ ⇒∉{Fault f} = (¬Γ⊢⟨c,s⟩ ⇒ Fault f)"
apply rule
apply (fastforce simp add: final_notin_def)
apply (fastforce intro: noFaultI')
done
lemma noStuckI: "⟦⋀t. Γ⊢⟨c,s⟩ ⇒t ⟹ t≠Stuck⟧ ⟹ Γ⊢⟨c,s⟩ ⇒∉{Stuck}"
by (simp add: final_notin_def)
lemma noStuckI':
assumes contr: "Γ⊢⟨c,s⟩ ⇒ Stuck ⟹ False"
shows "Γ⊢⟨c,s⟩ ⇒∉{Stuck}"
proof (rule noStuckI)
fix t assume "Γ⊢⟨c,s⟩ ⇒ t"
with contr show "t ≠ Stuck"
by (cases t) auto
qed
lemma noStuckE:
"⟦Γ⊢⟨c,s⟩ ⇒∉{Stuck}; Γ⊢⟨c,s⟩ ⇒ Stuck⟧ ⟹ P"
by (auto simp add: final_notin_def)
lemma noStuck_def': "Γ⊢⟨c,s⟩ ⇒∉{Stuck} = (¬Γ⊢⟨c,s⟩ ⇒ Stuck)"
apply rule
apply (fastforce simp add: final_notin_def)
apply (fastforce intro: noStuckI')
done
lemma noFaultn_execD: "⟦Γ⊢⟨c,s⟩ =n⇒∉{Fault f}; Γ⊢⟨c,s⟩ =n⇒t⟧ ⟹ t≠Fault f"
by (simp add: nfinal_notin_def)
lemma noFault_execD: "⟦Γ⊢⟨c,s⟩ ⇒∉{Fault f}; Γ⊢⟨c,s⟩ ⇒t⟧ ⟹ t≠Fault f"
by (simp add: final_notin_def)
lemma noFaultn_exec_startD: "⟦Γ⊢⟨c,s⟩ =n⇒∉{Fault f}; Γ⊢⟨c,s⟩ =n⇒t⟧ ⟹ s≠Fault f"
by (auto simp add: nfinal_notin_def dest: noFaultn_startD)
lemma noFault_exec_startD: "⟦Γ⊢⟨c,s⟩ ⇒∉{Fault f}; Γ⊢⟨c,s⟩ ⇒t⟧ ⟹ s≠Fault f"
by (auto simp add: final_notin_def dest: noFault_startD)
lemma noStuckn_execD: "⟦Γ⊢⟨c,s⟩ =n⇒∉{Stuck}; Γ⊢⟨c,s⟩ =n⇒t⟧ ⟹ t≠Stuck"
by (simp add: nfinal_notin_def)
lemma noStuck_execD: "⟦Γ⊢⟨c,s⟩ ⇒∉{Stuck}; Γ⊢⟨c,s⟩ ⇒t⟧ ⟹ t≠Stuck"
by (simp add: final_notin_def)
lemma noStuckn_exec_startD: "⟦Γ⊢⟨c,s⟩ =n⇒∉{Stuck}; Γ⊢⟨c,s⟩ =n⇒t⟧ ⟹ s≠Stuck"
by (auto simp add: nfinal_notin_def dest: noStuckn_startD)
lemma noStuck_exec_startD: "⟦Γ⊢⟨c,s⟩ ⇒∉{Stuck}; Γ⊢⟨c,s⟩ ⇒t⟧ ⟹ s≠Stuck"
by (auto simp add: final_notin_def dest: noStuck_startD)
lemma noFaultStuckn_execD:
"⟦Γ⊢⟨c,s⟩ =n⇒∉{Fault True,Fault False,Stuck}; Γ⊢⟨c,s⟩ =n⇒t⟧ ⟹
t∉{Fault True,Fault False,Stuck}"
by (simp add: nfinal_notin_def)
lemma noFaultStuck_execD: "⟦Γ⊢⟨c,s⟩ ⇒∉{Fault True,Fault False,Stuck}; Γ⊢⟨c,s⟩ ⇒t⟧
⟹ t∉{Fault True,Fault False,Stuck}"
by (simp add: final_notin_def)
lemma noFaultStuckn_exec_startD:
"⟦Γ⊢⟨c,s⟩ =n⇒∉{Fault True, Fault False,Stuck}; Γ⊢⟨c,s⟩ =n⇒t⟧
⟹ s∉{Fault True,Fault False,Stuck}"
by (auto simp add: nfinal_notin_def )
lemma noFaultStuck_exec_startD:
"⟦Γ⊢⟨c,s⟩ ⇒∉{Fault True, Fault False,Stuck}; Γ⊢⟨c,s⟩ ⇒t⟧
⟹ s∉{Fault True,Fault False,Stuck}"
by (auto simp add: final_notin_def )
lemma noStuck_Call:
assumes noStuck: "Γ⊢⟨Call p,Normal s⟩ ⇒∉{Stuck}"
shows "p ∈ dom Γ"
proof (cases "p ∈ dom Γ")
case True thus ?thesis by simp
next
case False
hence "Γ p = None" by auto
hence "Γ⊢⟨Call p,Normal s⟩ ⇒Stuck"
by (rule exec.CallUndefined)
with noStuck show ?thesis
by (auto simp add: final_notin_def)
qed
lemma Guard_noFaultStuckD:
assumes "Γ⊢⟨Guard f g c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
assumes "f ∉ F"
shows "s ∈ g"
using assms
by (auto simp add: final_notin_def intro: exec.intros)
lemma final_notin_to_finaln:
assumes notin: "Γ⊢⟨c,s⟩ ⇒∉T"
shows "Γ⊢⟨c,s⟩ =n⇒∉T"
proof (clarsimp simp add: nfinal_notin_def)
fix t assume "Γ⊢⟨c,s⟩ =n⇒ t" and "t∈T"
with notin show "False"
by (auto intro: execn_to_exec simp add: final_notin_def)
qed
lemma noFault_Call_body:
"Γ p=Some bdy⟹
Γ⊢⟨Call p ,Normal s⟩ ⇒∉{Fault f} =
Γ⊢⟨the (Γ p),Normal s⟩ ⇒∉{Fault f}"
by (simp add: noFault_def' exec_Call_body)
lemma noStuck_Call_body:
"Γ p=Some bdy⟹
Γ⊢⟨Call p,Normal s⟩ ⇒∉{Stuck} =
Γ⊢⟨the (Γ p),Normal s⟩ ⇒∉{Stuck}"
by (simp add: noStuck_def' exec_Call_body)
lemma exec_final_notin_to_execn: "Γ⊢⟨c,s⟩ ⇒∉T ⟹ Γ⊢⟨c,s⟩ =n⇒∉T"
by (auto simp add: final_notin_def nfinal_notin_def dest: execn_to_exec)
lemma execn_final_notin_to_exec: "∀n. Γ⊢⟨c,s⟩ =n⇒∉T ⟹ Γ⊢⟨c,s⟩ ⇒∉T"
by (auto simp add: final_notin_def nfinal_notin_def dest: exec_to_execn)
lemma exec_final_notin_iff_execn: "Γ⊢⟨c,s⟩ ⇒∉T = (∀n. Γ⊢⟨c,s⟩ =n⇒∉T)"
by (auto intro: exec_final_notin_to_execn execn_final_notin_to_exec)
lemma Seq_NoFaultStuckD2:
assumes noabort: "Γ⊢⟨Seq c1 c2,s⟩ ⇒∉({Stuck} ∪ Fault ` F)"
shows "∀t. Γ⊢⟨c1,s⟩ ⇒ t ⟶ t∉ ({Stuck} ∪ Fault ` F) ⟶
Γ⊢⟨c2,t⟩ ⇒∉({Stuck} ∪ Fault ` F)"
using noabort
by (auto simp add: final_notin_def intro: exec_Seq') lemma Seq_NoFaultStuckD1:
assumes noabort: "Γ⊢⟨Seq c1 c2,s⟩ ⇒∉({Stuck} ∪ Fault ` F)"
shows "Γ⊢⟨c1,s⟩ ⇒∉({Stuck} ∪ Fault ` F)"
proof (rule final_notinI)
fix t
assume exec_c1: "Γ⊢⟨c1,s⟩ ⇒ t"
show "t ∉ {Stuck} ∪ Fault ` F"
proof
assume "t ∈ {Stuck} ∪ Fault ` F"
moreover
{
assume "t = Stuck"
with exec_c1
have "Γ⊢⟨Seq c1 c2,s⟩ ⇒ Stuck"
by (auto intro: exec_Seq')
with noabort have False
by (auto simp add: final_notin_def)
hence False ..
}
moreover
{
assume "t ∈ Fault ` F"
then obtain f where
t: "t=Fault f" and f: "f ∈ F"
by auto
from t exec_c1
have "Γ⊢⟨Seq c1 c2,s⟩ ⇒ Fault f"
by (auto intro: exec_Seq')
with noabort f have False
by (auto simp add: final_notin_def)
hence False ..
}
ultimately show False by auto
qed
qed
lemma Seq_NoFaultStuckD2':
assumes noabort: "Γ⊢⟨Seq c1 c2,s⟩ ⇒∉({Stuck} ∪ Fault ` F)"
shows "∀t. Γ⊢⟨c1,s⟩ ⇒ t ⟶ t∉ ({Stuck} ∪ Fault ` F) ⟶
Γ⊢⟨c2,t⟩ ⇒∉({Stuck} ∪ Fault ` F)"
using noabort
by (auto simp add: final_notin_def intro: exec_Seq')
subsection ‹Lemmas about @{const "sequence"}, @{const "flatten"} and
@{const "normalize"}›
lemma execn_sequence_app: "⋀s s' t.
⟦Γ⊢⟨sequence Seq xs,Normal s⟩ =n⇒ s'; Γ⊢⟨sequence Seq ys,s'⟩ =n⇒ t⟧
⟹ Γ⊢⟨sequence Seq (xs@ys),Normal s⟩ =n⇒ t"
proof (induct xs)
case Nil
thus ?case by (auto elim: execn_Normal_elim_cases)
next
case (Cons x xs)
have exec_x_xs: "Γ⊢⟨sequence Seq (x # xs),Normal s⟩ =n⇒ s'" by fact
have exec_ys: "Γ⊢⟨sequence Seq ys,s'⟩ =n⇒ t" by fact
show ?case
proof (cases xs)
case Nil
with exec_x_xs have "Γ⊢⟨x,Normal s⟩ =n⇒ s'"
by (auto elim: execn_Normal_elim_cases )
with Nil exec_ys show ?thesis
by (cases ys) (auto intro: execn.intros elim: execn_elim_cases)
next
case Cons
with exec_x_xs
obtain s'' where
exec_x: "Γ⊢⟨x,Normal s⟩ =n⇒ s''" and
exec_xs: "Γ⊢⟨sequence Seq xs,s''⟩ =n⇒ s'"
by (auto elim: execn_Normal_elim_cases )
show ?thesis
proof (cases s'')
case (Normal s''')
from Cons.hyps [OF exec_xs [simplified Normal] exec_ys]
have "Γ⊢⟨sequence Seq (xs @ ys),Normal s'''⟩ =n⇒ t" .
with Cons exec_x Normal
show ?thesis
by (auto intro: execn.intros)
next
case (Abrupt s''')
with exec_xs have "s'=Abrupt s'''"
by (auto dest: execn_Abrupt_end)
with exec_ys have "t=Abrupt s'''"
by (auto dest: execn_Abrupt_end)
with exec_x Abrupt Cons show ?thesis
by (auto intro: execn.intros)
next
case (Fault f)
with exec_xs have "s'=Fault f"
by (auto dest: execn_Fault_end)
with exec_ys have "t=Fault f"
by (auto dest: execn_Fault_end)
with exec_x Fault Cons show ?thesis
by (auto intro: execn.intros)
next
case Stuck
with exec_xs have "s'=Stuck"
by (auto dest: execn_Stuck_end)
with exec_ys have "t=Stuck"
by (auto dest: execn_Stuck_end)
with exec_x Stuck Cons show ?thesis
by (auto intro: execn.intros)
qed
qed
qed
lemma execn_sequence_appD: "⋀s t. Γ⊢⟨sequence Seq (xs @ ys),Normal s⟩ =n⇒ t ⟹
∃s'. Γ⊢⟨sequence Seq xs,Normal s⟩ =n⇒ s' ∧ Γ⊢⟨sequence Seq ys,s'⟩ =n⇒ t"
proof (induct xs)
case Nil
thus ?case
by (auto intro: execn.intros)
next
case (Cons x xs)
have exec_app: "Γ⊢⟨sequence Seq ((x # xs) @ ys),Normal s⟩ =n⇒ t" by fact
show ?case
proof (cases xs)
case Nil
with exec_app show ?thesis
by (cases ys) (auto elim: execn_Normal_elim_cases intro: execn_Skip')
next
case Cons
with exec_app obtain s' where
exec_x: "Γ⊢⟨x,Normal s⟩ =n⇒ s'" and
exec_xs_ys: "Γ⊢⟨sequence Seq (xs @ ys),s'⟩ =n⇒ t"
by (auto elim: execn_Normal_elim_cases)
show ?thesis
proof (cases s')
case (Normal s'')
from Cons.hyps [OF exec_xs_ys [simplified Normal]] Normal exec_x Cons
show ?thesis
by (auto intro: execn.intros)
next
case (Abrupt s'')
with exec_xs_ys have "t=Abrupt s''"
by (auto dest: execn_Abrupt_end)
with Abrupt exec_x Cons
show ?thesis
by (auto intro: execn.intros)
next
case (Fault f)
with exec_xs_ys have "t=Fault f"
by (auto dest: execn_Fault_end)
with Fault exec_x Cons
show ?thesis
by (auto intro: execn.intros)
next
case Stuck
with exec_xs_ys have "t=Stuck"
by (auto dest: execn_Stuck_end)
with Stuck exec_x Cons
show ?thesis
by (auto intro: execn.intros)
qed
qed
qed
lemma execn_sequence_appE [consumes 1]:
"⟦Γ⊢⟨sequence Seq (xs @ ys),Normal s⟩ =n⇒ t;
⋀s'. ⟦Γ⊢⟨sequence Seq xs,Normal s⟩ =n⇒ s';Γ⊢⟨sequence Seq ys,s'⟩ =n⇒ t⟧ ⟹ P
⟧ ⟹ P"
by (auto dest: execn_sequence_appD)
lemma execn_to_execn_sequence_flatten:
assumes exec: "Γ⊢⟨c,s⟩ =n⇒ t"
shows "Γ⊢⟨sequence Seq (flatten c),s⟩ =n⇒ t"
using exec
proof induct
case (Seq c1 c2 n s s' s'') thus ?case
by (auto intro: execn.intros execn_sequence_app)
qed (auto intro: execn.intros)
lemma execn_to_execn_normalize:
assumes exec: "Γ⊢⟨c,s⟩ =n⇒ t"
shows "Γ⊢⟨normalize c,s⟩ =n⇒ t"
using exec
proof induct
case (Seq c1 c2 n s s' s'') thus ?case
by (auto intro: execn_to_execn_sequence_flatten execn_sequence_app )
qed (auto intro: execn.intros)
lemma execn_sequence_flatten_to_execn:
shows "⋀s t. Γ⊢⟨sequence Seq (flatten c),s⟩ =n⇒ t ⟹ Γ⊢⟨c,s⟩ =n⇒ t"
proof (induct c)
case (Seq c1 c2)
have exec_seq: "Γ⊢⟨sequence Seq (flatten (Seq c1 c2)),s⟩ =n⇒ t" by fact
show ?case
proof (cases s)
case (Normal s')
with exec_seq obtain s'' where
"Γ⊢⟨sequence Seq (flatten c1),Normal s'⟩ =n⇒ s''" and
"Γ⊢⟨sequence Seq (flatten c2),s''⟩ =n⇒ t"
by (auto elim: execn_sequence_appE)
with Seq.hyps Normal
show ?thesis
by (fastforce intro: execn.intros)
next
case Abrupt
with exec_seq
show ?thesis by (auto intro: execn.intros dest: execn_Abrupt_end)
next
case Fault
with exec_seq
show ?thesis by (auto intro: execn.intros dest: execn_Fault_end)
next
case Stuck
with exec_seq
show ?thesis by (auto intro: execn.intros dest: execn_Stuck_end)
qed
qed auto
lemma execn_normalize_to_execn:
shows "⋀s t n. Γ⊢⟨normalize c,s⟩ =n⇒ t ⟹ Γ⊢⟨c,s⟩ =n⇒ t"
proof (induct c)
case Skip thus ?case by simp
next
case Basic thus ?case by simp
next
case Spec thus ?case by simp
next
case (Seq c1 c2)
have "Γ⊢⟨normalize (Seq c1 c2),s⟩ =n⇒ t" by fact
hence exec_norm_seq:
"Γ⊢⟨sequence Seq (flatten (normalize c1) @ flatten (normalize c2)),s⟩ =n⇒ t"
by simp
show ?case
proof (cases s)
case (Normal s')
with exec_norm_seq obtain s'' where
exec_norm_c1: "Γ⊢⟨sequence Seq (flatten (normalize c1)),Normal s'⟩ =n⇒ s''" and
exec_norm_c2: "Γ⊢⟨sequence Seq (flatten (normalize c2)),s''⟩ =n⇒ t"
by (auto elim: execn_sequence_appE)
from execn_sequence_flatten_to_execn [OF exec_norm_c1]
execn_sequence_flatten_to_execn [OF exec_norm_c2] Seq.hyps Normal
show ?thesis
by (fastforce intro: execn.intros)
next
case (Abrupt s')
with exec_norm_seq have "t=Abrupt s'"
by (auto dest: execn_Abrupt_end)
with Abrupt show ?thesis
by (auto intro: execn.intros)
next
case (Fault f)
with exec_norm_seq have "t=Fault f"
by (auto dest: execn_Fault_end)
with Fault show ?thesis
by (auto intro: execn.intros)
next
case Stuck
with exec_norm_seq have "t=Stuck"
by (auto dest: execn_Stuck_end)
with Stuck show ?thesis
by (auto intro: execn.intros)
qed
next
case Cond thus ?case
by (auto intro: execn.intros elim!: execn_elim_cases)
next
case (While b c)
have "Γ⊢⟨normalize (While b c),s⟩ =n⇒ t" by fact
hence exec_norm_w: "Γ⊢⟨While b (normalize c),s⟩ =n⇒ t"
by simp
{
fix s t w
assume exec_w: "Γ⊢⟨w,s⟩ =n⇒ t"
have "w=While b (normalize c) ⟹ Γ⊢⟨While b c,s⟩ =n⇒ t"
using exec_w
proof (induct)
case (WhileTrue s b' c' n w t)
from WhileTrue obtain
s_in_b: "s ∈ b" and
exec_c: "Γ⊢⟨normalize c,Normal s⟩ =n⇒ w" and
hyp_w: "Γ⊢⟨While b c,w⟩ =n⇒ t"
by simp
from While.hyps [OF exec_c]
have "Γ⊢⟨c,Normal s⟩ =n⇒ w"
by simp
with hyp_w s_in_b
have "Γ⊢⟨While b c,Normal s⟩ =n⇒ t"
by (auto intro: execn.intros)
with WhileTrue show ?case by simp
qed (auto intro: execn.intros)
}
from this [OF exec_norm_w]
show ?case
by simp
next
case Call thus ?case by simp
next
case DynCom thus ?case by (auto intro: execn.intros elim!: execn_elim_cases)
next
case Guard thus ?case by (auto intro: execn.intros elim!: execn_elim_cases)
next
case Throw thus ?case by simp
next
case Catch thus ?case by (fastforce intro: execn.intros elim!: execn_elim_cases)
qed
lemma execn_normalize_iff_execn:
"Γ⊢⟨normalize c,s⟩ =n⇒ t = Γ⊢⟨c,s⟩ =n⇒ t"
by (auto intro: execn_to_execn_normalize execn_normalize_to_execn)
lemma exec_sequence_app:
assumes exec_xs: "Γ⊢⟨sequence Seq xs,Normal s⟩ ⇒ s'"
assumes exec_ys: "Γ⊢⟨sequence Seq ys,s'⟩ ⇒ t"
shows "Γ⊢⟨sequence Seq (xs@ys),Normal s⟩ ⇒ t"
proof -
from exec_to_execn [OF exec_xs]
obtain n where
execn_xs: "Γ⊢⟨sequence Seq xs,Normal s⟩ =n⇒ s'"..
from exec_to_execn [OF exec_ys]
obtain m where
execn_ys: "Γ⊢⟨sequence Seq ys,s'⟩ =m⇒ t"..
with execn_xs obtain
"Γ⊢⟨sequence Seq xs,Normal s⟩ =max n m⇒ s'"
"Γ⊢⟨sequence Seq ys,s'⟩ =max n m⇒ t"
by (auto intro: execn_mono max.cobounded1 max.cobounded2)
from execn_sequence_app [OF this]
have "Γ⊢⟨sequence Seq (xs @ ys),Normal s⟩ =max n m⇒ t" .
thus ?thesis
by (rule execn_to_exec)
qed
lemma exec_sequence_appD:
assumes exec_xs_ys: "Γ⊢⟨sequence Seq (xs @ ys),Normal s⟩ ⇒ t"
shows "∃s'. Γ⊢⟨sequence Seq xs,Normal s⟩ ⇒ s' ∧ Γ⊢⟨sequence Seq ys,s'⟩ ⇒ t"
proof -
from exec_to_execn [OF exec_xs_ys]
obtain n where "Γ⊢⟨sequence Seq (xs @ ys),Normal s⟩ =n⇒ t"..
thus ?thesis
by (cases rule: execn_sequence_appE) (auto intro: execn_to_exec)
qed
lemma exec_sequence_appE [consumes 1]:
"⟦Γ⊢⟨sequence Seq (xs @ ys),Normal s⟩ ⇒ t;
⋀s'. ⟦Γ⊢⟨sequence Seq xs,Normal s⟩ ⇒ s';Γ⊢⟨sequence Seq ys,s'⟩ ⇒ t⟧ ⟹ P
⟧ ⟹ P"
by (auto dest: exec_sequence_appD)
lemma exec_to_exec_sequence_flatten:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ t"
shows "Γ⊢⟨sequence Seq (flatten c),s⟩ ⇒ t"
proof -
from exec_to_execn [OF exec]
obtain n where "Γ⊢⟨c,s⟩ =n⇒ t"..
from execn_to_execn_sequence_flatten [OF this]
show ?thesis
by (rule execn_to_exec)
qed
lemma exec_sequence_flatten_to_exec:
assumes exec_seq: "Γ⊢⟨sequence Seq (flatten c),s⟩ ⇒ t"
shows "Γ⊢⟨c,s⟩ ⇒ t"
proof -
from exec_to_execn [OF exec_seq]
obtain n where "Γ⊢⟨sequence Seq (flatten c),s⟩ =n⇒ t"..
from execn_sequence_flatten_to_execn [OF this]
show ?thesis
by (rule execn_to_exec)
qed
lemma exec_to_exec_normalize:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ t"
shows "Γ⊢⟨normalize c,s⟩ ⇒ t"
proof -
from exec_to_execn [OF exec] obtain n where "Γ⊢⟨c,s⟩ =n⇒ t"..
hence "Γ⊢⟨normalize c,s⟩ =n⇒ t"
by (rule execn_to_execn_normalize)
thus ?thesis
by (rule execn_to_exec)
qed
lemma exec_normalize_to_exec:
assumes exec: "Γ⊢⟨normalize c,s⟩ ⇒ t"
shows "Γ⊢⟨c,s⟩ ⇒ t"
proof -
from exec_to_execn [OF exec] obtain n where "Γ⊢⟨normalize c,s⟩ =n⇒ t"..
hence "Γ⊢⟨c,s⟩ =n⇒ t"
by (rule execn_normalize_to_execn)
thus ?thesis
by (rule execn_to_exec)
qed
lemma exec_normalize_iff_exec:
"Γ⊢⟨normalize c,s⟩ ⇒ t = Γ⊢⟨c,s⟩ ⇒ t"
by (auto intro: exec_to_exec_normalize exec_normalize_to_exec)
subsection ‹Lemmas about @{term "c⇩1 ⊆⇩g c⇩2"}›
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: "r∈b" by simp
from WhileTrue.hyps eqs
have exec_mark_c: "Γ⊢⟨mark_guards f c,Normal r⟩ =n⇒ u" by simp
from WhileTrue.hyps eqs
have exec_mark_w: "Γ⊢⟨While b (mark_guards f c),u⟩ =n⇒ w"
by simp
show ?case
proof -
from WhileTrue.hyps eqs have "Γ⊢⟨mark_guards f c,Normal r⟩ =n⇒ u"
by simp
with While.hyps
obtain u' where
exec_c: "Γ⊢⟨c,Normal r⟩ =n⇒ u'" and
u_Fault: "isFault u ⟶ isFault u'" and
u'_Fault_f: "u' = Fault f ⟶ u'=u" and
u'_Fault: "isFault u' ⟶ isFault u" and
u'_noFault: "¬ isFault u' ⟶ u'=u"
by blast
show ?thesis
proof (cases "isFault u'")
case False
with u'_noFault have u': "u'=u" by simp
from WhileTrue.hyps eqs obtain w' where
"Γ⊢⟨While b c,u⟩ =n⇒ w'"
"isFault w ⟶ isFault w'"
"w' = Fault f ⟶ w'=w"
"isFault w' ⟶ isFault w"
"¬ isFault w' ⟶ w' = w"
by blast
with u' exec_c r_in_b
show ?thesis
by (blast intro: execn.WhileTrue)
next
case True
then obtain f' where u': "u'=Fault f'"..
with exec_c r_in_b
have exec: "Γ⊢⟨While b c,Normal r⟩ =n⇒ Fault f'"
by (blast intro: execn.intros)
from True u'_Fault have "isFault u"
by simp
then obtain f where u: "u=Fault f"..
with exec_mark_w have "w=Fault f"
by (auto dest: execn_Fault_end)
with exec u' u u'_Fault_f
show ?thesis
by auto
qed
qed
next
case (WhileFalse r b' c'' n)
have eqs: "While b' c'' = While b (mark_guards f c)" by fact
from WhileFalse.hyps eqs
have r_not_in_b: "r∉b" by simp
show ?case
proof -
from r_not_in_b
have "Γ⊢⟨While b c,Normal r⟩ =n⇒ Normal r"
by (rule execn.WhileFalse)
thus ?thesis
by blast
qed
qed auto
} note hyp_while = this
show ?thesis
proof (cases "s'∈b")
case False
with Normal exec_mark
have "t=s"
by (auto elim: execn_Normal_elim_cases)
with Normal False show ?thesis
by (auto intro: execn.intros)
next
case True note s'_in_b = this
with Normal exec_mark obtain r where
exec_mark_c: "Γ⊢⟨mark_guards f c,Normal s'⟩ =n⇒ r" and
exec_mark_w: "Γ⊢⟨While b (mark_guards f c),r⟩ =n⇒ t"
by (auto elim: execn_Normal_elim_cases)
from While.hyps exec_mark_c obtain r' where
exec_c: "Γ⊢⟨c,Normal s'⟩ =n⇒ r'" and
r_Fault: "isFault r ⟶ isFault r'" and
r'_Fault_f: "r' = Fault f ⟶ r'=r" and
r'_Fault: "isFault r' ⟶ isFault r" and
r'_noFault: "¬ isFault r' ⟶ r'=r"
by blast
show ?thesis
proof (cases "isFault r'")
case False
with r'_noFault have r': "r'=r" by simp
from hyp_while exec_mark_w
obtain t' where
"Γ⊢⟨While b c,r⟩ =n⇒ t'"
"isFault t ⟶ isFault t'"
"t' = Fault f ⟶ t'=t"
"isFault t' ⟶ isFault t"
"¬ isFault t' ⟶ t'=t"
by blast
with r' exec_c Normal s'_in_b
show ?thesis
by (blast intro: execn.intros)
next
case True
then obtain f' where r': "r'=Fault f'"..
hence "Γ⊢⟨While b c,r'⟩ =n⇒ Fault f'"
by auto
with Normal s'_in_b exec_c
have exec: "Γ⊢⟨While b c,Normal s'⟩ =n⇒ Fault f'"
by (auto intro: execn.intros)
from True r'_Fault
have "isFault r"
by simp
then obtain f where r: "r=Fault f"..
with exec_mark_w have "t=Fault f"
by (auto dest: execn_Fault_end)
with Normal exec r' r r'_Fault_f
show ?thesis
by auto
qed
qed
qed
next
case Call thus ?case by auto
next
case DynCom thus ?case
by (fastforce elim!: execn_elim_cases intro: execn.intros)
next
case (Guard f' g c s n t)
have exec_mark: "Γ⊢⟨mark_guards f (Guard f' g c),s⟩ =n⇒ t" by fact
show ?case
proof (cases s)
case (Fault f)
with exec_mark have "t=Fault f"
by (auto dest: execn_Fault_end)
with Fault show ?thesis
by auto
next
case Stuck
with exec_mark have "t=Stuck"
by (auto dest: execn_Stuck_end)
with Stuck show ?thesis
by auto
next
case (Abrupt s')
with exec_mark have "t=Abrupt s'"
by (auto dest: execn_Abrupt_end)
with Abrupt show ?thesis
by auto
next
case (Normal s')
show ?thesis
proof (cases "s'∈g")
case False
with Normal exec_mark have t: "t=Fault f"
by (auto elim: execn_Normal_elim_cases)
from False
have "Γ⊢⟨Guard f' g c,Normal s'⟩ =n⇒ Fault f'"
by (blast intro: execn.intros)
with Normal t show ?thesis
by auto
next
case True
with exec_mark Normal
have "Γ⊢⟨mark_guards f c,Normal s'⟩ =n⇒ t"
by (auto elim: execn_Normal_elim_cases)
with Guard.hyps obtain t' where
"Γ⊢⟨c,Normal s'⟩ =n⇒ t'" and
"isFault t ⟶ isFault t'" and
"t' = Fault f ⟶ t'=t" and
"isFault t' ⟶ isFault t" and
"¬ isFault t' ⟶ t'=t"
by blast
with Normal True
show ?thesis
by (blast intro: execn.intros)
qed
qed
next
case Throw thus ?case by auto
next
case (Catch c1 c2 s n t)
have exec_mark: "Γ⊢⟨mark_guards f (Catch c1 c2),s⟩ =n⇒ t" by fact
show ?case
proof (cases "s")
case (Fault f)
with exec_mark have "t=Fault f"
by (auto dest: execn_Fault_end)
with Fault show ?thesis
by auto
next
case Stuck
with exec_mark have "t=Stuck"
by (auto dest: execn_Stuck_end)
with Stuck show ?thesis
by auto
next
case (Abrupt s')
with exec_mark have "t=Abrupt s'"
by (auto dest: execn_Abrupt_end)
with Abrupt show ?thesis
by auto
next
case (Normal s') note s=this
with exec_mark have
"Γ⊢⟨Catch (mark_guards f c1) (mark_guards f c2),Normal s'⟩ =n⇒ t" by simp
thus ?thesis
proof (cases)
fix w
assume exec_mark_c1: "Γ⊢⟨mark_guards f c1,Normal s'⟩ =n⇒ Abrupt w"
assume exec_mark_c2: "Γ⊢⟨mark_guards f c2,Normal w⟩ =n⇒ t"
from exec_mark_c1 Catch.hyps
obtain w' where
exec_c1: "Γ⊢⟨c1,Normal s'⟩ =n⇒ w'" and
w'_Fault_f: "w' = Fault f ⟶ w'=Abrupt w" and
w'_Fault: "isFault w' ⟶ isFault (Abrupt w)" and
w'_noFault: "¬ isFault w' ⟶ w'=Abrupt w"
by fastforce
show ?thesis
proof (cases "w'")
case (Fault f')
with Normal exec_c1 have "Γ⊢⟨Catch c1 c2,s⟩ =n⇒ Fault f'"
by (auto intro: execn.intros)
with w'_Fault Fault show ?thesis
by auto
next
case Stuck
with w'_noFault have False
by simp
thus ?thesis ..
next
case (Normal w'')
with w'_noFault have False by simp