Theory Nielson_VCG

(* Author: Max Haslbeck *)

theory Nielson_VCG imports Nielson_Hoare begin

subsection "Verification Condition Generator"

text‹Annotated commands: commands where loops are annotated with
  invariants.›

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) |
  Aconseq assn2 assn2 tbd  acom
  ("({_'/_'/_}/ CONSEQ _)"  [0, 0, 0, 61] 61)|
  Awhile "(assn2)*((statestate)*(tbd))" bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
  
notation com.SKIP ("SKIP")

text‹Strip annotations:›

fun strip :: "acom  com" where
  "strip SKIP = SKIP" |
  "strip (x ::= a) = (x ::= a)" |
  "strip (C1;; C2) = (strip C1;; strip C2)" |
  "strip (IF b THEN C1 ELSE C2) = (IF b THEN strip C1 ELSE strip C2)" |
  "strip ({_/_/_} CONSEQ C) = strip C" |
  "strip ({_} WHILE b DO C) = (WHILE b DO strip C)"
  
  
  
text "support of an expression"

subsubsection "support and supportE"
  
  
  
definition supportE :: "((char list  nat)  (char list  int)  nat)   string set" where
  "supportE P = {x. l1 l2 s. (y. y  x  l1 y = l2 y)  P l1 s  P l2 s}"
  
  
lemma expr_lupd: "x  supportE Q  Q (l(x:=n)) = Q l"
  by(simp add: supportE_def fun_upd_other fun_eq_iff)
    (metis (no_types, lifting) fun_upd_def)

lemma supportE_if: "supportE (λl s. if b s then A l s else B l s)
   supportE A  supportE B"
  unfolding supportE_def apply(auto)
  by metis+


lemma support_eq: "support (λl s. l x = E l s)  supportE E  {x}"
  unfolding support_def supportE_def 
  apply(auto)
   apply blast
  by metis


lemma support_impl_in: "G e  support (λl s.  H e l s)  T
   support (λl s. G e   H e l s)  T"
  unfolding support_def apply(auto)
   apply blast+ done

lemma support_supportE: "P e. support (λl s.  P (e l) s)  supportE e"
  unfolding support_def supportE_def
  apply(rule subsetI)
  apply(simp)
proof (clarify, goal_cases)
  case (1 P e x l1 l2 s)
  have P: "s. e l1 s = e l2 s  e l1 = e l2" by fast
  show "l1 l2. (y. y  x  l1 y = l2 y)  (s. e l1 s  e l2 s)"
    apply(rule exI[where x=l1])
    apply(rule exI[where x=l2])
    apply(safe)
    using 1 apply blast
    apply(rule ccontr)
    apply(simp) 
    using 1(2) P by force            
qed 
  
― ‹collects the logical variables in the Invariants and Loop Bodies as well as the annotated
    assertions at CONSEQs of an annotated command›
fun varacom :: "acom  lvname set" where
  "varacom (C1;; C2)= varacom C1  varacom C2"
| "varacom (IF b THEN C1 ELSE C2)= varacom C1  varacom C2"
| "varacom ({P/Qannot/_} CONSEQ C)= support P  varacom C  support Qannot"
| "varacom ({(I,(S,(E)))} WHILE b DO C) = support I  varacom C"
| "varacom _ = {}"
    
text‹Weakest precondition from annotated commands:›

fun preT :: "acom  tbd  tbd" where
  "preT SKIP e = e" |
  "preT (x ::= a) e = (λs. e(s(x := aval a s)))" |
  "preT (C1;; C2) e = preT C1 (preT C2 e)" |
  "preT ({_/_/_} CONSEQ C) e = preT C e" |
  "preT (IF b THEN C1 ELSE C2) e =
  (λs. if bval b s then preT C1 e s else preT C2 e s)" |
  "preT ({(_,(S,_))} WHILE b DO C) e = e o S"
  
  
lemma preT_linear: "preT C (%s. k * e s) = (%s. k * preT C e s)"
by (induct C arbitrary: e, auto)
  
fun postQ :: "acom  state  state" where (* seems to be forward?! *)
  "postQ SKIP s = s" |
  "postQ (x ::= a) s =  s(x := aval a s)" |
  "postQ (C1;; C2) s = postQ C2 (postQ C1 s)" |
  "postQ ({_/_/_} CONSEQ C) s = postQ C s" |
  "postQ (IF b THEN C1 ELSE C2) s =
  (if bval b s then postQ C1 s else postQ C2 s)" |
  "postQ ({(_,(S,_))} WHILE b DO C) s = S s"
    
lemma TQ: "preT C e s = e (postQ C s)"
  apply(induct C arbitrary: e s) by (auto) 
  
(* given a state, how often will a While loop be evaluated ? *)  
function (domintros) times :: "state  bexp  acom  nat" where
  "times s b C = (if bval b s then Suc (times (postQ C s) b C) else 0)" 
   apply(auto) done

  
    
    
lemma assumes I: "I z s" and
  i:   "s z. I (Suc z) s  bval b s  I z (postQ C s)"
  and  ii:  "s. I 0 s  ~ bval b s"
shows times_z: "times s b C = z"
proof -  
  have "I z s  times_dom (s, b, C)  times s b C = z"
  proof(induct z arbitrary: s)
    case 0
    have A: "times_dom (s, b, C)"
      apply(rule times.domintros)
      apply(simp add:  ii[OF 0] ) done
    have B: "times s b C = 0"
      using times.psimps[OF A] by(simp add:  ii[OF 0])
    
    show ?case using A B by simp
  next
    case (Suc z)
    from i[OF Suc(2)] have bv: "bval b s"
      and g:  "I z (postQ C s)" by simp_all
    from Suc(1)[OF g] have p1: "times_dom (postQ C s, b, C)"
      and p2: "times (postQ C s) b C = z" by simp_all
    have A: "times_dom (s, b, C)" 
      apply(rule times.domintros) apply(rule p1) done
    have B: "times s b C = Suc z" 
      using times.psimps[OF A] bv p2 by simp
    show ?case using A B by simp
  qed
  
  then show "times s b C = z" using I by simp
qed
  
  
function (domintros) postQs :: "acom  bexp  state  state" where
  "postQs C b s = (if bval b s then (postQs C b (postQ C s))  else s)" 
  apply(auto) done
  
  
  
fun postQz :: "acom  state  nat  state" where
  "postQz C s 0 = s" |
  "postQz C s (Suc n) =  (postQz C (postQ C s) n)"
  
fun preTz :: "acom  tbd  nat  tbd" where
  "preTz C e 0 = e" |
  "preTz C e (Suc n) = preT C (preTz C e n)"
  
  
  
  
lemma TzQ: "preTz C e n s = e (postQz C s n)"
  by (induct n arbitrary: s, simp_all add: TQ)



subsubsection ‹Weakest precondition from annotated commands:›

fun pre :: "acom  assn2  assn2" where
  "pre SKIP Q  = Q" |
  "pre (x ::= a) Q = (λl s. Q l (s(x := aval a s)))" |
  "pre (C1;; C2) Q  = pre C1 (pre C2 Q)" |
  "pre ({P'/_/_} CONSEQ C) Q = P'" |
  "pre (IF b THEN C1 ELSE C2) Q =
  (λl s. if bval b s then pre C1 Q l s else pre C2 Q l s)" |
  "pre ({(I,(S,(E)))} WHILE b DO C) Q = I" 
  
lemma supportE_preT: "supportE (%l. preT C (e l))  supportE e"
proof(induct C arbitrary: e)
  case (Aif b C1 C2 e)
  show ?case
    apply(simp)
    apply(rule subset_trans[OF supportE_if])
    using Aif by fast
next
  case (Awhile A y C e)
  obtain I S E  where A: "A= (I,S,E)" using prod_cases3 by blast
  show ?case using A apply(simp) unfolding supportE_def
    by blast
next
  case (Aseq)
  then show ?case by force
qed (simp_all add: supportE_def, blast)

lemma supportE_twicepreT: "supportE (%l. preT C1 (preT C2 (e l)))  supportE e"
  by (rule subset_trans[OF supportE_preT supportE_preT])



lemma supportE_preTz: "supportE (%l. preTz C (e l) n)  supportE e"
proof (induct n) 
  case (Suc n)
  show ?case  
    apply(simp)
    apply(rule subset_trans[OF supportE_preT]) 
    by fact 
qed simp


lemma supportE_preTz_Un: (* like in support_wpw_Un *)
  "supportE (λl. preTz C (e l) (l x))  insert x (UN n. supportE (λl. preTz C (e l) n))"
  apply(auto simp add: supportE_def subset_iff)
  apply metis
  done


lemma supportE_preTz2: "supportE (%l. preTz C (e l) (l x))  insert x (supportE e)" 
  apply(rule subset_trans[OF supportE_preTz_Un])
  using supportE_preTz by blast  
  


lemma pff: "n. support (λl. I (l(x := n)))  support I - {x}"
  unfolding support_def apply(auto)  using fun_upd_apply apply smt
    apply (smt fun_upd_apply)  oops
  
lemma pff: "n. support (λl. I (l(x := n)))  support I"
  unfolding support_def apply(auto)  using fun_upd_apply apply smt
  by (smt fun_upd_apply)  


lemma supportAB: "support (λl s. A l s  B s)  support A"    
  apply(rule subset_trans[OF support_and]) 
    by (simp add: support_inv) 
    
lemma "support (pre ({(I,(S,(E )))} WHILE b DO C) Q)  support I" 
 by (simp add: supportAB) 

lemma support_pre: "support (pre C Q)  support Q  varacom C"
proof (induct C arbitrary: Q)
  case (Awhile A b C Q)
  obtain I S E  where A: "A= (I,(S,(E )))" using prod_cases3 by blast   
  have support_inv: "P. support (λl s. P s) = {}"
    unfolding support_def by blast   
  show ?case unfolding A  apply(simp) using supportAB  by fast
next
  case (Aseq C1 C2)
  then show ?case by(auto)
next
  case (Aif x C1 C2 Q)
  have s1: "support (λl s. bval x s  pre C1 Q l s)  support Q  varacom C1"
    apply(rule subset_trans[OF support_impl]) by(rule Aif)
  have s2: "support (λl s. ~ bval x s  pre C2 Q l s)  support Q  varacom C2"
    apply(rule subset_trans[OF support_impl]) by(rule Aif)
  
  show ?case apply(simp)
    apply(rule subset_trans[OF support_and]) 
    using s1 s2 by blast    
next
  case (Aconseq x1 x2 x3 C)
  then show ?case by(auto)
qed (auto simp add: support_def) 

lemma finite_support_pre[simp]: "finite (support Q)   finite (varacom C)   finite (support (pre C Q))"
  using finite_subset support_pre finite_UnI by metis 


fun time :: "acom  tbd" where
  "time SKIP = (%s. Suc 0)" |
  "time (x ::= a) = (%s. Suc 0)" |
  "time (C1;; C2) = (%s. time C1 s + preT C1 (time C2) s)" |
  "time ({_/_/e} CONSEQ C) = e" |
  "time (IF b THEN C1 ELSE C2) =
  (λs. if bval b s then 1 + time C1 s else 1 + time C2 s)" |
  "time ({(_,(E',(E )))} WHILE b DO C) = E"
   
    
lemma supportE_single: "supportE (λl s. P) = {}" 
  unfolding supportE_def by blast


lemma supportE_plus: "supportE (λl s. e1 l s + e2 l s)  supportE e1  supportE e2" 
  unfolding supportE_def apply(auto)
  by metis 

lemma supportE_Suc: "supportE (λl s. Suc (e1 l s)) = supportE e1"
  unfolding supportE_def by (auto) 


lemma supportE_single2: "supportE (λl . P) = {}" 
  unfolding supportE_def by blast

lemma supportE_time: "supportE (λl. time C) = {}"
  using supportE_single2 by simp   

lemma "s. (l. I (l(x:=0)) s) = (l. l x = 0  I l s)"
  apply(auto) 
  by (metis fun_upd_triv)

lemma "s. (l. I (l(x:=Suc (l x))) s) = (l. (n. l x = Suc n)  I l s)"
  apply(auto) 
proof (goal_cases)
  case (1 s l n)
  then have "l. I (l(x := Suc (l x))) s" by simp
  from this[where l="l(x:=n)"]
  have "I ((l(x:=n))(x := Suc ((l(x:=n)) x))) s" by simp
  then show ?case using 1(2) apply(simp) 
    by (metis fun_upd_triv)
qed 

text‹Verification condition:›
fun vc :: "acom  assn2   bool" where
  "vc SKIP Q = True" |
  "vc (x ::= a) Q = True" |
  "vc (C1 ;; C2) Q = ((vc C1 (pre C2 Q))  (vc C2 Q) )" |
  "vc (IF b THEN C1 ELSE C2) Q = (vc C1 Q  vc C2 Q)" |  
  "vc ({P'/Q/e'} CONSEQ C) Q' = (vc C Q  (k>0. (l s. P' l s  time C s  k * e' s   (t. l'. (pre C Q) l' s  ( Q l' t  Q' l t) ))))" |
  
  "vc ({(I,(S,(E)))} WHILE b DO C) Q = 
  ((l s. (I l s  bval b s   pre C I l s    E s  1 + preT C E s + time C s
   S s = S (postQ C s)) 
  (I l s  ¬ bval b s  Q l s  E s  1  S s = s) ) 
  vc C I)"
      
lemma pre_mono:
  "(l s. P l s  P' l s)  pre C P l s  pre C P' l s" 
proof (induction C arbitrary: P P' l s)
  case (Aseq C1 C2) 
  then have A: "pre C1 (pre C2 P) l s" by(simp)
  from Aseq(2)[OF Aseq(3)] Aseq(1)[OF _ A]
  show ?case by simp
next
  case (Awhile A b C)
  then obtain I S E   where A: "A = (I,S,E )"  using prod_cases3 by blast
  from Awhile show ?case unfolding A by simp
qed simp_all

lemma vc_mono: "(l s. P l s  P' l s)  vc C P  vc C P'"
  apply (induct C arbitrary: P P')
       apply auto 
  subgoal using pre_mono by metis 
  subgoal using pre_mono by metis
  done

subsubsection ‹Soundness:›
 
abbreviation "preSet U C l s == (Ball U (%u. case u of (x,e)  l x = preT C e s))"
abbreviation "postSet U l s == (Ball U (%u. case u of (x,e)  l x = e s))"

fun ListUpdate where
  "ListUpdate f [] l = f"
| "ListUpdate f ((x,e)#xs) q = (ListUpdate f xs q)(x:=q e x)"

lemma allg: 
  assumes U2: "l s n x. x fst ` upds  A (l(x := n))  = A l"
  shows
    "fst ` set xs  fst ` upds  A (ListUpdate l'' xs q) = A l''" 
proof (induct xs) 
  case (Cons a xs)
  obtain x e where axe: "a = (x,e)" by fastforce 
  have "A (ListUpdate l'' (a # xs) q) 
    = A ((ListUpdate l'' xs q)(x := q e x))  " unfolding axe by(simp)
  also have
    " =  A  (ListUpdate l'' xs q)  "
    apply(rule U2)
    using Cons axe by force
  also have " = A l'' "
    using Cons by force
  finally show ?case .
qed simp  

fun ListUpdateE where
  "ListUpdateE f []   = f"
| "ListUpdateE f ((x,v)#xs)  = (ListUpdateE f xs  )(x:=v)"

lemma ListUpdate_E: "ListUpdateE f xs = ListUpdate f xs (%e x. e)"
  apply(induct xs) apply(simp_all)
  subgoal for a xs apply(cases a) apply(simp) done
  done
lemma allg_E: fixes A::assn2
    assumes 
   " (l s n x. x  fst ` upds  A (l(x := n)) = A l)" "fst ` set xs  fst ` upds"
   shows "A (ListUpdateE f xs) = A f"
proof -
  have " A (ListUpdate f xs (%e x. e)) = A f"
    apply(rule allg) 
    apply fact+ done
  then show ?thesis by(simp only: ListUpdate_E)
qed 

lemma ListUpdateE_updates: "distinct (map fst xs)  x  set xs  ListUpdateE l'' xs (fst x) = snd x"
proof (induct xs)
  case Nil
  then show ?case apply(simp) done
next
  case (Cons a xs)
  show ?case
  proof (cases "fst a = fst x")
    case True
    then obtain y e where a: "a=(y,e)" by fastforce
    with True have fstx: "fst x=y" by simp
    from Cons(2,3) fstx  a have a2: "x=a"
      by force
    show ?thesis unfolding a2 a by(simp)
  next
    case False
    with Cons(3) have A: "xset xs" by auto
    obtain y e where a: "a=(y,e)" by fastforce
    from Cons(2) have B: "distinct (map fst xs)" by simp 
    from Cons(1)[OF B A] False
      show ?thesis unfolding a by(simp)  
  qed 
qed
  
    
lemma ListUpdate_updates: "x  fst ` (set xs)  ListUpdate l'' xs (%e. l) x = l x"
proof(induct xs)
  case Nil
  then show ?case by(simp)
next
  case (Cons a xs)
  obtain q p where axe: "a = (p,q)" by fastforce 
  from Cons show ?case unfolding axe
    apply(cases "x=p")  
    by(simp_all)
qed
  
abbreviation "lesvars xs == fst ` (set xs)"
  
fun preList where
  "preList [] C l s = True"
| "preList ((x,e)#xs) C l s = (l x = preT C e s  preList xs C l s)"
        
lemma preList_Seq: "preList upds (C1;; C2) l s = preList (map (λ(x, e). (x, preT C2 e)) upds) C1 l s"
proof (induct upds)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a by (simp)
qed

lemma support_True[simp]: "support (λa b. True) = {}" 
  unfolding support_def 
  by fast
  
lemma support_preList: "support (preList upds C1)  lesvars upds"
proof (induct upds)
  case Nil
  then show ?case by simp 
next
  case (Cons a upds)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a apply (simp)
    apply(rule subset_trans[OF support_and])
    apply(rule Un_least)
    subgoal apply(rule subset_trans[OF support_eq])
      using supportE_twicepreT subset_trans  supportE_single2 by simp
    subgoal by auto
    done
qed
  
  
lemma preListpreSet: "preSet (set xs) C l s  preList xs C l s"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a by (simp)
qed

lemma preSetpreList: "preList xs C l s   preSet (set xs) C l s"
proof (induct xs) 
  case (Cons a xs)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a
    by(simp)
qed simp


(* surprise. but makes sense, if the clauses are contradictory on the 
    left side, so are they on the right side *)
lemma preSetpreList_eq: "preList xs C l s = preSet (set xs) C l s"
proof (induct xs) 
  case (Cons a xs)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a
    by(simp)
qed simp  


fun postList where
  "postList []  l s = True"
| "postList ((x,e)#xs)  l s = (l x = e s  postList xs l s)"

  
lemma support_postList: "support (postList xs)  lesvars xs"
proof (induct xs)    
  case (Cons a xs)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a
    apply(simp) apply(rule subset_trans[OF support_and])
    apply(rule Un_least)
    subgoal apply(rule subset_trans[OF support_eq])
      using supportE_twicepreT subset_trans  supportE_single2 by simp
    subgoal by(auto)
      done   
qed simp
  
lemma postpreList_inv: assumes "S s = S (postQ C s)" 
  shows "postList (map (λ(x, e). (x, λs. e (S s))) upds) l s =  preList (map (λ(x, e). (x, λs. e (S s))) upds) C l s"
proof (induct upds) 
  case (Cons a upds)
  obtain y e where axe: "a = (y,e)" by fastforce    
  
  from Cons show ?case unfolding axe apply(simp) 
      apply(simp only: TQ) using assms by auto
qed simp
  
  
  
lemma postList_preList: "postList (map (λ(x, e). (x, preT C e)) upds) l s = preList upds C l s"
proof (induct upds) 
  case (Cons a xs)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a
    by(simp)
qed simp
  
lemma postSetpostList: "postList xs l s   postSet (set xs) l s"
proof (induct xs) 
  case (Cons a xs)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a
    by(simp)
qed simp
  

lemma postListpostSet: "postSet (set xs) l s  postList xs l s"
proof (induct xs) 
  case (Cons a xs)
  obtain y e where a: "a=(y,e)" by fastforce
  from Cons show ?case unfolding a
    by(simp)
qed simp


lemma ListAskip: "preList xs Askip l s = postList xs  l s"
  apply(induct xs)
   apply(simp) by force

lemma SetAskip: "preSet U Askip l s = postSet U l s"
by simp

lemma ListAassign: "preList upds (Aassign x1 x2) l s = postList upds l (s[x2/x1])"
  apply(induct upds)
   apply(simp) by force

lemma SetAassign: "preSet U (Aassign x1 x2) l s = postSet U l (s[x2/x1])"
by simp


lemma ListAconseq: "preList upds (Aconseq x1 x2 x3 C) l s = preList upds C l s"
  apply(induct upds)
   apply(simp) by force

lemma SetAconseq: "preSet U (Aconseq x1 x2 x3 C) l s = preSet U C l s"
by simp

lemma ListAif1: "bval b s  preList upds (IF b THEN C1 ELSE C2) l s = preList upds C1 l s"
  apply(induct upds)
   apply(simp) by force
lemma SetAif1: "bval b s  preSet upds (IF b THEN C1 ELSE C2) l s = preSet upds C1 l s"
  apply(simp) done
lemma ListAif2: "~ bval b s  preList upds (IF b THEN C1 ELSE C2) l s = preList upds C2 l s"
  apply(induct upds)
   apply(simp) by force

lemma SetAif2: "~ bval b s  preSet upds (IF b THEN C1 ELSE C2) l s = preSet upds C2 l s"
  apply(simp) done
 
    
(*
  In upds we collect pairs of logical variables and time expressions, these logical variables
  are bound to the value of these expressions. postList upds C l s is an assertion stating that
  for every (x,e) in upds, l x = e s; preList upds C l s does the same, but pulls the expression
  e through the command c, i.e. stating for ever (x,e) in upds, l x = preT C e s. 

  we have to make sure, that no variable is assigned twice (the 5th premise), as well as they are 
  different from all the logical variables that occur in the annotated program C (4th premise)

  we have to make sure that we can always choose new logical variables (premise 2, 3)
*)    
lemma vc_sound: "vc C Q  finite (support Q)  finite (varacom C)
   fst ` (set upds)  varacom C = {}  distinct (map fst upds)
    1 {%l s. pre C Q l s  preList upds C l s} strip C { time C  %l s. Q l s  postList upds l s}
   (l s. pre C Q l s  Q l (postQ C s))"
proof(induction C arbitrary: Q upds)    
  case (Askip Q upds)
  then show ?case
    apply(auto)
    apply(rule weaken_post[where Q="%l s. Q l s  preList upds Askip l s"])
     apply(simp add: Skip)  using ListAskip   
    by fast
next
  case (Aassign x1 x2 Q upds)
  then show ?case apply(safe) apply(auto simp add: Assign)[1]
     apply(rule weaken_post[where Q="%l s. Q l s  postList upds l s"]) 
      apply(simp only: ListAassign)
      apply(rule Assign) apply simp
    apply(simp only: postQ.simps pre.simps) done
next
  case (Aif b C1 C2 Q upds )
  then show ?case apply(auto simp add: Assign)
     apply(rule If2[where e="λa. if bval b a then  time C1 a else time C2 a"])
    subgoal
      apply(simp cong: rev_conj_cong)
      apply(rule ub_cost[where e'="time C1"])
       apply(simp) apply(auto)[1]
      apply(rule strengthen_pre[where P="%l s. pre C1 Q l s  preList upds C1 l s"]) 
        using ListAif1
       apply fast
      apply(rule Aif(1)[THEN conjunct1])
           apply(auto)  
      done
    subgoal 
      apply(simp cong: rev_conj_cong)
      apply(rule ub_cost[where e'="time C2"])  (* k=1 and *)
       apply(simp) apply(auto)[1]
      apply(rule strengthen_pre[where P="%l s. pre C2 Q l s  preList upds C2 l s"])
        using ListAif2
       apply fast
      apply(rule Aif(2)[THEN conjunct1])
           apply(auto)
      done
     apply auto apply fast+ done 
next
  case (Aconseq P' Qannot eannot C Q upds)  
  then obtain k where k: "k>0" and ih1: "vc C Qannot"
    and ih1': " (l s. P' l s   time C s  k * eannot s  (t. l'. pre C Qannot l' s  (Qannot l' t  Q l t)))"
    by auto                       
      
  have ih2': "l s. pre C Qannot l s  Qannot l (postQ C s)"
    apply(rule Aconseq(1)[THEN conjunct2]) using Aconseq(2-6) by auto    
    
  have G1: "1 {λl s. P' l s  preList upds ({P'/Qannot/eannot} CONSEQ C) l s} strip C
         { eannot  λl s. Q l s  postList upds l s}"
  proof (rule conseq[rotated])
    show "1 {λl s. pre C Qannot l s  preList upds C l s} strip C { time C  λl s. Qannot l s  postList upds l s}"
    apply(rule Aconseq(1)[THEN conjunct1])
      using Aconseq(2-6) by auto  
  next
    show "k>0. l s. P' l s  preList upds ({P'/Qannot/eannot} CONSEQ C) l s 
              time C s  k * eannot s 
              (t. l'. (pre C Qannot l' s  preList upds C l' s) 
                        (Qannot l' t  postList upds l' t  Q l t  postList upds l t))"
    proof(rule exI[where x=k], safe)
      fix l s
      assume P': "P' l s" and prelist: "preList upds ({P'/Qannot/eannot} CONSEQ C) l s"
      then show "time C s  k * eannot s" using ih1' by simp
                   
      fix t
      ― ‹we now have to construct a logical environment, that both
          * satisfies the annotated postcondition Qannot (we obtain it from the first IH)
          * lets the updates come true (we have to show that resetting these logical variables
              does not interfere with the other variables)›  
      
      from ih1' P' have satQan:"(l'. pre C Qannot l' s  (Qannot l' t  Q l t))" by simp
      then obtain l' where i': "pre C Qannot l' s" and ii': "(Qannot l' t  Q l t)" by blast
          
      let ?upds' = "(map (%(x,e). (x,preT C e s)) upds)"
      let ?l'' = "(ListUpdateE l' ?upds')"
        
      {
        fix l s n x
        assume "x  fst ` (set upds)"
        then have "x  support (pre C Qannot)" using Aconseq(5) support_pre by auto
        from assn2_lupd[OF this] have "pre C Qannot (l(x := n))  = pre C Qannot l" .
      } note U2=this 
      {
        fix l s n x
        assume "x  fst ` (set upds)"
        then have "x  support Qannot" using Aconseq(5) by auto
        from assn2_lupd[OF this] have "Qannot (l(x := n))  = Qannot l" .
      } note K2=this  
              
      have "pre C Qannot ?l''  = pre C Qannot l'  "
        apply(rule allg_E[where ?upds="set upds"]) apply(rule U2) by force+
      with i' have i'': "pre C Qannot ?l'' s" by simp
      
      have "Qannot ?l'' = Qannot l'"
        apply(rule allg_E[where ?upds="set upds"]) apply(rule K2) by force+              
      then have K: "(%l' s. Qannot l' t  Q l t) ?l'' s = (%l' s. Qannot l' t  Q l t) l' s"
        by simp
      with ii' have ii'': "(Qannot ?l'' t  Q l t)" by simp
            
      have xs_upds: "map fst ?upds' = map fst upds"
           by auto          
      have resets: "x. x  set ?upds'  ListUpdateE l' ?upds' (fst x) = snd x" apply(rule ListUpdateE_updates)
         apply(simp only: xs_upds) using Aconseq(6) apply simp
           apply(simp) done         
        
      have A: "preList upds C ?l'' s" 
      proof (rule preListpreSet,safe,goal_cases)
        case (1 x e)
        then have "(x, preT C e s)  set ?upds'"
          by fastforce
        from resets[OF this, simplified]
        show ?case .
      qed  
          
      have B: "Qannot ?l'' t  postList upds ?l'' t  postList upds l t"
      proof (rule postListpostSet, safe, goal_cases)        
        case (1 x e)            
        from postSetpostList[OF 1(2)] have g: "postSet (set upds) ?l'' t" .
        with 1(3) have A: "?l'' x = e t"
          by fast            
        from 1(3) resets[of "(x,preT C e s)"] have   B: "?l'' x = snd (x, preT C e s)"
          by fastforce
        from A B have X: "e t = preT C e s" by fastforce
        from preSetpreList[OF prelist] have "preSet (set upds) ({P'/Qannot/eannot} CONSEQ C) l s" .
        with 1(3) have Y: "l x = preT C e s" apply(simp) by fast
        from X Y show ?case by simp
      qed 
          
      show "l'. (pre C Qannot l' s  preList upds C l' s) 
                  (Qannot l' t  postList upds l' t  Q l t  postList upds l t)"        
        apply(rule exI[where x="?l''"], safe)        
        using i'' A ii'' B by auto            
    qed fact 
  qed
    
  have G2: "l s. P' l s  Q l (postQ C s)"
  proof -
    fix l s
    assume "P' l s"   
    with ih1' ih2' show "Q l (postQ C s)" by blast
  qed
     
  show ?case using G1 G2 by auto  
next
  case (Aseq C1 C2 Q upds)
   
  let ?P = "(λl s. pre (C1;; C2) Q l s  preList upds (C1;;C2) l s  )"
  let ?P' = "support Q  varacom C1  varacom C2  lesvars upds"  
  
  have finite_varacom: "finite (varacom (C1;; C2))" by fact 
  have sup_L: "support (preList upds (C1;;C2))  lesvars upds"
    apply(rule support_preList) done 
  
  ― ‹choose a fresh logical variable ?y in order to pull through the cost of the second command›
  let ?y = "SOME x. x  ?P'" 
  have fP': "finite (?P')" using finite_varacom Aseq(4,5)   apply simp done
  from fP' have "x. x  ?P'" using infinite_UNIV_listI
    using ex_new_if_finite by metis
  hence ynP': "?y  ?P'" by (rule someI_ex) 
  hence ysupC1: "?y  varacom C1" using support_pre by auto
  have sup_B: "support ?P  ?P'"                         
    apply(rule subset_trans[OF support_and]) apply simp using support_pre sup_L by blast   
        
  ― ‹we show the first goal: we can deduce the desired Hoare Triple›  
  have C1: "1 {λl s. pre (C1;; C2) Q l s  preList upds (C1;; C2) l s} strip C1;; strip C2
         { time (C1;; C2)  λl s. Q l s  postList upds l s}"
  proof (rule Seq[rotated])
    ― ‹start from the back: we can simply use the IH for C2, 
          and solve the side conditions automatically›
    show "1 {(%l s. pre C2 Q l s   preList upds C2 l s )} strip C2 { time C2  (%l s. Q l s  postList upds l s)}"
      apply(rule Aseq(2)[THEN conjunct1])  
      using Aseq(3-7) by auto   
  next    
    ― ‹prepare the new updates: pull them through C2 and save the new execution time of C2 in ?y›    
    let ?upds = "map (λa. case a of (x,e)  (x, preT C2 e )) upds"
    let ?upds' = "(?y,time C2)#?upds"   
      
    have dst_upds': "distinct (map fst ?upds')" 
      using  ynP' Aseq(7) apply simp apply safe 
        using image_iff apply fastforce  by (simp add: case_prod_beta' distinct_conv_nth) 
    
    ― ‹now use the first induction hypothesis (specialised with the augmented upds list, and the
        weakest precondition of Q through C as post condition)›
    have IH1s: "1 {λl s. pre C1 (pre C2 Q) l s  preList ?upds' C1 l s} strip C1
                    { time C1  λl s. pre C2 Q l s  postList ?upds' l s}"
      apply(rule Aseq(1)[THEN conjunct1])
        using Aseq(3-7) ysupC1 dst_upds' by auto  
    
    ― ‹glue it together with a consequence rule, side conditions are automatic›
    show " 1 {λl s. (pre (C1;; C2) Q l s  preList upds (C1;; C2) l s)  l ?y = preT C1 (time C2) s} strip C1
     { time C1  λl s. (λl s. pre C2 Q l s  preList upds C2 l s) l s  time C2 s  l ?y}" 
      apply(rule conseq_old[OF _ IH1s]) 
      by (auto simp: preList_Seq postList_preList)  
  next
    ― ‹solve some side conditions showing that, ?y is indeed fresh›
    show "?y  support ?P"
      using sup_B ynP' by auto        
    have F: "support (preList upds C2)  lesvars upds"  
      apply(rule support_preList) done 
    have "support (λl s. pre C2 Q  l s  preList upds C2 l s)  ?P'"
      apply(rule subset_trans[OF support_and]) using F support_pre by blast
    with ynP'
    show "?y  support (λl s. pre C2 Q l s  preList upds C2 l s)" by blast 
  qed simp
   
  ― ‹we show the second goal: weakest precondition implies, that
        Q holds after the execution of C1 and C2›  
  have C2: "l s. pre (C1;; C2) Q l s  Q l (postQ (C1;; C2) s)"
  proof -
    fix l s
    assume p: "pre (C1;; C2) Q l s"
    have A: "l s. pre C1 (pre C2 Q )  l s  pre C2 Q  l (postQ C1 s)"
      apply(rule Aseq(1)[where upds="[]", THEN conjunct2])
      using Aseq by auto 
    have B: "(l s. pre C2 Q  l s  Q l (postQ C2 s))" 
      apply(rule Aseq(2)[where upds="[]", THEN conjunct2])
      using Aseq by auto        
    from p A B show "Q l (postQ (C1;; C2) s)" by simp
  qed
    
  show ?case using C1 C2 by simp 
next
  case (Awhile A b C Q upds)
  
  ― ‹Let us first see, what we got from the induction hypothesis:›
  obtain I S E  where [simp]: "A = (I,(S,(E)))" using prod_cases3 by blast
  with vc (Awhile A b C) Q have "vc (Awhile (I,S,E) b C) Q" by blast
  then  have vc: "vc C I"  and  pre2: "l s. I l s  ¬ bval b s   Q l s  1  E s  S s = s"
    and IQ2: "l s. I l s  bval b s 
                         pre C I l s
                            1 + preT C E s + time C s  E s  S s = S (postQ C s)"  by auto      
    
  ― ‹the logical variable x represents the number of loop unfoldings›
       
  
  from IQ2 have IQ_in: "l s. I l s    bval b s  S s = S (postQ C s)" by auto
  
  have inv_impl: "l s.  I l s    bval b s   pre C I  l s" using IQ2 by auto    
  
  have yC: " lesvars upds  varacom C = {}" using Awhile(5) by auto
     
  let ?upds = "map (%(x,e). (x, %s. e (S s))) upds"
  let ?INV = "%l s. I l s  postList ?upds l s"      
    
  have "lesvars upds  support I = {}" using Awhile(5) by auto
    
    
  ― ‹we need a fresh variable ?z to remember the time bound of the tail of the loop›
  let ?P="lesvars upds  varacom ({A} WHILE b DO C)"
  let ?z="SOME z::lvname. z  ?P"
  have "finite ?P" using Awhile by auto 
  hence "z. z?P"  using infinite_UNIV_listI
    using ex_new_if_finite by metis
  hence znP: "?z  ?P" by (rule someI_ex) 
  from znP have (* znx:  "?z≠x" 
    and *) zny:  "?z  lesvars upds"
    and zI:   "?z  support I" 
    and blb:  "?z  varacom C" by (simp_all)
      
  from Awhile(4,6) have 23: "finite (varacom C)" 
    and  26: "finite (support I)" by auto 
   
  have "l s.  pre C I  l s  I l (postQ C s)"    
    apply(rule Awhile(1)[THEN conjunct2]) by(fact)+       
  hence step: "l s. pre C I l s  I l (postQ C s)" by simp
 
      
  ― ‹we adapt the updates, by pulling them through the loop body 
      and remembering the time bound of the tail of the loop›
  let ?upds = "map (λ(x, e). (x, λs. e (S s))) upds"
  have fua: "lesvars ?upds = lesvars upds"
    by force
  let ?upds' = "(?z,E) # ?upds" 
     
      
  have g: "e. e  S = (%s. e (S s))" by auto
       
  ― ‹show that the Hoare Rule is derivable›    
  have G1: "1 {λl s. I l s  preList upds ({(I, S, E)} WHILE b DO C) l s} WHILE b DO strip C
         { E  λl s. Q l s  postList upds l s}"
  proof(rule conseq_old)
    show "1 {λl s. I l s  postList ?upds l s} WHILE b DO strip C
              { E  λl s. (I l s  postList ?upds l s)  ¬bval b s }"
    ― ‹We use the While Rule and then have to show, that ...›
    proof(rule While, goal_cases) 
      ― ‹A) the loop body preserves the loop invariant›
      have "lesvars ?upds'  varacom C = {}"
        using yC blb by(auto)
          
      have z: "(fst  (λ(x, e). (x, λs. e (S s)))) = fst" by auto
      have "distinct (map fst ?upds')"
        using Awhile(6) zny by (auto simp add: z)       
      
      ― ‹for showing preservation of the invariant, use the consequence rule ...›
      show "1 {λl s. (I l s  postList ?upds l s)  bval b s  preT C E s = l ?z}
       strip C {  time C  λl s. (I l s  postList ?upds l s)  E s  l ?z}" 
      proof (rule conseq_old)
        ― ‹... and employ the induction hypothesis, ...›
        show " 1 {λl s. pre C I l s  preList ?upds' C l s} strip C
                { time C  λl s. I l s  postList ?upds' l s}"
          apply(rule Awhile.IH[THEN conjunct1]) by fact+              
      next
        ― ‹finally we have to prove the side condition.›
        show "k>0. l s. (I l s  postList ?upds l s)  bval b s  preT C E s = l ?z
                    (pre C I l s  preList ?upds' C l s)  time C s  k * time C s"
          apply(rule exI[where x=1]) apply(simp)
        proof (safe, goal_cases)              
          case (2 l s)
          note upds_invariant=postpreList_inv[OF IQ_in[OF 2(1)]]
          from 2  upds_invariant   show ?case by auto
        next
          case (1 l s) then show ?case using inv_impl by auto
        qed   
      qed auto
    next
      ― ‹B) the invariant with number of loop unfoldings greater than 0 implies true loop guard
             and running time is correctly bounded›
      show "l s. bval b s   I l s  postList ?upds l s  1 + preT C E s + time C s  E s"        
      proof (clarify, goal_cases)
        case (1 l s)          
        show ?case using IQ2 1(1,2) by auto            
      qed
    next
      ― ‹C) the invariant with number of loop unfoldings equal to 0 implies false loop guard
             and running time is correctly bounded›
      show "l s.  ¬ bval b s  I l s  postList ?upds l s   1  E s"
      proof (clarify, goal_cases)
        case (1 l s)  
        then show ?case 
          using pre2 1(2) by auto
      qed  
    next
      ― ‹D) ?z is indeed a fresh variable›
      have pff: "?z  lesvars ?upds" apply(simp only: fua) by fact
      have "support (λl s. I l s  postList ?upds l s)  support I  support (postList ?upds)"
        by(rule support_and) 
      also have "support (postList ?upds)  lesvars ?upds"
           apply(rule support_postList) done 
      finally 
      have "support (λl s. I l s  postList ?upds l s)  support I  lesvars ?upds"
        by blast 
      thus "?z  support (λl s. I l s  postList ?upds l s)" 
        apply(rule contra_subsetD) 
        using zI pff by(simp)
    qed
  next
    show "k>0. l s. I l s   preList upds ({(I, S, E)} WHILE b DO C) l s 
              (I l s  postList (map (λ(x, e). (x, λs. e (S s))) upds) l s)  E s  k * E s"
       apply(rule exI[where x=1])   apply(auto)  apply(simp only: postList_preList[symmetric] ) apply (auto)
        apply(simp only:   g)  
        done
  next
    show "l s. (I l s  postList (map (λ(x, e). (x, λs. e (S s))) upds) l s)  ¬ bval b s   Q l s  postList upds l s"
      using pre2  by(induct upds, auto)  
  qed
    
  have G2: "l s. pre ({A} WHILE b DO C) Q l s  Q l (postQ ({A} WHILE b DO C) s)"  
  proof -
    fix l s
    assume "pre ({A} WHILE b DO C) Q l s"
    then have I: "I l s" by simp
    { fix n
    have "E s = n  I l s  Q l (postQ ({A} WHILE b DO C) s)"
    proof (induct n arbitrary: s l rule: less_induct)
      case (less n)
      then show ?case 
      proof (cases "bval b s")
        case True
        with less IQ2 have "pre C I l s" and S: "S s = S (postQ C s)" and t: "1 + preT C E s + time C s  E s" by auto
        with step have I': "I l (postQ C s)" and "1 + E (postQ C s) + time C s  E s" using TQ by auto
        with less have "E (postQ C s) < n" by auto    
        with less(1) I' have "Q l (postQ ({A} WHILE b DO C) (postQ C s))" by auto
        with step show ?thesis using S by simp
      next
        case False
        with pre2 less(3) have "Q l s" "S s = s" by auto
        then show ?thesis by simp
      qed
    qed
    }
    with I show "Q l (postQ ({A} WHILE b DO C) s)" by simp   
  qed
   
  show ?case  using G1  G2 by auto    
qed
 


 


corollary vc_sound':
  assumes "vc C Q" 
          "finite (support Q)" "finite (varacom C)"
          "l s. P l s  pre C Q l s" 
  shows "1 {P} strip C {time C  Q}"
proof -
  show ?thesis
    apply(rule conseq_old)
      prefer 2 apply(rule vc_sound[where upds="[]", OF assms(1-3), THEN conjunct1])      
    using assms(4) apply auto 
    done 
qed

lemma preT_constant: "preT C (%_. a) = (%_. a)"
  apply(induct C) by (auto)
 

corollary vc_sound'':
  " vc C Q; (k>0. l s. P l s  pre C Q l s  time C s  k * e s);
  finite (support Q); finite (varacom C)  1 {P} strip C {e  Q}"
  apply(rule ub_cost[where e'="time C"])
   apply(auto)
  apply(rule vc_sound') by auto

subsubsection ‹Completeness:›

lemma vc_complete:
  "1 {P} c { e  Q}    C. strip C = c  vc C Q 
   (l s. P l s  pre C Q l s  Q l (postQ C s))
   (k. l s. P l s   time C s  k * e s)  "
  (is "_    C. ?G P c Q C e")
proof (induction  rule: hoare1.induct )
  case Skip
  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)" apply (simp del: fun_upd_apply) apply(auto) done qed
next
  case (Seq P x e2' c1 e1 Q e2 c2 R e) 
  from Seq.IH(1)   obtain C1 where "?G (λl s. P l s  l x = e2' s) c1 (λa b. Q a b  e2 b  a x) C1 e1 " by blast
  then obtain k where ih1: "strip C1 = c1"
    "vc C1 (λa b. Q a b  e2 b  a x)"
    "l s. P l s  l x = e2' s  pre C1 (λla sa. (Q la sa  e2 sa  la x)) l s"
    "(l s. P l s  l x = e2' s   time C1 s  k * e1 s)" 
    "l s.  P l s  l x = e2' s  Q l (postQ C1 s)  e2 (postQ C1 s)  l x" 
    apply auto done
  
  from Seq.IH(2)   obtain C2 where ih2: "?G Q c2 R C2 e2  " by blast
  then obtain k2 where ih2: "strip C2 = c2"
    "vc C2 R"
    "(l s. Q l s  pre C2 R l s)"
    "(l s. Q l s   time C2 s  k2 * e2 s)"
    "l s . Q l s  R l (postQ C2 s)"  apply auto done
  
  show ?case (is "C. ?C C")
  proof 
    show "?C(Aseq (Aconseq P Q (time C1) C1) C2)" (* with Q being (λla sa. (Q la sa ∧ e2 sa ≤ la x)) some less mono is needed *)
    proof (safe, goal_cases)
      case 1
      then show ?case apply(simp add: ih1(1) ih2(1)) done
    next
      case 2
      then show ?case apply(simp) apply(safe)
        subgoal apply(rule vc_mono) prefer 2 apply (rule ih1(2)) apply(auto) done
        subgoal apply(rule exI[where x=1]) apply safe
          subgoal by(auto)              
          subgoal for l s t
            apply(rule exI[where x="l(x:= e2' s)"])              
            apply(safe)              
            subgoal apply(rule pre_mono) prefer 2 apply (rule ih1(3))                
                apply(subst assn2_lupd) using Seq(3) by auto                
            subgoal apply(rule ih2(3)) using assn2_lupd[OF Seq(4)] by auto               
            done
          done
        subgoal by (rule ih2(2)) 
        done
    next
      case (3 l s)
      then show ?case apply(simp) done
    next
      
      case (4 l s)      
      from 4 have "P (l(x:=e2' s)) s" using assn2_lupd[OF Seq(3)] by simp
      with ih1(5)[where l="l(x:=e2' s)"]
      have "Q (l(x := e2' s)) (postQ C1 s)" by simp
      then have "Q l (postQ C1 s)" using assn2_lupd[OF Seq(4)] by simp
      with ih2(3) have "Q l (postQ C1 s)" by simp 
      with  ih2(5)
      show ?case apply(auto) done 
    next
      case 5
      from ih1(4) have
        gg: "l s. P l s; e2' s = l x    time C1 s  k * e1 s" by auto
      
      show ?case
      proof (rule exI[where x="(max k  k2)"], safe, goal_cases)
        case (1 l s)
        have xnP: "x  support P" by fact
        have 41: "P (l(x := e2' s)) s"
          apply(subst assn2_lupd)
           apply(fact xnP)
          apply(fact 5) done
        
        have A: "  time C1 s  k * e1 s"
          apply(rule gg[where l="l(x:=e2' s)"])
           apply(rule 41)
          apply(simp)  done  
        
        have B: "preT C1 (time C2) s  k2 * e2' s"
        proof - 
          from  1 have "P (l(x := e2' s)) s" using assn2_lupd[OF xnP] by simp
          
          have F: "Q (l(x:=e2' s)) (postQ C1 s)  e2 (postQ C1 s)  (l(x:=e2' s)) x"
            apply(rule ih1(5)[where l="l(x:=e2' s)" and s=s]) 
             apply(fact)
            apply(simp) done
          then have " time C2 (postQ C1 s)  k2 * e2 (postQ C1 s)" using ih2(4) by auto
          with F have "time C2 (postQ C1 s)  k2 * e2' s"
            using order_subst1 by fastforce 
          then show "preT C1 (time C2) s  k2 * e2' s" using TQ by simp  
        qed  
        have "time C1 s + preT C1 (time C2) s  k  * e1 s + k2 * e2' s" using A B by linarith
        also have "  (max k  k2) * e1 s + (max k  k2) * e2' s" 
        using nat_mult_max_left by auto
      also have " = (max k  k2) * (e1 s + e2' s)" by algebra
      also have "  (max k  k2) * e s" using Seq(5)[OF 1] by auto 
      finally
      have "time C1 s + preT C1 (time C2) s  (max k  k2) * e s" .
      then show ?case
        by auto  
    qed
  qed
  qed
  
next
  case (If P b c1 e1 Q c2) 
  from If.IH(1) obtain C1 where "?G (λl s. P l s  bval b s) c1 Q C1 e1"
    by blast
  then obtain k1 where ih1: " strip C1 = c1  vc C1 Q  (l s. P l s  bval b s  pre C1 Q l s  Q l (postQ C1 s))   ( l s. P l s  bval b s  time C1 s  k1 * e1 s) "
      by blast
  from If.IH(2) obtain C2 where "?G (λl s. P l s  ¬bval b s) c2 Q C2 e1"
    by blast
  then obtain k2 where ih2: " strip C2 = c2  vc C2 Q  (l s. P l s  ¬bval b s  pre C2 Q l s  Q l (postQ C2 s))   ( l s. P l s  ¬bval b s  time C2 s  k2 * e1 s )"
    by blast
  define k' where "k' == max (k1+1) (k2+1)"
  show ?case (is "C. ?C C")
  proof
    show "?C(Aif b C1 C2)"
      apply(safe)
          prefer 5
      apply(rule exI[where x="k'"]) apply(safe)
      subgoal for l s  apply(auto)
      proof(goal_cases)
        case 1
        with ih1 have "time C1 s  k1 * e1 s" by blast
        then have "Suc (time C1 s)  1 + k1 * e1 s" by auto
        also have "  k' + k1 * e1 s" unfolding k'_def by(auto)
        also have "  k' + k' * e1 s" unfolding k'_def
          by (simp add: max_def) 
        finally show ?case .
      next
        case 2
        with ih2 have "time C2 s  k2 * e1 s" by blast
        then have "Suc (time C2 s)  1 + k2 * e1 s" by auto
        also have "  k' + k2 * e1 s" unfolding k'_def by(auto)
        also have "  k' + k' * e1 s" unfolding k'_def
          by (simp add: max_def) 
        finally show ?case .
      qed       
      using ih1 ih2 apply(simp) 
      using ih1 ih2 apply(auto)
      done  
  qed  
next
  case (While P b e' y c e'' e)
  have supportPre: "support (λl s. P l s  bval b s  e' s = l y)  support P  {y}"
  using support_and support_single   by fast
  from   While.IH  obtain C where
    ih: "?G (λl s. P l s  bval b s  e' s = l y) c (λa b. P a b  e b  a y) C e''"
    using supportPre by blast
  then obtain k where ih2: "vc C (λa b. P a b  e b  a y)"
    "l s.  P l s ; bval b s ; e' s = l y   pre C (λla sa. (P la sa  e sa  la y)) l s" 
    "l s.  P l s ; bval b s ; e' s = l y     time C s  k * e'' s " 
    "l s. P l s ; bval b s ; e' s = l y  P l (postQ C s)  e (postQ C s)  l y"
    by fast
   
  let ?S = "postQs C b"
  {
    fix l s n
    have "e s = n  P l s  postQs_dom (C, b, s)  P l (?S s)  ~ bval b (?S s)"
    proof (induct n arbitrary: l s rule: less_induct)
      case (less x)
      show ?case
      proof (cases "bval b s")
        case True
        with While(2) less(3) have "1 + e' s + e'' s  e s" by auto
        then have e'e: "e' s < e s" by simp
        have "P (l(y:=e' s)) s" using less(3) assn2_lupd[OF While(4)] by simp    
        from ih2(4)[OF this] True have ee': "e (postQ C s)  e' s" and P': "P (l(y := e' s)) (postQ C s)" by auto
        from P' have P'': "P l (postQ C s)" using less(3) assn2_lupd[OF While(4)] by simp 
        from ee' e'e less(2) have "e (postQ C s) < x" by auto 
        from less(1)[OF this _ P''] have d: "postQs_dom (C, b, postQ C s)" 
              and p: "P l (postQs C b (postQ C s))"
              and b: "¬ bval b (postQs C b (postQ C s))" by auto
        have d': "postQs_dom (C, b, s)"
          by (simp add: d postQs.domintros)           
        have p': " P l (postQs C b s) "
          using True d p postQs.domintros postQs.psimps by fastforce 
        have b': "¬ bval b (postQs C b s)"
          by (metis b d postQs.domintros postQs.pelims)
          
        from d' p' b' show ?thesis by auto
      next
        case False
        then have 1: "postQs_dom (C, b, s)"
          using postQs.domintros by blast    
        then have 2: "?S s = s" using postQs.psimps False by force
        from 1 2 less(3) False show ?thesis by simp
      qed
    qed
  }
  then have Pdom: "l s. P l s  postQs_dom (C, b, s)  P l (?S s)  ~ bval b (?S s)" by simp
    
  have S1: "l s. P l s  P l (?S s)" using Pdom by simp
  have S2: "l s. P l s  ~ bval b (?S s)" using Pdom by simp  
  have S3: "l s. P l s  bval b s  ?S s = ?S (postQ C s)" using postQs.psimps Pdom by simp
  have S4: "l s. P l s  ¬ bval b s  ?S s = s" using postQs.psimps Pdom by simp
      
  let ?w = "{(P,?S,(%s. max k 1 * e s))} WHILE b DO (Aconseq (λl s. P l s  bval b s) (λla sa. P la sa  e sa  la y) (time C) C)"
  
  show ?case (is "C. ?C C")
  proof
    show "?C ?w" 
    proof (safe, goal_cases)
      case 1
      then show ?case using ih by(simp) 
    next
      case 2
      then show ?case 
      proof(simp, safe, goal_cases)
        case (1 l s)         
        from 2 have z: "P (l(y := e' s)) s "
          using 1 assn2_lupd[OF While(4)]  by metis
        from ih2(3)[where l="l(y := e' s)" and s=s]
        have A: " time C s  k * e'' s " using 1 z by(simp)         
        
        from ih2(4)[where l="l(y := e' s)" and s=s]
        have "e (postQ C s)  (l(y := e' s)) y" apply(simp) using 1 z by(simp) 
        then have "e (postQ C s)  e' s" by simp 
        
        with TQ have B: "preT C e s  e' s" by simp 
        let ?eskal = "(λs. max k (Suc 0) * e s)"
        have "preT C (λs. max k (Suc 0) * e s) s = max k (Suc 0) * preT C e s"
          using preT_linear by simp
        with B have  B: "preT C ?eskal s  max k (Suc 0) * e' s" by auto
        
        from  While.hyps(2) 1 have C: "1 + e' s + e'' s  e s" by auto       
        have "Suc (preT C ?eskal s + time C s)  1 + (max k 1) * e' s + k * e'' s"
          using A B by linarith
        also have "  (max k 1) + (max k 1) * e' s + (max k 1) * e'' s"
          using nat_mult_max_left by auto
        also have " = (max k 1) * (1 + e' s + e'' s)"
          by algebra
        also have "  (max k 1) * e s" 
          using C by (metis mult.assoc mult_le_mono2) 
        finally have "Suc (preT C ?eskal s + time C s)  ((max k 1) ) * e s" .
        thus ?case by auto
      next
        case (3 l s)
        with While.hyps(3) show ?case by auto      
      next
        case 5
        then show ?case
           apply(rule vc_mono)
           prefer 2 apply(fact ih2(1)) by auto
      next
        case 6
        show ?case apply(rule exI[where x="1"]) apply(safe)
          subgoal by simp
          subgoal for l s t apply(rule exI[where x="l(y:=e' s)"])
              
          proof (safe)
            assume 8: "P l s" and b: " bval b s"
            then have "P (l(y := e' s)) s" using assn2_lupd[OF While(4)]  by metis 
            with b ih2(2)  show "pre C (λla sa. P la sa  e sa  la y) (l(y := e' s)) s"
              apply(auto) done
            fix t
            assume "P (l(y := e' s)) t"
            thus "P l t" using assn2_lupd[OF While(4)] by simp
          qed 
          done       
      qed (simp_all add: S4 S3)   
    next
      case 6
      show ?case apply(rule exI[where x="k+1"]) by auto 
    qed (simp_all add: S1 S2)
  qed 
next
  case (conseq P' e e' P Q Q' c) 
  then obtain C k where C: "strip C = c"
    "vc C Q"
    "(l s  . P l s  pre C Q  l s )"
    "(l s . P l s  Q l (postQ C s))"
    "(l s. P l s   time C s  k * e s)" by metis
  from conseq(1) obtain k2 where cons: " l s. P' l s  e s  k2 * e' s  (t. l'. P l' s  (Q l' t  Q' l t))" by auto
   
  show ?case
    apply(rule exI[where x="Aconseq P' Q (time C) C"])
    apply(safe)
    subgoal apply(simp) by(fact)  
    subgoal apply(simp)
      apply(safe)
      subgoal using C(2)   
          apply(fast) done
      subgoal 
        apply(rule exI[where x="k+1"])
        apply auto
        using C(2) cons C(3) by blast   
      done
    subgoal apply(rule pre_mono)        
      prefer 2 apply(simp) using C(3) conseq(1) apply fast        
      done      
    subgoal  
      apply(simp)
      using C(4) conseq(1,3) apply blast done
    apply(rule exI[where x="k*k2"]) apply(safe)
    subgoal for l s
      using C(5) cons apply(auto) 
    proof(goal_cases)
      case 1
      then have absch: "e s  k2 * e' s" "time C s  k  * e s" by blast+
      show ?case  
        using absch order_trans by fastforce
    qed
    done
qed 

end