Theory Hoare_Total_EX2

(* Author: Tobias Nipkow *)

subsubsection "Hoare Logic for Total Correctness With Logical Variables"

theory Hoare_Total_EX2
imports Hoare
begin

text‹This is the standard set of rules that you find in many publications.
In the while-rule, a logical variable is needed to remember the pre-value
of the variant (an expression that decreases by one with each iteration).
In this theory, logical variables are modeled explicitly.
A simpler (but not quite as flexible) approach is found in theory ‹Hoare_Total_EX›:
pre and post-condition are connected via a universally quantified HOL variable.›

type_synonym lvname = string
type_synonym assn2 = "(lvname ⇒ nat) ⇒ state ⇒ bool"

definition hoare_tvalid :: "assn2 ⇒ com ⇒ assn2 ⇒ bool"
  ("⊨⇩_t {(1_)}/ (_)/ {(1_)}" 50) where
"⊨⇩_t {P}c{Q}  ⟷  (∀l s. P l s ⟶ (∃t. (c,s) ⇒ t ∧ Q l t))"

inductive
  hoaret :: "assn2 ⇒ com ⇒ assn2 ⇒ bool" ("⊢⇩_t ({(1_)}/ (_)/ {(1_)})" 50)
where

Skip:  "⊢⇩_t {P} SKIP {P}"  |

Assign:  "⊢⇩_t {λl s. P l (s[a/x])} x::=a {P}"  |

Seq: "⟦ ⊢⇩_t {P⇩₁} c⇩₁ {P⇩₂}; ⊢⇩_t {P⇩₂} c⇩₂ {P⇩₃} ⟧ ⟹ ⊢⇩_t {P⇩₁} c⇩₁;;c⇩₂ {P⇩₃}" |

If: "⟦ ⊢⇩_t {λl s. P l s ∧ bval b s} c⇩₁ {Q}; ⊢⇩_t {λl s. P l s ∧ ¬ bval b s} c⇩₂ {Q} ⟧
  ⟹ ⊢⇩_t {P} IF b THEN c⇩₁ ELSE c⇩₂ {Q}" |

While:
  "⟦ ⊢⇩_t {λl. P (l(x := Suc(l(x))))} c {P};
     ∀l s. l x > 0 ∧ P l s ⟶ bval b s;
     ∀l s. l x = 0 ∧ P l s ⟶ ¬ bval b s ⟧
   ⟹ ⊢⇩_t {λl s. ∃n. P (l(x:=n)) s} WHILE b DO c {λl s. P (l(x := 0)) s}" |

conseq: "⟦ ∀l s. P' l s ⟶ P l s; ⊢⇩_t {P}c{Q}; ∀l s. Q l s ⟶ Q' l s  ⟧ ⟹
           ⊢⇩_t {P'}c{Q'}"

text‹Building in the consequence rule:›

lemma strengthen_pre:
  "⟦ ∀l s. P' l s ⟶ P l s;  ⊢⇩_t {P} c {Q} ⟧ ⟹ ⊢⇩_t {P'} c {Q}"
by (metis conseq)

lemma weaken_post:
  "⟦ ⊢⇩_t {P} c {Q};  ∀l s. Q l s ⟶ Q' l s ⟧ ⟹  ⊢⇩_t {P} c {Q'}"
by (metis conseq)

lemma Assign': "∀l s. P l s ⟶ Q l (s[a/x]) ⟹ ⊢⇩_t {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])

text‹The soundness theorem:›

theorem hoaret_sound: "⊢⇩_t {P}c{Q}  ⟹  ⊨⇩_t {P}c{Q}"
proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
  case (While P x c b)
  have "⟦ l x = n; P l s ⟧ ⟹ ∃t. (WHILE b DO c, s) ⇒ t ∧ P (l(x := 0)) t" for n l s
  proof(induction "n" arbitrary: l s)
    case 0 thus ?case using While.hyps(3) WhileFalse
      by (metis fun_upd_triv)
  next
    case Suc
    thus ?case using While.IH While.hyps(2) WhileTrue
      by (metis fun_upd_same fun_upd_triv fun_upd_upd zero_less_Suc)
  qed
  thus ?case by fastforce
next
  case If thus ?case by auto blast
qed fastforce+


definition wpt :: "com ⇒ assn2 ⇒ assn2" ("wp⇩_t") where
"wp⇩_t c Q  =  (λl s. ∃t. (c,s) ⇒ t ∧ Q l t)"

lemma [simp]: "wp⇩_t SKIP Q = Q"
by(auto intro!: ext simp: wpt_def)

lemma [simp]: "wp⇩_t (x ::= e) Q = (λl s. Q l (s(x := aval e s)))"
by(auto intro!: ext simp: wpt_def)

lemma wpt_Seq[simp]: "wp⇩_t (c⇩₁;;c⇩₂) Q = wp⇩_t c⇩₁ (wp⇩_t c⇩₂ Q)"
by (auto simp: wpt_def fun_eq_iff)

lemma [simp]:
 "wp⇩_t (IF b THEN c⇩₁ ELSE c⇩₂) Q = (λl s. wp⇩_t (if bval b s then c⇩₁ else c⇩₂) Q l s)"
by (auto simp: wpt_def fun_eq_iff)


text‹Function ‹wpw› computes the weakest precondition of a While-loop
that is unfolded a fixed number of times.›

fun wpw :: "bexp ⇒ com ⇒ nat ⇒ assn2 ⇒ assn2" where
"wpw b c 0 Q l s = (¬ bval b s ∧ Q l s)" |
"wpw b c (Suc n) Q l s = (bval b s ∧ (∃s'. (c,s) ⇒ s' ∧  wpw b c n Q l s'))"

lemma WHILE_Its:
  "(WHILE b DO c,s) ⇒ t ⟹ Q l t ⟹ ∃n. wpw b c n Q l s"
proof(induction "WHILE b DO c" s t arbitrary: l rule: big_step_induct)
  case WhileFalse thus ?case using wpw.simps(1) by blast
next
  case WhileTrue show ?case
    using wpw.simps(2) WhileTrue(1,2) WhileTrue(5)[OF WhileTrue(6)] by blast
qed

definition support :: "assn2 ⇒ string set" where
"support P = {x. ∃l1 l2 s. (∀y. y ≠ x ⟶ l1 y = l2 y) ∧ P l1 s ≠ P l2 s}"

lemma support_wpt: "support (wp⇩_t c Q) ⊆ support Q"
by(simp add: support_def wpt_def) blast


lemma support_wpw0: "support (wpw b c n Q) ⊆ support Q"
proof(induction n)
  case 0 show ?case by (simp add: support_def) blast
next
  case Suc
  have 1: "support (λl s. A s ∧ B l s) ⊆ support B" for A B
    by(auto simp: support_def)
  have 2: "support (λl s. ∃s'. A s s' ∧ B l s') ⊆ support B" for A B
    by(auto simp: support_def) blast+
  from Suc 1 2 show ?case by simp (meson order_trans)
qed

lemma support_wpw_Un:
  "support (%l. wpw b c (l x) Q l) ⊆ insert x (UN n. support(wpw b c n Q))"
using support_wpw0[of b c _ Q]
apply(auto simp add: support_def subset_iff)
apply metis
apply metis
done

lemma support_wpw: "support (%l. wpw b c (l x) Q l) ⊆ insert x (support Q)"
using support_wpw0[of b c _ Q] support_wpw_Un[of b c _ Q]
by blast

lemma assn2_lupd: "x ∉ support Q ⟹ Q (l(x:=n)) = Q l"
by(simp add: support_def fun_upd_other fun_eq_iff)
  (metis (no_types, lifting) fun_upd_def)

abbreviation "new Q ≡ SOME x. x ∉ support Q"

lemma wpw_lupd: "x ∉ support Q ⟹ wpw b c n Q (l(x := u)) = wpw b c n Q l"
by(induction n) (auto simp: assn2_lupd fun_eq_iff)

lemma wpt_is_pre: "finite(support Q) ⟹ ⊢⇩_t {wp⇩_t c Q} c {Q}"
proof (induction c arbitrary: Q)
  case SKIP show ?case by (auto intro:hoaret.Skip)
next
  case Assign show ?case by (auto intro:hoaret.Assign)
next
  case (Seq c1 c2) show ?case
    by (auto intro:hoaret.Seq Seq finite_subset[OF support_wpt])
next
  case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
next
  case (While b c)
  let ?x = "new Q"
  have "∃x. x ∉ support Q" using While.prems infinite_UNIV_listI
    using ex_new_if_finite by blast
  hence [simp]: "?x ∉ support Q" by (rule someI_ex)
  let ?w = "WHILE b DO c"
  have fsup: "finite (support (λl. wpw b c (l x) Q l))" for x
    using finite_subset[OF support_wpw] While.prems by simp
  have c1: "∀l s. wp⇩_t ?w Q l s ⟶ (∃n. wpw b c n Q l s)"
    unfolding wpt_def by (metis WHILE_Its)
  have c2: "∀l s. l ?x = 0 ∧ wpw b c (l ?x) Q l s ⟶ ¬ bval b s"
    by (simp cong: conj_cong)
  have w2: "∀l s. 0 < l ?x ∧ wpw b c (l ?x) Q l s ⟶ bval b s"
    by (auto simp: gr0_conv_Suc cong: conj_cong)
  have 1: "∀l s. wpw b c (Suc(l ?x)) Q l s ⟶
                  (∃t. (c, s) ⇒ t ∧ wpw b c (l ?x) Q l t)"
    by simp
  have *: "⊢⇩_t {λl. wpw b c (Suc (l ?x)) Q l} c {λl. wpw b c (l ?x) Q l}"
    by(rule strengthen_pre[OF 1
          While.IH[of "λl. wpw b c (l ?x) Q l", unfolded wpt_def, OF fsup]])
  show ?case
  apply(rule conseq[OF _ hoaret.While[OF _ w2 c2]])
    apply (simp_all add: c1 * assn2_lupd wpw_lupd del: wpw.simps(2))
  done
qed

theorem hoaret_complete: "finite(support Q) ⟹ ⊨⇩_t {P}c{Q} ⟹ ⊢⇩_t {P}c{Q}"
apply(rule strengthen_pre[OF _ wpt_is_pre])
apply(auto simp: hoare_tvalid_def wpt_def)
done


text ‹Two examples:›

lemma "⊢⇩_t 
{λl s. l ''x'' = nat(s ''x'')}
 WHILE Less (N 0) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N (-1))
{λl s. s ''x'' ≤ 0}"
apply(rule conseq)
prefer 2
 apply(rule While[where P = "λl s. l ''x'' = nat(s ''x'')" and x = "''x''"])
   apply(rule Assign')
   apply auto
done

lemma "⊢⇩_t 
{λl s. l ''x'' = nat(s ''x'')}
 WHILE Less (N 0) (V ''x'')
 DO (''x'' ::= Plus (V ''x'') (N (-1));;
    (''y'' ::= V ''x'';;
     WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N (-1))))
{λl s. s ''x'' ≤ 0}"
apply(rule conseq)
prefer 2
 apply(rule While[where P = "λl s. l ''x'' = nat(s ''x'')" and x = "''x''"])
   defer
   apply auto
apply(rule Seq)
 prefer 2
 apply(rule Seq)
  prefer 2
  apply(rule weaken_post)
   apply(rule_tac P = "λl s. l ''x'' = nat(s ''x'') ∧ l ''y'' = nat(s ''y'')" and x = "''y''" in While)
     apply(rule Assign')
     apply auto[4]
 apply(rule Assign)
apply(rule Assign')
apply auto
done

end