Theory DiscussionO

subsection ‹Relation between the Hoare logics in big-O style›
theory DiscussionO
imports SepLogK_Hoare QuantK_Hoare Nielson_Hoare 
begin


(* here we compare quantitative Hoare logic with constant with Nielson's Hoare logic *)

subsubsection ‹Relation Nielson to quantHoare›
  
  
definition emN :: "qassn ⇒ Nielson_Hoare.assn2"  where "emN P = (λl s. P s < ∞)"  
 
(* quanthoare can be simulated by Nielson  *)  
lemma assumes s: "⊨⇩1 { emN P'} c {  %s. (THE e. enat e = P' s - Q' (THE t. (∃n. (c, s) ⇒ n ⇓ t ) )) ⇓ emN Q' }" (is "⊨⇩1 { ?P } c { ?e ⇓ ?Q }")
  shows quantNielson: "⊨⇩2⇩' { P' } c { Q' }"
proof -
  from s obtain k where k: "k>0" and qd: "⋀l s. emN P' l s ⟹ (∃t p. (c, s) ⇒ p ⇓ t ∧ p ≤ k * ?e s ∧ emN Q' l t)"
    unfolding hoare1_valid_def by blast 
    
  show ?thesis unfolding QuantK_Hoare.hoare2o_valid_def
    apply(rule exI[where x=k])
    apply safe apply fact
  proof -
    fix s
    assume P': "P' s < ∞"
    then have "(emN P') (λ_. 0) s" unfolding  emN_def by auto
    with qd obtain p t where i: "(c, s) ⇒ p ⇓ t" and p: "p ≤ k * ?e s" and e: "emN Q' (λ_. 0) t"
      by blast
    have t: "↓⇩s (c, s) = t" using bigstepT_the_state[OF i] by auto   
      
    from P' obtain pre where pre: "P' s = enat pre" by fastforce
    from e have "Q' t < ∞" unfolding emN_def by auto
    then obtain post where post: "Q' t = enat post" by fastforce
      
    have "p > 0" using i bigstep_progress by auto     
      
    thm enat.inject idiff_enat_enat the_equality
    have k: "(THE e. enat e = P' s - Q' (THE t. ∃n. (c, s) ⇒ n ⇓ t)) = pre - post" 
      unfolding t pre post apply(rule the_equality)   
       using idiff_enat_enat by auto 
    with p have ieq: "p ≤ k * (pre - post)" by auto
    then have "p + k * post ≤ k * pre" using ‹p>0›
      using diff_mult_distrib2 by auto
       then 
    have ii: "enat p + k * Q' t ≤ k * P' s" unfolding post pre by simp                           
    from i ii show "(∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + k * Q' t ≤ k * P' s)" by auto
  qed 
qed
 
  
  
(* Nielson can be simulated by quanthoare *)  
lemma assumes s: "⊨⇩2⇩' { %s . emb (∀l. P l s) + enat (e s) } c { %s. emb (∀l. Q l s) }" (is "⊨⇩2⇩' { ?P } c { ?Q }")
    and sP: "⋀l t. P l t ⟹ ∀l. P l t" (* "support P = {}" *)
    and sQ: "⋀l t. Q l t ⟹ ∀l. Q l t" (* "support Q = {}" *)
  shows  NielsonQuant: "⊨⇩1 { P } c { e ⇓ Q }" 
proof -
  from s obtain k where k: "k>0" and qd: "⋀s. ?P s < ∞ ⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * ?Q t ≤ enat k * ?P s)"
    unfolding QuantK_Hoare.hoare2o_valid_def by blast 
    
  show ?thesis unfolding hoare1_valid_def
    apply(rule exI[where x=k])
    apply safe apply fact
  proof -
    fix l s
    assume P': "P l s"
    then have aP: "∀l. P l s" using sP  by auto
    then have P: "?P s < ∞" by auto
    with qd obtain p t where i: "(c, s) ⇒ p ⇓ t" and p: "enat p + enat k * ?Q t ≤ enat k * ?P s"
      by blast
    have t: "↓⇩s (c, s) = t" using bigstepT_the_state[OF i] by auto   
       
    from P have Q: "Q l t" using p k
      apply auto
      by (metis (full_types) emb.simps(1) enat_ord_simps(2) imult_is_infinity infinity_ileE not_less_zero plus_enat_simps(3))      
    with sQ have "∀l. Q l t" by auto
    then have "?Q t = 0" by auto
    with p have "enat p ≤ enat k * ?P s" by auto
    with aP have p': "p ≤ k * e s" by auto
        
    from i Q p' show "∃t p. (c, s) ⇒ p ⇓ t ∧ p ≤ k * e s ∧ Q l t" by blast     
  qed
qed



 
subsubsection ‹Relation SepLogic to quantHoare› 

definition em :: "qassn ⇒ (pstate_t ⇒ bool)" where
  "em P = (%(ps,n). (∀ex. P (Partial_Evaluation.emb ps ex) ≤ enat n) )"  (* with equality next lemma also works *)

lemma assumes s: "⊨⇩3⇩' { em P} c { em Q }"
shows  "⊨⇩2⇩' { P } c { Q }"
proof -
  from s obtain k where k: "0<k" and s': "⋀ps n. em P (ps, n) ⟹ (∃ps' ps'' m e e'. (c, ps) ⇒⇩A m ⇓ ps'+ ps'' ∧ ps' ## ps'' ∧ k * n = k * e + e' + m ∧ em Q (ps', e))" unfolding hoare3o_valid_def  by auto
  {
    fix s
    assume P: "P s < ∞" 
    then obtain n where n: "P s = enat n"
      by fastforce
    with P have "em P (part s, n)" unfolding em_def by auto 
    with s' obtain ps' ps'' m e e' where c: "(c, part s) ⇒⇩A m ⇓ ps' + ps''" and orth: "ps' ## ps''"
              and m: "k * n = k * e + e' + m" and Q: "em Q (ps', e)" by blast
        
    from Q have q: "Q (Partial_Evaluation.emb ps' (Partial_Evaluation.emb ps'' (λ_. 0))) ≤ enat (e)" unfolding em_def by auto
        
    have z: "(Partial_Evaluation.emb ps' (Partial_Evaluation.emb ps'' (λ_. 0))) = (Partial_Evaluation.emb (ps'+ps'') (λ_. 0))"
      unfolding Partial_Evaluation.emb_def  apply (auto simp: plus_fun_def)
      apply (rule ext) subgoal for v apply (cases "ps' v") apply auto using orth    by (auto simp: sep_disj_fun_def domain_conv) done

    from q z have q:  "enat k * Q (Partial_Evaluation.emb (ps'+ps'') (λ_. 0)) ≤ enat k * enat e" using k
      by (metis i0_lb mult_left_mono) 

    have i: "(c, s) ⇒ m ⇓ (Partial_Evaluation.emb (ps'+ps'') (λ_. 0))" using  part_to_full'[OF c] by simp   
                
        
    have ii: "enat m + enat k * Q (Partial_Evaluation.emb (ps'+ps'') (λ_. 0)) ≤ enat k * P s" unfolding  n using q m
      using enat_ile by fastforce
      
    from i ii have "(∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * Q t ≤ enat k * P s)" by auto
  } note B=this
  show ?thesis unfolding QuantK_Hoare.hoare2o_valid_def
    apply(rule exI[where x=k], safe) apply fact
    apply (fact B) done
qed 

definition embe :: "(pstate_t ⇒ bool) ⇒ qassn" where
    "embe P = (%s. Inf {enat n|n. P (part s, n)} )"
 
lemma assumes s: "⊨⇩2⇩' { embe P } c { embe Q }" and full: "⋀ps n. P (ps,n) ⟹ dom ps = UNIV"            
  shows  "⊨⇩3⇩' {  P} c { Q }"
proof -
  from s obtain k where k: "k>0" and s: "⋀s. embe P s < ∞ ⟶ (∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * embe Q t ≤ enat k * embe P s)"
    unfolding QuantK_Hoare.hoare2o_valid_def by auto

  { fix ps n
    let ?s =" (Partial_Evaluation.emb ps (λ_. 0))"
    assume P: "P (ps, n)"
    with full have "dom ps = UNIV" by auto
    then have ps: "part ?s = ps" by simp
    from P have l': "({enat n |n. P (ps, n)} = {}) =  False " by auto
    have t: "embe P ?s < ∞" unfolding embe_def Inf_enat_def ps l'
      apply(rule ccontr) using l' apply auto
      by (metis (mono_tags, lifting) Least_le infinity_ileE)  
    with s obtain t p where c: "(c, ?s) ⇒ p ⇓ t" and ineq: "enat p + enat k * embe Q t ≤ enat k * embe P ?s" by blast
    from t obtain z where z: "embe P ?s = enat z"
      using less_infinityE by blast 
    with ineq obtain y where y: "embe Q t = enat y"
      using k by fastforce   
    then have l: "embe Q t < ∞" by auto
    then have zz: "({enat n|n. Q (part t, n)} = {}) = False" unfolding embe_def Inf_enat_def apply safe by simp  
    from y have "Q (part t, y)"  unfolding embe_def zz Inf_enat_def apply auto
       using zz apply auto   by (smt Collect_empty_eq LeastI enat.inject)
    
    from full_to_part[OF c] ps have c': "(c, ps) ⇒⇩A p ⇓ part t" by auto

    have "⋀P n. P (n::nat) ⟹ (LEAST n. P n) ≤ n" apply(rule Least_le) by auto

    from z P have zn: "z ≤ n" unfolding embe_def ps unfolding embe_def Inf_enat_def l'
      apply auto
      by (metis (mono_tags, lifting) Least_le enat_ord_simps(1))        

    from ineq z y have "enat p + enat k * y ≤ enat k * z" by auto
    then have "p + k * y ≤ k * z" by auto
    also have "… ≤ k * n"   using zn k by simp
    finally obtain e' where "k * n = k * y + e' + p" using k  by (metis add.assoc add.commute le_iff_add)    

    have "∃ps' ps'' m e e'. (c, ps) ⇒⇩A m ⇓ ps' + ps'' ∧ ps' ## ps'' ∧ k * n = k * e + e' + m ∧ Q (ps', e)"
      apply(rule exI[where x="part t"])
      apply(rule exI[where x="0"])
      apply(rule exI[where x="p"])
      apply(rule exI[where x="y"])
      apply(rule exI[where x="e'"]) apply auto by fact+ 
  }

  show ?thesis unfolding hoare3o_valid_def apply(rule exI[where x=k], safe)
    apply fact by fact
qed

subsection ‹A General Validity Predicate with Time›

  
definition valid  where
  "valid P c Q n = (∀s. P s ⟶ (∃s' m. (c, s) ⇒ m ⇓ s' ∧ m ≤ n ∧ Q s'))"  

definition validk  where
  "validk P c Q n = (∃k>0. (∀s. P s ⟶ (∃s' m. (c, s) ⇒ m ⇓ s' ∧ m ≤ k * n ∧ Q s')))"


lemma "validk P c Q n = (∃k>0. valid P c Q (k*n))"
  unfolding valid_def validk_def by simp

subsubsection ‹Relation between valid predicate and Quantitative Hoare Logic›
  
lemma "⊨⇩2⇩' {%s.  emb (P s)  + enat n} c { λs.  emb (Q s)  } ⟹ ∃k>0. valid P c Q (k*n)"
proof -
  assume valid: "⊨⇩2⇩' {λs. ↑ (P s) + enat n} c {λs. ↑ (Q s)}" 
  then obtain k where val: "⋀s. ↑ (P s) + enat n < ∞ ⟹ (∃t p. (c, s) ⇒ p ⇓ t ∧ enat p + enat k * ↑ (Q t) ≤ enat k * (↑ (P s) + enat n))"
    and k: "k>0" unfolding QuantK_Hoare.hoare2o_valid_def by blast
  { 
    fix s
    assume Ps: "P s"
    then have " ↑ (P s) + enat n < ∞" by auto
    with val obtain  t m where
        c: "(c, s) ⇒ m ⇓ t" and "enat m + k * ↑ (Q t) ≤ k * (↑ (P s) + enat n)" by blast
    
    then have "m ≤ k * n ∧ Q t" using k
      using Ps add.commute add.right_neutral emb.simps(1) emb.simps(2) enat_ord_simps(1) infinity_ileE plus_enat_simps(3)
      by (metis (full_types) mult_zero_right not_gr_zero times_enat_simps(1) times_enat_simps(4))
        
    with     c      
    have "(∃s' m. (c, s) ⇒ m ⇓ s' ∧ m ≤  k * n ∧ Q s')" by blast
  } note bla=this 
  show "∃k>0. valid P c Q (k*n)" unfolding valid_def apply(rule exI[where x=k]) using bla k by auto
qed  
 
lemma valid_quantHoare: "∃k>0. valid P c Q (k*n) ⟹ ⊨⇩2⇩' {%s. emb (P s)  + enat n} c { λs. emb (Q s)  }"
proof -
  assume  "∃k>0. valid P c Q (k*n)" 
  then obtain k where valid: "valid P c Q (k*n)" and k: "k>0" by blast
  { 
    fix s
    assume "(%s. emb (P s)  + enat n) s < ∞"
    then have Ps: "P s" apply auto
      by (metis emb.elims enat.distinct(2) enat.simps(5) enat_defs(4)) 
    with valid[unfolded valid_def] obtain t m where
        c: "(c, s) ⇒ m ⇓ t" and "m ≤ k * n" "Q t" by blast    
    then have "enat m +  k * ↑ (Q t) ≤  k * (↑ (P s) + enat n)" using Ps by simp
    with     c      
    have "(∃s' m. (c, s) ⇒ m ⇓ s' ∧ enat m + enat k * ↑ (Q s') ≤ enat k * (↑ (P s) + enat n))" by blast
  } note funk=this
  show "⊨⇩2⇩' {%s.  emb (P s)  + enat n} c { λs. emb (Q s)  }" unfolding QuantK_Hoare.hoare2o_valid_def
    apply(rule exI[where x=k]) using funk k by auto
qed  



subsubsection ‹Relation between valid predicate and Hoare Logic based on Separation Logic›
    
  
  

definition "embP2 P = (%(ps,n). ∀s.  P (Partial_Evaluation.emb ps s) ∧ n = 0)"
definition "embP3 P = (%(ps,n). dom ps = UNIV ∧ (∀s.  P (Partial_Evaluation.emb ps s)) ∧ n = 0)"
  
    
lemma emp: "a + Map.empty = a"
  by (simp add: plus_fun_conv) 
  
lemma oneway: "⊨⇩3⇩' {embP3 P ** $n} c {embP2 Q} ⟹ validk P c Q n"
proof -
  assume partial_true: "⊨⇩3⇩' {embP3 P ** $n} c {embP2 Q}" 
  from partial_true[unfolded hoare3o_valid_def] obtain k where k: "k>0" and
   q : "∀ps na. (embP3 P ∧* $ n) (ps, na) ⟶
                (∃ps' ps'' m e e'. (c, ps) ⇒⇩A m ⇓ ps' + ps'' ∧ ps' ## ps'' ∧ k * na = k * e + e' + m ∧ embP2 Q (ps', e)) " by blast
  { fix s
    assume "P s"
    then have g: " (embP3 P ∧* $ n) (part s, n)"
      unfolding embP3_def dollar_def sep_conj_def by auto
    from q  g
    obtain ps' ps'' m e e' where pbig: "(c, part s) ⇒⇩A m ⇓ ps' + ps''" and orth: "ps' ## ps''"
        and ii: "k * n = k * e + e' + m" and erg: "embP2 Q (ps', e)" by blast
    
    have ii': "m ≤ k * n" using ii by auto    
        
    from part_to_full'[OF pbig] have i: "(c, s ) ⇒ m ⇓ Partial_Evaluation.emb (ps' + ps'') s" by simp
    
    from erg have z2: "⋀s. Q (Partial_Evaluation.emb ps' s)" unfolding embP2_def by auto   
    have "Partial_Evaluation.emb (ps' + ps'') s = Partial_Evaluation.emb (ps'' + ps') s"
      using orth  by (simp add: sep_add_commute)
    also have "Partial_Evaluation.emb (ps'' + ps') s = Partial_Evaluation.emb (ps') (Partial_Evaluation.emb (ps'') s)"
      apply rule 
      unfolding emb_def plus_fun_conv map_add_def
      by (metis option.case_eq_if option.simps(5)) 
    finally have z: "Partial_Evaluation.emb (ps' + ps'') s = Partial_Evaluation.emb (ps') (Partial_Evaluation.emb (ps'') s)" .
    have iii: "Q (Partial_Evaluation.emb (ps' + ps'') s)" unfolding z apply (fact) . 
        
    from i ii' iii
      have "∃s' m. (c, s) ⇒ m ⇓ s' ∧ m ≤ k * n ∧ Q s'" by auto
    }
    with k show "validk P c Q n" unfolding validk_def by blast
qed
   
  
lemma theother: "validk P c Q n ⟹ ⊨⇩3⇩' {embP3 P ** $n} c {embP2 Q }"
proof -
  assume valid: "validk P c Q n" 
  then obtain k where k : "k>0" and v: "(∀s. P s ⟶ (∃s' m. (c, s) ⇒ m ⇓ s' ∧ m ≤ k * n ∧ Q s'))"
   unfolding validk_def by blast
  
  { fix ps na
    assume an: "(embP3 P ∧* $ n) (ps, na)" 
    have dom: "dom ps = UNIV" and Pps: "⋀s. P (Partial_Evaluation.emb ps s)" and nan: "na = n" using an unfolding sep_conj_def
        by (auto simp: embP3_def dollar_def)
        
    from v Pps
      obtain s' m where big: "(c, (Partial_Evaluation.emb ps (%_. 0))) ⇒ m ⇓ s'" and ii: "m ≤ k * n" and erg: "Q s'" by blast
                    
          
    have "part (Partial_Evaluation.emb ps (λ_. 0)) = ps " using dom by simp
    with full_to_part[OF big] have i: "(c, ps) ⇒⇩A m ⇓ part s'" by auto 
    
       
    have iii: "embP2 Q (part s', 0)" 
      unfolding embP2_def apply auto by fact 
         
    have "k * na = k * n - m + m" using ii k nan by simp  
        
    have "(∃ps' ps'' m e e'. (c, ps) ⇒⇩A m ⇓ ps' + ps'' ∧ ps' ## ps'' ∧ k * na = k * e + e' + m ∧ embP2 Q (ps', e))"
      apply(rule exI[where x="part s'"])
      apply(rule exI[where x="0"])
      apply(rule exI[where x="m"])
      apply(rule exI[where x="0"])
      apply(rule exI[where x="k * n - m"]) apply auto
      by fact+         
    }
    with k show "⊨⇩3⇩' {embP3 P ** $n} c {embP2 Q }" unfolding hoare3o_valid_def by blast
qed
  
  
lemma "validk P c Q n ⟷ ⊨⇩3⇩' {embP3 P ** $n} c {embP2 Q }"
using oneway and theother by metis



end