(* Author: Tobias Nipkow *)

theory Live_True

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

begin

subsection "True Liveness Analysis"

fun L :: "com => vname set => vname set" where

"L SKIP X = X" |

"L (x ::= a) X = (if x ∈ X then vars a ∪ (X - {x}) else X)" |

"L (c⇩_{1};; c⇩_{2}) X = L c⇩_{1}(L c⇩_{2}X)" |

"L (IF b THEN c⇩_{1}ELSE c⇩_{2}) X = vars b ∪ L c⇩_{1}X ∪ L c⇩_{2}X" |

"L (WHILE b DO c) X = lfp(λY. vars b ∪ X ∪ L c Y)"

lemma L_mono: "mono (L c)"

proof-

{ fix X Y have "X ⊆ Y ==> L c X ⊆ L c Y"

proof(induction c arbitrary: X Y)

case (While b c)

show ?case

proof(simp, rule lfp_mono)

fix Z show "vars b ∪ X ∪ L c Z ⊆ vars b ∪ Y ∪ L c Z"

using While by auto

qed

next

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

qed auto

} thus ?thesis by(rule monoI)

qed

lemma mono_union_L:

"mono (λY. X ∪ L c Y)"

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

lemma L_While_unfold:

"L (WHILE b DO c) X = vars b ∪ X ∪ L c (L (WHILE b DO c) X)"

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

lemma L_While_pfp: "L c (L (WHILE b DO c) X) ⊆ L (WHILE b DO c) X"

using L_While_unfold by blast

lemma L_While_vars: "vars b ⊆ L (WHILE b DO c) X"

using L_While_unfold by blast

lemma L_While_X: "X ⊆ L (WHILE b DO c) X"

using L_While_unfold by blast

text{* Disable @{text "L WHILE"} equation and reason only with @{text "L WHILE"} constraints: *}

declare L.simps(5)[simp del]

subsection "Correctness"

theorem L_correct:

"(c,s) => s' ==> s = t on L c X ==>

∃ t'. (c,t) => t' & s' = t' on X"

proof (induction arbitrary: X t rule: big_step_induct)

case Skip then show ?case by auto

next

case Assign then show ?case

by (auto simp: ball_Un)

next

case (Seq c1 s1 s2 c2 s3 X t1)

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

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

by simp blast

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

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

by auto

show ?case using t12 t23 s3t3 by auto

next

case (IfTrue b s c1 s' c2)

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

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

from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where

"(c1, t) => t'" "s' = t' on X" by auto

thus ?case using `bval b t` by auto

next

case (IfFalse b s c2 s' c1)

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

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

from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where

"(c2, t) => t'" "s' = t' on X" by auto

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

next

case (WhileFalse b s c)

hence "~ bval b t"

by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)

thus ?case using WhileFalse.prems L_While_X[of X b c] by auto

next

case (WhileTrue b s1 c s2 s3 X t1)

let ?w = "WHILE b DO c"

from `bval b s1` WhileTrue.prems have "bval b t1"

by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)

have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems

by (blast)

from WhileTrue.IH(1)[OF this] obtain t2 where

"(c, t1) => t2" "s2 = t2 on L ?w X" by auto

from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) => t3" "s3 = t3 on X"

by auto

with `bval b t1` `(c, t1) => t2` show ?case by auto

qed

subsection "Executability"

lemma L_subset_vars: "L c X ⊆ rvars c ∪ X"

proof(induction c arbitrary: X)

case (While b c)

have "lfp(λY. vars b ∪ X ∪ L c Y) ⊆ vars b ∪ rvars c ∪ X"

using While.IH[of "vars b ∪ rvars c ∪ X"]

by (auto intro!: lfp_lowerbound)

thus ?case by (simp add: L.simps(5))

qed auto

text{* Make @{const L} executable by replacing @{const lfp} with the @{const

while} combinator from theory @{theory While_Combinator}. The @{const while}

combinator obeys the recursion equation

@{thm[display] While_Combinator.while_unfold[no_vars]}

and is thus executable. *}

lemma L_While: fixes b c X

assumes "finite X" defines "f == λY. vars b ∪ X ∪ L c Y"

shows "L (WHILE b DO c) X = while (λY. f Y ≠ Y) f {}" (is "_ = ?r")

proof -

let ?V = "vars b ∪ rvars c ∪ X"

have "lfp f = ?r"

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

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

next

fix Y show "Y ⊆ ?V ==> f Y ⊆ ?V"

unfolding f_def using L_subset_vars[of c] by blast

next

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

qed

thus ?thesis by (simp add: f_def L.simps(5))

qed

lemma L_While_let: "finite X ==> L (WHILE b DO c) X =

(let f = (λY. vars b ∪ X ∪ L c Y)

in while (λY. f Y ≠ Y) f {})"

by(simp add: L_While)

lemma L_While_set: "L (WHILE b DO c) (set xs) =

(let f = (λY. vars b ∪ set xs ∪ L c Y)

in while (λY. f Y ≠ Y) f {})"

by(rule L_While_let, simp)

text{* Replace the equation for @{text "L (WHILE …)"} by the executable @{thm[source] L_While_set}: *}

lemmas [code] = L.simps(1-4) L_While_set

text{* Sorry, this syntax is odd. *}

text{* A test: *}

lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x'';; ''x'' ::= V ''z''

in L (WHILE b DO c) {''y''}) = {''x'', ''y'', ''z''}"

by eval

subsection "Limiting the number of iterations"

text{* The final parameter is the default value: *}

fun iter :: "('a => 'a) => nat => 'a => 'a => 'a" where

"iter f 0 p d = d" |

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

text{* A version of @{const L} with a bounded number of iterations (here: 2)

in the WHILE case: *}

fun Lb :: "com => vname set => vname set" where

"Lb SKIP X = X" |

"Lb (x ::= a) X = (if x ∈ X then X - {x} ∪ vars a else X)" |

"Lb (c⇩_{1};; c⇩_{2}) X = (Lb c⇩_{1}o Lb c⇩_{2}) X" |

"Lb (IF b THEN c⇩_{1}ELSE c⇩_{2}) X = vars b ∪ Lb c⇩_{1}X ∪ Lb c⇩_{2}X" |

"Lb (WHILE b DO c) X = iter (λA. vars b ∪ X ∪ Lb c A) 2 {} (vars b ∪ rvars c ∪ X)"

text{* @{const Lb} (and @{const iter}) is not monotone! *}

lemma "let w = WHILE Bc False DO (''x'' ::= V ''y'';; ''z'' ::= V ''x'')

in ¬ (Lb w {''z''} ⊆ Lb w {''y'',''z''})"

by eval

lemma lfp_subset_iter:

"[| mono f; !!X. f X ⊆ f' X; lfp f ⊆ D |] ==> lfp f ⊆ iter f' n A D"

proof(induction n arbitrary: A)

case 0 thus ?case by simp

next

case Suc thus ?case by simp (metis lfp_lowerbound)

qed

lemma "L c X ⊆ Lb c X"

proof(induction c arbitrary: X)

case (While b c)

let ?f = "λA. vars b ∪ X ∪ L c A"

let ?fb = "λA. vars b ∪ X ∪ Lb c A"

show ?case

proof (simp add: L.simps(5), rule lfp_subset_iter[OF mono_union_L])

show "!!X. ?f X ⊆ ?fb X" using While.IH by blast

show "lfp ?f ⊆ vars b ∪ rvars c ∪ X"

by (metis (full_types) L.simps(5) L_subset_vars rvars.simps(5))

qed

next

case Seq thus ?case by simp (metis (full_types) L_mono monoD subset_trans)

qed auto

end