|
43158
|
1 |
theory Def_Ass imports Vars Com
|
|
|
2 |
begin
|
|
|
3 |
|
|
|
4 |
subsection "Definite Assignment Analysis"
|
|
|
5 |
|
|
|
6 |
inductive D :: "name set \<Rightarrow> com \<Rightarrow> name set \<Rightarrow> bool" where
|
|
|
7 |
Skip: "D A SKIP A" |
|
|
|
8 |
Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
|
|
|
9 |
Semi: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2; D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |
|
|
|
10 |
If: "\<lbrakk> vars b \<subseteq> A; D A c\<^isub>1 A\<^isub>1; D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
|
|
|
11 |
D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
|
|
|
12 |
While: "\<lbrakk> vars b \<subseteq> A; D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
|
|
|
13 |
|
|
|
14 |
inductive_cases [elim!]:
|
|
|
15 |
"D A SKIP A'"
|
|
|
16 |
"D A (x ::= a) A'"
|
|
|
17 |
"D A (c1;c2) A'"
|
|
|
18 |
"D A (IF b THEN c1 ELSE c2) A'"
|
|
|
19 |
"D A (WHILE b DO c) A'"
|
|
|
20 |
|
|
|
21 |
lemma D_incr:
|
|
|
22 |
"D A c A' \<Longrightarrow> A \<subseteq> A'"
|
|
|
23 |
by (induct rule: D.induct) auto
|
|
|
24 |
|
|
|
25 |
end
|