Theory Quant_Hoare

section "Quantitative Hoare Logic (due to Carbonneaux)"
theory Quant_Hoare
imports Big_StepT Complex_Main "HOL-Library.Extended_Nat"
begin

  
abbreviation "eq a b == (And (Not (Less a b)) (Not (Less b a)))"
   
type_synonym lvname = string
type_synonym assn = "state  bool" (* time bound *)
type_synonym qassn = "state  enat" (* time bound *)

text ‹The support of an assn2›
 

abbreviation state_subst :: "state  aexp  vname  state"
  ("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

fun emb :: "bool  enat" ("") where
   "emb False = "
 | "emb True = 0"
  
subsection "Validity of quantitative Hoare Triple"
  
(* this definition refines the definition of validity of normal Hoare Triple for total correctness  *)

definition hoare2_valid :: "qassn  com  qassn  bool"
  ("2 {(1_)}/ (_)/ {(1_)}" 50) where
"2 {P} c {Q}    (s.  P s <   (t p. ((c,s)  p  t)  P s  p + Q t))"

subsection "Hoare logic for quantiative reasoning"

inductive
  hoare2 :: "qassn  com  qassn  bool" ("2 ({(1_)}/ (_)/ {(1_)})" 50)
where

Skip:  "2 {%s. eSuc (P s)} SKIP {P}"  |

Assign:  "2 {λs. eSuc (P (s[a/x]))} x::=a { P }"  |

If: " 2 {λs. P s + ( bval b s)} c1 { Q};
       2 {λs. P s + (¬ bval b s)} c2 { Q} 
   2 {λs. eSuc (P s)} IF b THEN c1 ELSE c2 { Q }"  |

Seq: " 2 { P1 } c1 { P2 }; 2 {P2} c2 { P3 }  2 {P1} c1;;c2 {P3}"  |
 
While:
  "   2 { %s. I s + (bval b s) } c { %t. I t + 1 }   
    2 {λs. I s + 1 } WHILE b DO c {λs.  I s + (¬ bval b s)  }" |

conseq: " 2 {P}c{Q} ; s. P s  P' s ; s. Q' s  Q s  
           2 {P'}c{ Q'}"  

text ‹derived rules›

lemma strengthen_pre: " s. P s  P' s;  2 {P} c {Q}   2 {P'} c {Q}"
  using conseq by blast 

lemma weaken_post: " 2 {P} c {Q};  s. Q s  Q' s    2 {P} c {Q'}"
  using conseq by blast

lemma Assign': "s. P s  eSuc ( Q(s[a/x]))  2 {P} x ::= a {Q}" 
  by (simp add: strengthen_pre[OF _ Assign])    

lemma progress: "(c, s)  p  t  p > 0"
  by (induct rule: big_step_t.induct, auto)
    

lemma FalseImplies: "2 {%s. } c { Q}"
  apply (induction c arbitrary: Q)
  apply(auto intro: hoare2.Skip hoare2.Assign hoare2.Seq hoare2.conseq)
  subgoal apply(rule hoare2.conseq) apply(rule hoare2.If[where P="%s. "]) by(auto intro: hoare2.If hoare2.conseq)
  subgoal apply(rule hoare2.conseq) apply(rule hoare2.While[where I="%s. "]) apply(rule hoare2.conseq) by auto 
  done
    
subsection "Soundness"

  
  
    
text‹The soundness theorem:›
   
lemma help1: assumes " enat a + X  Y"
    "enat b + Z  X"
  shows "enat (a + b) + Z  Y" 
  using assms  by (metis ab_semigroup_add_class.add_ac(1) add_left_mono order_trans plus_enat_simps(1))
    
lemma help2': assumes "enat p + INV t   INV s"
    "0 < p" "INV s = enat n"
  shows "INV t < INV s"
  using assms iadd_le_enat_iff by auto 
    
lemma help2: assumes "enat p + INV t + 1  INV s"
     "INV s = enat n"
  shows "INV t < INV s"
  using assms le_less_trans not_less_iff_gr_or_eq by fastforce  
  
    
lemma Seq_sound: assumes "2 {P1} C1 {P2}"
    "2 {P2} C2 {P3}" 
    shows  "2 {P1} C1 ;; C2 {P3}"
unfolding hoare2_valid_def                             
proof (safe) 
  fix s
  assume ninfP1: "P1 s < "
  with assms(1)[unfolded hoare2_valid_def] obtain t1 p1
    where 1: "(C1, s)  p1  t1" and q1: "enat p1 + P2 t1  P1 s" by blast
  with ninfP1 have ninfP2: "P2 t1 < "
    using not_le by fastforce 
  with assms(2)[unfolded hoare2_valid_def] obtain t2 p2
    where 2: "(C2, t1)  p2  t2" and q2: "enat p2 + P3 t2  P2 t1" by blast
  with ninfP2 have ninfP3: "P3 t2 < "
    using not_le by fastforce 
  
  from Big_StepT.Seq[OF 1 2] have bigstep: "(C1;; C2, s)  p1 + p2  t2" by simp
  from help1[OF q1 q2] have potential: "enat (p1 + p2) + P3 t2  P1 s" .
  
  show "t p. (C1;; C2, s)  p  t  enat p + P3 t  P1 s " 
    apply(rule exI[where x="t2"])
    apply(rule exI[where x="p1 + p2"]) 
    using bigstep potential by simp  
qed    
    
    
theorem hoare2_sound: "2 {P}c{ Q}    2 {P}c{ Q}"  
proof(induction rule: hoare2.induct) 
  case (Skip P)
  show ?case unfolding hoare2_valid_def apply(safe)
    subgoal for s apply(rule exI[where x=s]) apply(rule exI[where x="Suc 0"])  
      by (auto simp: eSuc_enat_iff eSuc_enat) 
    done
next
  case (Assign P a x)
  show ?case unfolding hoare2_valid_def apply(safe)
    subgoal for s apply(rule exI[where x="s[a/x]"]) apply(rule exI[where x="Suc 0"])  
      by (auto simp: eSuc_enat_iff eSuc_enat) 
    done
next
  case (Seq P1 C1 P2 C2 P3)
  thus ?case using Seq_sound by auto
next
  case (If P b c1 Q c2)
  show ?case  unfolding hoare2_valid_def
  proof (safe)
    fix s
    assume "eSuc (P s) < "
    then have i: "P s < "
      using enat_ord_simps(4) by fastforce  
    show "t p. (IF b THEN c1 ELSE c2, s)  p  t  enat p + Q t  eSuc (P s)"
    proof(cases "bval b s")
      case True
      with i have "P s + emb (bval b s) < " by simp
      with If(3)[unfolded hoare2_valid_def] obtain p t
        where 1: "(c1, s)  p  t" and q: "enat p + Q t  P s + emb (bval b s)"  by blast
      from Big_StepT.IfTrue[OF True 1] have 2: "(IF b THEN c1 ELSE c2, s)  p + 1  t" by simp
      show ?thesis apply(rule exI[where x=t]) apply(rule exI[where x="p+1"])
        apply(safe) apply(fact)
        using q True apply(simp) 
        by (metis eSuc_enat eSuc_ile_mono iadd_Suc) 
    next
      case False
      with i have "P s + emb (~ bval b s) < " by simp
      with If(4)[unfolded hoare2_valid_def] obtain p t
        where 1: "(c2, s)  p  t" and q: "enat p + Q t  P s + emb (~ bval b s)"  by blast
      from Big_StepT.IfFalse[OF False 1] have 2: "(IF b THEN c1 ELSE c2, s)  p + 1  t" by simp
      show ?thesis apply(rule exI[where x=t]) apply(rule exI[where x="p+1"])
        apply(safe) apply(fact)
        using q False apply(simp)
        by (metis eSuc_enat eSuc_ile_mono iadd_Suc)
    qed
  qed
next
  case (conseq P c Q P' Q') 
  show ?case unfolding hoare2_valid_def
  proof (safe)
    fix s
    assume "P' s < "
    with conseq(2) have "P s < "
      using le_less_trans by blast  
    with conseq(4)[unfolded hoare2_valid_def] obtain p t where "(c, s)  p  t" "enat p + Q t  P s" by blast    
    with conseq(2,3) show "t p. (c, s)  p  t  enat p + Q' t  P' s"
      by (meson add_left_mono dual_order.trans) 
  qed
next
  case (While INV b c)  
    
  from While(2)[unfolded hoare2_valid_def]
  have WH2: "s. INV s +  (bval b s) <   (t p. (c, s)  p  t  enat p + INV t + 1  INV s +  (bval b s))"
    by (simp add: add.commute add.left_commute)     
        
  show ?case unfolding hoare2_valid_def
  proof (safe)
    fix s
    assume ninfINV: "INV s + 1 < " 
    then have "INV s < "
      using enat_ord_simps(4) by fastforce 
    then obtain n where i: "INV s = enat n" using not_infinity_eq
      by auto      
    
    text ‹In order to prove validity, we induct on the value of the Invariant, which is a finite number
          and decreases in every loop iteration. For each step we show that validity holds.›
    have "INV s = enat n  t p. (WHILE b DO c, s)  p  t  enat p + (INV t + emb (¬ bval b t))  INV s + 1"
    proof (induct n arbitrary: s rule: less_induct)
      case (less n) 
      show ?case
      proof (cases "bval b s")
        case False
        show ?thesis
          using WhileFalse[OF False] one_enat_def by fastforce
      next
        case True
        ― ‹obtain the loop body from the outer IH›
        with less(2) WH2 obtain t p
          where o: "(c, s)  p  t"
            and q: "enat p + INV t + 1  INV s " by force

        ― ‹prepare premises to ...›
        from q have g: "INV t < INV s"
          using help2 less(2) by metis 
        then have ninfINVt: "INV t < " using less(2)
          using enat_ord_simps(4) by fastforce 
        then obtain n' where i: "INV t = enat n'" using not_infinity_eq
          by auto 
        with less(2) have ii: "n' < n"
          using g by auto
        ― ‹... obtain the tail of the While loop from the inner IH›
        from i ii less(1) obtain t2 p2
          where o2: "(WHILE b DO c, t)  p2  t2"
            and q2: "enat p2 + (INV t2 + emb (¬ bval b t2))  INV t + 1" by blast
        have ende: "~ bval b t2"
          apply(rule ccontr) apply(simp) using q2 ninfINVt
          by (simp add: i one_enat_def) 
            
        ― ‹combine body and tail to one loop unrolling:›
        ― ‹- the Bigstep Semantic›
        from WhileTrue[OF True o o2] have BigStep: "(WHILE b DO c, s)  1 + p + p2  t2" by simp

        ― ‹- the potentialPreservation›       
        from ende q2 have q2': "enat p2 + INV t2  INV t + 1" by simp
        
        have potentialPreservation: "enat (1 + p + p2) + (INV t2 +  (¬ bval b t2))  INV s + 1"     
        proof -
          have "enat (1 + p + p2) + (INV t2 +  (¬ bval b t2))
            = enat (Suc (p + p2)) + INV t2" using ende by simp
          also have " = enat (Suc p) + enat p2 + INV t2" by fastforce
          also have "  enat (Suc p) + INV t + 1" using q2'
            by (metis ab_semigroup_add_class.add_ac(1) add_left_mono) 
          also have "  INV s + 1" using q
            by (metis (no_types, opaque_lifting) add.commute add_left_mono eSuc_enat iadd_Suc plus_1_eSuc(1))
          finally show "enat (1 + p + p2) + (INV t2 +  (¬ bval b t2))  INV s + 1" .
        qed
            
        ― ‹finally combine BigStep Semantic and TimeBound›
        show ?thesis 
          apply(rule exI[where x=t2])
          apply(rule exI[where x= "1 + p + p2"])
          apply(safe)
           by(fact BigStep potentialPreservation)+ 
       qed 
     qed  
    from this[OF i] show "t p. (WHILE b DO c, s)  p  t  enat p + (INV t + emb (¬ bval b t))  INV s + 1" .        
  qed
qed 



  
subsection "Completeness"
    
  
(* the WeakestPrePotential  *)  
definition wp2 :: "com  qassn  qassn" ("wp2") where
"wp2 c Q  =  (λs. (if (t p. (c,s)  p  t  Q t < )  then enat (THE p. t. (c,s)  p  t) + Q (THE t. p. (c,s)  p  t) else ))"

lemma wp2_alt: "wp2 c Q = (λs. (if (c,s) then enat (t (c, s)) + Q (s (c, s)) else ))"
  apply(rule ext) by(auto simp: bigstepT_the_state wp2_def split: if_split)    
    

theorem wp2_is_weakestprePotential: "2 {P}c{Q}  (s. wp2 c Q s  P s)" 
  unfolding  wp2_def hoare2_valid_def
  apply(rule)
  subgoal 
    apply(safe) subgoal for s
      apply(cases "t p. (c, s)  p  t  Q t < ")
        apply(simp) apply auto oops
  
  
lemma wp2_Skip[simp]: "wp2 SKIP Q = (%s. eSuc (Q s))"
  apply(auto intro!: ext simp: wp2_def)
   prefer 2
   apply(simp only: SKIPnot)
   apply(simp)
  apply(simp only: SKIPp SKIPt)
  using one_enat_def plus_1_eSuc(1) by auto    

lemma wp2_Assign[simp]: "wp2 (x ::= e) Q = (λs. eSuc (Q (s(x := aval e s))))"
by (auto intro!: ext simp: wp2_def ASSp ASSt ASSnot eSuc_enat) 

   
  
lemma wp2_Seq[simp]: "wp2 (c1;;c2) Q = wp2 c1 (wp2 c2 Q)"
unfolding wp2_def (* what rule is doing: it uses the extensionality (ext) of functions *)
proof (rule, case_tac "t p. (c1;; c2, s)  p  t  Q t < ", goal_cases)
  case (1 s)
  then obtain u p where ter: "(c1;; c2, s)  p  u" and Q: "Q u < " by blast
  then obtain t p1 p2 where i: "(c1 , s)  p1  t" and ii: "(c2 , t)  p2  u" and p: "p1 + p2 = p" by blast

  from bigstepT_the_state[OF i] have t: "s (c1, s) = t"  
    by blast
  from bigstepT_the_state[OF ii] have t2: "s (c2, t) = u"  
    by blast
  from bigstepT_the_cost[OF i] have firstcost: "t (c1, s) = p1"  
    by blast
  from bigstepT_the_cost[OF ii] have secondcost: "t (c2, t) = p2"  
    by blast
  
  have totalcost: "t(c1;; c2, s) = p1 + p2"
    using bigstepT_the_cost[OF ter] p by auto
  have totalstate: "s(c1;; c2, s) = u"
    using bigstepT_the_state[OF ter] by auto
  
  have c2: "ta p. (c2, t)  p  ta  Q ta < "
    apply(rule exI[where x= u])
    apply(rule exI[where x= p2]) apply safe apply fact+ done
  
  
  have C: "t p. (c1, s)  p  t  (if ta p. (c2, t)  p  ta  Q ta <  then enat (THE p. Ex (big_step_t (c2, t) p)) + Q (THE ta. p. (c2, t)  p  ta) else ) < "
    apply(rule exI[where x=t])
    apply(rule exI[where x=p1])
    apply safe
     apply fact
    apply(simp only: c2 if_True)
    using Q bigstepT_the_state ii by auto
   
  show ?case
    apply(simp only: 1 if_True t t2 c2 C totalcost totalstate firstcost secondcost) by fastforce
next
  case (2 s)
  show ?case apply(simp only: 2 if_False)
    apply auto using 2  
    by force 
qed
   

lemma wp2_If[simp]:
 "wp2 (IF b THEN c1 ELSE c2) Q = (λs. eSuc (wp2 (if bval b s then c1 else c2) Q s))"
  apply (auto simp: wp2_def fun_eq_iff)
  subgoal for x t p i ta ia xa apply(simp only: IfTrue[THEN bigstepT_the_state])
    apply(simp only: IfTrue[THEN bigstepT_the_cost])
    apply(simp only: bigstepT_the_cost bigstepT_the_state)
    by (simp add: eSuc_enat)            
    apply(simp only: bigstepT_the_state bigstepT_the_cost) apply force
   apply(simp only: bigstepT_the_state bigstepT_the_cost)
proof(goal_cases)
  case (1 x t p i ta ia xa)
  note f= IfFalse[THEN bigstepT_the_state, of b x c2 xa ta "Suc xa" c1, simplified, OF 1(4) 1(5)]
  note f2= IfFalse[THEN bigstepT_the_cost, of b x c2 xa ta "Suc xa" c1, simplified, OF 1(4) 1(5)]
  note g= bigstep_det[OF 1(1) 1(5)]
  show ?case
    apply(simp only: f f2) using 1 g
    by (simp add: eSuc_enat)   
next
  case 2
  then 
  show ?case
    apply(simp only: bigstepT_the_state bigstepT_the_cost)  apply force done
qed
 

lemma assumes b: "bval b s"
  shows wp2WhileTrue: " wp2 c (wp2 (WHILE b DO c) Q) s  + 1  wp2 (WHILE b DO c) Q s"
proof (cases "t p. (WHILE b DO c, s)  p  t  Q t < ")
  case True
  then obtain t p where w: "(WHILE b DO c, s)  p  t" and q: "Q t < " by blast
  from b w obtain p1 p2 t1 where c: "(c, s)  p1  t1" and w': "(WHILE b DO c, t1)  p2  t" and sum: "1 + p1 + p2 = p"
    by auto 
  have g: "ta p. (WHILE b DO c, t1)  p  ta  Q ta < "
    apply(rule exI[where x="t"])
    apply(rule exI[where x="p2"])
      apply safe apply fact+ done
    
  have h: "t p. (c, s)  p  t  (if ta p. (WHILE b DO c, t)  p  ta  Q ta <  then enat (THE p. Ex (big_step_t (WHILE b DO c, t) p)) + Q (THE ta. p. (WHILE b DO c, t)  p  ta) else ) < "
    apply(rule exI[where x="t1"])
    apply(rule exI[where x="p1"])
    apply safe apply fact
    apply(simp only: g if_True) using   bigstepT_the_state bigstepT_the_cost w' q by(auto)
  
  have "wp2 c (wp2 (WHILE b DO c) Q) s + 1 = enat p + Q t"
    unfolding wp2_def apply(simp only: h if_True)
    apply(simp only: bigstepT_the_state[OF c] bigstepT_the_cost[OF c] g if_True bigstepT_the_state[OF w'] bigstepT_the_cost[OF w']) using sum
    by (metis One_nat_def ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral eSuc_enat plus_1_eSuc(2) plus_enat_simps(1)) 
  also have " = wp2 (WHILE b DO c) Q s"
    unfolding wp2_def apply(simp only: True if_True)
    using bigstepT_the_state bigstepT_the_cost w apply(simp) done
  finally show ?thesis by simp
next
  case False
  have "wp2 (WHILE b DO c) Q s = "
    unfolding wp2_def 
    apply(simp only: False if_False) done
  then show ?thesis by auto
qed

lemma assumes b: "bval b s"
shows wp2WhileTrue': "wp2 c (wp2 (WHILE b DO c) Q) s  + 1 = wp2 (WHILE b DO c) Q s"
proof (cases "p t. (WHILE b DO c, s)  p  t")
  case True
  then obtain t p where w: "(WHILE b DO c, s)  p  t"  by blast
  from b w obtain p1 p2 t1 where c: "(c, s)  p1  t1" and w': "(WHILE b DO c, t1)  p2  t" and sum: "1 + p1 + p2 = p"
    by auto 
  then have z: " (c, s)" and z2: " (WHILE b DO c, t1)" by auto 
  
  have "wp2 c (wp2 (WHILE b DO c) Q) s + 1 = enat p + Q t"
    unfolding wp2_alt apply(simp only: z if_True)
    apply(simp only: bigstepT_the_state[OF c] bigstepT_the_cost[OF c] z2 if_True bigstepT_the_state[OF w'] bigstepT_the_cost[OF w'])
      using sum
    by (metis One_nat_def ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral eSuc_enat plus_1_eSuc(2) plus_enat_simps(1)) 
  also have " = wp2 (WHILE b DO c) Q s"
    unfolding wp2_alt apply(simp only: True if_True)
    using bigstepT_the_state bigstepT_the_cost w apply(simp) done
  finally show ?thesis by simp
next
  case False
  have "¬ ( (WHILE b DO c, s(c,s))   (c, s))"
  proof (rule)
    assume P: " (WHILE b DO c, s (c, s))   (c, s)"
    then obtain t s' where A: "(c,s)  t  s'" by blast 
    with A P have " (WHILE b DO c, s')" using bigstepT_the_state by auto
    then obtain t' s'' where B: "(WHILE b DO c,s')  t'  s''" by auto
    have "(WHILE b DO c, s)  1+t+t'  s''" apply(rule WhileTrue) using b A B by auto
    then have " (WHILE b DO c, s)" by auto
    thus "False" using False by auto
  qed
  then have "¬ (WHILE b DO c, s(c,s))  ¬ (c, s)" by simp 
  
  then show ?thesis apply rule
    subgoal unfolding wp2_alt apply(simp only: if_False False) by auto
    subgoal unfolding wp2_alt apply(simp only: if_False False) by auto
  done
qed
  
  
lemma assumes b: "~ bval b s"
  shows wp2WhileFalse: " Q s  + 1  wp2 (WHILE b DO c) Q s"
proof (cases "t p. (WHILE b DO c, s)  p  t  Q t < ")
  case True
  with b obtain t p where w: "(WHILE b DO c, s)  p  t" and "Q t < " by blast
  with b have c: "s=t" "p=Suc 0" by auto
  have " wp2 (WHILE b DO c) Q s =  Q s  + 1"
    unfolding wp2_def apply(simp only: True if_True)
    using w c bigstepT_the_cost bigstepT_the_state by(auto simp add: one_enat_def)  
  then show ?thesis by auto
next
  case False
  have "wp2 (WHILE b DO c) Q s = "
    unfolding wp2_def 
    apply(simp only: False if_False) done
  then show ?thesis by auto
qed 
    
lemma thet_WhileFalse: "~ bval b s  t (WHILE b DO c, s) = 1" by auto 
lemma thes_WhileFalse: "~ bval b s  s (WHILE b DO c, s) = s" by auto 
  
lemma assumes b: "~ bval b s"
  shows wp2WhileFalse': "Q s  + 1 = wp2 (WHILE b DO c) Q s"
proof - 
  from b have T: " (WHILE b DO c, s)" by auto      
  show ?thesis unfolding wp2_alt using b apply(simp only: T if_True)
      by(simp add: thet_WhileFalse thes_WhileFalse one_enat_def) 
qed 
  
  
(* note that ≤ is sufficient for the completness proof *)
lemma wp2While: "(if bval b s then wp2 c (wp2 (WHILE b DO c) Q) s else Q s) + 1 = wp2 (WHILE b DO c) Q s"  
  apply(cases "bval b s")      
  using wp2WhileTrue' apply simp
  using wp2WhileFalse' apply simp   done 
    
 
  
lemma assumes "Q. 2 {wp2 c Q} c {Q}"
  shows  "2 {wp2 (WHILE b DO c) Q} WHILE b DO c {Q}"
proof -
  let ?I = "%s. (if bval b s then wp2 c (wp2 (WHILE b DO c) Q) s else Q s)"
  from assms[of "wp2 (WHILE b DO c) Q"]
  have A: " 2 {wp2 c (wp2 (WHILE b DO c) Q)} c {wp2 (WHILE b DO c) Q}" .
  have B: "2 {λs. (?I s) +  (bval b s)} c {λt. (?I t) + 1}"
    apply(rule conseq)
      apply(rule A)
     apply simp
      using wp2While apply simp done
  from hoare2.While[where I="?I"]
  have C: "2 {λs. (?I s) +  (bval b s)} c {λt. (?I t) + 1} 
          2 {λs. (?I s) + 1} WHILE b DO c {λs. (?I s) +  (¬ bval b s)}" by simp
  from C[OF B] have D: "2 {λs. (?I s) + 1} WHILE b DO c {λs. (?I s) +  (¬ bval b s)}" .                           
  show "2 {wp2 (WHILE b DO c) Q} WHILE b DO c {Q}"
    apply(rule conseq)
      apply(rule D)
    using wp2While apply simp
      apply simp  done
qed
                            

lemma wp2_is_pre: "2 {wp2 c Q} c { Q}"
proof (induction c arbitrary: Q)
  case SKIP show ?case by (auto intro: hoare2.Skip)
next
  case Assign show ?case by (auto intro:hoare2.Assign)
next
  case Seq thus ?case by (auto intro:hoare2.Seq)
next 
  case (If x1 c1 c2 Q) thus ?case
    apply (auto intro!: hoare2.If )  
     apply(rule hoare2.conseq) 
       apply(auto)
     apply(rule hoare2.conseq) 
      apply(auto)
    done
next
  case (While b c)   
  show ?case
    apply(rule conseq)       
      apply(rule hoare2.While[where I="%s. (if bval b s then wp2 c (wp2 (WHILE b DO c) Q) s else Q s)"])       
      apply(rule conseq)        
        apply(rule While[of "wp2 (WHILE b DO c) Q"])      
    using wp2While by auto       
qed
  
  
  
lemma wp2_is_weakestprePotential1: "2 {P}c{Q}  (s. wp2 c Q s  P s)" 
apply(auto simp: hoare2_valid_def wp2_def)
proof (goal_cases)
  case (1 s t p i) 
  show ?case
  proof(cases "P s < ")
    case True
    with 1(1) obtain t p' where i: "(c, s)  p'  t" and ii: "enat p' + Q t  P s"
      by auto    
    show ?thesis apply(simp add: bigstepT_the_state[OF i] bigstepT_the_cost[OF i] ii) done
  qed simp  
qed force
  
lemma wp2_is_weakestprePotential2: "(s. wp2 c Q s  P s)  2 {P}c{Q}" 
apply(auto simp: hoare2_valid_def wp2_def)
proof (goal_cases)
  case (1 s i)
  then have A: "(if t. (p. (c, s)  p  t)  (i. Q t = enat i) then enat (THE p. Ex (big_step_t (c, s) p)) + Q (THE t. p. (c, s)  p  t) else )  P s"
    by fast 
  show ?case
  proof (cases "t. (p. (c, s)  p  t)  (i. Q t = enat i)")
    case True
    then obtain t p where i: "(c, s)  p  t" by blast
    from True A have "enat p + Q t  P s" by (simp add: bigstepT_the_cost[OF i] bigstepT_the_state[OF i])
    then have "(c, s)  p  t  enat p + Q t  enat i" using 1(2) i by simp
    then show ?thesis by auto
  next
    case False
    with A have "P s  " by auto 
    then show ?thesis using 1 by auto
  qed   
qed
          
theorem wp2_is_weakestprePotential: "(s. wp2 c Q s  P s)  2 {P}c{Q}" 
 using   wp2_is_weakestprePotential2  wp2_is_weakestprePotential1 by metis

   
   
theorem hoare2_complete: "2 {P}c{Q}  2 {P}c{ Q}"  
apply(rule conseq[OF wp2_is_pre, where Q'=Q and Q=Q, simplified]) 
using wp2_is_weakestprePotential1 by blast

 


corollary hoare2_sound_complete: " 2 {P}c{Q}  2 {P}c{ Q}"
by (metis hoare2_sound hoare2_complete)



end