1.1 --- a/src/HOL/IMP/Live.thy	Thu Nov 20 19:43:34 2008 +0100
     1.2 +++ b/src/HOL/IMP/Live.thy	Thu Nov 20 22:39:12 2008 +0100
     1.3 @@ -92,17 +92,80 @@
     1.4        have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
     1.5        then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
     1.6          using WhileTrue(6,7) by auto
     1.7 -      note IH1 = IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`]
     1.8 -      have L1: "\<forall>x\<in>A. s'' x = t'' x" using IH1 WhileTrue(6,8)
     1.9 -	by(simp  add: ball_Un) (metis)
    1.10 -      have L2: "\<forall>x\<in>Dep b. s'' x = t'' x"
    1.11 -	using IH1 WhileTrue(6,8) by (auto simp:L_gen_kill)
    1.12 -      have L3: "\<forall>x\<in>L c A. s'' x = t'' x"
    1.13 -	using IH1 L_idemp[of c A] WhileTrue(6,8) by auto
    1.14 -      have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" using L1 L2 L3 by auto
    1.15 -      then show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
    1.16 +      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
    1.17 +	using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(6,8)
    1.18 +	by (auto simp:L_gen_kill)
    1.19 +      moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
    1.20 +      ultimately show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
    1.21      qed auto }
    1.22    from this[OF IH(3) _ IH(4,2)] show ?case by metis
    1.23  qed
    1.24  
    1.25 +
    1.26 +primrec bury :: "com \<Rightarrow> loc set \<Rightarrow> com" where
    1.27 +"bury SKIP _ = SKIP" |
    1.28 +"bury (x :== e) A = (if x:A then x:== e else SKIP)" |
    1.29 +"bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" |
    1.30 +"bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" |
    1.31 +"bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \<union> A \<union> L c A))"
    1.32 +
    1.33 +theorem bury_sound:
    1.34 +  "\<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>
    1.35 +   \<forall>x\<in>A. s' x = t' x"
    1.36 +proof (induct c arbitrary: A s t s' t')
    1.37 +  case SKIP then show ?case by auto
    1.38 +next
    1.39 +  case (Assign x e) then show ?case
    1.40 +    by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on)
    1.41 +next
    1.42 +  case (Semi c1 c2)
    1.43 +  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'"
    1.44 +    by auto
    1.45 +  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'"
    1.46 +    by auto
    1.47 +  show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
    1.48 +next
    1.49 +  case (Cond b c1 c2)
    1.50 +  show ?case
    1.51 +  proof cases
    1.52 +    assume "b s"
    1.53 +    hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
    1.54 +    have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
    1.55 +    hence t: "\<langle>bury c1 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
    1.56 +    show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
    1.57 +  next
    1.58 +    assume "\<not> b s"
    1.59 +    hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
    1.60 +    have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
    1.61 +    hence t: "\<langle>bury c2 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
    1.62 +    show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
    1.63 +  qed
    1.64 +next
    1.65 +  case (While b c) note IH = this
    1.66 +  { fix cw
    1.67 +    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>
    1.68 +          \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
    1.69 +    proof (induct arbitrary: t A pred:evalc)
    1.70 +      case WhileFalse
    1.71 +      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
    1.72 +      then have "t' = t" using WhileFalse by auto
    1.73 +      then show ?case using WhileFalse by auto
    1.74 +    next
    1.75 +      case (WhileTrue _ s _ s'' s')
    1.76 +      have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
    1.77 +      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
    1.78 +      then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
    1.79 +	and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
    1.80 +        using WhileTrue(6,7) by auto
    1.81 +      have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
    1.82 +	using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8)
    1.83 +	by (auto simp:L_gen_kill)
    1.84 +      moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
    1.85 +      ultimately show ?case
    1.86 +	using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
    1.87 +    qed auto }
    1.88 +  from this[OF IH(3) _ IH(4,2)] show ?case by metis
    1.89 +qed
    1.90 +
    1.91 +
    1.92  end
    1.93 \ No newline at end of file