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--
modernized header uniformly as section;
     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