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