Theory Nielson_Hoare

theory Nielson_Hoare
imports Big_StepT 
begin

section "Nielson Style Hoare Logic with logical variables"

abbreviation "eq a b == (And (Not (Less a b)) (Not (Less b a)))"
   
type_synonym lvname = string
type_synonym assn2 = "(lvname  nat)  state  bool"
type_synonym tbd = "state  nat" (* time bound *)

subsection ‹The support of an assn2›

definition support :: "assn2  string set" where
"support P = {x. l1 l2 s. (y. y  x  l1 y = l2 y)  P l1 s  P l2 s}"


lemma support_and: "support (λl s. P l s  Q l s)  support P  support Q"
unfolding support_def by blast
  
lemma support_impl: "support (λl s. P s  Q l s)  support Q"
unfolding support_def by blast
  
lemma support_exist: "support (λl s.  z::nat. Q z l s)  (UN n. support (Q n))"
  unfolding support_def apply(auto)
  by blast+   

    
lemma support_all: "support (λl s. z. Q z l s)  (UN n. support (Q n))"
  unfolding support_def apply(auto)
  by blast+  
    
    
lemma support_single: "support (λl s. P (l a) s)  {a}"
  unfolding support_def by fastforce
    
lemma support_inv: "P. support (λl s. P s) = {}"
unfolding support_def by blast 

lemma assn2_lupd: "x  support Q  Q (l(x:=n)) = Q l"
by(simp add: support_def fun_upd_other fun_eq_iff)
  (metis (no_types, lifting) fun_upd_def)

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

definition hoare1_valid :: "assn2  com  tbd  assn2  bool"
  ("1 {(1_)}/ (_)/ { _ (1_)}" 50) where
"1 {P} c {q  Q}    (k>0. (l s. P l s  (t p. ((c,s)  p  t)   p  k * (q s)  Q l t)))"


subsection "Hoare rules"
  
inductive
  hoare1 :: "assn2  com  tbd  assn2  bool" ("1 ({(1_)}/ (_)/ { _  (1_)})" 50)
where

Skip:  "1 {P} SKIP { (%s. Suc 0)  P}"  |

Assign:  "1 {λl s. P l (s[a/x])} x::=a {  (%s. Suc 0)  P}"  |

If: " 1 {λl s. P l s  bval b s} c1 { e1  Q};
       1 {λl s. P l s  ¬ bval b s} c2 { e1  Q} 
   1 {P} IF b THEN c1 ELSE c2 { (λs. e1 s + Suc 0 )  Q}"  |

Seq: " 1 { (%l s. P1 l s  l x = e2' s ) } c1 { e1  (%l s. P2 l s   e2 s  l x )};
         1 {P2} c2 { e2  P3}; x  support P1; x  support P2;
         l s. P1 l s  e1 s + e2' s  e s
           1 {P1} c1;;c2 { e  P3}"  |

While:
  " 1 {λl s. P l s  bval b s  e' s = l y} c {  e''  λl s. P l s  e s  l y};
       l s. bval b s  P l s   e s  1  +  e' s + e'' s  ; 
     l s. ~ bval b s  P l s  1  e s;
     y  support P  
    1 {P} WHILE b DO c { e  λl s. P l s  ¬ bval b s}" |

conseq: " k>0. l s. P' l s  ( e s  k * (e' s) (t. l'. P l' s  ( Q l' t  Q' l t) ));
           1 {P}c{ e  Q}    
           1 {P'}c{e'  Q'}"  
  
  
text‹Derived Rules:›

lemma conseq_old: "k>0. l s. P' l s  (P l s  ( e' s   k * (e s))); 1 {P}c{ e'   Q}; l s. Q l s  Q' l s   
           1 {P'}c{e  Q'}"
  using conseq apply(metis) done

lemma If2: " 1 {λl s. P l s  bval b s} c1 { e  Q}; 1 {λl s. P l s  ¬ bval b s} c2 { e  Q};
        l s. P l s  e s + 1 = e' s 
   1 {P} IF b THEN c1 ELSE c2 { e'  Q}"
apply(rule conseq[OF _ If, where P=P and P'=P]) by(auto)

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

lemma weaken_post:
  " 1 {P} c {e  Q};  l s. Q l s  Q' l s    1 {P} c {e  Q'}"
  apply(rule conseq_old[where   e'=e and Q=Q and P=P])
    by(auto)

lemma ub_cost:
  " (k>0. l s. P l s  e' s  k * (e s));  1 {P} c {e'  Q}    1 {P} c {e  Q}"
  apply(rule conseq_old[where e'=e' and Q=Q and P=P])
  by(auto) 

lemma Assign': "l s. P l s  Q l (s[a/x])  (1 {P} x ::= a { (%s. 1)  Q})"
using strengthen_pre[OF _ Assign] 
by (simp )

 
subsection "Soundness"
  
text‹The soundness theorem:›

theorem hoare1_sound: "1 {P}c{e  Q}    1 {P}c{e  Q}"
apply(unfold hoare1_valid_def)
proof(  induction  rule: hoare1.induct)
  case (Skip P)
  show ?case  by fastforce
next
  case (Assign P a x)
  show ?case  by fastforce 
next
  case (Seq P1 x e2' c1 e1 P2 e2 c2 P3 e)
  from Seq(6) obtain k where k: "k>0" and  S6: "l s. P1 l s  l x = e2' s  (t p. (c1, s)  p  t  p  k * e1 s  P2 l t  e2 t  l x)" by auto
  from Seq(7) obtain k' where k': "k'>0" and  S7:  "l s. P2 l s  (t p. (c2, s)  p  t  p  k' * e2 s  P3 l t)" by auto
  from k k' have "0 < max k k'" by auto
  show ?case 
  proof (rule exI[where x="max k k'"], safe)
    fix l s 
    have x_supp: "x  support P1" by fact
    have x_supp2: "x  support P2" by fact

    from S6 have S: "P1 (l(x := e2' s)) s  (l(x := e2' s)) x = e2' s  (t p. (c1, s)  p  t   p  k * e1 s  P2 (l(x := e2' s)) t  e2 t  (l(x := e2' s)) x) "
       by blast
     
    assume a: "P1 l s"

    with Seq(5) have 1: " e1 s + e2' s    e s" by simp 
    with a S assn2_lupd[OF x_supp] have "(t p. (c1, s)  p  t  p  k * e1 s  P2 (l(x := e2' s)) t  e2 t  (l(x := e2' s)) x)" by simp
    then obtain t p where c1: "(c1, s)  p  t" and cost1: " p  k * e1 s" and P2': "P2 (l(x := e2' s)) t" and 31: "e2 t  (l(x := e2' s)) x" by blast
    from P2' assn2_lupd[OF x_supp2] have P2: "P2 l t" by auto
    from 31 have 3: "e2 t  e2' s" by simp 
    from S7 P2 have "(t' p'. ((c2, t)  p'  t')    p'  k' * e2 t  P3 l t')" by blast
    then obtain t' p'  where c2: "(c2, t)  p'  t'" and cost2: " p'  k' * (e2 t)" and P3: "P3 l t'" by blast

    from c1 c2 have weg: "(c1;; c2, s)  p + p'  t'"  
      apply (rule Big_StepT.Seq) by simp
    from cost1 cost2 3 have " (p+p')  k * (e1 s) + k' * (e2' s)"
      by (meson add_mono mult_le_mono2 order_subst1)  
    also have "  (max k k') * (e1 s) + (max k k') * (e2' s)"
      by (simp add: add_mono) 
    also have "  (max k k') * (e1 s + e2' s)"
      by (simp add: add_mult_distrib2)      
    also have "  (max k k') * (e s)" using 1 by simp
  finally
    have cost: " (p + p')  (max k k') * (e s)" .
      
    from weg cost P3
    have "(c1;; c2, s)  p+p'  t'    (p+p')  (max k k') * (e s)  P3 l t'" by blast
    then show "(t p. (c1;; c2, s)  p  t   p  (max k k') * (e s)  P3 l t)" by metis
  qed fact
next
  case (If P b c1 e Q c2)
  from If(3) obtain k1 where k1: "k1>0" and If1: "l s. P l s  bval b s  (t p. (c1, s)  p  t  p  k1 * e s  Q l t)" by auto
  from If(4) obtain k2 where  k2: "k2>0" and If2: "l s. P l s  ¬ bval b s  (t p. (c2, s)  p  t  p  k2 * e s  Q l t)" by auto
  let ?k' = "max (k1+1) (k2+1)"
  have "?k'>0" by auto  
  show ?case
  proof (rule exI[where x="?k'"], safe)
    fix l s
    assume P1: "P l s"
    show "t p. (IF b THEN c1 ELSE c2, s)  p  t   p  ?k' * (e s + Suc 0)  Q l t"
    proof (cases "bval b s")
      case True
      with If1 P1 obtain t p where "(c1, s)  p  t" "p  k1 * (e s)" "Q l t" by blast
      with True have 1: "(IF b THEN c1 ELSE c2, s)  p+1  t" "(p + 1)  (k1+1) * (e s  + Suc 0)"
          "Q l t"
        by auto  
      have "(k1+1) * (e s  + Suc 0)  ?k' * (e s  + Suc 0)"
        by (simp add: nat_mult_max_left) 
      with 1 have 2: "p+1    ?k' * (e s  + Suc 0)"
        by linarith
      from 1 2 show "t p. (IF b THEN c1 ELSE c2, s)  p  t  p  ?k' * (e s + Suc 0)  Q l t" by metis
    next
      case False
      with If2 P1 obtain t p where "(c2, s)  p  t" "p  k2 * (e s)" "Q l t" by blast
      with False have 1: "(IF b THEN c1 ELSE c2, s)  p+1  t" "(p + 1)  (k2+1) * ( e s  + Suc 0)"
          "Q l t"
        by auto 
      have "(k2+1) * (e s  + Suc 0)  ?k' * (e s  + Suc 0)"
        by (simp add: nat_mult_max_left)  
      with 1 have 2: "p+1    ?k' * (e s  + Suc 0)"
        by linarith
      from 1 2 show "t p. (IF b THEN c1 ELSE c2, s)  p  t   p  ?k' * (e s + Suc 0)  Q l t" by metis
    qed
  qed fact
next
  case (conseq P' e e' P Q Q' c)
  from conseq(1) obtain k1 where k1: "k1>0" and c1: "l s. P' l s  e s  k1 * e' s  (t. l'. P l' s  (Q l' t  Q' l t))" by auto
  then have c1': "l s. P' l s  e s  k1 * e' s  (t. l'. P l' s  (Q l' t  Q' l t))"
    by auto
  from conseq(3) obtain k2 where k2: "k2>0" and c2: "l s. P l s  (t p. (c, s)  p  t  p  k2 * e s  Q l t)" by auto
  then have c2': "l s.  P l s  (t p. (c, s)  p  t  p  k2 * e s  Q l t)" by auto
  have "k2*k1 > 0" using k1 k2 by auto
  show ?case 
  proof (rule exI[where x="k2*k1"], safe)
    fix l s
    assume "P' l s"
    with c1' have A: "e s  k1 * e' s" and "t. l'. P l' s  (Q l' t  Q' l t)" by auto
    then obtain fl where "t. P (fl t) s" and B: "t. Q (fl t) t  Q' l t" by metis
    with c2' obtain ft fp where i: "t. (c, s)  (fp t)  (ft t)" and ii: "t. (fp t)  k2 * e s"
        and iii: "t. Q (fl t) (ft t)" 
      by meson
    from i obtain t p where tt: "x. ft x = t" "x. fp x = p" using big_step_t_determ2
      by meson
    with i have c: "(c, s)  p  t" by simp   
    from tt ii iii have p: "p  k2 * e s" and Q: "x. Q (fl x) t" by auto
    have p: "p  k2 * k1 * e' s" using p A
      by (metis le_trans mult.assoc mult_le_mono2)  
    from B Q have q: "Q' l t" by fast
    
    from c p q
    show "t p. (c, s)  p  t  p   k2 *k1 * e' s  Q' l t" 
      by blast
  qed fact  
next
  case (While INV b e' y c e'' e)  
  from While(5) obtain k where W6: "l s. INV l s  bval b s  e' s = l y  (t p. (c, s)  p  t  p  k * e'' s  INV l t  e t  l y)" by auto 
  let ?k' = "k+1"
  {
    fix n l s
    have " e s = n; INV l s   t p. (WHILE b DO c, s)  p  t  p  ?k' * e s  INV l t  ¬ bval b t"
    proof(induction "n" arbitrary: l s rule: less_induct)
      case (less x)
        
      show ?case
      proof (cases "bval b s")
        case False
        with less(2,3) While(3) have  b: "1  e s" by auto

        show ?thesis
          apply(rule exI[where x=s])
          apply(rule exI[where x=1]) apply safe
          subgoal using  WhileFalse[OF False] by simp 
          subgoal using b by auto 
          subgoal using less by auto
          subgoal using False by auto
          done
            
      next 
      case True
      with less(2,3) While(2) have bT: "bval b s" and cost1: "  1 + e' s + e'' s  e s" by auto 
      let ?l' = "l(y := e' s)"

      have y_supp: "y  support INV" by fact 
 
      from cost1 have Z: "e' s < x" using less(2) by auto
      from W6
      have "INV ?l' s  bval b s  e' s = ?l' y
             (t p. (c, s)  p  t    p  k * e'' s   INV ?l' t  e t  ?l' y)"
          by blast
      with less(3) bT
      have "(t p. ((c, s)  p  t)    p  k * e'' s   INV ?l' t  e t  e' s)"
            using   assn2_lupd[OF y_supp] 
        by(auto)  
      then obtain t p   where ceff: "(c, s)  p  t" and cost2: " p   k * e'' s" 
                    and INVz': "INV ?l' t" and cost3: "  e t    e' s"
        by blast 

      from INVz' have INVz: "INV l t" using assn2_lupd[OF y_supp] by auto 
      have "e t < x" using Z cost3 by auto
      with less(1)[OF _ _ INVz, of "e t"]  obtain t' p' 
        where weff: "(WHILE b DO c, t)  p'  t'" and cost4: " p'  ?k' *  e t" and INV0: "INV l t'"
            and nb: "¬ bval b t'"
          by fastforce      

      have "(WHILE b DO c, s)  1 + p + p'   t'"
        apply(rule WhileTrue)
          apply fact
          apply (fact ceff) 
          apply (fact weff) by simp
    moreover
      note INV0 nb
      moreover
      {
        have "(1 + p + p')  1 + k * e'' s + ?k' * e t" using cost2 cost4 by linarith
        also have "   1 + k * e'' s + ?k' * e' s" using cost3
          using add_left_mono mult_le_mono2 by blast 
        also have "  ?k'*1 + ?k'* e'' s + ?k' * e' s " by force 
        also have " = ?k' * (1+ e' s + e'' s)" by algebra
        also have "  ?k' * e s" using cost1
          using mult_le_mono2 by blast            
        finally have " (1 + p + p')  ?k' * e s" .
      }
    ultimately  
      show ?thesis by metis
    qed 
    qed
  }  
  then have erg: "l s. INV l s  t p. (WHILE b DO c, s)  p  t  p  (k + 1) * e s  INV l t  ¬ bval b t" by auto
  show ?case apply(rule exI[where x="?k'"]) using erg by fastforce
qed 

subsection "Completeness"

definition wp1 :: "com  assn2  assn2" ("wp1") where
"wp1 c Q  =  (λl s. t p. (c,s)  p  t  Q l t)"
 

lemma support_wpt: "support (wp1 c Q)  support Q"
by(simp add: support_def wp1_def) blast

  
lemma wp1_terminates: "wp1 c Q l s   (c, s)" unfolding wp1_def by auto

    
lemma wp1_SKIP[simp]: "wp1 SKIP Q = Q" by(auto intro!: ext simp: wp1_def)

lemma wp1_Assign[simp]: "wp1 (x ::= e) Q = (λl s. Q l (s(x := aval e s)))" by(auto intro!: ext simp: wp1_def)

lemma wp1_Seq[simp]: "wp1 (c1;;c2) Q = wp1 c1 (wp1 c2 Q)" by (auto simp: wp1_def fun_eq_iff)

lemma wp1_If[simp]: "wp1 (IF b THEN c1 ELSE c2) Q = (λl s. wp1 (if bval b s then c1 else c2) Q l s)" by (auto simp: wp1_def fun_eq_iff)

    
definition "prec c E == %s. E (THE t. (p. (c,s)  p  t))"
  
lemma wp1_prec_Seq_correct: "wp1 (c1;;c2) Q l s  t (c1, s) + prec c1 (λs. t (c2, s)) s  t (c1;; c2, s)"
proof -
  assume "wp1 (c1;;c2) Q l s"
  then have wp: "wp1 c1 (wp1 c2 Q) l s" by simp
  then obtain t p where c1_term: "(c1, s)  p  t" and "(ta p. (c2, t)  p  ta  Q l ta)" unfolding wp1_def by blast
  then obtain t' p' where c2_term: "(c2, t)  p'  t'" and  "Q l t'" by blast

  have p: "t (c1, s) = p" using c1_term bigstepT_the_cost by simp
  have "t (c2, t) = p'" using c2_term bigstepT_the_cost by simp

  have f: "(THE t. p. (c1, s)  p  t) = t" using c1_term bigstepT_the_state by simp

  have " prec c1 (λs. t (c2, s)) s = p'" unfolding prec_def f using c2_term bigstep_det by blast
  then have p': " prec c1 (λs.  (THE n. a. (c2, s)  n  a)) s
        =  p'" unfolding prec_def by blast

  from wp have "wp1 (c1;;c2) Q l s" by simp
  then obtain T P where c12_term: "(c1;;c2, s)  P  T" and "Q l T" unfolding wp1_def by blast

  have P: "(THE n. (a. (c1;;c2, s)  n  a)) = P" using c12_term bigstepT_the_cost by simp

  from c12_term have Ppp': "P = p + p'"
    apply(elim Seq_tE)
    using c1_term bigstep_det c2_term by blast

  have " (THE n. a. (c1, s)  n  a) + prec c1 (λs.  (THE n. a. (c2, s)  n  a)) s
        =  p +  p'" using p p' by auto
  also have " =  P" using Ppp' by auto
  also have " =  (THE n. (a. (c1;;c2, s)  n  a))" using P by auto
  finally
  show "t (c1, s) + prec c1 (λs. t (c2, s)) s  t (c1;; c2, s)"
    by simp
qed 
  


abbreviation "new Q  SOME x. x  support Q"

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 assumes b: "bval b s"
  shows wp1WhileTrue': "wp1 (WHILE b DO c) Q l s = wp1 c (wp1 (WHILE b DO c) Q) l s"
proof 
  assume "wp1 c (wp1 (WHILE b DO c) Q) l s"
  from this[unfolded wp1_def]
  obtain t s' t' s'' where "(c, s)  t  s'" "(WHILE b DO c, s')  t'  s''" and Q: "Q l s''" by blast
  with b have "(WHILE b DO c, s)  1+t+t'  s''" by auto
  with Q show "wp1 (WHILE b DO c) Q l s" unfolding wp1_def by auto
next
  assume "wp1 (WHILE b DO c) Q l s"
  from this[unfolded wp1_def]
  obtain t s'' where "(WHILE b DO c, s)  t  s''" and Q: "Q l s''" by blast
  with b  obtain t1 t2 s' where "(c, s)  t1  s'" "(WHILE b DO c, s')  t2  s''" by auto
  with Q show "wp1 c (wp1 (WHILE b DO c) Q) l s " unfolding wp1_def by auto
qed
  
lemma assumes b: "~ bval b s"
  shows wp1WhileFalse': "wp1 (WHILE b DO c) Q l s =  Q l s"
proof 
  assume "wp1 (WHILE b DO c) Q l s"
  from this[unfolded wp1_def]
  obtain t s' where "(WHILE b DO c, s)  t  s'" and Q: "Q l s'" by blast
  with b  have "s=s'" by auto
  with Q show "Q l s" by auto
next
  assume "Q l s"
  with b show  "wp1 (WHILE b DO c) Q l s" unfolding wp1_def by auto
qed
  
lemma wp1While: "wp1 (WHILE b DO c) Q l s = (if bval b s then wp1 c (wp1 (WHILE b DO c) Q) l s else Q l s)"  
  apply(cases "bval b s")      
  using wp1WhileTrue' apply simp
  using wp1WhileFalse' apply simp   done 
  
lemma wp1_prec2: fixes e::tbd
    shows "(wp1 c1 Q l s 
           l x = prec c1 e s) = wp1 c1 (λl s. Q l s  e s = l x) l s"
      by (metis (mono_tags, lifting) Big_StepT.bigstepT_the_state prec_def wp1_def)
      
      
lemma wp1_prec: fixes e::tbd
    shows "wp1 c1 Q l s 
           l x = prec c1 e s  wp1 c1 (λl s. Q l s  e s = l x) l s"
unfolding wp1_def prec_def apply(auto) 
proof -
  fix p t
  assume "l x = e (THE t. p. (c1, s)  p  t)"
  assume 2: "Q l t"
  assume 1: "(c1, s)  p  t "
  show "t. (p. (c1, s)  p  t)  Q l t  e t = e (THE t. p. (c1, s)  p  t) "
    apply(rule exI[where x=t])
    apply(safe)
      apply(rule exI[where x=p]) using 1 apply simp
      apply(fact)
      using 1 by(simp add: bigstepT_the_state)
qed 
  

lemma wp1_is_pre: "finite (support Q)  1 {wp1 c Q} c { λs. t (c, s)  Q}"
proof (induction c arbitrary: Q)
  case SKIP
  have ff: "s n. (a. (SKIP, s)  n  a) = (n=Suc 0)" by blast  
  show ?case apply (auto intro:hoare1.Skip simp add: ff) using ff done
next
  have gg: "x1 x2 s n. (a. (x1 ::= x2, s)  n  a) = (n=Suc 0)" by blast
  case Assign show ?case apply (auto intro:hoare1.Assign simp add: gg) done
next
  case (Seq c1 c2)  
  ― ‹choose a fresh logical variable x›
  let ?x = "new Q"
  have "x. x  support Q" using Seq.prems infinite_UNIV_listI
    using ex_new_if_finite by blast
  hence  "?x  support Q" by (rule someI_ex) 
  then have x2: "?x  support (wp1 c2 Q)"  using support_wpt by (fast)
  then have x12: "?x  support (wp1 (c1;;c2) Q)" apply simp using support_wpt by fast

  ― ‹assemble a postcondition Q1 that ensures the weakest precondition of Q before c2
        and saves the running time of c2 into the logical variable x›
  let ?Q1 = "(λl s. (wp1 c2 Q) l s   t (c2, s) = l ?x)"
  have "finite (support ?Q1)" apply(rule rev_finite_subset[OF _ support_and])
     apply(rule finite_UnI)
      apply(rule rev_finite_subset[OF _ support_wpt]) apply(fact)
    apply(rule rev_finite_subset[OF _ support_single]) by simp
  ― ‹we can now specify this Q1 in the first Induction Hypothesis›    
  then have pre: "u. 1 {wp1 c1 ?Q1 } c1 { λs. t (c1, s)   ?Q1  }"
    using Seq(1) by simp  

  ― ‹we can rewrite this into the form we need for the Seq rule›
  have A: " 1 {λl s. wp1 (c1;;c2) Q l s  l ?x = (prec c1 (%s. t (c2, s))) s} c1 { λs. t (c1, s)  λl s. wp1 c2 Q l s   t (c2, s)  l ?x}"
    apply(rule conseq_old[OF _ pre ])
    by(auto simp add: wp1_prec) 

  ― ‹we can now apply the Seq rule with the first IH (in the right shape A) and the second IH›
  show "1 {wp1 (c1;; c2) Q} c1;; c2 { λs. t (c1;; c2, s)  Q}"
    apply(rule hoare1.Seq[OF A Seq(2)])  
       ― ‹finally some side conditions have to be proven› 
       using Seq(3) x12 x2 wp1_prec_Seq_correct .
next
  case (If b c1 c2)
    
  show ?case apply(simp)
  apply(rule If2[where e="%s. if bval b s then t (c1, s) else t (c2, s)"]) 
    apply(simp_all  cong:rev_conj_cong)
    apply(rule conseq_old[where Q=Q and Q'=Q])
      prefer 2
      apply(rule If.IH(1)) apply(fact)
      apply(simp_all) apply(auto)[1]
    apply(rule conseq_old[where Q=Q and Q'=Q])
      prefer 2
      apply(rule If.IH(2)) apply(fact)
      apply(simp_all) apply(auto)[1]
      apply (blast intro: If_THE_True wp1_terminates If_THE_False) 
     done
 
next
  case (While b c)
 
      let ?y = "(new (wp1 (WHILE b DO c) Q))"
    have "finite (support (wp1 (WHILE b DO c) Q))"
      apply(rule finite_subset[OF support_wpt]) apply fact done
    then have "x. x  support (wp1 (WHILE b DO c) Q)" using infinite_UNIV_listI
      using ex_new_if_finite by blast
    hence yQx: "?y  support (wp1 (WHILE b DO c) Q)" by (rule someI_ex)

  show ?case
  proof (rule conseq_old[OF _  hoare1.While], safe )
    show "k>0. l s. wp1 (WHILE b DO c) Q l s  wp1 (WHILE b DO c) Q l s   t (WHILE b DO c, s)  k * t (WHILE b DO c, s)"
      apply auto done
  next
    fix l s
    assume "wp1 (WHILE b DO c) Q l s" "¬ bval b s"
    then show "Q l s" by (simp add: wp1While)
  next
    fix l s
    assume "wp1 (WHILE b DO c) Q l s"
    from this[unfolded wp1_def] obtain t s' where t: "(WHILE b DO c, s)  t  s'" and "Q l s'" by blast
    then have r: "t (WHILE b DO c, s) = t" using Nielson_Hoare.bigstepT_the_cost by auto 
    assume "¬ bval b s"
    with r t have   t2: "t=1" by auto 
    from r t2 show "1  t (WHILE b DO c, s)" by auto 
  next
    fix l s
    assume "wp1 (WHILE b DO c) Q l s"
    from this[unfolded wp1_def] obtain t s'' where t: "(WHILE b DO c, s)  t  s''" "Q l s''" by blast
    then have r: "t (WHILE b DO c, s) = t" using Nielson_Hoare.bigstepT_the_cost by auto 
    assume "bval b s" 
    with t obtain t1 t2 s' where 1: "(c,s)  t1  s'" and 2: "(WHILE b DO c, s')  t2  s''" and sum: "t=t1+t2+1" and "bval b s" by auto
    from 1 have A: "t (c,s) = t1" and s': "s (c,s) = s'" using Nielson_Hoare.bigstepT_the_cost bigstepT_the_state by auto
    from 2 s' have B: "t (WHILE b DO c, s(c,s)) = t2" using Nielson_Hoare.bigstepT_the_cost by auto

    show "1 + (%s. t (WHILE b DO c, s(c,s))) s  + (%s. t (c,s)) s  t (WHILE b DO c, s)"
      apply(simp add: r A B sum) done
  next 
    
    
    show "1 {λl s. wp1 (WHILE b DO c) Q l s  bval b s  t (WHILE b DO c, s (c, s)) = l ?y} c
         { λs. t (c, s)  λl s. wp1 (WHILE b DO c) Q l s  t (WHILE b DO c, s)  l ?y}"
       apply(rule conseq_old[OF _ While(1), of _ "%l s. wp1 (WHILE b DO c) Q l s  t (WHILE b DO c, s) = l ?y"])
        apply(rule exI[where x=1]) apply simp
      subgoal apply safe
        apply(subst (asm) wp1While) apply simp
      proof - fix l s
        assume 1: "wp1 c (wp1 (WHILE b DO c) Q) l s"
        assume 2: "t (WHILE b DO c, s (c, s)) = l ?y" 
        then have "l ?y = prec c (%s. t (WHILE b DO c, s)) s" unfolding prec_def by auto
        with 1 wp1_prec2[of c "(wp1 (WHILE b DO c) Q)" l s _ "(λs. t (WHILE b DO c, s))"]
          show "wp1 c (λl s. wp1 (WHILE b DO c) Q l s   t (WHILE b DO c, s) = l ?y) l s" by auto
        qed
        subgoal apply(rule finite_subset[OF support_and]) apply auto
           apply(rule finite_subset[OF support_wpt]) apply fact
             apply(rule finite_subset) apply(rule support_single)  by auto
        apply auto done 
    next
      assume "new (wp1 (WHILE b DO c) Q)  support (wp1 (WHILE b DO c) Q)"
      with yQx show "False"  
        by blast
       
    qed
  qed

    
lemma valid_wp: "1 {P}c{p  Q}  (k>0. (l s. P l s  (wp1 c Q l s  ((THE n. ( t. ((c,s)  n  t))))  k * p s)))"
  apply(rule)
   apply(auto simp: hoare1_valid_def wp1_def)    
  subgoal for k apply(rule exI[where x=k]) using bigstepT_the_cost by fast       
  subgoal for k apply(rule exI[where x=k]) using bigstepT_the_cost by fast
  done
    
    
theorem hoare1_complete: "finite (support Q)  1 {P}c{p  Q}  1 {P}c{p  Q}"   
  apply(rule conseq_old[OF _ wp1_is_pre, where Q'=Q and Q=Q, simplified]) 
  by (auto simp: valid_wp)   
  
    
corollary hoare1_sound_complete: "finite (support Q)  1 {P}c{p  Q}  1 {P}c{p  Q}"
  by (metis hoare1_sound hoare1_complete)
    
end