src/HOL/IMP/Live.thy
author nipkow
Thu Nov 20 22:39:12 2008 +0100 (2008-11-20)
changeset 28867 3d9873c4c409
parent 28583 9bb9791bdc18
child 32960 69916a850301
permissions -rw-r--r--
added optimizer
     1 theory Live imports Natural
     2 begin
     3 
     4 text{* Which variables/locations does an expression depend on?
     5 Any set of variables that completely determine the value of the expression,
     6 in the worst case all locations: *}
     7 
     8 consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set"
     9 specification (Dep)
    10 dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> e s = e t"
    11 by(rule_tac x="%x. UNIV" in exI)(simp add: expand_fun_eq[symmetric])
    12 
    13 text{* The following definition of @{const Dep} looks very tempting
    14 @{prop"Dep e = {a. EX s t. (ALL x. x\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"}
    15 but does not work in case @{text e} depends on an infinite set of variables.
    16 For example, if @{term"e s"} tests if @{text s} is 0 at infinitely many locations. Then @{term"Dep e"} incorrectly yields the empty set!
    17 
    18 If we had a concrete representation of expressions, we would simply write
    19 a recursive free-variables function.
    20 *}
    21 
    22 primrec L :: "com \<Rightarrow> loc set \<Rightarrow> loc set" where
    23 "L SKIP A = A" |
    24 "L (x :== e) A = A-{x} \<union> Dep e" |
    25 "L (c1; c2) A = (L c1 \<circ> L c2) A" |
    26 "L (IF b THEN c1 ELSE c2) A = Dep b \<union> L c1 A \<union> L c2 A" |
    27 "L (WHILE b DO c) A = Dep b \<union> A \<union> L c A"
    28 
    29 primrec "kill" :: "com \<Rightarrow> loc set" where
    30 "kill SKIP = {}" |
    31 "kill (x :== e) = {x}" |
    32 "kill (c1; c2) = kill c1 \<union> kill c2" |
    33 "kill (IF b THEN c1 ELSE c2) = Dep b \<union> kill c1 \<inter>  kill c2" |
    34 "kill (WHILE b DO c) = {}"
    35 
    36 primrec gen :: "com \<Rightarrow> loc set" where
    37 "gen SKIP = {}" |
    38 "gen (x :== e) = Dep e" |
    39 "gen (c1; c2) = gen c1 \<union> (gen c2-kill c1)" |
    40 "gen (IF b THEN c1 ELSE c2) = Dep b \<union> gen c1 \<union> gen c2" |
    41 "gen (WHILE b DO c) = Dep b \<union> gen c"
    42 
    43 lemma L_gen_kill: "L c A = gen c \<union> (A - kill c)"
    44 by(induct c arbitrary:A) auto
    45 
    46 lemma L_idemp: "L c (L c A) \<subseteq> L c A"
    47 by(fastsimp simp add:L_gen_kill)
    48 
    49 theorem L_sound: "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
    50  \<forall>x\<in>A. s' x = t' x"
    51 proof (induct c arbitrary: A s t s' t')
    52   case SKIP then show ?case by auto
    53 next
    54   case (Assign x e) then show ?case
    55     by (auto simp:update_def ball_Un dest!: dep_on)
    56 next
    57   case (Semi c1 c2)
    58   from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
    59     by auto
    60   from Semi(5) obtain t'' where t1: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>c2,t''\<rangle> \<longrightarrow>\<^sub>c t'"
    61     by auto
    62   show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
    63 next
    64   case (Cond b c1 c2)
    65   show ?case
    66   proof cases
    67     assume "b s"
    68     hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
    69     have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
    70     hence t: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
    71     show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
    72   next
    73     assume "\<not> b s"
    74     hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
    75     have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
    76     hence t: "\<langle>c2,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
    77     show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
    78   qed
    79 next
    80   case (While b c) note IH = this
    81   { fix cw
    82     have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>cw,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
    83           \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
    84     proof (induct arbitrary: t A pred:evalc)
    85       case WhileFalse
    86       have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
    87       then have "t' = t" using WhileFalse by auto
    88       then show ?case using WhileFalse by auto
    89     next
    90       case (WhileTrue _ s _ s'' s')
    91       have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
    92       have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
    93       then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
    94         using WhileTrue(6,7) by auto
    95       have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
    96 	using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(6,8)
    97 	by (auto simp:L_gen_kill)
    98       moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
    99       ultimately show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
   100     qed auto }
   101   from this[OF IH(3) _ IH(4,2)] show ?case by metis
   102 qed
   103 
   104 
   105 primrec bury :: "com \<Rightarrow> loc set \<Rightarrow> com" where
   106 "bury SKIP _ = SKIP" |
   107 "bury (x :== e) A = (if x:A then x:== e else SKIP)" |
   108 "bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" |
   109 "bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" |
   110 "bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \<union> A \<union> L c A))"
   111 
   112 theorem bury_sound:
   113   "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury c A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
   114    \<forall>x\<in>A. s' x = t' x"
   115 proof (induct c arbitrary: A s t s' t')
   116   case SKIP then show ?case by auto
   117 next
   118   case (Assign x e) then show ?case
   119     by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on)
   120 next
   121   case (Semi c1 c2)
   122   from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
   123     by auto
   124   from Semi(5) obtain t'' where t1: "\<langle>bury c1 (L c2 A),t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>bury c2 A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
   125     by auto
   126   show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
   127 next
   128   case (Cond b c1 c2)
   129   show ?case
   130   proof cases
   131     assume "b s"
   132     hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
   133     have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
   134     hence t: "\<langle>bury c1 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
   135     show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
   136   next
   137     assume "\<not> b s"
   138     hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
   139     have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
   140     hence t: "\<langle>bury c2 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
   141     show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
   142   qed
   143 next
   144   case (While b c) note IH = this
   145   { fix cw
   146     have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>bury cw A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
   147           \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
   148     proof (induct arbitrary: t A pred:evalc)
   149       case WhileFalse
   150       have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
   151       then have "t' = t" using WhileFalse by auto
   152       then show ?case using WhileFalse by auto
   153     next
   154       case (WhileTrue _ s _ s'' s')
   155       have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
   156       have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
   157       then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
   158 	and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
   159         using WhileTrue(6,7) by auto
   160       have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
   161 	using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8)
   162 	by (auto simp:L_gen_kill)
   163       moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
   164       ultimately show ?case
   165 	using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
   166     qed auto }
   167   from this[OF IH(3) _ IH(4,2)] show ?case by metis
   168 qed
   169 
   170 
   171 end