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