43158

1 
(* Author: Tobias Nipkow *)


2 


3 
header "Definite Assignment Analysis"


4 

45716

5 
theory Vars imports BExp

43158

6 
begin


7 

45716

8 
subsection "Show sets of variables as lists"


9 


10 
text {* Sets may be infinite and are not always displayed by element


11 
if computed as values. Lists do not have this problem.


12 


13 
We define a function @{text show} that converts a set of


14 
variable names into a list. To keep things simple, we rely on


15 
the convention that we only use single letter names.


16 
*}


17 
definition


18 
letters :: "string list" where


19 
"letters = map (\<lambda>c. [c]) chars"


20 


21 
definition


22 
"show" :: "string set \<Rightarrow> string list" where


23 
"show S = filter (\<lambda>x. x \<in> S) letters"


24 


25 
value "show {''x'', ''z''}"


26 

43158

27 
subsection "The Variables in an Expression"


28 


29 
text{* We need to collect the variables in both arithmetic and boolean


30 
expressions. For a change we do not introduce two functions, e.g.\ @{text


31 
avars} and @{text bvars}, but we overload the name @{text vars}


32 
via a \emph{type class}, a device that originated with Haskell: *}


33 


34 
class vars =

45212

35 
fixes vars :: "'a \<Rightarrow> vname set"

43158

36 


37 
text{* This defines a type class ``vars'' with a single


38 
function of (coincidentally) the same name. Then we define two separated


39 
instances of the class, one for @{typ aexp} and one for @{typ bexp}: *}


40 


41 
instantiation aexp :: vars


42 
begin


43 

45212

44 
fun vars_aexp :: "aexp \<Rightarrow> vname set" where

45774

45 
"vars (N n) = {}" 


46 
"vars (V x) = {x}" 


47 
"vars (Plus a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"

43158

48 


49 
instance ..


50 


51 
end


52 


53 
value "vars(Plus (V ''x'') (V ''y''))"


54 


55 
text{* We need to convert functions to lists before we can view them: *}


56 


57 
value "show (vars(Plus (V ''x'') (V ''y'')))"


58 


59 
instantiation bexp :: vars


60 
begin


61 

45212

62 
fun vars_bexp :: "bexp \<Rightarrow> vname set" where

45774

63 
"vars (Bc v) = {}" 


64 
"vars (Not b) = vars b" 


65 
"vars (And b\<^isub>1 b\<^isub>2) = vars b\<^isub>1 \<union> vars b\<^isub>2" 


66 
"vars (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"

43158

67 


68 
instance ..


69 


70 
end


71 


72 
value "show (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))"


73 


74 
abbreviation


75 
eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"


76 
("(_ =/ _/ on _)" [50,0,50] 50) where


77 
"f = g on X == \<forall> x \<in> X. f x = g x"


78 


79 
lemma aval_eq_if_eq_on_vars[simp]:


80 
"s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"

45015

81 
apply(induction a)

43158

82 
apply simp_all


83 
done


84 


85 
lemma bval_eq_if_eq_on_vars:


86 
"s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"

45015

87 
proof(induction b)

43158

88 
case (Less a1 a2)


89 
hence "aval a1 s\<^isub>1 = aval a1 s\<^isub>2" and "aval a2 s\<^isub>1 = aval a2 s\<^isub>2" by simp_all


90 
thus ?case by simp


91 
qed simp_all


92 


93 
end
