src/HOL/IMP/Def_Init.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 53015 a1119cf551e8
permissions -rw-r--r--
Lots of new material for multivariate analysis
nipkow@50161
     1
theory Def_Init
nipkow@50161
     2
imports Vars Com
kleing@43158
     3
begin
kleing@43158
     4
nipkow@50161
     5
subsection "Definite Initialization Analysis"
kleing@43158
     6
nipkow@45212
     7
inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
kleing@43158
     8
Skip: "D A SKIP A" |
kleing@43158
     9
Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
wenzelm@53015
    10
Seq: "\<lbrakk> D A\<^sub>1 c\<^sub>1 A\<^sub>2;  D A\<^sub>2 c\<^sub>2 A\<^sub>3 \<rbrakk> \<Longrightarrow> D A\<^sub>1 (c\<^sub>1;; c\<^sub>2) A\<^sub>3" |
wenzelm@53015
    11
If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^sub>1 A\<^sub>1;  D A c\<^sub>2 A\<^sub>2 \<rbrakk> \<Longrightarrow>
wenzelm@53015
    12
  D A (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (A\<^sub>1 Int A\<^sub>2)" |
kleing@43158
    13
While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
kleing@43158
    14
kleing@43158
    15
inductive_cases [elim!]:
kleing@43158
    16
"D A SKIP A'"
kleing@43158
    17
"D A (x ::= a) A'"
nipkow@52046
    18
"D A (c1;;c2) A'"
kleing@43158
    19
"D A (IF b THEN c1 ELSE c2) A'"
kleing@43158
    20
"D A (WHILE b DO c) A'"
kleing@43158
    21
kleing@43158
    22
lemma D_incr: 
kleing@43158
    23
  "D A c A' \<Longrightarrow> A \<subseteq> A'"
kleing@43158
    24
by (induct rule: D.induct) auto
kleing@43158
    25
kleing@43158
    26
end