Theory Def_Init

theory Def_Init
imports Vars
theory Def_Init
imports Vars Com
begin

subsection "Definite Initialization Analysis"

inductive D :: "vname set => com => vname set => bool" where
Skip: "D A SKIP A" |
Assign: "vars a ⊆ A ==> D A (x ::= a) (insert x A)" |
Seq: "[| D A1 c1 A2; D A2 c2 A3 |] ==> D A1 (c1;; c2) A3" |
If: "[| vars b ⊆ A; D A c1 A1; D A c2 A2 |] ==>
D A (IF b THEN c1 ELSE c2) (A1 Int A2)"
|
While: "[| vars b ⊆ A; D A c A' |] ==> D A (WHILE b DO c) A"

inductive_cases [elim!]:
"D A SKIP A'"
"D A (x ::= a) A'"
"D A (c1;;c2) A'"
"D A (IF b THEN c1 ELSE c2) A'"
"D A (WHILE b DO c) A'"

lemma D_incr:
"D A c A' ==> A ⊆ A'"
by (induct rule: D.induct) auto

end