Quelle  QuantK_VCG.thy

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 (C₁;; C₂) = (strip C₁;; strip C₂)" |
"strip (IF b THEN C₁ ELSE C₂) = (IF b THEN strip C₁ ELSE strip C₂)" |
"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 (C₁;; C₂) Q = pre C₁ (pre C₂ Q)" |
"pre (IF b THEN C₁ ELSE C₂) Q =
  (λs. eSuc (if bval b s then pre C₁ Q s else pre C₂ 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 (C₁ ;; C₂) Q = ((vc C₁ (pre C₂ Q)) ∧ (vc C₂ Q) )" |
"vc (IF b THEN C₁ ELSE C₂) Q = (vc C₁ Q ∧ vc C₂ 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 c₁ Q c₂)
  from If(3) obtain C1 where strip1: "strip C1 = c₁" 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 = c₂" 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 P₁ c₁ P₂ c₂ P₃)
  from Seq(3) obtain C1 where strip1: "strip C1 = c₁" and vc1: "vc C1 P₂"
      and pre1: "(∀s. pre C1 P₂ s ≤ P₁ s)"    by blast
  from Seq(4) obtain C2 where strip2: "strip C2 = c₂" and vc2: "vc C2 P₃"
      and pre2: "∧s. pre C2 P₃ s ≤ P₂ s"   by blast
       
  {
    fix s
    have "pre C1 (pre C2 P₃) s ≤ P₁ s" 
      apply(rule order.trans[where b="pre C1 P₂ 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 c₁ Q c₂)
  from ZIf(3) obtain C1 where strip1: "strip C1 = c₁" 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 = c₂" 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 P₁ c₁ P₂ c₂ P₃)
  from ZSeq(3) obtain C1 where strip1: "strip C1 = c₁" and vc1: "vc C1 P₂" and pre1: "(∀s. pre C1 P₂ s ≤ P₁ s)"  by blast
  from ZSeq(4) obtain C2 where strip2: "strip C2 = c₂" and vc2: "vc C2 P₃" and pre2: "(∀s. pre C2 P₃ s ≤ P₂ s)"  by blast
  {
    fix s
    have "pre C1 (pre C2 P₃) s ≤ P₁ s" 
      apply(rule order.trans[where b="pre C1 P₂ 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