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