(*<*)
theory tmpl09
imports Main "~~/src/HOL/IMP/Vars" "~~/src/HOL/IMP/Small_Step"
begin
(*>*)
text {* \ExerciseSheet{9}{8.~12.~2015} *}
text {*
\Exercise{Available Expressions}
*}
text {*
Regard the following function @{text "AA"}, which computes the {\em
available assignments} of a command. An available assignment is a
pair of a variable and an expression such that the variable holds
the value of the expression in the current state. The function
@{text "AA c A"} computes the available assignments after executing
command @{text "c"}, assuming that @{text "A"} is the set of
available assignments for the initial state.
Note that available assignments can be used for program
optimization, by avoiding recomputation of expressions whose value
is already available in some variable.
*}
fun AA :: "com \ (vname \ aexp) set \ (vname \ aexp) set" where
"AA SKIP A = A" |
"AA (x ::= a) A = (if x \ vars a then {} else {(x, a)})
\ {(x', a'). (x', a') \ A \ x \ {x'} \ vars a'}" |
"AA (c\<^sub>1;; c\<^sub>2) A = (AA c\<^sub>2 \ AA c\<^sub>1) A" |
"AA (IF b THEN c\<^sub>1 ELSE c\<^sub>2) A = AA c\<^sub>1 A \ AA c\<^sub>2 A" |
"AA (WHILE b DO c) A = A \ AA c A"
end