section {* Small-Step Semantics and Infinite Computations*}
theory SmallStep imports Termination
begin
text {* The redex of a statement is the substatement, which is actually altered
by the next step in the small-step semantics.
*}
primrec redex:: "('s,'p,'f)com ⇒ ('s,'p,'f)com"
where
"redex Skip = Skip" |
"redex (Basic f) = (Basic f)" |
"redex (Spec r) = (Spec r)" |
"redex (Seq c⇩1 c⇩2) = redex c⇩1" |
"redex (Cond b c⇩1 c⇩2) = (Cond b c⇩1 c⇩2)" |
"redex (While b c) = (While b c)" |
"redex (Call p) = (Call p)" |
"redex (DynCom d) = (DynCom d)" |
"redex (Guard f b c) = (Guard f b c)" |
"redex (Throw) = Throw" |
"redex (Catch c⇩1 c⇩2) = redex c⇩1"
subsection {*Small-Step Computation: @{text "Γ⊢(c, s) → (c', s')"}*}
type_synonym ('s,'p,'f) config = "('s,'p,'f)com × ('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
Basic: "Γ⊢(Basic f,Normal s) → (Skip,Normal (f s))"
| Spec: "(s,t) ∈ r ⟹ Γ⊢(Spec r,Normal s) → (Skip,Normal t)"
| SpecStuck: "∀t. (s,t) ∉ r ⟹ Γ⊢(Spec r,Normal s) → (Skip,Stuck)"
| Guard: "s∈g ⟹ Γ⊢(Guard f g c,Normal s) → (c,Normal s)"
| GuardFault: "s∉g ⟹ Γ⊢(Guard f g c,Normal s) → (Skip,Fault f)"
| Seq: "Γ⊢(c⇩1,s) → (c⇩1',s')
⟹
Γ⊢(Seq c⇩1 c⇩2,s) → (Seq c⇩1' c⇩2, s')"
| SeqSkip: "Γ⊢(Seq Skip c⇩2,s) → (c⇩2, s)"
| SeqThrow: "Γ⊢(Seq Throw c⇩2,Normal s) → (Throw, Normal s)"
| CondTrue: "s∈b ⟹ Γ⊢(Cond b c⇩1 c⇩2,Normal s) → (c⇩1,Normal s)"
| CondFalse: "s∉b ⟹ Γ⊢(Cond b c⇩1 c⇩2,Normal s) → (c⇩2,Normal s)"
| WhileTrue: "⟦s∈b⟧
⟹
Γ⊢(While b c,Normal s) → (Seq c (While b c),Normal s)"
| WhileFalse: "⟦s∉b⟧
⟹
Γ⊢(While b c,Normal s) → (Skip,Normal s)"
| Call: "Γ p=Some bdy ⟹
Γ⊢(Call p,Normal s) → (bdy,Normal s)"
| CallUndefined: "Γ p=None ⟹
Γ⊢(Call p,Normal s) → (Skip,Stuck)"
| DynCom: "Γ⊢(DynCom c,Normal s) → (c s,Normal s)"
| Catch: "⟦Γ⊢(c⇩1,s) → (c⇩1',s')⟧
⟹
Γ⊢(Catch c⇩1 c⇩2,s) → (Catch c⇩1' c⇩2,s')"
| CatchThrow: "Γ⊢(Catch Throw c⇩2,Normal s) → (c⇩2,Normal s)"
| CatchSkip: "Γ⊢(Catch Skip c⇩2,s) → (Skip,s)"
| FaultProp: "⟦c≠Skip; redex c = c⟧ ⟹ Γ⊢(c,Fault f) → (Skip,Fault f)"
| StuckProp: "⟦c≠Skip; redex c = c⟧ ⟹ Γ⊢(c,Stuck) → (Skip,Stuck)"
| AbruptProp: "⟦c≠Skip; redex c = c⟧ ⟹ Γ⊢(c,Abrupt f) → (Skip,Abrupt f)"
lemmas step_induct = step.induct [of _ "(c,s)" "(c',s')", split_format (complete), case_names
Basic Spec SpecStuck Guard GuardFault Seq SeqSkip SeqThrow CondTrue CondFalse
WhileTrue WhileFalse Call CallUndefined DynCom Catch CatchThrow CatchSkip
FaultProp StuckProp AbruptProp, induct set]
inductive_cases step_elim_cases [cases set]:
"Γ⊢(Skip,s) → u"
"Γ⊢(Guard f g c,s) → u"
"Γ⊢(Basic f,s) → u"
"Γ⊢(Spec r,s) → u"
"Γ⊢(Seq c1 c2,s) → u"
"Γ⊢(Cond b c1 c2,s) → u"
"Γ⊢(While b c,s) → u"
"Γ⊢(Call p,s) → u"
"Γ⊢(DynCom c,s) → u"
"Γ⊢(Throw,s) → u"
"Γ⊢(Catch c1 c2,s) → u"
inductive_cases step_Normal_elim_cases [cases set]:
"Γ⊢(Skip,Normal s) → u"
"Γ⊢(Guard f g c,Normal s) → u"
"Γ⊢(Basic f,Normal s) → u"
"Γ⊢(Spec r,Normal s) → u"
"Γ⊢(Seq c1 c2,Normal s) → u"
"Γ⊢(Cond b c1 c2,Normal s) → u"
"Γ⊢(While b c,Normal s) → u"
"Γ⊢(Call p,Normal s) → u"
"Γ⊢(DynCom c,Normal s) → u"
"Γ⊢(Throw,Normal s) → u"
"Γ⊢(Catch c1 c2,Normal s) → u"
text {* The final configuration is either of the form @{text "(Skip,_)"} for normal
termination, or @{term "(Throw,Normal s)"} in case the program was started in
a @{term "Normal"} state and terminated abruptly. The @{const "Abrupt"} state is not used to
model abrupt termination, in contrast to the big-step semantics. Only if the
program starts in an @{const "Abrupt"} states it ends in the same @{term "Abrupt"}
state.*}
definition final:: "('s,'p,'f) config ⇒ bool" where
"final cfg = (fst cfg=Skip ∨ (fst cfg=Throw ∧ (∃s. snd cfg=Normal s)))"
abbreviation
"step_rtrancl" :: "[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] ⇒ bool"
("_⊢ (_ →⇧*/ _)" [81,81,81] 100)
where
"Γ⊢cf0 →⇧* cf1 ≡ (CONST step Γ)⇧*⇧* cf0 cf1"
abbreviation
"step_trancl" :: "[('s,'p,'f) body,('s,'p,'f) config,('s,'p,'f) config] ⇒ bool"
("_⊢ (_ →⇧+/ _)" [81,81,81] 100)
where
"Γ⊢cf0 →⇧+ cf1 ≡ (CONST step Γ)⇧+⇧+ cf0 cf1"
subsection {* Structural Properties of Small Step Computations *}
lemma redex_not_Seq: "redex c = Seq c1 c2 ⟹ P"
apply (induct c)
apply auto
done
lemma no_step_final:
assumes step: "Γ⊢(c,s) → (c',s')"
shows "final (c,s) ⟹ P"
using step
by induct (auto simp add: final_def)
lemma no_step_final':
assumes step: "Γ⊢cfg → cfg'"
shows "final cfg ⟹ P"
using step
by (cases cfg, cases cfg') (auto intro: no_step_final)
lemma step_Abrupt:
assumes step: "Γ⊢ (c, s) → (c', s')"
shows "⋀x. s=Abrupt x ⟹ s'=Abrupt x"
using step
by (induct) auto
lemma step_Fault:
assumes step: "Γ⊢ (c, s) → (c', s')"
shows "⋀f. s=Fault f ⟹ s'=Fault f"
using step
by (induct) auto
lemma step_Stuck:
assumes step: "Γ⊢ (c, s) → (c', s')"
shows "⋀f. s=Stuck ⟹ s'=Stuck"
using step
by (induct) auto
lemma SeqSteps:
assumes steps: "Γ⊢cfg⇩1→⇧* cfg⇩2"
shows "⋀ c⇩1 s c⇩1' s'. ⟦cfg⇩1 = (c⇩1,s);cfg⇩2=(c⇩1',s')⟧
⟹ Γ⊢(Seq c⇩1 c⇩2,s) →⇧* (Seq c⇩1' c⇩2, s')"
using steps
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
case Refl
thus ?case
by simp
next
case (Trans cfg⇩1 cfg'')
have step: "Γ⊢ cfg⇩1 → cfg''" by fact
have steps: "Γ⊢ cfg'' →⇧* cfg⇩2" by fact
have cfg⇩1: "cfg⇩1 = (c⇩1, s)" and cfg⇩2: "cfg⇩2 = (c⇩1', s')" by fact+
obtain c⇩1'' s'' where cfg'': "cfg''=(c⇩1'',s'')"
by (cases cfg'') auto
from step cfg⇩1 cfg''
have "Γ⊢ (c⇩1,s) → (c⇩1'',s'')"
by simp
hence "Γ⊢ (Seq c⇩1 c⇩2,s) → (Seq c⇩1'' c⇩2,s'')"
by (rule step.Seq)
also from Trans.hyps (3) [OF cfg'' cfg⇩2]
have "Γ⊢ (Seq c⇩1'' c⇩2, s'') →⇧* (Seq c⇩1' c⇩2, s')" .
finally show ?case .
qed
lemma CatchSteps:
assumes steps: "Γ⊢cfg⇩1→⇧* cfg⇩2"
shows "⋀ c⇩1 s c⇩1' s'. ⟦cfg⇩1 = (c⇩1,s); cfg⇩2=(c⇩1',s')⟧
⟹ Γ⊢(Catch c⇩1 c⇩2,s) →⇧* (Catch c⇩1' c⇩2, s')"
using steps
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
case Refl
thus ?case
by simp
next
case (Trans cfg⇩1 cfg'')
have step: "Γ⊢ cfg⇩1 → cfg''" by fact
have steps: "Γ⊢ cfg'' →⇧* cfg⇩2" by fact
have cfg⇩1: "cfg⇩1 = (c⇩1, s)" and cfg⇩2: "cfg⇩2 = (c⇩1', s')" by fact+
obtain c⇩1'' s'' where cfg'': "cfg''=(c⇩1'',s'')"
by (cases cfg'') auto
from step cfg⇩1 cfg''
have s: "Γ⊢ (c⇩1,s) → (c⇩1'',s'')"
by simp
hence "Γ⊢ (Catch c⇩1 c⇩2,s) → (Catch c⇩1'' c⇩2,s'')"
by (rule step.Catch)
also from Trans.hyps (3) [OF cfg'' cfg⇩2]
have "Γ⊢ (Catch c⇩1'' c⇩2, s'') →⇧* (Catch c⇩1' c⇩2, s')" .
finally show ?case .
qed
lemma steps_Fault: "Γ⊢ (c, Fault f) →⇧* (Skip, Fault f)"
proof (induct c)
case (Seq c⇩1 c⇩2)
have steps_c⇩1: "Γ⊢ (c⇩1, Fault f) →⇧* (Skip, Fault f)" by fact
have steps_c⇩2: "Γ⊢ (c⇩2, Fault f) →⇧* (Skip, Fault f)" by fact
from SeqSteps [OF steps_c⇩1 refl refl]
have "Γ⊢ (Seq c⇩1 c⇩2, Fault f) →⇧* (Seq Skip c⇩2, Fault f)".
also
have "Γ⊢ (Seq Skip c⇩2, Fault f) → (c⇩2, Fault f)" by (rule SeqSkip)
also note steps_c⇩2
finally show ?case by simp
next
case (Catch c⇩1 c⇩2)
have steps_c⇩1: "Γ⊢ (c⇩1, Fault f) →⇧* (Skip, Fault f)" by fact
from CatchSteps [OF steps_c⇩1 refl refl]
have "Γ⊢ (Catch c⇩1 c⇩2, Fault f) →⇧* (Catch Skip c⇩2, Fault f)".
also
have "Γ⊢ (Catch Skip c⇩2, Fault f) → (Skip, Fault f)" by (rule CatchSkip)
finally show ?case by simp
qed (fastforce intro: step.intros)+
lemma steps_Stuck: "Γ⊢ (c, Stuck) →⇧* (Skip, Stuck)"
proof (induct c)
case (Seq c⇩1 c⇩2)
have steps_c⇩1: "Γ⊢ (c⇩1, Stuck) →⇧* (Skip, Stuck)" by fact
have steps_c⇩2: "Γ⊢ (c⇩2, Stuck) →⇧* (Skip, Stuck)" by fact
from SeqSteps [OF steps_c⇩1 refl refl]
have "Γ⊢ (Seq c⇩1 c⇩2, Stuck) →⇧* (Seq Skip c⇩2, Stuck)".
also
have "Γ⊢ (Seq Skip c⇩2, Stuck) → (c⇩2, Stuck)" by (rule SeqSkip)
also note steps_c⇩2
finally show ?case by simp
next
case (Catch c⇩1 c⇩2)
have steps_c⇩1: "Γ⊢ (c⇩1, Stuck) →⇧* (Skip, Stuck)" by fact
from CatchSteps [OF steps_c⇩1 refl refl]
have "Γ⊢ (Catch c⇩1 c⇩2, Stuck) →⇧* (Catch Skip c⇩2, Stuck)" .
also
have "Γ⊢ (Catch Skip c⇩2, Stuck) → (Skip, Stuck)" by (rule CatchSkip)
finally show ?case by simp
qed (fastforce intro: step.intros)+
lemma steps_Abrupt: "Γ⊢ (c, Abrupt s) →⇧* (Skip, Abrupt s)"
proof (induct c)
case (Seq c⇩1 c⇩2)
have steps_c⇩1: "Γ⊢ (c⇩1, Abrupt s) →⇧* (Skip, Abrupt s)" by fact
have steps_c⇩2: "Γ⊢ (c⇩2, Abrupt s) →⇧* (Skip, Abrupt s)" by fact
from SeqSteps [OF steps_c⇩1 refl refl]
have "Γ⊢ (Seq c⇩1 c⇩2, Abrupt s) →⇧* (Seq Skip c⇩2, Abrupt s)".
also
have "Γ⊢ (Seq Skip c⇩2, Abrupt s) → (c⇩2, Abrupt s)" by (rule SeqSkip)
also note steps_c⇩2
finally show ?case by simp
next
case (Catch c⇩1 c⇩2)
have steps_c⇩1: "Γ⊢ (c⇩1, Abrupt s) →⇧* (Skip, Abrupt s)" by fact
from CatchSteps [OF steps_c⇩1 refl refl]
have "Γ⊢ (Catch c⇩1 c⇩2, Abrupt s) →⇧* (Catch Skip c⇩2, Abrupt s)".
also
have "Γ⊢ (Catch Skip c⇩2, Abrupt s) → (Skip, Abrupt s)" by (rule CatchSkip)
finally show ?case by simp
qed (fastforce intro: step.intros)+
lemma step_Fault_prop:
assumes step: "Γ⊢ (c, s) → (c', s')"
shows "⋀f. s=Fault f ⟹ s'=Fault f"
using step
by (induct) auto
lemma step_Abrupt_prop:
assumes step: "Γ⊢ (c, s) → (c', s')"
shows "⋀x. s=Abrupt x ⟹ s'=Abrupt x"
using step
by (induct) auto
lemma step_Stuck_prop:
assumes step: "Γ⊢ (c, s) → (c', s')"
shows "s=Stuck ⟹ s'=Stuck"
using step
by (induct) auto
lemma steps_Fault_prop:
assumes step: "Γ⊢ (c, s) →⇧* (c', s')"
shows "s=Fault f ⟹ s'=Fault f"
using step
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl thus ?case by simp
next
case (Trans c s c'' s'')
thus ?case
by (auto intro: step_Fault_prop)
qed
lemma steps_Abrupt_prop:
assumes step: "Γ⊢ (c, s) →⇧* (c', s')"
shows "s=Abrupt t ⟹ s'=Abrupt t"
using step
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl thus ?case by simp
next
case (Trans c s c'' s'')
thus ?case
by (auto intro: step_Abrupt_prop)
qed
lemma steps_Stuck_prop:
assumes step: "Γ⊢ (c, s) →⇧* (c', s')"
shows "s=Stuck ⟹ s'=Stuck"
using step
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl thus ?case by simp
next
case (Trans c s c'' s'')
thus ?case
by (auto intro: step_Stuck_prop)
qed
subsection {* Equivalence between Small-Step and Big-Step Semantics *}
theorem exec_impl_steps:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ t"
shows "∃c' t'. Γ⊢(c,s) →⇧* (c',t') ∧
(case t of
Abrupt x ⇒ if s=t then c'=Skip ∧ t'=t else c'=Throw ∧ t'=Normal x
| _ ⇒ c'=Skip ∧ t'=t)"
using exec
proof (induct)
case Skip thus ?case
by simp
next
case Guard thus ?case by (blast intro: step.Guard rtranclp_trans)
next
case GuardFault thus ?case by (fastforce intro: step.GuardFault rtranclp_trans)
next
case FaultProp show ?case by (fastforce intro: steps_Fault)
next
case Basic thus ?case by (fastforce intro: step.Basic rtranclp_trans)
next
case Spec thus ?case by (fastforce intro: step.Spec rtranclp_trans)
next
case SpecStuck thus ?case by (fastforce intro: step.SpecStuck rtranclp_trans)
next
case (Seq c⇩1 s s' c⇩2 t)
have exec_c⇩1: "Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ s'" by fact
have exec_c⇩2: "Γ⊢ ⟨c⇩2,s'⟩ ⇒ t" by fact
show ?case
proof (cases "∃x. s'=Abrupt x")
case False
from False Seq.hyps (2)
have "Γ⊢ (c⇩1, Normal s) →⇧* (Skip, s')"
by (cases s') auto
hence seq_c⇩1: "Γ⊢ (Seq c⇩1 c⇩2, Normal s) →⇧* (Seq Skip c⇩2, s')"
by (rule SeqSteps) auto
from Seq.hyps (4) obtain c' t' where
steps_c⇩2: "Γ⊢ (c⇩2, s') →⇧* (c', t')" and
t: "(case t of
Abrupt x ⇒ if s' = t then c' = Skip ∧ t' = t
else c' = Throw ∧ t' = Normal x
| _ ⇒ c' = Skip ∧ t' = t)"
by auto
note seq_c⇩1
also have "Γ⊢ (Seq Skip c⇩2, s') → (c⇩2, s')" by (rule step.SeqSkip)
also note steps_c⇩2
finally have "Γ⊢ (Seq c⇩1 c⇩2, Normal s) →⇧* (c', t')".
with t False show ?thesis
by (cases t) auto
next
case True
then obtain x where s': "s'=Abrupt x"
by blast
from s' Seq.hyps (2)
have "Γ⊢ (c⇩1, Normal s) →⇧* (Throw, Normal x)"
by auto
hence seq_c⇩1: "Γ⊢ (Seq c⇩1 c⇩2, Normal s) →⇧* (Seq Throw c⇩2, Normal x)"
by (rule SeqSteps) auto
also have "Γ⊢ (Seq Throw c⇩2, Normal x) → (Throw, Normal x)"
by (rule SeqThrow)
finally have "Γ⊢ (Seq c⇩1 c⇩2, Normal s) →⇧* (Throw, Normal x)".
moreover
from exec_c⇩2 s' have "t=Abrupt x"
by (auto intro: Abrupt_end)
ultimately show ?thesis
by auto
qed
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 s b c s' t)
have exec_c: "Γ⊢ ⟨c,Normal s⟩ ⇒ s'" by fact
have exec_w: "Γ⊢ ⟨While b c,s'⟩ ⇒ t" by fact
have b: "s ∈ b" by fact
hence step: "Γ⊢ (While b c,Normal s) → (Seq c (While b c),Normal s)"
by (rule step.WhileTrue)
show ?case
proof (cases "∃x. s'=Abrupt x")
case False
from False WhileTrue.hyps (3)
have "Γ⊢ (c, Normal s) →⇧* (Skip, s')"
by (cases s') auto
hence seq_c: "Γ⊢ (Seq c (While b c), Normal s) →⇧* (Seq Skip (While b c), s')"
by (rule SeqSteps) auto
from WhileTrue.hyps (5) obtain c' t' where
steps_c⇩2: "Γ⊢ (While b c, s') →⇧* (c', t')" and
t: "(case t of
Abrupt x ⇒ if s' = t then c' = Skip ∧ t' = t
else c' = Throw ∧ t' = Normal x
| _ ⇒ c' = Skip ∧ t' = t)"
by auto
note step also note seq_c
also have "Γ⊢ (Seq Skip (While b c), s') → (While b c, s')"
by (rule step.SeqSkip)
also note steps_c⇩2
finally have "Γ⊢ (While b c, Normal s) →⇧* (c', t')".
with t False show ?thesis
by (cases t) auto
next
case True
then obtain x where s': "s'=Abrupt x"
by blast
note step
also
from s' WhileTrue.hyps (3)
have "Γ⊢ (c, Normal s) →⇧* (Throw, Normal x)"
by auto
hence
seq_c: "Γ⊢ (Seq c (While b c), Normal s) →⇧* (Seq Throw (While b c), Normal x)"
by (rule SeqSteps) auto
also have "Γ⊢ (Seq Throw (While b c), Normal x) → (Throw, Normal x)"
by (rule SeqThrow)
finally have "Γ⊢ (While b c, Normal s) →⇧* (Throw, Normal x)".
moreover
from exec_w s' have "t=Abrupt x"
by (auto intro: Abrupt_end)
ultimately show ?thesis
by auto
qed
next
case WhileFalse thus ?case by (fastforce intro: step.WhileFalse rtrancl_trans)
next
case Call thus ?case by (blast intro: step.Call rtranclp_trans)
next
case CallUndefined thus ?case by (fastforce intro: step.CallUndefined rtranclp_trans)
next
case StuckProp thus ?case by (fastforce intro: steps_Stuck)
next
case DynCom thus ?case by (blast intro: step.DynCom rtranclp_trans)
next
case Throw thus ?case by simp
next
case AbruptProp thus ?case by (fastforce intro: steps_Abrupt)
next
case (CatchMatch c⇩1 s s' c⇩2 t)
from CatchMatch.hyps (2)
have "Γ⊢ (c⇩1, Normal s) →⇧* (Throw, Normal s')"
by simp
hence "Γ⊢ (Catch c⇩1 c⇩2, Normal s) →⇧* (Catch Throw c⇩2, Normal s')"
by (rule CatchSteps) auto
also have "Γ⊢ (Catch Throw c⇩2, Normal s') → (c⇩2, Normal s')"
by (rule step.CatchThrow)
also
from CatchMatch.hyps (4) obtain c' t' where
steps_c⇩2: "Γ⊢ (c⇩2, Normal s') →⇧* (c', t')" and
t: "(case t of
Abrupt x ⇒ if Normal s' = t then c' = Skip ∧ t' = t
else c' = Throw ∧ t' = Normal x
| _ ⇒ c' = Skip ∧ t' = t)"
by auto
note steps_c⇩2
finally show ?case
using t
by (auto split: xstate.splits)
next
case (CatchMiss c⇩1 s t c⇩2)
have t: "¬ isAbr t" by fact
with CatchMiss.hyps (2)
have "Γ⊢ (c⇩1, Normal s) →⇧* (Skip, t)"
by (cases t) auto
hence "Γ⊢ (Catch c⇩1 c⇩2, Normal s) →⇧* (Catch Skip c⇩2, t)"
by (rule CatchSteps) auto
also
have "Γ⊢ (Catch Skip c⇩2, t) → (Skip, t)"
by (rule step.CatchSkip)
finally show ?case
using t
by (fastforce split: xstate.splits)
qed
corollary exec_impl_steps_Normal:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ Normal t"
shows "Γ⊢(c,s) →⇧* (Skip, Normal t)"
using exec_impl_steps [OF exec]
by auto
corollary exec_impl_steps_Normal_Abrupt:
assumes exec: "Γ⊢⟨c,Normal s⟩ ⇒ Abrupt t"
shows "Γ⊢(c,Normal s) →⇧* (Throw, Normal t)"
using exec_impl_steps [OF exec]
by auto
corollary exec_impl_steps_Abrupt_Abrupt:
assumes exec: "Γ⊢⟨c,Abrupt t⟩ ⇒ Abrupt t"
shows "Γ⊢(c,Abrupt t) →⇧* (Skip, Abrupt t)"
using exec_impl_steps [OF exec]
by auto
corollary exec_impl_steps_Fault:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ Fault f"
shows "Γ⊢(c,s) →⇧* (Skip, Fault f)"
using exec_impl_steps [OF exec]
by auto
corollary exec_impl_steps_Stuck:
assumes exec: "Γ⊢⟨c,s⟩ ⇒ Stuck"
shows "Γ⊢(c,s) →⇧* (Skip, Stuck)"
using exec_impl_steps [OF exec]
by auto
lemma step_Abrupt_end:
assumes step: "Γ⊢ (c⇩1, s) → (c⇩1', s')"
shows "s'=Abrupt x ⟹ s=Abrupt x"
using step
by induct auto
lemma step_Stuck_end:
assumes step: "Γ⊢ (c⇩1, s) → (c⇩1', s')"
shows "s'=Stuck ⟹
s=Stuck ∨
(∃r x. redex c⇩1 = Spec r ∧ s=Normal x ∧ (∀t. (x,t)∉r)) ∨
(∃p x. redex c⇩1=Call p ∧ s=Normal x ∧ Γ p = None)"
using step
by induct auto
lemma step_Fault_end:
assumes step: "Γ⊢ (c⇩1, s) → (c⇩1', s')"
shows "s'=Fault f ⟹
s=Fault f ∨
(∃g c x. redex c⇩1 = Guard f g c ∧ s=Normal x ∧ x ∉ g)"
using step
by induct auto
lemma exec_redex_Stuck:
"Γ⊢⟨redex c,s⟩ ⇒ Stuck ⟹ Γ⊢⟨c,s⟩ ⇒ Stuck"
proof (induct c)
case Seq
thus ?case
by (cases s) (auto intro: exec.intros elim:exec_elim_cases)
next
case Catch
thus ?case
by (cases s) (auto intro: exec.intros elim:exec_elim_cases)
qed simp_all
lemma exec_redex_Fault:
"Γ⊢⟨redex c,s⟩ ⇒ Fault f ⟹ Γ⊢⟨c,s⟩ ⇒ Fault f"
proof (induct c)
case Seq
thus ?case
by (cases s) (auto intro: exec.intros elim:exec_elim_cases)
next
case Catch
thus ?case
by (cases s) (auto intro: exec.intros elim:exec_elim_cases)
qed simp_all
lemma step_extend:
assumes step: "Γ⊢(c,s) → (c', s')"
shows "⋀t. Γ⊢⟨c',s'⟩ ⇒ t ⟹ Γ⊢⟨c,s⟩ ⇒ t"
using step
proof (induct)
case Basic thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case Spec thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case SpecStuck thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case Guard thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case GuardFault thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case (Seq c⇩1 s c⇩1' s' c⇩2)
have step: "Γ⊢ (c⇩1, s) → (c⇩1', s')" by fact
have exec': "Γ⊢ ⟨Seq c⇩1' c⇩2,s'⟩ ⇒ t" by fact
show ?case
proof (cases s)
case (Normal x)
note s_Normal = this
show ?thesis
proof (cases s')
case (Normal x')
from exec' [simplified Normal] obtain s'' where
exec_c⇩1': "Γ⊢ ⟨c⇩1',Normal x'⟩ ⇒ s''" and
exec_c⇩2: "Γ⊢ ⟨c⇩2,s''⟩ ⇒ t"
by cases
from Seq.hyps (2) Normal exec_c⇩1' s_Normal
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ s''"
by simp
from exec.Seq [OF this exec_c⇩2] s_Normal
show ?thesis by simp
next
case (Abrupt x')
with exec' have "t=Abrupt x'"
by (auto intro:Abrupt_end)
moreover
from step Abrupt
have "s=Abrupt x'"
by (auto intro: step_Abrupt_end)
ultimately
show ?thesis
by (auto intro: exec.intros)
next
case (Fault f)
from step_Fault_end [OF step this] s_Normal
obtain g c where
redex_c⇩1: "redex c⇩1 = Guard f g c" and
fail: "x ∉ g"
by auto
hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Fault f"
by (auto intro: exec.intros)
from exec_redex_Fault [OF this]
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ Fault f".
moreover from Fault exec' have "t=Fault f"
by (auto intro: Fault_end)
ultimately
show ?thesis
using s_Normal
by (auto intro: exec.intros)
next
case Stuck
from step_Stuck_end [OF step this] s_Normal
have "(∃r. redex c⇩1 = Spec r ∧ (∀t. (x, t) ∉ r)) ∨
(∃p. redex c⇩1 = Call p ∧ Γ p = None)"
by auto
moreover
{
fix r
assume "redex c⇩1 = Spec r" and "(∀t. (x, t) ∉ r)"
hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Stuck"
by (auto intro: exec.intros)
from exec_redex_Stuck [OF this]
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ Stuck".
moreover from Stuck exec' have "t=Stuck"
by (auto intro: Stuck_end)
ultimately
have ?thesis
using s_Normal
by (auto intro: exec.intros)
}
moreover
{
fix p
assume "redex c⇩1 = Call p" and "Γ p = None"
hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Stuck"
by (auto intro: exec.intros)
from exec_redex_Stuck [OF this]
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ Stuck".
moreover from Stuck exec' have "t=Stuck"
by (auto intro: Stuck_end)
ultimately
have ?thesis
using s_Normal
by (auto intro: exec.intros)
}
ultimately show ?thesis
by auto
qed
next
case (Abrupt x)
from step_Abrupt [OF step this]
have "s'=Abrupt x".
with exec'
have "t=Abrupt x"
by (auto intro: Abrupt_end)
with Abrupt
show ?thesis
by (auto intro: exec.intros)
next
case (Fault f)
from step_Fault [OF step this]
have "s'=Fault f".
with exec'
have "t=Fault f"
by (auto intro: Fault_end)
with Fault
show ?thesis
by (auto intro: exec.intros)
next
case Stuck
from step_Stuck [OF step this]
have "s'=Stuck".
with exec'
have "t=Stuck"
by (auto intro: Stuck_end)
with Stuck
show ?thesis
by (auto intro: exec.intros)
qed
next
case (SeqSkip c⇩2 s t) thus ?case
by (cases s) (fastforce intro: exec.intros elim: exec_elim_cases)+
next
case (SeqThrow c⇩2 s t) thus ?case
by (fastforce intro: exec.intros elim: exec_elim_cases)+
next
case CondTrue thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case CondFalse thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case WhileTrue thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case WhileFalse thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case Call thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case CallUndefined thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case DynCom thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case (Catch c⇩1 s c⇩1' s' c⇩2 t)
have step: "Γ⊢ (c⇩1, s) → (c⇩1', s')" by fact
have exec': "Γ⊢ ⟨Catch c⇩1' c⇩2,s'⟩ ⇒ t" by fact
show ?case
proof (cases s)
case (Normal x)
note s_Normal = this
show ?thesis
proof (cases s')
case (Normal x')
from exec' [simplified Normal]
show ?thesis
proof (cases)
fix s''
assume exec_c⇩1': "Γ⊢ ⟨c⇩1',Normal x'⟩ ⇒ Abrupt s''"
assume exec_c⇩2: "Γ⊢ ⟨c⇩2,Normal s''⟩ ⇒ t"
from Catch.hyps (2) Normal exec_c⇩1' s_Normal
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ Abrupt s''"
by simp
from exec.CatchMatch [OF this exec_c⇩2] s_Normal
show ?thesis by simp
next
assume exec_c⇩1': "Γ⊢ ⟨c⇩1',Normal x'⟩ ⇒ t"
assume t: "¬ isAbr t"
from Catch.hyps (2) Normal exec_c⇩1' s_Normal
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ t"
by simp
from exec.CatchMiss [OF this t] s_Normal
show ?thesis by simp
qed
next
case (Abrupt x')
with exec' have "t=Abrupt x'"
by (auto intro:Abrupt_end)
moreover
from step Abrupt
have "s=Abrupt x'"
by (auto intro: step_Abrupt_end)
ultimately
show ?thesis
by (auto intro: exec.intros)
next
case (Fault f)
from step_Fault_end [OF step this] s_Normal
obtain g c where
redex_c⇩1: "redex c⇩1 = Guard f g c" and
fail: "x ∉ g"
by auto
hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Fault f"
by (auto intro: exec.intros)
from exec_redex_Fault [OF this]
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ Fault f".
moreover from Fault exec' have "t=Fault f"
by (auto intro: Fault_end)
ultimately
show ?thesis
using s_Normal
by (auto intro: exec.intros)
next
case Stuck
from step_Stuck_end [OF step this] s_Normal
have "(∃r. redex c⇩1 = Spec r ∧ (∀t. (x, t) ∉ r)) ∨
(∃p. redex c⇩1 = Call p ∧ Γ p = None)"
by auto
moreover
{
fix r
assume "redex c⇩1 = Spec r" and "(∀t. (x, t) ∉ r)"
hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Stuck"
by (auto intro: exec.intros)
from exec_redex_Stuck [OF this]
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ Stuck".
moreover from Stuck exec' have "t=Stuck"
by (auto intro: Stuck_end)
ultimately
have ?thesis
using s_Normal
by (auto intro: exec.intros)
}
moreover
{
fix p
assume "redex c⇩1 = Call p" and "Γ p = None"
hence "Γ⊢ ⟨redex c⇩1,Normal x⟩ ⇒ Stuck"
by (auto intro: exec.intros)
from exec_redex_Stuck [OF this]
have "Γ⊢ ⟨c⇩1,Normal x⟩ ⇒ Stuck".
moreover from Stuck exec' have "t=Stuck"
by (auto intro: Stuck_end)
ultimately
have ?thesis
using s_Normal
by (auto intro: exec.intros)
}
ultimately show ?thesis
by auto
qed
next
case (Abrupt x)
from step_Abrupt [OF step this]
have "s'=Abrupt x".
with exec'
have "t=Abrupt x"
by (auto intro: Abrupt_end)
with Abrupt
show ?thesis
by (auto intro: exec.intros)
next
case (Fault f)
from step_Fault [OF step this]
have "s'=Fault f".
with exec'
have "t=Fault f"
by (auto intro: Fault_end)
with Fault
show ?thesis
by (auto intro: exec.intros)
next
case Stuck
from step_Stuck [OF step this]
have "s'=Stuck".
with exec'
have "t=Stuck"
by (auto intro: Stuck_end)
with Stuck
show ?thesis
by (auto intro: exec.intros)
qed
next
case CatchThrow thus ?case
by (fastforce intro: exec.intros elim: exec_Normal_elim_cases)
next
case CatchSkip thus ?case
by (fastforce intro: exec.intros elim: exec_elim_cases)
next
case FaultProp thus ?case
by (fastforce intro: exec.intros elim: exec_elim_cases)
next
case StuckProp thus ?case
by (fastforce intro: exec.intros elim: exec_elim_cases)
next
case AbruptProp thus ?case
by (fastforce intro: exec.intros elim: exec_elim_cases)
qed
theorem steps_Skip_impl_exec:
assumes steps: "Γ⊢(c,s) →⇧* (Skip,t)"
shows "Γ⊢⟨c,s⟩ ⇒ t"
using steps
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl thus ?case
by (cases t) (auto intro: exec.intros)
next
case (Trans c s c' s')
have "Γ⊢ (c, s) → (c', s')" and "Γ⊢ ⟨c',s'⟩ ⇒ t" by fact+
thus ?case
by (rule step_extend)
qed
theorem steps_Throw_impl_exec:
assumes steps: "Γ⊢(c,s) →⇧* (Throw,Normal t)"
shows "Γ⊢⟨c,s⟩ ⇒ Abrupt t"
using steps
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl thus ?case
by (auto intro: exec.intros)
next
case (Trans c s c' s')
have "Γ⊢ (c, s) → (c', s')" and "Γ⊢ ⟨c',s'⟩ ⇒ Abrupt t" by fact+
thus ?case
by (rule step_extend)
qed
subsection {* Infinite Computations: @{text "Γ⊢(c, s) → …(∞)"}*}
definition inf:: "('s,'p,'f) body ⇒ ('s,'p,'f) config ⇒ bool"
("_⊢ _ → …'(∞')" [60,80] 100) where
"Γ⊢ cfg → …(∞) ≡ (∃f. f (0::nat) = cfg ∧ (∀i. Γ⊢f i → f (i+1)))"
lemma not_infI: "⟦⋀f. ⟦f 0 = cfg; ⋀i. Γ⊢f i → f (Suc i)⟧ ⟹ False⟧
⟹ ¬Γ⊢ cfg → …(∞)"
by (auto simp add: inf_def)
subsection {* Equivalence between Termination and the Absence of Infinite Computations*}
lemma step_preserves_termination:
assumes step: "Γ⊢(c,s) → (c',s')"
shows "Γ⊢c↓s ⟹ Γ⊢c'↓s'"
using step
proof (induct)
case Basic thus ?case by (fastforce intro: terminates.intros)
next
case Spec thus ?case by (fastforce intro: terminates.intros)
next
case SpecStuck thus ?case by (fastforce intro: terminates.intros)
next
case Guard thus ?case
by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case GuardFault thus ?case by (fastforce intro: terminates.intros)
next
case (Seq c⇩1 s c⇩1' s' c⇩2) thus ?case
apply (cases s)
apply (cases s')
apply (fastforce intro: terminates.intros step_extend
elim: terminates_Normal_elim_cases)
apply (fastforce intro: terminates.intros dest: step_Abrupt_prop
step_Fault_prop step_Stuck_prop)+
done
next
case (SeqSkip c⇩2 s)
thus ?case
apply (cases s)
apply (fastforce intro: terminates.intros exec.intros
elim: terminates_Normal_elim_cases )+
done
next
case (SeqThrow c⇩2 s)
thus ?case
by (fastforce intro: terminates.intros exec.intros
elim: terminates_Normal_elim_cases )
next
case CondTrue
thus ?case
by (fastforce intro: terminates.intros exec.intros
elim: terminates_Normal_elim_cases )
next
case CondFalse
thus ?case
by (fastforce intro: terminates.intros
elim: terminates_Normal_elim_cases )
next
case WhileTrue
thus ?case
by (fastforce intro: terminates.intros
elim: terminates_Normal_elim_cases )
next
case WhileFalse
thus ?case
by (fastforce intro: terminates.intros
elim: terminates_Normal_elim_cases )
next
case Call
thus ?case
by (fastforce intro: terminates.intros
elim: terminates_Normal_elim_cases )
next
case CallUndefined
thus ?case
by (fastforce intro: terminates.intros
elim: terminates_Normal_elim_cases )
next
case DynCom
thus ?case
by (fastforce intro: terminates.intros
elim: terminates_Normal_elim_cases )
next
case (Catch c⇩1 s c⇩1' s' c⇩2) thus ?case
apply (cases s)
apply (cases s')
apply (fastforce intro: terminates.intros step_extend
elim: terminates_Normal_elim_cases)
apply (fastforce intro: terminates.intros dest: step_Abrupt_prop
step_Fault_prop step_Stuck_prop)+
done
next
case CatchThrow
thus ?case
by (fastforce intro: terminates.intros exec.intros
elim: terminates_Normal_elim_cases )
next
case (CatchSkip c⇩2 s)
thus ?case
by (cases s) (fastforce intro: terminates.intros)+
next
case FaultProp thus ?case by (fastforce intro: terminates.intros)
next
case StuckProp thus ?case by (fastforce intro: terminates.intros)
next
case AbruptProp thus ?case by (fastforce intro: terminates.intros)
qed
lemma steps_preserves_termination:
assumes steps: "Γ⊢(c,s) →⇧* (c',s')"
shows "Γ⊢c↓s ⟹ Γ⊢c'↓s'"
using steps
proof (induct rule: rtranclp_induct2 [consumes 1, case_names Refl Trans])
case Refl thus ?case .
next
case Trans
thus ?case
by (blast dest: step_preserves_termination)
qed
ML {*
ML_Thms.bind_thm ("tranclp_induct2", Split_Rule.split_rule @{context}
(Rule_Insts.read_instantiate @{context}
[((("a", 0), Position.none), "(aa,ab)"), ((("b", 0), Position.none), "(ba,bb)")] []
@{thm tranclp_induct}));
*}
lemma steps_preserves_termination':
assumes steps: "Γ⊢(c,s) →⇧+ (c',s')"
shows "Γ⊢c↓s ⟹ Γ⊢c'↓s'"
using steps
proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans])
case Step thus ?case by (blast intro: step_preserves_termination)
next
case Trans
thus ?case
by (blast dest: step_preserves_termination)
qed
definition head_com:: "('s,'p,'f) com ⇒ ('s,'p,'f) com"
where
"head_com c =
(case c of
Seq c⇩1 c⇩2 ⇒ c⇩1
| Catch c⇩1 c⇩2 ⇒ c⇩1
| _ ⇒ c)"
definition head:: "('s,'p,'f) config ⇒ ('s,'p,'f) config"
where "head cfg = (head_com (fst cfg), snd cfg)"
lemma le_Suc_cases: "⟦⋀i. ⟦i < k⟧ ⟹ P i; P k⟧ ⟹ ∀i<(Suc k). P i"
apply clarify
apply (case_tac "i=k")
apply auto
done
lemma redex_Seq_False: "⋀c' c''. (redex c = Seq c'' c') = False"
by (induct c) auto
lemma redex_Catch_False: "⋀c' c''. (redex c = Catch c'' c') = False"
by (induct c) auto
lemma infinite_computation_extract_head_Seq:
assumes inf_comp: "∀i::nat. Γ⊢f i → f (i+1)"
assumes f_0: "f 0 = (Seq c⇩1 c⇩2,s)"
assumes not_fin: "∀i<k. ¬ final (head (f i))"
shows "∀i<k. (∃c' s'. f (i + 1) = (Seq c' c⇩2, s')) ∧
Γ⊢head (f i) → head (f (i+1))"
(is "∀i<k. ?P i")
using not_fin
proof (induct k)
case 0
show ?case by simp
next
case (Suc k)
have not_fin_Suc:
"∀i<Suc k. ¬ final (head (f i))" by fact
from this[rule_format] have not_fin_k:
"∀i<k. ¬ final (head (f i))"
apply clarify
apply (subgoal_tac "i < Suc k")
apply blast
apply simp
done
from Suc.hyps [OF this]
have hyp: "∀i<k. (∃c' s'. f (i + 1) = (Seq c' c⇩2, s')) ∧
Γ⊢ head (f i) → head (f (i + 1))".
show ?case
proof (rule le_Suc_cases)
fix i
assume "i < k"
then show "?P i"
by (rule hyp [rule_format])
next
show "?P k"
proof -
from hyp [rule_format, of "k - 1"] f_0
obtain c' fs' L' s' where f_k: "f k = (Seq c' c⇩2, s')"
by (cases k) auto
from inf_comp [rule_format, of k] f_k
have "Γ⊢(Seq c' c⇩2, s') → f (k + 1)"
by simp
moreover
from not_fin_Suc [rule_format, of k] f_k
have "¬ final (c',s')"
by (simp add: final_def head_def head_com_def)
ultimately
obtain c'' s'' where
"Γ⊢(c', s') → (c'', s'')" and
"f (k + 1) = (Seq c'' c⇩2, s'')"
by cases (auto simp add: redex_Seq_False final_def)
with f_k
show ?thesis
by (simp add: head_def head_com_def)
qed
qed
qed
lemma infinite_computation_extract_head_Catch:
assumes inf_comp: "∀i::nat. Γ⊢f i → f (i+1)"
assumes f_0: "f 0 = (Catch c⇩1 c⇩2,s)"
assumes not_fin: "∀i<k. ¬ final (head (f i))"
shows "∀i<k. (∃c' s'. f (i + 1) = (Catch c' c⇩2, s')) ∧
Γ⊢head (f i) → head (f (i+1))"
(is "∀i<k. ?P i")
using not_fin
proof (induct k)
case 0
show ?case by simp
next
case (Suc k)
have not_fin_Suc:
"∀i<Suc k. ¬ final (head (f i))" by fact
from this[rule_format] have not_fin_k:
"∀i<k. ¬ final (head (f i))"
apply clarify
apply (subgoal_tac "i < Suc k")
apply blast
apply simp
done
from Suc.hyps [OF this]
have hyp: "∀i<k. (∃c' s'. f (i + 1) = (Catch c' c⇩2, s')) ∧
Γ⊢ head (f i) → head (f (i + 1))".
show ?case
proof (rule le_Suc_cases)
fix i
assume "i < k"
then show "?P i"
by (rule hyp [rule_format])
next
show "?P k"
proof -
from hyp [rule_format, of "k - 1"] f_0
obtain c' fs' L' s' where f_k: "f k = (Catch c' c⇩2, s')"
by (cases k) auto
from inf_comp [rule_format, of k] f_k
have "Γ⊢(Catch c' c⇩2, s') → f (k + 1)"
by simp
moreover
from not_fin_Suc [rule_format, of k] f_k
have "¬ final (c',s')"
by (simp add: final_def head_def head_com_def)
ultimately
obtain c'' s'' where
"Γ⊢(c', s') → (c'', s'')" and
"f (k + 1) = (Catch c'' c⇩2, s'')"
by cases (auto simp add: redex_Catch_False final_def)+
with f_k
show ?thesis
by (simp add: head_def head_com_def)
qed
qed
qed
lemma no_inf_Throw: "¬ Γ⊢(Throw,s) → …(∞)"
proof
assume "Γ⊢ (Throw, s) → …(∞)"
then obtain f where
step [rule_format]: "∀i::nat. Γ⊢f i → f (i+1)" and
f_0: "f 0 = (Throw, s)"
by (auto simp add: inf_def)
from step [of 0, simplified f_0] step [of 1]
show False
by cases (auto elim: step_elim_cases)
qed
lemma split_inf_Seq:
assumes inf_comp: "Γ⊢(Seq c⇩1 c⇩2,s) → …(∞)"
shows "Γ⊢(c⇩1,s) → …(∞) ∨
(∃s'. Γ⊢(c⇩1,s) →⇧* (Skip,s') ∧ Γ⊢(c⇩2,s') → …(∞))"
proof -
from inf_comp obtain f where
step: "∀i::nat. Γ⊢f i → f (i+1)" and
f_0: "f 0 = (Seq c⇩1 c⇩2, s)"
by (auto simp add: inf_def)
from f_0 have head_f_0: "head (f 0) = (c⇩1,s)"
by (simp add: head_def head_com_def)
show ?thesis
proof (cases "∃i. final (head (f i))")
case True
define k where "k = (LEAST i. final (head (f i)))"
have less_k: "∀i<k. ¬ final (head (f i))"
apply (intro allI impI)
apply (unfold k_def)
apply (drule not_less_Least)
apply auto
done
from infinite_computation_extract_head_Seq [OF step f_0 this]
obtain step_head: "∀i<k. Γ⊢ head (f i) → head (f (i + 1))" and
conf: "∀i<k. (∃c' s'. f (i + 1) = (Seq c' c⇩2, s'))"
by blast
from True
have final_f_k: "final (head (f k))"
apply -
apply (erule exE)
apply (drule LeastI)
apply (simp add: k_def)
done
moreover
from f_0 conf [rule_format, of "k - 1"]
obtain c' s' where f_k: "f k = (Seq c' c⇩2,s')"
by (cases k) auto
moreover
from step_head have steps_head: "Γ⊢head (f 0) →⇧* head (f k)"
proof (induct k)
case 0 thus ?case by simp
next
case (Suc m)
have step: "∀i<Suc m. Γ⊢ head (f i) → head (f (i + 1))" by fact
hence "∀i<m. Γ⊢ head (f i) → head (f (i + 1))"
by auto
hence "Γ⊢ head (f 0) →⇧* head (f m)"
by (rule Suc.hyps)
also from step [rule_format, of m]
have "Γ⊢ head (f m) → head (f (m + 1))" by simp
finally show ?case by simp
qed
{
assume f_k: "f k = (Seq Skip c⇩2, s')"
with steps_head
have "Γ⊢(c⇩1,s) →⇧* (Skip,s')"
using head_f_0
by (simp add: head_def head_com_def)
moreover
from step [rule_format, of k] f_k
obtain "Γ⊢(Seq Skip c⇩2,s') → (c⇩2,s')" and
f_Suc_k: "f (k + 1) = (c⇩2,s')"
by (fastforce elim: step.cases intro: step.intros)
define g where"g i = f (i + (k + 1))" for i
from f_Suc_k
have g_0: "g 0 = (c⇩2,s')"
by (simp add: g_def)
from step
have "∀i. Γ⊢g i → g (i + 1)"
by (simp add: g_def)
with g_0 have "Γ⊢(c⇩2,s') → …(∞)"
by (auto simp add: inf_def)
ultimately
have ?thesis
by auto
}
moreover
{
fix x
assume s': "s'=Normal x" and f_k: "f k = (Seq Throw c⇩2, s')"
from step [rule_format, of k] f_k s'
obtain "Γ⊢(Seq Throw c⇩2,s') → (Throw,s')" and
f_Suc_k: "f (k + 1) = (Throw,s')"
by (fastforce elim: step_elim_cases intro: step.intros)
define g where "g i = f (i + (k + 1))" for i
from f_Suc_k
have g_0: "g 0 = (Throw,s')"
by (simp add: g_def)
from step
have "∀i. Γ⊢g i → g (i + 1)"
by (simp add: g_def)
with g_0 have "Γ⊢(Throw,s') → …(∞)"
by (auto simp add: inf_def)
with no_inf_Throw
have ?thesis
by auto
}
ultimately
show ?thesis
by (auto simp add: final_def head_def head_com_def)
next
case False
then have not_fin: "∀i. ¬ final (head (f i))"
by blast
have "∀i. Γ⊢head (f i) → head (f (i + 1))"
proof
fix k
from not_fin
have "∀i<(Suc k). ¬ final (head (f i))"
by simp
from infinite_computation_extract_head_Seq [OF step f_0 this ]
show "Γ⊢ head (f k) → head (f (k + 1))" by simp
qed
with head_f_0 have "Γ⊢(c⇩1,s) → …(∞)"
by (auto simp add: inf_def)
thus ?thesis
by simp
qed
qed
lemma split_inf_Catch:
assumes inf_comp: "Γ⊢(Catch c⇩1 c⇩2,s) → …(∞)"
shows "Γ⊢(c⇩1,s) → …(∞) ∨
(∃s'. Γ⊢(c⇩1,s) →⇧* (Throw,Normal s') ∧ Γ⊢(c⇩2,Normal s') → …(∞))"
proof -
from inf_comp obtain f where
step: "∀i::nat. Γ⊢f i → f (i+1)" and
f_0: "f 0 = (Catch c⇩1 c⇩2, s)"
by (auto simp add: inf_def)
from f_0 have head_f_0: "head (f 0) = (c⇩1,s)"
by (simp add: head_def head_com_def)
show ?thesis
proof (cases "∃i. final (head (f i))")
case True
define k where "k = (LEAST i. final (head (f i)))"
have less_k: "∀i<k. ¬ final (head (f i))"
apply (intro allI impI)
apply (unfold k_def)
apply (drule not_less_Least)
apply auto
done
from infinite_computation_extract_head_Catch [OF step f_0 this]
obtain step_head: "∀i<k. Γ⊢ head (f i) → head (f (i + 1))" and
conf: "∀i<k. (∃c' s'. f (i + 1) = (Catch c' c⇩2, s'))"
by blast
from True
have final_f_k: "final (head (f k))"
apply -
apply (erule exE)
apply (drule LeastI)
apply (simp add: k_def)
done
moreover
from f_0 conf [rule_format, of "k - 1"]
obtain c' s' where f_k: "f k = (Catch c' c⇩2,s')"
by (cases k) auto
moreover
from step_head have steps_head: "Γ⊢head (f 0) →⇧* head (f k)"
proof (induct k)
case 0 thus ?case by simp
next
case (Suc m)
have step: "∀i<Suc m. Γ⊢ head (f i) → head (f (i + 1))" by fact
hence "∀i<m. Γ⊢ head (f i) → head (f (i + 1))"
by auto
hence "Γ⊢ head (f 0) →⇧* head (f m)"
by (rule Suc.hyps)
also from step [rule_format, of m]
have "Γ⊢ head (f m) → head (f (m + 1))" by simp
finally show ?case by simp
qed
{
assume f_k: "f k = (Catch Skip c⇩2, s')"
with steps_head
have "Γ⊢(c⇩1,s) →⇧* (Skip,s')"
using head_f_0
by (simp add: head_def head_com_def)
moreover
from step [rule_format, of k] f_k
obtain "Γ⊢(Catch Skip c⇩2,s') → (Skip,s')" and
f_Suc_k: "f (k + 1) = (Skip,s')"
by (fastforce elim: step.cases intro: step.intros)
from step [rule_format, of "k+1", simplified f_Suc_k]
have ?thesis
by (rule no_step_final') (auto simp add: final_def)
}
moreover
{
fix x
assume s': "s'=Normal x" and f_k: "f k = (Catch Throw c⇩2, s')"
with steps_head
have "Γ⊢(c⇩1,s) →⇧* (Throw,s')"
using head_f_0
by (simp add: head_def head_com_def)
moreover
from step [rule_format, of k] f_k s'
obtain "Γ⊢(Catch Throw c⇩2,s') → (c⇩2,s')" and
f_Suc_k: "f (k + 1) = (c⇩2,s')"
by (fastforce elim: step_elim_cases intro: step.intros)
define g where "g i = f (i + (k + 1))" for i
from f_Suc_k
have g_0: "g 0 = (c⇩2,s')"
by (simp add: g_def)
from step
have "∀i. Γ⊢g i → g (i + 1)"
by (simp add: g_def)
with g_0 have "Γ⊢(c⇩2,s') → …(∞)"
by (auto simp add: inf_def)
ultimately
have ?thesis
using s'
by auto
}
ultimately
show ?thesis
by (auto simp add: final_def head_def head_com_def)
next
case False
then have not_fin: "∀i. ¬ final (head (f i))"
by blast
have "∀i. Γ⊢head (f i) → head (f (i + 1))"
proof
fix k
from not_fin
have "∀i<(Suc k). ¬ final (head (f i))"
by simp
from infinite_computation_extract_head_Catch [OF step f_0 this ]
show "Γ⊢ head (f k) → head (f (k + 1))" by simp
qed
with head_f_0 have "Γ⊢(c⇩1,s) → …(∞)"
by (auto simp add: inf_def)
thus ?thesis
by simp
qed
qed
lemma Skip_no_step: "Γ⊢(Skip,s) → cfg ⟹ P"
apply (erule no_step_final')
apply (simp add: final_def)
done
lemma not_inf_Stuck: "¬ Γ⊢(c,Stuck) → …(∞)"
proof (induct c)
case Skip
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Skip, Stuck)"
from f_step [of 0] f_0
show False
by (auto elim: Skip_no_step)
qed
next
case (Basic g)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Basic g, Stuck)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Spec r)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Spec r, Stuck)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Seq c⇩1 c⇩2)
show ?case
proof
assume "Γ⊢ (Seq c⇩1 c⇩2, Stuck) → …(∞)"
from split_inf_Seq [OF this] Seq.hyps
show False
by (auto dest: steps_Stuck_prop)
qed
next
case (Cond b c⇩1 c⇩2)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Cond b c⇩1 c⇩2, Stuck)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (While b c)
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, Stuck)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Call p)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Call p, Stuck)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (DynCom d)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (DynCom d, Stuck)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Guard m g c)
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, Stuck)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case Throw
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Throw, Stuck)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Catch c⇩1 c⇩2)
show ?case
proof
assume "Γ⊢ (Catch c⇩1 c⇩2, Stuck) → …(∞)"
from split_inf_Catch [OF this] Catch.hyps
show False
by (auto dest: steps_Stuck_prop)
qed
qed
lemma not_inf_Fault: "¬ Γ⊢(c,Fault x) → …(∞)"
proof (induct c)
case Skip
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Skip, Fault x)"
from f_step [of 0] f_0
show False
by (auto elim: Skip_no_step)
qed
next
case (Basic g)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Basic g, Fault x)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Spec r)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Spec r, Fault x)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Seq c⇩1 c⇩2)
show ?case
proof
assume "Γ⊢ (Seq c⇩1 c⇩2, Fault x) → …(∞)"
from split_inf_Seq [OF this] Seq.hyps
show False
by (auto dest: steps_Fault_prop)
qed
next
case (Cond b c⇩1 c⇩2)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Cond b c⇩1 c⇩2, Fault x)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (While b c)
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, Fault x)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Call p)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Call p, Fault x)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (DynCom d)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (DynCom d, Fault x)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Guard m g c)
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, Fault x)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case Throw
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Throw, Fault x)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Catch c⇩1 c⇩2)
show ?case
proof
assume "Γ⊢ (Catch c⇩1 c⇩2, Fault x) → …(∞)"
from split_inf_Catch [OF this] Catch.hyps
show False
by (auto dest: steps_Fault_prop)
qed
qed
lemma not_inf_Abrupt: "¬ Γ⊢(c,Abrupt s) → …(∞)"
proof (induct c)
case Skip
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Skip, Abrupt s)"
from f_step [of 0] f_0
show False
by (auto elim: Skip_no_step)
qed
next
case (Basic g)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Basic g, Abrupt s)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Spec r)
thus ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Spec r, Abrupt s)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Seq c⇩1 c⇩2)
show ?case
proof
assume "Γ⊢ (Seq c⇩1 c⇩2, Abrupt s) → …(∞)"
from split_inf_Seq [OF this] Seq.hyps
show False
by (auto dest: steps_Abrupt_prop)
qed
next
case (Cond b c⇩1 c⇩2)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Cond b c⇩1 c⇩2, Abrupt s)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (While b c)
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, Abrupt s)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Call p)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Call p, Abrupt s)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (DynCom d)
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (DynCom d, Abrupt s)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Guard m g c)
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, Abrupt s)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case Throw
show ?case
proof (rule not_infI)
fix f
assume f_step: "⋀i. Γ⊢f i → f (Suc i)"
assume f_0: "f 0 = (Throw, Abrupt s)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Catch c⇩1 c⇩2)
show ?case
proof
assume "Γ⊢ (Catch c⇩1 c⇩2, Abrupt s) → …(∞)"
from split_inf_Catch [OF this] Catch.hyps
show False
by (auto dest: steps_Abrupt_prop)
qed
qed
theorem terminates_impl_no_infinite_computation:
assumes termi: "Γ⊢c ↓ s"
shows "¬ Γ⊢(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
show False
by (auto elim: Skip_no_step)
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 f_step [of 1]
show False
by (fastforce elim: Skip_no_step 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)"
from f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Guard s g c m)
have g: "s ∈ g" by fact
have hyp: "¬ Γ⊢ (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 f_step [of 0] f_0 g
have "f 1 = (c,Normal s)"
by (fastforce elim: step_elim_cases)
with f_step
have "Γ⊢ (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 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Fault c m)
thus ?case
by (rule not_inf_Fault)
next
case (Seq c⇩1 s c⇩2)
show ?case
proof
assume "Γ⊢ (Seq c⇩1 c⇩2, Normal s) → …(∞)"
from split_inf_Seq [OF this] Seq.hyps
show False
by (auto intro: steps_Skip_impl_exec)
qed
next
case (CondTrue s b c1 c2)
have b: "s ∈ b" by fact
have hyp_c1: "¬ Γ⊢ (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 "Γ⊢ (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: "¬ Γ⊢ (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 "Γ⊢ (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: "¬ Γ⊢ (c, Normal s) → …(∞)" by fact
have hyp_w: "∀s'. Γ⊢ ⟨c,Normal s⟩ ⇒ s' ⟶
Γ⊢While b c ↓ s' ∧ ¬ Γ⊢ (While b c, s') → …(∞)" by fact
have not_inf_Seq: "¬ Γ⊢ (Seq c (While b c), Normal s) → …(∞)"
proof
assume "Γ⊢ (Seq c (While b c), Normal s) → …(∞)"
from split_inf_Seq [OF this] hyp_c hyp_w show False
by (auto intro: steps_Skip_impl_exec)
qed
show ?case
proof
assume "Γ⊢ (While b c, Normal s) → …(∞)"
then obtain f where
f_step: "⋀i. Γ⊢f i → f (Suc i)" and
f_0: "f 0 = (While b c, Normal s)"
by (auto simp add: inf_def)
from f_step [of 0] f_0 b
have "f 1 = (Seq c (While b c),Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step
have "Γ⊢ (Seq c (While b c), Normal s) → …(∞)"
apply (simp add: inf_def)
apply (rule_tac x="λi. f (Suc i)" in exI)
by simp
with not_inf_Seq show False by simp
qed
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 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Call p bdy s)
have bdy: "Γ p = Some bdy" by fact
have hyp: "¬ Γ⊢ (bdy, 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 = (Call p, Normal s)"
from bdy f_step [of 0] f_0
have "f 1 = (bdy,Normal s)"
by (auto elim: step_Normal_elim_cases)
with f_step
have "Γ⊢ (bdy, 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 (CallUndefined p s)
have no_bdy: "Γ 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 no_bdy f_step [of 0] f_0 f_step [of 1]
show False
by (fastforce elim: Skip_no_step step_elim_cases)
qed
next
case (Stuck c)
show ?case
by (rule not_inf_Stuck)
next
case (DynCom c s)
have hyp: "¬ Γ⊢ (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 "Γ⊢ (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
show False
by (auto elim: step_elim_cases)
qed
next
case (Abrupt c)
show ?case
by (rule not_inf_Abrupt)
next
case (Catch c⇩1 s c⇩2)
show ?case
proof
assume "Γ⊢ (Catch c⇩1 c⇩2, Normal s) → …(∞)"
from split_inf_Catch [OF this] Catch.hyps
show False
by (auto intro: steps_Throw_impl_exec)
qed
qed
definition
termi_call_steps :: "('s,'p,'f) body ⇒ (('s × 'p) × ('s × 'p))set"
where
"termi_call_steps Γ =
{((t,q),(s,p)). Γ⊢Call p↓Normal s ∧
(∃c. Γ⊢(Call p,Normal s) →⇧+ (c,Normal t) ∧ redex c = Call q)}"
primrec subst_redex:: "('s,'p,'f)com ⇒ ('s,'p,'f)com ⇒ ('s,'p,'f)com"
where
"subst_redex Skip c = c" |
"subst_redex (Basic f) c = c" |
"subst_redex (Spec r) c = c" |
"subst_redex (Seq c⇩1 c⇩2) c = Seq (subst_redex c⇩1 c) c⇩2" |
"subst_redex (Cond b c⇩1 c⇩2) c = c" |
"subst_redex (While b c') c = c" |
"subst_redex (Call p) c = c" |
"subst_redex (DynCom d) c = c" |
"subst_redex (Guard f b c') c = c" |
"subst_redex (Throw) c = c" |
"subst_redex (Catch c⇩1 c⇩2) c = Catch (subst_redex c⇩1 c) c⇩2"
lemma subst_redex_redex:
"subst_redex c (redex c) = c"
by (induct c) auto
lemma redex_subst_redex: "redex (subst_redex c r) = redex r"
by (induct c) auto
lemma step_redex':
shows "Γ⊢(redex c,s) → (r',s') ⟹ Γ⊢(c,s) → (subst_redex c r',s')"
by (induct c) (auto intro: step.Seq step.Catch)
lemma step_redex:
shows "Γ⊢(r,s) → (r',s') ⟹ Γ⊢(subst_redex c r,s) → (subst_redex c r',s')"
by (induct c) (auto intro: step.Seq step.Catch)
lemma steps_redex:
assumes steps: "Γ⊢ (r, s) →⇧* (r', s')"
shows "⋀c. Γ⊢(subst_redex c r,s) →⇧* (subst_redex c r',s')"
using steps
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl
show "Γ⊢ (subst_redex c r', s') →⇧* (subst_redex c r', s')"
by simp
next
case (Trans r s r'' s'')
have "Γ⊢ (r, s) → (r'', s'')" by fact
from step_redex [OF this]
have "Γ⊢ (subst_redex c r, s) → (subst_redex c r'', s'')".
also
have "Γ⊢ (subst_redex c r'', s'') →⇧* (subst_redex c r', s')" by fact
finally show ?case .
qed
ML {*
ML_Thms.bind_thm ("trancl_induct2", Split_Rule.split_rule @{context}
(Rule_Insts.read_instantiate @{context}
[((("a", 0), Position.none), "(aa, ab)"), ((("b", 0), Position.none), "(ba, bb)")] []
@{thm trancl_induct}));
*}
lemma steps_redex':
assumes steps: "Γ⊢ (r, s) →⇧+ (r', s')"
shows "⋀c. Γ⊢(subst_redex c r,s) →⇧+ (subst_redex c r',s')"
using steps
proof (induct rule: tranclp_induct2 [consumes 1,case_names Step Trans])
case (Step r' s')
have "Γ⊢ (r, s) → (r', s')" by fact
then have "Γ⊢ (subst_redex c r, s) → (subst_redex c r', s')"
by (rule step_redex)
then show "Γ⊢ (subst_redex c r, s) →⇧+ (subst_redex c r', s')"..
next
case (Trans r' s' r'' s'')
have "Γ⊢ (subst_redex c r, s) →⇧+ (subst_redex c r', s')" by fact
also
have "Γ⊢ (r', s') → (r'', s'')" by fact
hence "Γ⊢ (subst_redex c r', s') → (subst_redex c r'', s'')"
by (rule step_redex)
finally show "Γ⊢ (subst_redex c r, s) →⇧+ (subst_redex c r'', s'')" .
qed
primrec seq:: "(nat ⇒ ('s,'p,'f)com) ⇒ 'p ⇒ nat ⇒ ('s,'p,'f)com"
where
"seq c p 0 = Call p" |
"seq c p (Suc i) = subst_redex (seq c p i) (c i)"
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 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 terminates_impl_no_infinite_trans_computation:
assumes terminates: "Γ⊢c↓s"
shows "¬(∃f. f 0 = (c,s) ∧ (∀i. Γ⊢f i →⇧+ f(Suc i)))"
proof -
have "wf({(y,x). Γ⊢(c,s) →⇧* x ∧ Γ⊢x → y}⇧+)"
proof (rule wf_trancl)
show "wf {(y, x). Γ⊢(c,s) →⇧* x ∧ Γ⊢x → y}"
proof (simp only: wf_iff_no_infinite_down_chain,clarify,simp)
fix f
assume "∀i. Γ⊢(c,s) →⇧* f i ∧ Γ⊢f i → f (Suc i)"
hence "∃f. f (0::nat) = (c,s) ∧ (∀i. Γ⊢f i → f (Suc i))"
by (rule renumber [to_pred])
moreover from terminates_impl_no_infinite_computation [OF terminates]
have "¬ (∃f. f (0::nat) = (c, s) ∧ (∀i. Γ⊢f i → f (Suc i)))"
by (simp add: inf_def)
ultimately show False
by simp
qed
qed
hence "¬ (∃f. ∀i. (f (Suc i), f i)
∈ {(y, x). Γ⊢(c, s) →⇧* x ∧ Γ⊢x → y}⇧+)"
by (simp add: wf_iff_no_infinite_down_chain)
thus ?thesis
proof (rule contrapos_nn)
assume "∃f. f (0::nat) = (c, s) ∧ (∀i. Γ⊢f i →⇧+ f (Suc i))"
then obtain f where
f0: "f 0 = (c, s)" and
seq: "∀i. Γ⊢f i →⇧+ f (Suc i)"
by iprover
show
"∃f. ∀i. (f (Suc i), f i) ∈ {(y, x). Γ⊢(c, s) →⇧* x ∧ Γ⊢x → y}⇧+"
proof (rule exI [where x=f],rule allI)
fix i
show "(f (Suc i), f i) ∈ {(y, x). Γ⊢(c, s) →⇧* x ∧ Γ⊢x → y}⇧+"
proof -
{
fix i have "Γ⊢(c,s) →⇧* f i"
proof (induct i)
case 0 show "Γ⊢(c, s) →⇧* f 0"
by (simp add: f0)
next
case (Suc n)
have "Γ⊢(c, s) →⇧* f n" by fact
with seq show "Γ⊢(c, s) →⇧* f (Suc n)"
by (blast intro: tranclp_into_rtranclp rtranclp_trans)
qed
}
hence "Γ⊢(c,s) →⇧* f i"
by iprover
with seq have
"(f (Suc i), f i) ∈ {(y, x). Γ⊢(c, s) →⇧* x ∧ Γ⊢x →⇧+ y}"
by clarsimp
moreover
have "∀y. Γ⊢f i →⇧+ y⟶Γ⊢(c, s) →⇧* f i⟶Γ⊢(c, s) →⇧* y"
by (blast intro: tranclp_into_rtranclp rtranclp_trans)
ultimately
show ?thesis
by (subst lem )
qed
qed
qed
qed
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 f
assume inf: "∀i. (λ(t, q) (s, p).
Γ⊢Call p ↓ Normal s ∧
(∃c. Γ⊢ (Call p, Normal s) →⇧+ (c, Normal t) ∧ redex c = Call q))
(f (Suc i)) (f i)"
define s where "s i = fst (f i)" for i::nat
define p where "p i =(snd (f i)::'b)" for i :: nat
from inf
have inf': "∀i. Γ⊢Call (p i) ↓ Normal (s i) ∧
(∃c. Γ⊢ (Call (p i), Normal (s i)) →⇧+ (c, Normal (s (i+1))) ∧
redex c = Call (p (i+1)))"
apply -
apply (rule allI)
apply (erule_tac x=i in allE)
apply (auto simp add: s_def p_def)
done
show False
proof -
from inf'
have "∃c. ∀i. Γ⊢Call (p i) ↓ Normal (s i) ∧
Γ⊢ (Call (p i), Normal (s i)) →⇧+ (c i, Normal (s (i+1))) ∧
redex (c i) = Call (p (i+1))"
apply -
apply (rule choice)
by blast
then obtain c where
termi_c: "∀i. Γ⊢Call (p i) ↓ Normal (s i)" and
steps_c: "∀i. Γ⊢ (Call (p i), Normal (s i)) →⇧+ (c i, Normal (s (i+1)))" and
red_c: "∀i. redex (c i) = Call (p (i+1))"
by auto
define g where "g i = (seq c (p 0) i,Normal (s i)::('a,'c) xstate)" for i
from red_c [rule_format, of 0]
have "g 0 = (Call (p 0), Normal (s 0))"
by (simp add: g_def)
moreover
{
fix i
have "redex (seq c (p 0) i) = Call (p i)"
by (induct i) (auto simp add: redex_subst_redex red_c)
from this [symmetric]
have "subst_redex (seq c (p 0) i) (Call (p i)) = (seq c (p 0) i)"
by (simp add: subst_redex_redex)
} note subst_redex_seq = this
have "∀i. Γ⊢ (g i) →⇧+ (g (i+1))"
proof
fix i
from steps_c [rule_format, of i]
have "Γ⊢ (Call (p i), Normal (s i)) →⇧+ (c i, Normal (s (i + 1)))".
from steps_redex' [OF this, of "(seq c (p 0) i)"]
have "Γ⊢ (subst_redex (seq c (p 0) i) (Call (p i)), Normal (s i)) →⇧+
(subst_redex (seq c (p 0) i) (c i), Normal (s (i + 1)))" .
hence "Γ⊢ (seq c (p 0) i, Normal (s i)) →⇧+
(seq c (p 0) (i+1), Normal (s (i + 1)))"
by (simp add: subst_redex_seq)
thus "Γ⊢ (g i) →⇧+ (g (i+1))"
by (simp add: g_def)
qed
moreover
from terminates_impl_no_infinite_trans_computation [OF termi_c [rule_format, of 0]]
have "¬ (∃f. f 0 = (Call (p 0), Normal (s 0)) ∧ (∀i. Γ⊢ f i →⇧+ f (Suc i)))" .
ultimately show False
by auto
qed
qed
lemma no_infinite_computation_implies_wf:
assumes not_inf: "¬ Γ⊢ (c, s) → …(∞)"
shows "wf {(c2,c1). Γ ⊢ (c,s) →⇧* c1 ∧ Γ ⊢ c1 → c2}"
proof (simp only: wf_iff_no_infinite_down_chain,clarify, simp)
fix f
assume "∀i. Γ⊢(c, s) →⇧* f i ∧ Γ⊢f i → f (Suc i)"
hence "∃f. f 0 = (c, s) ∧ (∀i. Γ⊢f i → f (Suc i))"
by (rule renumber [to_pred])
moreover from not_inf
have "¬ (∃f. f 0 = (c, s) ∧ (∀i. Γ⊢f i → f (Suc i)))"
by (simp add: inf_def)
ultimately show False
by simp
qed
lemma not_final_Stuck_step: "¬ final (c,Stuck) ⟹ ∃c' s'. Γ⊢ (c, Stuck) → (c',s')"
by (induct c) (fastforce intro: step.intros simp add: final_def)+
lemma not_final_Abrupt_step:
"¬ final (c,Abrupt s) ⟹ ∃c' s'. Γ⊢ (c, Abrupt s) → (c',s')"
by (induct c) (fastforce intro: step.intros simp add: final_def)+
lemma not_final_Fault_step:
"¬ final (c,Fault f) ⟹ ∃c' s'. Γ⊢ (c, Fault f) → (c',s')"
by (induct c) (fastforce intro: step.intros simp add: final_def)+
lemma not_final_Normal_step:
"¬ final (c,Normal s) ⟹ ∃c' s'. Γ⊢ (c, Normal s) → (c',s')"
proof (induct c)
case Skip thus ?case by (fastforce intro: step.intros simp add: final_def)
next
case Basic thus ?case by (fastforce intro: step.intros)
next
case (Spec r)
thus ?case
by (cases "∃t. (s,t) ∈ r") (fastforce intro: step.intros)+
next
case (Seq c⇩1 c⇩2)
thus ?case
by (cases "final (c⇩1,Normal s)") (fastforce intro: step.intros simp add: final_def)+
next
case (Cond b c1 c2)
show ?case
by (cases "s ∈ b") (fastforce intro: step.intros)+
next
case (While b c)
show ?case
by (cases "s ∈ b") (fastforce intro: step.intros)+
next
case (Call p)
show ?case
by (cases "Γ p") (fastforce intro: step.intros)+
next
case DynCom thus ?case by (fastforce intro: step.intros)
next
case (Guard f g c)
show ?case
by (cases "s ∈ g") (fastforce intro: step.intros)+
next
case Throw
thus ?case by (fastforce intro: step.intros simp add: final_def)
next
case (Catch c⇩1 c⇩2)
thus ?case
by (cases "final (c⇩1,Normal s)") (fastforce intro: step.intros simp add: final_def)+
qed
lemma final_termi:
"final (c,s) ⟹ Γ⊢c↓s"
by (cases s) (auto simp add: final_def terminates.intros)
lemma split_computation:
assumes steps: "Γ⊢ (c, s) →⇧* (c⇩f, s⇩f)"
assumes not_final: "¬ final (c,s)"
assumes final: "final (c⇩f,s⇩f)"
shows "∃c' s'. Γ⊢ (c, s) → (c',s') ∧ Γ⊢ (c', s') →⇧* (c⇩f, s⇩f)"
using steps not_final final
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl thus ?case by simp
next
case (Trans c s c' s')
thus ?case by auto
qed
lemma wf_implies_termi_reach_step_case:
assumes hyp: "⋀c' s'. Γ⊢ (c, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'"
shows "Γ⊢c ↓ Normal s"
using hyp
proof (induct c)
case Skip show ?case by (fastforce intro: terminates.intros)
next
case Basic show ?case by (fastforce intro: terminates.intros)
next
case (Spec r)
show ?case
by (cases "∃t. (s,t)∈r") (fastforce intro: terminates.intros)+
next
case (Seq c⇩1 c⇩2)
have hyp: "⋀c' s'. Γ⊢ (Seq c⇩1 c⇩2, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
show ?case
proof (rule terminates.Seq)
{
fix c' s'
assume step_c⇩1: "Γ⊢ (c⇩1, Normal s) → (c', s')"
have "Γ⊢c' ↓ s'"
proof -
from step_c⇩1
have "Γ⊢ (Seq c⇩1 c⇩2, Normal s) → (Seq c' c⇩2, s')"
by (rule step.Seq)
from hyp [OF this]
have "Γ⊢Seq c' c⇩2 ↓ s'".
thus "Γ⊢c'↓ s'"
by cases auto
qed
}
from Seq.hyps (1) [OF this]
show "Γ⊢c⇩1 ↓ Normal s".
next
show "∀s'. Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ s' ⟶ Γ⊢c⇩2 ↓ s'"
proof (intro allI impI)
fix s'
assume exec_c⇩1: "Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ s'"
show "Γ⊢c⇩2 ↓ s'"
proof (cases "final (c⇩1,Normal s)")
case True
hence "c⇩1=Skip ∨ c⇩1=Throw"
by (simp add: final_def)
thus ?thesis
proof
assume Skip: "c⇩1=Skip"
have "Γ⊢(Seq Skip c⇩2,Normal s) → (c⇩2,Normal s)"
by (rule step.SeqSkip)
from hyp [simplified Skip, OF this]
have "Γ⊢c⇩2 ↓ Normal s" .
moreover from exec_c⇩1 Skip
have "s'=Normal s"
by (auto elim: exec_Normal_elim_cases)
ultimately show ?thesis by simp
next
assume Throw: "c⇩1=Throw"
with exec_c⇩1 have "s'=Abrupt s"
by (auto elim: exec_Normal_elim_cases)
thus ?thesis
by auto
qed
next
case False
from exec_impl_steps [OF exec_c⇩1]
obtain c⇩f t where
steps_c⇩1: "Γ⊢ (c⇩1, Normal s) →⇧* (c⇩f, t)" and
fin:"(case s' of
Abrupt x ⇒ c⇩f = Throw ∧ t = Normal x
| _ ⇒ c⇩f = Skip ∧ t = s')"
by (fastforce split: xstate.splits)
with fin have final: "final (c⇩f,t)"
by (cases s') (auto simp add: final_def)
from split_computation [OF steps_c⇩1 False this]
obtain c'' s'' where
first: "Γ⊢ (c⇩1, Normal s) → (c'', s'')" and
rest: "Γ⊢ (c'', s'') →⇧* (c⇩f, t)"
by blast
from step.Seq [OF first]
have "Γ⊢ (Seq c⇩1 c⇩2, Normal s) → (Seq c'' c⇩2, s'')".
from hyp [OF this]
have termi_s'': "Γ⊢Seq c'' c⇩2 ↓ s''".
show ?thesis
proof (cases s'')
case (Normal x)
from termi_s'' [simplified Normal]
have termi_c⇩2: "∀t. Γ⊢ ⟨c'',Normal x⟩ ⇒ t ⟶ Γ⊢c⇩2 ↓ t"
by cases
show ?thesis
proof (cases "∃x'. s'=Abrupt x'")
case False
with fin obtain "c⇩f=Skip" "t=s'"
by (cases s') auto
from steps_Skip_impl_exec [OF rest [simplified this]] Normal
have "Γ⊢ ⟨c'',Normal x⟩ ⇒ s'"
by simp
from termi_c⇩2 [rule_format, OF this]
show "Γ⊢c⇩2 ↓ s'" .
next
case True
with fin obtain x' where s': "s'=Abrupt x'" and "c⇩f=Throw" "t=Normal x'"
by auto
from steps_Throw_impl_exec [OF rest [simplified this]] Normal
have "Γ⊢ ⟨c'',Normal x⟩ ⇒ Abrupt x'"
by simp
from termi_c⇩2 [rule_format, OF this] s'
show "Γ⊢c⇩2 ↓ s'" by simp
qed
next
case (Abrupt x)
from steps_Abrupt_prop [OF rest this]
have "t=Abrupt x" by simp
with fin have "s'=Abrupt x"
by (cases s') auto
thus "Γ⊢c⇩2 ↓ s'"
by auto
next
case (Fault f)
from steps_Fault_prop [OF rest this]
have "t=Fault f" by simp
with fin have "s'=Fault f"
by (cases s') auto
thus "Γ⊢c⇩2 ↓ s'"
by auto
next
case Stuck
from steps_Stuck_prop [OF rest this]
have "t=Stuck" by simp
with fin have "s'=Stuck"
by (cases s') auto
thus "Γ⊢c⇩2 ↓ s'"
by auto
qed
qed
qed
qed
next
case (Cond b c⇩1 c⇩2)
have hyp: "⋀c' s'. Γ⊢ (Cond b c⇩1 c⇩2, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
show ?case
proof (cases "s∈b")
case True
then have "Γ⊢ (Cond b c⇩1 c⇩2, Normal s) → (c⇩1, Normal s)"
by (rule step.CondTrue)
from hyp [OF this] have "Γ⊢c⇩1 ↓ Normal s".
with True show ?thesis
by (auto intro: terminates.intros)
next
case False
then have "Γ⊢ (Cond b c⇩1 c⇩2, Normal s) → (c⇩2, Normal s)"
by (rule step.CondFalse)
from hyp [OF this] have "Γ⊢c⇩2 ↓ Normal s".
with False show ?thesis
by (auto intro: terminates.intros)
qed
next
case (While b c)
have hyp: "⋀c' s'. Γ⊢ (While b c, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
show ?case
proof (cases "s∈b")
case True
then have "Γ⊢ (While b c, Normal s) → (Seq c (While b c), Normal s)"
by (rule step.WhileTrue)
from hyp [OF this] have "Γ⊢(Seq c (While b c)) ↓ Normal s".
with True show ?thesis
by (auto elim: terminates_Normal_elim_cases intro: terminates.intros)
next
case False
thus ?thesis
by (auto intro: terminates.intros)
qed
next
case (Call p)
have hyp: "⋀c' s'. Γ⊢ (Call p, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
show ?case
proof (cases "Γ p")
case None
thus ?thesis
by (auto intro: terminates.intros)
next
case (Some bdy)
then have "Γ⊢ (Call p, Normal s) → (bdy, Normal s)"
by (rule step.Call)
from hyp [OF this] have "Γ⊢bdy ↓ Normal s".
with Some show ?thesis
by (auto intro: terminates.intros)
qed
next
case (DynCom c)
have hyp: "⋀c' s'. Γ⊢ (DynCom c, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
have "Γ⊢ (DynCom c, Normal s) → (c s, Normal s)"
by (rule step.DynCom)
from hyp [OF this] have "Γ⊢c s ↓ Normal s".
then show ?case
by (auto intro: terminates.intros)
next
case (Guard f g c)
have hyp: "⋀c' s'. Γ⊢ (Guard f g c, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
show ?case
proof (cases "s∈g")
case True
then have "Γ⊢ (Guard f g c, Normal s) → (c, Normal s)"
by (rule step.Guard)
from hyp [OF this] have "Γ⊢c↓ Normal s".
with True show ?thesis
by (auto intro: terminates.intros)
next
case False
thus ?thesis
by (auto intro: terminates.intros)
qed
next
case Throw show ?case by (auto intro: terminates.intros)
next
case (Catch c⇩1 c⇩2)
have hyp: "⋀c' s'. Γ⊢ (Catch c⇩1 c⇩2, Normal s) → (c', s') ⟹ Γ⊢c' ↓ s'" by fact
show ?case
proof (rule terminates.Catch)
{
fix c' s'
assume step_c⇩1: "Γ⊢ (c⇩1, Normal s) → (c', s')"
have "Γ⊢c' ↓ s'"
proof -
from step_c⇩1
have "Γ⊢ (Catch c⇩1 c⇩2, Normal s) → (Catch c' c⇩2, s')"
by (rule step.Catch)
from hyp [OF this]
have "Γ⊢Catch c' c⇩2 ↓ s'".
thus "Γ⊢c'↓ s'"
by cases auto
qed
}
from Catch.hyps (1) [OF this]
show "Γ⊢c⇩1 ↓ Normal s".
next
show "∀s'. Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ Abrupt s' ⟶ Γ⊢c⇩2 ↓ Normal s'"
proof (intro allI impI)
fix s'
assume exec_c⇩1: "Γ⊢ ⟨c⇩1,Normal s⟩ ⇒ Abrupt s'"
show "Γ⊢c⇩2 ↓ Normal s'"
proof (cases "final (c⇩1,Normal s)")
case True
with exec_c⇩1
have Throw: "c⇩1=Throw"
by (auto simp add: final_def elim: exec_Normal_elim_cases)
have "Γ⊢(Catch Throw c⇩2,Normal s) → (c⇩2,Normal s)"
by (rule step.CatchThrow)
from hyp [simplified Throw, OF this]
have "Γ⊢c⇩2 ↓ Normal s".
moreover from exec_c⇩1 Throw
have "s'=s"
by (auto elim: exec_Normal_elim_cases)
ultimately show ?thesis by simp
next
case False
from exec_impl_steps [OF exec_c⇩1]
obtain c⇩f t where
steps_c⇩1: "Γ⊢ (c⇩1, Normal s) →⇧* (Throw, Normal s')"
by (fastforce split: xstate.splits)
from split_computation [OF steps_c⇩1 False]
obtain c'' s'' where
first: "Γ⊢ (c⇩1, Normal s) → (c'', s'')" and
rest: "Γ⊢ (c'', s'') →⇧* (Throw, Normal s')"
by (auto simp add: final_def)
from step.Catch [OF first]
have "Γ⊢ (Catch c⇩1 c⇩2, Normal s) → (Catch c'' c⇩2, s'')".
from hyp [OF this]
have "Γ⊢Catch c'' c⇩2 ↓ s''".
moreover
from steps_Throw_impl_exec [OF rest]
have "Γ⊢ ⟨c'',s''⟩ ⇒ Abrupt s'".
moreover
from rest obtain x where "s''=Normal x"
by (cases s'')
(auto dest: steps_Fault_prop steps_Abrupt_prop steps_Stuck_prop)
ultimately show ?thesis
by (fastforce elim: terminates_elim_cases)
qed
qed
qed
qed
lemma wf_implies_termi_reach:
assumes wf: "wf {(cfg2,cfg1). Γ ⊢ (c,s) →⇧* cfg1 ∧ Γ ⊢ cfg1 → cfg2}"
shows "⋀c1 s1. ⟦Γ ⊢ (c,s) →⇧* cfg1; cfg1=(c1,s1)⟧⟹ Γ⊢c1↓s1"
using wf
proof (induct cfg1, simp)
fix c1 s1
assume reach: "Γ⊢ (c, s) →⇧* (c1, s1)"
assume hyp_raw: "⋀y c2 s2.
⟦Γ⊢ (c1, s1) → (c2, s2); Γ⊢ (c, s) →⇧* (c2, s2); y = (c2, s2)⟧
⟹ Γ⊢c2 ↓ s2"
have hyp: "⋀c2 s2. Γ⊢ (c1, s1) → (c2, s2) ⟹ Γ⊢c2 ↓ s2"
apply -
apply (rule hyp_raw)
apply assumption
using reach
apply simp
apply (rule refl)
done
show "Γ⊢c1 ↓ s1"
proof (cases s1)
case (Normal s1')
with wf_implies_termi_reach_step_case [OF hyp [simplified Normal]]
show ?thesis
by auto
qed (auto intro: terminates.intros)
qed
theorem no_infinite_computation_impl_terminates:
assumes not_inf: "¬ Γ⊢ (c, s) → …(∞)"
shows "Γ⊢c↓s"
proof -
from no_infinite_computation_implies_wf [OF not_inf]
have wf: "wf {(c2, c1). Γ⊢(c, s) →⇧* c1 ∧ Γ⊢c1 → c2}".
show ?thesis
by (rule wf_implies_termi_reach [OF wf]) auto
qed
corollary terminates_iff_no_infinite_computation:
"Γ⊢c↓s = (¬ Γ⊢ (c, s) → …(∞))"
apply (rule)
apply (erule terminates_impl_no_infinite_computation)
apply (erule no_infinite_computation_impl_terminates)
done
subsection {* Generalised Redexes *}
text {*
For an important lemma for the completeness proof of the Hoare-logic for
total correctness we need a generalisation of @{const "redex"} that not only
yield the redex itself but all the enclosing statements as well.
*}
primrec redexes:: "('s,'p,'f)com ⇒ ('s,'p,'f)com set"
where
"redexes Skip = {Skip}" |
"redexes (Basic f) = {Basic f}" |
"redexes (Spec r) = {Spec r}" |
"redexes (Seq c⇩1 c⇩2) = {Seq c⇩1 c⇩2} ∪ redexes c⇩1" |
"redexes (Cond b c⇩1 c⇩2) = {Cond b c⇩1 c⇩2}" |
"redexes (While b c) = {While b c}" |
"redexes (Call p) = {Call p}" |
"redexes (DynCom d) = {DynCom d}" |
"redexes (Guard f b c) = {Guard f b c}" |
"redexes (Throw) = {Throw}" |
"redexes (Catch c⇩1 c⇩2) = {Catch c⇩1 c⇩2} ∪ redexes c⇩1"
lemma root_in_redexes: "c ∈ redexes c"
apply (induct c)
apply auto
done
lemma redex_in_redexes: "redex c ∈ redexes c"
apply (induct c)
apply auto
done
lemma redex_redexes: "⋀c'. ⟦c' ∈ redexes c; redex c' = c'⟧ ⟹ redex c = c'"
apply (induct c)
apply auto
done
lemma step_redexes:
shows "⋀r r'. ⟦Γ⊢(r,s) → (r',s'); r ∈ redexes c⟧
⟹ ∃c'. Γ⊢(c,s) → (c',s') ∧ r' ∈ redexes c'"
proof (induct c)
case Skip thus ?case by (fastforce intro: step.intros elim: step_elim_cases)
next
case Basic thus ?case by (fastforce intro: step.intros elim: step_elim_cases)
next
case Spec thus ?case by (fastforce intro: step.intros elim: step_elim_cases)
next
case (Seq c⇩1 c⇩2)
have "r ∈ redexes (Seq c⇩1 c⇩2)" by fact
hence r: "r = Seq c⇩1 c⇩2 ∨ r ∈ redexes c⇩1"
by simp
have step_r: "Γ⊢ (r, s) → (r', s')" by fact
from r show ?case
proof
assume "r = Seq c⇩1 c⇩2"
with step_r
show ?case
by (auto simp add: root_in_redexes)
next
assume r: "r ∈ redexes c⇩1"
from Seq.hyps (1) [OF step_r this]
obtain c' where
step_c⇩1: "Γ⊢ (c⇩1, s) → (c', s')" and
r': "r' ∈ redexes c'"
by blast
from step.Seq [OF step_c⇩1]
have "Γ⊢ (Seq c⇩1 c⇩2, s) → (Seq c' c⇩2, s')".
with r'
show ?case
by auto
qed
next
case Cond
thus ?case
by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes)
next
case While
thus ?case
by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes)
next
case Call thus ?case
by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes)
next
case DynCom thus ?case
by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes)
next
case Guard thus ?case
by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes)
next
case Throw thus ?case
by (fastforce intro: step.intros elim: step_elim_cases simp add: root_in_redexes)
next
case (Catch c⇩1 c⇩2)
have "r ∈ redexes (Catch c⇩1 c⇩2)" by fact
hence r: "r = Catch c⇩1 c⇩2 ∨ r ∈ redexes c⇩1"
by simp
have step_r: "Γ⊢ (r, s) → (r', s')" by fact
from r show ?case
proof
assume "r = Catch c⇩1 c⇩2"
with step_r
show ?case
by (auto simp add: root_in_redexes)
next
assume r: "r ∈ redexes c⇩1"
from Catch.hyps (1) [OF step_r this]
obtain c' where
step_c⇩1: "Γ⊢ (c⇩1, s) → (c', s')" and
r': "r' ∈ redexes c'"
by blast
from step.Catch [OF step_c⇩1]
have "Γ⊢ (Catch c⇩1 c⇩2, s) → (Catch c' c⇩2, s')".
with r'
show ?case
by auto
qed
qed
lemma steps_redexes:
assumes steps: "Γ⊢ (r, s) →⇧* (r', s')"
shows "⋀c. r ∈ redexes c ⟹ ∃c'. Γ⊢(c,s) →⇧* (c',s') ∧ r' ∈ redexes c'"
using steps
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl
then
show "∃c'. Γ⊢ (c, s') →⇧* (c', s') ∧ r' ∈ redexes c'"
by auto
next
case (Trans r s r'' s'')
have "Γ⊢ (r, s) → (r'', s'')" "r ∈ redexes c" by fact+
from step_redexes [OF this]
obtain c' where
step: "Γ⊢ (c, s) → (c', s'')" and
r'': "r'' ∈ redexes c'"
by blast
note step
also
from Trans.hyps (3) [OF r'']
obtain c'' where
steps: "Γ⊢ (c', s'') →⇧* (c'', s')" and
r': "r' ∈ redexes c''"
by blast
note steps
finally
show ?case
using r'
by blast
qed
lemma steps_redexes':
assumes steps: "Γ⊢ (r, s) →⇧+ (r', s')"
shows "⋀c. r ∈ redexes c ⟹ ∃c'. Γ⊢(c,s) →⇧+ (c',s') ∧ r' ∈ redexes c'"
using steps
proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans])
case (Step r' s' c')
have "Γ⊢ (r, s) → (r', s')" "r ∈ redexes c'" by fact+
from step_redexes [OF this]
show ?case
by (blast intro: r_into_trancl)
next
case (Trans r' s' r'' s'')
from Trans obtain c' where
steps: "Γ⊢ (c, s) →⇧+ (c', s')" and
r': "r' ∈ redexes c'"
by blast
note steps
moreover
have "Γ⊢ (r', s') → (r'', s'')" by fact
from step_redexes [OF this r'] obtain c'' where
step: "Γ⊢ (c', s') → (c'', s'')" and
r'': "r'' ∈ redexes c''"
by blast
note step
finally show ?case
using r'' by blast
qed
lemma step_redexes_Seq:
assumes step: "Γ⊢(r,s) → (r',s')"
assumes Seq: "Seq r c⇩2 ∈ redexes c"
shows "∃c'. Γ⊢(c,s) → (c',s') ∧ Seq r' c⇩2 ∈ redexes c'"
proof -
from step.Seq [OF step]
have "Γ⊢ (Seq r c⇩2, s) → (Seq r' c⇩2, s')".
from step_redexes [OF this Seq]
show ?thesis .
qed
lemma steps_redexes_Seq:
assumes steps: "Γ⊢ (r, s) →⇧* (r', s')"
shows "⋀c. Seq r c⇩2 ∈ redexes c ⟹
∃c'. Γ⊢(c,s) →⇧* (c',s') ∧ Seq r' c⇩2 ∈ redexes c'"
using steps
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl
then show ?case
by (auto)
next
case (Trans r s r'' s'')
have "Γ⊢ (r, s) → (r'', s'')" "Seq r c⇩2 ∈ redexes c" by fact+
from step_redexes_Seq [OF this]
obtain c' where
step: "Γ⊢ (c, s) → (c', s'')" and
r'': "Seq r'' c⇩2 ∈ redexes c'"
by blast
note step
also
from Trans.hyps (3) [OF r'']
obtain c'' where
steps: "Γ⊢ (c', s'') →⇧* (c'', s')" and
r': "Seq r' c⇩2 ∈ redexes c''"
by blast
note steps
finally
show ?case
using r'
by blast
qed
lemma steps_redexes_Seq':
assumes steps: "Γ⊢ (r, s) →⇧+ (r', s')"
shows "⋀c. Seq r c⇩2 ∈ redexes c
⟹ ∃c'. Γ⊢(c,s) →⇧+ (c',s') ∧ Seq r' c⇩2 ∈ redexes c'"
using steps
proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans])
case (Step r' s' c')
have "Γ⊢ (r, s) → (r', s')" "Seq r c⇩2 ∈ redexes c'" by fact+
from step_redexes_Seq [OF this]
show ?case
by (blast intro: r_into_trancl)
next
case (Trans r' s' r'' s'')
from Trans obtain c' where
steps: "Γ⊢ (c, s) →⇧+ (c', s')" and
r': "Seq r' c⇩2 ∈ redexes c'"
by blast
note steps
moreover
have "Γ⊢ (r', s') → (r'', s'')" by fact
from step_redexes_Seq [OF this r'] obtain c'' where
step: "Γ⊢ (c', s') → (c'', s'')" and
r'': "Seq r'' c⇩2 ∈ redexes c''"
by blast
note step
finally show ?case
using r'' by blast
qed
lemma step_redexes_Catch:
assumes step: "Γ⊢(r,s) → (r',s')"
assumes Catch: "Catch r c⇩2 ∈ redexes c"
shows "∃c'. Γ⊢(c,s) → (c',s') ∧ Catch r' c⇩2 ∈ redexes c'"
proof -
from step.Catch [OF step]
have "Γ⊢ (Catch r c⇩2, s) → (Catch r' c⇩2, s')".
from step_redexes [OF this Catch]
show ?thesis .
qed
lemma steps_redexes_Catch:
assumes steps: "Γ⊢ (r, s) →⇧* (r', s')"
shows "⋀c. Catch r c⇩2 ∈ redexes c ⟹
∃c'. Γ⊢(c,s) →⇧* (c',s') ∧ Catch r' c⇩2 ∈ redexes c'"
using steps
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
case Refl
then show ?case
by (auto)
next
case (Trans r s r'' s'')
have "Γ⊢ (r, s) → (r'', s'')" "Catch r c⇩2 ∈ redexes c" by fact+
from step_redexes_Catch [OF this]
obtain c' where
step: "Γ⊢ (c, s) → (c', s'')" and
r'': "Catch r'' c⇩2 ∈ redexes c'"
by blast
note step
also
from Trans.hyps (3) [OF r'']
obtain c'' where
steps: "Γ⊢ (c', s'') →⇧* (c'', s')" and
r': "Catch r' c⇩2 ∈ redexes c''"
by blast
note steps
finally
show ?case
using r'
by blast
qed
lemma steps_redexes_Catch':
assumes steps: "Γ⊢ (r, s) →⇧+ (r', s')"
shows "⋀c. Catch r c⇩2 ∈ redexes c
⟹ ∃c'. Γ⊢(c,s) →⇧+ (c',s') ∧ Catch r' c⇩2 ∈ redexes c'"
using steps
proof (induct rule: tranclp_induct2 [consumes 1, case_names Step Trans])
case (Step r' s' c')
have "Γ⊢ (r, s) → (r', s')" "Catch r c⇩2 ∈ redexes c'" by fact+
from step_redexes_Catch [OF this]
show ?case
by (blast intro: r_into_trancl)
next
case (Trans r' s' r'' s'')
from Trans obtain c' where
steps: "Γ⊢ (c, s) →⇧+ (c', s')" and
r': "Catch r' c⇩2 ∈ redexes c'"
by blast
note steps
moreover
have "Γ⊢ (r', s') → (r'', s'')" by fact
from step_redexes_Catch [OF this r'] obtain c'' where
step: "Γ⊢ (c', s') → (c'', s'')" and
r'': "Catch r'' c⇩2 ∈ redexes c''"
by blast
note step
finally show ?case
using r'' by blast
qed
lemma redexes_subset:"⋀c'. c' ∈ redexes c ⟹ redexes c' ⊆ redexes c"
by (induct c) auto
lemma redexes_preserves_termination:
assumes termi: "Γ⊢c↓s"
shows "⋀c'. c' ∈ redexes c ⟹ Γ⊢c'↓s"
using termi
by induct (auto intro: terminates.intros)
end