Quelle  Termination.thy

(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* Authors: David Cock - David.Cock@nicta.com.au, Thomas Sewell - Thomas.Sewell@nicta.com.au *)

section "Loop Termination"
 
theory Termination imports Embedding StructuredReasoning Loops begin

text_raw ‹\label{s:termination}›

text ‹Termination for loops can be shown by classical means (using a variant, or a measure
 ), or by probabilistic means: We only need that the loop terminates \emph{with probability
 }.›

subsection ‹Trivial Termination›

text ‹A maximal transformer (program) doesn't affect termination. This is
 essentially saying that such a program doesn't abort (or diverge).›
lemma maximal_Seq_term:
  fixes r::"'s prog" and s::"'s prog"
  assumes mr: "maximal (wp r)"
      and ws: "well_def s"
      and ts: "(λs. 1) ⊨!!! wp s (λs. 1)"
  shows "(λs. 1) ⊨!!! wp (r ;; s) (λs. 1)"
proof -
  note hs = well_def_wp_healthy[OF ws]
  have "wp s (λs. 1) = (λs. 1)"
  proof(rule antisym)
    show "(λs. 1) ⊨!!! wp s (λs. 1)" by(rule ts)
    have "bounded_by 1 (wp s (λs. 1))"
      by(auto intro!:healthy_bounded_byD[OF hs])
    thus "wp s (λs. 1) ⊨!!! (λs. 1)" by(auto intro!:le_funI)
  qed
  with mr show ?thesis
    by(simp add:wp_eval embed_bool_def maximalD)
qed

text ‹From any state where the guard does not hold, a loop terminates
 in a single step.›
lemma term_onestep:
  assumes wb: "well_def body"
  shows "«N G¬ ⊨!!! wp do G ⟶ body od (λs. 1)"
proof(rule le_funI)
  note hb = well_def_wp_healthy[OF wb]
  fix s
  show "«N G¬ s ≤ wp do G ⟶ body od (λs. 1) s"
  proof(cases "G s", simp_all add:wp_loop_nguard hb)
    from hb have "sound (wp do G ⟶ body od (λs. 1))"
      by(auto intro:healthy_sound[OF healthy_wp_loop])
    thus "0 ≤ wp do G ⟶ body od (λs. 1) s" by(auto)
  qed
qed

subsection ‹Classical Termination›

text ‹The first non-trivial termination result is quite standard: If we can provide a
 -number-valued measure, that decreases on every iteration, and implies termination on
  zero, the loop terminates.›

lemma loop_term_nat_measure_noinv:
  fixes m :: "'s ==> nat" and body :: "'s prog"
  assumes wb: "well_def body"
  and guard: "∧s. m s = 0 ⟶ ¬ G s"
  and variant: "∧n. «λs. m s = Suc n¬ ⊨!!! wp body «λs. m s = n¬"
  shows "λs. 1 ⊨!!! wp do G ⟶ body od (λs. 1)"
proof -
  note hb = well_def_wp_healthy[OF wb]
  have "∧n. (∀s. m s = n ⟶ 1 ≤ wp do G ⟶ body od (λs. 1) s)"
  proof(induct_tac n)
    fix n
    show "∀s. m s = 0 ⟶ 1 ≤ wp do G ⟶ body od (λs. 1) s"
    proof(clarify)
      fix s
      assume "m s = 0"
      with guard have "¬ G s" by(blast)
      with hb show "1 ≤ wp do G ⟶ body od (λs. 1) s"
        by(simp add:wp_loop_nguard)
    qed
    assume IH: "∀s. m s = n ⟶ 1 ≤ wp do G ⟶ body od (λs. 1) s"
    hence IH': "∀s. m s = n ⟶ 1 ≤ wp do G ⟶ body od «λs. True¬ s"
      by(simp add:embed_bool_def)
    have "∀s. m s = Suc n ⟶ 1 ≤ wp do G ⟶ body od «λs. True¬ s"
    proof(intro fold_premise healthy_intros hb, rule le_funI)
      fix s
      show "«λs. m s = Suc n¬ s ≤ wp do G ⟶ body od «λs. True¬ s"
      proof(cases "G s")
        case False
        hence "1 = «N G¬ s" by(auto)
        also from wb have "... ≤ wp do G ⟶ body od (λs. 1) s"
          by(rule le_funD[OF term_onestep])
        finally show ?thesis by(simp add:embed_bool_def)
      next
        case True note G = this
        from IH' have "«λs. m s = n¬ ⊨!!! wp do G ⟶ body od «λs. True¬"
          by(blast intro:use_premise healthy_intros hb)
        with variant wb
        have "«λs. m s = Suc n¬ ⊨!!! wp (body ;; do G ⟶ body od) «λs. True¬"
          by(blast intro:wp_Seq wd_intros)
        hence "«λs. m s = Suc n¬ s ≤ wp (body ;; do G ⟶ body od) «λs. True¬ s"
          by(auto)
        also from hb G have "... = wp do G ⟶ body od «λs. True¬ s"
          by(simp add:wp_loop_guard)
        finally show ?thesis .
      qed
    qed
    thus "∀s. m s = Suc n ⟶ 1 ≤ wp do G ⟶ body od (λs. 1) s"
      by(simp add:embed_bool_def)
  qed
  thus ?thesis by(auto)
qed

text ‹This version allows progress to depend on an invariant. Termination is then determined by
  invariant's value in the initial state.›
lemma loop_term_nat_measure:
  fixes m :: "'s ==> nat" and body :: "'s prog"
  assumes wb:  "well_def body"
  and guard:   "∧s. m s = 0 ⟶ ¬ G s"
  and variant: "∧n. «λs. m s = Suc n¬ && «I¬ ⊨!!! wp body «λs. m s = n¬"
  and inv:     "wp_inv G body «I¬"
  shows "«I¬ ⊨!!! wp do G ⟶ body od (λs. 1)"
proof -
  note hb = well_def_wp_healthy[OF wb]
  note scb = sublinear_sub_conj[OF well_def_wp_sublinear, OF wb]
  have "«I¬ ⊨!!! wp do G ⟶ body od «λs. True¬"
  proof(rule use_premise, intro healthy_intros hb)
    fix s
    have "∧n. (∀s. m s = n ∧ I s ⟶ 1 ≤ wp do G ⟶ body od «λs. True¬ s)"
    proof(induct_tac n)
      fix n
      show "∀s. m s = 0 ∧ I s ⟶ 1 ≤ wp do G ⟶ body od «λs. True¬ s"
      proof(clarify)
        fix s
        assume "m s = 0"
        with guard have "¬ G s" by(blast)
        with hb show "1 ≤ wp do G ⟶ body od «λs. True¬ s"
          by(simp add:wp_loop_nguard)
      qed
      assume IH: "∀s. m s = n ∧ I s ⟶ 1 ≤ wp do G ⟶ body od «λs. True¬ s"
      show "∀s. m s = Suc n ∧ I s ⟶ 1 ≤ wp do G ⟶ body od «λs. True¬ s"
      proof(intro fold_premise healthy_intros hb le_funI)
        fix s
        show "«λs. m s = Suc n ∧ I s¬ s ≤ wp do G ⟶ body od «λs. True¬ s"
        proof(cases "G s")
          case False with hb show ?thesis
            by(simp add:wp_loop_nguard)
        next
          case True note G = this
          have "«λs. m s = Suc n¬ && «I¬ && «G¬ =
                «λs. m s = Suc n¬ && («I¬ && «I¬) && «G¬"
            by(simp)
          also have "... = («λs. m s = Suc n¬ && «I¬) && («I¬ && «G¬)"
            by(simp add:exp_conj_assoc exp_conj_unitary del:exp_conj_idem)
          also have "... = («λs. m s = Suc n¬ && «I¬) && («G¬ && «I¬)"
            by(simp only:exp_conj_comm)
          also {
            from inv hb have "«G¬ && «I¬ ⊨!!! wp body «I¬"
              by(rule wp_inv_stdD)
            with variant
            have "(«λs. m s = Suc n¬ && «I¬) && («G¬ && «I¬) ⊨!!!
                  wp body «λs. m s = n¬ && wp body «I¬"
              by(rule entails_frame)
          }
          also from scb
          have "wp body «λs. m s = n¬ && wp body «I¬ ⊨!!!
                wp body («λs. m s = n¬ && «I¬)"
            by(blast)
          finally have "«λs. m s = Suc n ¬ && « I ¬ && « G ¬ ⊨!!!
                        wp body (« λs. m s = n ¬ && « I ¬)" .
          moreover {
            from IH have "«λs. m s = n ∧ I s¬ ⊨!!! wp do G ⟶ body od «λs. True¬"
              by(blast intro:use_premise healthy_intros hb)
            hence "«λs. m s = n¬ && «I¬ ⊨!!! wp do G ⟶ body od «λs. True¬"
              by(simp add:exp_conj_std_split)
          }
          ultimately
          have "«λs. m s = Suc n ¬ && « I ¬ && « G ¬ ⊨!!!
                wp (body ;; do G ⟶ body od) «λs. True¬"
            using wb by(blast intro:wp_Seq wd_intros)
          hence "(«λs. m s = Suc n ∧ I s¬ && « G ¬) s ≤
                 wp (body ;; do G ⟶ body od) «λs. True¬ s"
            by(auto simp:exp_conj_std_split)
          with G have "«λs. m s = Suc n ∧ I s¬ s ≤
                       wp (body ;; do G ⟶ body od) «λs. True¬ s"
            by(simp add:exp_conj_def)
          also from hb G have "... = wp do G ⟶ body od «λs. True¬ s"
            by(simp add:wp_loop_guard)
          finally show ?thesis .
        qed
      qed
    qed
    moreover assume "I s"
    ultimately show "1 ≤ wp do G ⟶ body od «λs. True¬ s"
      by(auto)
  qed
  thus ?thesis by(simp add:embed_bool_def)
qed

subsection ‹Probabilistic Termination›

text ‹Any loop that has a non-zero chance of terminating after each step terminates with
  1.›

lemma termination_0_1:
  fixes body :: "'s prog"
  assumes wb: "well_def body"
      ― ‹The loop terminates in one step with nonzero probability›
      and onestep: "(λs. p) ⊨!!! wp body «N G¬"
      and nzp:     "0 < p"
      ― ‹The body is maximal i.e.~it terminates absolutely.›
      and mb:      "maximal (wp body)"
  shows "λs. 1 ⊨!!! wp do G ⟶ body od (λs. 1)"
proof -
  note hb = well_def_wp_healthy[OF wb]
  note sb = healthy_scalingD[OF hb]
  note sab = sublinear_subadd[OF well_def_wp_sublinear, OF wb, OF healthy_feasibleD, OF hb]

  from hb have hloop: "healthy (wp do G ⟶ body od)"
    by(rule healthy_intros)
  hence swp: "sound (wp do G ⟶ body od (λs. 1))" by(blast)

  txt ‹@{term p} is no greater than $1$, by feasibility.›
  from onestep have onestep': "∧s. p ≤ wp body «N G¬ s" by(auto)
  also {
    from hb have "unitary (wp body «N G¬)" by(auto)
    hence "∧s. wp body «N G¬ s ≤ 1" by(auto)
  }
  finally have p1: "p ≤ 1" .

  txt ‹This is the crux of the proof: that given a lower bound below $1$, we can find another,
 higher one.›
  have new_bound: "∧k. 0 ≤ k ==> k ≤ 1 ==> (λs. k) ⊨!!! wp do G ⟶ body od (λs. 1) ==>
            (λs. p * (1-k) + k) ⊨!!! wp do G ⟶ body od (λs. 1)"
  proof(rule le_funI)
    fix k s
    assume X: "λs. k ⊨!!! wp do G ⟶ body od (λs. 1)"
       and k0: "0 ≤ k" and k1: "k ≤ 1"

    from k1 have nz1k: "0 ≤ 1 - k" by(auto)
    with p1 have "p * (1-k) + k ≤ 1 * (1-k) + k"
      by(blast intro:mult_right_mono add_mono)
    hence "p * (1 - k) + k ≤ 1"
      by(simp)
    txt ‹The new bound is @{term "p * (1-k) + k"}.›
    hence "p * (1-k) + k ≤ «N G¬ s + «G¬ s * (p * (1-k) + k)"
      by(cases "G s", simp_all)
    txt ‹By the one-step termination assumption:›
    also from onestep' nz1k
    have "... ≤ «N G¬ s + «G¬ s * (wp body «N G¬ s * (1-k) + k)"
      by (simp add: mult_right_mono ordered_comm_semiring_class.comm_mult_left_mono)
    txt ‹By scaling:›
    also from nz1k
    have "... = «N G¬ s + «G¬ s * (wp body (λs. «N G¬ s * (1-k)) s + k)"
      by(simp add:right_scalingD[OF sb])
    txt ‹By the maximality (termination) of the loop body:›
    also from mb k0
    have "... = «N G¬ s + «G¬ s * (wp body (λs. «N G¬ s * (1-k)) s + wp body (λs. k) s)"
      by(simp add:maximalD)
    txt ‹By sub-additivity of the loop body:›
    also from k0 nz1k
    have "... ≤ «N G¬ s + «G¬ s * (wp body (λs. «N G¬ s * (1-k) + k) s)"
      by(auto intro!:add_left_mono mult_left_mono sub_addD[OF sab] sound_intros)
    also
    have "... = «N G¬ s + «G¬ s * (wp body (λs. «N G¬ s + «G¬ s * k) s)"
      by(simp add:negate_embed algebra_simps)
    txt ‹By monotonicity of the loop body, and that @{term k} is a lower bound:›
    also from k0 hloop le_funD[OF X]
    have "... ≤ «N G¬ s +
      «G¬ s * (wp body (λs. «N G¬ s + «G¬ s * wp do G ⟶ body od (λs. 1) s) s)"
      by(iprover intro:add_left_mono mult_left_mono le_funI embed_ge_0
                       le_funD[OF mono_transD, OF healthy_monoD, OF hb]
                       sound_sum standard_sound sound_intros swp)
    txt ‹Unrolling the loop once and simplifying:›
    also {
      have "∧s. «N G¬ s + «G¬ s * wp body (wp do G ⟶ body od (λs. 1)) s =
        «N G¬ s + «G¬ s * («N G¬ s + «G¬ s * wp body (wp do G ⟶ body od (λs. 1)) s)"
        by(simp only:distrib_left mult.assoc[symmetric] embed_bool_idem embed_bool_cancel)
      also have "∧s. ... s = «N G¬ s + «G¬ s * wp do G ⟶ body od (λs. 1) s"
        by(simp add:fun_cong[OF wp_loop_unfold[symmetric, where P="λs. 1", simplified, OF hb]])
      finally have X: "∧s. «N G¬ s + «G¬ s * wp body (wp do G ⟶ body od (λs. 1)) s =
        «N G¬ s + «G¬ s * wp do G ⟶ body od (λs. 1) s" .
      have "«N G¬ s + «G¬ s * (wp body (λs. «N G¬ s + «G¬ s *
              wp do G ⟶ body od (λs. 1) s) s) =
            «N G¬ s + «G¬ s * (wp body (λs. «N G¬ s + «G¬ s *
              wp body (wp do G ⟶ body od (λs. 1)) s) s)"
        by(simp only:X)
    }
    txt ‹Lastly, by folding two loop iterations:›
    also
    have "«N G¬ s + «G¬ s * (wp body (λs. «N G¬ s + «G¬ s *
            wp body (wp do G ⟶ body od (λs. 1)) s) s) =
          wp do G ⟶ body od (λs. 1) s"
      by(simp add:wp_loop_unfold[OF _ hb, where P="λs. 1", simplified, symmetric]
                  fun_cong[OF wp_loop_unfold[OF _ hb, where P="λs. 1", simplified, symmetric]])
    finally show "p * (1-k) + k ≤ wp do G ⟶ body od (λs. 1) s" .
  qed

  txt ‹If the previous bound lay in $[0,1)$, the new bound is strictly greater. This is where
 we appeal to the fact that @{term p} is nonzero.›
  from nzp have inc: "∧k. 0 ≤ k ==> k < 1 ==> k < p * (1 - k) + k"
    by(auto intro:mult_pos_pos)

  txt ‹The result follows by contradiction.›
  show ?thesis
  proof(rule ccontr)
    txt ‹If the loop does not terminate everywhere, then there must exist some state
 from which the probability of termination is strictly less than one.›
    assume "¬ ?thesis"
    hence "¬ (∀s. 1 ≤ wp do G ⟶ body od (λs. 1) s)" by(auto)
    then obtain s where point: "¬ 1 ≤ wp do G ⟶ body od (λs. 1) s" by(auto)

    let ?k = "Inf (range (wp do G ⟶ body od (λs. 1)))"

    from hloop
    have Inflb: "∧s. ?k ≤ wp do G ⟶ body od (λs. 1) s"
      by(intro cInf_lower bdd_belowI, auto)
    also from point have "wp do G ⟶ body od (λs. 1) s < 1" by(auto)
    txt ‹Thus the least (infimum) probabilty of termination is strictly less than one.›
    finally have k1: "?k < 1" .
    hence "?k ≤ 1" by(auto)
    moreover from hloop have k0: "0 ≤ ?k"
      by(intro cInf_greatest, auto)
    txt ‹The infimum is, naturally, a lower bound.›
    moreover from Inflb have "(λs. ?k) ⊨!!! wp do G ⟶ body od (λs. 1)" by(auto)
    ultimately
    txt ‹We can therefore use the previous result to find a new bound, \ldots›
    have "∧s. p * (1 - ?k) + ?k ≤ wp do G ⟶ body od (λs. 1) s"
      by(blast intro:le_funD[OF new_bound])
    txt ‹\ldots which is lower than the infimum, by minimality, \ldots›
    hence "p * (1 - ?k) + ?k ≤ ?k"
      by(blast intro:cInf_greatest)
    txt ‹\ldots yet also strictly greater than it.›
    moreover from k0 k1 have "?k < p * (1 - ?k) + ?k" by(rule inc)
    txt ‹We thus have a contradiction.›
    ultimately show False by(simp)
  qed
qed

end