section "Small-Step Semantics of Commands"
theory Small_Step imports Star Big_Step begin
subsection "The transition relation"
inductive
small_step :: "com * state \ com * state \ bool" (infix "\" 55)
where
Assign: "(x ::= a, s) \ (SKIP, s(x := aval a s))" |
Seq1: "(SKIP;;c\<^sub>2,s) \ (c\<^sub>2,s)" |
Seq2: "(c\<^sub>1,s) \ (c\<^sub>1',s') \ (c\<^sub>1;;c\<^sub>2,s) \ (c\<^sub>1';;c\<^sub>2,s')" |
IfTrue: "bval b s \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \ (c\<^sub>1,s)" |
IfFalse: "\bval b s \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \ (c\<^sub>2,s)" |
While: "(WHILE b DO c,s) \
(IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
abbreviation
small_steps :: "com * state \ com * state \ bool" (infix "\*" 55)
where "x \* y == star small_step x y"
subsection\<open>Executability\<close>
code_pred small_step .
values "{(c',map t [''x'',''y'',''z'']) |c' t.
(''x'' ::= V ''z'';; ''y'' ::= V ''x'',
<''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}"
subsection\<open>Proof infrastructure\<close>
subsubsection\<open>Induction rules\<close>
text\<open>The default induction rule @{thm[source] small_step.induct} only works
for lemmas of the form \<open>a \<rightarrow> b \<Longrightarrow> \<dots>\<close> where \<open>a\<close> and \<open>b\<close> are
not already pairs \<open>(DUMMY,DUMMY)\<close>. We can generate a suitable variant
of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments
\<open>\<rightarrow>\<close> into pairs:\<close>
lemmas small_step_induct = small_step.induct[split_format(complete)]
subsubsection\<open>Proof automation\<close>
declare small_step.intros[simp,intro]
text\<open>Rule inversion:\<close>
inductive_cases SkipE[elim!]: "(SKIP,s) \ ct"
thm SkipE
inductive_cases AssignE[elim!]: "(x::=a,s) \ ct"
thm AssignE
inductive_cases SeqE[elim]: "(c1;;c2,s) \ ct"
thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ ct"
inductive_cases WhileE[elim]: "(WHILE b DO c, s) \ ct"
text\<open>A simple property:\<close>
lemma deterministic:
"cs \ cs' \ cs \ cs'' \ cs'' = cs'"
apply(induction arbitrary: cs'' rule: small_step.induct)
apply blast+
done
subsection "Equivalence with big-step semantics"
lemma star_seq2: "(c1,s) \* (c1',s') \ (c1;;c2,s) \* (c1';;c2,s')"
proof(induction rule: star_induct)
case refl thus ?case by simp
next
case step
thus ?case by (metis Seq2 star.step)
qed
lemma seq_comp:
"\ (c1,s1) \* (SKIP,s2); (c2,s2) \* (SKIP,s3) \
\<Longrightarrow> (c1;;c2, s1) \<rightarrow>* (SKIP,s3)"
by(blast intro: star.step star_seq2 star_trans)
text\<open>The following proof corresponds to one on the board where one would
show chains of \<open>\<rightarrow>\<close> and \<open>\<rightarrow>*\<close> steps.\<close>
lemma big_to_small:
"cs \ t \ cs \* (SKIP,t)"
proof (induction rule: big_step.induct)
fix s show "(SKIP,s) \* (SKIP,s)" by simp
next
fix x a s show "(x ::= a,s) \* (SKIP, s(x := aval a s))" by auto
next
fix c1 c2 s1 s2 s3
assume "(c1,s1) \* (SKIP,s2)" and "(c2,s2) \* (SKIP,s3)"
thus "(c1;;c2, s1) \* (SKIP,s3)" by (rule seq_comp)
next
fix s::state and b c0 c1 t
assume "bval b s"
hence "(IF b THEN c0 ELSE c1,s) \ (c0,s)" by simp
moreover assume "(c0,s) \* (SKIP,t)"
ultimately
show "(IF b THEN c0 ELSE c1,s) \* (SKIP,t)" by (metis star.simps)
next
fix s::state and b c0 c1 t
assume "\bval b s"
hence "(IF b THEN c0 ELSE c1,s) \ (c1,s)" by simp
moreover assume "(c1,s) \* (SKIP,t)"
ultimately
show "(IF b THEN c0 ELSE c1,s) \* (SKIP,t)" by (metis star.simps)
next
fix b c and s::state
assume b: "\bval b s"
let ?if = "IF b THEN c;; WHILE b DO c ELSE SKIP"
have "(WHILE b DO c,s) \ (?if, s)" by blast
moreover have "(?if,s) \ (SKIP, s)" by (simp add: b)
ultimately show "(WHILE b DO c,s) \* (SKIP,s)" by(metis star.refl star.step)
next
fix b c s s' t
let ?w = "WHILE b DO c"
let ?if = "IF b THEN c;; ?w ELSE SKIP"
assume w: "(?w,s') \* (SKIP,t)"
assume c: "(c,s) \* (SKIP,s')"
assume b: "bval b s"
have "(?w,s) \ (?if, s)" by blast
moreover have "(?if, s) \ (c;; ?w, s)" by (simp add: b)
moreover have "(c;; ?w,s) \* (SKIP,t)" by(rule seq_comp[OF c w])
ultimately show "(WHILE b DO c,s) \* (SKIP,t)" by (metis star.simps)
qed
text\<open>Each case of the induction can be proved automatically:\<close>
lemma "cs \ t \ cs \* (SKIP,t)"
proof (induction rule: big_step.induct)
case Skip show ?case by blast
next
case Assign show ?case by blast
next
case Seq thus ?case by (blast intro: seq_comp)
next
case IfTrue thus ?case by (blast intro: star.step)
next
case IfFalse thus ?case by (blast intro: star.step)
next
case WhileFalse thus ?case
by (metis star.step star_step1 small_step.IfFalse small_step.While)
next
case WhileTrue
thus ?case
by(metis While seq_comp small_step.IfTrue star.step[of small_step])
qed
lemma small1_big_continue:
"cs \ cs' \ cs' \ t \ cs \ t"
apply (induction arbitrary: t rule: small_step.induct)
apply auto
done
lemma small_to_big:
"cs \* (SKIP,t) \ cs \ t"
apply (induction cs "(SKIP,t)" rule: star.induct)
apply (auto intro: small1_big_continue)
done
text \<open>
Finally, the equivalence theorem:
\<close>
theorem big_iff_small:
"cs \ t = cs \* (SKIP,t)"
by(metis big_to_small small_to_big)
subsection "Final configurations and infinite reductions"
definition "final cs \ \(\cs'. cs \ cs')"
lemma finalD: "final (c,s) \ c = SKIP"
apply(simp add: final_def)
apply(induction c)
apply blast+
done
lemma final_iff_SKIP: "final (c,s) = (c = SKIP)"
by (metis SkipE finalD final_def)
text\<open>Now we can show that \<open>\<Rightarrow>\<close> yields a final state iff \<open>\<rightarrow>\<close>
terminates:\<close>
lemma big_iff_small_termination:
"(\t. cs \ t) \ (\cs'. cs \* cs' \ final cs')"
by(simp add: big_iff_small final_iff_SKIP)
text\<open>This is the same as saying that the absence of a big step result is
equivalent with absence of a terminating small step sequence, i.e.\ with
nontermination. Since \<open>\<rightarrow>\<close> is determininistic, there is no difference
between may and must terminate.\<close>
end
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
