src/HOL/IMP/Live.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 45770 5d35cb2c0f02
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
(* Author: Tobias Nipkow *)
kleing@43158
     2
kleing@43158
     3
header "Live Variable Analysis"
kleing@43158
     4
kleing@43158
     5
theory Live imports Vars Big_Step
kleing@43158
     6
begin
kleing@43158
     7
kleing@43158
     8
subsection "Liveness Analysis"
kleing@43158
     9
nipkow@45212
    10
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
kleing@43158
    11
"L SKIP X = X" |
kleing@43158
    12
"L (x ::= a) X = X-{x} \<union> vars a" |
kleing@43158
    13
"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
kleing@43158
    14
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
kleing@43158
    15
"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
kleing@43158
    16
kleing@43158
    17
value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
kleing@43158
    18
kleing@43158
    19
value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
kleing@43158
    20
nipkow@45212
    21
fun "kill" :: "com \<Rightarrow> vname set" where
kleing@43158
    22
"kill SKIP = {}" |
kleing@43158
    23
"kill (x ::= a) = {x}" |
kleing@43158
    24
"kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
kleing@43158
    25
"kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
kleing@43158
    26
"kill (WHILE b DO c) = {}"
kleing@43158
    27
nipkow@45212
    28
fun gen :: "com \<Rightarrow> vname set" where
kleing@43158
    29
"gen SKIP = {}" |
kleing@43158
    30
"gen (x ::= a) = vars a" |
kleing@43158
    31
"gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
kleing@43158
    32
"gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
kleing@43158
    33
"gen (WHILE b DO c) = vars b \<union> gen c"
kleing@43158
    34
kleing@43158
    35
lemma L_gen_kill: "L c X = (X - kill c) \<union> gen c"
kleing@43158
    36
by(induct c arbitrary:X) auto
kleing@43158
    37
kleing@43158
    38
lemma L_While_subset: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
kleing@43158
    39
by(auto simp add:L_gen_kill)
kleing@43158
    40
kleing@43158
    41
kleing@43158
    42
subsection "Soundness"
kleing@43158
    43
kleing@43158
    44
theorem L_sound:
kleing@43158
    45
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
kleing@43158
    46
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
nipkow@45015
    47
proof (induction arbitrary: X t rule: big_step_induct)
kleing@43158
    48
  case Skip then show ?case by auto
kleing@43158
    49
next
kleing@43158
    50
  case Assign then show ?case
kleing@43158
    51
    by (auto simp: ball_Un)
kleing@43158
    52
next
kleing@43158
    53
  case (Semi c1 s1 s2 c2 s3 X t1)
nipkow@45015
    54
  from Semi.IH(1) Semi.prems obtain t2 where
kleing@43158
    55
    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
kleing@43158
    56
    by simp blast
nipkow@45015
    57
  from Semi.IH(2)[OF s2t2] obtain t3 where
kleing@43158
    58
    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
kleing@43158
    59
    by auto
kleing@43158
    60
  show ?case using t12 t23 s3t3 by auto
kleing@43158
    61
next
kleing@43158
    62
  case (IfTrue b s c1 s' c2)
kleing@43158
    63
  hence "s = t on vars b" "s = t on L c1 X" by auto
kleing@43158
    64
  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
kleing@43158
    65
  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
kleing@43158
    66
    "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
kleing@43158
    67
  thus ?case using `bval b t` by auto
kleing@43158
    68
next
kleing@43158
    69
  case (IfFalse b s c2 s' c1)
kleing@43158
    70
  hence "s = t on vars b" "s = t on L c2 X" by auto
kleing@43158
    71
  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
kleing@43158
    72
  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
kleing@43158
    73
    "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
kleing@43158
    74
  thus ?case using `~bval b t` by auto
kleing@43158
    75
next
kleing@43158
    76
  case (WhileFalse b s c)
kleing@43158
    77
  hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
kleing@43158
    78
  thus ?case using WhileFalse(2) by auto
kleing@43158
    79
next
kleing@43158
    80
  case (WhileTrue b s1 c s2 s3 X t1)
kleing@43158
    81
  let ?w = "WHILE b DO c"
kleing@43158
    82
  from `bval b s1` WhileTrue(6) have "bval b t1"
kleing@43158
    83
    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
kleing@43158
    84
  have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
kleing@43158
    85
    by (blast)
nipkow@45015
    86
  from WhileTrue.IH(1)[OF this] obtain t2 where
kleing@43158
    87
    "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
nipkow@45015
    88
  from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
kleing@43158
    89
    by auto
kleing@43158
    90
  with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
kleing@43158
    91
qed
kleing@43158
    92
kleing@43158
    93
kleing@43158
    94
subsection "Program Optimization"
kleing@43158
    95
kleing@43158
    96
text{* Burying assignments to dead variables: *}
nipkow@45212
    97
fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
kleing@43158
    98
"bury SKIP X = SKIP" |
kleing@43158
    99
"bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
kleing@43158
   100
"bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
kleing@43158
   101
"bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
kleing@43158
   102
"bury (WHILE b DO c) X = WHILE b DO bury c (vars b \<union> X \<union> L c X)"
kleing@43158
   103
kleing@43158
   104
text{* We could prove the analogous lemma to @{thm[source]L_sound}, and the
kleing@43158
   105
proof would be very similar. However, we phrase it as a semantics
kleing@43158
   106
preservation property: *}
kleing@43158
   107
kleing@43158
   108
theorem bury_sound:
kleing@43158
   109
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
kleing@43158
   110
  \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
nipkow@45015
   111
proof (induction arbitrary: X t rule: big_step_induct)
kleing@43158
   112
  case Skip then show ?case by auto
kleing@43158
   113
next
kleing@43158
   114
  case Assign then show ?case
kleing@43158
   115
    by (auto simp: ball_Un)
kleing@43158
   116
next
kleing@43158
   117
  case (Semi c1 s1 s2 c2 s3 X t1)
nipkow@45015
   118
  from Semi.IH(1) Semi.prems obtain t2 where
kleing@43158
   119
    t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
kleing@43158
   120
    by simp blast
nipkow@45015
   121
  from Semi.IH(2)[OF s2t2] obtain t3 where
kleing@43158
   122
    t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
kleing@43158
   123
    by auto
kleing@43158
   124
  show ?case using t12 t23 s3t3 by auto
kleing@43158
   125
next
kleing@43158
   126
  case (IfTrue b s c1 s' c2)
kleing@43158
   127
  hence "s = t on vars b" "s = t on L c1 X" by auto
kleing@43158
   128
  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
kleing@43158
   129
  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
kleing@43158
   130
    "(bury c1 X, t) \<Rightarrow> t'" "s' =t' on X" by auto
kleing@43158
   131
  thus ?case using `bval b t` by auto
kleing@43158
   132
next
kleing@43158
   133
  case (IfFalse b s c2 s' c1)
kleing@43158
   134
  hence "s = t on vars b" "s = t on L c2 X" by auto
kleing@43158
   135
  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
kleing@43158
   136
  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
kleing@43158
   137
    "(bury c2 X, t) \<Rightarrow> t'" "s' = t' on X" by auto
kleing@43158
   138
  thus ?case using `~bval b t` by auto
kleing@43158
   139
next
kleing@43158
   140
  case (WhileFalse b s c)
kleing@43158
   141
  hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
kleing@43158
   142
  thus ?case using WhileFalse(2) by auto
kleing@43158
   143
next
kleing@43158
   144
  case (WhileTrue b s1 c s2 s3 X t1)
kleing@43158
   145
  let ?w = "WHILE b DO c"
kleing@43158
   146
  from `bval b s1` WhileTrue(6) have "bval b t1"
kleing@43158
   147
    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
kleing@43158
   148
  have "s1 = t1 on L c (L ?w X)"
kleing@43158
   149
    using L_While_subset WhileTrue.prems by blast
nipkow@45015
   150
  from WhileTrue.IH(1)[OF this] obtain t2 where
kleing@43158
   151
    "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
nipkow@45015
   152
  from WhileTrue.IH(2)[OF this(2)] obtain t3
kleing@43158
   153
    where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
kleing@43158
   154
    by auto
kleing@43158
   155
  with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
kleing@43158
   156
qed
kleing@43158
   157
kleing@43158
   158
corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
kleing@43158
   159
using bury_sound[of c s s' UNIV]
kleing@43158
   160
by (auto simp: fun_eq_iff[symmetric])
kleing@43158
   161
kleing@43158
   162
text{* Now the opposite direction. *}
kleing@43158
   163
kleing@43158
   164
lemma SKIP_bury[simp]:
kleing@43158
   165
  "SKIP = bury c X \<longleftrightarrow> c = SKIP | (EX x a. c = x::=a & x \<notin> X)"
kleing@43158
   166
by (cases c) auto
kleing@43158
   167
kleing@43158
   168
lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
kleing@43158
   169
by (cases c) auto
kleing@43158
   170
kleing@43158
   171
lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
kleing@43158
   172
  (EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
kleing@43158
   173
by (cases c) auto
kleing@43158
   174
kleing@43158
   175
lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
kleing@43158
   176
  (EX c1 c2. c = IF b THEN c1 ELSE c2 &
kleing@43158
   177
     bc1 = bury c1 X & bc2 = bury c2 X)"
kleing@43158
   178
by (cases c) auto
kleing@43158
   179
kleing@43158
   180
lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow>
kleing@43158
   181
  (EX c'. c = WHILE b DO c' & bc' = bury c' (vars b \<union> X \<union> L c X))"
kleing@43158
   182
by (cases c) auto
kleing@43158
   183
kleing@43158
   184
theorem bury_sound2:
kleing@43158
   185
  "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
kleing@43158
   186
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
nipkow@45015
   187
proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
kleing@43158
   188
  case Skip then show ?case by auto
kleing@43158
   189
next
kleing@43158
   190
  case Assign then show ?case
kleing@43158
   191
    by (auto simp: ball_Un)
kleing@43158
   192
next
kleing@43158
   193
  case (Semi bc1 s1 s2 bc2 s3 c X t1)
kleing@43158
   194
  then obtain c1 c2 where c: "c = c1;c2"
kleing@43158
   195
    and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
nipkow@45015
   196
  note IH = Semi.hyps(2,4)
nipkow@45015
   197
  from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
kleing@43158
   198
    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
nipkow@45015
   199
  from IH(2)[OF bc2 s2t2] obtain t3 where
kleing@43158
   200
    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
kleing@43158
   201
    by auto
kleing@43158
   202
  show ?case using c t12 t23 s3t3 by auto
kleing@43158
   203
next
kleing@43158
   204
  case (IfTrue b s bc1 s' bc2)
kleing@43158
   205
  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
kleing@43158
   206
    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
kleing@43158
   207
  have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
kleing@43158
   208
  from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
nipkow@45015
   209
  note IH = IfTrue.hyps(3)
nipkow@45015
   210
  from IH[OF bc1 `s = t on L c1 X`] obtain t' where
kleing@43158
   211
    "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
kleing@43158
   212
  thus ?case using c `bval b t` by auto
kleing@43158
   213
next
kleing@43158
   214
  case (IfFalse b s bc2 s' bc1)
kleing@43158
   215
  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
kleing@43158
   216
    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
kleing@43158
   217
  have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
kleing@43158
   218
  from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
nipkow@45015
   219
  note IH = IfFalse.hyps(3)
nipkow@45015
   220
  from IH[OF bc2 `s = t on L c2 X`] obtain t' where
kleing@43158
   221
    "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
kleing@43158
   222
  thus ?case using c `~bval b t` by auto
kleing@43158
   223
next
kleing@43158
   224
  case (WhileFalse b s c)
kleing@43158
   225
  hence "~ bval b t" by (auto simp: ball_Un dest: bval_eq_if_eq_on_vars)
kleing@43158
   226
  thus ?case using WhileFalse by auto
kleing@43158
   227
next
kleing@43158
   228
  case (WhileTrue b s1 bc' s2 s3 c X t1)
kleing@43158
   229
  then obtain c' where c: "c = WHILE b DO c'"
kleing@43158
   230
    and bc': "bc' = bury c' (vars b \<union> X \<union> L c' X)" by auto
kleing@43158
   231
  let ?w = "WHILE b DO c'"
kleing@43158
   232
  from `bval b s1` WhileTrue.prems c have "bval b t1"
kleing@43158
   233
    by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
nipkow@45015
   234
  note IH = WhileTrue.hyps(3,5)
kleing@43158
   235
  have "s1 = t1 on L c' (L ?w X)"
kleing@43158
   236
    using L_While_subset WhileTrue.prems c by blast
nipkow@45015
   237
  with IH(1)[OF bc', of t1] obtain t2 where
kleing@43158
   238
    "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
nipkow@45015
   239
  from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
kleing@43158
   240
    where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
kleing@43158
   241
    by auto
kleing@43158
   242
  with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
kleing@43158
   243
qed
kleing@43158
   244
kleing@43158
   245
corollary final_bury_sound2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'"
kleing@43158
   246
using bury_sound2[of c UNIV]
kleing@43158
   247
by (auto simp: fun_eq_iff[symmetric])
kleing@43158
   248
kleing@43158
   249
corollary bury_iff: "(bury c UNIV,s) \<Rightarrow> s' \<longleftrightarrow> (c,s) \<Rightarrow> s'"
kleing@43158
   250
by(metis final_bury_sound final_bury_sound2)
kleing@43158
   251
kleing@43158
   252
end