Theory SepLogK_Hoare

section "Hoare Logic based on Separation Logic and Time Credits (big-O style)" 
theory SepLogK_Hoare
  imports Big_StepT  Partial_Evaluation  Big_StepT_Partial
begin


   
subsection ‹Definition of Validity›
          
definition hoare3o_valid :: "assn2  com  assn2  bool"
  ("3'' {(1_)}/ (_)/ { (1_)}" 50) where
"3' { P } c { Q }  
    ( k>0. (ps n. P (ps,n)
  (ps' ps'' m e e'. ((c,ps) A m  ps' + ps'') 
      ps' ## ps''  k * n = k * e + e' + m
      Q (ps',e))))"
 
 


subsection "Hoare Rules"
     
inductive
  hoare3a :: "assn2  com  assn2  bool" ("3a ({(1_)}/ (_)/ { (1_)})" 50)
where

Skip:  "3a {$1} SKIP { $0}"  |

Assign4:  "3a { (λ(ps,t). xdom ps  vars a  dom ps  Q (ps(x(paval a ps)),t) ) ** $1} x::=a { Q }" |

If: " 3a { λ(s,n). P (s,n)  lmaps_to_axpr b True s } c1 { Q };
       3a {  λ(s,n). P (s,n)  lmaps_to_axpr b False s } c2 { Q } 
   3a { (λ(s,n). P (s,n)  vars b  dom s) ** $1} IF b THEN c1 ELSE c2 { Q}"   |

Frame:  "    3a { P } C { Q  } 
              3a { P ** F } C { Q ** F } "  |

Seq:  " 3a { P } C1 { Q } ;  3a { Q } C2 { R  } 
              3a { P } C1 ;; C2 { R } "  |

While:  " 3a { (λ(s,n). P (s,n)  lmaps_to_axpr b True s) } C { (λ(s,n). P (s,n)   vars b  dom s)  ** $1 }  
              3a { (λ(s,n). P (s,n)   vars b  dom s) ** $1 } WHILE b DO C {  λ(s,n). P (s,n)  lmaps_to_axpr b False s } "  |
   
conseqS: " 3a {P}c{Q} ; s n. P' (s,n)  P (s,n) ; s n. Q (s,n)  Q' (s,n)   
           3a {P'}c{ Q'}"   
  
inductive
  hoare3b :: "assn2  com  assn2  bool" ("3b ({(1_)}/ (_)/ { (1_)})" 50)
where

import:  "3a {P} c { Q}  3b {P} c { Q}"  |


conseq: " 3b {P}c{Q} ; s n. P' (s,n)  P (s,k*n) ; s n. Q (s,n)  Q' (s,n div k); k>0   
           3b {P'}c{ Q'}"   

  
  
inductive
  hoare3' :: "assn2  com  assn2  bool" ("3'' ({(1_)}/ (_)/ { (1_)})" 50)
where

Skip:  "3' {$1} SKIP { $0}"  |


Assign:  "3' {lmaps_to_expr_x x a v ** $1} x::=a { (%(s,c). dom s = vars a - {x}  c = 0) ** x  v }"  |

Assign':  "3' {pointsto x v' ** ( pointsto x v ⟶* Q)  ** $1} x::= N v { Q }"  |


Assign2:  "3' {v . ( ((v'. pointsto x v') ** ( pointsto x v ⟶* Q)  ** $1)
                 and sep_true ** (%(ps,n). vars a  dom ps  paval a ps = v  ) )} x::= a { Q }"  |



If: " 3' { λ(s,n). P (s,n)  lmaps_to_axpr b True s } c1 { Q };
       3' {  λ(s,n). P (s,n)  lmaps_to_axpr b False s } c2 { Q } 
   3' { (λ(s,n). P (s,n)  vars b  dom s) ** $1} IF b THEN c1 ELSE c2 { Q}"   |

Frame:  "    3' { P } C { Q  } 
              3' { P ** F } C { Q ** F } "  |

Seq:  " 3' { P } C1 { Q } ;  3' { Q } C2 { R  } 
              3' { P } C1 ;; C2 { R } "  |

While:  " 3' { (λ(s,n). P (s,n)  lmaps_to_axpr b True s) } C { (λ(s,n). P (s,n)   vars b  dom s)  ** $1 }  
              3' { (λ(s,n). P (s,n)   vars b  dom s) ** $1 } WHILE b DO C {  λ(s,n). P (s,n)  lmaps_to_axpr b False s } "  |
   
conseq: " 3' {P}c{Q} ; s n. P' (s,n)  P (s,k*n) ; s n. Q (s,n)  Q' (s,n div k); k>0   
           3' {P'}c{ Q'}"   |

normalize:  "    3' { P ** $m } C { Q  ** $n }; nm 
              3' { P ** $(m-n) } C { Q } "   | 

Assign''': "3' {  $1 ** (x  ds) } x ::= (N v) {  (x  v) }" |

Assign'''': "  symeval P a v; 3' {P} x ::= (N v) {Q'}    3' {P} x ::= a {Q'}" |

Assign4:  "3' { (λ(ps,t). xdom ps  vars a  dom ps  Q (ps(x(paval a ps)),t) ) ** $1} x::=a { Q }" |

False: "3' {  λ(ps,n). False } c {  Q }" |

pureI: "( P   3' { Q} c { R})   3' {P ** Q} c { R}"
   

(* which is more general Assign4 or Assign2 ? *)

definition A4 :: "vname  aexp  assn2  assn2" 
  where "A4 x a Q = ((λ(ps,t). xdom ps  vars a  dom ps  Q (ps(x(paval a ps)),t) ) ** $1)"
definition A2 :: "vname  aexp  assn2  assn2" 
  where "A2 x a Q = (v . ( ((v'. pointsto x v') ** ( pointsto x v ⟶* Q)  ** $1)
                 and sep_true ** (%(ps,n). vars a  dom ps  paval a ps = v  ) ))"

    
lemma "A4 x a Q (ps,n)  A2 x a Q (ps,n)"
unfolding A4_def A2_def sep_conj_def dollar_def sep_impl_def pointsto_def apply auto
  apply(rule exI[where x="paval a ps"])
  apply safe
  subgoal for n v
    apply(rule exI[where x="[x  v]::partstate"])
    apply(rule exI[where x=0])
    apply auto apply(rule exI[where x="ps(x:=None)"])
    apply auto
    unfolding sep_disj_fun_def domain_conv apply auto  
    unfolding plus_fun_conv apply auto 
      by (simp add: map_add_upd_left map_upd_triv) 
  subgoal for n v
    apply(rule exI[where x=0])
    apply(rule exI[where x=n])
    apply(rule exI[where x=ps])
    by auto 
  done
          
lemma "A2 x a Q (ps,n)  A4 x a Q (ps,n)"
  unfolding A4_def A2_def sep_conj_def dollar_def sep_impl_def pointsto_def
  apply (auto simp: sep_disj_commute) 
  subgoal for aa ba ab ac bc xa bd apply(rule exI[where x=bd])
    by (auto simp: sep_add_ac  domain_conv sep_disj_fun_def)
  subgoal  for aa ba ab ac bc xa bd apply(rule exI[where x=bd])
    apply (auto simp: sep_add_ac)      
    subgoal apply (auto simp:   domain_conv sep_disj_fun_def)
      by (metis fun_upd_same none_def plus_fun_def)
    subgoal 
      by (metis domD map_add_dom_app_simps(1) plus_fun_conv subsetCE)      
    subgoal 
    proof -
      assume a: "ab + [x  xa] = aa + ac"
      assume b: "ps = aa + ac" and o: "aa ## ac"
      then have b': "ps = ac + aa" by(simp add: sep_add_ac)
      assume vars: "vars a  dom ac"
      have pa: "paval a ps = paval a ac" unfolding b' 
        apply(rule paval_extend) using o vars by (simp_all add: sep_add_ac)
        
      have f: "f. (ab + [x  xa])(x  f) = ab + [x  f]"
        by (simp add: plus_fun_conv) 
          
      assume "Q (ab + [x  paval a ac], bd)"
      thus "Q ((aa + ac)(x  paval a (aa + ac)), bd)"
        unfolding b[symmetric] pa
        unfolding b a[symmetric] pa f by auto
    qed
    done
  done
    
lemma E_extendsR: "3a { P } c { F }  3' { P } c { F }"      
  apply (induct  rule: hoare3a.induct)
    apply(intro hoare3'.Skip)
    apply(intro hoare3'.Assign4)
    subgoal using hoare3'.If by auto
    subgoal using hoare3'.Frame by auto
    subgoal using hoare3'.Seq by auto
    subgoal using hoare3'.While by auto
    subgoal using hoare3'.conseq[where k=1] by simp
    done
  
lemma E_extendsS: "3b { P } c { F }  3' { P } c { F }"      
  apply (induct  rule: hoare3b.induct)
    apply(erule E_extendsR) 
    using hoare3'.conseq  by blast
 
      


lemma Skip':  "P = (F ** $1)  3' { P } SKIP { F }" 
  apply(rule conseq[where k=1])
    apply(rule Frame[where F=F])
     apply(rule Skip)
    by (auto simp: sep_conj_ac)
 
  
subsubsection "experiments with explicit and implicit GarbageCollection"
 
lemma "( (ps n. P (ps,n)
  (ps' ps'' m e e'. ((c,ps) A m  ps' + ps'') 
      ps' ## ps''   n =  e + e' + m
      Q (ps',e))))
     (ps n. P (ps,n)  (ps' m e . ((c,ps) A m  ps')     n = e  + m  (Q ** (λ_. True)) (ps',e)))"

proof (safe)
  fix ps n
  assume "ps n. P (ps, n)  (ps' ps'' m e e'. (c, ps) A m  ps' + ps''  ps' ## ps''  n = e + e' + m  Q (ps', e))"
    "P (ps, n)"
  then obtain ps' ps'' m e e' where C: "(c, ps) A m  ps' + ps''  ps' ## ps''  n = e + e' + m  Q (ps', e)" by blast
  show "ps' m e. (c, ps) A m  ps'  n = e + m  (Q ** (λ_. True)) (ps',e)"   unfolding   sep_conj_def
    apply(rule exI[where x="ps' + ps''"])
    apply(rule exI[where x="m"])
    apply(rule exI[where x="e+e'"]) using C   by auto
next
  fix ps n
  assume "ps n. P (ps,n)  (ps' m e . ((c,ps) A m  ps')     n = e  + m  (Q ** (λ_. True)) (ps',e))"
    "P (ps, n)"
  then obtain ps' m e where C: "((c,ps) A m  ps')     n = e  + m" and Q: "(Q ** (λ_. True)) (ps',e)" by blast
  from Q obtain ps1 ps2 e1 e2 where Q': "Q (ps1,e1)" "ps'=ps1+ps2" "ps1##ps2" "e=e1+e2" unfolding sep_conj_def by auto
  show "ps' ps'' m e e'. (c, ps) A m  ps' + ps''  ps' ## ps''  n = e + e' + m  Q (ps', e)"
    apply(rule exI[where x="ps1"])
    apply(rule exI[where x="ps2"])
    apply(rule exI[where x="m"])
    apply(rule exI[where x="e1"])
    apply(rule exI[where x="e2"]) using C Q' by auto
qed
       
subsection ‹Soundness›

theorem hoareT_sound2_part: assumes "3' { P }c{ Q  }"
  shows "3' { P } c { Q }" using assms        
proof(induction  rule: hoare3'.induct) 
   case (conseq P c Q P' k1 Q')
  then obtain k where p: "ps n. P (ps, n)  (ps' ps'' m e e'. ((c,ps) A m  ps' + ps'')   ps' ## ps''  k * n = k * e + e' + m  Q (ps',e))" and gt0: "k>0"
    unfolding hoare3o_valid_def by blast
      
      
  show ?case    unfolding hoare3o_valid_def
    apply(rule exI[where x="k*k1"])
    apply safe
    using gt0 conseq(4) apply simp
  proof -
    fix ps n
    assume "P' (ps,n)"
    with conseq(2) have "P (ps, k1*n)" by simp
    with p obtain ps' ps'' m e e' where pB: "(c, ps) A m  ps' + ps''" and orth: "ps' ## ps''"
          and m: "k * (k1 * n) = k*e + e' + m" and Q:  "Q (ps', e)"  by blast
                 
    from Q conseq(3) have Q': "Q' (ps', e div k1)" by auto
      
    have "k * k1 * n = k*e + e' + m" using m by auto
    also have " = k*(k1 * (e div k1) + e mod k1) + e' + m" using mod_mult_div_eq by simp
    also have " = k*k1*(e div k1) + (k*(e mod k1) + e') + m"
      by (metis add.assoc distrib_left mult.assoc) 
    finally have "k * k1 * n = k * k1 * (e div k1) + (k * (e mod k1) + e') + m" .
      
        
    show "ps' ps'' m e e'. (c, ps) A m  ps' + ps''  ps' ## ps''  k * k1 * n = k * k1 * e + e' + m  Q' (ps', e)"
      apply(rule exI[where x="ps'"])
      apply(rule exI[where x="ps''"])
      apply(rule exI[where x=m])
      apply(rule exI[where x="e div k1"])
      apply(rule exI[where x="k * (e mod k1) + e'"])
      apply safe apply fact apply fact apply fact apply fact done
  qed  
next     
  case (Frame P c Q F)
  from Frame(2)[unfolded hoare3o_valid_def]  obtain k
    where hyp: "ps n. P (ps, n)  (ps' ps'' m e e'. ((c,ps) A m  ps' + ps'')   ps' ## ps''  k * n = k * e + e' + m  Q (ps',e))"
        and k: "k>0"
    unfolding hoare3o_valid_def by blast
      
  show ?case unfolding hoare3o_valid_def apply(rule exI[where x=k]) using k apply simp
  proof(safe)
    fix ps n
    assume "(P ∧* F) (ps, n)"
    then obtain ps1 ps2 where orth: "ps1 ## ps2" and add: "(ps, n) = ps1 + ps2"
                  and P: "P ps1" and F: "F ps2" unfolding sep_conj_def by blast
    from hyp P have "(ps' ps'' m e e'. ((c,fst ps1) A m  ps' + ps'')   ps' ## ps''  k * snd ps1 = k * e + e' + m  Q (ps',e))"
      by simp
    then obtain ps' ps'' m e e' where a: "(c, fst ps1) A m  ps' + ps''" and orth2[simp]: "ps' ## ps''"
              and m: "k * snd ps1 = k * e + e' + m"  and Q: "Q (ps', e)" by blast                                                      
   
    from big_step_t3_post_dom_conv[OF a] have dom: "dom (ps' + ps'') = dom (fst ps1)" by auto         
        
        
    from add have g: "ps = fst ps1 + fst ps2" and h: "n = snd ps1 + snd ps2" by (auto simp add: plus_prod_def)  
      
    from orth have [simp]: "fst ps2 ## ps'" "fst ps2 ## ps''"
       apply (metis dom map_convs(1) orth2 sep_disj_addD1 sep_disj_commuteI sep_disj_fun_def sep_disj_prod_def) 
      by (metis dom map_convs(1) orth orth2 sep_add_commute sep_disj_addD1 sep_disj_commuteI sep_disj_fun_def sep_disj_prod_def)
        
    then have e: "ps' ## fst ps2" unfolding sep_disj_fun_def using dom   unfolding domain_conv  by blast
        
    have 3: "(Q ∧* F) (ps'+fst ps2, e+snd ps2)" unfolding sep_conj_def
        apply(rule exI[where x="(ps',e)"])
      apply(rule exI[where x="ps2"])
      apply safe
      subgoal  using orth  unfolding sep_disj_prod_def apply (auto simp: sep_disj_nat_def) 
        apply(rule e) done             
      subgoal unfolding plus_prod_def apply auto done
        apply fact apply fact done
        
    show "ps' ps'' m. (c, ps) A m  ps' + ps''  ps' ## ps''  (e. (e'. k * n = k * e + e' + m)  (Q ∧* F) (ps', e))" 
      apply(rule exI[where x="ps'+fst ps2"])
      apply(rule exI[where x="ps''"])
      apply(rule exI[where x=m])
    proof safe
      show "(c, ps) A m  ps' + fst ps2 + ps''"
        apply(rule Framer2[OF _ _ g]) apply (fact a)
         using orth apply (auto simp: sep_disj_prod_def)
         by (metis fst ps2 ## ps'' fst ps2 ## ps' orth2 sep_add_assoc sep_add_commute sep_disj_commuteI)   
     next
       show "ps' + fst ps2 ## ps''"
         by (metis dom map_convs(1) orth orth2 sep_add_disjI1 sep_disj_fun_def sep_disj_prod_def)
     next
       show "e. (e'. k * n = k * e + e' + m)  (Q ∧* F) (ps' + fst ps2, e)"
         apply(rule exI[where x="e+snd ps2"])
         apply safe
         subgoal proof(rule exI[where x=e'])
           have "k * n = k * snd ps1 + k * snd ps2" unfolding h by (simp add: distrib_left)  
           also have " =  k * e + e' + m + k* snd ps2" unfolding m by auto
           finally show "k * n = k * (e + snd ps2) + e' + m"
             by algebra
         qed  apply fact done
     qed 
   qed
next 
  case (False c Q)    
  then show ?case by (auto simp: hoare3o_valid_def) 
next
  case (Assign2 x Q a)
  show ?case 
    unfolding hoare3o_valid_def
    apply (rule exI[where x=1], safe) apply auto
    proof -
      fix ps n v
      assume A: "((λs. xa. (x  xa) s) ∧* (x  v ⟶* Q) ∧* $ (Suc 0)) (ps, n)"
      assume B: "((λs. True) ∧* (λ(ps, n). vars a  dom ps  paval a ps = v)) (ps, n)"
        
        
      from A obtain ps1 ps2 n1 n2 v' where  "ps1 ## ps2" and add1: "ps = ps1 + ps2" and n: "n = n1 + n2" and
         1: "(xaa. (x  xaa) (ps1,n1))"
         and 2:  "((x  v ⟶* Q) ∧* $ (Suc 0)) (ps2,n2)"  unfolding sep_conj_def
        by fastforce
          
      from 2 obtain ps2a ps2b n2a n2b where "ps2a ## ps2b" and add2: "ps2 = ps2a + ps2b" and n2: "n2 = n2a + n2b"
        and Q: "(x  v ⟶* Q) (ps2a,n2a)" and ps2b: "ps2b=0" and n2b: "n2b=1" unfolding dollar_def sep_conj_def
        by fastforce
          
        
      from 1 obtain v' where n1: "n1=0" and p: "ps1 = ([x  v']::partstate)" 
          and x: "x : dom ps1" by (auto simp: pointsto_def)
      from x add1 have x: "x : dom ps"
        by (simp add: plus_fun_conv subset_iff) 
           
      have f: "([x  v'] + ps2a)(x  v) = ps2a + [x  v]"
        by (smt thesis. (v'. n1 = 0; ps1 = [x  v']; x  dom ps1  thesis)  thesis ps1 ## ps2 add2 disjoint_iff_not_equal dom_fun_upd domain_conv fun_upd_upd map_add_upd_left option.distinct(1) plus_fun_conv ps2b sep_add_commute sep_add_zero sep_disj_fun_def) 
        
          
      let ?n' = "n2a + n1"
      from n n2 n2b have n': "n=1+?n'" by simp
      have Q': "Q (ps(x  v), ?n')" using Q n1 unfolding sep_impl_def apply auto
        unfolding pointsto_def apply auto
        subgoal 
          by (metis ps1 ## ps2 ps2 = ps2a + ps2b ps2b = 0 dom_fun_upd domain_conv option.distinct(1) p sep_add_zero sep_disj_commute sep_disj_fun_def)
        subgoal unfolding add1 p add2 ps2b
          by (auto simp: f)  
        done
            
      from B obtain ps1 ps2 n1 n2 where orth: "ps1 ## ps2" and add: "ps = ps2 + ps1" and n: "n=n1+n2"
          and vars: "vars a  dom ps2" and v: "paval a ps2 = v"
        unfolding sep_conj_def by (auto simp: sep_add_ac)
          
      from vars add have a: "vars a  dom ps"
        by (simp add: plus_fun_conv subset_iff)          
          
      from a x have "vars a  {x}  dom ps" by auto
          
      have "paval a ps = v" unfolding add apply(subst paval_extend)
        using orth vars v by(auto simp: sep_disj_commute)
          
        
      show "ps' ps'' m. (x ::= a, ps) A m  ps' + ps''  ps' ## ps''  (e. (e'. n = e + e' + m)  Q (ps', e))"
        apply(rule exI[where x="ps(xv)"])
        apply(rule exI[where x=0])
        apply(rule exI[where x="Suc 0"])
        apply auto
        apply(rule big_step_t_part.Assign)
           apply fact+ apply simp 
        apply(rule exI[where x="?n'"])
          apply safe 
          apply(rule exI[where x=0]) using n' apply simp
          using Q' by auto
          
    qed
next
  case Skip
  then show ?case by (auto simp: hoare3o_valid_def dollar_def)   
next
  case (Assign4 x a Q)
  then show ?case
    apply (auto simp: dollar_def sep_conj_def  hoare3o_valid_def ) 
      apply(rule exI[where x=1]) apply auto
      subgoal for ps b y
        apply(rule exI[where x="ps(x  paval a ps)"])
        apply(rule exI[where x="0"])
        apply(rule exI[where x="Suc 0"]) apply auto
          apply(rule exI[where x=b]) by auto
      done
next
  case (Assign' x v' v Q )
  have "aa. aa ## [x  v'] 
       ¬ aa ## [x  v]  False"   unfolding sep_disj_fun_def domain_def
    apply auto by (smt Collect_conj_eq Collect_empty_eq) 
  have f: "v'. domain [x  v'] = {x}" unfolding domain_conv by auto 
     
  { fix ps
    assume u: "ps ## [x  v']"
    have 2: "[x  v'] + ps = ps + [x  v']"
          "[x  v] + ps = ps + [x  v]"
         subgoal apply (subst sep_add_commute) using u by (auto simp: sep_add_ac) 
         subgoal apply (subst sep_add_commute) using u apply (auto simp: sep_add_ac)
             unfolding sep_disj_fun_def f by auto  done
    have "(x ::= N v, [x  v'] + ps) A Suc 0  [x  v] + ps"
      apply(rule Framer[OF big_step_t_part.Assign])
         apply simp_all using u  by (auto simp: sep_add_ac) 
    then have "(x ::= N v, ps + [x  v']) A Suc 0  ps + [x  v]" 
      by (simp only: 2)  
  } note f2 = this
      
  from Assign' show ?case 
    apply (auto simp: dollar_def sep_conj_def pointsto_def sep_impl_def hoare3o_valid_def ) 
    apply(rule exI[where x=1]) apply (auto simp: sep_add_ac) 
    subgoal unfolding sep_disj_fun_def f by auto 
    subgoal for ps n
      apply(rule exI[where x="ps+[x  v]"])
      apply(rule exI[where x="0"])
      apply(rule exI[where x="Suc 0"])
      apply safe 
      subgoal using f2 by auto
      subgoal  by auto 
      subgoal by force
      done
    done
next
  case (Assign x a v)   
  then show ?case unfolding hoare3o_valid_def
    apply(rule exI[where x=1]) 
    apply auto apply (auto simp: dollar_def )
      subgoal for ps n
         apply (subst (asm) separate_othogonal) apply auto
      apply(rule exI[where x="ps(x:=Some v)"])
      apply(rule exI[where x="0"])
      apply(rule exI[where x="1"])
      apply auto 
      apply (auto simp: pointsto_def)  unfolding  sep_conj_def
    subgoal  apply(rule exI[where x="((%y. if y=x then None else ps y) , 0)"])
      apply(rule exI[where x="((%y. if y = x then Some (paval a ps) else None),0)"])
        apply (auto simp: sep_disj_prod_def sep_disj_fun_def plus_fun_def)
      apply (smt domIff domain_conv)
      apply (metis domI insertE option.simps(3))
      using domIff by fastforce
    done  
  done
next
  case (If P b c1 Q c2)
  from If(3)[unfolded hoare3o_valid_def]
    obtain k1 where T: "ps n. P (ps, n)  vars b  dom ps  pbval b ps
      (ps' ps'' m e e'. (c1, ps) A m  ps' + ps''  ps' ## ps''  k1 * n = k1 * e + e' + m  Q (ps', e))"
        and k1: "k1 > 0" by force
  from If(4)[unfolded hoare3o_valid_def]
    obtain k2 where F: "ps n. P (ps, n)  vars b  dom ps  ¬ pbval b ps
      (ps' ps'' m e e'. (c2, ps) A m  ps' + ps''  ps' ## ps''  k2 * n = k2 * e + e' + m  Q (ps', e))"
        and k2: "k2 > 0" by force
        
    show ?case unfolding hoare3o_valid_def apply auto apply (auto simp: dollar_def)   
        apply(rule exI[where x="k1 * k2"]) using k1 k2 apply auto
  proof (goal_cases)
    case (1 ps n)   
    then obtain n' where P: "P (ps, n')" and dom: "vars b  dom ps" and Suc: "n = Suc n'" unfolding sep_conj_def
      by force
    show ?case 
    proof(cases "pbval b ps")
      case True
      with T[OF P dom] obtain ps' ps'' m e e' where d: "(c1, ps) A m  ps' + ps''"
            and orth: "ps' ## ps''" and m1:  "k1 * n' = k1 * e + e' + m" and Q:  "Q (ps', e)"
          by blast
        from big_step_t3_post_dom_conv[OF d] have klong: "dom (ps' + ps'') = dom ps" . 
      from k1 obtain k1' where k1': "k1 = Suc k1'"
        using gr0_implies_Suc by blast 
      from k2 obtain k2' where k2': "k2 = Suc k2'"
        using gr0_implies_Suc by blast 
      let ?e1 = "(k2' * (e' + m + k1) + e' + k1')"
      show ?thesis
        apply(rule exI[where x=ps']) 
        apply(rule exI[where x=ps'']) apply(rule exI[where x="m+1"])   
          apply safe
            apply(rule big_step_t_part.IfTrue)
              apply (rule dom)
              apply fact
               apply (rule True)
           apply (rule d)
          apply simp 
         apply fact
        subgoal apply(rule exI[where x="e"])
          apply safe
          subgoal proof (rule exI[where x="?e1"]) 
            have "k1 * k2 * n = k2 * (k1*n)" by auto
            also have " = k2 * (k1*n' + k1)" unfolding Suc  by auto
            also have " = k2 * (k1 * e + e' + m + k1)" unfolding m1 by auto
            also have " = k1 * k2 * e + k2* (e' + m + k1)"  by algebra
            also have " = k1 * k2 * e + k2' * (e' + m + k1) + (e' + m + k1)" unfolding k2'
              by simp 
            also have " = k1 * k2 * e + k2' * (e' + m + k1) + (e' + k1' + m + 1)" unfolding k1' by simp
            also have " = k1 *k2*e + (k2' * (e' + m + k1) + e' + k1') + (m+1)" by algebra  
            finally show "k1 * k2 * n = k1 * k2 * e + ?e1 + (m + 1)" .
          qed  using Q by force   
        done          
    next
      case False
      with F[OF P dom] obtain ps' ps'' m e e' where d: "(c2, ps) A m  ps' + ps''"
            and orth: "ps' ## ps''" and m2:  "k2 * n' = k2 * e + e' + m" and Q:  "Q (ps', e)"
          by blast
        from big_step_t3_post_dom_conv[OF d] have klong: "dom (ps' + ps'') = dom ps" . 
      from k1 obtain k1' where k1': "k1 = Suc k1'"
        using gr0_implies_Suc by blast 
      from k2 obtain k2' where k2': "k2 = Suc k2'"
        using gr0_implies_Suc by blast 
      let ?e2 = "(k1' * (e' + m + k2) + e' + k2')"
      show ?thesis
        apply(rule exI[where x=ps']) 
        apply(rule exI[where x=ps'']) apply(rule exI[where x="m+1"])   
          apply safe
            apply(rule big_step_t_part.IfFalse)
              apply (rule dom)
              apply fact
               apply (rule False)
           apply (rule d)
          apply simp 
         apply fact
        subgoal apply(rule exI[where x="e"])
          apply safe
          subgoal proof (rule exI[where x="?e2"]) 
            have "k1 * k2 * n = k1 * (k2*n)" by auto
            also have " = k1 * (k2*n' + k2)" unfolding Suc  by auto
            also have " = k1 * (k2 * e + e' + m + k2)" unfolding m2 by auto
            also have " = k1 * k2 * e + k1* (e' + m + k2)"  by algebra
            also have " = k1 * k2 * e + k1' * (e' + m + k2) + (e' + m + k2)" unfolding k1'
              by simp 
            also have " = k1 * k2 * e + k1' * (e' + m + k2) + (e' + k2' + m + 1)" unfolding k2' by simp
            also have " = k1 *k2*e + (k1' * (e' + m + k2) + e' + k2') + (m+1)" by algebra  
            finally show "k1 * k2 * n = k1 * k2 * e + ?e2 + (m + 1)" .
          qed  using Q by force   
        done
    qed 
  qed
next
  case (Seq P C1 Q C2 R) 
    
  from Seq(3)[unfolded hoare3o_valid_def] obtain k1 where
    1: "(ps n. P (ps, n)  (ps' ps'' m e e'. (C1, ps) A m  ps' + ps''  ps' ## ps''  k1 * n = k1 * e + e' + m  Q (ps', e)))"
      and k10: "k1 > 0" by blast
  from Seq(4)[unfolded hoare3o_valid_def]  obtain k2 where 
    2: " (ps n. Q (ps, n)  (ps' ps'' m e e'. (C2, ps) A m  ps' + ps''  ps' ## ps''  k2 * n = k2 * e + e' + m  R (ps', e)))"
      and k20: "k2 > 0" by blast
      
  from k10 obtain k1' where k1': "k1 = Suc k1'"
    using gr0_implies_Suc by blast 
  from k20 obtain k2' where k2': "k2 = Suc k2'"
    using gr0_implies_Suc by blast 
        
  show ?case unfolding hoare3o_valid_def
  apply(rule exI[where x="k2*k1"])
  proof safe        
    fix ps n      
    assume "P (ps, n)"
      
    with 1 obtain ps1' ps1'' m1 e1 e1' where C1: "(C1, ps) A m1  ps1' + ps1''" and orth: "ps1' ## ps1''"
          and m1: "k1 * n = k1 * e1 + e1' + m1"and Q: "Q (ps1', e1)" by blast
      
    from Q and 2 obtain ps2' ps2'' m2 e2 e2' where C2: "(C2, ps1') A m2  ps2' + ps2''" and orth2: "ps2' ## ps2''"
        and m2: "k2 * e1 = k2 * e2 + e2' + m2" and R: "R (ps2', e2)" by blast
    
    let ?ee = "(k1 *e2'  + k2*e1' +k2'*m1+ k1'*m2)"
      
    show "ps' ps'' m e e'. (C1;; C2, ps) A m  ps' + ps''  ps' ## ps''  k2 * k1 * n = k2 * k1 * e + e' + m  R (ps', e)"
      apply(rule exI[where x=ps2'])
        apply(rule exI[where x="ps2'' + ps1''"])
        apply(rule exI[where x="m1+m2"])
        apply(rule exI[where x="e2"])
      apply(rule exI[where x="?ee"])
    proof safe
      have C2': "(C2, ps1' + ps1'') A m2  ps2' + (ps2'' + ps1'')" 
        apply(rule Framer2[OF C2, of ps1'']) apply fact apply simp
          using sep_add_assoc
          by (metis C2 big_step_t3_post_dom_conv map_convs(1) orth orth2 sep_add_commute sep_disj_addD1 sep_disj_commuteI sep_disj_fun_def)
      show "(C1;; C2, ps) A m1 + m2  ps2' + (ps2'' + ps1'')"
        using C1 C2' by auto
    next
      show "ps2' ## ps2'' + ps1''"
        by (metis C2 big_step_t3_post_dom_conv map_convs(1) orth orth2 sep_disj_addI3 sep_disj_fun_def)
    next
      have "k2 * k1 * n = k2 * (k1 * n)" by auto
      also have " = k2 * (k1 * e1 + e1' + m1)" using m1 by auto
      also have " = k1 * k2 * e1 + k2 * (e1' + m1)" by algebra
      also have " = k1 * (k2 * e2 + e2' + m2) + k2 * (e1' + m1)" using m2 by auto
      also have " = k2 * k1 * e2 + (k1 *e2'  + k2*e1' +k2*m1+ k1*m2)" by algebra
      also have " = k2 * k1 * e2 + (k1 *e2'  + k2*e1' +k2'*m1+m1+ k1'*m2+m2)" unfolding k1' k2' by auto
      also have " = k2 * k1 * e2 + (k1 *e2'  + k2*e1' +k2'*m1+ k1'*m2)+(m1+m2)"  by auto
      finally show "k2 * k1 * n = k2 * k1 * e2 + ?ee + (m1 + m2)" .
    qed fact 
  qed (simp add: k10 k20)     
next
  case (While P b C) 
     
   {
     assume "k>0. ps n. (case (ps, n) of (s, n)  P (s, n)  lmaps_to_axpr b True s) 
                 (ps' ps'' m e e'. (C, ps) A m  ps' + ps''  ps' ## ps''  k * n = k * e + e' + m  ((λ(s, n). P (s, n)  vars b  dom s) ∧* $ 1) (ps', e))"
     then obtain k where  While2: "ps n. (case (ps, n) of (s, n)  P (s, n)  lmaps_to_axpr b True s)  (ps' ps'' m e e'. (C, ps) A m  ps' + ps''  ps' ## ps''  k * n = k * e + e' + m  ((λ(s, n). P (s, n)  vars b  dom s) ∧* $ 1) (ps', e))" and k: "k>0" by blast
         
  from k obtain k' where k': "k = Suc k'"
    using gr0_implies_Suc by blast
      
    have "k>0. ps n. ((λ(s, n). P (s, n)  vars b  dom s) ∧* $ 1) (ps, n) 
                 (ps' ps'' m e e'.
                     (WHILE b DO C, ps) A m  ps' + ps'' 
                     ps' ## ps''  k * n = k * e + e' + m  (case (ps', e) of (s, n)  P (s, n)  lmaps_to_axpr b False s))" (* 
    have "∃k>0. ∀ps n. ((λ(s, n). P (s, n) ∧ vars b ⊆ dom s) ∧* $ 1) (ps, n) ⟶ (∃ps' m. (WHILE b DO C, ps) ⇒A m ⇓ ps' ∧ m ≤ k * n ∧ (case (ps', n - m) of (s, n) ⇒ P (s, n) ∧ lmaps_to_axpr b False s))"
   *)   proof (rule exI[where x=k], safe, goal_cases)
    case (2 ps n)  
    from 2 show ?case  
      proof(induct n arbitrary: ps rule: less_induct)
        case (less x ps3) 
          
      show ?case 
      proof(cases "pbval b ps3")
        case True
        from less(2) obtain x' where P: "P (ps3, x')" and dom: "vars b  dom ps3"  and Suc: "x = Suc x'" unfolding sep_conj_def dollar_def by auto 
        from P dom True have 
           g: "((λ(s, n). P (s, n)  lmaps_to_axpr b True s)) (ps3, x')" 
            unfolding dollar_def by auto  
          from While2 g obtain ps3' ps3'' m e e' where C: "(C, ps3) A m  ps3' + ps3''" and orth: "ps3' ## ps3''"
                and x: "k * x' = k * e + e' + m" and P': "((λ(s, n). P (s, n)  vars b  dom s) ∧* $ 1) (ps3', e)" by blast
          then obtain x''' where P'': "P (ps3', x''')" and domb: "vars b  dom ps3'" and Suc'': "e = Suc x'''"
              unfolding sep_conj_def dollar_def by auto  
              
          from C big_step_t3_post_dom_conv have "dom ps3 = dom (ps3' + ps3'')" by simp
          with dom have dom': "vars b  dom (ps3' + ps3'')" by auto
              
          from C big_step_t3_gt0 have gt0: "m > 0" by auto
            
          have "e < x" using  x Suc gt0
            by (metis k le_add1 le_less_trans less_SucI less_add_same_cancel1 nat_mult_less_cancel1)   
 
          (*have "∃ps' m. (WHILE b DO C, ps3') ⇒A m ⇓ ps' ∧ m ≤ k * (x - (1 + m)) ∧ P (ps', (x - (1 + m)) - m) ∧ vars b ⊆ dom ps' ∧ ¬ pbval b ps'"
           *)
          have "ps' ps'' m e2 e2'. (WHILE b DO C, ps3') A m  ps' + ps''  ps' ## ps''  k * e = k * e2 + e2' + m  P (ps', e2)  lmaps_to_axpr b False ps'" 
                 apply(rule less(1))
             apply fact by fact 
              
          then obtain ps4' ps4'' mt et et' where w: "((WHILE b DO C, ps3') A mt  ps4' + ps4'')"
              and ortho: "ps4' ## ps4''" and m'': "k * e = k * et + et' + mt"
              and P'': "P (ps4', et)" and dom'': "vars b  dom ps4'" and b'': "¬ pbval b ps4'" by auto
                 
          have "ps4'' ## ps3''" and "ps4' ## ps3''" by (metis big_step_t3_post_dom_conv domain_conv orth ortho sep_add_disjD sep_disj_fun_def w)+  
              
          show ?thesis
            apply(rule exI[where x="ps4'"])
            apply(rule exI[where x="(ps4'' +  ps3'')"])
            apply(rule exI[where x="1 + m + mt"])
            apply(rule exI[where x="et"])
            apply(rule exI[where x=" et'  + k' + e'"])
          proof (safe)
            have "(WHILE b DO C, ps3' + ps3'') A mt  ps4' + (ps4'' +  ps3'')"
              apply(rule Framer2[OF w, of ps3'']) apply fact
               apply simp 
              apply(rule sep_add_assoc[symmetric])
                by fact+
            show "(WHILE b DO C, ps3) A 1 + m + mt  ps4' + (ps4'' +  ps3'')"
              apply(rule WhileTrue) apply fact apply fact apply (fact C) apply fact by auto
          next
            show "ps4' ## ps4'' + ps3''"
              by (metis big_step_t3_post_dom_conv domain_conv orth ortho sep_disj_addI3 sep_disj_fun_def w)   
          next 
            have "k * x = k * x' + k" unfolding Suc by auto
            also have " = k * e + e' + m + k" unfolding x by simp
            also have " = k * et + et' + mt + e' + m + k" using m'' by simp
            also have " = k * et + et' + mt + e' + m + 1 + k'" using k' by simp
            also have " = k * et + ( et'  + k' + e') + (1 + m + mt)" using k' by simp
            finally show "k * x = k * et + ( et'  + k' + e') + (1 + m + mt)" by simp
          next
            show "P (ps4', et)" by fact
          next
            show "lmaps_to_axpr b False ps4'" apply simp using dom'' b'' .. 
          qed                   
      next
        case False
        from less(2) obtain x' where P: "P (ps3, x')" and dom: "vars b  dom ps3" and Suc: "x = Suc x'" unfolding dollar_def sep_conj_def
          by force
        show ?thesis 
        apply(rule exI[where x=ps3])
        apply(rule exI[where x=0])
        apply(rule exI[where x="Suc 0"])
        apply(rule exI[where x="x'"])
          apply(rule exI[where x="k'"]) apply safe
            apply simp apply (rule big_step_t_part.WhileFalse)
        subgoal using dom by simp 
            apply fact apply simp
        using Suc k k' apply simp
        using P Suc apply simp
          using dom apply auto
          using False apply auto done    
      qed 
        
      qed
       
  qed (fact)
      
      
} with While(2)
  show ?case  unfolding hoare3o_valid_def by simp
next 
  case (Assign''' x ds v)
  then show ?case  
    unfolding hoare3o_valid_def apply auto 
    apply(rule exI[where x=1]) apply auto
    subgoal for ps n apply(rule exI[where x="ps(xv)"]) apply(rule exI[where x="0"])
      apply(rule exI[where x="Suc 0"]) 
      apply safe 
        apply(rule big_step_t_part.Assign)
        apply (auto) 
         subgoal apply(subst (asm) separate_othogonal_commuted') by(auto simp: dollar_def pointsto_def)
         subgoal apply(subst (asm) separate_othogonal_commuted') by(auto simp: dollar_def pointsto_def)
         done
       done          
next
  case (Assign'''' P a v x Q')
  from Assign''''(3)[unfolded hoare3o_valid_def] obtain k where k: "k>0" and 
   A: " ps n. P (ps, n)  (ps' ps'' m e e'. (x ::= N v, ps) A m  ps' + ps''  ps' ## ps''  k * n = k * e + e' + m  Q' (ps', e)) "
    by auto
  show ?case   
    unfolding hoare3o_valid_def apply auto 
    apply(rule exI[where x=k]) using k apply auto
    proof (goal_cases)
      case (1 ps n)
      with A obtain ps' ps'' m e e' 
        where " (x ::= N v, ps) A m  ps' + ps''" and orth: "ps' ## ps''" and m: "k * n = k * e + e' + m" and Q: "Q' (ps', e)" by metis
      from 1(2) Assign''''(1)[unfolded symeval_def] have "paval' a ps = Some v" by auto
      show ?case apply(rule exI[where x=ps']) apply(rule exI[where x=ps'']) apply(rule exI[where x=m])
          apply safe
          apply(rule avalDirekt3_correct) apply fact+
          apply(rule exI[where x=e]) apply safe
          apply(rule exI[where x=e']) apply fact 
          apply fact done  
    qed 
next
  case (pureI P Q c R)
  show ?case
  proof (cases "P")
    case True
    with pureI(2)[unfolded hoare3o_valid_def] obtain k where k: "k>0" and
     thing: " ps n. Q (ps, n)  (ps' ps'' m e e'. (c, ps) A m  ps' + ps''  ps' ## ps''  k * n = k * e + e' + m  R (ps', e))" by auto
        
    show ?thesis unfolding hoare3o_valid_def apply(rule exI[where x=k])
      apply safe apply fact
      using thing by fastforce
  next
    case False
    show ?thesis unfolding hoare3o_valid_def apply(rule exI[where x=1])
        using False by auto
    qed 
      next
case (normalize P m C Q n)
  then show ?case unfolding hoare3o_valid_def
  apply(safe) subgoal for k apply(rule exI[where x=k]) apply safe proof (goal_cases)
    case (1 ps N)
    have Q2: "P (ps, N - (m - n))" apply(rule stardiff) by fact
    have mn: "m - n  N" apply(rule stardiff(2)) by fact 
    have P: "(P ∧* $ m) (ps, N - (m - n) + m)"  unfolding sep_conj_def dollar_def
      apply(rule exI[where x="(ps,N - (m - n))"]) apply(rule exI[where x="(0,m)"])
      apply(auto simp: sep_disj_prod_def sep_disj_nat_def) by fact
    have N: " N - (m - n) + m =  N +n" using normalize(2)
      using mn by auto 
    from P N have P': "(P ∧* $ m) (ps, N +n)"    by auto
        
    from P' 1(4) obtain ps' ps'' m' e e' where "(C, ps) A m'  ps' + ps''" and orth: "ps' ## ps''"
        and m': "k * (N +n) = k * e + e' + m'" and Q: "(Q ∧* $ n) (ps', e)" by blast 
        
    have Q2: "Q (ps', e - n)" apply(rule stardiff) by fact
    
    have en: "en" using Q
      using stardiff(2) by blast     
        
    show ?case
      apply(rule exI[where x="ps'"])
      apply(rule exI[where x="ps''"]) apply(rule exI[where x="m'"])
      apply(rule exI[where x="e - n"])
      apply(rule exI[where x="e'"])
      proof (safe)
        show "(C, ps) A m'  ps' + ps''" by fact 
      next
        show "ps' ## ps''" by fact
      next
        have "k * N = k * ( (N + n)- n)" by auto
        also have " = k*(N + n) - k*n"  using right_diff_distrib' by blast 
        also have " = (k * e + e' + m') - k*n" using m' by auto
        also have " = k * e - k*n + e' + m'" using en
          by (metis Nat.add_diff_assoc2 ab_semigroup_add_class.add_ac(1) distrib_left le_add1 le_add_diff_inverse)
        also have " = k * (e-n) + e' + m'" by (simp add: diff_mult_distrib2)   
        finally show "k * N = k * (e - n) + e' + m'" .
      next
        show "Q (ps', e - n)" by fact
      qed     
    qed
  done
qed
  
    
    
    
thm hoareT_sound2_part E_extendsR
  
lemma hoareT_sound2_partR: "3a {P} c { Q}  3' {P} c {Q}"
  using hoareT_sound2_part E_extendsR by blast
    

subsubsection ‹nice example›
  
lemma Frame_R:  assumes "3' { P } C { Q  }" "Frame P' P F"
             shows "3' { P' } C { Q ** F } "  
  apply(rule conseq[where k=1]) apply(rule Frame) apply(rule assms(1))
      using assms(2) unfolding Frame_def by auto
  
lemma strengthen_post: assumes "3' {P}c{Q}" "s. Q s  Q' s"
  shows "3' {P}c{ Q'}"
  apply(rule conseq[where k=1])
    apply (rule assms(1))
    apply simp apply simp apply fact apply simp done
           
lemmas strongAssign = Assign''''[OF _ strengthen_post, OF _ Frame_R, OF _ Assign''']   
  
        
lemma weakenpre:  " 3' {P}c{Q} ; s. P' s  P s   
           3' {P'}c{ Q}"
  using conseq[where k=1] by auto
    
lemma weakenpreR:  " 3a {P}c{Q} ; s. P' s  P s   
           3a {P'}c{ Q}"
  using hoare3a.conseqS by auto
   
    
subsection "Completeness"
    
    
definition wp3' :: "com  assn2  assn2" ("wp3''") where 
"wp3' c Q  =  (λ(s,n). t m. nm  (c,s) A m  t  Q (t,n-m))" 
    
lemma wp3Skip[simp]: "wp3' SKIP Q = (Q ** $1)"
  apply (auto intro!: ext simp: wp3'_def) 
    unfolding sep_conj_def dollar_def sep_disj_prod_def sep_disj_nat_def apply auto apply force
    subgoal for t n apply(rule exI[where x=t])  apply(rule exI[where x="Suc 0"])
      using big_step_t_part.Skip by auto
    done
 
lemma wp3Assign[simp]: "wp3' (x ::= e) Q = ((λ(ps,t). vars e  {x}  dom ps  Q (ps(x  paval e ps),t)) ** $1)"
  apply (auto intro!: ext simp: wp3'_def )  
  unfolding sep_conj_def apply (auto simp: sep_disj_prod_def sep_disj_nat_def dollar_def) apply force
    by fastforce  

lemma wpt_Seq[simp]: "wp3' (c1;;c2) Q = wp3' c1 (wp3' c2 Q)"
  apply (auto simp: wp3'_def fun_eq_iff ) 
  subgoal for a b t m1 s2 m2  
      apply(rule exI[where x="s2"])
      apply(rule exI[where x="m1"])
        apply simp
      apply(rule exI[where x="t"])
      apply(rule exI[where x="m2"])
      apply simp done
  subgoal for s m t' m1 t m2
      apply(rule exI[where x="t"])
      apply(rule exI[where x="m1+m2"])
    apply (auto simp: big_step_t_part.Seq) done
      done

lemma wp3If[simp]:
 "wp3' (IF b THEN c1 ELSE c2) Q = ((λ(ps,t). vars b  dom ps  wp3' (if pbval b ps then c1 else c2) Q (ps,t)) ** $1)"
  apply (auto simp: wp3'_def fun_eq_iff)
  unfolding sep_conj_def apply (auto simp: sep_disj_prod_def sep_disj_nat_def dollar_def)    
  subgoal for a ba t x apply(rule exI[where x="ba - 1"]) apply auto  
    apply(rule exI[where x=t]) apply(rule exI[where x=x]) apply auto done
  subgoal for a ba t x apply(rule exI[where x="ba - 1"]) apply auto 
    apply(rule exI[where x=t]) apply(rule exI[where x=x]) apply auto done
  subgoal for a ba t m
    apply(rule exI[where x=t]) apply(rule exI[where x="Suc m"]) apply auto
    apply(cases "pbval b a")
    subgoal apply simp apply(subst big_step_t_part.IfTrue) using big_step_t3_post_dom_conv by auto 
    subgoal apply simp apply(subst big_step_t_part.IfFalse) using big_step_t3_post_dom_conv by auto  
  done
  done 
             
    
lemma sFTrue: assumes "pbval b ps" "vars b  dom ps"
  shows "wp3' (WHILE b DO c) Q (ps, n) = ((λ(ps, n). vars b  dom ps  (if pbval b ps then wp3' c (wp3' (WHILE b DO c) Q) (ps, n) else Q (ps, n))) ∧* $ 1) (ps, n)"
    (is "?wp = (?I ∧* $ 1) _")
proof 
  assume "wp3' (WHILE b DO c) Q (ps, n)"
  from this[unfolded wp3'_def] obtain ps'' tt where tn: "tt  n" and w1: "(WHILE b DO c, ps) A tt  ps''" and Q: "Q (ps'', n - tt) " by blast      
  with assms obtain t t' ps' where w2: "(WHILE b DO c, ps') A t'  ps''" and c: "(c, ps) A t  ps'" and tt: "tt=1+t+t'" by auto
  
  from tn obtain k where n: "n=tt+k"
    using le_Suc_ex by blast  
      
  from assms show "(?I ∧* $ 1) (ps,n)"
    unfolding sep_conj_def dollar_def  wp3'_def  apply auto
    apply(rule exI[where x="t+t'+k"])
      apply safe subgoal using n tt by auto
      apply(rule exI[where x="ps'"])
    apply(rule exI[where x="t"])
    using c apply auto
      apply(rule exI[where x="ps''"])
    apply(rule exI[where x="t'"])
    using w2 Q n by auto
next
  assume "(?I ∧* $ 1) (ps,n)"
  with assms have Q: "wp3' c (wp3' (WHILE b DO c) Q) (ps, n-1)" and n: "n1" unfolding dollar_def sep_conj_def by auto
  then obtain t ps' t' ps'' where t: "t  n - 1"  
        and c: "(c, ps) A t  ps'" and  t': "t'  (n-1) - t" and w: "(WHILE b DO c, ps') A t'  ps''" 
        and Q: "Q (ps'', ((n-1) - t) - t')"
    unfolding wp3'_def by auto
  show "?wp" unfolding wp3'_def
    apply simp apply(rule exI[where x="ps''"]) apply(rule exI[where x="1+t+t'"])
    apply safe
    subgoal using t t' n by simp
    subgoal using c w assms by auto
    subgoal using Q t t' n by simp
    done      
qed

lemma sFFalse: assumes "~ pbval b ps" "vars b  dom ps"
  shows "wp3' (WHILE b DO c) Q (ps, n) = ((λ(ps, n). vars b  dom ps  (if pbval b ps then wp3' c (wp3' (WHILE b DO c) Q) (ps, n) else Q (ps, n))) ∧* $ 1) (ps, n)"
    (is "?wp = (?I ∧* $ 1) _")
proof 
  assume "wp3' (WHILE b DO c) Q (ps, n)"
  from this[unfolded wp3'_def] obtain ps' t where tn: "t  n" and w1: "(WHILE b DO c, ps) A t  ps'" and Q: "Q (ps', n - t) " by blast      
  from assms have w2: "(WHILE b DO c, ps) A 1  ps" by auto
  from w1 w2 big_step_t_determ2 have t1: "t=1" and pps: "ps=ps'" by auto
  from assms show "(?I ∧* $ 1) (ps,n)"
    unfolding sep_conj_def dollar_def using t1 tn Q pps apply auto  apply(rule exI[where x="n-1"]) by auto
next
  assume "(?I ∧* $ 1) (ps,n)"
  with assms have Q: "Q(ps,n-1)" "n1" unfolding dollar_def sep_conj_def by auto
  from assms have w2: "(WHILE b DO c, ps) A 1  ps" by auto   
  show "?wp" unfolding wp3'_def
    apply auto   apply(rule exI[where x=ps]) apply(rule exI[where x=1])
      using Q w2 by auto  
qed

lemma sF': "wp3' (WHILE b DO c) Q (ps,n) = ((λ(ps, n). vars b  dom ps  (if pbval b ps then wp3' c (wp3' (WHILE b DO c) Q) (ps, n) else Q (ps, n))) ∧* $ 1) (ps,n)"   
  apply(cases "vars b  dom ps")
  subgoal apply(cases "pbval b ps") using sFTrue sFFalse by auto
  subgoal   by (auto simp add: dollar_def wp3'_def sep_conj_def) 
      done
    
lemma sF: "wp3' (WHILE b DO c) Q s = ((λ(ps, n). vars b  dom ps  (if pbval b ps then wp3' c (wp3' (WHILE b DO c) Q) (ps, n) else Q (ps, n))) ∧* $ 1) s"   
 using sF'
  by (metis (mono_tags, lifting) prod.case_eq_if prod.collapse sep_conj_impl1) 
    
    
    
lemma strengthen_postR: assumes "3a {P}c{Q}" "s. Q s  Q' s"
  shows "3a {P}c{ Q'}"
  apply(rule hoare3a.conseqS)
    apply (rule assms(1))
    apply simp by (fact assms(2))  
    
lemma assumes "Q. 3a {wp3' c Q} c {Q}"
  shows WhileWpisPre: "3a {wp3' (WHILE b DO c) Q} WHILE b DO c { Q}"
proof - 
  define I where  "I  (λ(ps, n). vars b  dom ps  (if pbval b ps then wp3' c (wp3' (WHILE b DO c) Q) (ps, n) else Q (ps, n)))"
  define I' where  "I'  (λ(ps, n). (if pbval b ps then wp3' c (wp3' (WHILE b DO c) Q) (ps, n) else Q (ps, n)))"
  have I': "I = (λ(ps, n). vars b  dom ps  I' (ps, n))" unfolding I_def I'_def by auto
   
  from assms[where Q="(wp3' (WHILE b DO c) Q)"] have 
    c: "3a {wp3' c (wp3' (WHILE b DO c) Q)} c {(wp3' (WHILE b DO c) Q)}" .
  have c': "3a { (λ(s,n). I (s,n)  lmaps_to_axpr b True s) } c { I  ** $1 }"
    apply(rule hoare3a.conseqS)             
      apply(rule c)              
    subgoal apply auto unfolding I_def by auto            
    subgoal  unfolding I_def   using sF by auto 
    done
      
  have c'': "3a { (λ(s,n). I (s,n)  lmaps_to_axpr b True s) } c { (λ(s, n). I (s, n)  vars b  dom s)  ** $1 }"
    apply(rule strengthen_postR[OF c'])
      unfolding I'
      by (smt R case_prod_beta prod.sel(1) prod.sel(2))  
   
    have ka: "(λ(s, n). I (s, n)  vars b  dom s) = I"
      apply rule unfolding I' by auto
        
  from hoare3a.While[where P="I"] c'' have
    w: "3a { (λ(s,n). I (s,n)   vars b  dom s) ** $1 } WHILE b DO c {  λ(s,n). I (s,n)  lmaps_to_axpr b False s }" .
        
  show "3a {wp3' (WHILE b DO c) Q} WHILE b DO c { Q}"       
      apply(rule hoare3a.conseqS)      
      apply(rule w)           
    subgoal unfolding ka using sF I_def by simp  
    subgoal unfolding I_def by auto 
    done
qed
     

lemma wpT_is_pre: "3a {wp3' c Q} c { Q}"
proof (induction c arbitrary: Q)
  case SKIP
  then show ?case apply auto 
    using hoare3a.Frame[where F=Q and Q="$0" and P="$1", OF hoare3a.Skip]
      by (auto simp: sep.add_ac) 
next
  case (Assign x1 x2) 
  then show ?case using hoare3a.Assign4 by simp 
next               
  case (Seq c1 c2)
  then show ?case apply auto
    apply(subst hoare3a.Seq[rotated]) by auto
next
  case (If x1 c1 c2)
  then show ?case apply auto 
    apply(rule weakenpreR[OF hoare3a.If, where P1="%(ps,n). wp3' (if pbval x1 ps then c1 else c2) Q (ps,n)"])
      apply auto
    subgoal apply(rule hoare3a.conseqS[where P="wp3' c1 Q" and Q=Q]) by auto 
    subgoal apply(rule hoare3a.conseqS[where P="wp3' c2 Q" and Q=Q]) by auto 
  proof -
    fix a b
    assume "((λ(ps, t). vars x1  dom ps  wp3' (if pbval x1 ps then c1 else c2) Q (ps, t)) ∧* $ (Suc 0)) (a, b)"
    then show "((λ(ps, t). wp3' (if pbval x1 ps then c1 else c2) Q (ps, t)  vars x1  dom ps) ∧* $ (Suc 0)) (a, b)"
       unfolding sep_conj_def apply auto apply(case_tac "pbval x1 aa") apply auto done (* strange! *)
  qed 
next
  case (While b c)
  with WhileWpisPre show ?case .
qed  
   
lemma hoare3o_valid_alt: "3' { P } c { Q }  
    ( k>0. (ps n. P (ps,n div k)
  (ps' ps'' m e e'. ((c,ps) A m  ps' + ps'') 
      ps' ## ps''  n = e + e' + m
      Q (ps',e div k))))"  
proof -
  assume "3' {P} c { Q}"
  from this[unfolded hoare3o_valid_def] obtain k where k0: "k>0" and 
     P: "ps n. P (ps, n)  (ps' ps'' m e e'. (c, ps) A m  ps' + ps''  ps' ## ps''  k * n = k * e + e' + m  Q (ps', e)) "
    by blast
  show ?thesis apply(rule exI[where x=k])
      apply safe apply fact
  proof -
    fix ps n
    assume "P (ps, n div k)"
    with P obtain ps' ps'' m e e' where 1: "(c, ps) A m  ps' + ps''" "ps' ## ps''" and e: "k * (n div k) = k * e + e' + m" and Q: "Q (ps', e)"
      by blast
    have "k * (n div k)  n" using k0
      by simp  
    then obtain e'' where "n = k * (n div k) + e''" using le_Suc_ex by blast
    also have " = k * e + e' + e'' + m" using e   by auto 
    finally have "n = k * e + (e'+e'') + m"  and "Q (ps', (k*e) div k)" using Q k0 by auto
    with 1     
     show " ps' ps'' m e e'. (c, ps) A m  ps' + ps''  ps' ## ps''  n = e + e' + m  Q (ps', e div k)" by blast
  qed
qed         
              
  
lemma valid_alternative_with_GC: assumes "(ps n. P (ps,n)
  (ps' ps'' m e e'. ((c,ps) A m  ps' + ps'') 
      ps' ## ps''  n = e + e' + m
      Q (ps',e))) " shows "(ps n. P (ps,n)    
  (ps'  m e . ((c,ps) A m  ps'  ) 
       n = e + m  (Q ** sep_true) (ps',e)))" 
proof safe
  fix ps n
  assume P: "P (ps,n)"
  with assms obtain ps' ps'' m e e' where c: "(c,ps) A m  ps' + ps''" and
     ps: "ps' ## ps''" and n: "n = e + e' + m" and Q: "Q (ps',e)" by blast
  show "ps' m e. (c, ps) A m  ps'  n = e + m  (Q ∧* (λs. True)) (ps', e)"
    apply(rule exI[where x="ps' + ps''"])
    apply(rule exI[where x=m])
    apply(rule exI[where x="e+e'"])
    apply safe apply fact apply fact
      unfolding sep_conj_def apply simp apply(rule exI[where x=ps']) apply(rule exI[where x=e])
      apply(rule exI[where x=ps'']) apply safe apply fact apply(rule exI[where x=e']) apply simp
      apply fact done
  qed
     
    
lemma hoare3o_valid_GC: "3' {P} c { Q }  3' {P} c { Q ** sep_true}"
proof -
  assume "3' {P} c { Q }" 
  then obtain k where "k>0" and P: "ps n. P (ps, n)  (ps' ps'' m e e'. (c, ps) A m  ps' + ps''  ps' ## ps''  k * n = k * e + e' + m  Q (ps', e))"
    unfolding hoare3o_valid_def by blast
  show "3' {P} c { Q ** sep_true}" unfolding hoare3o_valid_def
    apply(rule exI[where x=k])
    apply safe apply fact
  proof -
    fix ps n
    assume "P (ps, n)"
    with P obtain ps' ps'' m e e' where "(c, ps) A m  ps' + ps''"" ps' ## ps'' "" k * n = k * e + e' + m " and Q: " Q (ps', e)"
      by blast

    show "ps' ps'' m e e'. (c, ps) A m  ps' + ps''  ps' ## ps''  k * n = k * e + e' + m  (Q ∧* (λs. True)) (ps', e)"    
      apply(rule exI[where x=ps'])
      apply(rule exI[where x=ps''])
      apply(rule exI[where x=m])
      apply(rule exI[where x=e])
      apply(rule exI[where x=e'])
      apply safe apply fact+ unfolding sep_conj_def apply(rule exI[where x="(ps', e)"])  apply(rule exI[where x="0"]) using Q by simp
  qed
qed
  
lemma hoare3a_sound_GC: "3a {P} c { Q}  3' {P} c { Q ** sep_true}" using hoare3o_valid_GC hoareT_sound2_partR by auto  
  
lemma valid_wp: "3' {P} c { Q}  (k>0. s n. P (s, n)  wp3' c (λ(ps, n). (Q ** sep_true) (ps, n div k)) (s, k * n))"
proof -
  let ?P = "λk (ps,n). P (ps,n div k)"
  let ?Q = "λk (ps,n). Q (ps,n div k)"
  let ?QG = "λk (ps,n). (Q ** sep_true) (ps,n div k)"
  assume "3' {P} c { Q}" 
  then obtain k where k[simp]: "k>0" and "(ps n. P (ps,n div k)
  (ps' ps'' m e e'. ((c,ps) A m  ps' + ps'') 
      ps' ## ps''  n = e + e' + m
      Q (ps',e div k)))" using hoare3o_valid_alt by blast  
  then have "(ps n. ?P k (ps,n)
  (ps' ps'' m e e'. ((c,ps) A m  ps' + ps'') 
      ps' ## ps''  n = e + e' + m
      ?Q k (ps',e)))" by auto
  then have f: "(ps n. ?P k (ps,n)  (ps'  m e . ((c,ps) A m  ps'  ) 
       n = e + m  (?Q k ** sep_true) (ps',e)))"
    apply(rule valid_alternative_with_GC) done
  
      
  have "s n. P (s, n)  wp3' c (λ(ps, n). (Q ** sep_true) (ps, n div k)) (s, k * n)" 
    unfolding wp3'_def apply auto
  proof -
    fix ps n
    assume "P (ps,n)"
    then have "P (ps,(k*n) div k)" apply simp done
    with f obtain ps' m e where "((c,ps) A m  ps'  )" and z: "k * n = e + m"
        and Q: "(?Q k ** sep_true) (ps',e)" by blast
    from z have e: "e = k * n -m " by auto
    from Q[unfolded e sep_conj_def] obtain ps1 ps2 e1 e2 where
      "ps1 ## ps2" "(ps' = ps1 +ps2)" and eq: "k * n - m = e1 +  e2" and Q: "Q (ps1, e1 div k)" by force

    let ?f = "(e1 + e2) div k - (e1 div k + (e2 div k))"
    have kl: "(e1 + e2) div k  (e1 div k + (e2 div k))" using k
      using div_add1_eq le_iff_add by blast                        
    show "t m. m  k * n  (c, ps) A m  t  (Q ∧* (λs. True)) (t, (k * n - m) div k)"   
      apply(rule exI[where x=ps'])  
      apply(rule exI[where x=m]) apply safe using z apply simp
       apply fact unfolding e unfolding sep_conj_def 
        apply(rule exI[where x="(ps1,e1 div k)"])
      apply(rule exI[where x="(ps2,e2 div k+?f)"]) apply auto apply fact+
      unfolding eq using kl 
      apply force using Q by auto
  qed 
  then show "(k>0. s n. P (s, n)  wp3' c (λ(ps, n). (Q ** sep_true) (ps, n div k)) (s, k * n))"
    using k by metis
qed
    
    
theorem completeness: "3' {P} c { Q}  3b {P} c { Q ** sep_true}"
proof -
  let ?P = "λk (ps,n). P (ps,n div k)"
  let ?Q = "λk (ps,n). Q (ps,n div k)"
  let ?QG = "λk (ps,n). (Q ** sep_true) (ps,n div k)"
  assume "3' {P} c { Q}" 
  then obtain k where k[simp]: "k>0" and P: "s n. P (s, n)  wp3' c (λ(ps, n). (Q ** sep_true) (ps, n div k)) (s, k * n)" 
    using valid_wp by blast 
      
  from wpT_is_pre  have R: "3a {wp3' c (?QG k)} c {?QG k}" by auto
  
  show "3b {P} c { Q ** sep_true}" 
    apply(rule hoare3b.conseq[OF hoare3b.import[OF R], where k=k])
    subgoal for s n  by (fact P) 
        apply simp by (fact k)
qed
  
  
thm E_extendsR completeness
  
lemma completenessR: "3' {P} c { Q}  3' {P} c { Q ** sep_true}"  
  using E_extendsS completeness by metis


end