SSL Discussion.thy

section "Discussion"
subsection ‹Relation between the explicit Hoare logics›
theory Discussion
imports Quant_Hoare SepLog_Hoare
begin
 
subsubsection ‹Relation SepLogic to quantHoare›
     
definition em where "em P' = (%(ps,n). P' (emb ps (%_. 0)) ≤ enat n )"  (* with equality next lemma also works *)
  
lemma assumes s: "⊨₃ { em P'} c { em Q' }"
shows  "⊨₂ { P' } c { Q' }"
proof -
  from s have s': "∧ps n. em P' (ps, n) ==> (∃ps' m. (c, ps) ==>_A m ⇓ ps' ∧ m ≤ n ∧ em Q' (ps', n - m))" unfolding hoare3_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' m where c: "(c, part s) ==>_A m ⇓ ps'" and m: "m ≤ n" and Q': "em Q' (ps', n - m)" by blast
        
    from Q' have q: "Q' (emb ps' (λ_. 0)) ≤ enat ( n - m)" unfolding em_def by auto
        
        
    thm full_to_part  part_to_full
    have i: "(c, s) ==> m ⇓ emb ps' (λ_. 0)" using  part_to_full'[OF c] apply simp done 
                
        
    have ii: "enat m + Q' (emb ps' (λ_. 0)) ≤ P' s" unfolding  n using q m
      using enat_ile by fastforce 
      
    from i ii have "(∃t p. (c, s) ==> p ⇓ t ∧ enat p + Q' t ≤ P' s)" by auto
  } then
  show ?thesis unfolding hoare2_valid_def by blast
qed 
  

end