(*<*) theory sol03 imports "~~/src/HOL/IMP/AExp" begin (*>*) text \\ExerciseSheet{3}{08.~11.~2016}\ text \ This exercise sheet depends on definitions from the file \AExp.thy\, which may be imported as follows: \textbf{theory} \textit{Ex03} \\ \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 \subst :: vname \ aexp \ aexp \ aexp\ that performs a syntactic substitution, i.e., \subst x a' a\ shall be the expression \a\ where every occurrence of variable \x\ has been replaced by expression \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 \x\ by an expression \a'\, we can also change the state \s\ by replacing the value of \x\ by the value of \a'\ under \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 \s(x:=v)\ updates a function at point \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 (\'\) to them, e.g., \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 \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 \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 \aval'\ for this intermediate language should have type \aexp' \ state \ val\state\. After completing the entire exercise with this version, modify your definitions to add division and exceptions.)\ text \ Test your function for some terms. Is the output as expected? Note: \<>\ 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)+ done (*>*) text \ Hint: If \auto\ on its own leaves you with an \if\ in the assumptions or with a \case\-statement, you should modify it like this: (\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 (*>*)