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