43158
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
50303
|
3 |
header "Definite Initialization Analysis"
|
43158
|
4 |
|
51698
|
5 |
theory Vars imports Com
|
43158
|
6 |
begin
|
|
7 |
|
|
8 |
subsection "The Variables in an Expression"
|
|
9 |
|
|
10 |
text{* We need to collect the variables in both arithmetic and boolean
|
|
11 |
expressions. For a change we do not introduce two functions, e.g.\ @{text
|
|
12 |
avars} and @{text bvars}, but we overload the name @{text vars}
|
|
13 |
via a \emph{type class}, a device that originated with Haskell: *}
|
|
14 |
|
|
15 |
class vars =
|
45212
|
16 |
fixes vars :: "'a \<Rightarrow> vname set"
|
43158
|
17 |
|
|
18 |
text{* This defines a type class ``vars'' with a single
|
|
19 |
function of (coincidentally) the same name. Then we define two separated
|
|
20 |
instances of the class, one for @{typ aexp} and one for @{typ bexp}: *}
|
|
21 |
|
|
22 |
instantiation aexp :: vars
|
|
23 |
begin
|
|
24 |
|
45212
|
25 |
fun vars_aexp :: "aexp \<Rightarrow> vname set" where
|
45774
|
26 |
"vars (N n) = {}" |
|
|
27 |
"vars (V x) = {x}" |
|
|
28 |
"vars (Plus a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
|
43158
|
29 |
|
|
30 |
instance ..
|
|
31 |
|
|
32 |
end
|
|
33 |
|
50173
|
34 |
value "vars (Plus (V ''x'') (V ''y''))"
|
43158
|
35 |
|
|
36 |
instantiation bexp :: vars
|
|
37 |
begin
|
|
38 |
|
45212
|
39 |
fun vars_bexp :: "bexp \<Rightarrow> vname set" where
|
45774
|
40 |
"vars (Bc v) = {}" |
|
|
41 |
"vars (Not b) = vars b" |
|
|
42 |
"vars (And b\<^isub>1 b\<^isub>2) = vars b\<^isub>1 \<union> vars b\<^isub>2" |
|
|
43 |
"vars (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
|
43158
|
44 |
|
|
45 |
instance ..
|
|
46 |
|
|
47 |
end
|
|
48 |
|
50173
|
49 |
value "vars (Less (Plus (V ''z'') (V ''y'')) (V ''x''))"
|
43158
|
50 |
|
|
51 |
abbreviation
|
|
52 |
eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
|
|
53 |
("(_ =/ _/ on _)" [50,0,50] 50) where
|
|
54 |
"f = g on X == \<forall> x \<in> X. f x = g x"
|
|
55 |
|
|
56 |
lemma aval_eq_if_eq_on_vars[simp]:
|
|
57 |
"s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2"
|
45015
|
58 |
apply(induction a)
|
43158
|
59 |
apply simp_all
|
|
60 |
done
|
|
61 |
|
|
62 |
lemma bval_eq_if_eq_on_vars:
|
|
63 |
"s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2"
|
45015
|
64 |
proof(induction b)
|
43158
|
65 |
case (Less a1 a2)
|
|
66 |
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
|
|
67 |
thus ?case by simp
|
|
68 |
qed simp_all
|
|
69 |
|
52072
|
70 |
fun lvars :: "com \<Rightarrow> vname set" where
|
|
71 |
"lvars SKIP = {}" |
|
|
72 |
"lvars (x::=e) = {x}" |
|
|
73 |
"lvars (c1;;c2) = lvars c1 \<union> lvars c2" |
|
|
74 |
"lvars (IF b THEN c1 ELSE c2) = lvars c1 \<union> lvars c2" |
|
|
75 |
"lvars (WHILE b DO c) = lvars c"
|
|
76 |
|
|
77 |
fun rvars :: "com \<Rightarrow> vname set" where
|
|
78 |
"rvars SKIP = {}" |
|
|
79 |
"rvars (x::=e) = vars e" |
|
|
80 |
"rvars (c1;;c2) = rvars c1 \<union> rvars c2" |
|
|
81 |
"rvars (IF b THEN c1 ELSE c2) = vars b \<union> rvars c1 \<union> rvars c2" |
|
|
82 |
"rvars (WHILE b DO c) = vars b \<union> rvars c"
|
51698
|
83 |
|
|
84 |
instantiation com :: vars
|
|
85 |
begin
|
|
86 |
|
52072
|
87 |
definition "vars_com c = lvars c \<union> rvars c"
|
51698
|
88 |
|
|
89 |
instance ..
|
|
90 |
|
43158
|
91 |
end
|
51698
|
92 |
|
52072
|
93 |
lemma vars_com_simps[simp]:
|
|
94 |
"vars SKIP = {}"
|
|
95 |
"vars (x::=e) = {x} \<union> vars e"
|
|
96 |
"vars (c1;;c2) = vars c1 \<union> vars c2"
|
|
97 |
"vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2"
|
|
98 |
"vars (WHILE b DO c) = vars b \<union> vars c"
|
|
99 |
by(auto simp: vars_com_def)
|
51698
|
100 |
|
|
101 |
lemma finite_avars[simp]: "finite(vars(a::aexp))"
|
|
102 |
by(induction a) simp_all
|
|
103 |
|
|
104 |
lemma finite_bvars[simp]: "finite(vars(b::bexp))"
|
52072
|
105 |
by(induction b) simp_all
|
|
106 |
|
|
107 |
lemma finite_lvars[simp]: "finite(lvars(c))"
|
|
108 |
by(induction c) simp_all
|
|
109 |
|
|
110 |
lemma finite_rvars[simp]: "finite(rvars(c))"
|
|
111 |
by(induction c) simp_all
|
51698
|
112 |
|
|
113 |
lemma finite_cvars[simp]: "finite(vars(c::com))"
|
52072
|
114 |
by(simp add: vars_com_def)
|
51698
|
115 |
|
|
116 |
end
|