Theory Def_Init

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 A⇣1 c⇣1 A⇣2;  D A⇣2 c⇣2 A⇣3 |] ==> D A⇣1 (c⇣1; c⇣2) A⇣3" |
If: "[| vars b ⊆ A;  D A c⇣1 A⇣1;  D A c⇣2 A⇣2 |] ==>
  D A (IF b THEN c⇣1 ELSE c⇣2) (A⇣1 Int A⇣2)" |
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