Theory Simple_TBOUND_Cond

(*by Ammer*)
theory Simple_TBOUND_Cond
imports Time_Reasoning
begin

text ‹This entry stops at showing the correctness and complexity of the operations,
  but does not provide a complete or universally usable methods to reason about
  programs using these operations. 
  
  In this theory, we provide an ad-hoc method, which is showcased 
  with a simple example later on.
›

text ‹definition of conditional TBOUND relation  and setup›

definition cond_TBOUND::"assn ⇒ 'a Heap  ⇒ nat⇒ bool"("§ _ §/ TBOUND/ _ _") where
  "cond_TBOUND P c t ≡ (∀h as. (h,as) ⊨ P ⟶ time c h ≤ t)" 

named_theorems cond_TBOUND  

lemma htt_elim:
  assumes "<P> c <Q>T[b]"
  shows "§P§ TBOUND c b"
  using assms
  unfolding htt_def cond_TBOUND_def by simp

lemma htt_intro:
  assumes "<P> c <Q>"
    and   "§P§ TBOUND c b"
  shows "<P> c <Q> T[b]"
  using assms unfolding htt_def cond_TBOUND_def by simp

lemma cond_TBOUND_mono: "§P§ TBOUND c b ⟹ b ≤ b' ⟹ §P§ TBOUND c b'"
  unfolding cond_TBOUND_def by auto

lemma time_leq_bindy: "time c h ≤ t1 ⟹ time (d (the_res c h)) (the_heap c h) ≤ t2 ⟹
              time (c ⤜ d) h ≤ t1+t2"
 by (simp add: time_bind)

lemma cond_TBOUND_bind[cond_TBOUND]: 
  assumes "§P§ TBOUND c t1" 
  and "<P> c <Q>"  
  and "(⋀ x h. x = the_res c h ⟹ §Q x§ TBOUND (d x) t2)"
shows  "§P§ TBOUND (c ⤜ d) (t1+t2)"
  unfolding cond_TBOUND_def hoare_triple_def 
  apply auto
  subgoal for h as
    apply(cases "fails (d (the_res c h)) (the_heap c h)")
   apply (simp add: time_bind)
    apply(rule time_leq_bindy)
    subgoal
    using assms  unfolding cond_TBOUND_def hoare_triple_def 
    apply auto
    done
  using assms(3)[of "(the_res c h)" h]
  unfolding cond_TBOUND_def
  using assms(2) 
  unfolding hoare_triple_def Let_def the_res_def the_heap_def
  apply(auto split: option.split)
   apply force+
  done
  done
    
lemma cond_TBOUND_return[cond_TBOUND]: "§ P § TBOUND (return x) 1"
  by (simp add: cond_TBOUND_def time_return)

lemma cond_TBOUND_cons:
  assumes "P ⟹⇩A Q"
      and "§ Q § TBOUND c b"
    shows "§ P § TBOUND c b"
  using assms
  unfolding cond_TBOUND_def
  apply sep_auto
  by (meson entailsD)

method cond_TBOUND= (rule cond_TBOUND_mono, rule cond_TBOUND)



end