Theory QuantK_Hoare

section ‹Quantitative Hoare Logic (big-O style)›

theory QuantK_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 "Definition of Validity"
  
(* this definition refines the normal Hoare Triple Validity *)
definition hoare2o_valid :: "qassn  com  qassn  bool"
  ("2'' {(1_)}/ (_)/ {(1_)}" 50) where
"2' {P} c {Q}    (k>0. (s.  P s <   (t p. ((c,s)  p  t)  enat k * P s  p + enat k * Q t)))"


subsection "Hoare Rules"

inductive
  hoareQ :: "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  enat k *  P' s ; s. enat k * Q' s  Q s; k>0  
           2' {P'}c{ Q'}" 
  
text ‹Derived Rules›

lemma const: " 2' {λs. enat k * P s}c{λs. enat k * Q s};  k>0  
           2' {P}c{ Q}" 
  apply(rule conseq) by auto

inductive
  hoareQ' :: "qassn  com  qassn  bool" ("Z ({(1_)}/ (_)/ {(1_)})" 50)
where

ZSkip:  "Z {%s. eSuc (P s)} SKIP {P}"  |

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

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

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

Zconseq': " Z {P}c{Q} ; s. P s   P' s ; s. Q' s  Q s  
           Z {P'}c{ Q'}"   |
   
Zconst:  " Z {λs. enat k * P s}c{λs. enat k * Q s};  k>0  
           Z {P}c{ Q}"  
    

lemma Zconseq: " Z {P}c{Q} ; s. P s  enat k *  P' s ; s. enat k * Q' s  Q s; k>0  
           Z {P'}c{ Q'}"
  apply(rule Zconst[of k P' c Q'])
  apply(rule Zconseq'[where P=P and Q=Q]) by auto
    
    
lemma ZQ: " Z { P } c { Q }   2' { P } c { Q }"
  apply(induct rule: hoareQ'.induct) 
    apply (auto simp: hoareQ.Skip  hoareQ.Assign hoareQ.If hoareQ.Seq hoareQ.While) 
    subgoal using conseq[where k=1] using one_enat_def by auto  
    subgoal for k P c Q  using const by auto  
    done
lemma QZ: " 2' { P } c { Q }   Z { P } c { Q }"
  apply(induct rule: hoareQ.induct) 
    apply (auto simp: ZSkip  ZAssign ZIf ZSeq ZWhile ) 
    using Zconseq by blast 
      
lemma QZ_iff:  "2' { P } c { Q }   Z { P } c { Q }"   
using ZQ QZ by metis      

  
subsection "Soundness"

lemma enatSuc0[simp]: "enat (Suc 0) * x = x"
  using one_enat_def by auto 
 
    
theorem hoareQ_sound: "2' {P}c{ Q}    2' {P}c{ Q}"
apply(unfold hoare2o_valid_def)
proof(  induction  rule: hoareQ.induct)
  case (Skip P)
  show ?case apply(rule exI[where x=1]) apply(auto)
    subgoal for s apply(rule exI[where x=s]) apply(rule exI[where x="Suc 0"])  
      apply safe 
      apply fast    
      by (metis add.left_neutral add.right_neutral eSuc_enat iadd_Suc le_iff_add zero_enat_def)
    done
next
  case (Assign P a x)
  show ?case apply(rule exI[where x=1])   apply(auto)
    subgoal for s apply(rule exI[where x="s[a/x]"]) apply(rule exI[where x="Suc 0"]) 
      apply safe 
      apply fast
      by (metis add.left_neutral add.right_neutral  eSuc_enat iadd_Suc le_iff_add zero_enat_def)      
    done
next
  case (Seq P1 C1 P2 C2 P3)
  from Seq(3) obtain k1 where Seq3: "s. P1 s <   (t p. (C1, s)  p  t  enat p + enat k1 * P2 t  enat k1 * P1 s)" and 10: "k1>0" by blast
  from Seq(4) obtain k2 where Seq4: "s. P2 s <   (t p. (C2, s)  p  t  enat p + enat k2 * P3 t  enat k2 * P2 s)" and 20: "k2>0" by blast
  let ?k = "lcm k1 k2" (* or k1*k2 *)
  show ?case apply(rule exI[where x="?k"])
  proof (safe)
    from 10 20 show "lcm k1 k2>0" by (auto simp: lcm_pos_nat)
    fix s
    assume ninfP1: "P1 s < "
    with Seq3 obtain t1 p1 where 1: "(C1, s)  p1  t1" and q1: "enat p1 + k1 * P2 t1  k1 * P1 s" by blast
    with ninfP1 have ninfP2: "P2 t1 < "
      using not_le 10 by fastforce 
    with Seq4 obtain t2 p2 where 2: "(C2, t1)  p2  t2" and q2: "enat p2 + k2 * P3 t2  k2 * P2 t1" by blast
    with ninfP2 have ninfP3: "P3 t2 < "
      using not_le 20  by fastforce 
    then obtain u2 where u2: "P3 t2 = enat u2" by auto
    from ninfP2 obtain u1 where u1: "P2 t1 = enat u1" by auto
    from ninfP1 obtain u0 where u0: "P1 s = enat u0" by auto
    
    from Big_StepT.Seq[OF 1 2] have 12: "(C1;; C2, s)  p1 + p2  t2" by simp
    
    have i: "(C1;; C2, s)  p1+p2  t2" using 1 and 2 by auto
    
    from 10 20 have p: "k1 div gcd k1 k2 > 0" "k2 div gcd k1 k2 > 0" by (simp_all add: Divides.div_positive)
        
    have za: "?k = (k1 div gcd k1 k2) * k2" 
      apply(simp only: lcm_nat_def)
      by (simp add: dvd_div_mult)
        
    have za2: "?k = (k2 div gcd k1 k2) * k1" 
      apply(simp only: lcm_nat_def)
      by (metis dvd_div_mult gcd_dvd2 mult.commute)
        
    from q1[unfolded u1 u2 u0] have z: "p1 + k1 * u1  k1 * u0" by auto
    from q2[unfolded u1 u2 u0] have y: "  p2 + k2 *   u2  k2 *   u1" by auto
    have "p1+p2 + ?k * u2  p1 + (k1 div gcd k1 k2)*p2  + ?k * u2  " using p by simp
    also have "  (k2 div gcd k1 k2)*p1 + (k1 div gcd k1 k2)*p2  + ?k * u2  " using p by simp                                      
    also have " = (k2 div gcd k1 k2)*p1 + (k1 div gcd k1 k2)*(p2 + k2* u2)"
      apply(simp only: za) by algebra  
    also have "  (k2 div gcd k1 k2)*p1 + (k1 div gcd k1 k2)*(k2 *   u1)" using y
      by (metis add_left_mono distrib_left le_iff_add)   
    also have " = (k2 div gcd k1 k2)*p1 + ?k * u1" by(simp only: za)
    also have " = (k2 div gcd k1 k2)*p1 + (k2 div gcd k1 k2) *(k1* u1)" by(simp only: za2)
    also have "  (k2 div gcd k1 k2)*(p1 + k1*u1)"
      by (simp add: distrib_left)
    also have "  (k2 div gcd k1 k2)*(k1 * u0)" using z  
      by fastforce
    also have "  ?k * u0" by(simp only: za2)
    finally   
    have "p1+p2 + ?k * u2  ?k * u0" .
    then have ii: "enat (p1+p2) + ?k * P3 t2  ?k * P1 s" 
      unfolding u0 u2  by auto
        
    from i ii show "t p. (C1;; C2, s)  p  t  enat p + ?k * P3 t  ?k * P1 s " by blast 
  qed  
next
  case (If P b c1 Q c2)
  from If(3) obtain kT where If3: "s. P s +  (bval b s) <   (t p. (c1, s)  p  t  enat p + enat kT * Q t  enat kT * (P s +  (bval b s))) " and T: "kT > 0" by blast
  from If(4) obtain kF where If4: "s. P s +  (¬ bval b s) <   (t p. (c2, s)  p  t  enat p + enat kF * Q t  enat kF * (P s +  (¬ bval b s)))" and F: "kF > 0" by blast
  show ?case apply(rule exI[where x="kT*kF"])
  proof (safe)
    from T F show "0 < kT * kF" by auto
    fix s
    assume "eSuc (P s) < "
    then have i: "P s < "
      using enat_ord_simps(4) by fastforce  
    then obtain u0 where u0: "P s = enat u0" by auto
    show "t p. (IF b THEN c1 ELSE c2, s)  p  t  enat p + enat (kT * kF) * Q t  enat (kT * kF) * eSuc (P s)"
    proof(cases "bval b s")
      case True
      with i have "P s + emb (bval b s) < " by simp
      with If3 obtain p t where 1: "(c1, s)  p  t" and q: "enat p + enat kT * Q t  enat kT * (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
           
      from q have "Q t < " using i T True
        using less_irrefl by fastforce
      then obtain u1 where u1: "Q t = enat u1" by auto 
      from q True have q': "p + kT * u1  kT * u0" unfolding u0 u1 by auto
      have "(p+1) +  (kT * kF) * u1  kF*(p+1) + (kT * kF) * u1" using F 
        by (simp add: mult_eq_if)
      also have "  kF*(p+1  + kT  * u1)"
        by (simp add: add_mult_distrib2)  
      also have "  kF*(1  + kT  * u0)"
        using q' by auto
      also have "  (kT * kF) * Suc u0" using T by simp
      finally 
      have " (p+1) +  (kT * kF) * u1   (kT * kF) * Suc u0" .
      then have 1: "enat (p+1) + enat (kT * kF) * Q t  enat (kT * kF) * eSuc (P s)"
        unfolding u1 u0 by (simp add: eSuc_enat) 
      from 1 2 show ?thesis by metis 
    next
      case False
      with i have "P s + emb (~bval b s) < " by simp
      with If4 obtain p t where 1: "(c2, s)  p  t" and q: "enat p + enat kF * Q t  enat kF * (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
           
      from q have "Q t < " using i F False
        using less_irrefl by fastforce
      then obtain u1 where u1: "Q t = enat u1" by auto 
      from q False have q': "p + kF * u1  kF * u0" unfolding u0 u1 by auto
      have "(p+1) +  (kF * kT) * u1  kT*(p+1) + (kF * kT) * u1" using T 
        by (simp add: mult_eq_if)
      also have "  kT*(p+1  + kF  * u1)"
        by (simp add: add_mult_distrib2)  
      also have "  kT*(1  + kF  * u0)"
        using q' by auto
      also have "  (kF * kT) * Suc u0" using F by simp
      finally 
      have " (p+1) +  (kT * kF) * u1   (kT * kF) * Suc u0"
        by (simp add: mult.commute) 
      then have 1: "enat (p+1) + enat (kT * kF) * Q t  enat (kT * kF) * eSuc (P s)"
        unfolding u1 u0 by (simp add: eSuc_enat) 
      from 1 2 show ?thesis by metis 
    qed
  qed
next
  case (conseq P c Q k1 P' Q') 
  from conseq(5) obtain k where c4: "s. P s <   (t p. (c, s)  p  t  enat p + enat k * Q t  enat k * P s)" and 0: "k>0" by blast
  show ?case apply(rule exI[where x="k*k1"])
  proof (safe)
    show "k*k1>0" using 0 conseq(4) by auto
    fix s
    assume "P' s < "
    with conseq(2,4)  have "P s < "
      using le_less_trans
      by (metis enat.distinct(2) enat_ord_simps(4) imult_is_infinity)  
    with c4 obtain p t where 1: "(c, s)  p  t" and 2: "enat p + enat k * Q t  enat k * P s" by blast   
               
    have "enat p + enat (k*k1) * Q' t = enat p + enat (k) * ( (enat k1) * Q' t)"
      by (metis mult.assoc times_enat_simps(1))       
    also have "  enat p + enat (k) * Q t" using conseq(3)
      by (metis add_left_mono distrib_left le_iff_add)  
    also have "  enat k * P s" using 2 by auto
    also have "  enat (k*k1)  * P' s" using conseq(2)
      by (metis mult.assoc mult_left_mono not_less not_less_zero times_enat_simps(1))
    finally have 2: "enat p + enat (k*k1) * Q' t  enat (k*k1) * P' s"
      by auto
    from 1 2 show "t p. (c, s)  p  t  enat p + (k*k1) * Q' t  (k*k1) * P' s" by auto
  qed
next
  case (While INV b c)  
  then obtain k where W2: "s. INV s +  (bval b s) <   (t p. (c, s)  p  t  enat p + enat k * (INV t + 1)  enat k * (INV s +  (bval b s)))" and g0: "k>0"
    by blast
  show ?case apply(rule exI[where x=k])
  proof (safe)
    show "0<k" by fact
    fix s
    assume ninfINV: "INV s + 1 < " 
    then have f: "INV s < "
      using enat_ord_simps(4) by fastforce 
    then obtain n where i: "INV s = enat n" using not_infinity_eq
      by auto      
    
    have "INV s = enat n  t p. (WHILE b DO c, s)  p  t  enat p + enat k * (INV t + emb (¬ bval b t))  enat k * (INV s + 1)"
    proof (induct n arbitrary: s rule: less_induct)
      case (less n) 
      
      then show ?case 
      proof (cases "bval b s")
        case False
        show ?thesis
            apply(rule exI[where x="s"])
          apply(rule exI[where x="Suc 0"])
          apply safe
           apply (fact WhileFalse[OF False])
          using False 
          apply (simp add: one_enat_def) using g0
          by (metis One_nat_def Suc_ile_eq add.commute add_left_mono distrib_left enat_0_iff(2) mult.right_neutral not_gr_zero one_enat_def)    
      next
        case True
        with less(2) W2 have "(t p. (c, s)  p  t  enat p + enat k * (INV t + 1)  enat k * INV s )"
          by force  
        then obtain t p where o: "(c, s)  p  t" and q: "enat p + enat k * (INV t + 1)  enat k * INV s " by auto
        from o bigstep_progress have p: "p > 0" by blast
             
            
        from q  have pf: "enat k * (INV t + 1)  enat k * INV s"
          using dual_order.trans by fastforce
        then have "INV t < " using less(2) 
          using g0 not_le by fastforce 
        then obtain invt where invt: "INV t = enat invt" by auto
        from pf g0 have g: "INV t  < INV s"
          unfolding less(2) invt
          by (metis (full_types) Suc_ile_eq add.commute eSuc_enat enat_ord_simps(1) nat_mult_le_cancel_disj plus_1_eSuc(1) times_enat_simps(1))
              
              
        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
        from i ii less(1) obtain t2 p2 where o2: "(WHILE b DO c, t)  p2  t2" and q2: "enat p2 + enat k * (INV t2 + emb (¬ bval b t2))  enat k * ( INV t + 1)" by blast
        have ende: "~ bval b t2"
          apply(rule ccontr) apply(simp) using q2 g0 ninfINVt
          by (simp add: i one_enat_def) 
        from WhileTrue[OF True o o2] have "(WHILE b DO c, s)  1 + p + p2  t2" by simp
       
        from ende q2 have q2': "enat p2 + enat k * INV t2  enat k * (INV t + 1)" by simp
        
        show ?thesis 
          apply(rule exI[where x=t2])
          apply(rule exI[where x= "1 + p + p2"])
          apply(safe)
           apply(fact)
          using ende apply(simp)
        proof -
          have "enat (Suc (p + p2)) +  enat k * INV t2 = enat (Suc p) + enat p2 +  enat k * INV t2" by fastforce
          also have "  enat (Suc p) + enat k * (INV t + 1)" using q2'
            by (metis ab_semigroup_add_class.add_ac(1) add_left_mono) 
          also have "  1 + enat k * (INV s)" using q
            by (metis (no_types, opaque_lifting) add.commute add_left_mono eSuc_enat iadd_Suc plus_1_eSuc(1))
          also have "  enat k + enat k * (INV s)" using g0
            by (simp add: Suc_leI one_enat_def) 
          also have "   enat k * (INV s + 1)"
            by (simp add: add.commute distrib_left)
          finally show "enat (Suc (p + p2)) +  enat k * INV t2   enat k * (INV s + 1)" .
          qed
        qed 
      qed
        
    from this[OF i] show "t p. (WHILE b DO c, s)  p  t  enat p + enat k * (INV t + emb (¬ bval b t))  enat k * (INV s + 1)" .
        
  qed
qed 

  
lemma conseq':
  " 2' {P} c {Q} ;  s. P s  P' s; s. Q' s  Q s    2' {P'} c {Q'}"
  apply(rule conseq[where k=1]) by auto

lemma strengthen_pre:
  " s. P s  P' s;  2' {P} c {Q}   2' {P'} c {Q}"
  apply(rule conseq[where k=1 and Q'=Q and Q=Q]) by auto

lemma weaken_post:
  " 2' {P} c {Q};  s. Q s  Q' s    2' {P} c {Q'}"
  apply(rule conseq[where k=1]) by auto 

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

  
subsection "Completeness"
    
lemma bigstep_det: "(c1, s)  p1  t1  (c1, s)  p  t  p1=p  t1=t"
  using big_step_t_determ2 by simp

lemma bigstepT_the_cost: "(c, s)  P  T  (THE n. a. (c, s)  n  a) = P"
  using bigstep_det by blast 

lemma bigstepT_the_state: "(c, s)  P  T  (THE a. n. (c, s)  n  a) = T"
  using bigstep_det by blast 


lemma SKIPnot: "(¬ (SKIP, s)  p  t) = (st  pSuc 0)" by blast

 
lemma SKIPp: "(THE p. t. (SKIP, s)  p  t) = Suc 0"
  apply(rule the_equality)
  apply fast
  apply auto done 

lemma SKIPt: "(THE t. p. (SKIP, s)  p  t) = s"
  apply(rule the_equality)
  apply fast
  apply auto done 


lemma ASSp: "(THE p. Ex (big_step_t (x ::= e, s) p)) = Suc 0"
  apply(rule the_equality)
  apply fast
  apply auto done 

lemma ASSt: "(THE t. p. (x ::= e, s)  p  t) = s(x := aval e s)"
  apply(rule the_equality)
  apply fast
  apply auto done 

lemma ASSnot: "( ¬ (x ::= e, s)  p  t ) = (pSuc 0  ts(x := aval e s))"
  apply auto done

text‹
The completeness proof proceeds along the same lines as the one for partial
correctness. First we have to strengthen our notion of weakest precondition
to take termination into account:›

definition wpQ :: "com  qassn  qassn" ("wpQ") where
"wpQ 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 wpQ_skip[simp]: "wpQ SKIP Q = (%s. eSuc (Q s))"
  apply(auto intro!: ext simp: wpQ_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 wpQ_ass[simp]: "wpQ (x ::= e) Q = (λs. eSuc (Q (s(x := aval e s))))"
by (auto intro!: ext simp: wpQ_def ASSp ASSt ASSnot eSuc_enat) 

lemma wpt_Seq[simp]: "wpQ (c1;;c2) Q = wpQ c1 (wpQ c2 Q)"
unfolding wpQ_def
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: "(THE t. p. (c1, s)  p  t) = t"  
    by blast
  from bigstepT_the_state[OF ii] have t2: "(THE u. p. (c2, t)  p  u) = u"  
    by blast
  from bigstepT_the_cost[OF i] have firstcost: "(THE p. t. (c1, s)  p  t) = p1"  
    by blast
  from bigstepT_the_cost[OF ii] have secondcost: "(THE p. u. (c2, t)  p  u) = p2"  
    by blast
  
  have totalcost: "(THE p. Ex (big_step_t (c1;; c2, s) p)) = p1 + p2"
    using bigstepT_the_cost[OF ter] p by auto
  have totalstate: "(THE t. p. (c1;; c2, s)  p  t) = 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 wpQ_If[simp]:
 "wpQ (IF b THEN c1 ELSE c2) Q = (λs. eSuc (wpQ (if bval b s then c1 else c2) Q s))"
  apply (auto simp: wpQ_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 hoareQ_inf: "2' {%s. } c { Q}"
  apply (induction c arbitrary: Q)
  apply(auto intro: hoareQ.Skip hoareQ.Assign hoareQ.Seq hoareQ.conseq)
  subgoal apply(rule hoareQ.conseq) apply(rule hoareQ.If[where P="%s. "]) by(auto intro: hoareQ.If hoareQ.conseq)
  subgoal apply(rule hoareQ.conseq) apply(rule hoareQ.While[where I="%s. "]) apply(rule hoareQ.conseq) by auto 
  done

lemma assumes b: "bval b s"
  shows wpQ_WhileTrue: " wpQ c (wpQ (WHILE b DO c) Q) s  + 1  wpQ (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 "wpQ c (wpQ (WHILE b DO c) Q) s + 1 = enat p + Q t"
    unfolding wpQ_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 " = wpQ (WHILE b DO c) Q s"
    unfolding wpQ_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 "wpQ (WHILE b DO c) Q s = "
    unfolding wpQ_def 
    apply(simp only: False if_False) done
  then show ?thesis by auto
qed

lemma assumes b: "~ bval b s"
  shows wpQ_WhileFalse: " Q s  + 1  wpQ (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 " wpQ (WHILE b DO c) Q s =  Q s  + 1"
    unfolding wpQ_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 "wpQ (WHILE b DO c) Q s = "
    unfolding wpQ_def 
    apply(simp only: False if_False) done
  then show ?thesis by auto
qed 
                            

lemma wpQ_is_pre: "2' {wpQ c Q} c { Q}"
proof (induction c arbitrary: Q)
  case SKIP show ?case apply (auto intro: hoareQ.Skip) done
next
  case Assign show ?case apply (auto intro:hoareQ.Assign) done
next
  case Seq thus ?case by (auto intro:hoareQ.Seq)
next 
  case (If x1 c1 c2 Q) thus ?case
    apply (auto intro!: hoareQ.If )  
     apply(rule hoareQ.conseq) 
       apply(auto)
     apply(rule hoareQ.conseq) 
      apply(auto)
    done
next
  case (While b c)   
  show ?case
      apply(rule conseq[where k=1])   
      apply(rule hoareQ.While[where I="%s. (if bval b s then  wpQ c (wpQ (WHILE b DO c) Q) s else Q s)"])
      apply(rule conseq[where k=1])  
        apply(rule While[of "wpQ (WHILE b DO c) Q"])
       apply(case_tac "bval b s")  
        apply(simp) apply(simp)
      subgoal for s
        apply(cases "bval b s")
        using wpQ_WhileTrue apply simp
        using wpQ_WhileFalse apply simp done
        apply simp
      subgoal for s
        apply(cases "bval b s")
        using wpQ_WhileTrue apply simp
        using wpQ_WhileFalse apply simp done 
       apply(case_tac "bval b s")  
        apply(simp) apply(simp)
        apply simp done  
qed
  
  
lemma wpQ_is_pre': "2' {wpQ c (%s. enat k * Q s )} c {(%s. enat k * Q s )}"  
  using wpQ_is_pre by blast 
    
lemma wpQ_is_weakestprePotential1: "2' {P}c{Q}  (k>0. s. wpQ c (%s. enat k* Q s) s  enat k * P s)" 
apply(auto simp: hoare2o_valid_def wpQ_def)
proof (goal_cases)
  case (1 k) 
  show ?case 
  proof (rule exI[where x=k], safe)
    show "0<k" by fact
  next
    fix s t p i
    assume "(c, s)  p  t" "enat k * Q t = enat i"
    
    show "enat (t (c, s)) + enat k * Q (s (c, s))  enat k * P s"
    proof (cases "P s < ") 
      case True
      with 1 obtain t p' where i: "(c, s)  p'  t" and ii: "enat p' + enat k *  Q t  enat k * P s"
        by auto    
      show ?thesis by(simp add: bigstepT_the_state[OF i] bigstepT_the_cost[OF i] ii)
    next
      case False
      then show ?thesis
        using 1 by auto 
    qed  
  next
    fix s
    assume "t. (p. ¬ (c, s)  p  t)  enat k * Q t = "
    then show "enat k * P s = " using 1 by force
  qed
qed   

theorem hoareQ_complete: "2' {P}c{Q}  2' {P}c{ Q}" 
proof -
  assume "2' {P}c{Q}"
  with wpQ_is_weakestprePotential1 obtain k where "k>0" 
    and 1: "s. wpQ c (λs. enat k * Q s) s  enat k * P s" by blast
  show "2' {P}c{Q}"
    apply(rule conseq[OF wpQ_is_pre'])
    apply(fact 1)
     apply simp by fact
qed
    
theorem hoareQ_complete': "2' {P}c{Q}  2' {P}c{ Q}"  
  unfolding hoare2o_valid_def
proof -
  assume "k>0. s. P s <   (t p. (c, s)  p  t  enat p + enat k * Q t  enat k * P s)"
  then obtain k where f: "s. P s <   (t p. (c, s)  p  t  enat p + enat k * Q t  enat k * P s)" and k: "k>0" by auto
  
  show "2' {P}c{ Q}"
    apply(rule conseq[OF wpQ_is_pre', where Q'=Q, simplified, where k1=k and k=k and Q1=Q])
    unfolding  wpQ_def
    subgoal for s
      proof(cases "P s < ") 
        case True
        with f obtain t p' where i: "(c, s)  p'  t" and ii: "enat p' + enat k * Q t  enat k * P s"
          by auto    
        from ii k True have iii: "enat k * Q t < "
          using imult_is_infinity by fastforce 
        have kla: "t p. (c, s)  p  t  enat k * Q t < "
          using iii i by auto
        show ?thesis unfolding bigstepT_the_state[OF i]
            unfolding bigstepT_the_cost[OF i] 
            apply(simp only: kla) using ii by simp
      next
        case False
        then show ?thesis using k by auto
      qed   
    subgoal by auto 
    using k by auto  
qed 

corollary hoareQ_sound_complete: " 2' {P}c{Q}  2' {P}c{ Q}"
  by (metis hoareQ_sound hoareQ_complete)
  
subsection "Example"
 
lemma fixes X::int assumes "0 < X" shows  
 Z: "eSuc (enat (nat (2 * X) * nat (2 * X)))  enat (5 * (nat (X * X)))"
proof -
  from assms have nn: "0  X" by auto
  from assms have "0 < nat X" by auto 
  then have "0 < enat (nat X)" by (simp add: zero_enat_def)  
  then have A: "eSuc 0  enat (nat X)" using ileI1
    by blast
      
  have " (nat X)   (nat (X*X))"  using nn nat_mult_distrib  by auto
  then have D: "enat (nat X)  enat (nat (X*X))"    by auto
      
  have C: "(enat (nat (2 * X) * nat (2 * X))) = 4* enat (nat (X * X))"   
    using nn nat_mult_distrib
    by (simp add: numeral_eq_enat)    
  have "eSuc (enat (nat (2 * X) * nat (2 * X)))
    = eSuc 0 +  (enat (nat (2 * X) * nat (2 * X)))"
    using one_eSuc plus_1_eSuc(1) by auto
  also have "  enat (nat X) +  (enat (nat (2 * X) * nat (2 * X)))"
    using A  add_right_mono by blast  
  also have "  enat (nat X) + 4* enat (nat (X * X))" using C by auto
  also have "  enat (nat (X * X)) + 4* enat (nat (X * X))" using D by auto
  also have " = 5* enat (nat (X * X))"
    by (metis eSuc_numeral mult_eSuc semiring_norm(5)) 
  also have " =  enat ( 5* nat (X * X))"
    by (simp add: numeral_eq_enat) 
  finally 
  show ?thesis .
qed
          
     
 
lemma weakenpre: " 2' {P}c{Q} ;   (s. P s   P' s)   
           2' {P'}c{ Q}"  using conseq[where Q'=Q and k=1]  
  by auto  

lemma whileDecr: "2' { %s. enat (nat (s ''x'')) + 1} WHILE (Less (N 0) (V ''x'')) DO (SKIP;; SKIP;; ''x'' ::= Plus (V ''x'') (N (-1))) { %s. enat 0}" 
  apply(rule conseq[where k=4])
     apply(rule While[where I="%s. enat 4 * (enat (nat (s ''x'')))"])
     prefer 2
  subgoal for s apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1)) by presburger
      apply(rule Seq[where P2="wpQ (''x'' ::= Plus (V ''x'') (N (-1))) (λt. enat 4 * enat (nat (t ''x'')) + 1)"])
      apply(simp)
     apply(rule Seq[where P2="wpQ (SKIP) (λs. eSuc (enat (4 * nat (s ''x'' - 1)) + 1))"])
      apply simp
  subgoal apply(rule weakenpre) apply(rule Skip) apply auto
    subgoal for s apply(cases "s ''x'' > 0") apply auto
      apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
    done
  subgoal apply simp   apply(rule Skip) done
  subgoal apply simp apply(rule weakenpre) apply(rule Assign) by simp
     apply simp 
  subgoal for s apply(cases "s ''x'' > 0") by auto
  by simp
    
    
lemma whileDecrIf: "2' { %s. enat (nat (s ''x'')) + 1} WHILE (Less (N 0) (V ''x'')) DO ( (IF Less (N 0) (V ''z'') THEN SKIP;; SKIP ELSE SKIP );; ''x'' ::= Plus (V ''x'') (N (-1))) { %s. enat 0}"
  apply(rule conseq[OF While, where k=6 and I1="%s. enat 6 * (enat (nat (s ''x'')))"])  
     prefer 2
  subgoal for s apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1)) by presburger
      apply(rule Seq[where P2="wpQ (''x'' ::= Plus (V ''x'') (N (-1))) (λt. enat 6 * enat (nat (t ''x'')) + 1)"])
     apply(simp)
      apply(rule weakenpre)
      apply(rule If[where P="wpQ (IF Less (N 0) (V ''z'') THEN SKIP;; SKIP ELSE SKIP ) (λs. eSuc (enat (6 * nat (s ''x'' - 1)) + 1))"])
      subgoal  
        apply simp 
        apply(rule Seq[where P2="wpQ (SKIP) (λs. eSuc (enat (6 * nat (s ''x'' - 1)) + 1))"])
        subgoal apply(rule weakenpre)  apply(rule Skip) by auto  
        subgoal apply(rule weakenpre) apply(rule Skip) by auto
        done
      subgoal
        apply simp 
        subgoal apply(rule weakenpre)  apply(rule Skip) by auto  
        done
     subgoal
              apply auto
    subgoal for s apply(cases "s ''x'' > 0") apply auto
      apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
    subgoal for s apply(cases "s ''x'' > 0") apply auto
      apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
    done
  subgoal apply simp apply(rule weakenpre) apply(rule Assign) by simp
     apply simp 
  subgoal for s apply(cases "s ''x'' > 0") by auto
  by simp
   
    
lemma whileDecrIf2: "2' { %s. enat (nat (s ''x'')) + 1} WHILE (Less (N 0) (V ''x'')) DO ( (IF Less (N 0) (V ''z'') THEN SKIP;; SKIP ELSE SKIP );; ''x'' ::= Plus (V ''x'') (N (-1))) { %s. enat 0}"
  apply(rule conseq[OF While, where k=6 and I1="%s. enat 6 * (enat (nat (s ''x'')))"])
      apply(rule Seq[where P2="wpQ (''x'' ::= Plus (V ''x'') (N (-1))) (λt. enat 6 * enat (nat (t ''x'')) + 1)"])
     apply(simp)
      apply(rule weakenpre)
      apply(rule If[where P="wpQ (IF Less (N 0) (V ''z'') THEN SKIP;; SKIP ELSE SKIP ) (λs. eSuc (enat (6 * nat (s ''x'' - 1)) + 1))"])
      subgoal  
        apply simp 
        apply(rule Seq[where P2="wpQ (SKIP) (λs. eSuc (enat (6 * nat (s ''x'' - 1)) + 1))"])
        subgoal apply(rule weakenpre)  apply(rule Skip) by auto  
        subgoal apply(rule weakenpre) apply(rule Skip) by auto
        done
      subgoal
        apply simp 
        subgoal apply(rule weakenpre)  apply(rule Skip) by auto  
        done
     prefer 2
    subgoal apply simp apply(rule weakenpre) apply(rule Assign) by simp        
     subgoal
              apply auto
    subgoal for s apply(cases "s ''x'' > 0") apply auto
      apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
    subgoal for s apply(cases "s ''x'' > 0") apply auto
      apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1) eSuc_enat) done
    done 
  subgoal for s apply(simp only: one_enat_def plus_enat_simps times_enat_simps enat_ord_code(1)) by presburger
  subgoal for s apply(cases "s ''x'' > 0") by auto
  by simp
    

end