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


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


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


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


55 
by simp blast


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


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 
(* move to Inductive; call Kleene? *)


127 
lemma lfp_finite_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot"


128 
shows "lfp f = (f^^k) bot"


129 
proof(rule antisym)


130 
show "lfp f \<le> (f^^k) bot"


131 
proof(rule lfp_lowerbound)


132 
show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp


133 
qed


134 
next


135 
show "(f^^k) bot \<le> lfp f"


136 
proof(induction k)


137 
case 0 show ?case by simp


138 
next


139 
case Suc


140 
from monoD[OF assms(1) Suc] lfp_unfold[OF assms(1)]


141 
show ?case by simp


142 
qed


143 
qed


144 


145 
(* move to While_Combinator *)


146 
lemma while_option_stop2:


147 
"while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"


148 
apply(simp add: while_option_def split: if_splits)


149 
by (metis (lam_lifting) LeastI_ex)


150 
(* move to While_Combinator *)


151 
lemma while_option_finite_subset_Some: fixes C :: "'a set"


152 
assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"


153 
shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"


154 
proof(rule measure_while_option_Some[where


155 
f= "%A::'a set. card C  card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])


156 
fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"


157 
show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C  card (f A) < card C  card A"


158 
(is "?L \<and> ?R")


159 
proof


160 
show ?L by(metis A(1) assms(2) monoD[OF `mono f`])


161 
show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)


162 
qed


163 
qed simp


164 
(* move to While_Combinator *)


165 
lemma lfp_eq_while_option:


166 
assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"


167 
shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"


168 
proof


169 
obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"


170 
using while_option_finite_subset_Some[OF assms] by blast


171 
with while_option_stop2[OF this] lfp_finite_iter[OF assms(1)]


172 
show ?thesis by auto


173 
qed


174 


175 
text{* For code generation: *}


176 
lemma L_While: fixes b c X


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


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


179 
proof 


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


181 
have "lfp f = ?r"


182 
proof(rule lfp_eq_while_option[where C = "?V"])


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


184 
next


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


186 
unfolding f_def using L_subset_vars[of c] by blast


187 
next


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


189 
qed


190 
thus ?thesis by (simp add: f_def)


191 
qed


192 


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


194 


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


196 
where


197 
"iter f 0 p d = d" 


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


199 


200 
lemma iter_pfp:


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


202 
apply(induction i arbitrary: x)


203 
apply simp


204 
apply (simp add: mono_def)


205 
done


206 


207 
lemma iter_While_pfp:


208 
fixes b c X W k f


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


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


211 
shows "f P \<subseteq> P"


212 
proof


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


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


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


216 
show ?thesis by(simp add: P_def)


217 
qed


218 


219 
end
