45812

1 
(* Author: Tobias Nipkow *)


2 


3 
theory Live_True


4 
imports "~~/src/HOL/Library/While_Combinator" Vars Big_Step


5 
begin


6 


7 
subsection "True Liveness Analysis"


8 


9 
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where


10 
"L SKIP X = X" 


11 
"L (x ::= a) X = (if x:X then X{x} \<union> vars a else X)" 


12 
"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" 


13 
"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" 


14 
"L (WHILE b DO c) X = lfp(%Y. vars b \<union> X \<union> L c Y)"


15 


16 
lemma L_mono: "mono (L c)"


17 
proof


18 
{ fix X Y have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y"


19 
proof(induction c arbitrary: X Y)


20 
case (While b c)


21 
show ?case


22 
proof(simp, rule lfp_mono)


23 
fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z"


24 
using While by auto


25 
qed


26 
next


27 
case If thus ?case by(auto simp: subset_iff)


28 
qed auto


29 
} thus ?thesis by(rule monoI)


30 
qed


31 


32 
lemma mono_union_L:


33 
"mono (%Y. X \<union> L c Y)"


34 
by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono)


35 


36 
lemma L_While_unfold:


37 
"L (WHILE b DO c) X = vars b \<union> X \<union> L c (L (WHILE b DO c) X)"


38 
by(metis lfp_unfold[OF mono_union_L] L.simps(5))


39 


40 


41 
subsection "Soundness"


42 


43 
theorem L_sound:


44 
"(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow>


45 
\<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"


46 
proof (induction arbitrary: X t rule: big_step_induct)


47 
case Skip then show ?case by auto


48 
next


49 
case Assign then show ?case


50 
by (auto simp: ball_Un)


51 
next

47818

52 
case (Seq c1 s1 s2 c2 s3 X t1)


53 
from Seq.IH(1) Seq.prems obtain t2 where

45812

54 
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"


55 
by simp blast

47818

56 
from Seq.IH(2)[OF s2t2] obtain t3 where

45812

57 
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"


58 
by auto


59 
show ?case using t12 t23 s3t3 by auto


60 
next


61 
case (IfTrue b s c1 s' c2)


62 
hence "s = t on vars b" "s = t on L c1 X" by auto


63 
from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp


64 
from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where


65 
"(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto


66 
thus ?case using `bval b t` by auto


67 
next


68 
case (IfFalse b s c2 s' c1)


69 
hence "s = t on vars b" "s = t on L c2 X" by auto


70 
from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp


71 
from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where


72 
"(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto


73 
thus ?case using `~bval b t` by auto


74 
next


75 
case (WhileFalse b s c)


76 
hence "~ bval b t"


77 
by (metis L_While_unfold UnI1 bval_eq_if_eq_on_vars)


78 
thus ?case using WhileFalse.prems L_While_unfold[of b c X] 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.prems have "bval b t1"


83 
by (metis L_While_unfold UnI1 bval_eq_if_eq_on_vars)


84 
have "s1 = t1 on L c (L ?w X)" using L_While_unfold 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 
instantiation com :: vars


95 
begin


96 


97 
fun vars_com :: "com \<Rightarrow> vname set" where


98 
"vars SKIP = {}" 


99 
"vars (x::=e) = vars e" 


100 
"vars (c\<^isub>1; c\<^isub>2) = vars c\<^isub>1 \<union> vars c\<^isub>2" 


101 
"vars (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> vars c\<^isub>1 \<union> vars c\<^isub>2" 


102 
"vars (WHILE b DO c) = vars b \<union> vars c"


103 


104 
instance ..


105 


106 
end


107 


108 
lemma L_subset_vars: "L c X \<subseteq> vars c \<union> X"


109 
proof(induction c arbitrary: X)


110 
case (While b c)


111 
have "lfp(%Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> vars c \<union> X"


112 
using While.IH[of "vars b \<union> vars c \<union> X"]


113 
by (auto intro!: lfp_lowerbound)


114 
thus ?case by simp


115 
qed auto


116 


117 
lemma afinite[simp]: "finite(vars(a::aexp))"


118 
by (induction a) auto


119 


120 
lemma bfinite[simp]: "finite(vars(b::bexp))"


121 
by (induction b) auto


122 


123 
lemma cfinite[simp]: "finite(vars(c::com))"


124 
by (induction c) auto


125 


126 
text{* For code generation: *}


127 
lemma L_While: fixes b c X


128 
assumes "finite X" defines "f == \<lambda>A. vars b \<union> X \<union> L c A"


129 
shows "L (WHILE b DO c) X = the(while_option (\<lambda>A. f A \<noteq> A) f {})" (is "_ = ?r")


130 
proof 


131 
let ?V = "vars b \<union> vars c \<union> X"


132 
have "lfp f = ?r"

48256

133 
proof(rule lfp_the_while_option[where C = "?V"])

45812

134 
show "mono f" by(simp add: f_def mono_union_L)


135 
next


136 
fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V"


137 
unfolding f_def using L_subset_vars[of c] by blast


138 
next


139 
show "finite ?V" using `finite X` by simp


140 
qed


141 
thus ?thesis by (simp add: f_def)


142 
qed


143 


144 
text{* An approximate computation of the WHILEcase: *}


145 


146 
fun iter :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"


147 
where


148 
"iter f 0 p d = d" 


149 
"iter f (Suc n) p d = (if f p = p then p else iter f n (f p) d)"


150 


151 
lemma iter_pfp:


152 
"f d \<le> d \<Longrightarrow> mono f \<Longrightarrow> x \<le> f x \<Longrightarrow> f(iter f i x d) \<le> iter f i x d"


153 
apply(induction i arbitrary: x)


154 
apply simp


155 
apply (simp add: mono_def)


156 
done


157 


158 
lemma iter_While_pfp:


159 
fixes b c X W k f


160 
defines "f == \<lambda>A. vars b \<union> X \<union> L c A" and "W == vars b \<union> vars c \<union> X"


161 
and "P == iter f k {} W"


162 
shows "f P \<subseteq> P"


163 
proof


164 
have "f W \<subseteq> W" unfolding f_def W_def using L_subset_vars[of c] by blast


165 
have "mono f" by(simp add: f_def mono_union_L)


166 
from iter_pfp[of f, OF `f W \<subseteq> W` `mono f` empty_subsetI]


167 
show ?thesis by(simp add: P_def)


168 
qed


169 


170 
end
