Quelle  Live_True.thy   Sprache: Isabelle

(* Author: Tobias Nipkow *)

subsection "True Liveness Analysis"

theory Live_True
imports "HOL-Library.While_Combinator" Vars Big_Step
begin

subsubsection "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\<^sub>1;; c\<^sub>2) X = L c\<^sub>1 (L c\<^sub>2 X)" |
"L (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \ L c\<^sub>1 X \ L c\<^sub>2 X" |
"L (WHILE b DO c) X = lfp(\Y. vars b \ X \ L c Y)"

lemma L_mono: "mono (L c)"
proof-
  have "X \ Y \ L c X \ L c Y" for X 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)"
using L_mono unfolding mono_def by (metis (no_types) 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 ‹L WHILE› equation and reason only with ‹L WHILE› constraints:›
declare L.simps(5)[simp del]


subsubsection "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 subsetD)
  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 subsetD)
  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


subsubsection "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 🍋‹L› executable by replacing 🍋‹lfp› with the 🍋‹while› combinator from theory 🍋‹HOL-Library.While_Combinator›. The 🍋‹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 ‹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


subsubsection "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 🍋‹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\<^sub>1;; c\<^sub>2) X = (Lb c\<^sub>1 \ Lb c\<^sub>2) X" |
"Lb (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \ Lb c\<^sub>1 X \ Lb c\<^sub>2 X" |
"Lb (WHILE b DO c) X = iter (\A. vars b \ X \ Lb c A) 2 {} (vars b \ rvars c \ X)"

text‹🍋‹Lb› (and 🍋‹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