43158

1 
theory Def_Ass imports Vars Com


2 
begin


3 


4 
subsection "Definite Assignment Analysis"


5 

45212

6 
inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where

43158

7 
Skip: "D A SKIP A" 


8 
Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" 

47818

9 
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" 

43158

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
