Theory AlternativeSmallStep
section ‹Alternative Small Step Semantics›
theory AlternativeSmallStep imports HoareTotalDef
begin
text ‹
This is the small-step semantics, which is described and used in my PhD-thesis \<^cite>‹"Schirmer-PhD"›.
It decomposes the statement into a list of statements and finally executes the head.
So the redex is always the head of the list. The equivalence between termination
(based on the big-step semantics) and the absence of infinite computations in
this small-step semantics follows the same lines of reasoning as for
the new small-step semantics. However, it is technically more involved since
the configurations are more complicated. Thats why I switched to the new small-step
semantics in the "main trunk". I keep this alternative version and the important
proofs in this theory, so that one can compare both approaches.
›
subsection ‹Small-Step Computation: ‹Γ⊢(cs, css, s) → (cs', css', s')››
type_synonym ('s,'p,'f) continuation = "('s,'p,'f) com list × ('s,'p,'f) com list"
type_synonym ('s,'p,'f) config =
"('s,'p,'f)com list × ('s,'p,'f)continuation list × ('s,'f) xstate"
inductive "step"::"[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] ⇒ bool"
(‹_⊢ (_ →/ _)› [81,81,81] 100)
for Γ::"('s,'p,'f) body"
where
Skip: "Γ⊢(Skip#cs,css,Normal s) → (cs,css,Normal s)"
| Guard: "s∈g ⟹ Γ⊢(Guard f g c#cs,css,Normal s) → (c#cs,css,Normal s)"
| GuardFault: "s∉g ⟹ Γ⊢(Guard f g c#cs,css,Normal s) → (cs,css,Fault f)"
| FaultProp: "Γ⊢(c#cs,css,Fault f) → (cs,css,Fault f)"
| FaultPropBlock: "Γ⊢([],(nrms,abrs)#css,Fault f) → (nrms,css,Fault f)"
| AbruptProp: "Γ⊢(c#cs,css,Abrupt s) → (cs,css,Abrupt s)"
| ExitBlockNormal:
"Γ⊢([],(nrms,abrs)#css,Normal s) → (nrms,css,Normal s)"
| ExitBlockAbrupt:
"Γ⊢([],(nrms,abrs)#css,Abrupt s) → (abrs,css,Normal s)"
| Basic: "Γ⊢(Basic f#cs,css,Normal s) → (cs,css,Normal (f s))"
| Spec: "(s,t) ∈ r ⟹ Γ⊢(Spec r#cs,css,Normal s) → (cs,css,Normal t)"
| SpecStuck: "∀t. (s,t) ∉ r ⟹ Γ⊢(Spec r#cs,css,Normal s) → (cs,css,Stuck)"
| Seq: "Γ⊢(Seq c⇩1 c⇩2#cs,css,Normal s) → (c⇩1#c⇩2#cs,css,Normal s)"
| CondTrue: "s∈b ⟹ Γ⊢(Cond b c⇩1 c⇩2#cs,css,Normal s) → (c⇩1#cs,css,Normal s)"
| CondFalse: "s∉b ⟹ Γ⊢(Cond b c⇩1 c⇩2#cs,css,Normal s) → (c⇩2#cs,css,Normal s)"
| WhileTrue: "⟦s∈b⟧
⟹
Γ⊢(While b c#cs,css,Normal s) → (c#While b c#cs,css,Normal s)"
| WhileFalse: "⟦s∉b⟧
⟹
Γ⊢(While b c#cs,css,Normal s) → (cs,css,Normal s)"
| Call: "Γ p=Some bdy ⟹
Γ⊢(Call p#cs,css,Normal s) → ([bdy],(cs,Throw#cs)#css,Normal s)"
| CallUndefined: "Γ p=None ⟹
Γ⊢(Call p#cs,css,Normal s) → (cs,css,Stuck)"
| StuckProp: "Γ⊢(c#cs,css,Stuck) → (cs,css,Stuck)"
| StuckPropBlock: "Γ⊢([],(nrms,abrs)#css,Stuck) → (nrms,css,Stuck)"
| DynCom: "Γ⊢(DynCom c#cs,css,Normal s) → (c s#cs,css,Normal s)"
| Throw: "Γ⊢(Throw#cs,css,Normal s) → (cs,css,Abrupt s)"
| Catch: "Γ⊢(Catch c⇩1 c⇩2#cs,css,Normal s) → ([c⇩1],(cs,c⇩2#cs)#css,Normal s)"
lemmas step_induct = step.induct [of _ "(c,css,s)" "(c',css',s')", split_format (complete),
case_names
Skip Guard GuardFault FaultProp FaultPropBlock AbruptProp ExitBlockNormal ExitBlockAbrupt
Basic Spec SpecStuck Seq CondTrue CondFalse WhileTrue WhileFalse Call CallUndefined
StuckProp StuckPropBlock DynCom Throw Catch, induct set]
inductive_cases step_elim_cases [cases set]:
"Γ⊢(c#cs,css,Fault f) → u"
"Γ⊢([],css,Fault f) → u"
"Γ⊢(c#cs,css,Stuck) → u"
"Γ⊢([],css,Stuck) → u"
"Γ⊢(c#cs,css,Abrupt s) → u"
"Γ⊢([],css,Abrupt s) → u"
"Γ⊢([],css,Normal s) → u"
"Γ⊢(Skip#cs,css,s) → u"
"Γ⊢(Guard f g c#cs,css,s) → u"
"Γ⊢(Basic f#cs,css,s) → u"
"Γ⊢(Spec r#cs,css,s) → u"
"Γ⊢(Seq c1 c2#cs,css,s) → u"
"Γ⊢(Cond b c1 c2#cs,css,s) → u"
"Γ⊢(While b c#cs,css,s) → u"
"Γ⊢(Call p#cs,css,s) → u"
"Γ⊢(DynCom c#cs,css,s) → u"
"Γ⊢(Throw#cs,css,s) → u"
"Γ⊢(Catch c1 c2#cs,css,s) → u"
inductive_cases step_Normal_elim_cases [cases set]:
"Γ⊢(c#cs,css,Fault f) → u"
"Γ⊢([],css,Fault f) → u"
"Γ⊢(c#cs,css,Stuck) → u"
"Γ⊢([],css,Stuck) → u"
"Γ⊢([],(nrms,abrs)#css,Normal s) → u"
"Γ⊢([],(nrms,abrs)#css,Abrupt s) → u"
"Γ⊢(Skip#cs,css,Normal s) → u"
"Γ⊢(Guard f g c#cs,css,Normal s) → u"
"Γ⊢(Basic f#cs,css,Normal s) → u"
"Γ⊢(Spec r#cs,css,Normal s) → u"
"Γ⊢(Seq c1 c2#cs,css,Normal s) → u"
"Γ⊢(Cond b c1 c2#cs,css,Normal s) → u"
"Γ⊢(While b c#cs,css,Normal s) → u"
"Γ⊢(Call p#cs,css,Normal s) → u"
"Γ⊢(DynCom c#cs,css,Normal s) → u"
"Γ⊢(Throw#cs,css,Normal s) → u"
"Γ⊢(Catch c1 c2#cs,css,Normal s) → u"
abbreviation
"step_rtrancl" :: "[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] ⇒ bool"
(‹_⊢ (_ →⇧*/ _)› [81,81,81] 100)
where
"Γ⊢cs0 →⇧* cs1 == (step Γ)⇧*⇧* cs0 cs1"
abbreviation
"step_trancl" :: "[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] ⇒ bool"
(‹_⊢ (_ →⇧+/ _)› [81,81,81] 100)
where
"Γ⊢cs0 →⇧+ cs1 == (step Γ)⇧+⇧+ cs0 cs1"
subsubsection ‹Structural Properties of Small Step Computations›
lemma Fault_app_steps: "Γ⊢(cs@xs,css,Fault f) →⇧* (xs,css,Fault f)"
proof (induct cs)
case Nil thus ?case by simp
next
case (Cons c cs)
have "Γ⊢(c#cs@xs, css, Fault f) →⇧* (xs, css, Fault f)"
proof -
have "Γ⊢(c#cs@xs, css, Fault f) → (cs@xs, css, Fault f)"
by (rule step.FaultProp)
also
have "Γ⊢(cs@xs, css, Fault f) →⇧* (xs, css, Fault f)"
by (rule Cons.hyps)
finally show ?thesis .
qed
thus ?case
by simp
qed
lemma Stuck_app_steps: "Γ⊢(cs@xs,css,Stuck) →⇧* (xs,css,Stuck)"
proof (induct cs)
case Nil thus ?case by simp
next
case (Cons c cs)
have "Γ⊢(c#cs@xs, css, Stuck) →⇧* (xs, css, Stuck)"
proof -
have "Γ⊢(c#cs@xs, css, Stuck) → (cs@xs, css, Stuck)"
by (rule step.StuckProp)
also
have "Γ⊢(cs@xs, css, Stuck) →⇧* (xs, css, Stuck)"
by (rule Cons.hyps)
finally show ?thesis .
qed
thus ?case
by simp
qed
text ‹We can only append commands inside a block, if execution does not
enter or exit a block.
›
lemma app_step:
assumes step: "Γ⊢(cs,css,s) → (cs',css',t)"
shows "css=css' ⟹ Γ⊢(cs@xs,css,s) → (cs'@xs,css',t)"
using step
apply induct
apply (simp_all del: fun_upd_apply,(blast intro: step.intros)+)
done
text ‹We can append whole blocks, without interfering with the actual
block. Outer blocks do not influence execution of
inner blocks.›
lemma app_css_step:
assumes step: "Γ⊢(cs,css,s) → (cs',css',t)"
shows "Γ⊢(cs,css@xs,s) → (cs',css'@xs,t)"
using step
apply induct
apply (simp_all del: fun_upd_apply,(blast intro: step.intros)+)
done
ML ‹
ML_Thms.bind_thm ("trancl_induct3", Split_Rule.split_rule @{context}
(Rule_Insts.read_instantiate @{context}
[((("a", 0), Position.none), "(ax, ay, az)"),
((("b", 0), Position.none), "(bx, by, bz)")] []
@{thm tranclp_induct}));
›
lemma app_css_steps:
assumes step: "Γ⊢(cs,css,s) →⇧+ (cs',css',t)"
shows "Γ⊢(cs,css@xs,s) →⇧+ (cs',css'@xs,t)"
apply(rule trancl_induct3 [OF step])
apply (rule app_css_step [THEN tranclp.r_into_trancl [of "step Γ"]],assumption)
apply(blast intro:app_css_step tranclp_trans)
done
lemma step_Cons':
assumes step: "Γ⊢(ccs,css,s) → (cs',css',t)"
shows
"⋀c cs. ccs=c#cs ⟹ ∃css''. css'=css''@css ∧
(if css''=[] then ∃p. cs'=p@cs
else (∃pnorm pabr. css''=[(pnorm@cs,pabr@cs)]))"
using step
by induct force+
lemma step_Cons:
assumes step: "Γ⊢(c#cs,css,s) → (cs',css',t)"
shows "∃pcss. css'=pcss@css ∧
(if pcss=[] then ∃ps. cs'=ps@cs
else (∃pcs_normal pcs_abrupt. pcss=[(pcs_normal@cs,pcs_abrupt@cs)]))"
using step_Cons' [OF step]
by blast
lemma step_Nil':
assumes step: "Γ⊢(cs,asscss,s) → (cs',css',t)"
shows
"⋀ass. ⟦cs=[]; asscss=ass@css; ass≠Nil⟧ ⟹
css'=tl ass@css ∧
(case s of
Abrupt s' ⇒ cs'=snd (hd ass) ∧ t=Normal s'
| _ ⇒ cs'=fst (hd ass) ∧ t=s)"
using step
by (induct) (fastforce simp add: neq_Nil_conv)+
lemma step_Nil:
assumes step: "Γ⊢([],ass@css,s) → (cs',css',t)"
assumes ass_not_Nil: "ass≠[]"
shows "css'=tl ass@css ∧
(case s of
Abrupt s' ⇒ cs'=snd (hd ass) ∧ t=Normal s'
| _ ⇒ cs'=fst (hd ass) ∧ t=s)"
using step_Nil' [OF step _ _ ass_not_Nil]
by simp
lemma step_Nil'':
assumes step: "Γ⊢([],(pcs_normal,pcs_abrupt)#pcss@css,s) → (cs',pcss@css,t)"
shows "(case s of
Abrupt s' ⇒ cs'=pcs_abrupt ∧ t=Normal s'
| _ ⇒ cs'=pcs_normal ∧ t=s)"
using step_Nil' [OF step, where ass ="(pcs_normal,pcs_abrupt)#pcss" and css="css"]
by (auto split: xstate.splits)
lemma drop_suffix_css_step':
assumes step: "Γ⊢(cs,cssxs,s) → (cs',css'xs,t)"
shows "⋀css css' xs. ⟦cssxs = css@xs; css'xs=css'@xs⟧
⟹ Γ⊢(cs,css,s) → (cs',css',t)"
using step
apply induct
apply (fastforce intro: step.intros)+
done
lemma drop_suffix_css_step:
assumes step: "Γ⊢(cs,pcss@css,s) → (cs',pcss'@css,t)"
shows "Γ⊢(cs,pcss,s) → (cs',pcss',t)"
using step by (blast intro: drop_suffix_css_step')
lemma drop_suffix_hd_css_step':
assumes step: "Γ⊢ (pcs,css,s) → (cs',css'css,t)"
shows "⋀p ps cs pnorm pabr. ⟦pcs=p#ps@cs; css'css=(pnorm@cs,pabr@cs)#css⟧
⟹ Γ⊢ (p#ps,css,s) → (cs',(pnorm,pabr)#css,t)"
using step
by induct (force intro: step.intros)+
lemma drop_suffix_hd_css_step'':
assumes step: "Γ⊢ (p#ps@cs,css,s) → (cs',(pnorm@cs,pabr@cs)#css,t)"
shows "Γ⊢ (p#ps,css,s) → (cs',(pnorm,pabr)#css,t)"
using drop_suffix_hd_css_step' [OF step]
by auto
lemma drop_suffix_hd_css_step:
assumes step: "Γ⊢ (p#ps@cs,css,s) → (cs',[(pnorm@ps@cs,pabr@ps@cs)]@css,t)"
shows "Γ⊢ (p#ps,css,s) → (cs',[(pnorm@ps,pabr@ps)]@css,t)"
proof -
from step drop_suffix_hd_css_step'' [of _ p ps cs css s cs' "pnorm@ps" "pabr@ps" t]
show ?thesis
by auto
qed
lemma drop_suffix':
assumes step: "Γ⊢(csxs,css,s) → (cs'xs,css',t)"
shows "⋀xs cs cs'. ⟦css=css'; csxs=cs@xs; cs'xs = cs'@xs; cs≠[] ⟧
⟹ Γ⊢(cs,css,s) → (cs',css,t)"
using step
apply induct
apply (fastforce intro: step.intros simp add: neq_Nil_conv)+
done
lemma drop_suffix:
assumes step: "Γ⊢(c#cs@xs,css,s) → (cs'@xs,css,t)"
shows "Γ⊢(c#cs,css,s) → (cs',css,t)"
by(rule drop_suffix' [OF step _ _ _]) auto
lemma drop_suffix_same_css_step:
assumes step: "Γ⊢(cs@xs,css,s) → (cs'@xs,css,t)"
assumes not_Nil: "cs≠[]"
shows "Γ⊢(cs,xss,s) → (cs',xss,t)"
proof-
from drop_suffix' [OF step _ _ _ not_Nil]
have "Γ⊢(cs,css,s) → (cs',css,t)"
by auto
with drop_suffix_css_step [of _ cs "[]" css s cs' "[]" t]
have "Γ⊢ (cs, [], s) → (cs', [], t)"
by auto
from app_css_step [OF this]
show ?thesis
by auto
qed
lemma Cons_change_css_step:
assumes step: "Γ⊢ (cs,css,s) → (cs',css'@css,t)"
shows "Γ⊢ (cs,xss,s) → (cs',css'@xss,t)"
proof -
from step
drop_suffix_css_step [where cs=cs and pcss="[]" and css=css and s=s
and cs'=cs' and pcss'=css' and t=t]
have "Γ⊢ (cs, [], s) → (cs', css', t)"
by auto
from app_css_step [where xs=xss, OF this]
show ?thesis
by auto
qed
lemma Nil_change_css_step:
assumes step: "Γ⊢([],ass@css,s) → (cs',ass'@css,t)"
assumes ass_not_Nil: "ass≠[]"
shows "Γ⊢([],ass@xss,s) → (cs',ass'@xss,t)"
proof -
from step drop_suffix_css_step [of _ "[]" ass css s cs' ass' t]
have "Γ⊢ ([], ass, s) → (cs', ass', t)"
by auto
from app_css_step [where xs=xss, OF this]
show ?thesis
by auto
qed
subsubsection ‹Equivalence between Big and Small-Step Semantics›
lemma exec_impl_steps:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ t"
shows "⋀cs css. Γ⊢(c#cs,css,s) →⇧* (cs,css,t)"
using exec
proof (induct)
case Skip thus ?case by (blast intro: step.Skip)
next
case Guard thus ?case by (blast intro: step.Guard rtranclp_trans)
next
case GuardFault thus ?case by (blast intro: step.GuardFault)
next
case FaultProp thus ?case by (blast intro: step.FaultProp)
next
case Basic thus ?case by (blast intro: step.Basic)
next
case Spec thus ?case by (blast intro: step.Spec)
next
case SpecStuck thus ?case by (blast intro: step.SpecStuck)
next
case Seq thus ?case by (blast intro: step.Seq rtranclp_trans)
next
case CondTrue thus ?case by (blast intro: step.CondTrue rtranclp_trans)
next
case CondFalse thus ?case by (blast intro: step.CondFalse rtranclp_trans)
next
case WhileTrue thus ?case by (blast intro: step.WhileTrue rtranclp_trans)
next
case WhileFalse thus ?case by (blast intro: step.WhileFalse)
next
case (Call p bdy s s' cs css)
have bdy: "Γ p = Some bdy" by fact
have steps_body: "Γ⊢([bdy],(cs,Throw#cs)#css,Normal s) →⇧*
([],(cs,Throw#cs)#css, s')" by fact
show ?case
proof (cases s')
case (Normal s'')
note steps_body
also from Normal have "Γ⊢([],(cs,Throw#cs)#css, s') → (cs,css,s')"
by (auto intro: step.intros)
finally show ?thesis
using bdy
by (blast intro: step.Call rtranclp_trans)
next
case (Abrupt s'')
with steps_body
have "Γ⊢([bdy],(cs,Throw#cs)#css,Normal s) →⇧*
([],(cs,Throw#cs)#css, Abrupt s'')" by simp
also have "Γ⊢([],(cs,Throw#cs)#css, Abrupt s'') → (Throw#cs,css,Normal s'')"
by (rule ExitBlockAbrupt)
also have "Γ⊢(Throw#cs,css,Normal s'') → (cs,css,Abrupt s'')"
by (rule Throw)
finally show ?thesis
using bdy Abrupt
by (auto intro: step.Call rtranclp_trans)
next
case Fault
note steps_body
also from Fault have "Γ⊢([],(cs,Throw#cs)#css, s') → (cs,css,s')"
by (auto intro: step.intros)
finally show ?thesis
using bdy
by (blast intro: step.Call rtranclp_trans)
next
case Stuck
note steps_body
also from Stuck have "Γ⊢([],(cs,Throw#cs)#css, s') → (cs,css,s')"
by (auto intro: step.intros)
finally show ?thesis
using bdy
by (blast intro: step.Call rtranclp_trans)
qed
next
case (CallUndefined p s cs css)
have undef: "Γ p = None" by fact
hence "Γ⊢(Call p # cs, css, Normal s) → (cs, css, Stuck)"
by (rule step.CallUndefined)
thus ?case ..
next
case StuckProp thus ?case by (blast intro: step.StuckProp rtrancl_trans)
next
case DynCom thus ?case by (blast intro: step.DynCom rtranclp_trans)
next
case Throw thus ?case by (blast intro: step.Throw)
next
case AbruptProp thus ?case by (blast intro: step.AbruptProp)
next
case (CatchMatch c⇩1 s s' c⇩2 s'' cs css)
have steps_c1: "Γ⊢([c⇩1],(cs,c⇩2#cs)#css,Normal s) →⇧*
([],(cs,c⇩2#cs)#css,Abrupt s')" by fact
also
have "Γ⊢([],(cs,c⇩2#cs)#css,Abrupt s') → (c⇩2#cs,css,Normal s')"
by (rule ExitBlockAbrupt)
also
have steps_c2: "Γ⊢(c⇩2#cs,css,Normal s') →⇧* (cs,css,s'')" by fact
finally
show "Γ⊢(Catch c⇩1 c⇩2 # cs, css, Normal s) →⇧* (cs, css, s'')"
by (blast intro: step.Catch rtranclp_trans)
next
case (CatchMiss c⇩1 s s' c⇩2 cs css)
assume notAbr: "¬ isAbr s'"
have steps_c1: "Γ⊢([c⇩1],(cs,c⇩2#cs)#css,Normal s) →⇧* ([],(cs,c⇩2#cs)#css,s')" by fact
show "Γ⊢(Catch c⇩1 c⇩2 # cs, css, Normal s) →⇧* (cs, css, s')"
proof (cases s')
case (Normal w)
with steps_c1
have "Γ⊢([c⇩1],(cs,c⇩2#cs)#css,Normal s) →⇧* ([],(cs,c⇩2#cs)#css,Normal w)"
by simp
also
have "Γ⊢([],(cs,c⇩2#cs)#css,Normal w) → (cs,css,Normal w)"
by (rule ExitBlockNormal)
finally show ?thesis using Normal
by (auto intro: step.Catch rtranclp_trans)
next
case Abrupt with notAbr show ?thesis by simp
next
case (Fault f)
with steps_c1
have "Γ⊢([c⇩1],(cs,c⇩2#cs)#css,Normal s) →⇧* ([],(cs,c⇩2#cs)#css,Fault f)"
by simp
also
have "Γ⊢([],(cs,c⇩2#cs)#css,Fault f) → (cs,css,Fault f)"
by (rule FaultPropBlock)
finally show ?thesis using Fault
by (auto intro: step.Catch rtranclp_trans)
next
case Stuck
with steps_c1
have "Γ⊢([c⇩1],(cs,c⇩2#cs)#css,Normal s) →⇧* ([],(cs,c⇩2#cs)#css,Stuck)"
by simp
also
have "Γ⊢([],(cs,c⇩2#cs)#css,Stuck) → (cs,css,Stuck)"
by (rule StuckPropBlock)
finally show ?thesis using Stuck
by (auto intro: step.Catch rtranclp_trans)
qed
qed
inductive "execs"::"[('s,'p,'f) body,('s,'p,'f) com list,
('s,'p,'f) continuation list,
('s,'f) xstate,('s,'f) xstate] ⇒ bool"
(‹_⊢ ⟨_,_,_⟩ ⇒ _› [50,50,50,50,50] 50)
for Γ:: "('s,'p,'f) body"
where
Nil: "Γ⊢⟨[],[],s⟩ ⇒ s"
| ExitBlockNormal: "Γ⊢⟨nrms,css,Normal s⟩ ⇒ t
⟹
Γ⊢⟨[],(nrms,abrs)#css,Normal s⟩ ⇒ t"
| ExitBlockAbrupt: "Γ⊢⟨abrs,css,Normal s⟩ ⇒ t
⟹
Γ⊢⟨[],(nrms,abrs)#css,Abrupt s⟩ ⇒ t"
| ExitBlockFault: "Γ⊢⟨nrms,css,Fault f⟩ ⇒ t
⟹
Γ⊢⟨[],(nrms,abrs)#css,Fault f⟩ ⇒ t"
| ExitBlockStuck: "Γ⊢⟨nrms,css,Stuck⟩ ⇒ t
⟹
Γ⊢⟨[],(nrms,abrs)#css,Stuck⟩ ⇒ t"
| Cons: "⟦Γ⊢⟨c,s⟩ ⇒ t; Γ⊢⟨cs,css,t⟩ ⇒ u⟧
⟹
Γ⊢⟨c#cs,css,s⟩ ⇒ u"
inductive_cases execs_elim_cases [cases set]:
"Γ⊢⟨[],css,s⟩ ⇒ t"
"Γ⊢⟨c#cs,css,s⟩ ⇒ t"
ML ‹
ML_Thms.bind_thm ("converse_rtrancl_induct3", Split_Rule.split_rule @{context}
(Rule_Insts.read_instantiate @{context}
[((("a", 0), Position.none), "(cs, css, s)"),
((("b", 0), Position.none), "(cs', css', t)")] []
@{thm converse_rtranclp_induct}));
›
lemma execs_Fault_end:
assumes execs: "Γ⊢⟨cs,css,s⟩ ⇒ t" shows "s=Fault f⟹ t=Fault f"
using execs
by (induct) (auto dest: Fault_end)
lemma execs_Stuck_end:
assumes execs: "Γ⊢⟨cs,css,s⟩ ⇒ t" shows "s=Stuck ⟹ t=Stuck"
using execs
by (induct) (auto dest: Stuck_end)
theorem steps_impl_execs:
assumes steps: "Γ⊢(cs,css,s) →⇧* ([],[],t)"
shows "Γ⊢⟨cs,css,s⟩ ⇒ t"
using steps
proof (induct rule: converse_rtrancl_induct3 [consumes 1])
show "Γ⊢⟨[],[],t⟩ ⇒ t" by (rule execs.Nil)
next
fix cs css s cs' css' w
assume step: "Γ⊢(cs,css, s) → (cs',css', w)"
assume execs: "Γ⊢⟨cs',css',w⟩ ⇒ t"
from step
show "Γ⊢⟨cs,css,s⟩ ⇒ t"
proof (cases)
case (Catch c1 c2 cs s)
with execs obtain t' where
exec_c1: "Γ⊢⟨c1,Normal s⟩ ⇒ t'" and
execs_rest: "Γ⊢⟨[],(cs, c2 # cs) # css,t'⟩ ⇒ t"
by (clarsimp elim!: execs_elim_cases)
have "Γ⊢⟨Catch c1 c2 # cs,css,Normal s⟩ ⇒ t"
proof (cases t')
case (Normal t'')
with exec_c1 have "Γ⊢⟨Catch c1 c2,Normal s⟩ ⇒ t'"
by (auto intro: exec.CatchMiss)
moreover
from execs_rest Normal have "Γ⊢⟨cs,css,t'⟩ ⇒ t"
by (cases) auto
ultimately show ?thesis
by (rule execs.Cons)
next
case (Abrupt t'')
from execs_rest Abrupt have "Γ⊢⟨c2#cs,css,Normal t''⟩ ⇒ t"
by (cases) auto
then obtain v where
exec_c2: "Γ⊢⟨c2,Normal t''⟩ ⇒ v" and
rest: "Γ⊢⟨cs,css,v⟩ ⇒ t"
by cases
from exec_c1 Abrupt exec_c2
have "Γ⊢⟨Catch c1 c2,Normal s⟩ ⇒ v"
by - (rule exec.CatchMatch, auto)
from this rest
show ?thesis
by (rule execs.Cons)
next
case (Fault f)
with exec_c1 have "Γ⊢⟨Catch c1 c2,Normal s⟩ ⇒ Fault f"
by (auto intro: exec.intros)
moreover from execs_rest Fault have "Γ⊢⟨cs,css,Fault f⟩ ⇒ t"
by (cases) auto
ultimately show ?thesis
by (rule execs.Cons)
next
case Stuck
with exec_c1 have "Γ⊢⟨Catch c1 c2,Normal s⟩ ⇒ Stuck"
by (auto intro: exec.intros)
moreover from execs_rest Stuck have "Γ⊢⟨cs,css,Stuck⟩ ⇒ t"
by (cases) auto
ultimately show ?thesis
by (rule execs.Cons)
qed
with Catch show ?thesis by simp
next
case (Call p bdy cs s)
have bdy: "Γ p = Some bdy" by fact
from Call execs obtain t' where
exec_body: "Γ⊢⟨bdy,Normal s⟩ ⇒ t'" and
execs_rest:
"Γ⊢⟨[],(cs,Throw#cs)#css ,t'⟩ ⇒ t"
by (clarsimp elim!: execs_elim_cases)
have "Γ⊢⟨Call p # cs,css,Normal s⟩ ⇒ t"
proof (cases t')
case (Normal t'')
with exec_body bdy
have "Γ⊢⟨Call p ,Normal s⟩ ⇒ Normal t''"
by (auto intro: exec.intros)
moreover
from execs_rest Normal
have "Γ⊢⟨cs,css ,Normal t''⟩ ⇒ t"
by cases auto
ultimately show ?thesis by (rule execs.Cons)
next
case (Abrupt t'')
with exec_body bdy
have "Γ⊢⟨Call p,Normal s⟩ ⇒ Abrupt t''"
by (auto intro: exec.intros)
moreover
from execs_rest Abrupt have
"Γ⊢⟨Throw # cs,css,Normal t''⟩ ⇒ t"
by (cases) auto
then obtain v where v: "Γ⊢⟨Throw,Normal t''⟩ ⇒ v" "Γ⊢⟨cs,css,v⟩ ⇒ t"
by (clarsimp elim!: execs_elim_cases)
moreover from v have "v=Abrupt t''"
by (auto elim: exec_Normal_elim_cases)
ultimately
show ?thesis by (auto intro: execs.Cons)
next
case (Fault f)
with exec_body bdy have "Γ⊢⟨Call p,Normal s⟩ ⇒ Fault f"
by (auto intro: exec.intros)
moreover from execs_rest Fault have "Γ⊢⟨cs,css,Fault f⟩ ⇒ t"
by (cases) (auto elim: execs_elim_cases dest: Fault_end)
ultimately
show ?thesis by (rule execs.Cons)
next
case Stuck
with exec_body bdy have "Γ⊢⟨Call p,Normal s⟩ ⇒ Stuck"
by (auto intro: exec.intros)
moreover from execs_rest Stuck have "Γ⊢⟨cs,css,Stuck⟩ ⇒ t"
by (cases) (auto elim: execs_elim_cases dest: Stuck_end)
ultimately
show ?thesis by (rule execs.Cons)
qed
with Call show ?thesis by simp
qed (insert execs,
(blast intro:execs.intros exec.intros elim!: execs_elim_cases)+)
qed
theorem steps_impl_exec:
assumes steps: "Γ⊢([c],[],s) →⇧* ([],[],t)"
shows "Γ⊢⟨c,s⟩ ⇒ t"
using steps_impl_execs [OF steps]
by (blast elim: execs_elim_cases)
corollary steps_eq_exec: "Γ⊢([c],[],s) →⇧* ([],[],t) = Γ⊢⟨c,s⟩ ⇒ t"
by (blast intro: steps_impl_exec exec_impl_steps)
subsection ‹Infinite Computations: ‹inf Γ cs css s››
definition inf ::
"[('s,'p,'f) body,('s,'p,'f) com list,('s,'p,'f) continuation list,('s,'f) xstate]
⇒ bool"
where "inf Γ cs css s = (∃f. f 0 = (cs,css,s) ∧ (∀i. Γ⊢f i → f(Suc i)))"
lemma not_infI: "⟦⋀f. ⟦f 0 = (cs,css,s); ⋀i. Γ⊢f i → f (Suc i)⟧ ⟹ False⟧
⟹ ¬inf Γ cs css s"
by (auto simp add: inf_def)
subsection ‹Equivalence of Termination and Absence of Infinite Computations›
inductive "terminatess":: "[('s,'p,'f) body,('s,'p,'f) com list,
('s,'p,'f) continuation list,('s,'f) xstate] ⇒ bool"
(‹_⊢_,_ ⇓ _› [60,20,60] 89)
for Γ::"('s,'p,'f) body"
where
Nil: "Γ⊢[],[]⇓s"
| ExitBlockNormal: "Γ⊢nrms,css⇓Normal s
⟹
Γ⊢[],(nrms,abrs)#css⇓Normal s"
| ExitBlockAbrupt: "Γ⊢abrs,css⇓Normal s
⟹
Γ⊢[],(nrms,abrs)#css⇓Abrupt s"
| ExitBlockFault: "Γ⊢nrms,css⇓Fault f
⟹
Γ⊢[],(nrms,abrs)#css⇓Fault f"
| ExitBlockStuck: "Γ⊢nrms,css⇓Stuck
⟹
Γ⊢[],(nrms,abrs)#css⇓Stuck"
| Cons: "⟦Γ⊢c↓s; (∀t. Γ⊢⟨c,s⟩ ⇒ t ⟶ Γ⊢cs,css⇓t)⟧
⟹
Γ⊢c#cs,css⇓s"
inductive_cases terminatess_elim_cases [cases set]:
"Γ⊢[],css⇓t"
"Γ⊢c#cs,css⇓t"
lemma terminatess_Fault: "⋀cs. Γ⊢cs,css⇓Fault f"
proof (induct css)
case Nil
show "Γ⊢cs,[]⇓Fault f"
proof (induct cs)
case Nil show "Γ⊢[],[]⇓Fault f" by (rule terminatess.Nil)
next
case (Cons c cs)
thus ?case
by (auto intro: terminatess.intros terminates.intros dest: Fault_end)
qed
next
case (Cons d css)
have hyp: "⋀cs. Γ⊢cs,css⇓Fault f" by fact
obtain nrms abrs where d: "d=(nrms,abrs)" by (cases d) auto
have "Γ⊢cs,(nrms,abrs)#css⇓Fault f"
proof (induct cs)
case Nil
show "Γ⊢[],(nrms, abrs) # css⇓Fault f"
by (rule terminatess.ExitBlockFault) (rule hyp)
next
case (Cons c cs)
have hyp1: "Γ⊢cs,(nrms, abrs) # css⇓Fault f" by fact
show "Γ⊢c#cs,(nrms, abrs)#css⇓Fault f"
by (auto intro: hyp1 terminatess.Cons terminates.intros dest: Fault_end)
qed
with d show ?case by simp
qed
lemma terminatess_Stuck: "⋀cs. Γ⊢cs,css⇓Stuck"
proof (induct css)
case Nil
show "Γ⊢cs,[]⇓Stuck"
proof (induct cs)
case Nil show "Γ⊢[],[]⇓Stuck" by (rule terminatess.Nil)
next
case (Cons c cs)
thus ?case
by (auto intro: terminatess.intros terminates.intros dest: Stuck_end)
qed
next
case (Cons d css)
have hyp: "⋀cs. Γ⊢cs,css⇓Stuck" by fact
obtain nrms abrs where d: "d=(nrms,abrs)" by (cases d) auto
have "Γ⊢cs,(nrms,abrs)#css⇓Stuck"
proof (induct cs)
case Nil
show "Γ⊢[],(nrms, abrs) # css⇓Stuck"
by (rule terminatess.ExitBlockStuck) (rule hyp)
next
case (Cons c cs)
have hyp1: "Γ⊢cs,(nrms, abrs) # css⇓Stuck" by fact
show "Γ⊢c#cs,(nrms, abrs)#css⇓Stuck"
by (auto intro: hyp1 terminatess.Cons terminates.intros dest: Stuck_end)
qed
with d show ?case by simp
qed
lemma Basic_terminates: "Γ⊢Basic f ↓ t"
by (cases t) (auto intro: terminates.intros)
lemma step_preserves_terminations:
assumes step: "Γ⊢(cs,css,s) → (cs',css',t)"
shows "Γ⊢cs,css⇓s ⟹ Γ⊢cs',css'⇓t"
using step
proof (induct)
case Skip thus ?case
by (auto elim: terminates_Normal_elim_cases terminatess_elim_cases
intro: exec.intros)
next
case Guard thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case GuardFault thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case FaultProp show ?case by (rule terminatess_Fault)
next
case FaultPropBlock show ?case by (rule terminatess_Fault)
next
case AbruptProp thus ?case
by (blast elim: terminatess_elim_cases
intro: terminatess.intros)
next
case ExitBlockNormal thus ?case
by (blast elim: terminatess_elim_cases
intro: terminatess.intros )
next
case ExitBlockAbrupt thus ?case
by (blast elim: terminatess_elim_cases
intro: terminatess.intros )
next
case Basic thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case Spec thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case SpecStuck thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case Seq thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case CondTrue thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case CondFalse thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case WhileTrue thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case WhileFalse thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case (Call p bdy cs css s)
have bdy: "Γ p = Some bdy" by fact
from Call obtain
term_body: "Γ⊢bdy ↓ Normal s" and
term_rest: "∀t. Γ⊢⟨Call p,Normal s⟩ ⇒ t ⟶ Γ⊢cs,css⇓t"
by (fastforce elim!: terminatess_elim_cases terminates_Normal_elim_cases)
show "Γ⊢[bdy],(cs,Throw # cs)#css⇓Normal s"
proof (rule terminatess.Cons [OF term_body],clarsimp)
fix t
assume exec_body: "Γ⊢⟨bdy,Normal s⟩ ⇒ t"
show "Γ⊢[],(cs,Throw # cs) # css⇓t"
proof (cases t)
case (Normal t')
with exec_body bdy
have "Γ⊢⟨Call p,Normal s⟩ ⇒ Normal t'"
by (auto intro: exec.intros)
with term_rest have "Γ⊢cs,css⇓Normal t'"
by iprover
with Normal show ?thesis
by (auto intro: terminatess.intros terminates.intros
elim: exec_Normal_elim_cases)
next
case (Abrupt t')
with exec_body bdy
have "Γ⊢⟨Call p,Normal s⟩ ⇒ Abrupt t'"
by (auto intro: exec.intros)
with term_rest have "Γ⊢cs,css⇓Abrupt t'"
by iprover
with Abrupt show ?thesis
by (fastforce intro: terminatess.intros terminates.intros
elim: exec_Normal_elim_cases)
next
case Fault
thus ?thesis
by (iprover intro: terminatess_Fault)
next
case Stuck
thus ?thesis
by (iprover intro: terminatess_Stuck)
qed
qed
next
case CallUndefined thus ?case
by (iprover intro: terminatess_Stuck)
next
case StuckProp show ?case by (rule terminatess_Stuck)
next
case StuckPropBlock show ?case by (rule terminatess_Stuck)
next
case DynCom thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case Throw thus ?case
by (blast elim: terminatess_elim_cases terminates_Normal_elim_cases
intro: terminatess.intros terminates.intros exec.intros)
next
case (Catch c1 c2 cs css s)
then obtain
term_c1: "Γ⊢c1 ↓ Normal s" and
term_c2: "∀s'. Γ⊢⟨c1,Normal s⟩ ⇒ Abrupt s' ⟶ Γ⊢c2 ↓ Normal s'"and
term_rest: "∀t. Γ⊢⟨Catch c1 c2,Normal s⟩ ⇒ t ⟶ Γ⊢cs,css⇓t"
by (clarsimp elim!: terminatess_elim_cases terminates_Normal_elim_cases)
show "Γ⊢[c1],(cs, c2 # cs) # css⇓Normal s"
proof (rule terminatess.Cons [OF term_c1],clarsimp)
fix t
assume exec_c1: "Γ⊢⟨c1,Normal s⟩ ⇒ t"
show "Γ⊢[],(cs, c2 # cs) # css⇓t"
proof (cases t)
case (Normal t')
with exec_c1 have "Γ⊢⟨Catch c1 c2,Normal s⟩ ⇒ t"
by (auto intro: exec.intros)
with term_rest have "Γ⊢cs,css⇓t"
by iprover
with Normal show ?thesis
by (iprover intro: terminatess.intros)
next
case (Abrupt t')
with exec_c1 term_c2 have "Γ⊢c2 ↓ Normal t'"
by auto
moreover
{
fix w
assume exec_c2: "Γ⊢⟨c2,Normal t'⟩ ⇒ w"
have "Γ⊢cs,css⇓w"
proof -
from exec_c1 Abrupt exec_c2
have "Γ⊢⟨Catch c1 c2,Normal s⟩ ⇒ w"
by (auto intro: exec.intros)
with term_rest show ?thesis by simp
qed
}
ultimately
show ?thesis using Abrupt
by (auto intro: terminatess.intros)
next
case Fault thus ?thesis
by (iprover intro: terminatess_Fault)
next
case Stuck thus ?thesis
by (iprover intro: terminatess_Stuck)
qed
qed
qed
ML ‹
ML_Thms.bind_thm ("rtrancl_induct3", Split_Rule.split_rule @{context}
(Rule_Insts.read_instantiate @{context}
[((("a", 0), Position.none), "(ax, ay, az)"),
((("b", 0), Position.none), "(bx, by, bz)")] []
@{thm rtranclp_induct}));
›
lemma steps_preserves_terminations:
assumes steps: "Γ⊢(cs,css,s) →⇧* (cs',css',t)"
shows "Γ⊢cs,css⇓s ⟹ Γ⊢cs',css'⇓t"
using steps
proof (induct rule: rtrancl_induct3 [consumes 1])
assume "Γ⊢cs,css⇓s" then show "Γ⊢cs,css⇓s".
next
fix cs'' css'' w cs' css' t
assume "Γ⊢(cs'',css'', w) → (cs',css', t)" "Γ⊢cs,css⇓s ⟹ Γ⊢cs'',css''⇓w"
"Γ⊢cs,css⇓s"
then show "Γ⊢cs',css'⇓t"
by (blast dest: step_preserves_terminations)
qed
theorem steps_preserves_termination:
assumes steps: "Γ⊢([c],[],s) →⇧* (c'#cs',css',t)"
assumes term_c: "Γ⊢c↓s"
shows "Γ⊢c'↓t"
proof -
from term_c have "Γ⊢[c],[]⇓s"
by (auto intro: terminatess.intros)
from steps this
have "Γ⊢c'#cs',css'⇓t"
by (rule steps_preserves_terminations)
thus "Γ⊢c'↓t"
by (auto elim: terminatess_elim_cases)
qed
lemma renumber':
assumes f: "∀i. (a,f i) ∈ r⇧* ∧ (f i,f(Suc i)) ∈ r"
assumes a_b: "(a,b) ∈ r⇧*"
shows "b = f 0 ⟹ (∃f. f 0 = a ∧ (∀i. (f i, f(Suc i)) ∈ r))"
using a_b
proof (induct rule: converse_rtrancl_induct [consumes 1])
assume "b = f 0"
with f show "∃f. f 0 = b ∧ (∀i. (f i, f (Suc i)) ∈ r)"
by blast
next
fix a z
assume a_z: "(a, z) ∈ r" and "(z, b) ∈ r⇧*"
assume "b = f 0 ⟹ ∃f. f 0 = z ∧ (∀i. (f i, f (Suc i)) ∈ r)"
"b = f 0"
then obtain f where f0: "f 0 = z" and seq: "∀i. (f i, f (Suc i)) ∈ r"
by iprover
{
fix i have "((λi. case i of 0 ⇒ a | Suc i ⇒ f i) i, f i) ∈ r"
using seq a_z f0
by (cases i) auto
}
then
show "∃f. f 0 = a ∧ (∀i. (f i, f (Suc i)) ∈ r)"
by - (rule exI [where x="λi. case i of 0 ⇒ a | Suc i ⇒ f i"],simp)
qed
lemma renumber:
"∀i. (a,f i) ∈ r⇧* ∧ (f i,f(Suc i)) ∈ r
⟹ ∃f. f 0 = a ∧ (∀i. (f i, f(Suc i)) ∈ r)"
by(blast dest:renumber')
lemma not_inf_Fault':
assumes enum_step: "∀i. Γ⊢f i → f (Suc i)"
shows "⋀k cs. f k = (cs,css,Fault m) ⟹ False"
proof (induct css)
case Nil
have f_k: "f k = (cs,[],Fault m)" by fact
have "⋀k. f k = (cs,[],Fault m) ⟹ False"
proof (induct cs)
case Nil
have "f k = ([], [], Fault m)" by fact
moreover
from enum_step have "Γ⊢f k → f (Suc k)"..
ultimately show "False"
by (fastforce elim: step_elim_cases)
next
case (Cons c cs)
have fk: "f k = (c # cs, [], Fault m)" by fact
from enum_step have "Γ⊢f k → f (Suc k)"..
with fk have "f (Suc k) = (cs,[],Fault m)"
by (fastforce elim: step_elim_cases)
with enum_step Cons.hyps
show False
by blast
qed
from this f_k show False by blast
next
case (Cons ds css)
then obtain nrms abrs where ds: "ds=(nrms,abrs)" by (cases ds) auto
have hyp: "⋀k cs. f k = (cs,css,Fault m) ⟹ False" by fact
have "⋀k. f k = (cs,(nrms,abrs)#css,Fault m) ⟹ False"
proof (induct cs)
case Nil
have fk: "f k = ([], (nrms, abrs) # css, Fault m)" by fact
from enum_step have "Γ⊢f k → f (Suc k)"..
with fk have "f (Suc k) = (nrms,css,Fault m)"
by (fastforce elim: step_elim_cases)
thus ?case
by (rule hyp)
next
case (Cons c cs)
have fk: "f k = (c#cs, (nrms, abrs) # css, Fault m)" by fact
have hyp1: "⋀k. f k = (cs, (nrms, abrs) # css, Fault m) ⟹ False" by fact
from enum_step have "Γ⊢f k → f (Suc k)"..
with fk have "f (Suc k) = (cs,(nrms,abrs)#css,Fault m)"
by (fastforce elim: step_elim_cases)
thus ?case
by (rule hyp1)
qed
with ds Cons.prems show False by auto
qed
lemma not_inf_Fault:
"¬ inf Γ cs css (Fault m)"
apply (rule not_infI)
apply (rule_tac f=f in not_inf_Fault' )
by auto
lemma not_inf_Stuck':
assumes enum_step: "∀i. Γ⊢f i → f (Suc i)"
shows "⋀k cs. f k = (cs,css,Stuck) ⟹ False"
proof (induct css)
case Nil
have f_k: "f k = (cs,[],Stuck)" by fact
have "⋀k. f k = (cs,[],Stuck) ⟹ False"
proof (induct cs)
case Nil
have "f k = ([], [], Stuck)" by fact
moreover
from enum_step have "Γ⊢f k → f (Suc k)"..
ultimately show "False"
by (fastforce elim: step_elim_cases)
next
case (Cons c cs)
have fk: "f k = (c # cs, [], Stuck)" by fact
from enum_step have "Γ⊢f k → f (Suc k)"..
with fk have "f (Suc k) = (cs,[],Stuck)"
by (fastforce elim: step_elim_cases)
with enum_step Cons.hyps
show False
by blast
qed
from this f_k show False .
next
case (Cons ds css)
then obtain nrms abrs where ds: "ds=(nrms,abrs)" by (cases ds) auto
have hyp: "⋀k cs. f k = (cs,css,Stuck) ⟹ False" by fact
have "⋀k. f k = (cs,(nrms,abrs)#css,Stuck) ⟹ False"
proof (induct cs)
case Nil
have fk: "f k = ([], (nrms, abrs) # css, Stuck)" by fact
from enum_step have "Γ⊢f k → f (Suc k)"..
with fk have "f (Suc k) = (nrms,css,Stuck)"
by (fastforce elim: step_elim_cases)
thus ?case
by (rule hyp)
next
case (Cons c cs)
have fk: "f k = (c#cs, (nrms, abrs) # css, Stuck)" by fact
have hyp1: "⋀k. f k = (cs, (nrms, abrs) # css, Stuck) ⟹ False" by fact
from enum_step have "Γ⊢f k → f (Suc k)"..
with fk have "f (Suc k) = (cs,(nrms,abrs)#css,Stuck)"
by (fastforce elim: step_elim_cases)
thus ?case
by (rule hyp1)
qed
with ds Cons.prems show False by auto
qed
lemma not_inf_Stuck:
"¬ inf Γ cs css Stuck"
apply (rule not_infI)
apply (rule_tac f=f in not_inf_Stuck')
by auto
lemma last_butlast_app:
assumes butlast: "butlast as = xs @ butlast bs"
assumes not_Nil: "bs ≠ []" "as ≠ []"
assumes last: "fst (last as) = fst (last bs)" "snd (last as) = snd (last bs)"
shows "as = xs @ bs"
proof -
from last have "last as = last bs"
by (cases "last as",cases "last bs") simp
moreover
from not_Nil have "as = butlast as @ [last as]" "bs = butlast bs @ [last bs]"
by auto
ultimately show ?thesis
using butlast
by simp
qed
lemma last_butlast_tl:
assumes butlast: "butlast bs = x # butlast as"
assumes not_Nil: "bs ≠ []" "as ≠ []"
assumes last: "fst (last as) = fst (last bs)" "snd (last as) = snd (last bs)"
shows "as = tl bs"
proof -
from last have "last as = last bs"
by (cases "last as",cases "last bs") simp
moreover
from not_Nil have "as = butlast as @ [last as]" "bs = butlast bs @ [last bs]"
by auto
ultimately show ?thesis
using butlast
by simp
qed
locale inf =
fixes CS:: "('s,'p,'f) config ⇒ ('s, 'p,'f) com list"
and CSS:: "('s,'p,'f) config ⇒ ('s, 'p,'f) continuation list"
and S:: "('s,'p,'f) config ⇒ ('s,'f) xstate"
defines CS_def : "CS ≡ fst"
defines CSS_def : "CSS ≡ λc. fst (snd c)"
defines S_def: "S ≡ λc. snd (snd c)"
lemma (in inf) steps_hd_drop_suffix:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "∀i. Γ⊢ f(i) → f(Suc i)"
assumes not_finished: "∀i < k. ¬ (CS (f i) = cs ∧ CSS (f i) = css)"
assumes simul: "∀i≤k.
(if pcss i = [] then CSS (f i)=css ∧ CS (f i)=pcs i@cs
else CS (f i)=pcs i ∧
CSS (f i)= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css)"
defines "p≡λi. (pcs i, pcss i, S (f i))"
shows "∀i<k. Γ⊢ p i → p (Suc i)"
using not_finished simul
proof (induct k)
case 0
thus ?case by simp
next
case (Suc k)
have simul: "∀i≤Suc k.
(if pcss i = [] then CSS (f i)=css ∧ CS (f i)=pcs i@cs
else CS (f i)=pcs i ∧
CSS (f i)= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css)" by fact
have not_finished': "∀i < Suc k. ¬ (CS (f i) = cs ∧ CSS (f i) = css)" by fact
with simul
have not_finished: "∀i<Suc k. ¬ (pcs i = [] ∧ pcss i = [])"
by (auto simp add: CS_def CSS_def S_def split: if_split_asm)
show ?case
proof (clarify)
fix i
assume i_le_Suc_k: "i < Suc k"
show "Γ⊢ p i → p (Suc i)"
proof (cases "i < k")
case True
with not_finished' simul Suc.hyps
show ?thesis
by auto
next
case False
with i_le_Suc_k
have eq_i_k: "i=k"
by simp
show "Γ⊢p i → p (Suc i)"
proof -
obtain cs' css' t' where
f_Suc_i: "f (Suc i) = (cs', css', t')"
by (cases "f (Suc i)")
obtain cs'' css'' t'' where
f_i: "f i = (cs'',css'',t'')"
by (cases "f i")
from not_finished eq_i_k
have pcs_pcss_not_Nil: "¬ (pcs i = [] ∧ pcss i = [])"
by auto
from simul [rule_format, of i] i_le_Suc_k f_i
have pcs_pcss_i:
"if pcss i = [] then css''=css ∧ cs''=pcs i@cs
else cs''=pcs i ∧
css''= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css"
by (simp add: CS_def CSS_def S_def cong: if_cong)
from simul [rule_format, of "Suc i"] i_le_Suc_k f_Suc_i
have pcs_pcss_Suc_i:
"if pcss (Suc i) = [] then css' = css ∧ cs' = pcs (Suc i) @ cs
else cs' = pcs (Suc i) ∧
css' = butlast (pcss (Suc i)) @
[(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @
css"
by (simp add: CS_def CSS_def S_def cong: if_cong)
show ?thesis
proof (cases "pcss i = []")
case True
note pcss_Nil = this
with pcs_pcss_i pcs_pcss_not_Nil obtain p ps where
pcs_i: "pcs i = p#ps" and
css'': "css''=css" and
cs'': "cs''=(p#ps)@cs"
by (auto simp add: neq_Nil_conv)
with f_i have "f i = (p#(ps@cs),css,t'')"
by simp
with f_Suc_i f_step [rule_format, of i]
have step_css: "Γ⊢ (p#(ps@cs),css,t'') → (cs',css',t')"
by simp
from step_Cons' [OF this, of p "ps@cs"]
obtain css''' where
css''': "css' = css''' @ css"
"if css''' = [] then ∃p. cs' = p @ ps @ cs
else (∃pnorm pabr. css'''=[(pnorm @ ps @ cs,pabr @ ps @ cs)])"
by auto
show ?thesis
proof (cases "css''' = []")
case True
with css'''
obtain p' where
css': "css' = css" and
cs': "cs' = p' @ ps @ cs"
by auto
from css' cs' step_css
have step: "Γ⊢ (p#(ps@cs),css,t'') → (p'@ps@cs,css,t')"
by simp
hence "Γ⊢ ((p#ps)@cs,css,t'') → ((p'@ps)@cs,css,t')"
by simp
from drop_suffix_css_step' [OF drop_suffix_same_css_step [OF this],
where xs="css" and css="[]" and css'="[]"]
have "Γ⊢ (p#ps,[],t'') → (p'@ps,[],t')"
by simp
moreover
from css' cs' pcs_pcss_Suc_i
obtain "pcs (Suc i) = p'@ps" and "pcss (Suc i) = []"
by (simp split: if_split_asm)
ultimately show ?thesis
using pcs_i pcss_Nil f_i f_Suc_i
by (simp add: CS_def CSS_def S_def p_def)
next
case False
with css'''
obtain pnorm pabr where
css': "css'=css'''@css"
"css'''=[(pnorm @ ps @ cs,pabr @ ps @ cs)]"
by auto
with css''' step_css
have "Γ⊢ (p#ps@cs,css,t'') → (cs',[(pnorm@ps@cs,pabr@ps@cs)]@css,t')"
by simp
then
have "Γ⊢(p#ps, css, t'') → (cs', [(pnorm@ps, pabr@ps)] @ css, t')"
by (rule drop_suffix_hd_css_step)
from drop_suffix_css_step' [OF this,
where css="[]" and xs="css" and css'="[(pnorm@ps, pabr@ps)]"]
have "Γ⊢ (p#ps,[],t'') → (cs',[(pnorm@ps, pabr@ps)],t')"
by simp
moreover
from css' pcs_pcss_Suc_i
obtain "pcs (Suc i) = cs'" "pcss (Suc i) = [(pnorm@ps, pabr@ps)]"
apply (cases "pcss (Suc i)")
apply (auto split: if_split_asm)
done
ultimately show ?thesis
using pcs_i pcss_Nil f_i f_Suc_i
by (simp add: p_def CS_def CSS_def S_def)
qed
next
case False
note pcss_i_not_Nil = this
with pcs_pcss_i obtain
cs'': "cs''=pcs i" and
css'': "css''= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css"
by auto
from f_Suc_i f_i f_step [rule_format, of i]
have step_i_full: "Γ⊢ (cs'',css'',t'') → (cs',css',t')"
by simp
show ?thesis
proof (cases cs'')
case (Cons c' cs)
with step_Cons' [OF step_i_full]
obtain css''' where css': "css' = css'''@css''"
by auto
with step_i_full
have "Γ⊢ (cs'',css'',t'') → (cs',css'''@css'',t')"
by simp
from Cons_change_css_step [OF this, where xss="pcss i"] Cons cs''
have "Γ⊢ (pcs i, pcss i,t'') → (cs',css'''@pcss i,t')"
by simp
moreover
from cs'' css'' css' False pcs_pcss_Suc_i
obtain "pcs (Suc i) = cs'" "pcss (Suc i) = css'''@pcss i"
apply (auto split: if_split_asm)
apply (drule (4) last_butlast_app)
by simp
ultimately show ?thesis
using f_i f_Suc_i
by (simp add: p_def CS_def CSS_def S_def)
next
case Nil
note cs''_Nil = this
show ?thesis
proof (cases "butlast (pcss i)")
case (Cons bpcs bpcss)
with cs''_Nil step_i_full css''
have *: "Γ⊢ ([],[hd css'']@tl css'',t'') → (cs',css',t')"
by simp
moreover
from step_Nil [OF *]
have css': "css'=tl css''"
by simp
ultimately have
step_i_full: "Γ⊢ ([],[hd css'']@tl css'',t'') → (cs',tl css'',t')"
by simp
from css'' Cons pcss_i_not_Nil
have "hd css'' = hd (pcss i)"
by (auto simp add: neq_Nil_conv split: if_split_asm)
with cs'' cs''_Nil
Nil_change_css_step [where ass="[hd css'']" and
css="tl css''" and ass'="[]" and
xss="tl (pcss i)", simplified, OF step_i_full [simplified]]
have "Γ⊢ (pcs i,[hd (pcss i)]@tl (pcss i),t'') → (cs',tl (pcss i),t')"
by simp
with pcss_i_not_Nil
have "Γ⊢ (pcs i,pcss i,t'') → (cs',tl (pcss i),t')"
by simp
moreover
from css' css'' cs''_Nil Cons pcss_i_not_Nil pcs_pcss_Suc_i
obtain "pcs (Suc i) = cs'" "pcss (Suc i) = tl (pcss i)"
apply (clarsimp split: if_split_asm)
apply (drule (4) last_butlast_tl)
by simp
ultimately show ?thesis
using f_i f_Suc_i
by (simp add: p_def CS_def CSS_def S_def)
next
case Nil
with css'' pcss_i_not_Nil
obtain pnorm pabr
where css'': "css''= [(pnorm@cs,pabr@cs)]@css" and
pcss_i: "pcss i = [(pnorm,pabr)]"
by (force simp add: neq_Nil_conv split: if_split_asm)
with cs''_Nil step_i_full
have "Γ⊢([],[(pnorm@cs,pabr@cs)]@css,t'') → (cs',css',t')"
by simp
from step_Nil [OF this]
obtain
css': "css'=css" and
cs': "(case t'' of
Abrupt s' ⇒ cs' = pabr @ cs ∧ t' = Normal s'
| _ ⇒ cs' = pnorm @ cs ∧ t' = t'')"
by (simp cong: xstate.case_cong)
let "?pcs_Suc_i " = "(case t'' of Abrupt s' ⇒ pabr | _ ⇒ pnorm)"
from cs'
have "Γ⊢([],[(pnorm,pabr)],t'') → (?pcs_Suc_i,[],t')"
by (auto intro: step.intros split: xstate.splits)
moreover
from css'' css' cs' pcss_i pcs_pcss_Suc_i
obtain "pcs (Suc i) = ?pcs_Suc_i" "pcss (Suc i) = []"
by (simp split: if_split_asm xstate.splits)
ultimately
show ?thesis
using pcss_i cs'' cs''_Nil f_i f_Suc_i
by (simp add: p_def CS_def CSS_def S_def)
qed
qed
qed
qed
qed
qed
qed
lemma k_steps_to_rtrancl:
assumes steps: "∀i<k. Γ⊢ p i → p (Suc i)"
shows "Γ⊢p 0→⇧* p k"
using steps
proof (induct k)
case 0 thus ?case by auto
next
case (Suc k)
have "∀i<Suc k. Γ⊢ p i → p (Suc i)" by fact
then obtain
step_le_k: "∀i<k. Γ⊢ p i → p (Suc i)" and step_k: "Γ⊢ p k → p (Suc k)"
by auto
from Suc.hyps [OF step_le_k]
have "Γ⊢ p 0 →⇧* p k".
also note step_k
finally show ?case .
qed
lemma (in inf) steps_hd_drop_suffix_finite:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "∀i. Γ⊢ f(i) → f(Suc i)"
assumes not_finished: "∀i < k. ¬ (CS (f i) = cs ∧ CSS (f i) = css)"
assumes simul: "∀i≤k.
(if pcss i = [] then CSS (f i)=css ∧ CS (f i)=pcs i@cs
else CS (f i)=pcs i ∧
CSS (f i)= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css)"
shows "Γ⊢([c],[],s) →⇧* (pcs k, pcss k, S (f k))"
proof -
from steps_hd_drop_suffix [OF f_0 f_step not_finished simul]
have "∀i<k. Γ⊢ (pcs i, pcss i, S (f i)) →
(pcs (Suc i), pcss (Suc i), S (f (Suc i)))".
from k_steps_to_rtrancl [OF this]
have "Γ⊢ (pcs 0, pcss 0, S (f 0)) →⇧* (pcs k, pcss k, S (f k))".
moreover from f_0 simul [rule_format, of 0]
have "(pcs 0, pcss 0, S (f 0)) = ([c],[],s)"
by (auto split: if_split_asm simp add: CS_def CSS_def S_def)
ultimately show ?thesis by simp
qed
lemma (in inf) steps_hd_drop_suffix_infinite:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "∀i. Γ⊢ f(i) → f(Suc i)"
assumes not_finished: "∀i. ¬ (CS (f i) = cs ∧ CSS (f i) = css)"
assumes simul: "∀i.
(if pcss i = [] then CSS (f i)=css ∧ CS (f i)=pcs i@cs
else CS (f i)=pcs i ∧
CSS (f i)= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css)"
defines "p≡λi. (pcs i, pcss i, S (f i))"
shows "Γ⊢ p i → p (Suc i)"
proof -
from steps_hd_drop_suffix [OF f_0 f_step, of "Suc i" pcss pcs] not_finished simul
show ?thesis
by (auto simp add: p_def)
qed
lemma (in inf) steps_hd_progress:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "∀i. Γ⊢ f(i) → f(Suc i)"
assumes c_unfinished: "∀i < k. ¬ (CS (f i) = cs ∧ CSS (f i) = css)"
shows "∀i ≤ k. (∃pcs pcss.
(if pcss = [] then CSS (f i)=css ∧ CS (f i)=pcs@cs
else CS (f i)=pcs ∧
CSS (f i)= butlast pcss@
[(fst (last pcss)@cs,(snd (last pcss))@cs)]@
css))"
using c_unfinished
proof (induct k)
case 0
with f_0 show ?case
by (simp add: CSS_def CS_def)
next
case (Suc k)
have c_unfinished: "∀i<Suc k. ¬ (CS (f i) = cs ∧ CSS (f i) = css)" by fact
hence c_unfinished': "∀i< k. ¬ (CS (f i) = cs ∧ CSS (f i) = css)" by simp
show ?case
proof (clarify)
fix i
assume i_le_Suc_k: "i ≤ Suc k"
show "∃pcs pcss.
(if pcss = [] then CSS (f i)=css ∧ CS (f i)=pcs@cs
else CS (f i)=pcs ∧
CSS (f i)= butlast pcss@
[(fst (last pcss)@cs,(snd (last pcss))@cs)]@
css)"
proof (cases "i < Suc k")
case True
with Suc.hyps [OF c_unfinished', rule_format, of i] c_unfinished
show ?thesis
by auto
next
case False
with i_le_Suc_k have eq_i_Suc_k: "i=Suc k"
by auto
obtain cs' css' t' where
f_Suc_k: "f (Suc k) = (cs', css', t')"
by (cases "f (Suc k)")
obtain cs'' css'' t'' where
f_k: "f k = (cs'',css'',t'')"
by (cases "f k")
with Suc.hyps [OF c_unfinished',rule_format, of k]
obtain pcs pcss where
pcs_pcss_k:
"if pcss = [] then css'' = css ∧ cs'' = pcs @ cs
else cs'' = pcs ∧
css'' = butlast pcss @
[(fst (last pcss) @ cs, snd (last pcss) @ cs)] @
css"
by (auto simp add: CSS_def CS_def cong: if_cong)
from c_unfinished [rule_format, of k] f_k pcs_pcss_k
have pcs_pcss_empty: "¬ (pcs = [] ∧ pcss = [])"
by (auto simp add: CS_def CSS_def S_def split: if_split_asm)
show ?thesis
proof (cases "pcss = []")
case True
note pcss_Nil = this
with pcs_pcss_k pcs_pcss_empty obtain p ps where
pcs_i: "pcs = p#ps" and
css'': "css''=css" and
cs'': "cs''=(p#ps)@cs"
by (cases "pcs") auto
with f_k have "f k = (p#(ps@cs),css,t'')"
by simp
with f_Suc_k f_step [rule_format, of k]
have step_css: "Γ⊢ (p#(ps@cs),css,t'') → (cs',css',t')"
by simp
from step_Cons' [OF this, of p "ps@cs"]
obtain css''' where
css''': "css' = css''' @ css"
"if css''' = [] then ∃p. cs' = p @ ps @ cs
else (∃pnorm pabr. css'''=[(pnorm @ ps @ cs,pabr @ ps @ cs)])"
by auto
show ?thesis
proof (cases "css''' = []")
case True
with css'''
obtain p' where
css': "css' = css" and
cs': "cs' = p' @ ps @ cs"
by auto
from css' cs' f_Suc_k
show ?thesis
apply (rule_tac x="p'@ps" in exI)
apply (rule_tac x="[]" in exI)
apply (simp add: CSS_def CS_def eq_i_Suc_k)
done
next
case False
with css'''
obtain pnorm pabr where
css': "css'=css'''@css"
"css'''=[(pnorm @ ps @ cs,pabr @ ps @ cs)]"
by auto
with f_Suc_k eq_i_Suc_k
show ?thesis
apply (rule_tac x="cs'" in exI)
apply (rule_tac x="[(pnorm@ps, pabr@ps)]" in exI)
by (simp add: CSS_def CS_def)
qed
next
case False
note pcss_k_not_Nil = this
with pcs_pcss_k obtain
cs'': "cs''=pcs" and
css'': "css''= butlast pcss@
[(fst (last pcss)@cs,(snd (last pcss))@cs)]@
css"
by auto
from f_Suc_k f_k f_step [rule_format, of k]
have step_i_full: "Γ⊢ (cs'',css'',t'') → (cs',css',t')"
by simp
show ?thesis
proof (cases cs'')
case (Cons c' cs)
with step_Cons' [OF step_i_full]
obtain css''' where css': "css' = css'''@css''"
by auto
with cs'' css'' f_Suc_k eq_i_Suc_k pcss_k_not_Nil
show ?thesis
apply (rule_tac x="cs'" in exI)
apply (rule_tac x="css'''@pcss" in exI)
by (clarsimp simp add: CSS_def CS_def butlast_append)
next
case Nil
note cs''_Nil = this
show ?thesis
proof (cases "butlast pcss")
case (Cons bpcs bpcss)
with cs''_Nil step_i_full css''
have *: "Γ⊢ ([],[hd css'']@tl css'',t'') → (cs',css',t')"
by simp
moreover
from step_Nil [OF *]
obtain css': "css'=tl css''" and
cs': "cs' = (case t'' of Abrupt s' ⇒ snd (hd css'')
| _ ⇒ fst (hd css''))"
by (auto split: xstate.splits)
from css'' Cons pcss_k_not_Nil
have "hd css'' = hd pcss"
by (auto simp add: neq_Nil_conv split: if_split_asm)
with css' cs' css'' cs''_Nil Cons pcss_k_not_Nil f_Suc_k eq_i_Suc_k
show ?thesis
apply (rule_tac x="cs'" in exI)
apply (rule_tac x="tl pcss" in exI)
apply (clarsimp split: xstate.splits
simp add: CS_def CSS_def neq_Nil_conv split: if_split_asm)
done
next
case Nil
with css'' pcss_k_not_Nil
obtain pnorm pabr
where css'': "css''= [(pnorm@cs,pabr@cs)]@css" and
pcss_k: "pcss = [(pnorm,pabr)]"
by (force simp add: neq_Nil_conv split: if_split_asm)
with cs''_Nil step_i_full
have "Γ⊢([],[(pnorm@cs,pabr@cs)]@css,t'') → (cs',css',t')"
by simp
from step_Nil [OF this]
obtain
css': "css'=css" and
cs': "(case t'' of
Abrupt s' ⇒ cs' = pabr @ cs ∧ t' = Normal s'
| _ ⇒ cs' = pnorm @ cs ∧ t' = t'')"
by (simp cong: xstate.case_cong)
let "?pcs_Suc_k " = "(case t'' of Abrupt s' ⇒ pabr | _ ⇒ pnorm)"
from css'' css' cs' pcss_k f_Suc_k eq_i_Suc_k
show ?thesis
apply (rule_tac x="?pcs_Suc_k" in exI)
apply (rule_tac x="[]" in exI)
apply (simp split: xstate.splits add: CS_def CSS_def)
done
qed
qed
qed
qed
qed
qed
lemma (in inf) inf_progress:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "∀i. Γ⊢ f(i) → f(Suc i)"
assumes unfinished: "∀i. ¬ ((CS (f i) = cs) ∧ (CSS (f i) = css))"
shows "∃pcs pcss.
(if pcss = [] then CSS (f i)=css ∧ CS (f i)=pcs@cs
else CS (f i)=pcs ∧
CSS (f i)= butlast pcss@
[(fst (last pcss)@cs,(snd (last pcss))@cs)]@
css)"
proof -
from steps_hd_progress [OF f_0 f_step, of "i"] unfinished
show ?thesis
by auto
qed
lemma skolemize1: "∀x. P x ⟶ (∃y. Q x y) ⟹ ∃f.∀x. P x ⟶ Q x (f x)"
by (rule choice) blast
lemma skolemize2: "∀x. P x ⟶ (∃y z. Q x y z) ⟹ ∃f g.∀x. P x ⟶ Q x (f x) (g x)"
apply (drule skolemize1)
apply (erule exE)
apply (drule skolemize1)
apply fast
done
lemma skolemize2': "∀x.∃y z. P x y z ⟹ ∃f g.∀x. P x (f x) (g x)"
apply (drule choice)
apply (erule exE)
apply (drule choice)
apply fast
done
theorem (in inf) inf_cases:
fixes c::"('s,'p,'f) com"
assumes inf: "inf Γ (c#cs) css s"
shows "inf Γ [c] [] s ∨ (∃t. Γ⊢⟨c,s⟩ ⇒ t ∧ inf Γ cs css t)"
proof -
from inf obtain f where
f_0: "f 0 = (c#cs,css,s)" and
f_step: "(∀i. Γ⊢f i → f (Suc i))"
by (auto simp add: inf_def)
show ?thesis
proof (cases "∃i. CS (f i) = cs ∧ CSS (f i) = css")
case True
define k where "k = (LEAST i. CS (f i) = cs ∧ CSS (f i) = css)"
from True
obtain CS_f_k: "CS (f k) = cs" and CSS_f_k: "CSS (f k) = css"
apply -
apply (erule exE)
apply (drule LeastI)
apply (simp add: k_def)
done
have less_k_prop: "∀i<k. ¬ (CS (f i) = cs ∧ CSS (f i) = css)"
apply (intro allI impI)
apply (unfold k_def)
apply (drule not_less_Least)
apply simp
done
have "Γ⊢([c], [], s) →⇧* ([],[],S (f k))"
proof -
have "∀i≤k. ∃pcs pcss.
(if pcss = [] then CSS (f i)=css ∧ CS (f i)=pcs@cs
else CS (f i)=pcs ∧
CSS (f i)= butlast pcss@
[(fst (last pcss)@cs,(snd (last pcss))@cs)]@
css)"
by (rule steps_hd_progress
[OF f_0 f_step, where k=k, OF less_k_prop])
from skolemize2 [OF this] obtain pcs pcss where
pcs_pcss:
"∀i≤k.
(if pcss i = [] then CSS (f i)=css ∧ CS (f i)=pcs i@cs
else CS (f i)=pcs i ∧
CSS (f i)= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css)"
by iprover
from pcs_pcss [rule_format, of k] CS_f_k CSS_f_k
have finished: "pcs k = []" "pcss k = []"
by (auto simp add: CS_def CSS_def S_def split: if_split_asm)
from pcs_pcss
have simul: "∀i≤k. (if pcss i = [] then CSS (f i)=css ∧ CS (f i)=pcs i@cs
else CS (f i)=pcs i ∧
CSS (f i)= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css)"
by auto
from steps_hd_drop_suffix_finite [OF f_0 f_step less_k_prop simul] finished
show ?thesis
by simp
qed
hence "Γ⊢⟨c,s⟩ ⇒ S (f k)"
by (rule steps_impl_exec)
moreover
from CS_f_k CSS_f_k f_step
have "inf Γ cs css (S (f k))"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (i + k)" in exI)
apply simp
apply (auto simp add: CS_def CSS_def S_def)
done
ultimately
have "(∃t. Γ⊢⟨c,s⟩ ⇒ t ∧ inf Γ cs css t)"
by blast
thus ?thesis
by simp
next
case False
hence unfinished: "∀i. ¬ ((CS (f i) = cs) ∧ (CSS (f i) = css))"
by simp
from inf_progress [OF f_0 f_step this]
have "∀i. ∃pcs pcss.
(if pcss = [] then CSS (f i)=css ∧ CS (f i)=pcs@cs
else CS (f i)=pcs ∧
CSS (f i)= butlast pcss@
[(fst (last pcss)@cs,(snd (last pcss))@cs)]@
css)"
by auto
from skolemize2' [OF this] obtain pcs pcss where
pcs_pcss: "∀i.
(if pcss i = [] then CSS (f i)=css ∧ CS (f i)=pcs i@cs
else CS (f i)=pcs i ∧
CSS (f i)= butlast (pcss i)@
[(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
css)"
by iprover
define g where "g i = (pcs i, pcss i, S (f i))" for i
from pcs_pcss [rule_format, of 0] f_0
have "g 0 = ([c],[],s)"
by (auto split: if_split_asm simp add: CS_def CSS_def S_def g_def)
moreover
from steps_hd_drop_suffix_infinite [OF f_0 f_step unfinished pcs_pcss]
have "∀i. Γ⊢g i → g (Suc i)"
by (simp add: g_def)
ultimately
have "inf Γ [c] [] s"
by (auto simp add: inf_def)
thus ?thesis
by simp
qed
qed
lemma infE [consumes 1]:
assumes inf: "inf Γ (c#cs) css s"
assumes cases: "inf Γ [c] [] s ⟹ P"
"⋀t. ⟦Γ⊢⟨c,s⟩ ⇒ t; inf Γ cs css t⟧ ⟹ P"
shows P
using inf cases
apply -
apply (drule inf.inf_cases)
apply auto
done
lemma inf_Seq:
"inf Γ (Seq c1 c2#cs) css (Normal s) = inf Γ (c1#c2#cs) css (Normal s)"
proof
assume "inf Γ (Seq c1 c2 # cs) css (Normal s)"
then obtain f where
f_0: "f 0 = (Seq c1 c2#cs,css,Normal s)" and
f_step: "∀i. Γ⊢f i → f (Suc i)"
by (auto simp add: inf_def)
from f_step [rule_format, of 0] f_0
have "f 1 = (c1#c2#cs,css,Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step show "inf Γ (c1#c2#cs) css (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
apply simp
done
next
assume "inf Γ (c1 # c2 # cs) css (Normal s)"
then obtain f where
f_0: "f 0 = (c1# c2#cs,css,Normal s)" and
f_step: "∀i. Γ⊢f i → f (Suc i)"
by (auto simp add: inf_def)
define g where "g i = (case i of 0 ⇒ (Seq c1 c2#cs,css,Normal s) | Suc j ⇒ f j)" for i
with f_0 have
"Γ⊢g 0 → g (Suc 0)"
by (auto intro: step.intros)
moreover
from f_step have "∀i. i≠0 ⟶ Γ⊢g i → g (Suc i)"
by (auto simp add: g_def split: nat.splits)
ultimately
show "inf Γ (Seq c1 c2 # cs) css (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x=g in exI)
apply (simp add: g_def split: nat.splits)
done
qed
lemma inf_WhileTrue:
assumes b: "s ∈ b"
shows "inf Γ (While b c#cs) css (Normal s) =
inf Γ (c#While b c#cs) css (Normal s)"
proof
assume "inf Γ (While b c # cs) css (Normal s)"
then obtain f where
f_0: "f 0 = (While b c#cs,css,Normal s)" and
f_step: "∀i. Γ⊢f i → f (Suc i)"
by (auto simp add: inf_def)
from b f_step [rule_format, of 0] f_0
have "f 1 = (c#While b c#cs,css,Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step show "inf Γ (c # While b c # cs) css (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
apply simp
done
next
assume "inf Γ (c # While b c # cs) css (Normal s)"
then obtain f where
f_0: "f 0 = (c # While b c #cs,css,Normal s)" and
f_step: "∀i. Γ⊢f i → f (Suc i)"
by (auto simp add: inf_def)
define h where "h i = (case i of 0 ⇒ (While b c#cs,css,Normal s) | Suc j ⇒ f j)" for i
with b f_0 have
"Γ⊢h 0 → h (Suc 0)"
by (auto intro: step.intros)
moreover
from f_step have "∀i. i≠0 ⟶ Γ⊢h i → h (Suc i)"
by (auto simp add: h_def split: nat.splits)
ultimately
show "inf Γ (While b c # cs) css (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x=h in exI)
apply (simp add: h_def split: nat.splits)
done
qed
lemma inf_Catch:
"inf Γ (Catch c1 c2#cs) css (Normal s) = inf Γ [c1] ((cs,c2#cs)#css) (Normal s)"
proof
assume "inf Γ (Catch c1 c2#cs) css (Normal s)"
then obtain f where
f_0: "f 0 = (Catch c1 c2#cs,css,Normal s)" and
f_step: "∀i. Γ⊢f i → f (Suc i)"
by (auto simp add: inf_def)
from f_step [rule_format, of 0] f_0
have "f 1 = ([c1],(cs,c2#cs)#css,Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step show "inf Γ [c1] ((cs,c2#cs)#css) (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
apply simp
done
next
assume "inf Γ [c1] ((cs,c2#cs)#css) (Normal s)"
then obtain f where
f_0: "f 0 = ([c1],(cs,c2#cs)#css,Normal s)" and
f_step: "∀i. Γ⊢f i → f (Suc i)"
by (auto simp add: inf_def)
define h where "h i = (case i of 0 ⇒ (Catch c1 c2#cs,css,Normal s) | Suc j ⇒ f j)" for i
with f_0 have
"Γ⊢h 0 → h (Suc 0)"
by (auto intro: step.intros)
moreover
from f_step have "∀i. i≠0 ⟶ Γ⊢h i → h (Suc i)"
by (auto simp add: h_def split: nat.splits)
ultimately
show "inf Γ (Catch c1 c2 # cs) css (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x=h in exI)
apply (simp add: h_def split: nat.splits)
done
qed
theorem terminates_impl_not_inf:
assumes termi: "Γ⊢c ↓ s"
shows "¬inf Γ [c] [] s"
using termi
proof induct
case (Skip s) thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Skip], [], Normal s)"
from f_step [of 0] f_0
have "f (Suc 0) = ([],[],Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step [of 1]
show False
by (auto elim: step_elim_cases)
qed
next
case (Basic g s)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Basic g], [], Normal s)"
from f_step [of 0] f_0
have "f (Suc 0) = ([],[],Normal (g s))"
by (auto elim: step_Normal_elim_cases)
with f_step [of 1]
show False
by (auto elim: step_elim_cases)
qed
next
case (Spec r s)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Spec r], [], Normal s)"
with f_step [of 0]
have "Γ⊢([Spec r], [], Normal s) → f (Suc 0)"
by simp
then show False
proof (cases)
fix t
assume "(s, t) ∈ r" "f (Suc 0) = ([], [], Normal t)"
with f_step [of 1]
show False
by (auto elim: step_elim_cases)
next
assume "∀t. (s, t) ∉ r" "f (Suc 0) = ([], [], Stuck)"
with f_step [of 1]
show False
by (auto elim: step_elim_cases)
qed
qed
next
case (Guard s g c m)
have g: "s ∈ g" by fact
have hyp: "¬ inf Γ [c] [] (Normal s)" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Guard m g c], [], Normal s)"
from g f_step [of 0] f_0
have "f (Suc 0) = ([c],[],Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step
have "inf Γ [c] [] (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with hyp show False ..
qed
next
case (GuardFault s g m c)
have g: "s ∉ g" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Guard m g c], [], Normal s)"
from g f_step [of 0] f_0
have "f (Suc 0) = ([],[],Fault m)"
by (auto elim: step_Normal_elim_cases)
with f_step [of 1]
show False
by (auto elim: step_elim_cases)
qed
next
case (Fault c m)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([c], [], Fault m)"
from f_step [of 0] f_0
have "f (Suc 0) = ([],[],Fault m)"
by (auto elim: step_Normal_elim_cases)
with f_step [of 1]
show False
by (auto elim: step_elim_cases)
qed
next
case (Seq c1 s c2)
have hyp_c1: "¬ inf Γ [c1] [] (Normal s)" by fact
have hyp_c2: "∀s'. Γ⊢⟨c1,Normal s⟩ ⇒ s' ⟶ Γ⊢c2 ↓ s' ∧ ¬ inf Γ [c2] [] s'" by fact
have "¬ inf Γ ([c1,c2]) [] (Normal s)"
proof
assume "inf Γ [c1, c2] [] (Normal s)"
then show False
proof (cases rule: infE)
assume "inf Γ [c1] [] (Normal s)"
with hyp_c1 show ?thesis by simp
next
fix t
assume "Γ⊢⟨c1,Normal s⟩ ⇒ t" "inf Γ [c2] [] t"
with hyp_c2 show ?thesis by simp
qed
qed
thus ?case
by (simp add: inf_Seq)
next
case (CondTrue s b c1 c2)
have b: "s ∈ b" by fact
have hyp_c1: "¬ inf Γ [c1] [] (Normal s)" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Cond b c1 c2], [], Normal s)"
from b f_step [of 0] f_0
have "f 1 = ([c1],[],Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step
have "inf Γ [c1] [] (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with hyp_c1 show False by simp
qed
next
case (CondFalse s b c2 c1)
have b: "s ∉ b" by fact
have hyp_c2: "¬ inf Γ [c2] [] (Normal s)" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Cond b c1 c2], [], Normal s)"
from b f_step [of 0] f_0
have "f 1 = ([c2],[],Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step
have "inf Γ [c2] [] (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with hyp_c2 show False by simp
qed
next
case (WhileTrue s b c)
have b: "s ∈ b" by fact
have hyp_c: "¬ inf Γ [c] [] (Normal s)" by fact
have hyp_w: "∀s'. Γ⊢⟨c,Normal s⟩ ⇒ s' ⟶
Γ⊢While b c ↓ s' ∧ ¬ inf Γ [While b c] [] s'" by fact
have "¬ inf Γ [c,While b c] [] (Normal s)"
proof
assume "inf Γ [c,While b c] [] (Normal s)"
from this hyp_c hyp_w show False
by (cases rule: infE) auto
qed
with b show ?case
by (simp add: inf_WhileTrue)
next
case (WhileFalse s b c)
have b: "s ∉ b" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([While b c], [], Normal s)"
from b f_step [of 0] f_0
have "f (Suc 0) = ([],[],Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step [of 1]
show False
by (auto elim: step_elim_cases)
qed
next
case (Call p bdy s)
have bdy: "Γ p = Some bdy" by fact
have hyp: "¬ inf Γ [bdy] [] (Normal s)" by fact
have not_inf_bdy:
"¬ inf Γ [bdy] [([],[Throw])] (Normal s)"
proof
assume "inf Γ [bdy] [([],[Throw])] (Normal s)"
then show False
proof (rule infE)
assume "inf Γ [bdy] [] (Normal s)"
with hyp show False by simp
next
fix t
assume "Γ⊢⟨bdy,Normal s⟩ ⇒ t"
assume inf: "inf Γ [] [([], [Throw])] t"
then obtain f where
f_0: "f 0 = ([],[([], [Throw])],t)" and
f_step: "∀i. Γ⊢f i → f (Suc i)"
by (auto simp add: inf_def)
show False
proof (cases t)
case (Normal t')
with f_0 f_step [rule_format, of 0]
have "f (Suc 0) = ([],[],(Normal t'))"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of "Suc 0"]
show False
by (auto elim: step.cases)
next
case (Abrupt t')
with f_0 f_step [rule_format, of 0]
have "f (Suc 0) = ([Throw],[],(Normal t'))"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of "Suc 0"]
have "f (Suc (Suc 0)) = ([],[],(Abrupt t'))"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of "Suc(Suc 0)"]
show False
by (auto elim: step.cases)
next
case (Fault m)
with f_0 f_step [rule_format, of 0]
have "f (Suc 0) = ([],[],Fault m)"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of 1]
have "f (Suc (Suc 0)) = ([],[],Fault m)"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of "Suc (Suc 0)"]
show False
by (auto elim: step.cases)
next
case Stuck
with f_0 f_step [rule_format, of 0]
have "f (Suc 0) = ([],[],Stuck)"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of 1]
have "f (Suc (Suc 0)) = ([],[],Stuck)"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of "Suc (Suc 0)"]
show False
by (auto elim: step.cases)
qed
qed
qed
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Call p], [], Normal s)"
from bdy f_step [of 0] f_0
have "f (Suc 0) =
([bdy],[([],[Throw])],Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step
have "inf Γ [bdy] [([],[Throw])] (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with not_inf_bdy
show False by simp
qed
next
case (CallUndefined p s)
have undef: "Γ p = None" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Call p], [], Normal s)"
from undef f_step [of 0] f_0
have "f (Suc 0) = ([],[],Stuck)"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of "Suc 0"]
show False
by (auto elim: step_elim_cases)
qed
next
case (Stuck c)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([c], [], Stuck)"
from f_step [of 0] f_0
have "f (Suc 0) = ([],[],Stuck)"
by (auto elim: step_elim_cases)
with f_step [rule_format, of "Suc 0"]
show False
by (auto elim: step_elim_cases)
qed
next
case (DynCom c s)
have hyp: "¬ inf Γ [(c s)] [] (Normal s)" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([DynCom c], [], Normal s)"
from f_step [of 0] f_0
have "f (Suc 0) = ([(c s)], [], Normal s)"
by (auto elim: step_elim_cases)
with f_step have "inf Γ [(c s)] [] (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with hyp
show False by simp
qed
next
case (Throw s)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([Throw], [], Normal s)"
from f_step [of 0] f_0
have "f (Suc 0) = ([],[],Abrupt s)"
by (auto elim: step_Normal_elim_cases)
with f_step [of 1]
show False
by (auto elim: step_elim_cases)
qed
next
case (Abrupt c s)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = ([c], [], Abrupt s)"
from f_step [of 0] f_0
have "f (Suc 0) = ([],[],Abrupt s)"
by (auto elim: step_elim_cases)
with f_step [rule_format, of "Suc 0"]
show False
by (auto elim: step_elim_cases)
qed
next
case (Catch c1 s c2)
have hyp_c1: "¬ inf Γ [c1] [] (Normal s)" by fact
have hyp_c2: "∀s'. Γ⊢⟨c1,Normal s⟩ ⇒ Abrupt s' ⟶
Γ⊢c2 ↓ Normal s' ∧ ¬ inf Γ [c2] [] (Normal s')" by fact
have "¬ inf Γ [c1] [([],[c2])] (Normal s)"
proof
assume "inf Γ [c1] [([],[c2])] (Normal s)"
then show False
proof (rule infE)
assume "inf Γ [c1] [] (Normal s)"
with hyp_c1 show False by simp
next
fix t
assume eval: "Γ⊢⟨c1,Normal s⟩ ⇒ t"
assume inf: "inf Γ [] [([], [c2])] t"
then obtain f where
f_0: "f 0 = ([],[([], [c2] )],t)" and
f_step: "∀i. Γ⊢f i → f (Suc i)"
by (auto simp add: inf_def)
show False
proof (cases t)
case (Normal t')
with f_0 f_step [rule_format, of 0]
have "f (Suc 0) = ([],[],Normal t')"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of 1]
show False
by (auto elim: step_elim_cases)
next
case (Abrupt t')
with f_0 f_step [rule_format, of 0]
have "f (Suc 0) = ([c2],[],Normal t')"
by (auto elim: step_Normal_elim_cases)
with f_step eval Abrupt
have "inf Γ [c2] [] (Normal t')"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with eval hyp_c2 Abrupt show False by simp
next
case (Fault m)
with f_0 f_step [rule_format, of 0]
have "f (Suc 0) = ([],[],Fault m)"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of 1]
show False
by (auto elim: step_elim_cases)
next
case Stuck
with f_0 f_step [rule_format, of 0]
have "f (Suc 0) = ([],[],Stuck)"
by (auto elim: step_Normal_elim_cases)
with f_step [rule_format, of 1]
show False
by (auto elim: step_elim_cases)
qed
qed
qed
thus ?case
by (simp add: inf_Catch)
qed
lemma terminatess_impl_not_inf:
assumes termi: "Γ⊢cs,css⇓s"
shows "¬inf Γ cs css s"
using termi
proof (induct)
case (Nil s)
show ?case
proof (rule not_infI)
fix f
assume "⋀i. Γ⊢f i → f (Suc i)"
hence "Γ⊢f 0 → f (Suc 0)"
by simp
moreover
assume "f 0 = ([], [], s)"
ultimately show False
by (fastforce elim: step.cases)
qed
next
case (ExitBlockNormal nrms css s abrs)
have hyp: "¬ inf Γ nrms css (Normal s)" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f0: "f 0 = ([], (nrms, abrs) # css, Normal s)"
with f_step [of 0] have "f (Suc 0) = (nrms,css,Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step have "inf Γ nrms css (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with hyp show False ..
qed
next
case (ExitBlockAbrupt abrs css s nrms)
have hyp: "¬ inf Γ abrs css (Normal s)" by fact
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f0: "f 0 = ([], (nrms, abrs) # css, Abrupt s)"
with f_step [of 0] have "f (Suc 0) = (abrs,css,Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step have "inf Γ abrs css (Normal s)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with hyp show False ..
qed
next
case (ExitBlockFault nrms css f abrs)
show ?case
by (rule not_inf_Fault)
next
case (ExitBlockStuck nrms css abrs)
show ?case
by (rule not_inf_Stuck)
next
case (Cons c s cs css)
have termi_c: "Γ⊢c ↓ s" by fact
have hyp: "∀t. Γ⊢⟨c,s⟩ ⇒ t ⟶ Γ⊢cs,css⇓t ∧ ¬ inf Γ cs css t" by fact
show "¬ inf Γ (c # cs) css s"
proof
assume "inf Γ (c # cs) css s"
thus False
proof (rule infE)
assume "inf Γ [c] [] s"
with terminates_impl_not_inf [OF termi_c]
show False ..
next
fix t
assume "Γ⊢⟨c,s⟩ ⇒ t" "inf Γ cs css t"
with hyp show False by simp
qed
qed
qed
lemma lem:
"∀y. r⇧+⇧+ a y ⟶ P a ⟶ P y
⟹ ((b,a) ∈ {(y,x). P x ∧ r x y}⇧+) = ((b,a) ∈ {(y,x). P x ∧ r⇧+⇧+ x y})"
apply(rule iffI)
apply clarify
apply(erule trancl_induct)
apply blast
apply(blast intro:tranclp_trans)
apply clarify
apply(erule tranclp_induct)
apply blast
apply(blast intro:trancl_trans)
done
corollary terminatess_impl_no_inf_chain:
assumes terminatess: "Γ⊢cs,css⇓s"
shows "¬(∃f. f 0 = (cs,css,s) ∧ (∀i::nat. Γ⊢f i →⇧+ f(Suc i)))"
proof -
have "wf({(y,x). Γ⊢(cs,css,s) →⇧* x ∧ Γ⊢x → y}⇧+)"
proof (rule wf_trancl)
show "wf {(y, x). Γ⊢(cs, css, s) →⇧* x ∧ Γ⊢x → y}"
proof (simp only: wf_iff_no_infinite_down_chain,clarify,simp)
fix f
assume "∀i. Γ⊢(cs, css, s) →⇧* f i ∧ Γ⊢f i → f (Suc i)"
hence "∃f. f 0 = (cs, css, s) ∧ (∀i. Γ⊢f i → f (Suc i))"
by (rule renumber [to_pred])
moreover from terminatess
have "¬ (∃f. f 0 = (cs, css, s) ∧ (∀i. Γ⊢f i → f (Suc i)))"
by (rule terminatess_impl_not_inf [unfolded inf_def])
ultimately show False
by simp
qed
qed
hence "¬ (∃f. ∀i. (f (Suc i), f i)
∈ {(y, x). Γ⊢(cs, css, s) →⇧* x ∧ Γ⊢x → y}⇧+)"
by (simp add: wf_iff_no_infinite_down_chain)
thus ?thesis
proof (rule contrapos_nn)
assume "∃f. f 0 = (cs, css, s) ∧ (∀i. Γ⊢f i →⇧+ f (Suc i))"
then obtain f where
f0: "f 0 = (cs, css, s)" and
seq: "∀i. Γ⊢f i →⇧+ f (Suc i)"
by iprover
show
"∃f. ∀i. (f (Suc i), f i) ∈ {(y, x). Γ⊢(cs, css, s) →⇧* x ∧ Γ⊢x → y}⇧+"
proof (rule exI [where x=f],rule allI)
fix i
show "(f (Suc i), f i) ∈ {(y, x). Γ⊢(cs, css, s) →⇧* x ∧ Γ⊢x → y}⇧+"
proof -
{
fix i have "Γ⊢(cs,css,s) →⇧* f i"
proof (induct i)
case 0 show "Γ⊢(cs, css, s) →⇧* f 0"
by (simp add: f0)
next
case (Suc n)
have "Γ⊢(cs, css, s) →⇧* f n" by fact
with seq show "Γ⊢(cs, css, s) →⇧* f (Suc n)"
by (blast intro: tranclp_into_rtranclp rtranclp_trans)
qed
}
hence "Γ⊢(cs,css,s) →⇧* f i"
by iprover
with seq have
"(f (Suc i), f i) ∈ {(y, x). Γ⊢(cs, css, s) →⇧* x ∧ Γ⊢x →⇧+ y}"
by clarsimp
moreover
have "∀y. Γ⊢f i →⇧+ y⟶Γ⊢(cs, css, s) →⇧* f i⟶Γ⊢(cs, css, s) →⇧* y"
by (blast intro: tranclp_into_rtranclp rtranclp_trans)
ultimately
show ?thesis
by (subst lem)
qed
qed
qed
qed
corollary terminates_impl_no_inf_chain:
"Γ⊢c↓s ⟹ ¬(∃f. f 0 = ([c],[],s) ∧ (∀i::nat. Γ⊢f i →⇧+ f(Suc i)))"
by (rule terminatess_impl_no_inf_chain) (iprover intro: terminatess.intros)
definition
termi_call_steps :: "('s,'p,'f) body ⇒ (('s × 'p) × ('s × 'p))set"
where
"termi_call_steps Γ =
{((t,q),(s,p)). Γ⊢the (Γ p)↓Normal s ∧
(∃css. Γ⊢([the (Γ p)],[],Normal s) →⇧+ ([the (Γ q)],css,Normal t))}"
text ‹Sequencing computations, or more exactly continuation stacks›
primrec seq:: "(nat ⇒ 'a list) ⇒ nat ⇒ 'a list"
where
"seq css 0 = []" |
"seq css (Suc i) = css i@seq css i"
theorem wf_termi_call_steps: "wf (termi_call_steps Γ)"
proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain,
clarify,simp)
fix S
assume inf:
"∀i. (λ(t,q) (s,p). Γ⊢(the (Γ p)) ↓ Normal s ∧
(∃css. Γ⊢([the (Γ p)],[],Normal s) →⇧+ ([the (Γ q)],css,Normal t)))
(S (Suc i)) (S i)"
obtain s p where "s = (λi. fst (S i))" and "p = (λi. snd (S i))"
by auto
with inf
have inf':
"∀i. Γ⊢(the (Γ (p i))) ↓ Normal (s i) ∧
(∃css. Γ⊢([the (Γ (p i))],[],Normal (s i)) →⇧+
([the (Γ (p (Suc i)))],css,Normal (s (Suc i))))"
apply -
apply (rule allI)
apply (erule_tac x=i in allE)
apply auto
done
show False
proof -
from inf'
have "∃css. ∀i. Γ⊢(the (Γ (p i))) ↓ Normal (s i) ∧
Γ⊢([the (Γ (p i))],[],Normal (s i)) →⇧+
([the (Γ (p (Suc i)))],css i,Normal (s (Suc i)))"
apply -
apply (rule choice)
by blast
then obtain css where
termi_css: "∀i. Γ⊢(the (Γ (p i))) ↓ Normal (s i)" and
step_css: "∀i. Γ⊢([the (Γ (p i))],[],Normal (s i)) →⇧+
([the (Γ (p (Suc i)))],css i,Normal (s (Suc i)))"
by blast
define f where "f i = ([the (Γ (p i))], seq css i,Normal (s i)::('a,'c) xstate)" for i
have "f 0 = ([the (Γ (p 0))],[],Normal (s 0))"
by (simp add: f_def)
moreover
have "∀i. Γ⊢ (f i) →⇧+ (f (i+1))"
proof
fix i
from step_css [rule_format, of i]
have "Γ⊢([the (Γ (p i))], [], Normal (s i)) →⇧+
([the (Γ (p (Suc i)))], css i, Normal (s (Suc i)))".
from app_css_steps [OF this,simplified]
have "Γ⊢([the (Γ (p i))], seq css i, Normal (s i)) →⇧+
([the (Γ (p (Suc i)))], css i@seq css i, Normal (s (Suc i)))".
thus "Γ⊢ (f i) →⇧+ (f (i+1))"
by (simp add: f_def)
qed
moreover from termi_css [rule_format, of 0]
have "¬ (∃f. (f 0 = ([the (Γ (p 0))],[],Normal (s 0)) ∧
(∀i. Γ⊢(f i) →⇧+ f(Suc i))))"
by (rule terminates_impl_no_inf_chain)
ultimately show False
by auto
qed
qed
text ‹An alternative proof using Hilbert-choice instead of axiom of choice.›
theorem "wf (termi_call_steps Γ)"
proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain,
clarify,simp)
fix S
assume inf:
"∀i. (λ(t,q) (s,p). Γ⊢(the (Γ p)) ↓ Normal s ∧
(∃css. Γ⊢([the (Γ p)],[],Normal s) →⇧+ ([the (Γ q)],css,Normal t)))
(S (Suc i)) (S i)"
obtain s p where "s = (λi. fst (S i))" and "p = (λi. snd (S i))"
by auto
with inf
have inf':
"∀i. Γ⊢(the (Γ (p i))) ↓ Normal (s i) ∧
(∃css. Γ⊢([the (Γ (p i))],[],Normal (s i)) →⇧+
([the (Γ (p (Suc i)))],css,Normal (s (Suc i))))"
apply -
apply (rule allI)
apply (erule_tac x=i in allE)
apply auto
done
show "False"
proof -
define CSS where "CSS i = (SOME css.
Γ⊢([the (Γ (p i))],[], Normal (s i)) →⇧+
([the (Γ (p (i+1)))],css,Normal (s (i+1))))" for i
define f where "f i = ([the (Γ (p i))], seq CSS i,Normal (s i)::('a,'c) xstate)" for i
have "f 0 = ([the (Γ (p 0))],[],Normal (s 0))"
by (simp add: f_def)
moreover
have "∀i. Γ⊢ (f i) →⇧+ (f (i+1))"
proof
fix i
from inf' [rule_format, of i] obtain css where
css: "Γ⊢([the (Γ (p i))],[],Normal (s i)) →⇧+
([the (Γ (p (i+1)))],css,Normal (s (i+1)))"
by fastforce
hence "Γ⊢([the (Γ (p i))], seq CSS i, Normal (s i)) →⇧+
([the (Γ (p (i+1)))], CSS i @ seq CSS i, Normal (s (i+1)))"
apply -
apply (unfold CSS_def)
apply (rule someI2
[where P="λcss.
Γ⊢([the (Γ (p i))],[],Normal (s i))→⇧+
([the (Γ (p (i+1)))],css, Normal (s (i+1)))"])
apply (rule css)
apply (fastforce dest: app_css_steps)
done
thus "Γ⊢ (f i) →⇧+ (f (i+1))"
by (simp add: f_def)
qed
moreover from inf' [rule_format, of 0]
have "Γ⊢the (Γ (p 0)) ↓ Normal (s 0)"
by iprover
then have "¬ (∃f. (f 0 = ([the (Γ (p 0))],[],Normal (s 0)) ∧
(∀i. Γ⊢(f i) →⇧+ f(Suc i))))"
by (rule terminates_impl_no_inf_chain)
ultimately show False
by auto
qed
qed
lemma not_inf_implies_wf: assumes not_inf: "¬ inf Γ cs css s"
shows "wf {(c2,c1). Γ ⊢ (cs,css,s) →⇧* c1 ∧ Γ ⊢ c1 → c2}"
proof (simp only: wf_iff_no_infinite_down_chain,clarify, simp)
fix f
assume "∀i. Γ⊢(cs, css, s) →⇧* f i ∧ Γ⊢f i → f (Suc i)"
hence "∃f. f 0 = (cs, css, s) ∧ (∀i. Γ⊢f i → f (Suc i))"
by (rule renumber [to_pred])
moreover from not_inf
have "¬ (∃f. f 0 = (cs, css, s) ∧ (∀i. Γ⊢f i → f (Suc i)))"
by (unfold inf_def)
ultimately show False
by simp
qed
lemma wf_implies_termi_reach:
assumes wf: "wf {(c2,c1). Γ ⊢ (cs,css,s) →⇧* c1 ∧ Γ ⊢ c1 → c2}"
shows "⋀cs1 css1 s1. ⟦Γ ⊢ (cs,css,s) →⇧* c1; c1=(cs1,css1,s1)⟧⟹ Γ⊢cs1,css1⇓s1"
using wf
proof (induct c1, simp)
fix cs1 css1 s1
assume reach: "Γ⊢(cs, css, s) →⇧* (cs1, css1, s1)"
assume hyp_raw: "⋀y cs2 css2 s2. ⟦Γ ⊢ (cs1,css1,s1) → (cs2,css2,s2);
Γ ⊢ (cs,css,s) →⇧* (cs2,css2,s2); y=(cs2,css2,s2)⟧ ⟹
Γ⊢cs2,css2⇓s2"
have hyp: "⋀cs2 css2 s2. ⟦Γ ⊢ (cs1,css1,s1) → (cs2,css2,s2)⟧ ⟹
Γ⊢cs2,css2⇓s2"
apply -
apply (rule hyp_raw)
apply assumption
using reach
apply simp
apply (rule refl)
done
show "Γ⊢cs1,css1⇓s1"
proof (cases s1)
case (Normal s1')
show ?thesis
proof (cases cs1)
case Nil
note cs1_Nil = this
show ?thesis
proof (cases css1)
case Nil
with cs1_Nil show ?thesis
by (auto intro: terminatess.intros)
next
case (Cons nrms_abrs css1')
then obtain nrms abrs where nrms_abrs: "nrms_abrs=(nrms,abrs)"
by (cases "nrms_abrs")
have "Γ ⊢ ([],(nrms,abrs)#css1',Normal s1') → (nrms,css1',Normal s1')"
by (rule step.intros)
from hyp [simplified cs1_Nil Cons nrms_abrs Normal, OF this]
have "Γ⊢nrms,css1'⇓Normal s1'".
from ExitBlockNormal [OF this] cs1_Nil Cons nrms_abrs Normal
show ?thesis
by auto
qed
next
case (Cons c1 cs1')
have "Γ⊢c1#cs1',css1⇓Normal s1'"
proof (cases c1)
case Skip
have "Γ ⊢ (Skip#cs1',css1,Normal s1') → (cs1',css1,Normal s1')"
by (rule step.intros)
from hyp [simplified Cons Skip Normal, OF this]
have "Γ⊢cs1',css1⇓Normal s1'".
with Normal Skip show ?thesis
by (auto intro: terminatess.intros terminates.intros
elim: exec_Normal_elim_cases)
next
case (Basic f)
have "Γ ⊢ (Basic f#cs1',css1,Normal s1') → (cs1',css1,Normal (f s1'))"
by (rule step.intros)
from hyp [simplified Cons Basic Normal, OF this]
have "Γ⊢cs1',css1⇓Normal (f s1')".
with Normal Basic show ?thesis
by (auto intro: terminatess.intros terminates.intros
elim: exec_Normal_elim_cases)
next
case (Spec r)
with Normal show ?thesis
apply simp
apply (rule terminatess.Cons)
apply (fastforce intro: terminates.intros)
apply (clarify)
apply (erule exec_Normal_elim_cases)
apply clarsimp
apply (rule hyp)
apply (fastforce intro: step.intros simp add: Cons Spec Normal )
apply (fastforce intro: terminatess_Stuck)
done
next
case (Seq c⇩1 c⇩2)
have "Γ ⊢ (Seq c⇩1 c⇩2#cs1',css1,Normal s1') → (c⇩1#c⇩2#cs1',css1,Normal s1')"
by (rule step.intros)
from hyp [simplified Cons Seq Normal, OF this]
have "Γ⊢c⇩1 # c⇩2 # cs1',css1⇓Normal s1'".
with Normal Seq show ?thesis
by (fastforce intro: terminatess.intros terminates.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
next
case (Cond b c⇩1 c⇩2)
show ?thesis
proof (cases "s1' ∈ b")
case True
hence "Γ⊢(Cond b c⇩1 c⇩2#cs1',css1,Normal s1') → (c⇩1#cs1',css1,Normal s1')"
by (rule step.intros)
from hyp [simplified Cons Cond Normal, OF this]
have "Γ⊢c⇩1 # cs1',css1⇓Normal s1'".
with Normal Cond True show ?thesis
by (fastforce intro: terminatess.intros terminates.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
next
case False
hence "Γ⊢(Cond b c⇩1 c⇩2#cs1',css1,Normal s1') → (c⇩2#cs1',css1,Normal s1')"
by (rule step.intros)
from hyp [simplified Cons Cond Normal, OF this]
have "Γ⊢c⇩2 # cs1',css1⇓Normal s1'".
with Normal Cond False show ?thesis
by (fastforce intro: terminatess.intros terminates.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
qed
next
case (While b c')
show ?thesis
proof (cases "s1' ∈ b")
case True
then have "Γ⊢(While b c' # cs1', css1, Normal s1') →
(c' # While b c' # cs1', css1, Normal s1')"
by (rule step.intros)
from hyp [simplified Cons While Normal, OF this]
have "Γ⊢c' # While b c' # cs1',css1⇓Normal s1'".
with Cons While True Normal
show ?thesis
by (fastforce intro: terminatess.intros terminates.intros exec.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
next
case False
then
have "Γ⊢(While b c' # cs1', css1, Normal s1') → (cs1', css1, Normal s1')"
by (rule step.intros)
from hyp [simplified Cons While Normal, OF this]
have "Γ⊢cs1',css1⇓Normal s1'".
with Cons While False Normal
show ?thesis
by (fastforce intro: terminatess.intros terminates.intros exec.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
qed
next
case (Call p)
show ?thesis
proof (cases "Γ p")
case None
with Call Normal show ?thesis
by (fastforce intro: terminatess.intros terminates.intros terminatess_Stuck
elim: exec_Normal_elim_cases)
next
case (Some bdy)
then
have "Γ ⊢ (Call p#cs1',css1,Normal s1') →
([bdy],(cs1',Throw#cs1')#css1,Normal s1')"
by (rule step.intros)
from hyp [simplified Cons Call Normal Some, OF this]
have "Γ⊢[bdy],(cs1', Throw # cs1') # css1⇓Normal s1'".
with Some Call Normal show ?thesis
apply simp
apply (rule terminatess.intros)
apply (blast elim: terminatess_elim_cases intro: terminates.intros)
apply clarify
apply (erule terminatess_elim_cases)
apply (erule exec_Normal_elim_cases)
prefer 2
apply simp
apply (erule_tac x=t in allE)
apply (case_tac t)
apply (auto intro: terminatess_Stuck terminatess_Fault exec.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
done
qed
next
case (DynCom c')
have "Γ ⊢ (DynCom c'#cs1',css1,Normal s1') → (c' s1'#cs1',css1,Normal s1')"
by (rule step.intros)
from hyp [simplified Cons DynCom Normal, OF this]
have "Γ⊢c' s1'#cs1',css1⇓Normal s1'".
with Normal DynCom show ?thesis
by (fastforce intro: terminatess.intros terminates.intros exec.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
next
case (Guard f g c')
show ?thesis
proof (cases "s1' ∈ g")
case True
then have "Γ ⊢ (Guard f g c'#cs1',css1,Normal s1') → (c'#cs1',css1,Normal s1')"
by (rule step.intros)
from hyp [simplified Cons Guard Normal, OF this]
have "Γ⊢c'#cs1',css1⇓Normal s1'".
with Normal Guard True show ?thesis
by (fastforce intro: terminatess.intros terminates.intros exec.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
next
case False
with Guard Normal show ?thesis
by (fastforce intro: terminatess.intros terminatess_Fault
terminates.intros
elim: exec_Normal_elim_cases)
qed
next
case Throw
have "Γ ⊢ (Throw#cs1',css1,Normal s1') → (cs1',css1,Abrupt s1')"
by (rule step.intros)
from hyp [simplified Cons Throw Normal, OF this]
have "Γ⊢cs1',css1⇓Abrupt s1'".
with Normal Throw show ?thesis
by (auto intro: terminatess.intros terminates.intros
elim: exec_Normal_elim_cases)
next
case (Catch c⇩1 c⇩2)
have "Γ ⊢ (Catch c⇩1 c⇩2#cs1',css1,Normal s1') →
([c⇩1], (cs1',c⇩2#cs1')# css1,Normal s1')"
by (rule step.intros)
from hyp [simplified Cons Catch Normal, OF this]
have "Γ⊢[c⇩1],(cs1', c⇩2 # cs1') # css1⇓Normal s1'".
with Normal Catch show ?thesis
by (fastforce intro: terminatess.intros terminates.intros exec.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
qed
with Cons Normal show ?thesis
by simp
qed
next
case (Abrupt s1')
show ?thesis
proof (cases cs1)
case Nil
note cs1_Nil = this
show ?thesis
proof (cases css1)
case Nil
with cs1_Nil show ?thesis by (auto intro: terminatess.intros)
next
case (Cons nrms_abrs css1')
then obtain nrms abrs where nrms_abrs: "nrms_abrs=(nrms,abrs)"
by (cases "nrms_abrs")
have "Γ ⊢ ([],(nrms,abrs)#css1',Abrupt s1') → (abrs,css1',Normal s1')"
by (rule step.intros)
from hyp [simplified cs1_Nil Cons nrms_abrs Abrupt, OF this]
have "Γ⊢abrs,css1'⇓Normal s1'".
from ExitBlockAbrupt [OF this] cs1_Nil Cons nrms_abrs Abrupt
show ?thesis
by auto
qed
next
case (Cons c1 cs1')
have "Γ⊢c1#cs1',css1⇓Abrupt s1'"
proof -
have "Γ ⊢ (c1#cs1',css1,Abrupt s1') → (cs1',css1,Abrupt s1')"
by (rule step.intros)
from hyp [simplified Cons Abrupt, OF this]
have "Γ⊢cs1',css1⇓Abrupt s1'".
with Cons Abrupt
show ?thesis
by (fastforce intro: terminatess.intros terminates.intros exec.intros
elim: terminatess_elim_cases exec_Normal_elim_cases)
qed
with Cons Abrupt show ?thesis by simp
qed
next
case (Fault f)
thus ?thesis by (auto intro: terminatess_Fault)
next
case Stuck
thus ?thesis by (auto intro: terminatess_Stuck)
qed
qed
lemma not_inf_impl_terminatess:
assumes not_inf: "¬ inf Γ cs css s"
shows "Γ⊢cs,css⇓s"
proof -
from not_inf_implies_wf [OF not_inf]
have wf: "wf {(c2, c1). Γ⊢(cs, css, s) →⇧* c1 ∧ Γ⊢c1 → c2}".
show ?thesis
by (rule wf_implies_termi_reach [OF wf]) auto
qed
lemma not_inf_impl_terminates:
assumes not_inf: "¬ inf Γ [c] [] s"
shows "Γ⊢c↓s"
proof -
from not_inf_impl_terminatess [OF not_inf]
have "Γ⊢[c],[]⇓s".
thus ?thesis
by (auto elim: terminatess_elim_cases)
qed
theorem terminatess_iff_not_inf:
"Γ⊢cs,css⇓s = (¬ inf Γ cs css s)"
apply rule
apply (erule terminatess_impl_not_inf)
apply (erule not_inf_impl_terminatess)
done
corollary terminates_iff_not_inf:
"Γ⊢c↓s = (¬ inf Γ [c] [] s)"
apply (rule)
apply (erule terminates_impl_not_inf)
apply (erule not_inf_impl_terminates)
done
subsection ‹Completeness of Total Correctness Hoare Logic›
lemma ConseqMGT:
assumes modif: "∀Z::'a. Γ,Θ ⊢⇩t⇘/F⇙ (P' Z::'a assn) c (Q' Z),(A' Z)"
assumes impl: "⋀s. s ∈ P ⟹ s ∈ P' s ∧ (∀t. t ∈ Q' s ⟶ t ∈ Q) ∧
(∀t. t ∈ A' s ⟶ t ∈ A)"
shows "Γ,Θ ⊢⇩t⇘/F⇙ P c Q,A"
using impl
by - (rule conseq [OF modif],blast)
lemma :
assumes state_indep_prop:"∀s ∈ P. R"
assumes to_show: "R ⟹ Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
shows "Γ,Θ⊢⇩t⇘/F⇙ P c Q,A"
apply (rule Conseq)
apply (clarify)
apply (rule_tac x="P" in exI)
apply (rule_tac x="Q" in exI)
apply (rule_tac x="A" in exI)
using state_indep_prop to_show
by blast
lemma Call_lemma':
assumes Call_hyp:
"∀q∈dom Γ. ∀Z. Γ,Θ⊢⇩t⇘/F⇙{s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
shows "⋀Z. Γ,Θ ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧ Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c#cs,css,Normal s))}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
proof (induct c)
case Skip
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Skip,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Skip # cs,css,Normal s))}
Skip
{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Skip,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Skip [THEN conseqPre]) (blast intro: exec.Skip)
next
case (Basic f)
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Basic f,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Basic f#cs,css,Normal s))}
Basic f
{t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Basic f,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Basic [THEN conseqPre]) (blast intro: exec.Basic)
next
case (Spec r)
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Spec r,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Spec r#cs,css,Normal s))}
Spec r
{t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Spec r,Normal Z⟩ ⇒ Abrupt t}"
apply (rule hoaret.Spec [THEN conseqPre])
apply (clarsimp)
apply (case_tac "∃t. (Z,t) ∈ r")
apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
done
next
case (Seq c1 c2)
have hyp_c1:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c1#cs,css,Normal s))}
c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
using Seq.hyps by iprover
have hyp_c2:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c2#cs,css,Normal s))}
c2
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
using Seq.hyps by iprover
have c1: "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Seq c1 c2#cs,css,Normal s))}
c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t ∧
Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c2#cs,css,Normal t))},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
assume "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c1,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (blast dest: Seq_NoFaultStuckD1)
next
fix cs css
assume "Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Seq c1 c2 # cs,css,Normal Z)"
thus "∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c1 # cs,css, Normal Z)"
by (blast intro: rtranclp_into_tranclp1 [THEN tranclp_into_rtranclp]
step.Seq)
next
fix t
assume "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨c2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (blast dest: Seq_NoFaultStuckD2)
next
fix cs css t
assume "Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Seq c1 c2#cs,css,Normal Z)"
also have "Γ⊢(Seq c1 c2 # cs,css,Normal Z) → (c1#c2#cs,css,Normal Z)"
by (rule step.Seq)
also assume "Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t"
hence "Γ⊢ (c1#c2#cs,css,Normal Z) →⇧* (c2#cs,css,Normal t)"
by (rule exec_impl_steps)
finally
show "∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c2 # cs,css, Normal t)"
by iprover
next
fix t
assume "Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t"
by (blast intro: exec.intros)
qed
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Seq c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Seq c1 c2#cs,css,Normal s))}
Seq c1 c2
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Seq c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Seq [OF c1 ConseqMGT [OF hyp_c2]])
(blast intro: exec.intros)
next
case (Cond b c1 c2)
have hyp_c1:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[], Normal σ) →⇧* (c1#cs,css,Normal s))}
c1
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t}"
using Cond.hyps by iprover
have
"Γ,Θ⊢⇩t⇘/F⇙ ({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Cond b c1 c2#cs,css,Normal s))}
∩ b)
c1
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c1],safe)
assume "Z ∈ b" "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c1,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.CondTrue)
next
fix cs css
assume "Z ∈ b"
"Γ⊢([the (Γ p)],[], Normal σ) →⇧* (Cond b c1 c2 # cs,css, Normal Z)"
thus "∃cs css. Γ⊢([the (Γ p)],[], Normal σ) →⇧* (c1 # cs,css, Normal Z)"
by (blast intro: rtranclp_into_tranclp1 [THEN tranclp_into_rtranclp]
step.CondTrue)
next
fix t assume "Z ∈ b" "Γ⊢⟨c1,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t"
by (blast intro: exec.CondTrue)
next
fix t assume "Z ∈ b" "Γ⊢⟨c1,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t"
by (blast intro: exec.CondTrue)
qed
moreover
have hyp_c2:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c2#cs,css,Normal s))}
c2
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t}"
using Cond.hyps by iprover
have
"Γ,Θ⊢⇩t⇘/F⇙ ({s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧*(Cond b c1 c2#cs,css, Normal s))}
∩ -b)
c2
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c2],safe)
assume "Z ∉ b" "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.CondFalse)
next
fix cs css
assume "Z ∉ b"
"Γ⊢([the (Γ p)],[], Normal σ) →⇧* (Cond b c1 c2 # cs,css, Normal Z)"
thus "∃cs css. Γ⊢([the (Γ p)],[], Normal σ) →⇧* (c2 # cs,css,Normal Z)"
by (blast intro: rtranclp_into_tranclp1 [THEN tranclp_into_rtranclp]
step.CondFalse)
next
fix t assume "Z ∉ b" "Γ⊢⟨c2,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t"
by (blast intro: exec.CondFalse)
next
fix t assume "Z ∉ b" "Γ⊢⟨c2,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t"
by (blast intro: exec.CondFalse)
qed
ultimately
show
"Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Cond b c1 c2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Cond b c1 c2#cs,css,Normal s))}
(Cond b c1 c2)
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Cond b c1 c2,Normal Z⟩ ⇒ Abrupt t}"
by (rule hoaret.Cond)
next
case (While b c)
let ?unroll = "({(s,t). s∈b ∧ Γ⊢⟨c,Normal s⟩ ⇒ Normal t})⇧*"
let ?P' = "λZ. {t. (Z,t)∈?unroll ∧
(∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧*
(While b c#cs,css,Normal t))}"
let ?A = "λZ. {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
let ?r = "{(t,s). Γ⊢(While b c)↓Normal s ∧ s∈b ∧
Γ⊢⟨c,Normal s⟩ ⇒ Normal t}"
show "Γ,Θ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨While b c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ)→⇧*(While b c#cs,css,Normal s))}
(While b c)
{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [where ?P'="λ Z. ?P' Z"
and ?Q'="λ Z. ?P' Z ∩ - b"])
have wf_r: "wf ?r" by (rule wf_terminates_while)
show "∀ Z. Γ,Θ⊢⇩t⇘/F⇙ (?P' Z) (While b c) (?P' Z ∩ - b),(?A Z)"
proof (rule allI, rule hoaret.While [OF wf_r])
fix Z
from While
have hyp_c: "∀Z. Γ,Θ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c # cs,css,Normal s))}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}" by iprover
show "∀σ. Γ,Θ⊢⇩t⇘/F⇙ ({σ} ∩ ?P' Z ∩ b) c
({t. (t, σ) ∈ ?r} ∩ ?P' Z),(?A Z)"
proof (rule allI, rule ConseqMGT [OF hyp_c])
fix τ s
assume asm: "s∈ {τ} ∩
{t. (Z, t) ∈ ?unroll ∧
(∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)) ∧
Γ⊢the (Γ p)↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧*
(While b c#cs,css,Normal t))}
∩ b"
then obtain cs css where
s_eq_τ: "s=τ" and
Z_s_unroll: "(Z,s) ∈ ?unroll" and
noabort:"∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)" and
termi: "Γ⊢the (Γ p) ↓ Normal σ" and
reach: "Γ⊢([the (Γ p)],[],Normal σ) →⇧*
(While b c#cs,css,Normal s)"and
s_in_b: "s∈b"
by blast
have reach_c:
"Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c#While b c#cs,css,Normal s)"
proof -
note reach
also from s_in_b
have "Γ⊢(While b c#cs,css,Normal s)→
(c#While b c#cs,css,Normal s)"
by (rule step.WhileTrue)
finally
show ?thesis .
qed
from reach termi have
termi_while: "Γ⊢While b c ↓ Normal s"
by (rule steps_preserves_termination)
show "s ∈ {t. t = s ∧ Γ⊢⟨c,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c#cs,css,Normal t))} ∧
(∀t. t ∈ {t. Γ⊢⟨c,Normal s⟩ ⇒ Normal t} ⟶
t ∈ {t. (t,τ) ∈ ?r} ∩
{t. (Z, t) ∈ ?unroll ∧
(∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧*
(While b c # cs,css,Normal t))}) ∧
(∀t. t ∈ {t. Γ⊢⟨c,Normal s⟩ ⇒ Abrupt t} ⟶
t ∈ {t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t})"
(is "?C1 ∧ ?C2 ∧ ?C3")
proof (intro conjI)
from Z_s_unroll noabort s_in_b termi reach_c show ?C1
by blast
next
{
fix t
assume s_t: "Γ⊢⟨c,Normal s⟩ ⇒ Normal t"
with s_eq_τ termi_while s_in_b have "(t,τ) ∈ ?r"
by blast
moreover
from Z_s_unroll s_t s_in_b
have "(Z, t) ∈ ?unroll"
by (blast intro: rtrancl_into_rtrancl)
moreover
have "Γ⊢([the (Γ p)],[],Normal σ) →⇧* (While b c#cs,css,Normal t)"
proof -
note reach_c
also from s_t
have "Γ⊢(c#While b c#cs,css,Normal s)→⇧*
(While b c#cs,css, Normal t)"
by (rule exec_impl_steps)
finally show ?thesis .
qed
moreover note noabort termi
ultimately
have "(t,τ) ∈ ?r ∧ (Z, t) ∈ ?unroll ∧
(∀e. (Z,e)∈?unroll ⟶ e∈b
⟶ Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧*
(While b c # cs,css, Normal t))"
by iprover
}
then show ?C2 by blast
next
{
fix t
assume s_t: "Γ⊢⟨c,Normal s⟩ ⇒ Abrupt t"
from Z_s_unroll noabort s_t s_in_b
have "Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt t"
by blast
} thus ?C3 by simp
qed
qed
qed
next
fix s
assume P: "s ∈ {s. s=Z ∧ Γ⊢⟨While b c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧*
(While b c#cs,css,Normal s))}"
hence WhileNoFault: "Γ⊢⟨While b c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by auto
show "s ∈ ?P' s ∧
(∀t. t∈(?P' s ∩ - b)⟶
t∈{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t})∧
(∀t. t∈?A s ⟶ t∈?A Z)"
proof (intro conjI)
{
fix e
assume "(Z,e) ∈ ?unroll" "e ∈ b"
from this WhileNoFault
have "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
(∀u. Γ⊢⟨c,Normal e⟩ ⇒Abrupt u ⟶
Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u)" (is "?Prop Z e")
proof (induct rule: converse_rtrancl_induct [consumes 1])
assume e_in_b: "e ∈ b"
assume WhileNoFault: "Γ⊢⟨While b c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
with e_in_b WhileNoFault
have cNoFault: "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.intros)
moreover
{
fix u assume "Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u"
with e_in_b have "Γ⊢⟨While b c,Normal e⟩ ⇒ Abrupt u"
by (blast intro: exec.intros)
}
ultimately
show "?Prop e e"
by iprover
next
fix Z r
assume e_in_b: "e∈b"
assume WhileNoFault: "Γ⊢⟨While b c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
assume hyp: "⟦e∈b;Γ⊢⟨While b c,Normal r⟩ ⇒∉({Stuck} ∪ Fault ` (-F))⟧
⟹ ?Prop r e"
assume Z_r:
"(Z, r) ∈ {(Z, r). Z ∈ b ∧ Γ⊢⟨c,Normal Z⟩ ⇒ Normal r}"
with WhileNoFault
have "Γ⊢⟨While b c,Normal r⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.intros)
from hyp [OF e_in_b this] obtain
cNoFault: "Γ⊢⟨c,Normal e⟩ ⇒∉({Stuck} ∪ Fault ` (-F))" and
Abrupt_r: "∀u. Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u ⟶
Γ⊢⟨While b c,Normal r⟩ ⇒ Abrupt u"
by simp
{
fix u assume "Γ⊢⟨c,Normal e⟩ ⇒ Abrupt u"
with Abrupt_r have "Γ⊢⟨While b c,Normal r⟩ ⇒ Abrupt u" by simp
moreover from Z_r obtain
"Z ∈ b" "Γ⊢⟨c,Normal Z⟩ ⇒ Normal r"
by simp
ultimately have "Γ⊢⟨While b c,Normal Z⟩ ⇒ Abrupt u"
by (blast intro: exec.intros)
}
with cNoFault show "?Prop Z e"
by iprover
qed
}
with P show "s ∈ ?P' s"
by blast
next
{
fix t
assume "termination": "t ∉ b"
assume "(Z, t) ∈ ?unroll"
hence "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
proof (induct rule: converse_rtrancl_induct [consumes 1])
from "termination"
show "Γ⊢⟨While b c,Normal t⟩ ⇒ Normal t"
by (blast intro: exec.WhileFalse)
next
fix Z r
assume first_body:
"(Z, r) ∈ {(s, t). s ∈ b ∧ Γ⊢⟨c,Normal s⟩ ⇒ Normal t}"
assume "(r, t) ∈ ?unroll"
assume rest_loop: "Γ⊢⟨While b c, Normal r⟩ ⇒ Normal t"
show "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
proof -
from first_body obtain
"Z ∈ b" "Γ⊢⟨c,Normal Z⟩ ⇒ Normal r"
by fast
moreover
from rest_loop have
"Γ⊢⟨While b c,Normal r⟩ ⇒ Normal t"
by fast
ultimately show "Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t"
by (rule exec.WhileTrue)
qed
qed
}
with P
show "∀t. t∈(?P' s ∩ - b)
⟶t∈{t. Γ⊢⟨While b c,Normal Z⟩ ⇒ Normal t}"
by blast
next
from P show "∀t. t∈?A s ⟶ t∈?A Z"
by simp
qed
qed
next
case (Call q)
let ?P = "{s. s=Z ∧ Γ⊢⟨Call q ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧*
(Call q # cs,css,Normal s))}"
from noStuck_Call
have "∀s ∈ ?P. q ∈ dom Γ"
by (fastforce simp add: final_notin_def)
then show ?case
proof (rule conseq_extract_state_indep_prop)
assume q_defined: "q ∈ dom Γ"
from Call_hyp have
"∀q∈dom Γ. ∀Z.
Γ,Θ⊢⇩t⇘/F⇙{s. s=Z ∧ Γ⊢⟨the (Γ q),Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(the (Γ q))↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨the (Γ q),Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨the (Γ q),Normal Z⟩ ⇒ Abrupt t}"
by (simp add: exec_Call_body' noFaultStuck_Call_body' [simplified]
terminates_Normal_Call_body)
from Call_hyp q_defined have Call_hyp':
"∀Z. Γ,Θ ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
by auto
show
"Γ,Θ⊢⇩t⇘/F⇙ ?P
(Call q)
{t. Γ⊢⟨Call q ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q ,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF Call_hyp'],safe)
fix cs css
assume
"Γ⊢([the (Γ p)],[],Normal σ)→⇧* (Call q # cs,css,Normal Z)"
"Γ⊢the (Γ p) ↓ Normal σ"
hence "Γ⊢Call q ↓ Normal Z"
by (rule steps_preserves_termination)
with q_defined show "Γ⊢Call q ↓ Normal Z"
by (auto elim: terminates_Normal_elim_cases)
next
fix cs css
assume reach:
"Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Call q#cs,css,Normal Z)"
moreover have "Γ⊢(Call q # cs,css, Normal Z) →
([the (Γ q)],(cs,Throw#cs)#css, Normal Z)"
by (rule step.Call) (insert q_defined,auto)
ultimately
have "Γ⊢([the (Γ p)],[],Normal σ) →⇧+ ([the (Γ q)],(cs,Throw#cs)#css,Normal Z)"
by (rule rtranclp_into_tranclp1)
moreover
assume termi: "Γ⊢the (Γ p) ↓ Normal σ"
ultimately
show "((Z,q), σ,p) ∈ termi_call_steps Γ"
by (auto simp add: termi_call_steps_def)
qed
qed
next
case (DynCom c)
have hyp:
"⋀s'. ∀Z. Γ,Θ⊢⇩t⇘/F⇙
{s. s = Z ∧ Γ⊢⟨c s',Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c s'#cs,css,Normal s))}
(c s')
{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c s',Normal Z⟩ ⇒ Abrupt t}"
using DynCom by simp
have hyp':
"Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨DynCom c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (DynCom c#cs,css,Normal s))}
(c Z)
{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp],safe)
assume "Γ⊢⟨DynCom c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
then show "Γ⊢⟨c Z,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (fastforce simp add: final_notin_def intro: exec.intros)
next
fix cs css
assume "Γ⊢([the (Γ p)], [], Normal σ) →⇧* (DynCom c # cs, css, Normal Z)"
also have "Γ⊢(DynCom c # cs, css, Normal Z) → (c Z#cs,css,Normal Z)"
by (rule step.DynCom)
finally
show "∃cs css. Γ⊢([the (Γ p)], [], Normal σ) →⇧* (c Z # cs, css, Normal Z)"
by blast
next
fix t
assume "Γ⊢⟨c Z,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Normal t"
by (auto intro: exec.intros)
next
fix t
assume "Γ⊢⟨c Z,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨DynCom c,Normal Z⟩ ⇒ Abrupt t"
by (auto intro: exec.intros)
qed
show ?case
apply (rule hoaret.DynCom)
apply safe
apply (rule hyp')
done
next
case (Guard f g c)
have hyp_c: "∀Z. Γ,Θ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨c,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c#cs,css,Normal s))}
c
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t}"
using Guard.hyps by iprover
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Guard f g c ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Guard f g c#cs,css,Normal s))}
Guard f g c
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t}"
proof (cases "f ∈ F")
case True
have "Γ,Θ⊢⇩t⇘/F⇙ (g ∩ {s. s=Z ∧
Γ⊢⟨Guard f g c ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Guard f g c#cs,css,Normal s))})
c
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c], safe)
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))" "Z∈g"
thus "Γ⊢⟨c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.intros)
next
fix cs css
assume "Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Guard f g c#cs,css,Normal Z)"
also
assume "Z ∈ g"
hence "Γ⊢(Guard f g c#cs,css,Normal Z) → (c#cs,css,Normal Z)"
by (rule step.Guard)
finally show "∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c#cs,css,Normal Z)"
by iprover
next
fix t
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c,Normal Z⟩ ⇒ Normal t" "Z ∈ g"
thus "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t"
by (auto simp add: final_notin_def intro: exec.intros )
next
fix t
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t" "Z ∈ g"
thus "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t"
by (auto simp add: final_notin_def intro: exec.intros )
qed
from True this show ?thesis
by (rule conseqPre [OF Guarantee]) auto
next
case False
have "Γ,Θ⊢⇩t⇘/F⇙ (g ∩ {s. s=Z ∧
Γ⊢⟨Guard f g c ,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Guard f g c#cs,css,Normal s))})
c
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t}"
proof (rule ConseqMGT [OF hyp_c], safe)
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
using False
by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros)
next
fix cs css
assume "Γ⊢([the (Γ p)],[],Normal σ) →⇧* (Guard f g c#cs,css,Normal Z)"
also assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
hence "Z ∈ g"
using False by (auto simp add: final_notin_def intro: exec.GuardFault)
hence "Γ⊢(Guard f g c#cs,css,Normal Z) → (c#cs,css,Normal Z)"
by (rule step.Guard)
finally show "∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c#cs,css,Normal Z)"
by iprover
next
fix t
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Normal t"
using False
by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros )
next
fix t
assume "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨Guard f g c ,Normal Z⟩ ⇒ Abrupt t"
using False
by (cases "Z∈ g") (auto simp add: final_notin_def intro: exec.intros )
qed
then show ?thesis
apply (rule conseqPre [OF hoaret.Guard])
apply clarify
apply (frule Guard_noFaultStuckD [OF _ False])
apply auto
done
qed
next
case Throw
show "Γ,Θ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Throw,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[], Normal σ) →⇧* (Throw#cs,css,Normal s))}
Throw
{t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Throw,Normal Z⟩ ⇒ Abrupt t}"
by (rule conseqPre [OF hoaret.Throw])
(blast intro: exec.intros terminates.intros)
next
case (Catch c⇩1 c⇩2)
have hyp_c1:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s= Z ∧ Γ⊢⟨c⇩1,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c⇩1# cs, css,Normal s))}
c⇩1
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t}"
using Catch.hyps by iprover
have hyp_c2:
"∀Z. Γ,Θ⊢⇩t⇘/F⇙ {s. s= Z ∧ Γ⊢⟨c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c⇩2# cs, css,Normal s))}
c⇩2
{t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Normal t},{t. Γ⊢⟨c⇩2,Normal Z⟩ ⇒ Abrupt t}"
using Catch.hyps by iprover
have
"Γ,Θ⊢⇩t⇘/F⇙ {s. s = Z ∧ Γ⊢⟨Catch c⇩1 c⇩2,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ)→⇧*(Catch c⇩1 c⇩2 #cs,css,Normal s))}
c⇩1
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t ∧
Γ⊢⟨c⇩2,Normal t⟩ ⇒∉({Stuck} ∪ Fault`(-F)) ∧ Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c⇩2# cs, css,Normal t))}"
proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
assume "Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
thus "Γ⊢⟨c⇩1,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (fastforce simp add: final_notin_def intro: exec.intros)
next
fix cs css
assume "Γ⊢([the (Γ p)], [], Normal σ) →⇧* (Catch c⇩1 c⇩2 # cs, css, Normal Z)"
also have
"Γ⊢(Catch c⇩1 c⇩2 # cs, css, Normal Z) → ([c⇩1],(cs,c⇩2#cs)#css,Normal Z)"
by (rule step.Catch)
finally
show "∃cs css. Γ⊢([the (Γ p)], [], Normal σ) →⇧* (c⇩1 # cs, css, Normal Z)"
by iprover
next
fix t
assume "Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Normal t"
thus "Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t"
by (auto intro: exec.intros)
next
fix t
assume "Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
"Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t"
thus "Γ⊢⟨c⇩2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F))"
by (auto simp add: final_notin_def intro: exec.intros)
next
fix cs css t
assume "Γ⊢([the (Γ p)], [], Normal σ) →⇧* (Catch c⇩1 c⇩2 # cs, css, Normal Z)"
also have
"Γ⊢(Catch c⇩1 c⇩2 # cs, css, Normal Z) → ([c⇩1],(cs,c⇩2#cs)#css,Normal Z)"
by (rule step.Catch)
also
assume "Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t"
hence "Γ⊢([c⇩1],(cs,c⇩2#cs)#css,Normal Z) →⇧* ([],(cs,c⇩2#cs)#css,Abrupt t)"
by (rule exec_impl_steps)
also
have "Γ⊢([],(cs,c⇩2#cs)#css,Abrupt t) → (c⇩2#cs,css,Normal t)"
by (rule step.intros)
finally
show "∃cs css. Γ⊢([the (Γ p)], [], Normal σ) →⇧* (c⇩2 # cs, css, Normal t)"
by iprover
qed
moreover
have "Γ,Θ⊢⇩t⇘/F⇙ {t. Γ⊢⟨c⇩1,Normal Z⟩ ⇒ Abrupt t ∧
Γ⊢⟨c⇩2,Normal t⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p) ↓ Normal σ ∧
(∃cs css. Γ⊢([the (Γ p)],[],Normal σ) →⇧* (c⇩2# cs, css,Normal t))}
c⇩2
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Catch c⇩1 c⇩2,Normal Z⟩ ⇒ Abrupt t}"
by (rule ConseqMGT [OF hyp_c2]) (fastforce intro: exec.intros)
ultimately show ?case
by (rule hoaret.Catch)
qed
text ‹To prove a procedure implementation correct it suffices to assume
only the procedure specifications of procedures that actually
occur during evaluation of the body.
›
lemma Call_lemma:
assumes
Call: "∀q ∈ dom Γ. ∀Z. Γ,Θ ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
shows "⋀Z. Γ,Θ ⊢⇩t⇘/F⇙
({σ} ∩ {s. s=Z ∧ Γ⊢⟨the (Γ p),Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal s})
the (Γ p)
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Abrupt t}"
apply (rule conseqPre)
apply (rule Call_lemma')
apply (rule Call)
apply blast
done
lemma Call_lemma_switch_Call_body:
assumes
call: "∀q ∈ dom Γ. ∀Z. Γ,Θ ⊢⇩t⇘/F⇙
{s. s=Z ∧ Γ⊢⟨Call q,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call q↓Normal s ∧ ((s,q),(σ,p)) ∈ termi_call_steps Γ}
(Call q)
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call q,Normal Z⟩ ⇒ Abrupt t}"
assumes p_defined: "p ∈ dom Γ"
shows "⋀Z. Γ,Θ ⊢⇩t⇘/F⇙
({σ} ∩ {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s})
the (Γ p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
apply (simp only: exec_Call_body' [OF p_defined] noFaultStuck_Call_body' [OF p_defined] terminates_Normal_Call_body [OF p_defined])
apply (rule conseqPre)
apply (rule Call_lemma')
apply (rule call)
apply blast
done
lemma MGT_Call:
"∀p ∈ dom Γ. ∀Z.
Γ,Θ ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(Call p)↓Normal s}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
apply (intro ballI allI)
apply (rule CallRec' [where Procs="dom Γ" and
P="λp Z. {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s}" and
Q="λp Z. {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t}" and
A="λp Z. {t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}" and
r="termi_call_steps Γ"
])
apply simp
apply simp
apply (rule wf_termi_call_steps)
apply (intro ballI allI)
apply simp
apply (rule Call_lemma_switch_Call_body [rule_format, simplified])
apply (rule hoaret.Asm)
apply fastforce
apply assumption
done
lemma CollInt_iff: "{s. P s} ∩ {s. Q s} = {s. P s ∧ Q s}"
by auto
lemma image_Un_conv: "f ` (⋃p∈dom Γ. ⋃Z. {x p Z}) = (⋃p∈dom Γ. ⋃Z. {f (x p Z)})"
by (auto iff: not_None_eq)
text ‹Another proof of ‹MGT_Call›, maybe a little more readable›
lemma
"∀p ∈ dom Γ. ∀Z.
Γ,{} ⊢⇩t⇘/F⇙ {s. s=Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢(Call p)↓Normal s}
(Call p)
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
proof -
{
fix p Z σ
assume defined: "p ∈ dom Γ"
define Specs where "Specs = (⋃p∈dom Γ. ⋃Z.
{({s. s=Z ∧
Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s},
p,
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t})})"
define Specs_wf where "Specs_wf p σ = (λ(P,q,Q,A).
(P ∩ {s. ((s,q),σ,p) ∈ termi_call_steps Γ}, q, Q, A)) ` Specs" for p σ
have "Γ,Specs_wf p σ
⊢⇩t⇘/F⇙({σ} ∩
{s. s = Z ∧ Γ⊢⟨the (Γ p),Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢the (Γ p)↓Normal s})
(the (Γ p))
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨the (Γ p),Normal Z⟩ ⇒ Abrupt t}"
apply (rule Call_lemma [rule_format])
apply (rule hoaret.Asm)
apply (clarsimp simp add: Specs_wf_def Specs_def image_Un_conv)
apply (rule_tac x=q in bexI)
apply (rule_tac x=Z in exI)
apply (clarsimp simp add: CollInt_iff)
apply auto
done
hence "Γ,Specs_wf p σ
⊢⇩t⇘/F⇙({σ} ∩
{s. s = Z ∧ Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s})
(the (Γ p))
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t}"
by (simp only: exec_Call_body' [OF defined]
noFaultStuck_Call_body' [OF defined]
terminates_Normal_Call_body [OF defined])
} note bdy=this
show ?thesis
apply (intro ballI allI)
apply (rule hoaret.CallRec [where Specs="(⋃p∈dom Γ. ⋃Z.
{({s. s=Z ∧
Γ⊢⟨Call p,Normal s⟩ ⇒∉({Stuck} ∪ Fault ` (-F)) ∧
Γ⊢Call p↓Normal s},
p,
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Normal t},
{t. Γ⊢⟨Call p,Normal Z⟩ ⇒ Abrupt t})})",
OF _ wf_termi_call_steps [of Γ] refl])
apply fastforce
apply clarify
apply (rule conjI)
apply fastforce
apply (rule allI)
apply (simp (no_asm_use) only : Un_empty_left)
apply (rule bdy)
apply auto
done
qed
end