theory ex05
imports Main AExp BExp ASM Star Com Big_Step Small_Step
begin
text {*
Prove or disprove (by giving counterexamples) the following program equivalences.
\begin{enumerate}
\item
\mbox{@{term "IF And b1 b2 THEN c1 ELSE c2 \ IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2"}}
\item
@{term "WHILE And b1 b2 DO c \ WHILE b1 DO WHILE b2 DO c"}
\item
@{term "WHILE And b1 b2 DO c \ WHILE b1 DO c; WHILE And b1 b2 DO c"}
\item
@{term "WHILE Or b1 b2 DO c \ WHILE Or b1 b2 DO c; WHILE b1 DO c"}
\end{enumerate}
*}
(*
a) equivalent, see below
b) not equivalent: {a=2, b=1} while (a < 3 & b < 2) do a := 4
c) not equivalent: {a=1} while (a < 2 & a < 1) do a := 4
d) equivalent, see below
*)
text {* Hint: Use the following definition for @{text Or}: *}
definition Or :: "bexp \ bexp \ bexp" where
"Or b1 b2 = Not (And (Not b1) (Not b2))"
lemma
"IF And b1 b2 THEN c1 ELSE c2 \ IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2"
(is "?i \ ?ii")
proof - (* sledgehammer also proves this, but here is a detailed proof *)
{
fix s t
assume "(?i, s) \ t"
moreover
{
assume "bval b1 s \ bval b2 s"
hence "bval (And b1 b2) s" by simp
}
moreover
{
assume "\bval b1 s \ \bval b2 s"
hence "\bval (And b1 b2) s" by simp
}
ultimately
have "(?ii, s) \ t" by blast
}
then show ?thesis by auto (* the other direction is automatic *)
qed
text {* At the end of a loop the condition is always false *}
lemma While_end: "(WHILE b DO c, s) \ t \ \bval b t"
proof -
assume "(WHILE b DO c, s) \ t"
then obtain c' where "(c', s) \ t" and "c' = WHILE b DO c" by blast
then show "\bval b t"
by (induct c' s t rule: big_step_induct) auto
qed
lemma "WHILE Or b1 b2 DO c \ WHILE Or b1 b2 DO c; WHILE b1 DO c"
proof -
{
fix s
assume "\bval (Or b1 b2) s"
hence "\bval b1 s" by (auto simp add: Or_def)
}
then show ?thesis by (blast intro!: While_end)
qed
text {*
\Exercise{Nondeterminism}
In this exercise we extend our language with nondeterminism. We want
to include a command @{text "c\<^isub>1 OR c\<^isub>2"}, which expresses the
nondeterministic choice between two commands. That is, when executing
@{text "c\<^isub>1 OR c\<^isub>2"} either @{text "c\<^isub>1"} or @{text "c\<^isub>2"} may be
executed, and it is not specified which one.
\begin{enumerate}
\item Modify the datatype @{text com} to include a new constructor @{text OR}.
\item Adapt the big step semantics to include rules for the new construct.
\item Prove that @{text "c\<^isub>1 OR c\<^isub>2 \ c\<^isub>2 OR c\<^isub>1"}.
\item Adapt the small step semantics, and the equivalence proof of big
and small step semantics.
\end{enumerate}
\emph{Note:} It is easiest if you take the existing theories and modify them.
*}
text_raw{* \clearpage *}
text {*
\Homework{Step-Index Semantics}{November 30, 2011}
Note: In order to save you some typing, we provide a template for this
homework on the lecture's homepage.
In this homework, a denotational semantics for while-programs will be defined,
i.e., a function that takes a command and a state, and returns the result state.
In order to make this function well-defined even for non-terminating programs,
it is parameterized with an additional number, that indicates the maximum
number of steps to make. If the program has not yet terminated after this many
steps, @{text "None"} is returned.
*}
fun si :: "com \ state \ nat \ state option" where
si_None: "si _ s 0 = None" |
si_SKIP: "si SKIP s (Suc i) = Some s" |
si_ASS: "si (x::=v) s (Suc i) = Some (s(x:=aval v s))" |
si_SEMI: "si (c1;c2) s (Suc i) = (
case (si c1 s i) of None \ None | Some s' \ si c2 s' i)" |
si_IF: "si (IF b THEN c1 ELSE c2) s (Suc i) =
(if bval b s then si c1 s i else si c2 s i)" |
si_WHILE: "si (WHILE b DO c) s (Suc i) = (
if bval b s then
(case (si c s i) of
None \ None |
Some s' \ si (WHILE b DO c) s' i)
else Some s)"
text {*
Prove the equivalence of the big-step and the step-index semantics, i.e., show
that
@{text [display] "(\i. si c s i = Some s') \ big_step (c,s) s'"}
As this proof is more complicated than any proof in homeworks so far, we
will give a bit of guidance:
*}
text {* The two directions are proved separately. The proof of the first
direction should be quite straightforward, and is left to you. *}
lemma si_imp_bigstep: "si c s i = Some s' \ big_step (c,s) s'"
(*<*)
apply (induct c s i arbitrary: s' rule: si.induct)
apply (auto intro: big_step.intros split: option.split_asm split_if_asm)
done
(*>*)
text {*
For the other direction, it is useful to prove a monotonicity lemma first.
If the step-index semantics yields a result for index @{text "i"}, it
yields the same result for any @{text "i'\i"}.
*}
lemma si_mono: "si c s i = Some s' \ si c s (i+k) = Some s'"
proof (induction c s i arbitrary: s'
rule: si.induct[case_names None SKIP ASS SEMI IF WHILE])
case (WHILE b c s i s') thus ?case
txt {* Only the WHILE-case requires some effort. Hint: Make a
case distinction on the value of the condition @{text "b"}. *}
(*<*)
apply (cases "bval b s")
apply (auto split: option.split option.split_asm)
done
(*>*)
qed (auto split: option.split option.split_asm)
text {*
The main lemma is proved by induction over the big-step semantics. Remember
the adapted induction rule @{text "big_step_induct"} that nicely handles the
pattern @{text "big_step (c,s) s'"}.
*}
lemma bigstep_imp_si:
"big_step (c,s) s' \ \i. si c s i = Some s'"
proof (induct rule: big_step_induct)
txt {* We demonstrate the skip, while-true and sequential composition case
here. The other cases are left to you! *}
case (Skip s) have "si SKIP s 1 = Some s" by auto
thus ?case by blast
next
case (WhileTrue b s1 c s2 s3)
then obtain i1 i2 where "si c s1 i1 = Some s2"
and "si (WHILE b DO c) s2 i2 = Some s3" by auto
with si_mono[of c s1 i1 s2 i2]
si_mono[of "WHILE b DO c" s2 i2 s3 i1] have
"si c s1 (i1+i2) = Some s2"
and "si (WHILE b DO c) s2 (i2+i1) = Some s3"
by auto
hence "si (WHILE b DO c) s1 (Suc (i1+i2)) = Some s3"
using `bval b s1` by (auto simp add: add_ac)
thus ?case by blast
next
case (Semi c1 s1 s2 c2 s3)
then obtain i1 i2 where "si c1 s1 i1 = Some s2" and "si c2 s2 i2 = Some s3"
by auto
with si_mono[of c1 s1 i1 s2 i2]
si_mono[of c2 s2 i2 s3 i1]
have
"si c1 s1 (i1+i2) = Some s2" and "si c2 s2 (i2+i1) = Some s3"
by auto
hence "si (c1;c2) s1 (Suc (i1+i2)) = Some s3" by (auto simp add: add_ac)
thus ?case by blast
(*<*)
next
case (Assign x a s)
have "si (x::=a) s 1 = Some (s(x:=aval a s))" by auto
thus ?case by blast
next
case (IfTrue b s c1 t c2)
then obtain i where "si c1 s i = Some t" by blast
hence "si (IF b THEN c1 ELSE c2) s (Suc i) = Some t" using `bval b s` by auto
thus ?case by blast
next
case (IfFalse b s c2 t c1)
then obtain i where "si c2 s i = Some t" by blast
hence "si (IF b THEN c1 ELSE c2) s (Suc i) = Some t" using `\ bval b s` by auto
thus ?case by blast
next
case (WhileFalse b s c)
hence "si (WHILE b DO c) s 1 = Some s" by auto
thus ?case by blast
qed
(*>*)
text {* Finally, prove the main theorem of the homework: *}
theorem si_equiv_bigstep: "(\i. si c s i = Some s') \ big_step (c,s) s'"
(*<*) by (metis si_imp_bigstep bigstep_imp_si) (*>*)
end