Theory VEBT_Example_Setup
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