diff -r b505be6f029a -r 686fa0a0696e src/HOL/IMP/Def_Ass.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IMP/Def_Ass.thy Mon Jun 06 16:29:38 2011 +0200 @@ -0,0 +1,25 @@ +theory Def_Ass imports Vars Com +begin + +subsection "Definite Assignment Analysis" + +inductive D :: "name set \ com \ name set \ bool" where +Skip: "D A SKIP A" | +Assign: "vars a \ A \ D A (x ::= a) (insert x A)" | +Semi: "\ D A\<^isub>1 c\<^isub>1 A\<^isub>2; D A\<^isub>2 c\<^isub>2 A\<^isub>3 \ \ D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" | +If: "\ vars b \ A; D A c\<^isub>1 A\<^isub>1; D A c\<^isub>2 A\<^isub>2 \ \ + D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>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