Quelle  Quant_VCG.thy

subsection "Verification Condition Generator"
theory Quant_VCG
imports Quant_Hoare
begin

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)

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)"
  
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 ({I} WHILE b DO C) Q = (λs. I s + 1)"
   
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))"


subsubsection "Soundness of VCG"
  
lemma vc_sound: "vc C Q ==> ⊨₂ {pre C Q} strip C { Q }"
proof (induct C arbitrary: Q) 
  case (Aif b C1 C2)
  then have Aif1: "⊨₂ {pre C1 Q} strip C1 {Q}" and Aif2: "⊨₂ {pre C2 Q} strip C2 {Q}" by auto
    show ?case apply auto apply(rule hoare2.conseq)
      apply(rule hoare2.If[where P="%s. if bval b s then pre C1 Q s else pre C2 Q s" and Q="Q"])
    subgoal
      apply(rule hoare2.conseq)
        apply (fact Aif1)
      subgoal for s apply(cases "bval b s") by auto
      apply simp done
    subgoal 
      apply(rule hoare2.conseq)
        apply (fact Aif2)
      subgoal for s apply(cases "bval b s") by auto
      apply simp done
     apply auto
    done
next
  case (Awhile I b C)
  then have i: "(∧Q. vc C Q ==> ⊨₂ {pre C Q} strip C {Q})"
   and ii: " ∀s. pre C (λs. I s + 1) s ≤ I s + ↑ (bval b s) ∧ Q s ≤ I s + ↑ (¬ bval b s)" 
     and iii: "vc C (λs. I s + 1)" by auto
     
  from i iii have  A: "⊨₂ {pre C (λs. I s + 1)} strip C {(λs. I s + 1)}" by auto 
    
  have   "⊨₂ {λs. I s + 1} WHILE b DO strip C {Q}"
    apply(rule hoare2.conseq)
     apply(rule hoare2.While[where I=I])
      apply(rule hoare2.conseq)
        apply(rule A) using ii by auto
  then show ?case by auto      
qed (auto intro: hoare2.Skip hoare2.Assign hoare2.Seq )
  
  
lemma vc_sound': "[vc C Q ; (∀s. pre C Q s ≤ P s) ] ==> ⊨₂ {P} strip C { Q }"
  apply(rule hoare2.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)    
    
    
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)
  thus ?case 
    apply (auto simp: pre_mono) 
    using order.trans by blast   
qed (auto simp: pre_mono)
    
    
lemma "⊨₂ { 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: hoare2.induct)
  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 simp 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 Q 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 using vc1 vc2 vc_mono pre2 by auto 
    subgoal 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 using pre vc by auto
    subgoal by simp
  done
next
  case (conseq 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 conseq(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 conseq(3) vc_mono by auto
    subgoal using pre conseq(2) 1 using order.trans  by metis
    done
qed
     
  
  
  
    
end