(*<*)
theory sol02
imports "~~/src/HOL/IMP/AExp"
begin
(*>*)
text {* \ExerciseSheet{2}{22.~10.~2013} *}
(*
text {*
This exercise sheet depends on definitions from the file
@{text "AExp.thy"}, which may be imported as follows:
\textbf{theory} \textit{Ex02} \\
\textbf{imports} \textit{"\isachartilde\isachartilde/src/HOL/IMP/AExp"} \\
\textbf{begin}
*}
*)
text {* \Exercise{Substitution Lemma}
A syntactic substitution replaces a variable by an expression.
Define a function @{text "subst :: vname \ aexp \ aexp \ aexp"} that
performs a syntactic substitution, i.e., @{text "subst x a' a"} shall be the
expression @{text a} where every occurrence of variable @{text x} has been replaced
by expression @{text a'}.
*}
(*<*)
fun subst :: "vname \ aexp \ aexp \ aexp" where
"subst x a' (N n) = N n" |
"subst x a' (V y) = (if x=y then a' else V y)" |
"subst x a' (Plus a1 a2) = Plus (subst x a' a1) (subst x a' a2)"
(*>*)
text {*
Instead of syntactically replacing a variable @{text x} by an expression
@{text a'}, we can also change the state @{text s} by replacing the value of @{text x}
by the value of @{text a'} under @{text s}. This is called {\em semantic substitution}.
The {\em substitution lemma} states that semantic and syntactic substitution are
compatible. Prove the substitution lemma:
*}
lemma subst_lemma: "aval (subst x a' a) s = aval a (s(x:=aval a' s))"
(*<*)
by (induct a) auto
(*>*)
text {*
Note: The expression @{text "s(x:=v)"} updates a function at point
@{text "x"}. It is defined as:
@{thm [display] fun_upd_def[THEN meta_eq_to_obj_eq, no_vars]}
*}
text {*
Compositionality means that one can replace equal expressions by equal expressions.
Use the substitution lemma to prove {\em compositionality} of arithmetic expressions:
*}
lemma comp: "aval a1 s = aval a2 s \ aval (subst x a1 a) s = aval (subst x a2 a) s"
(*<*) by (simp add: subst_lemma)(*>*)
text {* \Exercise{Arithmetic Expressions With Side-Effects and Exceptions}
We want to extend arithmetic expressions by the division operation and
by the postfix increment operation $x{+}{+}$, as known from Java or C++. *}
text {* The problem with the division operation is that division by
zero is not defined. In this case, the arithmetic expression should
evaluate to a special value indicating an exception. *}
text {* The increment can only be applied to variables. The problem
is, that it changes the state, and the evaluation of the rest of the
term depends on the changed state. We assume left to right
evaluation order here. *}
text {* Define the datatype of extended arithmetic expressions. Hint:
If you do not want to hide the standard constructor names from IMP,
add a tick (@{text"'"}) to them, e.g., @{text "V' x"}. *}
(*<*)
datatype aexp' = N' int | V' vname | PI' vname | Plus' aexp' aexp' | Div' aexp' aexp'
(*>*)
text {*
The semantics of extended arithmetic expressions has the type
@{text "aval' :: aexp' \ state \ (val\state) option"},
i.e., it takes an expression and a state, and returns a value and a new state, or
an error value.
Define the function @{text "aval'"}.
*}
(*<*)
fun aval' where
"aval' (N' n) s = Some (n,s)" |
"aval' (V' x) s = Some (s x,s)" |
"aval' (PI' x) s = Some (s x,s(x:=s x+1))" |
"aval' (Plus' a1 a2) s = (
case aval' a1 s of
None \ None |
Some (v1,s') \ (
case aval' a2 s' of
None \ None |
Some (v2,s'') \ Some (v1+v2,s'')
)
)" |
"aval' (Div' a1 a2) s = (
case aval' a1 s of
None \ None |
Some (v1,s') \ (
case aval' a2 s' of
None \ None |
Some (v2,s'') \ if v2=0 then None else Some (v1 div v2,s'')
)
)"
(*>*)
text {* (Hint: To make things easier, we recommend an incremental
approach to this exercise: First define arithmetic expressions with
incrementing, but without division. The function @{text
"aval'"} for this intermediate language should have type @{text
"aexp' \ state \ val\state"}. After completing the entire exercise
with this version, then modify your definitions to add division and
exceptions.) *}
text {*
Test your function for some terms. Is the output as expected?
Note: @{text "<>"} is an abbreviation for the state that assigns every
variable to zero:
@{thm [display] null_state_def[where 'b=int, no_vars]}
*}
value "aval' (Div' (V' ''x'') (V' ''x'')) <>"
value "aval' (Div' (PI' ''x'') (V' ''x'')) <''x'':=1>"
value "aval' (Plus' (PI' ''x'') (V' ''x'')) <>"
value "aval' (Plus' (Plus' (PI' ''x'') (PI' ''x'')) (PI' ''x'')) <>"
text {*
Is the plus-operation still commutative? Prove or disprove!
*}
(*<*)
lemma "aval' (Plus' (PI' x) (V' x)) <> \ aval' (Plus' (V' x) (PI' x)) <>"
by auto
(*>*)
(*<*) (* Nitpick also works ! *)
lemma "aval' (Plus' a1 a2) s = aval' (Plus' a2 a1) s"
(*nitpick*)
oops
(*>*)
text {*
Show that the valuation of a variable cannot decrease during evaluation of
an expression:
*}
lemma aval'_inc: "aval' a s = Some (v,s') \ s x \ s' x"
(*<*)
apply (induct a arbitrary: s s' v) apply auto
apply (fastforce split: option.splits if_splits)+
(* OR:
apply (blast intro: order_trans)+
OR:
apply force+
*)
done
(*>*)
text {*
Hint: If @{text "auto"} on its own leaves you with an @{text "if"} in the
assumptions or with a @{text "case"}-statement, you should modify it like
this: (@{text "auto split: split_if_asm option.splits"}).
*}
text {*
\Exercise{Variables of Expression}
Define a function that returns the set of variables occurring in an
arithmetic expression.
*}
fun vars :: "aexp \ vname set" where
(*<*)
"vars (N _) = {}"
| "vars (V x) = {x}"
| "vars (Plus a1 a2) = vars a1 \ vars a2"
(*>*)
text {*
Show that arithmetic expressions do not depend on variables
that they don't contain.
*}
lemma ndep: "x\vars e \ aval e (s(x:=v)) = aval e s"
by (induction e) auto
(*<*)
end
(*>*)