Theory VEBT_Example_Setup

(*by Lammich and Ammer*)
section ‹Setup for Usage Example›
theory VEBT_Example_Setup
imports "Time_Reasoning/Simple_TBOUND_Cond"
begin
  text ‹We provide a few monadic combinators and associated reasoning rules, 
    that are required for our usage example.
    
    Warning: ad-hoc and highly incomplete!
  ›

  fun mfold where
    "mfold f [] s = return s"
  | "mfold f (x#xs) s = do { s ← f x s; mfold f xs s }"  

  fun mmap where
    "mmap f [] = return []"
  | "mmap f (x#xs) = do { y←f x; ys ← mmap f xs; return (y#ys) }"
  
  definition mIf :: "bool Heap ⇒ 'a Heap ⇒ 'a Heap ⇒ 'a Heap"
    (‹(if⇩m (_)/ then (_)/ else (_))› [0, 0, 10] 10)
    where "mIf b t e ≡ do { bb ← b; if bb then t else e }"
  
  lemma mIf_rule[sep_decon_rules]: 
    "<P> do { bb ← b; if bb then t else e } <Q> ⟹ <P> mIf b t e <Q>"  
    unfolding mIf_def by simp

  abbreviation (input) pure_app (infix ‹$⇩m› 10) where "f $⇩m m ≡ do { x←m; return (f x) }" 
  
    
  lemma mmap_pure_aux:
    assumes "⋀x. x∈set xs ⟹ <P> fi x <λr. P * ↑(r = f x)>"
    shows "<P> mmap fi xs <λys. P * ↑(ys = map f xs )>"
    using assms
  proof (induction xs)
    case Nil
    then show ?case by sep_auto
  next
    case (Cons a xs)
    
    note [sep_heap_rules] = Cons
    
    show ?case 
      by sep_auto
    
  qed

lemma mmap_pres:
    assumes "⋀x. x∈set xs ⟹ <P> fi x <λr. P>"
    shows "<P> mmap fi xs <λys. P >"
  using assms
  apply(induction xs)
   apply sep_auto+
  done

  
 lemma cond_TBOUND_mIf[cond_TBOUND]:
   assumes "§ P § TBOUND cond b1"
    and    "⋀ h. § Q (the_res cond h)§ TBOUND t b2"
    and    "⋀ h.§ Q (the_res cond h) § TBOUND e b3"
    and    "<P> cond <Q>"
  shows    "§ P § TBOUND (if⇩m cond then t else e) (b1 + max b2 b3)"
   unfolding mIf_def
   apply(rule cond_TBOUND_bind)
   apply (rule assms)+
   subgoal for x h
    apply(auto split: if_split)
    apply(rule cond_TBOUND_mono[where b = b2])
     using assms apply (metis (full_types))
      apply simp
    apply(rule cond_TBOUND_mono[where b = b3])
     using assms apply (metis (full_types))
     apply simp
    done
   done

end