src/HOL/IMP/Def_Ass.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 47818 151d137f1095
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
kleing@43158
     1
theory Def_Ass imports Vars Com
kleing@43158
     2
begin
kleing@43158
     3
kleing@43158
     4
subsection "Definite Assignment Analysis"
kleing@43158
     5
nipkow@45212
     6
inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
kleing@43158
     7
Skip: "D A SKIP A" |
kleing@43158
     8
Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
kleing@43158
     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" |
kleing@43158
    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>
kleing@43158
    11
  D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
kleing@43158
    12
While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
kleing@43158
    13
kleing@43158
    14
inductive_cases [elim!]:
kleing@43158
    15
"D A SKIP A'"
kleing@43158
    16
"D A (x ::= a) A'"
kleing@43158
    17
"D A (c1;c2) A'"
kleing@43158
    18
"D A (IF b THEN c1 ELSE c2) A'"
kleing@43158
    19
"D A (WHILE b DO c) A'"
kleing@43158
    20
kleing@43158
    21
lemma D_incr: 
kleing@43158
    22
  "D A c A' \<Longrightarrow> A \<subseteq> A'"
kleing@43158
    23
by (induct rule: D.induct) auto
kleing@43158
    24
kleing@43158
    25
end