Theory QuantK_VCG

subsection "Verification Condition Generator"
theory QuantK_VCG
imports QuantK_Hoare
begin

subsubsection "Ceiling integer division on extended natural numbers"

definition "mydiv (a::nat) (k::nat) = (if k dvd a then a div k else (a div k) + 1)"
   
lemma mydivcode: "k>0 ⟹ D≥k ⟹ mydiv D k = Suc (mydiv (D-k) k)"  
  unfolding mydiv_def apply (auto simp add: le_div_geq)
  using dvd_minus_self by auto 
    
lemma mydivcode1: "mydiv 0 k = 0"  
  unfolding mydiv_def by auto 
    
lemma mydivcode2: "k>0 ⟹ 0<D ⟹ D<k ⟹ mydiv D k = Suc 0"  
  unfolding mydiv_def by auto
    
lemma mydiv_mono: "a≤b ⟹ mydiv a k ≤ mydiv b k" unfolding mydiv_def
  apply(cases "k dvd a")
  subgoal apply(cases "k dvd b")  apply auto apply (auto simp add: div_le_mono)
    using div_le_mono le_Suc_eq by blast  
  subgoal apply(cases "k dvd b")  apply auto apply (auto simp add: div_le_mono)
    by (metis Suc_leI add.right_neutral div_le_mono div_mult_mod_eq dvd_imp_mod_0 le_add1 le_antisym less_le) 
     done
      
lemma mydiv_cancel: "0 < k ⟹ mydiv (k * i) k = i"    
  unfolding mydiv_def by auto 
    
lemma assumes k: "k>0" and B: "B ≤ k*A"
  shows mydiv_le_E: "mydiv B k ≤ A"
proof - 
  from mydiv_mono[OF B] and k mydiv_cancel show ?thesis 
    by metis
qed
lemma mydiv_mult_leq: "0 < k ⟹ l≤k ⟹ mydiv (l*A) k ≤ A"
  by(simp add: mydiv_le_E)
   
lemma mydiv_cancel3: "0 < k ⟹ i ≤ k * mydiv i k"
  by (auto simp add: mydiv_def dividend_less_times_div le_eq_less_or_eq)  
                                                                                                    
definition "ediv a k = (if a=∞ then ∞ else enat (mydiv (THE i. a=enat i) k))"  
  
lemma ediv_enat[simp]: "ediv (enat a) k = enat (mydiv a k)"
  unfolding ediv_def by auto
lemma ediv_mydiv[simp]: "ediv (enat a) k ≤ enat f ⟷ mydiv a k ≤ f"
  unfolding ediv_def by auto
  
lemma ediv_mono: "a≤b ⟹ ediv a k ≤ ediv b k"
  unfolding ediv_def by (auto simp add: mydiv_mono) 

lemma ediv_cancel2: "k>0 ⟹ ediv (enat k * x) k = x"
  unfolding ediv_def apply(cases "x=∞") using mydiv_cancel by auto
        
lemma ediv_cancel3: "k>0 ⟹ A ≤ enat k * ediv A k"
  unfolding ediv_def apply(cases "A=∞") using mydiv_cancel3 by auto 

subsubsection "Definition of VCG"    
  
datatype acom =
  Askip                  (‹SKIP›) |
  Aassign vname aexp     (‹(_ ::= _)› [1000, 61] 61) |
  Aseq   acom acom       (‹_;;/ _›  [60, 61] 60) | 
  Aif bexp acom acom     (‹(IF _/ THEN _/ ELSE _)›  [0, 0, 61] 61) |
  Awhile qassn bexp acom  (‹({_}/ WHILE _/ DO _)›  [0, 0, 61] 61)
 |  Abst nat acom  (‹({_}/ Ab _)›  [0, 61] 61)

notation com.SKIP (‹SKIP›)
  
fun strip :: "acom ⇒ com" where
"strip SKIP = SKIP" |
"strip (x ::= a) = (x ::= a)" |
"strip (C1;; C2) = (strip C1;; strip C2)" |
"strip (IF b THEN C1 ELSE C2) = (IF b THEN strip C1 ELSE strip C2)" |
"strip ({_} WHILE b DO C) = (WHILE b DO strip C)" |
"strip ({_} Ab C) = strip C"
    
fun pre :: "acom ⇒ qassn ⇒ qassn" where
"pre SKIP Q = (λs. eSuc (Q s))" |
"pre (x ::= a) Q = (λs. eSuc (Q (s[a/x])))" |
"pre (C1;; C2) Q = pre C1 (pre C2 Q)" |
"pre (IF b THEN C1 ELSE C2) Q =
  (λs. eSuc (if bval b s then pre C1 Q s  else pre C2 Q s  ))" |
"pre ({P} WHILE b DO C) Q = (%s. P s + 1)" |
"pre ({k} Ab C) Q = (λs. ediv (pre C (λs. k*Q s) s) k)"
  
text ‹In contrast to @{term pre}, @{term vc} produces a formula that is independent of the state:›
  
fun vc :: "acom ⇒ qassn ⇒ bool" where
"vc SKIP Q = True" |
"vc (x ::= a) Q = True" |
"vc (C1 ;; C2) Q = ((vc C1 (pre C2 Q)) ∧ (vc C2 Q) )" |
"vc (IF b THEN C1 ELSE C2) Q = (vc C1 Q ∧ vc C2 Q)" |  
"vc ({I} WHILE b DO C) Q =  ( (∀s.  (pre C (λs. I s + 1) s ≤ I s + ↑(bval b s)) ∧ ( Q s ≤ I s + ↑ (¬ bval b s))) ∧ vc C (%s. I s + 1))" |
"vc ({k} Ab C) Q = (vc C (λs. enat k* Q s) ∧ k>0 ⌦‹∧ (∀s. pre C (λs. enat k * Q s) s ≤ enat k * ediv (pre C (λs. enat k * Q s) s) k)›)"

subsubsection "Soundness of VCG"
  
lemma vc_sound: "vc C Q ⟹  ⊢2' {pre C Q} strip C { Q }"
proof (induct C arbitrary: Q) 
  case (Aif b C1 C2)
  then have Aif1: "⊢2' {pre C1 Q} strip C1 {Q}" and Aif2: "⊢2' {pre C2 Q} strip C2 {Q}" by auto
    show ?case apply auto apply(rule hoareQ.conseq[where k=1])
      apply(rule hoareQ.If[where P="%s. if bval b s then pre C1 Q s else pre C2 Q s" and Q="Q"])
    subgoal
      apply(rule hoareQ.conseq[where k=1])
         apply (fact Aif1)
      subgoal for s apply(cases "bval b s") by auto
      apply auto done
    subgoal 
      apply(rule hoareQ.conseq[where k=1])
        apply (fact Aif2)
      subgoal for s apply(cases "bval b s") by auto
      apply auto done
     apply auto
    done
next
  case (Awhile I b C)
  then have i: "(⋀Q. vc C Q ⟹ ⊢2' {pre C Q} strip C {Q})"
   and ii': " ∀s. pre C (λs. I s + 1) s ≤ I s + ↑ (bval b s)" 
   and ii'': "⋀s. Q s ≤  I s + ↑ (¬ bval b s)" 
     and iii: "vc C (λs. I s + 1)"
    by auto

  from i iii have  A: "⊢2' {pre C (λs. I s + 1)} strip C {(λs. I s + 1)}" by auto 
     
  show ?case
    apply simp
    apply(rule conseq[where k=1])
       apply(rule While[where I=I])
       apply(rule weakenpre)
        apply(rule A)
      apply(rule ii') apply simp
    using ii'' apply auto done  
next
  case (Abst k C)
  then have vc: "vc C (λs. k* Q s)" and k: "k>0" by auto
  from Abst(1) vc have C: "⊢2' {pre C (%s. k*Q s)} strip C {(%s. k*Q s)}" by auto
  show ?case apply(simp)
    apply(rule conseq)
       apply(rule C) using k apply auto
      using ediv_cancel3 by auto
qed (auto intro: hoareQ.Skip hoareQ.Assign hoareQ.Seq )


lemma vc_sound': "⟦vc C Q ; (∀s. pre C Q s ≤ P s) ⟧ ⟹  ⊢2' {P} strip C { Q }"
  apply(rule hoareQ.conseq[where k=1])
    apply(rule vc_sound) by auto


lemma vc_sound'': "⟦vc C Q' ; (∀s.  pre C Q' s ≤ k * P s)  ; (⋀s. enat k * Q s ≤ Q' s); k>0 ⟧ ⟹  ⊢2' {P} strip C { Q }"
  apply(rule hoareQ.conseq )
    apply(rule vc_sound) by auto

  
subsubsection "Completeness" 
  
lemma pre_mono: assumes "⋀s. P' s ≤ P s" 
  shows "⋀s. pre C P' s ≤ pre C P s"
  using assms by (induct C arbitrary: P P', auto simp: ediv_mono mult_left_mono )    
      
lemma vc_mono: assumes "⋀s. P' s ≤ P s" 
  shows "vc C P ⟹ vc C P'"    
  using assms
proof (induct C arbitrary: P P') 
  case (Awhile I b C Q)
  thus ?case 
    apply (auto simp: pre_mono) 
    using order.trans by blast  
next
  case (Abst x1 C)
  then show ?case by (auto simp: mult_left_mono)  
qed (auto simp: pre_mono)
      
    
lemma "⊢2' { P } c { Q } ⟹ ∃C. strip C = c ∧ vc C Q ∧ (∀s. pre C Q s ≤ P s)"
  (is "_ ⟹   ∃C. ?G P c Q C")
proof (induction rule: hoareQ.induct)
  case (conseq P c Q k P' Q')
  then obtain C where strip: "strip C = c" and vc: "vc C Q" and pre: "⋀s. pre C Q s ≤ P s"
    by blast
  
  { fix s
    have "pre C (λs. enat k * Q' s) s ≤ pre C Q s" using pre_mono conseq(3) by simp 
    also 
    from pre conseq(2) have "…  ≤ enat k * P' s" using order.trans by blast
    finally have  "pre C (λs. enat k * Q' s) s  ≤ enat k * P' s" by auto
        then have  "ediv (pre C (λs. enat k * Q' s) s) k  ≤ ediv (enat k * P' s) k" using ediv_mono by auto
    moreover note  ediv_cancel2[OF conseq(4)]
    ultimately have "ediv (pre C (λs. enat k * Q' s) s) k ≤ P' s"    
      by simp
  } note compensate=this
  
  show ?case
    apply(rule exI[where x="{k} Ab C"])
    apply(safe)
    subgoal using strip by simp
    subgoal apply simp apply safe
      subgoal using vc vc_mono conseq(3) by force
      subgoal by fact
      done
    subgoal apply simp using compensate by auto
        done
next
  case (Skip P)
  show ?case (is "∃C. ?C C")
  proof show "?C Askip" by auto  qed
next
  case (Assign P a x)
  show ?case (is "∃C. ?C C")
  proof show "?C(Aassign x a)" by auto  qed
next
  case (If P b c1 Q c2)
  from If(3) obtain C1 where strip1: "strip C1 = c1" and vc1: "vc C1 Q"
        and pre1: "(⋀s. pre C1 Q s ≤ (P s + ↑(bval b s)))"
         by blast
  from If(4) obtain C2 where strip2: "strip C2 = c2" and vc2: "vc C2 Q"
        and pre2: "(⋀s. pre C2 (λs. Q s) s ≤ (P s + ↑(¬ bval b s)))"
    by blast

  show ?case
    apply(rule exI[where x="IF b THEN C1 ELSE C2"], safe)
    subgoal using strip1 strip2 by auto
    subgoal  using vc1 vc2 by auto 
    subgoal for s using pre1[of s] pre2[of s] by auto  
    done      
next
  case (Seq P1 c1 P2 c2 P3)
  from Seq(3) obtain C1 where strip1: "strip C1 = c1" and vc1: "vc C1 P2"
      and pre1: "(∀s. pre C1 P2 s ≤   P1 s)"    by blast
  from Seq(4) obtain C2 where strip2: "strip C2 = c2" and vc2: "vc C2 P3"
      and pre2: "⋀s. pre C2 P3 s ≤   P2 s"   by blast
       
  {
    fix s
    have "pre C1 (pre C2 P3) s ≤ P1 s" 
      apply(rule order.trans[where b="pre C1 P2 s"])
       apply(rule pre_mono) using pre2 apply simp using pre1 by simp
  } note pre = this
  show ?case
    apply(rule exI[where x="C1 ;; C2"], safe)
    subgoal using strip1 strip2 by simp
    subgoal apply simp apply safe  using vc1 vc2 vc_mono pre2 by auto 
    subgoal    apply simp using  pre by auto  
      done 
next
  case (While I b c)
  from While(2) obtain C where strip: "strip C = c" and vc: "vc C (λa. I a + 1)"
    and pre: "⋀s. pre C (λa. I a + 1) s ≤ I s + ↑ (bval b s)" by blast
  show ?case 
    apply(rule exI[where x="{I} WHILE b DO C"], safe)
    subgoal using strip by simp
    subgoal apply simp using pre vc by auto
    subgoal by simp
  done
qed
    
lemma "⊢Z { P } c { Q } ⟹ ∃C. strip C = c ∧ vc C Q ∧ (∀s. pre C Q s ≤ P s)"
  (is "_ ⟹   ∃C. ?G P c Q C")
proof (induction rule: hoareQ'.induct)
  case (ZSkip P)
  show ?case (is "∃C. ?C C")
  proof show "?C Askip" by auto   
  qed
next
  case (ZAssign P a x)
  show ?case (is "∃C. ?C C")
  proof show "?C(Aassign x a)" by simp qed
next
  case (ZIf P b c1 Q c2)
  from ZIf(3) obtain C1 where strip1: "strip C1 = c1" and vc1: "vc C1 Q" and pre1: "(⋀s. pre C1 Q s ≤ P s + ↑ (bval b s))"  by blast
  from ZIf(4) obtain C2 where strip2: "strip C2 = c2" and vc2: "vc C2 Q" and pre2: "(⋀s. pre C2 Q s ≤ P s + ↑ (¬ bval b s))"  by blast
      
  show ?case apply(rule exI[where x="IF b THEN C1 ELSE C2"])
    apply(safe)
    subgoal using strip1 strip2 by auto
    subgoal using vc1 vc2 by auto
    subgoal for s apply auto 
        subgoal using pre1[of s] by auto 
        subgoal using pre2[of s] by auto 
        done
      done
next
  case (ZSeq P1 c1 P2 c2 P3)
  from ZSeq(3) obtain C1 where strip1: "strip C1 = c1" and vc1: "vc C1 P2" and pre1: "(∀s. pre C1 P2 s ≤ P1 s)"  by blast
  from ZSeq(4) obtain C2 where strip2: "strip C2 = c2" and vc2: "vc C2 P3" and pre2: "(∀s. pre C2 P3 s ≤ P2 s)"  by blast
  {
    fix s
    have "pre C1 (pre C2 P3) s ≤ P1 s" 
      apply(rule order.trans[where b="pre C1 P2 s"])
       apply(rule pre_mono) using pre2 apply simp using pre1 by simp
  } note pre = this
  show ?case apply(rule exI[where x="C1 ;; C2"])
    apply safe
    subgoal using strip1 strip2 by simp
    subgoal using vc1 vc2 vc_mono pre2 by auto 
    subgoal using pre by auto 
    done      
next
  case (ZWhile I b c)
  from ZWhile(2) obtain C where strip: "strip C = c" and vc: "vc C (λa. I a + 1)"
    and pre: "⋀s. pre C (λa. I a + 1) s ≤ I s + ↑ (bval b s)" by blast
  show ?case apply(rule exI[where x="{I} WHILE b DO C"])
    apply safe
    subgoal using strip by simp
    subgoal using pre vc by auto
    subgoal by simp
  done
next
  case (Zconseq' P c Q P' Q')
  then obtain C where "strip C = c" and vc: "vc C Q" and pre: "⋀s. pre C Q s ≤ P s" by blast
   
  from pre_mono[OF Zconseq'(3)] have 1: "⋀s. pre C Q' s ≤ pre C Q s" by auto
    
  show ?case
    apply(rule exI[where x=C])
    apply safe
      apply fact
    subgoal using vc Zconseq'(3) vc_mono by auto
    subgoal using pre Zconseq'(2) 1 using order.trans  by metis
    done
next
  case (Zconst k P c Q)
  then obtain C where strip: "strip C = c" and vc: "vc C (λa. enat k * Q a)" 
    and k: "k>0" and pre: "⋀s. pre C (λa. enat k * Q a) s ≤ enat k * P s" by blast
  show ?case
    apply(rule exI[where x="{k} Ab C"]) apply safe
    subgoal using strip by auto
    subgoal using vc k by auto
    subgoal apply auto using ediv_mono[OF pre] ediv_cancel2[OF k] by metis
    done
qed
  
    
end