|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 header "Definite Assignment Analysis" |
|
4 |
|
5 theory Vars imports Util BExp |
|
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 = |
|
16 fixes vars :: "'a \<Rightarrow> name set" |
|
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 |
|
25 fun vars_aexp :: "aexp \<Rightarrow> name set" where |
|
26 "vars_aexp (N n) = {}" | |
|
27 "vars_aexp (V x) = {x}" | |
|
28 "vars_aexp (Plus a\<^isub>1 a\<^isub>2) = vars_aexp a\<^isub>1 \<union> vars_aexp a\<^isub>2" |
|
29 |
|
30 instance .. |
|
31 |
|
32 end |
|
33 |
|
34 value "vars(Plus (V ''x'') (V ''y''))" |
|
35 |
|
36 text{* We need to convert functions to lists before we can view them: *} |
|
37 |
|
38 value "show (vars(Plus (V ''x'') (V ''y'')))" |
|
39 |
|
40 instantiation bexp :: vars |
|
41 begin |
|
42 |
|
43 fun vars_bexp :: "bexp \<Rightarrow> name set" where |
|
44 "vars_bexp (B bv) = {}" | |
|
45 "vars_bexp (Not b) = vars_bexp b" | |
|
46 "vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" | |
|
47 "vars_bexp (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2" |
|
48 |
|
49 instance .. |
|
50 |
|
51 end |
|
52 |
|
53 value "show (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))" |
|
54 |
|
55 abbreviation |
|
56 eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" |
|
57 ("(_ =/ _/ on _)" [50,0,50] 50) where |
|
58 "f = g on X == \<forall> x \<in> X. f x = g x" |
|
59 |
|
60 lemma aval_eq_if_eq_on_vars[simp]: |
|
61 "s\<^isub>1 = s\<^isub>2 on vars a \<Longrightarrow> aval a s\<^isub>1 = aval a s\<^isub>2" |
|
62 apply(induct a) |
|
63 apply simp_all |
|
64 done |
|
65 |
|
66 lemma bval_eq_if_eq_on_vars: |
|
67 "s\<^isub>1 = s\<^isub>2 on vars b \<Longrightarrow> bval b s\<^isub>1 = bval b s\<^isub>2" |
|
68 proof(induct b) |
|
69 case (Less a1 a2) |
|
70 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 |
|
71 thus ?case by simp |
|
72 qed simp_all |
|
73 |
|
74 end |