section {* Terminating Programs *}
theory Termination imports Semantic begin
subsection {* Inductive Characterisation: @{text "Γ⊢c↓s"}*}
inductive "terminates"::"('s,'p,'f) body ⇒ ('s,'p,'f) com ⇒ ('s,'f) xstate ⇒ bool"
("_⊢_ ↓ _" [60,20,60] 89)
for Γ::"('s,'p,'f) body"
where
Skip: "Γ⊢Skip ↓(Normal s)"
| Basic: "Γ⊢Basic f ↓(Normal s)"
| Spec: "Γ⊢Spec r ↓(Normal s)"
| Guard: "⟦s∈g; Γ⊢c↓(Normal s)⟧
⟹
Γ⊢Guard f g c↓(Normal s)"
| GuardFault: "s∉g
⟹
Γ⊢Guard f g c↓(Normal s)"
| Fault [intro,simp]: "Γ⊢c↓Fault f"
| Seq: "⟦Γ⊢c⇩1↓Normal s; ∀s'. Γ⊢⟨c⇩1,Normal s⟩ ⇒ s' ⟶ Γ⊢c⇩2↓s'⟧
⟹
Γ⊢Seq c⇩1 c⇩2↓(Normal s)"
| CondTrue: "⟦s ∈ b; Γ⊢c⇩1↓(Normal s)⟧
⟹
Γ⊢Cond b c⇩1 c⇩2↓(Normal s)"
| CondFalse: "⟦s ∉ b; Γ⊢c⇩2↓(Normal s)⟧
⟹
Γ⊢Cond b c⇩1 c⇩2↓(Normal s)"
| WhileTrue: "⟦s ∈ b; Γ⊢c↓(Normal s);
∀s'. Γ⊢⟨c,Normal s ⟩ ⇒ s' ⟶ Γ⊢While b c↓s'⟧
⟹
Γ⊢While b c↓(Normal s)"
| WhileFalse: "⟦s ∉ b⟧
⟹
Γ⊢While b c↓(Normal s)"
| Call: "⟦Γ p=Some bdy;Γ⊢bdy↓(Normal s)⟧
⟹
Γ⊢Call p↓(Normal s)"
| CallUndefined: "⟦Γ p = None⟧
⟹
Γ⊢Call p↓(Normal s)"
| Stuck [intro,simp]: "Γ⊢c↓Stuck"
| DynCom: "⟦Γ⊢(c s)↓(Normal s)⟧
⟹
Γ⊢DynCom c↓(Normal s)"
| Throw: "Γ⊢Throw↓(Normal s)"
| Abrupt [intro,simp]: "Γ⊢c↓Abrupt s"
| Catch: "⟦Γ⊢c⇩1↓Normal s;
∀s'. Γ⊢⟨c⇩1,Normal s ⟩ ⇒ Abrupt s' ⟶ Γ⊢c⇩2↓Normal s'⟧
⟹
Γ⊢Catch c⇩1 c⇩2↓Normal s"
inductive_cases terminates_elim_cases [cases set]:
"Γ⊢Skip ↓ s"
"Γ⊢Guard f g c ↓ s"
"Γ⊢Basic f ↓ s"
"Γ⊢Spec r ↓ s"
"Γ⊢Seq c1 c2 ↓ s"
"Γ⊢Cond b c1 c2 ↓ s"
"Γ⊢While b c ↓ s"
"Γ⊢Call p ↓ s"
"Γ⊢DynCom c ↓ s"
"Γ⊢Throw ↓ s"
"Γ⊢Catch c1 c2 ↓ s"
inductive_cases terminates_Normal_elim_cases [cases set]:
"Γ⊢Skip ↓ Normal s"
"Γ⊢Guard f g c ↓ Normal s"
"Γ⊢Basic f ↓ Normal s"
"Γ⊢Spec r ↓ Normal s"
"Γ⊢Seq c1 c2 ↓ Normal s"
"Γ⊢Cond b c1 c2 ↓ Normal s"
"Γ⊢While b c ↓ Normal s"
"Γ⊢Call p ↓ Normal s"
"Γ⊢DynCom c ↓ Normal s"
"Γ⊢Throw ↓ Normal s"
"Γ⊢Catch c1 c2 ↓ Normal s"
lemma terminates_Skip': "Γ⊢Skip ↓ s"
by (cases s) (auto intro: terminates.intros)
lemma terminates_Call_body:
"Γ p=Some bdy⟹Γ⊢Call p ↓s = Γ⊢(the (Γ p))↓s"
by (cases s)
(auto elim: terminates_Normal_elim_cases intro: terminates.intros)
lemma terminates_Normal_Call_body:
"p ∈ dom Γ ⟹
Γ⊢Call p ↓Normal s = Γ⊢(the (Γ p))↓Normal s"
by (auto elim: terminates_Normal_elim_cases intro: terminates.intros)
lemma terminates_implies_exec:
assumes terminates: "Γ⊢c↓s"
shows "∃t. Γ⊢⟨c,s⟩ ⇒ t"
using terminates
proof (induct)
case Skip thus ?case by (iprover intro: exec.intros)
next
case Basic thus ?case by (iprover intro: exec.intros)
next
case (Spec r s) thus ?case
by (cases "∃t. (s,t)∈ r") (auto intro: exec.intros)
next
case Guard thus ?case by (iprover intro: exec.intros)
next
case GuardFault thus ?case by (iprover intro: exec.intros)
next
case Fault thus ?case by (iprover intro: exec.intros)
next
case Seq thus ?case by (iprover intro: exec_Seq')
next
case CondTrue thus ?case by (iprover intro: exec.intros)
next
case CondFalse thus ?case by (iprover intro: exec.intros)
next
case WhileTrue thus ?case by (iprover intro: exec.intros)
next
case WhileFalse thus ?case by (iprover intro: exec.intros)
next
case (Call p bdy s)
then obtain s' where
"Γ⊢⟨bdy,Normal s ⟩ ⇒ s'"
by iprover
moreover have "Γ p = Some bdy" by fact
ultimately show ?case
by (cases s') (iprover intro: exec.intros)+
next
case CallUndefined thus ?case by (iprover intro: exec.intros)
next
case Stuck thus ?case by (iprover intro: exec.intros)
next
case DynCom thus ?case by (iprover intro: exec.intros)
next
case Throw thus ?case by (iprover intro: exec.intros)
next
case Abrupt thus ?case by (iprover intro: exec.intros)
next
case (Catch c1 s c2)
then obtain s' where exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ s'"
by iprover
thus ?case
proof (cases s')
case (Normal s'')
with exec_c1 show ?thesis by (auto intro!: exec.intros)
next
case (Abrupt s'')
with exec_c1 Catch.hyps
obtain t where "Γ⊢⟨c2,Normal s'' ⟩ ⇒ t"
by auto
with exec_c1 Abrupt show ?thesis by (auto intro: exec.intros)
next
case Fault
with exec_c1 show ?thesis by (auto intro!: exec.CatchMiss)
next
case Stuck
with exec_c1 show ?thesis by (auto intro!: exec.CatchMiss)
qed
qed
lemma terminates_block:
"⟦Γ⊢bdy ↓ Normal (init s);
∀t. Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t ⟶ Γ⊢c s t ↓ Normal (return s t)⟧
⟹ Γ⊢block init bdy return c ↓ Normal s"
apply (unfold block_def)
apply (fastforce intro: terminates.intros elim!: exec_Normal_elim_cases
dest!: not_isAbrD)
done
lemma terminates_block_elim [cases set, consumes 1]:
assumes termi: "Γ⊢block init bdy return c ↓ Normal s"
assumes e: "⟦Γ⊢bdy ↓ Normal (init s);
∀t. Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t ⟶ Γ⊢c s t ↓ Normal (return s t)
⟧ ⟹ P"
shows P
proof -
have "Γ⊢⟨Basic init,Normal s⟩ ⇒ Normal (init s)"
by (auto intro: exec.intros)
with termi
have "Γ⊢bdy ↓ Normal (init s)"
apply (unfold block_def)
apply (elim terminates_Normal_elim_cases)
by simp
moreover
{
fix t
assume exec_bdy: "Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t"
have "Γ⊢c s t ↓ Normal (return s t)"
proof -
from exec_bdy
have "Γ⊢⟨Catch (Seq (Basic init) bdy)
(Seq (Basic (return s)) Throw),Normal s⟩ ⇒ Normal t"
by (fastforce intro: exec.intros)
with termi have "Γ⊢DynCom (λt. Seq (Basic (return s)) (c s t)) ↓ Normal t"
apply (unfold block_def)
apply (elim terminates_Normal_elim_cases)
by simp
thus ?thesis
apply (elim terminates_Normal_elim_cases)
apply (auto intro: exec.intros)
done
qed
}
ultimately show P by (iprover intro: e)
qed
lemma terminates_call:
"⟦Γ p = Some bdy; Γ⊢bdy ↓ Normal (init s);
∀t. Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t ⟶ Γ⊢c s t ↓ Normal (return s t)⟧
⟹ Γ⊢call init p return c ↓ Normal s"
apply (unfold call_def)
apply (rule terminates_block)
apply (iprover intro: terminates.intros)
apply (auto elim: exec_Normal_elim_cases)
done
lemma terminates_callUndefined:
"⟦Γ p = None⟧
⟹ Γ⊢call init p return result ↓ Normal s"
apply (unfold call_def)
apply (rule terminates_block)
apply (iprover intro: terminates.intros)
apply (auto elim: exec_Normal_elim_cases)
done
lemma terminates_call_elim [cases set, consumes 1]:
assumes termi: "Γ⊢call init p return c ↓ Normal s"
assumes bdy: "⋀bdy. ⟦Γ p = Some bdy; Γ⊢bdy ↓ Normal (init s);
∀t. Γ⊢⟨bdy,Normal (init s)⟩ ⇒ Normal t ⟶ Γ⊢c s t ↓ Normal (return s t)⟧ ⟹ P"
assumes undef: "⟦Γ p = None⟧ ⟹ P"
shows P
apply (cases "Γ p")
apply (erule undef)
using termi
apply (unfold call_def)
apply (erule terminates_block_elim)
apply (erule terminates_Normal_elim_cases)
apply simp
apply (frule (1) bdy)
apply (fastforce intro: exec.intros)
apply assumption
apply simp
done
lemma terminates_dynCall:
"⟦Γ⊢call init (p s) return c ↓ Normal s⟧
⟹ Γ⊢dynCall init p return c ↓ Normal s"
apply (unfold dynCall_def)
apply (auto intro: terminates.intros terminates_call)
done
lemma terminates_dynCall_elim [cases set, consumes 1]:
assumes termi: "Γ⊢dynCall init p return c ↓ Normal s"
assumes "⟦Γ⊢call init (p s) return c ↓ Normal s⟧ ⟹ P"
shows P
using termi
apply (unfold dynCall_def)
apply (elim terminates_Normal_elim_cases)
apply fact
done
subsection {* Lemmas about @{const "sequence"}, @{const "flatten"} and
@{const "normalize"} *}
lemma terminates_sequence_app:
"⋀s. ⟦Γ⊢sequence Seq xs ↓ Normal s;
∀s'. Γ⊢⟨sequence Seq xs,Normal s ⟩ ⇒ s' ⟶ Γ⊢sequence Seq ys ↓ s'⟧
⟹ Γ⊢sequence Seq (xs @ ys) ↓ Normal s"
proof (induct xs)
case Nil
thus ?case by (auto intro: exec.intros)
next
case (Cons x xs)
have termi_x_xs: "Γ⊢sequence Seq (x # xs) ↓ Normal s" by fact
have termi_ys: "∀s'. Γ⊢⟨sequence Seq (x # xs),Normal s ⟩ ⇒ s' ⟶ Γ⊢sequence Seq ys ↓ s'" by fact
show ?case
proof (cases xs)
case Nil
with termi_x_xs termi_ys show ?thesis
by (cases ys) (auto intro: terminates.intros)
next
case Cons
from termi_x_xs Cons
have "Γ⊢x ↓ Normal s"
by (auto elim: terminates_Normal_elim_cases)
moreover
{
fix s'
assume exec_x: "Γ⊢⟨x,Normal s ⟩ ⇒ s'"
have "Γ⊢sequence Seq (xs @ ys) ↓ s'"
proof -
from exec_x termi_x_xs Cons
have termi_xs: "Γ⊢sequence Seq xs ↓ s'"
by (auto elim: terminates_Normal_elim_cases)
show ?thesis
proof (cases s')
case (Normal s'')
with exec_x termi_ys Cons
have "∀s'. Γ⊢⟨sequence Seq xs,Normal s'' ⟩ ⇒ s' ⟶ Γ⊢sequence Seq ys ↓ s'"
by (auto intro: exec.intros)
from Cons.hyps [OF termi_xs [simplified Normal] this]
have "Γ⊢sequence Seq (xs @ ys) ↓ Normal s''".
with Normal show ?thesis by simp
next
case Abrupt thus ?thesis by (auto intro: terminates.intros)
next
case Fault thus ?thesis by (auto intro: terminates.intros)
next
case Stuck thus ?thesis by (auto intro: terminates.intros)
qed
qed
}
ultimately show ?thesis
using Cons
by (auto intro: terminates.intros)
qed
qed
lemma terminates_sequence_appD:
"⋀s. Γ⊢sequence Seq (xs @ ys) ↓ Normal s
⟹ Γ⊢sequence Seq xs ↓ Normal s ∧
(∀s'. Γ⊢⟨sequence Seq xs,Normal s ⟩ ⇒ s' ⟶ Γ⊢sequence Seq ys ↓ s')"
proof (induct xs)
case Nil
thus ?case
by (auto elim: terminates_Normal_elim_cases exec_Normal_elim_cases
intro: terminates.intros)
next
case (Cons x xs)
have termi_x_xs_ys: "Γ⊢sequence Seq ((x # xs) @ ys) ↓ Normal s" by fact
show ?case
proof (cases xs)
case Nil
with termi_x_xs_ys show ?thesis
by (cases ys)
(auto elim: terminates_Normal_elim_cases exec_Normal_elim_cases
intro: terminates_Skip')
next
case Cons
with termi_x_xs_ys
obtain termi_x: "Γ⊢x ↓ Normal s" and
termi_xs_ys: "∀s'. Γ⊢⟨x,Normal s ⟩ ⇒ s' ⟶ Γ⊢sequence Seq (xs@ys) ↓ s'"
by (auto elim: terminates_Normal_elim_cases)
have "Γ⊢Seq x (sequence Seq xs) ↓ Normal s"
proof (rule terminates.Seq [rule_format])
show "Γ⊢x ↓ Normal s" by (rule termi_x)
next
fix s'
assume exec_x: "Γ⊢⟨x,Normal s ⟩ ⇒ s'"
show "Γ⊢sequence Seq xs ↓ s'"
proof -
from termi_xs_ys [rule_format, OF exec_x]
have termi_xs_ys': "Γ⊢sequence Seq (xs@ys) ↓ s'" .
show ?thesis
proof (cases s')
case (Normal s'')
from Cons.hyps [OF termi_xs_ys' [simplified Normal]]
show ?thesis
using Normal by auto
next
case Abrupt thus ?thesis by (auto intro: terminates.intros)
next
case Fault thus ?thesis by (auto intro: terminates.intros)
next
case Stuck thus ?thesis by (auto intro: terminates.intros)
qed
qed
qed
moreover
{
fix s'
assume exec_x_xs: "Γ⊢⟨Seq x (sequence Seq xs),Normal s ⟩ ⇒ s'"
have "Γ⊢sequence Seq ys ↓ s'"
proof -
from exec_x_xs obtain t where
exec_x: "Γ⊢⟨x,Normal s ⟩ ⇒ t" and
exec_xs: "Γ⊢⟨sequence Seq xs,t ⟩ ⇒ s'"
by cases
show ?thesis
proof (cases t)
case (Normal t')
with exec_x termi_xs_ys have "Γ⊢sequence Seq (xs@ys) ↓ Normal t'"
by auto
from Cons.hyps [OF this] exec_xs Normal
show ?thesis
by auto
next
case (Abrupt t')
with exec_xs have "s'=Abrupt t'"
by (auto dest: Abrupt_end)
thus ?thesis by (auto intro: terminates.intros)
next
case (Fault f)
with exec_xs have "s'=Fault f"
by (auto dest: Fault_end)
thus ?thesis by (auto intro: terminates.intros)
next
case Stuck
with exec_xs have "s'=Stuck"
by (auto dest: Stuck_end)
thus ?thesis by (auto intro: terminates.intros)
qed
qed
}
ultimately show ?thesis
using Cons
by auto
qed
qed
lemma terminates_sequence_appE [consumes 1]:
"⟦Γ⊢sequence Seq (xs @ ys) ↓ Normal s;
⟦Γ⊢sequence Seq xs ↓ Normal s;
∀s'. Γ⊢⟨sequence Seq xs,Normal s ⟩ ⇒ s' ⟶ Γ⊢sequence Seq ys ↓ s'⟧ ⟹ P⟧
⟹ P"
by (auto dest: terminates_sequence_appD)
lemma terminates_to_terminates_sequence_flatten:
assumes termi: "Γ⊢c↓s"
shows "Γ⊢sequence Seq (flatten c)↓s"
using termi
by (induct)
(auto intro: terminates.intros terminates_sequence_app
exec_sequence_flatten_to_exec)
lemma terminates_to_terminates_normalize:
assumes termi: "Γ⊢c↓s"
shows "Γ⊢normalize c↓s"
using termi
proof induct
case Seq
thus ?case
by (fastforce intro: terminates.intros terminates_sequence_app
terminates_to_terminates_sequence_flatten
dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
next
case WhileTrue
thus ?case
by (fastforce intro: terminates.intros terminates_sequence_app
terminates_to_terminates_sequence_flatten
dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
next
case Catch
thus ?case
by (fastforce intro: terminates.intros terminates_sequence_app
terminates_to_terminates_sequence_flatten
dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
qed (auto intro: terminates.intros)
lemma terminates_sequence_flatten_to_terminates:
shows "⋀s. Γ⊢sequence Seq (flatten c)↓s ⟹ Γ⊢c↓s"
proof (induct c)
case (Seq c1 c2)
have "Γ⊢sequence Seq (flatten (Seq c1 c2)) ↓ s" by fact
hence termi_app: "Γ⊢sequence Seq (flatten c1 @ flatten c2) ↓ s" by simp
show ?case
proof (cases s)
case (Normal s')
have "Γ⊢Seq c1 c2 ↓ Normal s'"
proof (rule terminates.Seq [rule_format])
from termi_app [simplified Normal]
have "Γ⊢sequence Seq (flatten c1) ↓ Normal s'"
by (cases rule: terminates_sequence_appE)
with Seq.hyps
show "Γ⊢c1 ↓ Normal s'"
by simp
next
fix s''
assume "Γ⊢⟨c1,Normal s' ⟩ ⇒ s''"
from termi_app [simplified Normal] exec_to_exec_sequence_flatten [OF this]
have "Γ⊢sequence Seq (flatten c2) ↓ s''"
by (cases rule: terminates_sequence_appE) auto
with Seq.hyps
show "Γ⊢c2 ↓ s''"
by simp
qed
with Normal show ?thesis
by simp
qed (auto intro: terminates.intros)
qed (auto intro: terminates.intros)
lemma terminates_normalize_to_terminates:
shows "⋀s. Γ⊢normalize c↓s ⟹ Γ⊢c↓s"
proof (induct c)
case Skip thus ?case by (auto intro: terminates_Skip')
next
case Basic thus ?case by (cases s) (auto intro: terminates.intros)
next
case Spec thus ?case by (cases s) (auto intro: terminates.intros)
next
case (Seq c1 c2)
have "Γ⊢normalize (Seq c1 c2) ↓ s" by fact
hence termi_app: "Γ⊢sequence Seq (flatten (normalize c1) @ flatten (normalize c2)) ↓ s"
by simp
show ?case
proof (cases s)
case (Normal s')
have "Γ⊢Seq c1 c2 ↓ Normal s'"
proof (rule terminates.Seq [rule_format])
from termi_app [simplified Normal]
have "Γ⊢sequence Seq (flatten (normalize c1)) ↓ Normal s'"
by (cases rule: terminates_sequence_appE)
from terminates_sequence_flatten_to_terminates [OF this] Seq.hyps
show "Γ⊢c1 ↓ Normal s'"
by simp
next
fix s''
assume "Γ⊢⟨c1,Normal s' ⟩ ⇒ s''"
from exec_to_exec_normalize [OF this]
have "Γ⊢⟨normalize c1,Normal s' ⟩ ⇒ s''" .
from termi_app [simplified Normal] exec_to_exec_sequence_flatten [OF this]
have "Γ⊢sequence Seq (flatten (normalize c2)) ↓ s''"
by (cases rule: terminates_sequence_appE) auto
from terminates_sequence_flatten_to_terminates [OF this] Seq.hyps
show "Γ⊢c2 ↓ s''"
by simp
qed
with Normal show ?thesis by simp
qed (auto intro: terminates.intros)
next
case (Cond b c1 c2)
thus ?case
by (cases s)
(auto intro: terminates.intros elim!: terminates_Normal_elim_cases)
next
case (While b c)
have "Γ⊢normalize (While b c) ↓ s" by fact
hence termi_norm_w: "Γ⊢While b (normalize c) ↓ s" by simp
{
fix t w
assume termi_w: "Γ⊢ w ↓ t"
have "w=While b (normalize c) ⟹ Γ⊢While b c ↓ t"
using termi_w
proof (induct)
case (WhileTrue t' b' c')
from WhileTrue obtain
t'_b: "t' ∈ b" and
termi_norm_c: "Γ⊢normalize c ↓ Normal t'" and
termi_norm_w': "∀s'. Γ⊢⟨normalize c,Normal t' ⟩ ⇒ s' ⟶ Γ⊢While b c ↓ s'"
by auto
from While.hyps [OF termi_norm_c]
have "Γ⊢c ↓ Normal t'".
moreover
from termi_norm_w'
have "∀s'. Γ⊢⟨c,Normal t' ⟩ ⇒ s' ⟶ Γ⊢While b c ↓ s'"
by (auto intro: exec_to_exec_normalize)
ultimately show ?case
using t'_b
by (auto intro: terminates.intros)
qed (auto intro: terminates.intros)
}
from this [OF termi_norm_w]
show ?case
by auto
next
case Call thus ?case by simp
next
case DynCom thus ?case
by (cases s) (auto intro: terminates.intros rangeI elim: terminates_Normal_elim_cases)
next
case Guard thus ?case
by (cases s) (auto intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case Throw thus ?case by (cases s) (auto intro: terminates.intros)
next
case Catch
thus ?case
by (cases s)
(auto dest: exec_to_exec_normalize elim!: terminates_Normal_elim_cases
intro!: terminates.Catch)
qed
lemma terminates_iff_terminates_normalize:
"Γ⊢normalize c↓s = Γ⊢c↓s"
by (auto intro: terminates_to_terminates_normalize
terminates_normalize_to_terminates)
subsection {* Lemmas about @{const "strip_guards"} *}
lemma terminates_strip_guards_to_terminates: "⋀s. Γ⊢strip_guards F c↓s ⟹ Γ⊢c↓s"
proof (induct c)
case Skip thus ?case by simp
next
case Basic thus ?case by simp
next
case Spec thus ?case by simp
next
case (Seq c1 c2)
hence "Γ⊢Seq (strip_guards F c1) (strip_guards F c2) ↓ s" by simp
thus "Γ⊢Seq c1 c2 ↓ s"
proof (cases)
fix f assume "s=Fault f" thus ?thesis by simp
next
assume "s=Stuck" thus ?thesis by simp
next
fix s' assume "s=Abrupt s'" thus ?thesis by simp
next
fix s'
assume s: "s=Normal s'"
assume "Γ⊢strip_guards F c1 ↓ Normal s'"
hence "Γ⊢c1 ↓ Normal s'"
by (rule Seq.hyps)
moreover
assume c2:
"∀s''. Γ⊢⟨strip_guards F c1,Normal s'⟩ ⇒ s'' ⟶ Γ⊢strip_guards F c2↓s''"
{
fix s'' assume exec_c1: "Γ⊢⟨c1,Normal s' ⟩ ⇒ s''"
have " Γ⊢c2 ↓ s''"
proof (cases s'')
case (Normal s''')
with exec_c1
have "Γ⊢⟨strip_guards F c1,Normal s' ⟩ ⇒ s''"
by (auto intro: exec_to_exec_strip_guards)
with c2
show ?thesis
by (iprover intro: Seq.hyps)
next
case (Abrupt s''')
with exec_c1
have "Γ⊢⟨strip_guards F c1,Normal s' ⟩ ⇒ s''"
by (auto intro: exec_to_exec_strip_guards )
with c2
show ?thesis
by (iprover intro: Seq.hyps)
next
case Fault thus ?thesis by simp
next
case Stuck thus ?thesis by simp
qed
}
ultimately show ?thesis
using s
by (iprover intro: terminates.intros)
qed
next
case (Cond b c1 c2)
hence "Γ⊢Cond b (strip_guards F c1) (strip_guards F c2) ↓ s" by simp
thus "Γ⊢Cond b c1 c2 ↓ s"
proof (cases)
fix f assume "s=Fault f" thus ?thesis by simp
next
assume "s=Stuck" thus ?thesis by simp
next
fix s' assume "s=Abrupt s'" thus ?thesis by simp
next
fix s'
assume "s'∈b" "Γ⊢strip_guards F c1 ↓ Normal s'" "s = Normal s'"
thus ?thesis
by (iprover intro: terminates.intros Cond.hyps)
next
fix s'
assume "s'∉b" "Γ⊢strip_guards F c2 ↓ Normal s'" "s = Normal s'"
thus ?thesis
by (iprover intro: terminates.intros Cond.hyps)
qed
next
case (While b c)
have hyp_c: "⋀s. Γ⊢strip_guards F c ↓ s ⟹ Γ⊢c ↓ s" by fact
have "Γ⊢While b (strip_guards F c) ↓ s" using While.prems by simp
moreover
{
fix sw
assume "Γ⊢sw↓s"
then have "sw=While b (strip_guards F c) ⟹
Γ⊢While b c ↓ s"
proof (induct)
case (WhileTrue s b' c')
have eqs: "While b' c' = While b (strip_guards F c)" by fact
with `s∈b'` have b: "s∈b" by simp
from eqs `Γ⊢c' ↓ Normal s` have "Γ⊢strip_guards F c ↓ Normal s"
by simp
hence term_c: "Γ⊢c ↓ Normal s"
by (rule hyp_c)
moreover
{
fix t
assume exec_c: "Γ⊢⟨c,Normal s ⟩ ⇒ t"
have "Γ⊢While b c ↓ t"
proof (cases t)
case Fault
thus ?thesis by simp
next
case Stuck
thus ?thesis by simp
next
case (Abrupt t')
thus ?thesis by simp
next
case (Normal t')
with exec_c
have "Γ⊢⟨strip_guards F c,Normal s ⟩ ⇒ Normal t'"
by (auto intro: exec_to_exec_strip_guards)
with WhileTrue.hyps eqs Normal
show ?thesis
by fastforce
qed
}
ultimately
show ?case
using b
by (auto intro: terminates.intros)
next
case WhileFalse thus ?case by (auto intro: terminates.intros)
qed simp_all
}
ultimately show "Γ⊢While b c ↓ s"
by auto
next
case Call thus ?case by simp
next
case DynCom thus ?case
by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros rangeI)
next
case Guard
thus ?case
by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros
split: if_split_asm)
next
case Throw thus ?case by simp
next
case (Catch c1 c2)
hence "Γ⊢Catch (strip_guards F c1) (strip_guards F c2) ↓ s" by simp
thus "Γ⊢Catch c1 c2 ↓ s"
proof (cases)
fix f assume "s=Fault f" thus ?thesis by simp
next
assume "s=Stuck" thus ?thesis by simp
next
fix s' assume "s=Abrupt s'" thus ?thesis by simp
next
fix s'
assume s: "s=Normal s'"
assume "Γ⊢strip_guards F c1 ↓ Normal s'"
hence "Γ⊢c1 ↓ Normal s'"
by (rule Catch.hyps)
moreover
assume c2:
"∀s''. Γ⊢⟨strip_guards F c1,Normal s'⟩ ⇒ Abrupt s''
⟶ Γ⊢strip_guards F c2↓Normal s''"
{
fix s'' assume exec_c1: "Γ⊢⟨c1,Normal s' ⟩ ⇒ Abrupt s''"
have " Γ⊢c2 ↓ Normal s''"
proof -
from exec_c1
have "Γ⊢⟨strip_guards F c1,Normal s' ⟩ ⇒ Abrupt s''"
by (auto intro: exec_to_exec_strip_guards)
with c2
show ?thesis
by (auto intro: Catch.hyps)
qed
}
ultimately show ?thesis
using s
by (iprover intro: terminates.intros)
qed
qed
lemma terminates_strip_to_terminates:
assumes termi_strip: "strip F Γ⊢c↓s"
shows "Γ⊢c↓s"
using termi_strip
proof induct
case (Seq c1 s c2)
have "Γ⊢c1 ↓ Normal s" by fact
moreover
{
fix s'
assume exec: "Γ⊢ ⟨c1,Normal s⟩ ⇒ s'"
have "Γ⊢c2 ↓ s'"
proof (cases "isFault s'")
case True
thus ?thesis
by (auto elim: isFaultE)
next
case False
from exec_to_exec_strip [OF exec this] Seq.hyps
show ?thesis
by auto
qed
}
ultimately show ?case
by (auto intro: terminates.intros)
next
case (WhileTrue s b c)
have "Γ⊢c ↓ Normal s" by fact
moreover
{
fix s'
assume exec: "Γ⊢ ⟨c,Normal s⟩ ⇒ s'"
have "Γ⊢While b c ↓ s'"
proof (cases "isFault s'")
case True
thus ?thesis
by (auto elim: isFaultE)
next
case False
from exec_to_exec_strip [OF exec this] WhileTrue.hyps
show ?thesis
by auto
qed
}
ultimately show ?case
by (auto intro: terminates.intros)
next
case (Catch c1 s c2)
have "Γ⊢c1 ↓ Normal s" by fact
moreover
{
fix s'
assume exec: "Γ⊢ ⟨c1,Normal s⟩ ⇒ Abrupt s'"
from exec_to_exec_strip [OF exec] Catch.hyps
have "Γ⊢c2 ↓ Normal s'"
by auto
}
ultimately show ?case
by (auto intro: terminates.intros)
next
case Call thus ?case
by (auto intro: terminates.intros terminates_strip_guards_to_terminates)
qed (auto intro: terminates.intros)
subsection {* Lemmas about @{term "c⇩1 ∩⇩g c⇩2"} *}
lemma inter_guards_terminates:
"⋀c c2 s. ⟦(c1 ∩⇩g c2) = Some c; Γ⊢c1↓s ⟧
⟹ Γ⊢c↓s"
proof (induct c1)
case Skip thus ?case by (fastforce simp add: inter_guards_Skip)
next
case (Basic f) thus ?case by (fastforce simp add: inter_guards_Basic)
next
case (Spec r) thus ?case by (fastforce simp add: inter_guards_Spec)
next
case (Seq a1 a2)
have "(Seq a1 a2 ∩⇩g c2) = Some c" by fact
then obtain b1 b2 d1 d2 where
c2: "c2=Seq b1 b2" and
d1: "(a1 ∩⇩g b1) = Some d1" and d2: "(a2 ∩⇩g b2) = Some d2" and
c: "c=Seq d1 d2"
by (auto simp add: inter_guards_Seq)
have termi_c1: "Γ⊢Seq a1 a2 ↓ s" by fact
have "Γ⊢Seq d1 d2 ↓ s"
proof (cases s)
case Fault thus ?thesis by simp
next
case Stuck thus ?thesis by simp
next
case Abrupt thus ?thesis by simp
next
case (Normal s')
note Normal_s = this
with d1 termi_c1
have "Γ⊢d1 ↓ Normal s'"
by (auto elim: terminates_Normal_elim_cases intro: Seq.hyps)
moreover
{
fix t
assume exec_d1: "Γ⊢⟨d1,Normal s' ⟩ ⇒ t"
have "Γ⊢d2 ↓ t"
proof (cases t)
case Fault thus ?thesis by simp
next
case Stuck thus ?thesis by simp
next
case Abrupt thus ?thesis by simp
next
case (Normal t')
with inter_guards_exec_noFault [OF d1 exec_d1]
have "Γ⊢⟨a1,Normal s' ⟩ ⇒ Normal t'"
by simp
with termi_c1 Normal_s have "Γ⊢a2 ↓ Normal t'"
by (auto elim: terminates_Normal_elim_cases)
with d2 have "Γ⊢d2 ↓ Normal t'"
by (auto intro: Seq.hyps)
with Normal show ?thesis by simp
qed
}
ultimately have "Γ⊢Seq d1 d2 ↓ Normal s'"
by (fastforce intro: terminates.intros)
with Normal show ?thesis by simp
qed
with c show ?case by simp
next
case Cond thus ?case
by - (cases s,
auto intro: terminates.intros elim!: terminates_Normal_elim_cases
simp add: inter_guards_Cond)
next
case (While b bdy1)
have "(While b bdy1 ∩⇩g c2) = Some c" by fact
then obtain bdy2 bdy where
c2: "c2=While b bdy2" and
bdy: "(bdy1 ∩⇩g bdy2) = Some bdy" and
c: "c=While b bdy"
by (auto simp add: inter_guards_While)
have "Γ⊢While b bdy1 ↓ s" by fact
moreover
{
fix s w w1 w2
assume termi_w: "Γ⊢w ↓ s"
assume w: "w=While b bdy1"
from termi_w w
have "Γ⊢While b bdy ↓ s"
proof (induct)
case (WhileTrue s b' bdy1')
have eqs: "While b' bdy1' = While b bdy1" by fact
from WhileTrue have s_in_b: "s ∈ b" by simp
from WhileTrue have termi_bdy1: "Γ⊢bdy1 ↓ Normal s" by simp
show ?case
proof -
from bdy termi_bdy1
have "Γ⊢bdy↓(Normal s)"
by (rule While.hyps)
moreover
{
fix t
assume exec_bdy: "Γ⊢⟨bdy,Normal s ⟩ ⇒ t"
have "Γ⊢While b bdy↓t"
proof (cases t)
case Fault thus ?thesis by simp
next
case Stuck thus ?thesis by simp
next
case Abrupt thus ?thesis by simp
next
case (Normal t')
with inter_guards_exec_noFault [OF bdy exec_bdy]
have "Γ⊢⟨bdy1,Normal s ⟩ ⇒ Normal t'"
by simp
with WhileTrue have "Γ⊢While b bdy ↓ Normal t'"
by simp
with Normal show ?thesis by simp
qed
}
ultimately show ?thesis
using s_in_b
by (blast intro: terminates.WhileTrue)
qed
next
case WhileFalse thus ?case
by (blast intro: terminates.WhileFalse)
qed (simp_all)
}
ultimately
show ?case using c by simp
next
case Call thus ?case by (simp add: inter_guards_Call)
next
case (DynCom f1)
have "(DynCom f1 ∩⇩g c2) = Some c" by fact
then obtain f2 f where
c2: "c2=DynCom f2" and
f_defined: "∀s. ((f1 s) ∩⇩g (f2 s)) ≠ None" and
c: "c=DynCom (λs. the ((f1 s) ∩⇩g (f2 s)))"
by (auto simp add: inter_guards_DynCom)
have termi: "Γ⊢DynCom f1 ↓ s" by fact
show ?case
proof (cases s)
case Fault thus ?thesis by simp
next
case Stuck thus ?thesis by simp
next
case Abrupt thus ?thesis by simp
next
case (Normal s')
from f_defined obtain f where f: "((f1 s') ∩⇩g (f2 s')) = Some f"
by auto
from Normal termi
have "Γ⊢f1 s'↓ (Normal s')"
by (auto elim: terminates_Normal_elim_cases)
from DynCom.hyps f this
have "Γ⊢f↓ (Normal s')"
by blast
with c f Normal
show ?thesis
by (auto intro: terminates.intros)
qed
next
case (Guard f g1 bdy1)
have "(Guard f g1 bdy1 ∩⇩g c2) = Some c" by fact
then obtain g2 bdy2 bdy where
c2: "c2=Guard f g2 bdy2" and
bdy: "(bdy1 ∩⇩g bdy2) = Some bdy" and
c: "c=Guard f (g1 ∩ g2) bdy"
by (auto simp add: inter_guards_Guard)
have termi_c1: "Γ⊢Guard f g1 bdy1 ↓ s" by fact
show ?case
proof (cases s)
case Fault thus ?thesis by simp
next
case Stuck thus ?thesis by simp
next
case Abrupt thus ?thesis by simp
next
case (Normal s')
show ?thesis
proof (cases "s' ∈ g1")
case False
with Normal c show ?thesis by (auto intro: terminates.GuardFault)
next
case True
note s_in_g1 = this
show ?thesis
proof (cases "s' ∈ g2")
case False
with Normal c show ?thesis by (auto intro: terminates.GuardFault)
next
case True
with termi_c1 s_in_g1 Normal have "Γ⊢bdy1 ↓ Normal s'"
by (auto elim: terminates_Normal_elim_cases)
with c bdy Guard.hyps Normal True s_in_g1
show ?thesis by (auto intro: terminates.Guard)
qed
qed
qed
next
case Throw thus ?case
by (auto simp add: inter_guards_Throw)
next
case (Catch a1 a2)
have "(Catch a1 a2 ∩⇩g c2) = Some c" by fact
then obtain b1 b2 d1 d2 where
c2: "c2=Catch b1 b2" and
d1: "(a1 ∩⇩g b1) = Some d1" and d2: "(a2 ∩⇩g b2) = Some d2" and
c: "c=Catch d1 d2"
by (auto simp add: inter_guards_Catch)
have termi_c1: "Γ⊢Catch a1 a2 ↓ s" by fact
have "Γ⊢Catch d1 d2 ↓ s"
proof (cases s)
case Fault thus ?thesis by simp
next
case Stuck thus ?thesis by simp
next
case Abrupt thus ?thesis by simp
next
case (Normal s')
note Normal_s = this
with d1 termi_c1
have "Γ⊢d1 ↓ Normal s'"
by (auto elim: terminates_Normal_elim_cases intro: Catch.hyps)
moreover
{
fix t
assume exec_d1: "Γ⊢⟨d1,Normal s' ⟩ ⇒ Abrupt t"
have "Γ⊢d2 ↓ Normal t"
proof -
from inter_guards_exec_noFault [OF d1 exec_d1]
have "Γ⊢⟨a1,Normal s' ⟩ ⇒ Abrupt t"
by simp
with termi_c1 Normal_s have "Γ⊢a2 ↓ Normal t"
by (auto elim: terminates_Normal_elim_cases)
with d2 have "Γ⊢d2 ↓ Normal t"
by (auto intro: Catch.hyps)
with Normal show ?thesis by simp
qed
}
ultimately have "Γ⊢Catch d1 d2 ↓ Normal s'"
by (fastforce intro: terminates.intros)
with Normal show ?thesis by simp
qed
with c show ?case by simp
qed
lemma inter_guards_terminates':
assumes c: "(c1 ∩⇩g c2) = Some c"
assumes termi_c2: "Γ⊢c2↓s"
shows "Γ⊢c↓s"
proof -
from c have "(c2 ∩⇩g c1) = Some c"
by (rule inter_guards_sym)
from this termi_c2 show ?thesis
by (rule inter_guards_terminates)
qed
subsection {* Lemmas about @{const "mark_guards"} *}
lemma terminates_to_terminates_mark_guards:
assumes termi: "Γ⊢c↓s"
shows "Γ⊢mark_guards f c↓s"
using termi
proof (induct)
case Skip thus ?case by (fastforce intro: terminates.intros)
next
case Basic thus ?case by (fastforce intro: terminates.intros)
next
case Spec thus ?case by (fastforce intro: terminates.intros)
next
case Guard thus ?case by (fastforce intro: terminates.intros)
next
case GuardFault thus ?case by (fastforce intro: terminates.intros)
next
case Fault thus ?case by (fastforce intro: terminates.intros)
next
case (Seq c1 s c2)
have "Γ⊢mark_guards f c1 ↓ Normal s" by fact
moreover
{
fix t
assume exec_mark: "Γ⊢⟨mark_guards f c1,Normal s ⟩ ⇒ t"
have "Γ⊢mark_guards f c2 ↓ t"
proof -
from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ t'" and
t_Fault: "isFault t ⟶ isFault t'" and
t'_Fault_f: "t' = Fault f ⟶ t' = t" and
t'_Fault: "isFault t' ⟶ isFault t" and
t'_noFault: "¬ isFault t' ⟶ t' = t"
by blast
show ?thesis
proof (cases "isFault t'")
case True
with t'_Fault have "isFault t" by simp
thus ?thesis
by (auto elim: isFaultE)
next
case False
with t'_noFault have "t'=t" by simp
with exec_c1 Seq.hyps
show ?thesis
by auto
qed
qed
}
ultimately show ?case
by (auto intro: terminates.intros)
next
case CondTrue thus ?case by (fastforce intro: terminates.intros)
next
case CondFalse thus ?case by (fastforce intro: terminates.intros)
next
case (WhileTrue s b c)
have s_in_b: "s ∈ b" by fact
have "Γ⊢mark_guards f c ↓ Normal s" by fact
moreover
{
fix t
assume exec_mark: "Γ⊢⟨mark_guards f c,Normal s ⟩ ⇒ t"
have "Γ⊢mark_guards f (While b c) ↓ t"
proof -
from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
exec_c1: "Γ⊢⟨c,Normal s ⟩ ⇒ t'" and
t_Fault: "isFault t ⟶ isFault t'" and
t'_Fault_f: "t' = Fault f ⟶ t' = t" and
t'_Fault: "isFault t' ⟶ isFault t" and
t'_noFault: "¬ isFault t' ⟶ t' = t"
by blast
show ?thesis
proof (cases "isFault t'")
case True
with t'_Fault have "isFault t" by simp
thus ?thesis
by (auto elim: isFaultE)
next
case False
with t'_noFault have "t'=t" by simp
with exec_c1 WhileTrue.hyps
show ?thesis
by auto
qed
qed
}
ultimately show ?case
by (auto intro: terminates.intros)
next
case WhileFalse thus ?case by (fastforce intro: terminates.intros)
next
case Call thus ?case by (fastforce intro: terminates.intros)
next
case CallUndefined thus ?case by (fastforce intro: terminates.intros)
next
case Stuck thus ?case by (fastforce intro: terminates.intros)
next
case DynCom thus ?case by (fastforce intro: terminates.intros)
next
case Throw thus ?case by (fastforce intro: terminates.intros)
next
case Abrupt thus ?case by (fastforce intro: terminates.intros)
next
case (Catch c1 s c2)
have "Γ⊢mark_guards f c1 ↓ Normal s" by fact
moreover
{
fix t
assume exec_mark: "Γ⊢⟨mark_guards f c1,Normal s ⟩ ⇒ Abrupt t"
have "Γ⊢mark_guards f c2 ↓ Normal t"
proof -
from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ t'" and
t'_Fault_f: "t' = Fault f ⟶ t' = Abrupt t" and
t'_Fault: "isFault t' ⟶ isFault (Abrupt t)" and
t'_noFault: "¬ isFault t' ⟶ t' = Abrupt t"
by fastforce
show ?thesis
proof (cases "isFault t'")
case True
with t'_Fault have "isFault (Abrupt t)" by simp
thus ?thesis by simp
next
case False
with t'_noFault have "t'=Abrupt t" by simp
with exec_c1 Catch.hyps
show ?thesis
by auto
qed
qed
}
ultimately show ?case
by (auto intro: terminates.intros)
qed
lemma terminates_mark_guards_to_terminates_Normal:
"⋀s. Γ⊢mark_guards f c↓Normal s ⟹ Γ⊢c↓Normal s"
proof (induct c)
case Skip thus ?case by (fastforce intro: terminates.intros)
next
case Basic thus ?case by (fastforce intro: terminates.intros)
next
case Spec thus ?case by (fastforce intro: terminates.intros)
next
case (Seq c1 c2)
have "Γ⊢mark_guards f (Seq c1 c2) ↓ Normal s" by fact
then obtain
termi_merge_c1: "Γ⊢mark_guards f c1 ↓ Normal s" and
termi_merge_c2: "∀s'. Γ⊢⟨mark_guards f c1,Normal s ⟩ ⇒ s' ⟶
Γ⊢mark_guards f c2 ↓ s'"
by (auto elim: terminates_Normal_elim_cases)
from termi_merge_c1 Seq.hyps
have "Γ⊢c1 ↓ Normal s" by iprover
moreover
{
fix s'
assume exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ s'"
have "Γ⊢ c2 ↓ s'"
proof (cases "isFault s'")
case True
thus ?thesis by (auto elim: isFaultE)
next
case False
from exec_to_exec_mark_guards [OF exec_c1 False]
have "Γ⊢⟨mark_guards f c1,Normal s ⟩ ⇒ s'" .
from termi_merge_c2 [rule_format, OF this] Seq.hyps
show ?thesis
by (cases s') (auto)
qed
}
ultimately show ?case by (auto intro: terminates.intros)
next
case Cond thus ?case
by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case (While b c)
{
fix u c'
assume termi_c': "Γ⊢c' ↓ Normal u"
assume c': "c' = mark_guards f (While b c)"
have "Γ⊢While b c ↓ Normal u"
using termi_c' c'
proof (induct)
case (WhileTrue s b' c')
have s_in_b: "s ∈ b" using WhileTrue by simp
have "Γ⊢mark_guards f c ↓ Normal s"
using WhileTrue by (auto elim: terminates_Normal_elim_cases)
with While.hyps have "Γ⊢c ↓ Normal s"
by auto
moreover
have hyp_w: "∀w. Γ⊢⟨mark_guards f c,Normal s ⟩ ⇒ w ⟶ Γ⊢While b c ↓ w"
using WhileTrue by simp
hence "∀w. Γ⊢⟨c,Normal s ⟩ ⇒ w ⟶ Γ⊢While b c ↓ w"
apply -
apply (rule allI)
apply (case_tac "w")
apply (auto dest: exec_to_exec_mark_guards)
done
ultimately show ?case
using s_in_b
by (auto intro: terminates.intros)
next
case WhileFalse thus ?case by (auto intro: terminates.intros)
qed auto
}
with While show ?case by simp
next
case Call thus ?case
by (fastforce intro: terminates.intros )
next
case DynCom thus ?case
by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case (Guard f g c)
thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case Throw thus ?case
by (fastforce intro: terminates.intros )
next
case (Catch c1 c2)
have "Γ⊢mark_guards f (Catch c1 c2) ↓ Normal s" by fact
then obtain
termi_merge_c1: "Γ⊢mark_guards f c1 ↓ Normal s" and
termi_merge_c2: "∀s'. Γ⊢⟨mark_guards f c1,Normal s ⟩ ⇒ Abrupt s' ⟶
Γ⊢mark_guards f c2 ↓ Normal s'"
by (auto elim: terminates_Normal_elim_cases)
from termi_merge_c1 Catch.hyps
have "Γ⊢c1 ↓ Normal s" by iprover
moreover
{
fix s'
assume exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ Abrupt s'"
have "Γ⊢ c2 ↓ Normal s'"
proof -
from exec_to_exec_mark_guards [OF exec_c1]
have "Γ⊢⟨mark_guards f c1,Normal s ⟩ ⇒ Abrupt s'" by simp
from termi_merge_c2 [rule_format, OF this] Catch.hyps
show ?thesis
by iprover
qed
}
ultimately show ?case by (auto intro: terminates.intros)
qed
lemma terminates_mark_guards_to_terminates:
"Γ⊢mark_guards f c↓s ⟹ Γ⊢c↓ s"
by (cases s) (auto intro: terminates_mark_guards_to_terminates_Normal)
subsection {* Lemmas about @{const "merge_guards"} *}
lemma terminates_to_terminates_merge_guards:
assumes termi: "Γ⊢c↓s"
shows "Γ⊢merge_guards c↓s"
using termi
proof (induct)
case (Guard s g c f)
have s_in_g: "s ∈ g" by fact
have termi_merge_c: "Γ⊢merge_guards c ↓ Normal s" by fact
show ?case
proof (cases "∃f' g' c'. merge_guards c = Guard f' g' c'")
case False
hence "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
by (cases "merge_guards c") (auto simp add: Let_def)
with s_in_g termi_merge_c show ?thesis
by (auto intro: terminates.intros)
next
case True
then obtain f' g' c' where
mc: "merge_guards c = Guard f' g' c'"
by blast
show ?thesis
proof (cases "f=f'")
case False
with mc have "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
by (simp add: Let_def)
with s_in_g termi_merge_c show ?thesis
by (auto intro: terminates.intros)
next
case True
with mc have "merge_guards (Guard f g c) = Guard f (g ∩ g') c'"
by simp
with s_in_g mc True termi_merge_c
show ?thesis
by (cases "s ∈ g'")
(auto intro: terminates.intros elim: terminates_Normal_elim_cases)
qed
qed
next
case (GuardFault s g f c)
have "s ∉ g" by fact
thus ?case
by (cases "merge_guards c")
(auto intro: terminates.intros split: if_split_asm simp add: Let_def)
qed (fastforce intro: terminates.intros dest: exec_merge_guards_to_exec)+
lemma terminates_merge_guards_to_terminates_Normal:
shows "⋀s. Γ⊢merge_guards c↓Normal s ⟹ Γ⊢c↓Normal s"
proof (induct c)
case Skip thus ?case by (fastforce intro: terminates.intros)
next
case Basic thus ?case by (fastforce intro: terminates.intros)
next
case Spec thus ?case by (fastforce intro: terminates.intros)
next
case (Seq c1 c2)
have "Γ⊢merge_guards (Seq c1 c2) ↓ Normal s" by fact
then obtain
termi_merge_c1: "Γ⊢merge_guards c1 ↓ Normal s" and
termi_merge_c2: "∀s'. Γ⊢⟨merge_guards c1,Normal s ⟩ ⇒ s' ⟶
Γ⊢merge_guards c2 ↓ s'"
by (auto elim: terminates_Normal_elim_cases)
from termi_merge_c1 Seq.hyps
have "Γ⊢c1 ↓ Normal s" by iprover
moreover
{
fix s'
assume exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ s'"
have "Γ⊢ c2 ↓ s'"
proof -
from exec_to_exec_merge_guards [OF exec_c1]
have "Γ⊢⟨merge_guards c1,Normal s ⟩ ⇒ s'" .
from termi_merge_c2 [rule_format, OF this] Seq.hyps
show ?thesis
by (cases s') (auto)
qed
}
ultimately show ?case by (auto intro: terminates.intros)
next
case Cond thus ?case
by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case (While b c)
{
fix u c'
assume termi_c': "Γ⊢c' ↓ Normal u"
assume c': "c' = merge_guards (While b c)"
have "Γ⊢While b c ↓ Normal u"
using termi_c' c'
proof (induct)
case (WhileTrue s b' c')
have s_in_b: "s ∈ b" using WhileTrue by simp
have "Γ⊢merge_guards c ↓ Normal s"
using WhileTrue by (auto elim: terminates_Normal_elim_cases)
with While.hyps have "Γ⊢c ↓ Normal s"
by auto
moreover
have hyp_w: "∀w. Γ⊢⟨merge_guards c,Normal s ⟩ ⇒ w ⟶ Γ⊢While b c ↓ w"
using WhileTrue by simp
hence "∀w. Γ⊢⟨c,Normal s ⟩ ⇒ w ⟶ Γ⊢While b c ↓ w"
by (simp add: exec_iff_exec_merge_guards [symmetric])
ultimately show ?case
using s_in_b
by (auto intro: terminates.intros)
next
case WhileFalse thus ?case by (auto intro: terminates.intros)
qed auto
}
with While show ?case by simp
next
case Call thus ?case
by (fastforce intro: terminates.intros )
next
case DynCom thus ?case
by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case (Guard f g c)
have termi_merge: "Γ⊢merge_guards (Guard f g c) ↓ Normal s" by fact
show ?case
proof (cases "∃f' g' c'. merge_guards c = Guard f' g' c'")
case False
hence m: "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
by (cases "merge_guards c") (auto simp add: Let_def)
from termi_merge Guard.hyps show ?thesis
by (simp only: m)
(fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case True
then obtain f' g' c' where
mc: "merge_guards c = Guard f' g' c'"
by blast
show ?thesis
proof (cases "f=f'")
case False
with mc have m: "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
by (simp add: Let_def)
from termi_merge Guard.hyps show ?thesis
by (simp only: m)
(fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
next
case True
with mc have m: "merge_guards (Guard f g c) = Guard f (g ∩ g') c'"
by simp
from termi_merge Guard.hyps
show ?thesis
by (simp only: m mc)
(auto intro: terminates.intros elim: terminates_Normal_elim_cases)
qed
qed
next
case Throw thus ?case
by (fastforce intro: terminates.intros )
next
case (Catch c1 c2)
have "Γ⊢merge_guards (Catch c1 c2) ↓ Normal s" by fact
then obtain
termi_merge_c1: "Γ⊢merge_guards c1 ↓ Normal s" and
termi_merge_c2: "∀s'. Γ⊢⟨merge_guards c1,Normal s ⟩ ⇒ Abrupt s' ⟶
Γ⊢merge_guards c2 ↓ Normal s'"
by (auto elim: terminates_Normal_elim_cases)
from termi_merge_c1 Catch.hyps
have "Γ⊢c1 ↓ Normal s" by iprover
moreover
{
fix s'
assume exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ Abrupt s'"
have "Γ⊢ c2 ↓ Normal s'"
proof -
from exec_to_exec_merge_guards [OF exec_c1]
have "Γ⊢⟨merge_guards c1,Normal s ⟩ ⇒ Abrupt s'" .
from termi_merge_c2 [rule_format, OF this] Catch.hyps
show ?thesis
by iprover
qed
}
ultimately show ?case by (auto intro: terminates.intros)
qed
lemma terminates_merge_guards_to_terminates:
"Γ⊢merge_guards c↓ s ⟹ Γ⊢c↓ s"
by (cases s) (auto intro: terminates_merge_guards_to_terminates_Normal)
theorem terminates_iff_terminates_merge_guards:
"Γ⊢c↓ s = Γ⊢merge_guards c↓ s"
by (iprover intro: terminates_to_terminates_merge_guards
terminates_merge_guards_to_terminates)
subsection {* Lemmas about @{term "c⇩1 ⊆⇩g c⇩2"} *}
lemma terminates_fewer_guards_Normal:
shows "⋀c s. ⟦Γ⊢c'↓Normal s; c ⊆⇩g c'; Γ⊢⟨c',Normal s ⟩ ⇒∉Fault ` UNIV⟧
⟹ Γ⊢c↓Normal s"
proof (induct c')
case Skip thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
case Basic thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
case Spec thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
case (Seq c1' c2')
have termi: "Γ⊢Seq c1' c2' ↓ Normal s" by fact
then obtain
termi_c1': "Γ⊢c1'↓ Normal s" and
termi_c2': "∀s'. Γ⊢⟨c1',Normal s ⟩ ⇒ s' ⟶ Γ⊢c2'↓ s'"
by (auto elim: terminates_Normal_elim_cases)
have noFault: "Γ⊢⟨Seq c1' c2',Normal s ⟩ ⇒∉Fault ` UNIV" by fact
hence noFault_c1': "Γ⊢⟨c1',Normal s ⟩ ⇒∉Fault ` UNIV"
by (auto intro: exec.intros simp add: final_notin_def)
have "c ⊆⇩g Seq c1' c2'" by fact
from subseteq_guards_Seq [OF this] obtain c1 c2 where
c: "c = Seq c1 c2" and
c1_c1': "c1 ⊆⇩g c1'" and
c2_c2': "c2 ⊆⇩g c2'"
by blast
from termi_c1' c1_c1' noFault_c1'
have "Γ⊢c1↓ Normal s"
by (rule Seq.hyps)
moreover
{
fix t
assume exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ t"
have "Γ⊢c2↓ t"
proof -
from exec_to_exec_subseteq_guards [OF c1_c1' exec_c1] obtain t' where
exec_c1': "Γ⊢⟨c1',Normal s ⟩ ⇒ t'" and
t_Fault: "isFault t ⟶ isFault t'" and
t'_noFault: "¬ isFault t' ⟶ t' = t"
by blast
show ?thesis
proof (cases "isFault t'")
case True
with exec_c1' noFault_c1'
have False
by (fastforce elim: isFaultE dest: Fault_end simp add: final_notin_def)
thus ?thesis ..
next
case False
with t'_noFault have t': "t'=t" by simp
with termi_c2' exec_c1'
have termi_c2': "Γ⊢c2'↓ t"
by auto
show ?thesis
proof (cases t)
case Fault thus ?thesis by auto
next
case Abrupt thus ?thesis by auto
next
case Stuck thus ?thesis by auto
next
case (Normal u)
with noFault exec_c1' t'
have "Γ⊢⟨c2',Normal u ⟩ ⇒∉Fault ` UNIV"
by (auto intro: exec.intros simp add: final_notin_def)
from termi_c2' [simplified Normal] c2_c2' this
have "Γ⊢c2 ↓ Normal u"
by (rule Seq.hyps)
with Normal exec_c1
show ?thesis by simp
qed
qed
qed
}
ultimately show ?case using c by (auto intro: terminates.intros)
next
case (Cond b c1' c2')
have noFault: "Γ⊢⟨Cond b c1' c2',Normal s ⟩ ⇒∉Fault ` UNIV" by fact
have termi: "Γ⊢Cond b c1' c2' ↓ Normal s" by fact
have "c ⊆⇩g Cond b c1' c2'" by fact
from subseteq_guards_Cond [OF this] obtain c1 c2 where
c: "c = Cond b c1 c2" and
c1_c1': "c1 ⊆⇩g c1'" and
c2_c2': "c2 ⊆⇩g c2'"
by blast
thus ?case
proof (cases "s ∈ b")
case True
with termi have termi_c1': "Γ⊢c1' ↓ Normal s"
by (auto elim: terminates_Normal_elim_cases)
from True noFault have "Γ⊢⟨c1',Normal s ⟩ ⇒∉Fault ` UNIV"
by (auto intro: exec.intros simp add: final_notin_def)
from termi_c1' c1_c1' this
have "Γ⊢c1 ↓ Normal s"
by (rule Cond.hyps)
with True c show ?thesis
by (auto intro: terminates.intros)
next
case False
with termi have termi_c2': "Γ⊢c2' ↓ Normal s"
by (auto elim: terminates_Normal_elim_cases)
from False noFault have "Γ⊢⟨c2',Normal s ⟩ ⇒∉Fault ` UNIV"
by (auto intro: exec.intros simp add: final_notin_def)
from termi_c2' c2_c2' this
have "Γ⊢c2 ↓ Normal s"
by (rule Cond.hyps)
with False c show ?thesis
by (auto intro: terminates.intros)
qed
next
case (While b c')
have noFault: "Γ⊢⟨While b c',Normal s ⟩ ⇒∉Fault ` UNIV" by fact
have termi: "Γ⊢While b c' ↓ Normal s" by fact
have "c ⊆⇩g While b c'" by fact
from subseteq_guards_While [OF this]
obtain c'' where
c: "c = While b c''" and
c''_c': "c'' ⊆⇩g c'"
by blast
{
fix d u
assume termi: "Γ⊢d ↓ u"
assume d: "d = While b c'"
assume noFault: "Γ⊢⟨While b c',u ⟩ ⇒∉Fault ` UNIV"
have "Γ⊢While b c'' ↓ u"
using termi d noFault
proof (induct)
case (WhileTrue u b' c''')
have u_in_b: "u ∈ b" using WhileTrue by simp
have termi_c': "Γ⊢c' ↓ Normal u" using WhileTrue by simp
have noFault: "Γ⊢⟨While b c',Normal u ⟩ ⇒∉Fault ` UNIV" using WhileTrue by simp
hence noFault_c': "Γ⊢⟨c',Normal u ⟩ ⇒∉Fault ` UNIV" using u_in_b
by (auto intro: exec.intros simp add: final_notin_def)
from While.hyps [OF termi_c' c''_c' this]
have "Γ⊢c'' ↓ Normal u".
moreover
from WhileTrue
have hyp_w: "∀s'. Γ⊢⟨c',Normal u ⟩ ⇒ s' ⟶ Γ⊢⟨While b c',s' ⟩ ⇒∉Fault ` UNIV
⟶ Γ⊢While b c'' ↓ s'"
by simp
{
fix v
assume exec_c'': "Γ⊢⟨c'',Normal u ⟩ ⇒ v"
have "Γ⊢While b c'' ↓ v"
proof -
from exec_to_exec_subseteq_guards [OF c''_c' exec_c''] obtain v' where
exec_c': "Γ⊢⟨c',Normal u ⟩ ⇒ v'" and
v_Fault: "isFault v ⟶ isFault v'" and
v'_noFault: "¬ isFault v' ⟶ v' = v"
by auto
show ?thesis
proof (cases "isFault v'")
case True
with exec_c' noFault u_in_b
have False
by (fastforce
simp add: final_notin_def intro: exec.intros elim: isFaultE)
thus ?thesis ..
next
case False
with v'_noFault have v': "v'=v"
by simp
with noFault exec_c' u_in_b
have "Γ⊢⟨While b c',v ⟩ ⇒∉Fault ` UNIV"
by (fastforce simp add: final_notin_def intro: exec.intros)
from hyp_w [rule_format, OF exec_c' [simplified v'] this]
show "Γ⊢While b c'' ↓ v" .
qed
qed
}
ultimately
show ?case using u_in_b
by (auto intro: terminates.intros)
next
case WhileFalse thus ?case by (auto intro: terminates.intros)
qed auto
}
with c noFault termi show ?case
by auto
next
case Call thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
case (DynCom C')
have termi: "Γ⊢DynCom C' ↓ Normal s" by fact
hence termi_C': "Γ⊢C' s ↓ Normal s"
by cases
have noFault: "Γ⊢⟨DynCom C',Normal s ⟩ ⇒∉Fault ` UNIV" by fact
hence noFault_C': "Γ⊢⟨C' s,Normal s ⟩ ⇒∉Fault ` UNIV"
by (auto intro: exec.intros simp add: final_notin_def)
have "c ⊆⇩g DynCom C'" by fact
from subseteq_guards_DynCom [OF this] obtain C where
c: "c = DynCom C" and
C_C': "∀s. C s ⊆⇩g C' s"
by blast
from DynCom.hyps termi_C' C_C' [rule_format] noFault_C'
have "Γ⊢C s ↓ Normal s"
by fast
with c show ?case
by (auto intro: terminates.intros)
next
case (Guard f' g' c')
have noFault: "Γ⊢⟨Guard f' g' c',Normal s ⟩ ⇒∉Fault ` UNIV" by fact
have termi: "Γ⊢Guard f' g' c' ↓ Normal s" by fact
have "c ⊆⇩g Guard f' g' c'" by fact
hence c_cases: "(c ⊆⇩g c') ∨ (∃c''. c = Guard f' g' c'' ∧ (c'' ⊆⇩g c'))"
by (rule subseteq_guards_Guard)
thus ?case
proof (cases "s ∈ g'")
case True
note s_in_g' = this
with noFault have noFault_c': "Γ⊢⟨c',Normal s ⟩ ⇒∉Fault ` UNIV"
by (auto simp add: final_notin_def intro: exec.intros)
from termi s_in_g' have termi_c': "Γ⊢c' ↓ Normal s"
by cases auto
from c_cases show ?thesis
proof
assume "c ⊆⇩g c'"
from termi_c' this noFault_c'
show "Γ⊢c ↓ Normal s"
by (rule Guard.hyps)
next
assume "∃c''. c = Guard f' g' c'' ∧ (c'' ⊆⇩g c')"
then obtain c'' where
c: "c = Guard f' g' c''" and c''_c': "c'' ⊆⇩g c'"
by blast
from termi_c' c''_c' noFault_c'
have "Γ⊢c'' ↓ Normal s"
by (rule Guard.hyps)
with s_in_g' c
show ?thesis
by (auto intro: terminates.intros)
qed
next
case False
with noFault have False
by (auto intro: exec.intros simp add: final_notin_def)
thus ?thesis ..
qed
next
case Throw thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
next
case (Catch c1' c2')
have termi: "Γ⊢Catch c1' c2' ↓ Normal s" by fact
then obtain
termi_c1': "Γ⊢c1'↓ Normal s" and
termi_c2': "∀s'. Γ⊢⟨c1',Normal s ⟩ ⇒ Abrupt s' ⟶ Γ⊢c2'↓ Normal s'"
by (auto elim: terminates_Normal_elim_cases)
have noFault: "Γ⊢⟨Catch c1' c2',Normal s ⟩ ⇒∉Fault ` UNIV" by fact
hence noFault_c1': "Γ⊢⟨c1',Normal s ⟩ ⇒∉Fault ` UNIV"
by (fastforce intro: exec.intros simp add: final_notin_def)
have "c ⊆⇩g Catch c1' c2'" by fact
from subseteq_guards_Catch [OF this] obtain c1 c2 where
c: "c = Catch c1 c2" and
c1_c1': "c1 ⊆⇩g c1'" and
c2_c2': "c2 ⊆⇩g c2'"
by blast
from termi_c1' c1_c1' noFault_c1'
have "Γ⊢c1↓ Normal s"
by (rule Catch.hyps)
moreover
{
fix t
assume exec_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒ Abrupt t"
have "Γ⊢c2↓ Normal t"
proof -
from exec_to_exec_subseteq_guards [OF c1_c1' exec_c1] obtain t' where
exec_c1': "Γ⊢⟨c1',Normal s ⟩ ⇒ t'" and
t'_noFault: "¬ isFault t' ⟶ t' = Abrupt t"
by blast
show ?thesis
proof (cases "isFault t'")
case True
with exec_c1' noFault_c1'
have False
by (fastforce elim: isFaultE dest: Fault_end simp add: final_notin_def)
thus ?thesis ..
next
case False
with t'_noFault have t': "t'=Abrupt t" by simp
with termi_c2' exec_c1'
have termi_c2': "Γ⊢c2'↓ Normal t"
by auto
with noFault exec_c1' t'
have "Γ⊢⟨c2',Normal t ⟩ ⇒∉Fault ` UNIV"
by (auto intro: exec.intros simp add: final_notin_def)
from termi_c2' c2_c2' this
show "Γ⊢c2 ↓ Normal t"
by (rule Catch.hyps)
qed
qed
}
ultimately show ?case using c by (auto intro: terminates.intros)
qed
theorem terminates_fewer_guards:
shows "⟦Γ⊢c'↓s; c ⊆⇩g c'; Γ⊢⟨c',s ⟩ ⇒∉Fault ` UNIV⟧
⟹ Γ⊢c↓s"
by (cases s) (auto intro: terminates_fewer_guards_Normal)
lemma terminates_noFault_strip_guards:
assumes termi: "Γ⊢c↓Normal s"
shows "⟦Γ⊢⟨c,Normal s ⟩ ⇒∉Fault ` F⟧ ⟹ Γ⊢strip_guards F c↓Normal s"
using termi
proof (induct)
case Skip thus ?case by (auto intro: terminates.intros)
next
case Basic thus ?case by (auto intro: terminates.intros)
next
case Spec thus ?case by (auto intro: terminates.intros)
next
case (Guard s g c f)
have s_in_g: "s ∈ g" by fact
have "Γ⊢c ↓ Normal s" by fact
have "Γ⊢⟨Guard f g c,Normal s ⟩ ⇒∉Fault ` F" by fact
with s_in_g have "Γ⊢⟨c,Normal s ⟩ ⇒∉Fault ` F"
by (fastforce simp add: final_notin_def intro: exec.intros)
with Guard.hyps have "Γ⊢strip_guards F c ↓ Normal s" by simp
with s_in_g show ?case
by (auto intro: terminates.intros)
next
case GuardFault thus ?case
by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
next
case Fault thus ?case by (auto intro: terminates.intros)
next
case (Seq c1 s c2)
have noFault_Seq: "Γ⊢⟨Seq c1 c2,Normal s ⟩ ⇒∉Fault ` F" by fact
hence noFault_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
with Seq.hyps have "Γ⊢strip_guards F c1 ↓ Normal s" by simp
moreover
{
fix s'
assume exec_strip_guards_c1: "Γ⊢⟨strip_guards F c1,Normal s ⟩ ⇒ s'"
have "Γ⊢strip_guards F c2 ↓ s'"
proof (cases "isFault s'")
case True
thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
next
case False
with exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1
have "Γ⊢⟨c1,Normal s ⟩ ⇒ s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this noFault_Seq have "Γ⊢⟨c2,s' ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
ultimately show ?thesis
using Seq.hyps by simp
qed
}
ultimately show ?case
by (auto intro: terminates.intros)
next
case CondTrue thus ?case
by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
next
case CondFalse thus ?case
by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
next
case (WhileTrue s b c)
have s_in_b: "s ∈ b" by fact
have noFault_while: "Γ⊢⟨While b c,Normal s ⟩ ⇒∉Fault ` F" by fact
with s_in_b have noFault_c: "Γ⊢⟨c,Normal s ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
with WhileTrue.hyps have "Γ⊢strip_guards F c ↓ Normal s" by simp
moreover
{
fix s'
assume exec_strip_guards_c: "Γ⊢⟨strip_guards F c,Normal s ⟩ ⇒ s'"
have "Γ⊢strip_guards F (While b c) ↓ s'"
proof (cases "isFault s'")
case True
thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
next
case False
with exec_strip_guards_to_exec [OF exec_strip_guards_c] noFault_c
have "Γ⊢⟨c,Normal s ⟩ ⇒ s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this s_in_b noFault_while have "Γ⊢⟨While b c,s' ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
ultimately show ?thesis
using WhileTrue.hyps by simp
qed
}
ultimately show ?case
using WhileTrue.hyps by (auto intro: terminates.intros)
next
case WhileFalse thus ?case by (auto intro: terminates.intros)
next
case Call thus ?case by (auto intro: terminates.intros)
next
case CallUndefined thus ?case by (auto intro: terminates.intros)
next
case Stuck thus ?case by (auto intro: terminates.intros)
next
case DynCom thus ?case
by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
next
case Throw thus ?case by (auto intro: terminates.intros)
next
case Abrupt thus ?case by (auto intro: terminates.intros)
next
case (Catch c1 s c2)
have noFault_Catch: "Γ⊢⟨Catch c1 c2,Normal s ⟩ ⇒∉Fault ` F" by fact
hence noFault_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒∉Fault ` F"
by (fastforce simp add: final_notin_def intro: exec.intros)
with Catch.hyps have "Γ⊢strip_guards F c1 ↓ Normal s" by simp
moreover
{
fix s'
assume exec_strip_guards_c1: "Γ⊢⟨strip_guards F c1,Normal s ⟩ ⇒ Abrupt s'"
have "Γ⊢strip_guards F c2 ↓ Normal s'"
proof -
from exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1
have "Γ⊢⟨c1,Normal s ⟩ ⇒ Abrupt s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this noFault_Catch have "Γ⊢⟨c2,Normal s' ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
ultimately show ?thesis
using Catch.hyps by simp
qed
}
ultimately show ?case
using Catch.hyps by (auto intro: terminates.intros)
qed
subsection {* Lemmas about @{const "strip_guards"} *}
lemma terminates_noFault_strip:
assumes termi: "Γ⊢c↓Normal s"
shows "⟦Γ⊢⟨c,Normal s ⟩ ⇒∉Fault ` F⟧ ⟹ strip F Γ⊢c↓Normal s"
using termi
proof (induct)
case Skip thus ?case by (auto intro: terminates.intros)
next
case Basic thus ?case by (auto intro: terminates.intros)
next
case Spec thus ?case by (auto intro: terminates.intros)
next
case (Guard s g c f)
have s_in_g: "s ∈ g" by fact
have "Γ⊢⟨Guard f g c,Normal s ⟩ ⇒∉Fault ` F" by fact
with s_in_g have "Γ⊢⟨c,Normal s ⟩ ⇒∉Fault ` F"
by (fastforce simp add: final_notin_def intro: exec.intros)
then have "strip F Γ⊢c ↓ Normal s" by (simp add: Guard.hyps)
with s_in_g show ?case
by (auto intro: terminates.intros simp del: strip_simp)
next
case GuardFault thus ?case
by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
next
case Fault thus ?case by (auto intro: terminates.intros)
next
case (Seq c1 s c2)
have noFault_Seq: "Γ⊢⟨Seq c1 c2,Normal s ⟩ ⇒∉Fault ` F" by fact
hence noFault_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
then have "strip F Γ⊢c1 ↓ Normal s" by (simp add: Seq.hyps)
moreover
{
fix s'
assume exec_strip_c1: "strip F Γ⊢⟨c1,Normal s ⟩ ⇒ s'"
have "strip F Γ⊢c2 ↓ s'"
proof (cases "isFault s'")
case True
thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
next
case False
with exec_strip_to_exec [OF exec_strip_c1] noFault_c1
have "Γ⊢⟨c1,Normal s ⟩ ⇒ s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this noFault_Seq have "Γ⊢⟨c2,s' ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
ultimately show ?thesis
using Seq.hyps by (simp del: strip_simp)
qed
}
ultimately show ?case
by (fastforce intro: terminates.intros)
next
case CondTrue thus ?case
by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
next
case CondFalse thus ?case
by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
next
case (WhileTrue s b c)
have s_in_b: "s ∈ b" by fact
have noFault_while: "Γ⊢⟨While b c,Normal s ⟩ ⇒∉Fault ` F" by fact
with s_in_b have noFault_c: "Γ⊢⟨c,Normal s ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
then have "strip F Γ⊢c ↓ Normal s" by (simp add: WhileTrue.hyps)
moreover
{
fix s'
assume exec_strip_c: "strip F Γ⊢⟨c,Normal s ⟩ ⇒ s'"
have "strip F Γ⊢While b c ↓ s'"
proof (cases "isFault s'")
case True
thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
next
case False
with exec_strip_to_exec [OF exec_strip_c] noFault_c
have "Γ⊢⟨c,Normal s ⟩ ⇒ s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this s_in_b noFault_while have "Γ⊢⟨While b c,s' ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
ultimately show ?thesis
using WhileTrue.hyps by (simp del: strip_simp)
qed
}
ultimately show ?case
using WhileTrue.hyps by (auto intro: terminates.intros simp del: strip_simp)
next
case WhileFalse thus ?case by (auto intro: terminates.intros)
next
case (Call p bdy s)
have bdy: "Γ p = Some bdy" by fact
have "Γ⊢⟨Call p,Normal s ⟩ ⇒∉Fault ` F" by fact
with bdy have bdy_noFault: "Γ⊢⟨bdy,Normal s ⟩ ⇒∉Fault ` F"
by (auto intro: exec.intros simp add: final_notin_def)
then have strip_bdy_noFault: "strip F Γ⊢⟨bdy,Normal s ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def dest!: exec_strip_to_exec elim!: isFaultE)
from bdy_noFault have "strip F Γ⊢bdy ↓ Normal s" by (simp add: Call.hyps)
from terminates_noFault_strip_guards [OF this strip_bdy_noFault]
have "strip F Γ⊢strip_guards F bdy ↓ Normal s".
with bdy show ?case
by (fastforce intro: terminates.Call)
next
case CallUndefined thus ?case by (auto intro: terminates.intros)
next
case Stuck thus ?case by (auto intro: terminates.intros)
next
case DynCom thus ?case
by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
next
case Throw thus ?case by (auto intro: terminates.intros)
next
case Abrupt thus ?case by (auto intro: terminates.intros)
next
case (Catch c1 s c2)
have noFault_Catch: "Γ⊢⟨Catch c1 c2,Normal s ⟩ ⇒∉Fault ` F" by fact
hence noFault_c1: "Γ⊢⟨c1,Normal s ⟩ ⇒∉Fault ` F"
by (fastforce simp add: final_notin_def intro: exec.intros)
then have "strip F Γ⊢c1 ↓ Normal s" by (simp add: Catch.hyps)
moreover
{
fix s'
assume exec_strip_c1: "strip F Γ⊢⟨c1,Normal s ⟩ ⇒ Abrupt s'"
have "strip F Γ⊢c2 ↓ Normal s'"
proof -
from exec_strip_to_exec [OF exec_strip_c1] noFault_c1
have "Γ⊢⟨c1,Normal s ⟩ ⇒ Abrupt s'"
by (auto simp add: final_notin_def elim!: isFaultE)
moreover
from this noFault_Catch have "Γ⊢⟨c2,Normal s' ⟩ ⇒∉Fault ` F"
by (auto simp add: final_notin_def intro: exec.intros)
ultimately show ?thesis
using Catch.hyps by (simp del: strip_simp)
qed
}
ultimately show ?case
using Catch.hyps by (auto intro: terminates.intros simp del: strip_simp)
qed
subsection {* Miscellaneous *}
lemma terminates_while_lemma:
assumes termi: "Γ⊢w↓fk"
shows "⋀k b c. ⟦fk = Normal (f k); w=While b c;
∀i. Γ⊢⟨c,Normal (f i) ⟩ ⇒ Normal (f (Suc i))⟧
⟹ ∃i. f i ∉ b"
using termi
proof (induct)
case WhileTrue thus ?case by blast
next
case WhileFalse thus ?case by blast
qed simp_all
lemma terminates_while:
"⟦Γ⊢(While b c)↓Normal (f k);
∀i. Γ⊢⟨c,Normal (f i) ⟩ ⇒ Normal (f (Suc i))⟧
⟹ ∃i. f i ∉ b"
by (blast intro: terminates_while_lemma)
lemma wf_terminates_while:
"wf {(t,s). Γ⊢(While b c)↓Normal s ∧ s∈b ∧
Γ⊢⟨c,Normal s ⟩ ⇒ Normal t}"
apply(subst wf_iff_no_infinite_down_chain)
apply(rule notI)
apply clarsimp
apply(insert terminates_while)
apply blast
done
lemma terminates_restrict_to_terminates:
assumes terminates_res: "Γ|⇘M⇙⊢ c ↓ s"
assumes not_Stuck: "Γ|⇘M⇙⊢⟨c,s ⟩ ⇒∉{Stuck}"
shows "Γ⊢ c ↓ s"
using terminates_res not_Stuck
proof (induct)
case Skip show ?case by (rule terminates.Skip)
next
case Basic show ?case by (rule terminates.Basic)
next
case Spec show ?case by (rule terminates.Spec)
next
case Guard thus ?case
by (auto intro: terminates.Guard dest: notStuck_GuardD)
next
case GuardFault thus ?case by (auto intro: terminates.GuardFault)
next
case Fault show ?case by (rule terminates.Fault)
next
case (Seq c1 s c2)
have not_Stuck: "Γ|⇘M⇙⊢⟨Seq c1 c2,Normal s ⟩ ⇒∉{Stuck}" by fact
hence c1_notStuck: "Γ|⇘M⇙⊢⟨c1,Normal s ⟩ ⇒∉{Stuck}"
by (rule notStuck_SeqD1)
show "Γ⊢Seq c1 c2 ↓ Normal s"
proof (rule terminates.Seq,safe)
from c1_notStuck
show "Γ⊢c1 ↓ Normal s"
by (rule Seq.hyps)
next
fix s'
assume exec: "Γ⊢⟨c1,Normal s ⟩ ⇒ s'"
show "Γ⊢c2 ↓ s'"
proof -
from exec_to_exec_restrict [OF exec] obtain t' where
exec_res: "Γ|⇘M⇙⊢⟨c1,Normal s ⟩ ⇒ t'" and
t'_notStuck: "t' ≠ Stuck ⟶ t' = s'"
by blast
show ?thesis
proof (cases "t'=Stuck")
case True
with c1_notStuck exec_res have "False"
by (auto simp add: final_notin_def)
thus ?thesis ..
next
case False
with t'_notStuck have t': "t'=s'" by simp
with not_Stuck exec_res
have "Γ|⇘M⇙⊢⟨c2,s' ⟩ ⇒∉{Stuck}"
by (auto dest: notStuck_SeqD2)
with exec_res t' Seq.hyps
show ?thesis
by auto
qed
qed
qed
next
case CondTrue thus ?case
by (auto intro: terminates.CondTrue dest: notStuck_CondTrueD)
next
case CondFalse thus ?case
by (auto intro: terminates.CondFalse dest: notStuck_CondFalseD)
next
case (WhileTrue s b c)
have s: "s ∈ b" by fact
have not_Stuck: "Γ|⇘M⇙⊢⟨While b c,Normal s ⟩ ⇒∉{Stuck}" by fact
with WhileTrue have c_notStuck: "Γ|⇘M⇙⊢⟨c,Normal s ⟩ ⇒∉{Stuck}"
by (iprover intro: notStuck_WhileTrueD1)
show ?case
proof (rule terminates.WhileTrue [OF s],safe)
from c_notStuck
show "Γ⊢c ↓ Normal s"
by (rule WhileTrue.hyps)
next
fix s'
assume exec: "Γ⊢⟨c,Normal s ⟩ ⇒ s'"
show "Γ⊢While b c ↓ s'"
proof -
from exec_to_exec_restrict [OF exec] obtain t' where
exec_res: "Γ|⇘M⇙⊢⟨c,Normal s ⟩ ⇒ t'" and
t'_notStuck: "t' ≠ Stuck ⟶ t' = s'"
by blast
show ?thesis
proof (cases "t'=Stuck")
case True
with c_notStuck exec_res have "False"
by (auto simp add: final_notin_def)
thus ?thesis ..
next
case False
with t'_notStuck have t': "t'=s'" by simp
with not_Stuck exec_res s
have "Γ|⇘M⇙⊢⟨While b c,s' ⟩ ⇒∉{Stuck}"
by (auto dest: notStuck_WhileTrueD2)
with exec_res t' WhileTrue.hyps
show ?thesis
by auto
qed
qed
qed
next
case WhileFalse then show ?case by (iprover intro: terminates.WhileFalse)
next
case Call thus ?case
by (auto intro: terminates.Call dest: notStuck_CallD restrict_SomeD)
next
case CallUndefined
thus ?case
by (auto dest: notStuck_CallDefinedD)
next
case Stuck show ?case by (rule terminates.Stuck)
next
case DynCom
thus ?case
by (auto intro: terminates.DynCom dest: notStuck_DynComD)
next
case Throw show ?case by (rule terminates.Throw)
next
case Abrupt show ?case by (rule terminates.Abrupt)
next
case (Catch c1 s c2)
have not_Stuck: "Γ|⇘M⇙⊢⟨Catch c1 c2,Normal s ⟩ ⇒∉{Stuck}" by fact
hence c1_notStuck: "Γ|⇘M⇙⊢⟨c1,Normal s ⟩ ⇒∉{Stuck}"
by (rule notStuck_CatchD1)
show "Γ⊢Catch c1 c2 ↓ Normal s"
proof (rule terminates.Catch,safe)
from c1_notStuck
show "Γ⊢c1 ↓ Normal s"
by (rule Catch.hyps)
next
fix s'
assume exec: "Γ⊢⟨c1,Normal s ⟩ ⇒ Abrupt s'"
show "Γ⊢c2 ↓ Normal s'"
proof -
from exec_to_exec_restrict [OF exec] obtain t' where
exec_res: "Γ|⇘M⇙⊢⟨c1,Normal s ⟩ ⇒ t'" and
t'_notStuck: "t' ≠ Stuck ⟶ t' = Abrupt s'"
by blast
show ?thesis
proof (cases "t'=Stuck")
case True
with c1_notStuck exec_res have "False"
by (auto simp add: final_notin_def)
thus ?thesis ..
next
case False
with t'_notStuck have t': "t'=Abrupt s'" by simp
with not_Stuck exec_res
have "Γ|⇘M⇙⊢⟨c2,Normal s' ⟩ ⇒∉{Stuck}"
by (auto dest: notStuck_CatchD2)
with exec_res t' Catch.hyps
show ?thesis
by auto
qed
qed
qed
qed
end