src/HOL/IMP/Def_Ass.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43158 686fa0a0696e
child 45212 e87feee00a4c
permissions -rw-r--r--
remove lemma stupid_ext
     1 theory Def_Ass imports Vars Com
     2 begin
     3 
     4 subsection "Definite Assignment Analysis"
     5 
     6 inductive D :: "name set \<Rightarrow> com \<Rightarrow> name set \<Rightarrow> bool" where
     7 Skip: "D A SKIP A" |
     8 Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
     9 Semi: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |
    10 If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^isub>1 A\<^isub>1;  D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
    11   D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
    12 While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
    13 
    14 inductive_cases [elim!]:
    15 "D A SKIP A'"
    16 "D A (x ::= a) A'"
    17 "D A (c1;c2) A'"
    18 "D A (IF b THEN c1 ELSE c2) A'"
    19 "D A (WHILE b DO c) A'"
    20 
    21 lemma D_incr: 
    22   "D A c A' \<Longrightarrow> A \<subseteq> A'"
    23 by (induct rule: D.induct) auto
    24 
    25 end