Theory Nielson_VCGi

theory Nielson_VCGi
imports Nielson_Hoare "Vars"
begin

subsection "Optimized 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*(vname set)" "assn2*(vname set)" "tbd * (vname set)"  acom
  (‹({_'/_'/_}/ CONSEQ _)›  [0, 0, 0, 61] 61)|
  Awhile "(assn2*(vname set))*((state⇒state)*(tbd*((vname set*(vname ⇒ vname set)))))" 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 (C⇩1;; C⇩2) = (strip C⇩1;; strip C⇩2)" |
  "strip (IF b THEN C⇩1 ELSE C⇩2) = (IF b THEN strip C⇩1 ELSE strip C⇩2)" |
  "strip ({_/_/_} CONSEQ C) = strip C" |
  "strip ({_} WHILE b DO C) = (WHILE b DO strip C)"
  
  
  
text "support of an expression"

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)

 
fun varacom :: "acom ⇒ lvname set" where
  "varacom (C⇩1;; C⇩2)= varacom C⇩1 ∪ varacom C⇩2"
| "varacom (IF b THEN C⇩1 ELSE C⇩2)= varacom C⇩1 ∪ varacom C⇩2"
| "varacom ({(P,_)/(Qannot,_)/_} CONSEQ C)= support P ∪ varacom C ∪ support Qannot"
| "varacom ({((I,_),(S,(E,Es)))} WHILE b DO C) = support I ∪ varacom C "
| "varacom _ = {}"
     
  
fun varnewacom :: "acom ⇒ lvname set" where
  "varnewacom (C⇩1;; C⇩2)= varnewacom C⇩1 ∪ varnewacom C⇩2"
| "varnewacom (IF b THEN C⇩1 ELSE C⇩2)= varnewacom C⇩1 ∪ varnewacom C⇩2"
| "varnewacom ({_/_/_} CONSEQ C)= varnewacom C"
| "varnewacom ({(I,(S,(E,Es)))} WHILE b DO C) = varnewacom C"
| "varnewacom _ = {}"
  
lemma finite_varnewacom: "finite (varnewacom C)"
  by (induct C) (auto)



fun wf :: "acom ⇒ lvname set ⇒ bool" where
  "wf SKIP _ = True" |
  "wf (x ::= a) _ = True" |
  "wf (C⇩1;; C⇩2) S = (wf C⇩1 (S ∪ varnewacom C⇩2) ∧ wf C⇩2 S)" |
  "wf (IF b THEN C⇩1 ELSE C⇩2) S = (wf C⇩1 S ∧ wf C⇩2 S)" |
  "wf ({_/(Qannot,_)/_} CONSEQ C) S = (finite (support Qannot) ∧ wf C S)" |
  "wf ({(_,(_,(_,Es)))} WHILE b DO C) S = ( wf C S)"
    
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 (C⇩1;; C⇩2) e = preT C⇩1 (preT C⇩2 e)" |
  "preT ({_/_/_} CONSEQ C) e = preT C e" |
  "preT (IF b THEN C⇩1 ELSE C⇩2) e =
  (λs. if bval b s then preT C⇩1 e s else preT C⇩2 e s)" |
  "preT ({(_,(S,_))} WHILE b DO C) e = e o S"
  

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

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 (C⇩1;; C⇩2) s = postQ C⇩2 (postQ C⇩1 s)" |
  "postQ ({_/_/_} CONSEQ C) s = postQ C s" |
  "postQ (IF b THEN C⇩1 ELSE C⇩2) s =
  (if bval b s then postQ C⇩1 s else postQ C⇩2 s)" |
  "postQ ({(_,(S,_))} WHILE b DO C) s = S s"
  
  
  
(* function that, given a Command C and a set of variables 
  gives the set of variables, that Es depends on,
  meaning a set S where
  if s1 = s2 on S ⟶ ∀x:Es. postQ C s1 x = postQ C s2 x
*)
fun fune :: "acom ⇒ vname set ⇒ vname set" where
  "fune SKIP LV = LV" |
  "fune (x ::= a) LV = LV ∪ vars a" |
  "fune (C⇩1;; C⇩2) LV = fune C⇩1 (fune C⇩2 LV)" |
  "fune ({_/_/_} CONSEQ C) LV = fune C LV" |
  "fune (IF b THEN C⇩1 ELSE C⇩2) LV = vars b ∪ fune C⇩1 LV ∪ fune C⇩2 LV" |
  "fune ({(_,(S,(E,Es,SS)))} WHILE b DO C) LV = (⋃x∈LV. SS x)"
  
lemma fune_mono: "A ⊆ B ⟹ fune C A ⊆ fune C B"
proof(induct C arbitrary: A B)  
  case (Awhile x1 x2 C)
  obtain a b c d e f where a: "x1 = (a,b,c,d,e)" using prod_cases5 by blast
  from Awhile show ?case unfolding a by(auto)
qed (auto simp add: le_supI1 le_supI2)
  
  
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

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)



text‹Weakest precondition from annotated commands:›

  (* if the annotated command contains no loops,
  then the weakest precondition is just some mangled post condition
  in the other case, 
  the weakest precondition is essentially the annotated invariant
  of the first while loop, mangled somewhat by the commands
  preceding the loop. *)

fun pre :: "acom ⇒ assn2 ⇒ assn2" where
  "pre SKIP Q  = Q" |
  "pre (x ::= a) Q = (λl s. Q l (s(x := aval a s)))" |
  "pre (C⇩1;; C⇩2) Q  = pre C⇩1 (pre C⇩2 Q)" |
  "pre ({(P',Ps)/_/_} CONSEQ C) Q = P'" |
  "pre (IF b THEN C⇩1 ELSE C⇩2) Q =
  (λl s. if bval b s then pre C⇩1 Q l s else pre C⇩2 Q l s)" |
  "pre ({((I,Is),(S,(E,Es,SS)))} WHILE b DO C) Q = I" 
  
  
fun qdeps :: "acom ⇒ vname set ⇒ vname set" where
  "qdeps SKIP LV  = LV" |
  "qdeps (x ::= a) LV = LV ∪ vars a" | 
  "qdeps (C⇩1;; C⇩2) LV  = qdeps C⇩1 (qdeps C⇩2 LV)" |
  "qdeps ({(P',Ps)/_/_} CONSEQ C) _ = Ps" | (* the variables P' depends on *)
  "qdeps (IF b THEN C⇩1 ELSE C⇩2) LV = vars b ∪ qdeps C⇩1 LV ∪ qdeps C⇩2 LV" | 
  "qdeps ({((I,Is),(S,(E,x,Es)))} WHILE b DO C) _ = Is" (* the variables I depends on *) 
   
lemma qdeps_mono: "A ⊆ B ⟹ qdeps C A ⊆ qdeps C B"
  by (induct C arbitrary: A B, auto simp: le_supI1 le_supI2)
  
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 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 x where A: "A= (I,S,E,x)" using prod_cases4 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 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 

lemma support_pre: "support (pre C Q) ⊆ support Q ∪ varacom C"
proof (induct C arbitrary: Q)
  case (Awhile A b C Q)
  obtain I2 S E Es SS where A: "A= (I2,(S,(E,Es,SS)))" using prod_cases5 by blast 
  obtain I Is where "I2=(I,Is)" by fastforce
  note A=this A
  have support_inv: "⋀P. support (λl s. P s) = {}"
    unfolding support_def by blast  
  show ?case unfolding A  by(auto)
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)
  obtain a b c d e f where "x1=(a,b)" "x2=(c,d)" "x3=(e,f)" by force
  with Aconseq show ?case by auto  
qed (auto simp add: support_def) 

lemma finite_support_pre: "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 (C⇩1;; C⇩2) = (%s. time C⇩1 s + preT C⇩1 (time C⇩2) s)" |
  "time ({_/_/(e,es)} CONSEQ C) = e" |
  "time (IF b THEN C⇩1 ELSE C⇩2) =
  (λs. if bval b s then 1 + time C⇩1 s else 1 + time C⇩2 s)" |
  "time ({(_,(E',(E,x)))} WHILE b DO C) = E"
   
   
(* the set of variables, i need to know about, i.e. s1 and s2 have to agree on 
  s.th. time C s1 = time C s2 *)    
fun kdeps :: "acom ⇒ vname set" where
  "kdeps SKIP = {}" |
  "kdeps (x ::= a) = {}" |
  "kdeps (C⇩1;; C⇩2) = kdeps C⇩1 ∪ fune C⇩1 (kdeps C⇩2)" |
  "kdeps (IF b THEN C⇩1 ELSE C⇩2) =  vars b ∪ kdeps C⇩1 ∪ kdeps C⇩2" |
  "kdeps ({(_,(E',(E,Es,SS)))} WHILE b DO C) = Es" |
  "kdeps ({_/_/(e,es)} CONSEQ C) = es"  
     
     
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:›

     
definition funStar where "funStar f = (%x. {y. (x,y)∈{(x,y). y∈f x}⇧*})"
  
lemma funStart_prop1: "x ∈ (funStar f) x" unfolding funStar_def by auto
lemma funStart_prop2: "f x ⊆ (funStar f) x" unfolding funStar_def by auto

fun vc :: "acom ⇒ assn2 ⇒ vname set ⇒ vname set ⇒ bool" where
  "vc SKIP Q _ _ = True" |
  "vc (x ::= a) Q _ _ = True" |
  "vc (C⇩1 ;; C⇩2) Q LVQ LVE = ((vc C⇩1 (pre C⇩2 Q) (qdeps C⇩2 LVQ) (fune C⇩2 LVE ∪ kdeps C⇩2)) ∧ (vc C⇩2 Q LVQ LVE) )" |
  "vc (IF b THEN C⇩1 ELSE C⇩2) Q LVQ LVE = (vc C⇩1 Q LVQ LVE ∧ vc C⇩2 Q LVQ LVE)" |  
  "vc ({(P',Ps)/(Q,Qs)/(e',es)} CONSEQ C) Q' LVQ LVE = (vc C Q Qs LVE  ― ‹evtl ‹LV› weglassen - glaub eher nicht›
              ∧ (∀s1 s2 l. (∀x∈Ps. s1 x=s2 x) ⟶ P' l s1 = P' l s2)    ― ‹annotation ‹Ps› (the set of variables ‹P'› depends on) is correct›
              ∧ (∀s1 s2 l. (∀x∈Qs. s1 x=s2 x) ⟶ Q l s1 = Q l s2)    ― ‹annotation ‹Qs› (the set of variables ‹Q› depends on) is correct›
              ∧ (∀s1 s2. (∀x∈es. s1 x=s2 x) ⟶ e' s1 = e' s2)          ― ‹annotation ‹es› (the set of variables ‹e'› depends on) is correct›
              ∧ (∃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,Is),(S,(E,es,SS)))} WHILE b DO C) Q LVQ LVE = ((∀s1 s2 l. (∀x∈Is. s1 x = s2 x) ⟶ I l s1 = I l s2)  ― ‹annotation ‹Is› is correct›
        ∧ (∀y∈LVE ∪ LVQ. (let Ss=SS y in (∀s1 s2. (∀x∈Ss. s1 x = s2 x) ⟶ (S s1) y = (S s2) y)))                   ― ‹annotation ‹SS› is correct, for only one step›
        ∧ (∀s1 s2. (∀x∈es. s1 x=s2 x) ⟶ E s1 = E s2)                                ― ‹annotation ‹es› (the set of variables ‹E› depends on) is correct›
  ∧ (∀l s. (I l s ∧ bval b s ⟶ pre C I l s ∧   E s ≥ 1 + preT C E s + time C s
  ∧ (∀v∈(⋃y∈LVE ∪ LVQ. (funStar SS) y). (S s) v = (S (postQ C s)) v) ) ∧
  (I l s ∧ ¬ bval b s ⟶ Q l s ∧ E s ≥ 1 ∧ (∀v∈(⋃y∈LVE ∪ LVQ. (funStar SS) y). (S s) v  = s v)) ) ∧
  vc C I Is (es ∪ (⋃y∈LVE. (funStar SS) y)))"
     
subsubsection ‹Soundness:›

abbreviation "preSet U C l s == (Ball U (%u. case u of (x,e,v) ⇒ l x = preT C e s))"
abbreviation "postSet U l s == (Ball U (%u. case u of (x,e,v) ⇒ l x = e s))"


fun ListUpdate where
  "ListUpdate f [] l = f"
| "ListUpdate f ((x,e,v)#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 v where axe: "a = (x,e,v)"
    using prod_cases3 by blast 
  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,e,v)#xs)  = (ListUpdateE f xs  )(x:=e)"

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) = fst (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 v where a: "a=(y,e,v)"
      using prod_cases3 by blast 
    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: "x∈set xs" by auto
    then obtain y e v where a: "a=(y,e,v)"
      using prod_cases3 by blast 
    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 v where axe: "a = (p,q,v)"
      using prod_cases3 by blast 
  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,v))#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, v). (x, preT C2 e, fune C2 v)) upds) C1 l s"
proof (induct upds)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  obtain y e v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  from Cons show ?case unfolding a by (simp)
qed

lemma [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 v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  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 v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  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 v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  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 v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  from Cons show ?case unfolding a
    by(simp)
qed simp  


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

lemma "postList xs l s = (foldr (λ(x,e,v) acc l s. l x = e s ∧ acc l s) xs (%l s. True)) l s" 
apply(induct xs) apply(simp) by (auto)  
  
lemma support_postList: "support (postList xs) ⊆ lesvars xs"
proof (induct xs)    
  case (Cons a xs)
  obtain y e v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  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 postList_preList: "postList (map (λ(x, e, v). (x, preT C2 e, fune C2 v)) upds) l s = preList upds C2 l s"
proof (induct upds) 
  case (Cons a xs)
  obtain y e v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  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 v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  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 v where a: "a=(y,(e,v))"
    using prod_cases3 by blast 
  from Cons show ?case unfolding a
    by(simp)
qed simp

lemma postListpostSet2: " postList xs l s = postSet (set xs) l s "
  using postListpostSet postSetpostList by metis



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

definition K where "K C LVQ Q == (∀l s1 s2. s1 = s2 on qdeps C LVQ ⟶ pre C Q l s1 = pre C Q l s2)"
  

definition K2 where "K2 C e Es Q == (∀s1 s2. s1 = s2 on fune C Es ⟶ preT C e s1 = preT C e s2)"
  
definition K3 where "K3 upds C Q = (∀(a,b,c)∈set upds. K2 C b c Q)"
definition K4 where "K4 upds LV C Q = (K C LV Q ∧ K3 upds C Q ∧ (∀s1 s2. s1 = s2 on kdeps C ⟶ time C s1 = time C s2))"

lemma k4If: "K4 upds LVQ C1 Q ⟹ K4 upds LVQ C2 Q ⟹ K4 upds LVQ (IF b THEN C1 ELSE C2) Q"    
proof -
  have fl: "⋀A B s1 s2. A ⊆ B ⟹ s1 = s2 on B ⟹ s1 = s2 on A" by auto
  assume "K4 upds LVQ C1 Q" "K4 upds LVQ C2 Q"
  then show "K4 upds LVQ (IF b THEN C1 ELSE C2) Q"
    unfolding K4_def K_def K3_def K2_def using bval_eq_if_eq_on_vars fl apply auto
       apply blast+ done
qed
   

subsubsection "Soundness"
  
lemma vc_sound: "vc C Q LVQ LVE ⟹ finite (support Q)
  ⟹ fst ` (set upds) ∩ varacom C = {} ⟹ distinct (map fst upds)
  ⟹ finite (varacom C) 
  ⟹ (∀l s1 s2. s1 = s2 on LVQ ⟶ Q l s1 = Q l s2)
  ⟹ (∀l s1 s2. s1 = s2 on LVE ⟶ postList upds l s1 = postList upds l s2)
  ⟹ (∀(a,b,c)∈set upds. (∀s1 s2. s1 = s2 on c ⟶ b s1 = b s2))             ― ‹‹c› are really the variables ‹b› depends on›
  ⟹ (⋃(a,b,c)∈set upds. c) ⊆ LVE                                     ― ‹in ‹LV› are all the variables that the expressions in ‹upds› depend on›
  ⟹ ⊢⇩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)) ∧  K4 upds LVQ C Q)"
proof(induction C arbitrary: Q upds LVE LVQ)    
  case (Askip Q upds)
  then show ?case unfolding K4_def K_def K3_def K2_def
    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 unfolding K_def 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) apply(auto)  
        unfolding K4_def K2_def K3_def K_def by (auto)
next
  case (Aif b C1 C2 Q upds ) 
  from Aif(3) have 1: "vc C1 Q LVQ LVE" and 2: "vc C2 Q LVQ LVE" by auto
  have T: "⋀l s. pre C1 Q l s ⟹ bval b s ⟹ Q l (postQ C1 s)"
      and kT: "K4 upds LVQ C1 Q"
    using Aif(1)[OF 1 Aif(4) _ Aif(6)] Aif(5-11) by auto 
  have F: "⋀l s. pre C2 Q l s ⟹ ¬ bval b s ⟹ Q l (postQ C2 s)"
    and kF: "K4 upds LVQ C2 Q"
    using Aif(2)[OF 2 Aif(4) _ Aif(6)] Aif(5-11) by auto

  show ?case apply(safe)
    subgoal
      apply(simp)
     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])
          using Aif
           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])
          using Aif
           apply(auto)
          done
        by simp
    using T F kT kF  by (auto intro: k4If)  
next
  case (Aconseq P'2 Qannot2 eannot2 C Q upds) 
  obtain P' Ps where [simp]: "P'2 = (P',Ps)" by fastforce
  obtain Qannot Q's where [simp]: "Qannot2 = (Qannot,Q's)" by fastforce
  obtain eannot es where [simp]: "eannot2 = (eannot,es)" by fastforce
    
  have ih0: "finite (support Qannot)" using Aconseq(3,6) by simp
  
  from ‹vc ({P'2/Qannot2/eannot2} CONSEQ C) Q LVQ LVE›
  obtain k where k0: "k>0" and ih1: "vc C Qannot Q's LVE"
    and ih2: " (∀l s. P' l s ⟶  time C s ≤ k * eannot s ∧ (∀t. ∃l'. pre C Qannot l' s ∧ (Qannot l' t ⟶ Q l t)))"
    and pc: "(∀s1 s2 l. (∀x∈Ps. s1 x=s2 x) ⟶ P' l s1 = P' l s2)"
    and qc: "(∀s1 s2 l. (∀x∈Q's. s1 x=s2 x) ⟶ Qannot l s1 = Qannot l s2)"
    and ec: "(∀s1 s2. (∀x∈es. s1 x=s2 x) ⟶ eannot s1 = eannot s2)"  
    by auto
  have  k: "⊢⇩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}
    ∧ ((∀l s. pre C Qannot l s ⟶ Qannot l (postQ C s)) ∧ K4 upds Q's C Qannot)" 
    apply(rule Aconseq(1)) using Aconseq(2-10) by auto 
      
  note ih=k[THEN conjunct1] and ihsnd=k[THEN conjunct2]

  show ?case apply(simp, safe)
     apply(rule conseq[where e="time C" and P="λl s. pre C Qannot l s ∧ preList upds C l s" and Q="%l s. Qannot l s ∧ postList upds l s"])
      prefer 2
      apply(rule ih) 
    subgoal apply(rule exI[where x=k])
    proof (safe, goal_cases)
      case (1)
      with k0 show ?case by auto
    next      
      case (2 l s)
      then show ?case using ih2 by simp
    next
      case (3 l s t) 
      have finupds: "finite (set upds)" by simp
      {
        fix l s n x
        assume "x ∈ fst ` (set upds)"
        then have "x ∉ support (pre C Qannot)" using Aconseq(4) 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(4) by auto
        from assn2_lupd[OF this] have "Qannot (l(x := n))  = Qannot l" .
      } note K2=this  
                           
      from ih2 3(1) have *: "(∃l'. pre C Qannot l' s ∧ (Qannot l' t ⟶ Q l t))" by simp
      obtain l' where i': "pre C Qannot l' s" and ii': "(Qannot l' t ⟶ Q l t)" 
        and lxlx: "⋀x. x∈ fst ` (set upds) ⟹ l' x = l x" 
      proof (goal_cases)
        case 1
        from * obtain l'' where i': "pre C Qannot l'' s" and ii': "(Qannot l'' t ⟶ Q l t)" 
          by blast
        
        note allg=allg[where q="%e x. l x"]
        
        have "pre C Qannot (ListUpdate l'' upds (λe. l))  = pre C Qannot l''  "
          apply(rule allg[where ?upds="set upds"]) apply(rule U2) apply fast   by fast
        with i' have U: "pre C Qannot (ListUpdate l'' upds (λe. l)) s" by simp
        
        have "Qannot (ListUpdate l'' upds (λe. l)) = Qannot l''"
          apply(rule allg[where ?upds="set upds"]) apply(rule K2) apply fast  by fast
                
        then have K: "(%l' s. Qannot l' t ⟶ Q l t) (ListUpdate l'' upds (λe. l)) s = (%l' s. Qannot l' t ⟶ Q l t) l'' s"
          by simp
        with ii' have K: "(Qannot (ListUpdate l'' upds (λe. l)) t ⟶ Q l t)" by simp
        
        {
          fix x
          assume as: "x ∈ fst ` (set upds)" 
          have "ListUpdate l'' upds (λe. l) x = l x"
            apply(rule ListUpdate_updates)
            using as   by fast
        } note kla=this        
        
        show "thesis"
          apply(rule 1)
            apply(fact U)
           apply(fact K)
          apply(fact kla)
          done
      qed 
      
      let ?upds' = "set (map (%(x,e,v). (x,preT C e s,fune C v)) upds)"
      have "finite ?upds'" by simp 
      define xs where "xs = map (%(x,e,v). (x,preT C e s,fune C v)) upds"
      then have "set xs= ?upds'" by simp
                                
      have "pre C Qannot (ListUpdateE l' xs)  = pre C Qannot l' " 
        apply(rule allg_E[where ?upds="?upds'"]) apply(rule U2)  
         apply force   unfolding xs_def by simp
      with i' have U: "pre C Qannot (ListUpdateE l' xs ) s" by simp
      
      have "Qannot (ListUpdateE l' xs) = Qannot l' "
          apply(rule allg_E[where ?upds="?upds'"]) apply(rule K2) apply force unfolding xs_def by auto
        then have K: "(%l' s. Qannot l' t ⟶ Q l t) (ListUpdateE l' xs) s = (%l' s. Qannot l' t ⟶ Q l t) l' s"
          by simp
        with ii' have K: "(Qannot (ListUpdateE l' xs) t ⟶ Q l t)" by simp
                  
        
      have xs_upds: "map fst xs = map fst upds"
          unfolding xs_def by auto
      
      have grr: "⋀x. x ∈ ?upds' ⟹ ListUpdateE l' xs (fst x) = fst (snd x)" apply(rule ListUpdateE_updates)
         apply(simp only: xs_upds) using Aconseq(5) apply simp
          unfolding xs_def apply(simp) done
      show ?case
        apply(rule exI[where x="ListUpdateE l' xs"]) 
        apply(safe)
        subgoal by fact
        subgoal apply(rule preListpreSet)   proof (safe,goal_cases)
          case (1 x e v)
          then have "(x, preT C e s, fune C v) ∈ ?upds'"  
            by force
          from grr[OF this, simplified]
          show ?case .
         
          qed 
        subgoal using K apply(simp) done (* Qannot must be independent of x *)
        subgoal apply(rule postListpostSet) 
          proof (safe, goal_cases)
            case (1 x e v)
            with lxlx[of x] have fF: "l x = l' x"  
              by force 
            
            from postSetpostList[OF 1(2)] have g: "postSet (set upds) (ListUpdateE l' xs) t" .
            with 1(3) have A: "(ListUpdateE l' xs) x = e t"
              by fast            
            from 1(3) grr[of "(x,preT C e s, fune C v)"] have   B: "ListUpdateE l' xs x = fst (snd (x, preT C e s, fune C v))"
               by force
            from A B have X: "e t = preT C e s" by fastforce
            from preSetpreList[OF 3(2)] have "preSet (set upds) ({P'2/Qannot2/eannot2} CONSEQ C) l s" apply(simp) done
            with 1(3) have Y: "l x = preT C e s" apply(simp) by fast
            from X Y show ?case by simp
          qed  
        done
    qed
    subgoal using ihsnd ih2 by blast
    subgoal using ihsnd[THEN conjunct2] pc unfolding K4_def K_def apply(auto)
              unfolding K3_def K2_def using ec by auto
    done 
next
  case (Aseq C1 C2 Q upds)
   
  let ?P = "(λl s. pre C1 (pre 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 finite_varacomC2: "finite (varacom C2)" 
    apply(rule finite_subset[OF _ finite_varacom]) by simp 
  
  let ?y = "SOME x. x ∉ ?P'" 
  have sup_L: "support (preList upds (C1;;C2)) ⊆ lesvars upds"
    apply(rule support_preList) done 
  
  
  have sup_B: "support ?P ⊆ ?P'"                         
    apply(rule subset_trans[OF support_and]) using support_pre sup_L by blast 
  have fP': "finite (?P')" using finite_varacom Aseq(3,4,5)   apply simp done
  hence "∃x. x ∉ ?P'" using infinite_UNIV_listI
    using ex_new_if_finite by metis
  hence ynP': "?y ∉ ?P'" by (rule someI_ex) 
  hence ysupPreC2Q: "?y ∉ support (pre C2 Q)" and ysupC1: "?y ∉ varacom C1" using support_pre by auto
  
  from Aseq(5) have "lesvars upds ∩ varacom C2 = {}" by auto
  
  from Aseq show ?case apply(auto)
  proof (rule Seq, goal_cases)
    case 2   
    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 weaken_post[where Q="(%l s. Q l s ∧ postList upds l s)"])
       apply(rule 2(2)[THEN conjunct1])
          apply fact
         apply (fact)+ using 2(8) by simp      
  next
    case 3
    fix s
    show "time C1 s + preT C1 (time C2) s  ≤ time C1 s + preT C1 (time C2) s"
      by simp
  next
    case 1 
     
    
    from ynP' have yC1: "?y ∉ varacom C1" by blast
    have xC1: "lesvars upds ∩ varacom C1 = {}" using Aseq(5) by auto
    from finite_support_pre[OF Aseq(4) finite_varacomC2] 
    have G: "finite (support (pre C2 Q))" . 
         
    let ?upds = "map (λa. case a of (x,e,v) ⇒ (x, preT C2 e, fune C2 v)) upds"
    let ?upds' = "(?y,time C2, kdeps C2)#?upds"
    
    { 
      have A: " lesvars ?upds' = {?y} ∪ lesvars upds" apply simp 
        by force
      from Aseq(5) have 2: "lesvars upds ∩ varacom C1 = {}" by auto
      have " lesvars ?upds' ∩ varacom C1 = {}"
        unfolding A using ysupC1 2 by blast
    } note klar=this
    
    have t: "fst ∘ (λ(x, e, v). (x, preT C2 e, fune C2 v)) = fst" by auto
    
    {
      fix a b c X
      assume "a ∉ lesvars X" "(a,b,c) ∈ set X" 
      then have "False" by force
    } note helper=this
    
    have dmap: "distinct (map fst ?upds')"
      apply(auto simp add: t)
      subgoal for e apply(rule helper[of ?y upds e])  using ynP' by auto
      subgoal by fact
      done
    note bla1=1(1)[where Q="pre C2 Q" and upds="?upds'", OF 1(10) G klar dmap]  
      
    note bla=1(2)[OF 1(11,3), THEN conjunct2, THEN conjunct2] 
    from 1(4) have kal: "lesvars upds ∩ varacom C2 = {}" by auto
    from bla[OF kal Aseq.prems(4,6,7,8,9)] have bla4: "K4 upds LVQ C2 Q"   by auto
    then   have bla: "K C2 LVQ Q" unfolding K4_def  by auto
      
    have A:  
        "⊢⇩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} ∧
  (∀l s. pre C1 (pre C2 Q) l s ⟶ pre C2 Q l (postQ C1 s)) ∧  K4 ?upds' (qdeps C2 LVQ) C1 (pre C2 Q)"
      apply(rule 1(1)[where Q="pre C2 Q" and upds="?upds'", OF 1(10) G klar dmap]) 
    proof (goal_cases)
      case 1        
      then show ?case using bla  unfolding K_def by auto
    next
      case 2
      show ?case apply(rule,rule,rule,rule) proof (goal_cases)
        case (1 l s1 s2)
      then show ?case using bla4 using Aseq.prems(9) unfolding K4_def K3_def K2_def
        apply(simp)
        proof (goal_cases)
          case 1
          then have t: "time C2 s1 = time C2 s2" by auto
          
          have post: "postList (map (λ(x, e, v). (x, preT C2 e, fune C2 v)) upds) l s1 = postList (map (λ(x, e, v). (x, preT C2 e, fune C2 v)) upds) l s2" (is "?IH upds")
            using 1 
          proof (induct upds) 
            case (Cons a upds)
            then have IH: "?IH upds" by auto
            obtain x e v where a: "a = (x,e,v)" using prod_cases3 by blast
            from Cons(4) have "v ⊆ LVE" unfolding a by auto
            with Cons(2) have s12v: "s1 = s2 on fune C2 v" unfolding a using fune_mono by blast 
            with Cons(3) IH a show ?case by auto 
          qed auto
          
          from post t show ?case by auto
        qed 
      qed
    next
      case 3
      then show ?case  using bla4 unfolding K4_def K3_def K2_def by(auto)
    next
      case 4
      then show ?case apply(auto)
      proof (goal_cases)
        case (1 x a aa b)
        with Aseq.prems(9) have "b ⊆ LVE" by auto
        with fune_mono have "fune C2 b ⊆ fune C2 LVE" by auto
        with 1 show ?case by blast
      qed  
    qed
       
    show " ⊢⇩1 {λl s. (pre C1 (pre C2 Q) l s ∧ preList upds (C1;; C2) l s) ∧ l ?y = preT C1 (time C2) s} strip C1
         { time C1 ⇓ λl s. (pre C2 Q l s ∧ preList upds C2 l s) ∧ time C2 s ≤ l ?y}" 
      apply(rule conseq_old)
       prefer 2 
      apply(rule A[THEN conjunct1]) 
       apply(auto simp: preList_Seq postList_preList) done 
    
    from A[THEN conjunct2, THEN conjunct2] have A1: "K C1 (qdeps C2 LVQ) (pre C2 Q)" 
            and A2: "K3 ?upds' C1 (pre C2 Q)"  and A3: "(∀s1 s2. s1 = s2 on kdeps C1 ⟶ time C1 s1 = time C1 s2)" unfolding K4_def by auto
    from bla4 have B1: "K C2 LVQ Q" and B2: "K3 upds C2 Q" and B3: "(∀s1 s2. s1 = s2 on kdeps C2 ⟶ time C2 s1 = time C2 s2)" unfolding K4_def by auto
    show "K4 upds LVQ (C1;; C2) Q " 
      unfolding K4_def apply(safe)
      subgoal using A1 B1 unfolding K_def by(simp)  
      subgoal using A2 B2 unfolding K3_def K2_def apply(auto) done
      subgoal for s1 s2 using A3 B3 apply auto
      proof (goal_cases)
        case 1
        then have t: "time C1 s1 = time C1 s2" by auto
        from A2 have "∀s1 s2. s1 = s2 on fune C1 (kdeps C2) ⟶ preT C1 (time C2) s1 = preT C1 (time C2) s2" unfolding K3_def K2_def by auto
        then have p: "preT C1 (time C2) s1 =  preT C1 (time C2) s2"
            using 1(1) by simp
        from t p show ?case by auto
      qed
      done
  next    
    from ynP' sup_B show "?y ∉ support ?P" by blast 
    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
  next
    case (6 l s) 
    
    
    note bla=6(2)[OF 6(11,3), THEN conjunct2, THEN conjunct2] 
    from 6(4) have kal: "lesvars upds ∩ varacom C2 = {}" by auto
    from bla[OF kal Aseq.prems(4,6,7,8,9)] have bla4: "K4 upds LVQ C2 Q"   by auto
    then   have bla: "K C2 LVQ Q" unfolding K4_def  by auto
    
    have 11: "finite (support (pre C2 Q )) " 
      apply(rule finite_subset[OF support_pre])
      using 6(3,4,10)  finite_varacomC2 by blast 
    have A: "∀l s. pre C1 (pre C2 Q )  l s ⟶ pre C2 Q  l (postQ C1 s)"
      apply(rule 6(1)[where upds="[]", THEN conjunct2, THEN conjunct1])
            apply(fact)+  apply(auto) using bla unfolding K_def apply blast+ done 
    have B: "(∀l s. pre C2 Q  l s ⟶ Q l (postQ C2 s))" 
      apply(rule 6(2)[where upds="[]", THEN conjunct2, THEN conjunct1])
        apply(fact)+ apply auto using Aseq.prems(6) by auto    
    from A B 6 show ?case by simp 
  qed  
next
  case (Awhile A b C Q upds)
  obtain I2 S E Es SS where aha[simp]: "A = (I2,(S,(E,Es,SS)))" using prod_cases5 by blast
  obtain I Is where aha2: "I2 = (I, Is)"  
    by fastforce
  let ?LV ="(⋃y∈LVE ∪ LVQ. (funStar SS) y)" 
  have LVE_LVE: "LVE ⊆ (⋃y∈LVE. (funStar SS) y)" using funStart_prop1  by fast
  have LV_LV: "LVE ∪ LVQ ⊆ ?LV" using funStart_prop1  by fast
  have LV_LV2: "(⋃y∈LVE ∪ LVQ. SS y) ⊆ ?LV" using funStart_prop2 by fast
  have LVE_LV2: "(⋃y∈LVE. SS y) ⊆ (⋃y∈LVE. (funStar SS) y)" using funStart_prop2 by fast
  note aha = aha2 aha 
  with aha aha2 ‹vc (Awhile A b C) Q LVQ LVE› have "vc (Awhile ((I,Is),S,E,Es,SS) b C) Q LVQ LVE" apply auto apply fast+ done
  then                 
  have vc: "vc C I Is (Es ∪ (⋃y∈LVE. (funStar SS) y))" 
    and IQ: "∀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) on ?LV)" and
    pre: "∀l s. (I l s ∧ ¬ bval b s ⟶ Q l s ∧ 1 ≤ E s ∧ S s = s on ?LV)"
    and Is: "(∀s1 s2 l. s1 = s2 on Is ⟶ I l s1 = I l s2)"
    and Ss:  "(∀y∈LVE ∪ LVQ. let Ss = SS y in ∀s1 s2. s1 = s2 on Ss ⟶ S s1 y = S s2 y)"
    and Es: "(∀s1 s2. s1 = s2 on Es ⟶ E s1 = E s2)" apply simp_all apply auto apply fast+ done
    
  then have pre2: "⋀l s. I l s ⟹ ¬ bval b s ⟹ Q l s ∧ 1 ≤ E s ∧ S s = s on ?LV"
    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) on ?LV)"
    and Ss2:  "⋀y s1 s2. s1 = s2 on (⋃y∈LVE. SS y) ⟹ S s1 = S s2 on LVE"
    by auto
  
  from Ss have Ssc: "⋀c s1 s2. c ⊆ LVE ⟹  s1 = s2 on (⋃y∈c. SS y) ⟹ S s1 = S s2 on c" 
    by auto
    
  from IQ have IQ_in: "⋀l s. I l s ⟹ bval b s ⟹ S s = S (postQ C s) on ?LV" by auto
  
  have inv_impl: "⋀l s. I l s ⟹ bval b s ⟹ pre C I  l s" using IQ by auto    
  
  have yC: "lesvars upds ∩ varacom C = {}" using Awhile(4) aha by auto
   
  let ?upds = "map (%(x,e,v). (x, %s. e (S s), ⋃x∈v. SS x)) upds"
  let ?INV = "%l s. I l s ∧ postList ?upds l s" 
    
  have "lesvars upds ∩ support I = {}" using Awhile(4) unfolding aha by auto
    
  let ?P="lesvars upds ∪ varacom ({A} WHILE b DO C) "
  let ?z="SOME z::lvname. z ∉ ?P"
  have "finite ?P" apply(auto simp del: aha)   by (fact Awhile(6))  
  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   
      zny:  "?z ∉ lesvars upds"
    and zI:   "?z ∉ support I" 
    and blb:      "?z ∉ varacom C" by (simp_all add: aha)
  
  from Awhile(4,6) have 23: "finite (varacom C)" 
    and  26: "finite (support I)" by (auto simp add: finite_subset aha) 
   
  have "∀l s.  pre C I  l s ⟶ I l (postQ C s)"
    apply(rule Awhile(1)[THEN conjunct2, THEN conjunct1])
            apply(fact)+ subgoal using  Is apply auto done
    subgoal using Awhile(8) LVE_LVE  by (metis subsetD sup.cobounded2)
            apply fact using Awhile(10) LVE_LVE by blast 
  hence step: "⋀l s. pre C I  l s ⟹ I l (postQ C s)" by simp
   
  have fua: "lesvars ?upds = lesvars upds"
    by force
  let ?upds' = "(?z,E,Es) # ?upds"
  
  show ?case
  proof (safe, goal_cases)
    case (2 l s)
    from 2 have A: "I l s" unfolding aha by(simp) 
    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) on ?LV" 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  apply simp using Awhile(7)
          by (metis (no_types, lifting) LV_LV SUP_union contra_subsetD sup.boundedE)
      next
        case False
        with pre2 less(3) have "Q l s" "S s = s  on ?LV" by auto
        then show ?thesis apply simp using Awhile(7)
          by (metis (no_types, lifting) LV_LV SUP_union contra_subsetD sup.boundedE)  
      qed
    qed
    }
    with I show "Q l (postQ ({A} WHILE b DO C) s)" by simp   
  next
    case 1    
   have g: "⋀e. e ∘ S = (%s. e (S s)) " by auto
   
   
   have "lesvars ?upds' ∩ varacom C = {}"
          using yC blb by(auto)
        
        have z: "(fst ∘ (λ(x, e, v). (x, λs. e (S s), ⋃x∈v. SS x))) = fst" by(auto)
        have "distinct (map fst ?upds')"
          using Awhile(5) zny by (auto simp add: z)
          
        have klae: "⋀s1 s2 A B. B ⊆ A ⟹ s1 = s2 on A ⟹ s1 = s2 on B" by auto
        from Awhile(8) Awhile(9) have gl: "⋀a b c s1 s2. (a,b,c) ∈ set upds ⟹ s1 = s2 on c ⟹ b s1 = b s2" 
          by fast
        have CombALL: " ⊢⇩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}   ∧
(∀l s. pre C I l s ⟶ I l (postQ C s)) ∧ K4 ((SOME z. z ∉ lesvars upds ∪ varacom ({A} WHILE b DO C), E, Es) # map (λ(x, e, v). (x, λs. e (S s), ⋃x∈v. SS x)) upds) Is C I "
          apply(rule Awhile.IH[where upds="?upds'" ] )
                 apply (fact)+  
          
          subgoal apply safe using Is apply blast
            using Is apply blast done
          subgoal
            using Is Es apply auto   
             apply(simp_all add: postListpostSet2, safe) 
          proof (goal_cases)
            case (1 l s1 s2 x e v)
            from 1(5,6) have i: "l x = e (S s1)" by auto
            from  Awhile(10) 1(6) have vLC: "v ⊆ LVE" by auto
            have st: "(⋃y∈v. SS y) ⊆ (⋃y∈LVE. SS y)" using vLC by blast
            also have "… ⊆ (⋃y∈LVE. funStar SS y)" using LVE_LV2 by blast
            finally have st: "(⋃y∈v. SS y) ⊆  Es ∪ (⋃y∈LVE. funStar SS y)" by blast
            have ii: "e (S s1) = e (S s2)"
              apply(rule gl)
               apply fact
              apply(rule Ssc)
              apply fact
              using st 1(3) by blast
            from i ii show ?case by simp 
          next
            case (2 l s1 s2 x e v)
            from 2(5,6) have i: "l x = e (S s2)" by auto
            from  Awhile(10) 2(6) have vLC: "v ⊆ LVE" by auto
            have st: "(⋃y∈v. SS y) ⊆ (⋃y∈LVE. SS y)" using vLC by blast
            also have "… ⊆ (⋃y∈LVE. funStar SS y)" using LVE_LV2 by blast
            finally have st: "(⋃y∈v. SS y) ⊆  Es ∪ (⋃y∈LVE. funStar SS y)" by blast
            have ii: "e (S s1) = e (S s2)"
              apply(rule gl)
               apply fact
              apply(rule Ssc)
              apply fact
              using st 2(3) by blast
            from i ii show ?case by simp 
          qed  apply(auto)
          subgoal using Es by auto
          subgoal apply(rule gl) apply(simp) using Ss Awhile(10) by fastforce
          subgoal using Awhile(10) LVE_LV2 by  blast       
          done
        from this[THEN conjunct2, THEN conjunct2] have
          K: "K C Is I" and K3: "K3 ?upds' C I" and Kt: "∀s1 s2. s1 = s2 on kdeps C ⟶ time C s1 = time C s2" unfolding K4_def by auto
        show "K4 upds LVQ ({A} WHILE b DO C) Q" 
          unfolding K4_def apply safe
          subgoal using K unfolding K_def aha using Is by auto 
          subgoal using K3 unfolding K3_def K2_def aha apply auto
            subgoal for x e v apply (rule gl) apply simp apply(rule Ssc)  using Awhile(10) 
               apply fast  apply blast done done
          subgoal using Kt Es unfolding aha by auto
          done
   
    show ?case  
      
      apply(simp add: aha) 
      apply(rule conseq_old[where P="?INV" and e'=E and Q="λl s. ?INV l s ∧ ~ bval b s"])
      defer 
    proof (goal_cases)
      case 3
      show ?case  apply(rule exI[where x=1]) apply(auto)[1] apply(simp only: postList_preList[symmetric] ) apply (auto)[1]
        by(simp only:  g) 
    next
      case 2 (* post condition is satisfied after exiting the loop *)
      show ?case
      proof (safe, goal_cases)
        case (1 l s)
        then show ?case using pre by auto
      next
        case (2 l s)
        from Awhile(8) have Aw7: "⋀l s1 s2. s1 = s2 on LVE ⟹  postList upds l s1 = postList upds l s2" by auto
        have "postList (map (λ(x, e, v). (x, λs. e (S s), ⋃x∈v. SS x)) upds) l s =
                postList upds l (S s)" apply(induct upds) apply auto done
        also have "… = postList upds l s" using  Aw7[of "S s" s "l"] pre2 2 LV_LV
          by fast
        finally show ?case using 2(3) by simp
      qed 
    next
      case 1
      show ?case 
      proof(rule While, goal_cases)
        case 1          
        
        
        note Comb=CombALL[THEN conjunct1]
        
        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}" 
          apply(rule conseq_old)
          apply(rule exI[where x=1]) apply(simp)
            prefer 2 
        proof (rule Comb, safe, goal_cases) 
          case (2 l s)
          from IQ_in[OF 2(1)] gl Awhile(10,9)
          have y: "postList ?upds l s = 
                preList ?upds C l s" (is "?IH upds")
          proof (induct upds) 
            case (Cons a  upds')
            obtain y e v where axe: "a = (y,e,v)" using prod_cases3 by blast    
            have IH: "?IH upds'" apply(rule Cons(1))
              using Cons(2-5) by auto
            from Cons(3) axe have ke: "⋀s1 s2. s1 = s2 on v ⟹ e s1 = e s2"
              by fastforce
            have vLC: "v ⊆ LVE" using axe Cons(4) by simp
            have step: "e (S s) = e (S (postQ C s))" apply(rule ke) using Cons(2)  using vLC LV_LV 2(3) 
              by blast
            show ?case unfolding axe using IH step apply(simp) 
                apply(simp only: TQ) done
          qed simp
          from 2 show ?case by(simp add: y) 
        qed  (auto simp: inv_impl)
      next 
        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)
          thus ?case
            using 1 IQ by auto
        qed
      next 
        show "∀l s. ~bval b s ∧ I l s ∧ postList ?upds l s ⟶  1 ≤ E s"
        proof (clarify, goal_cases)
          case (1 l s)
          with pre show ?case by auto
        qed  
      next
        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
    qed 
    
  qed
qed
 

corollary vc_sound':
  assumes "vc C Q Qset {}" 
          "finite (support Q)" "finite (varacom C)"
          "∀l s. P l s ⟶ pre C Q l s" 
          "⋀s1 s2 l. s1 = s2 on Qset ⟹ Q l s1 = Q l s2"
  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), simplified, OF assms(2-3), THEN conjunct1])      
    using assms(4,5) apply auto 
    done 
qed

corollary vc_sound'':
  assumes "vc C Q Qset {}" 
          "finite (support Q)" "finite (varacom C)"
          " (∃k>0. ∀l s. P l s ⟶ pre C Q l s ∧ time C s ≤ k * e s)"
          "⋀s1 s2 l. s1 = s2 on Qset ⟹ Q l s1 = Q l s2"
  shows "⊢⇩1 {P} strip C {e ⇓ Q}"
proof -
  show ?thesis
    apply(rule conseq_old)
      prefer 2 apply(rule vc_sound[where upds="[]", OF assms(1), simplified, OF assms(2-3), THEN conjunct1])      
    using assms(4,5) apply auto 
    done 
qed    

end