header {* Assessed Exercise II: Semantics*}
(*<*) theory semantics_ex imports Main begin (*>*)
text {* This assessed exercise continues the proofs concerning
operational semantics that were outlined in the lectures. Please
deliver the completed exercise and theory file by the appropriate
deadline.*}
subsection {* Syntax and Semantics of Commands*}
text {*As in the lectures, the theory begins by specifying the types of
locations, values (here we use the natural numbers), states, and
finally arithmetic and boolean expressions. *}
typedecl loc
-- "an unspecified (arbitrary) type of locations
(adresses/names) for variables"
types
val = nat -- "or anything else, @{text nat} used in examples"
state = "loc \ val"
aexp = "state \ val"
bexp = "state \ bool"
-- "arithmetic and boolean expressions are not modelled explicitly here,"
-- "they are just functions on states"
text {* The commands include SKIP, which does nothing, assignments,
sequencing, conditionals and repetition. Note: our use of the
semicolon character for sequencing could cause syntactic ambiguities
if you attempt to use the semicolons to separate the preconditions of
theorems. You can instead express properties using the symbol @{text
\}. *}
datatype
com = SKIP
| Assign loc aexp (infixr ":==" 80)
| Semi com com (infixr ";" 70)
| Cond bexp com com ("IF _ THEN _ ELSE _" [0, 90, 90] 91)
| While bexp com ("WHILE _ DO _" [0, 91] 90)
text {* The big-step execution relation @{text evalc} is defined
inductively, as in the lectures. *}
inductive
evalc :: "[com,state,state] \ bool" ("\_, _\/ \ _" [0,0,60] 60)
where
Skip: "\SKIP,s\ \ s"
| Assign: "\x :== a,s\ \ s(x := a s)"
| Semi: "\c0,s\ \ s'' \ \c1,s''\ \ s' \ \c0; c1, s\ \ s'"
| IfTrue: "b s \ \c0,s\ \ s' \ \IF b THEN c0 ELSE c1, s\ \ s'"
| IfFalse: "\b s \ \c1,s\ \ s' \ \IF b THEN c0 ELSE c1, s\ \ s'"
| WhileFalse: "\b s \ \WHILE b DO c,s\ \ s"
| WhileTrue: "b s \ \c,s\ \ s'' \ \WHILE b DO c, s''\ \ s'
\ \WHILE b DO c, s\ \ s'"
text {*Next come commands that set up Isabelle's automation. The rules
that make up the inductive definition can be used as introduction
rules, and rule inversion from the definition supplies us with
elimination rules. This again is very similar to the material in the
lectures. *}
lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
inductive_cases skipE [elim!]: "\SKIP,s\ \ s'"
inductive_cases semiE [elim!]: "\c0; c1, s\ \ s'"
inductive_cases assignE [elim!]: "\x :== a,s\ \ s'"
inductive_cases ifE [elim!]: "\IF b THEN c0 ELSE c1, s\ \ s'"
inductive_cases whileE [elim]: "\WHILE b DO c,s\ \ s'"
subsection {*Equivalence of commands*}
text{*Two commands are equivalent if they allow the same transitions.*}
definition
equiv_c :: "com \ com \ bool" (infixr "\" 60)
where
"(c \ c') = (\s s'. (\c, s\ \ s') = (\c', s\ \ s'))"
text {* The following rule of inference, made available to Isabelle's
automatic methods as an introduction rule, allows us to prove semantic
equivalence statements. This again was covered in the lectures. *}
lemma equivI [intro!]:
"(\s s'. \c, s\ \ s' = \c', s\ \ s') \ c \ c'"
(*<*)by (auto simp add: equiv_c_def)(*>*)
text {* \begin{task}Prove the following theorem. \end{task}
*}
lemma equiv_if3:
"c1 \ c2 \
(IF b1 THEN c1 ELSE IF b2 THEN c2 ELSE c3) \
(IF b2 THEN c2 ELSE IF b1 THEN c1 ELSE c3)"
(*<*)oops(*>*)
text {* \begin{task}
Prove the following theorem, which establishes that semantic
equivalence is a congruence relation with respect to @{text
While}. Unlike analogous proofs for other constructors, this proof
requires a lemma proved by induction.
\end{task}
*}
lemma equiv_while:
"c \ c' \ (WHILE b DO c) \ (WHILE b DO c')"
(*<*)oops(*>*)
text {* \begin{task}
Prove the following theorem, which expresses that the
Boolean expression guarding the loop holds at the start of the loop
body.\end{task}
*}
lemma equiv_while_if:
"(WHILE b1 DO IF b2 THEN c1 ELSE c2) \
(WHILE b1 DO IF (\s. b1 s & b2 s) THEN c1 ELSE c2)"
(*<*)oops(*>*)
subsection{*A Command Preserves a Boolean Expression*}
(*<*)consts
preserves :: "com \ bexp \ bool"
(*>*)
text {* The following two properties allow a command @{text c} to be
moved out of a conditional command. One of them can be proved as shown.
The other one can be proved subject to the precondition
@{text "preserves c b"}, which expresses that the command @{text c}
preserves the value of the Boolean expression @{text b}.
\begin{task}
Formalise the concept @{text "preserves c b"} in Isabelle, and prove
both properties in the appropriate form.\end{task} *}
lemma equiv_if1:
"(IF b THEN (c; c1) ELSE (c; c2)) \ (c; (IF b THEN c1 ELSE c2))"
(*<*)oops(*>*)
lemma equiv_if2:
"(IF b THEN (c1; c) ELSE (c2; c)) \ ((IF b THEN c1 ELSE c2); c)"
(*<*)oops(*>*)
(*<*) end (*>*)