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