src/HOL/IMP/Live.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58889 5b7a9633cfa8
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
wenzelm@58889
     3
section "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
nipkow@51425
    11
"L SKIP X = X" |
nipkow@51448
    12
"L (x ::= a) X = vars a \<union> (X - {x})" |
wenzelm@53015
    13
"L (c\<^sub>1;; c\<^sub>2) X = L c\<^sub>1 (L c\<^sub>2 X)" |
wenzelm@53015
    14
"L (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \<union> L c\<^sub>1 X \<union> L c\<^sub>2 X" |
nipkow@51425
    15
"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
kleing@43158
    16
nipkow@52046
    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}" |
wenzelm@53015
    24
"kill (c\<^sub>1;; c\<^sub>2) = kill c\<^sub>1 \<union> kill c\<^sub>2" |
wenzelm@53015
    25
"kill (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = kill c\<^sub>1 \<inter> kill c\<^sub>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" |
wenzelm@53015
    31
"gen (c\<^sub>1;; c\<^sub>2) = gen c\<^sub>1 \<union> (gen c\<^sub>2 - kill c\<^sub>1)" |
wenzelm@53015
    32
"gen (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = vars b \<union> gen c\<^sub>1 \<union> gen c\<^sub>2" |
kleing@43158
    33
"gen (WHILE b DO c) = vars b \<union> gen c"
kleing@43158
    34
nipkow@51433
    35
lemma L_gen_kill: "L c X = gen c \<union> (X - kill c)"
kleing@43158
    36
by(induct c arbitrary:X) auto
kleing@43158
    37
nipkow@45771
    38
lemma L_While_pfp: "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
nipkow@45771
    41
lemma L_While_lpfp:
nipkow@45784
    42
  "vars b \<union> X \<union> L c P \<subseteq> P \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
nipkow@45771
    43
by(simp add: L_gen_kill)
nipkow@45771
    44
nipkow@51468
    45
lemma L_While_vars: "vars b \<subseteq> L (WHILE b DO c) X"
nipkow@51468
    46
by auto
nipkow@51468
    47
nipkow@51468
    48
lemma L_While_X: "X \<subseteq> L (WHILE b DO c) X"
nipkow@51468
    49
by auto
nipkow@51468
    50
nipkow@51468
    51
text{* Disable L WHILE equation and reason only with L WHILE constraints *}
nipkow@51468
    52
declare L.simps(5)[simp del]
kleing@43158
    53
nipkow@51975
    54
subsection "Correctness"
kleing@43158
    55
nipkow@51975
    56
theorem L_correct:
kleing@43158
    57
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
kleing@43158
    58
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
nipkow@45015
    59
proof (induction arbitrary: X t rule: big_step_induct)
kleing@43158
    60
  case Skip then show ?case by auto
kleing@43158
    61
next
kleing@43158
    62
  case Assign then show ?case
kleing@43158
    63
    by (auto simp: ball_Un)
kleing@43158
    64
next
nipkow@47818
    65
  case (Seq c1 s1 s2 c2 s3 X t1)
nipkow@47818
    66
  from Seq.IH(1) Seq.prems obtain t2 where
kleing@43158
    67
    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
kleing@43158
    68
    by simp blast
nipkow@47818
    69
  from Seq.IH(2)[OF s2t2] obtain t3 where
kleing@43158
    70
    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
kleing@43158
    71
    by auto
kleing@43158
    72
  show ?case using t12 t23 s3t3 by auto
kleing@43158
    73
next
kleing@43158
    74
  case (IfTrue b s c1 s' c2)
kleing@43158
    75
  hence "s = t on vars b" "s = t on L c1 X" by auto
kleing@43158
    76
  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
nipkow@50009
    77
  from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where
kleing@43158
    78
    "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
kleing@43158
    79
  thus ?case using `bval b t` by auto
kleing@43158
    80
next
kleing@43158
    81
  case (IfFalse b s c2 s' c1)
kleing@43158
    82
  hence "s = t on vars b" "s = t on L c2 X" by auto
kleing@43158
    83
  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
nipkow@50009
    84
  from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where
kleing@43158
    85
    "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
kleing@43158
    86
  thus ?case using `~bval b t` by auto
kleing@43158
    87
next
kleing@43158
    88
  case (WhileFalse b s c)
nipkow@51468
    89
  hence "~ bval b t"
nipkow@51468
    90
    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
nipkow@51468
    91
  thus ?case by(metis WhileFalse.prems L_While_X big_step.WhileFalse set_mp)
kleing@43158
    92
next
kleing@43158
    93
  case (WhileTrue b s1 c s2 s3 X t1)
kleing@43158
    94
  let ?w = "WHILE b DO c"
nipkow@45770
    95
  from `bval b s1` WhileTrue.prems have "bval b t1"
nipkow@51468
    96
    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
nipkow@51468
    97
  have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems
kleing@43158
    98
    by (blast)
nipkow@45015
    99
  from WhileTrue.IH(1)[OF this] obtain t2 where
kleing@43158
   100
    "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
nipkow@45015
   101
  from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
kleing@43158
   102
    by auto
kleing@43158
   103
  with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
kleing@43158
   104
qed
kleing@43158
   105
kleing@43158
   106
kleing@43158
   107
subsection "Program Optimization"
kleing@43158
   108
kleing@43158
   109
text{* Burying assignments to dead variables: *}
nipkow@45212
   110
fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
kleing@43158
   111
"bury SKIP X = SKIP" |
nipkow@50009
   112
"bury (x ::= a) X = (if x \<in> X then x ::= a else SKIP)" |
wenzelm@53015
   113
"bury (c\<^sub>1;; c\<^sub>2) X = (bury c\<^sub>1 (L c\<^sub>2 X);; bury c\<^sub>2 X)" |
wenzelm@53015
   114
"bury (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = IF b THEN bury c\<^sub>1 X ELSE bury c\<^sub>2 X" |
nipkow@51468
   115
"bury (WHILE b DO c) X = WHILE b DO bury c (L (WHILE b DO c) X)"
kleing@43158
   116
nipkow@51975
   117
text{* We could prove the analogous lemma to @{thm[source]L_correct}, and the
kleing@43158
   118
proof would be very similar. However, we phrase it as a semantics
kleing@43158
   119
preservation property: *}
kleing@43158
   120
nipkow@51975
   121
theorem bury_correct:
kleing@43158
   122
  "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
kleing@43158
   123
  \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
nipkow@45015
   124
proof (induction arbitrary: X t rule: big_step_induct)
kleing@43158
   125
  case Skip then show ?case by auto
kleing@43158
   126
next
kleing@43158
   127
  case Assign then show ?case
kleing@43158
   128
    by (auto simp: ball_Un)
kleing@43158
   129
next
nipkow@47818
   130
  case (Seq c1 s1 s2 c2 s3 X t1)
nipkow@47818
   131
  from Seq.IH(1) Seq.prems obtain t2 where
kleing@43158
   132
    t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
kleing@43158
   133
    by simp blast
nipkow@47818
   134
  from Seq.IH(2)[OF s2t2] obtain t3 where
kleing@43158
   135
    t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
kleing@43158
   136
    by auto
kleing@43158
   137
  show ?case using t12 t23 s3t3 by auto
kleing@43158
   138
next
kleing@43158
   139
  case (IfTrue b s c1 s' c2)
kleing@43158
   140
  hence "s = t on vars b" "s = t on L c1 X" by auto
kleing@43158
   141
  from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
nipkow@50009
   142
  from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where
kleing@43158
   143
    "(bury c1 X, t) \<Rightarrow> t'" "s' =t' on X" by auto
kleing@43158
   144
  thus ?case using `bval b t` by auto
kleing@43158
   145
next
kleing@43158
   146
  case (IfFalse b s c2 s' c1)
kleing@43158
   147
  hence "s = t on vars b" "s = t on L c2 X" by auto
kleing@43158
   148
  from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
nipkow@50009
   149
  from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where
kleing@43158
   150
    "(bury c2 X, t) \<Rightarrow> t'" "s' = t' on X" by auto
kleing@43158
   151
  thus ?case using `~bval b t` by auto
kleing@43158
   152
next
kleing@43158
   153
  case (WhileFalse b s c)
nipkow@51468
   154
  hence "~ bval b t" by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
nipkow@51468
   155
  thus ?case
nipkow@51468
   156
    by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse set_mp)
kleing@43158
   157
next
kleing@43158
   158
  case (WhileTrue b s1 c s2 s3 X t1)
kleing@43158
   159
  let ?w = "WHILE b DO c"
nipkow@45770
   160
  from `bval b s1` WhileTrue.prems have "bval b t1"
nipkow@51468
   161
    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
kleing@43158
   162
  have "s1 = t1 on L c (L ?w X)"
nipkow@45771
   163
    using L_While_pfp WhileTrue.prems by blast
nipkow@45015
   164
  from WhileTrue.IH(1)[OF this] obtain t2 where
kleing@43158
   165
    "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
nipkow@45015
   166
  from WhileTrue.IH(2)[OF this(2)] obtain t3
kleing@43158
   167
    where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
kleing@43158
   168
    by auto
kleing@43158
   169
  with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
kleing@43158
   170
qed
kleing@43158
   171
nipkow@51975
   172
corollary final_bury_correct: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
nipkow@51975
   173
using bury_correct[of c s s' UNIV]
kleing@43158
   174
by (auto simp: fun_eq_iff[symmetric])
kleing@43158
   175
kleing@43158
   176
text{* Now the opposite direction. *}
kleing@43158
   177
kleing@43158
   178
lemma SKIP_bury[simp]:
kleing@43158
   179
  "SKIP = bury c X \<longleftrightarrow> c = SKIP | (EX x a. c = x::=a & x \<notin> X)"
kleing@43158
   180
by (cases c) auto
kleing@43158
   181
kleing@43158
   182
lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
kleing@43158
   183
by (cases c) auto
kleing@43158
   184
wenzelm@53015
   185
lemma Seq_bury[simp]: "bc\<^sub>1;;bc\<^sub>2 = bury c X \<longleftrightarrow>
wenzelm@53015
   186
  (EX c\<^sub>1 c\<^sub>2. c = c\<^sub>1;;c\<^sub>2 & bc\<^sub>2 = bury c\<^sub>2 X & bc\<^sub>1 = bury c\<^sub>1 (L c\<^sub>2 X))"
kleing@43158
   187
by (cases c) auto
kleing@43158
   188
kleing@43158
   189
lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
kleing@43158
   190
  (EX c1 c2. c = IF b THEN c1 ELSE c2 &
kleing@43158
   191
     bc1 = bury c1 X & bc2 = bury c2 X)"
kleing@43158
   192
by (cases c) auto
kleing@43158
   193
kleing@43158
   194
lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow>
nipkow@51468
   195
  (EX c'. c = WHILE b DO c' & bc' = bury c' (L (WHILE b DO c') X))"
kleing@43158
   196
by (cases c) auto
kleing@43158
   197
nipkow@51975
   198
theorem bury_correct2:
kleing@43158
   199
  "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
kleing@43158
   200
  \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
nipkow@45015
   201
proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
kleing@43158
   202
  case Skip then show ?case by auto
kleing@43158
   203
next
kleing@43158
   204
  case Assign then show ?case
kleing@43158
   205
    by (auto simp: ball_Un)
kleing@43158
   206
next
nipkow@47818
   207
  case (Seq bc1 s1 s2 bc2 s3 c X t1)
nipkow@52046
   208
  then obtain c1 c2 where c: "c = c1;;c2"
kleing@43158
   209
    and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
nipkow@47818
   210
  note IH = Seq.hyps(2,4)
nipkow@47818
   211
  from IH(1)[OF bc1, of t1] Seq.prems c obtain t2 where
kleing@43158
   212
    t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
nipkow@45015
   213
  from IH(2)[OF bc2 s2t2] obtain t3 where
kleing@43158
   214
    t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
kleing@43158
   215
    by auto
kleing@43158
   216
  show ?case using c t12 t23 s3t3 by auto
kleing@43158
   217
next
kleing@43158
   218
  case (IfTrue b s bc1 s' bc2)
kleing@43158
   219
  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
kleing@43158
   220
    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
kleing@43158
   221
  have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
kleing@43158
   222
  from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
nipkow@45015
   223
  note IH = IfTrue.hyps(3)
nipkow@45015
   224
  from IH[OF bc1 `s = t on L c1 X`] obtain t' where
kleing@43158
   225
    "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
kleing@43158
   226
  thus ?case using c `bval b t` by auto
kleing@43158
   227
next
kleing@43158
   228
  case (IfFalse b s bc2 s' bc1)
kleing@43158
   229
  then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
kleing@43158
   230
    and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
kleing@43158
   231
  have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
kleing@43158
   232
  from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
nipkow@45015
   233
  note IH = IfFalse.hyps(3)
nipkow@45015
   234
  from IH[OF bc2 `s = t on L c2 X`] obtain t' where
kleing@43158
   235
    "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
kleing@43158
   236
  thus ?case using c `~bval b t` by auto
kleing@43158
   237
next
kleing@43158
   238
  case (WhileFalse b s c)
nipkow@51468
   239
  hence "~ bval b t"
nipkow@51468
   240
    by auto (metis L_While_vars bval_eq_if_eq_on_vars set_rev_mp)
nipkow@51468
   241
  thus ?case using WhileFalse
nipkow@51468
   242
    by auto (metis L_While_X big_step.WhileFalse set_mp)
kleing@43158
   243
next
nipkow@51468
   244
  case (WhileTrue b s1 bc' s2 s3 w X t1)
nipkow@51468
   245
  then obtain c' where w: "w = WHILE b DO c'"
nipkow@51468
   246
    and bc': "bc' = bury c' (L (WHILE b DO c') X)" by auto
nipkow@51468
   247
  from `bval b s1` WhileTrue.prems w have "bval b t1"
nipkow@51468
   248
    by auto (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
nipkow@45015
   249
  note IH = WhileTrue.hyps(3,5)
nipkow@51468
   250
  have "s1 = t1 on L c' (L w X)"
nipkow@51468
   251
    using L_While_pfp WhileTrue.prems w by blast
nipkow@51468
   252
  with IH(1)[OF bc', of t1] w obtain t2 where
nipkow@51468
   253
    "(c', t1) \<Rightarrow> t2" "s2 = t2 on L w X" by auto
nipkow@51468
   254
  from IH(2)[OF WhileTrue.hyps(6), of t2] w this(2) obtain t3
nipkow@51468
   255
    where "(w,t2) \<Rightarrow> t3" "s3 = t3 on X"
kleing@43158
   256
    by auto
nipkow@51468
   257
  with `bval b t1` `(c', t1) \<Rightarrow> t2` w show ?case by auto
kleing@43158
   258
qed
kleing@43158
   259
nipkow@51975
   260
corollary final_bury_correct2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'"
nipkow@51975
   261
using bury_correct2[of c UNIV]
kleing@43158
   262
by (auto simp: fun_eq_iff[symmetric])
kleing@43158
   263
nipkow@51433
   264
corollary bury_sim: "bury c UNIV \<sim> c"
nipkow@51975
   265
by(metis final_bury_correct final_bury_correct2)
kleing@43158
   266
kleing@43158
   267
end