Theory Time_Refinement
section ‹Currency Refinement›
theory Time_Refinement
imports NREST NREST_Type_Classes
begin
paragraph ‹Summary›
text ‹This theory introduces currency refinement.›
subsection "time refine"
definition timerefine ::"('b ⇒ ('c,'d::{complete_lattice,comm_monoid_add,times,mult_zero}) acost)
⇒ ('a, ('b,'d) acost) nrest ⇒ ('a, ('c,'d) acost) nrest" ("⇓⇩C")
where "⇓⇩C R m = (case m of FAILi ⇒ FAILi |
REST M ⇒ REST (λr. case M r of None ⇒ None |
Some cm ⇒ Some (acostC (λcc. Sum_any (λac. the_acost cm ac * the_acost (R ac) cc)))))"
lemma timerefine_alt3:
assumes "TR =( λcm. (acostC (λcc. Sum_any (λac. the_acost cm ac * the_acost (R ac) cc))))"
shows
"⇓⇩C R m = (case m of FAILi ⇒ FAILi |
REST M ⇒ REST (λr. case M r of None ⇒ None |
Some cm ⇒ Some (TR cm) ))"
unfolding assms unfolding timerefine_def by simp
definition "timerefine' TR m = (case m of FAILi ⇒ FAILi |
REST M ⇒ REST (λr. case M r of None ⇒ None |
Some cm ⇒ Some (TR cm) ))"
lemma timerefine_alt4:
fixes R
defines "TR ≡ ( λcm. (acostC (λcc. Sum_any (λac. the_acost cm ac * the_acost (R ac) cc))))"
shows "⇓⇩C R m = timerefine' TR m"
unfolding timerefine_def timerefine'_def
unfolding assms by simp
definition timerefineF ::"('b ⇒ ('c,'d::{complete_lattice,comm_monoid_add,times,mult_zero}) acost)
⇒ ('a ⇒ ('b,'d) acost option) ⇒ ('a ⇒ ('c,'d) acost option)"
where "timerefineF R M = (λr. case M r of None ⇒ None |
Some cm ⇒ Some (acostC (λcc. Sum_any (λac. the_acost cm ac * the_acost (R ac) cc))))"
definition timerefineA ::"('b ⇒ ('c,'d::{complete_lattice,comm_monoid_add,times,mult_zero}) acost)
⇒ ( ('b,'d) acost) ⇒ ( ('c,'d) acost)"
where "timerefineA R cm = (acostC (λcc. Sum_any (λac. the_acost cm ac * the_acost (R ac) cc)))"
lemma timerefineA_0[simp]: "timerefineA r 0 = 0"
by(auto simp: timerefineA_def zero_acost_def)
lemma timerefine_alt: "⇓⇩C R m = case_nrest FAILi (λM. SPECT (timerefineF R M)) m"
unfolding timerefine_def timerefineF_def ..
lemma timerefine_SPECT: "⇓⇩C R (SPECT Q) = SPECT (timerefineF R Q)"
unfolding timerefine_alt by simp
lemma SPEC_timerefine_conv:
"⇓⇩C R (SPEC A B') = SPEC A (λx. timerefineA R (B' x))"
apply(auto simp: SPEC_def)
unfolding timerefine_SPECT
apply auto
unfolding timerefineF_def timerefineA_def
by auto
lemma timerefineA_upd_aux: "(if a = m then x else (0::enat)) * b = (if a = m then x * b else 0)"
by auto
lemma timerefineA_cost_apply: "timerefineA TR (cost n (t::enat)) = acostC (λx. t * the_acost (TR n) x)"
unfolding timerefineA_def cost_def zero_acost_def
apply simp
apply(subst timerefineA_upd_aux)
apply(subst Sum_any.delta) by simp
lemma timerefineA_update_apply_same_cost':
"timerefineA (F(n := y)) (cost n (t::enat)) = t *m y"
by (auto simp: costmult_def timerefineA_def cost_def zero_acost_def timerefineA_upd_aux )
lemma timerefineA_cost_apply_costmult: "timerefineA TR (cost n (t::enat)) = t *m (TR n)"
by (simp add: costmult_def timerefineA_cost_apply)
lemma timerefineA_update_apply_same_cost:
"timerefineA (F(n := y)) (cost n (t::enat)) = acostC (λx. t * the_acost y x)"
by (auto simp: timerefineA_def cost_def zero_acost_def timerefineA_upd_aux )
lemma timerefineA_cost: "timerefineA TR (cost n (1::enat)) = TR n"
unfolding timerefineA_def cost_def zero_acost_def
apply simp
apply(subst timerefineA_upd_aux)
apply(subst Sum_any.delta) by simp
lemma timerefineA_update_cost[simp]:
"n≠m ⟹ timerefineA (F(n := y)) (cost m (t::enat)) = timerefineA F (cost m t)"
by (auto simp: timerefineA_def cost_def zero_acost_def timerefineA_upd_aux )
lemma timerefineA_upd:
fixes R :: "'b ⇒ ('c, enat) acost"
shows "timerefineA (R(n:=y)) (cost m x) = (if n=m then acostC (λz. x * the_acost y z) else timerefineA R (cost m x))"
unfolding timerefineA_def
by (auto simp: cost_def zero_acost_def timerefineA_upd_aux)
definition wfn :: "('a, ('c,'d::{complete_lattice,comm_monoid_add,times,mult_zero}) acost) nrest ⇒ bool" where
"wfn m = (case m of FAILi ⇒ True |
REST M ⇒ ∀r∈dom M. (case M r of None ⇒ True | Some cm ⇒ finite {x. the_acost cm x ≠ 0}))"
definition wfR :: "('b ⇒ ('c, _::mult_zero) acost) ⇒ bool" where
"wfR R = (finite {(s,f). the_acost (R s) f ≠ 0})"
lemma wfR_sup:
fixes A :: "('b ⇒ ('c, enat) acost)"
shows "wfR A ⟹ wfR B ⟹ wfR (sup A B)"
unfolding wfR_def sup_fun_def sup_acost_def sup_enat_def
apply(rule finite_subset[where B="{(s, f). the_acost (A s) f ≠ 0}∪{(s, f). the_acost (B s) f ≠ 0}"])
by auto
definition wfR' :: "('b ⇒ ('c, _::mult_zero) acost) ⇒ bool" where
"wfR' R = (∀s. finite {f. the_acost (R s) f ≠ 0})"
definition wfR'' :: "('b ⇒ ('c, _::mult_zero) acost) ⇒ bool" where
"wfR'' R = (∀f. finite {s. the_acost (R s) f ≠ 0})"
lemma wfR''_upd[intro]: "wfR'' F ⟹ wfR'' (F(x:=y))"
unfolding wfR''_def
apply auto
subgoal for f
apply(rule finite_subset[where B="{s. the_acost (F s) f ≠ 0} ∪ {x}"])
by auto
done
lemma "wfR R ⟹ wfR'' R"
unfolding wfR_def wfR''_def apply safe
subgoal for f
apply(rule finite_cartesian_productD1[where B="{f}"])
apply(rule finite_subset[rotated]) by auto
done
lemma "wfR R ⟹ wfR' R"
unfolding wfR_def wfR'_def apply safe
subgoal for s
apply(rule finite_cartesian_productD2[where A="{s}"])
apply(rule finite_subset) by auto
done
lemma timerefineA_propagate:
assumes "wfR'' E"
fixes a b :: "('a, enat) acost"
shows "timerefineA E (a + b) = timerefineA E a + timerefineA E b"
unfolding timerefineA_def
apply(auto simp: timerefine_def consume_def timerefineA_def split: nrest.splits option.splits intro!: ext)
subgoal for cc
apply(cases a, cases b)
unfolding plus_acost_alt apply simp
unfolding ring_distribs(2)
apply(subst Sum_any.distrib)
subgoal apply(rule finite_subset[OF _ assms[unfolded wfR''_def, rule_format]]) by auto
subgoal apply(rule finite_subset[OF _ assms[unfolded wfR''_def, rule_format]]) by auto
apply simp
done
done
lemma timerefine_consume:
assumes "wfR'' E"
shows "⇓⇩C E (consume M t) = consume (⇓⇩C E (M:: (_, (_, enat) acost) nrest)) (timerefineA E t)"
apply(auto simp: timerefine_def consume_def timerefineA_def split: nrest.splits option.splits intro!: ext)
subgoal for x2 r x2a cc
apply(cases t, cases x2a)
unfolding plus_acost_alt apply simp
unfolding ring_distribs(2)
apply(subst Sum_any.distrib)
subgoal apply(rule finite_subset[OF _ assms[unfolded wfR''_def, rule_format]]) by auto
subgoal apply(rule finite_subset[OF _ assms[unfolded wfR''_def, rule_format]]) by auto
apply simp
done
done
lemma assumes "wfn m"
assumes "m = SPECT M" "M r = Some cm"
shows "finite {ac. the_acost cm ac * the_acost (R ac) cc ≠ 0}"
proof -
from assms have "finite {x. the_acost cm x ≠ 0}" unfolding wfn_def by force
show ?thesis
apply(rule finite_subset[where B="{ac. the_acost cm ac ≠ 0}"])
subgoal by auto
subgoal apply fact done
done
qed
lemma "wfR'' (λx. acostC (λy. if x = y then 1 else 0))"
unfolding wfR''_def
by auto
lemma wfR''_finite_mult_left:
assumes "wfR'' R"
shows "finite {ac. the_acost cm ac * the_acost (R ac) cc ≠ 0}"
proof -
from assms have "finite {s. the_acost (R s) cc ≠ 0}" unfolding wfR''_def by auto
show ?thesis
apply(rule finite_subset[where B="{ac. the_acost (R ac) cc ≠ 0}"])
subgoal by auto
subgoal apply fact done
done
qed
definition wfR2 :: "(('c, _::mult_zero) acost) ⇒ bool" where
"wfR2 R = (finite {f. the_acost R f ≠ 0})"
lemma wfR2_If_if_wfR2: "(I ⟹ wfR2 f) ⟹ wfR2 (if I then f else 0)"
unfolding wfR2_def apply(cases I) by (auto simp: zero_acost_def)
lemma wfR2_enum:
fixes R :: "(('c::enum, _) acost)"
shows "wfR2 R"
unfolding wfR2_def by simp
lemma wfR_fst: "⋀y. wfR R ⟹ finite {x. the_acost (R x) y ≠ 0}"
unfolding wfR_def apply(rule finite_subset[where B="fst ` {(s, f). the_acost (R s) f ≠ 0}"])
subgoal by auto
apply(rule finite_imageI) by simp
lemma wfR_snd: "⋀s. wfR R ⟹ finite {y. the_acost (R s) y ≠ 0}"
unfolding wfR_def apply(rule finite_subset[where B="snd ` {(s, f). the_acost (R s) f ≠ 0}"])
subgoal by auto
apply(rule finite_imageI) by simp
lemma
finite_wfR_middle_mult:
fixes R1 :: "_ ⇒ ('a, 'b::{semiring_no_zero_divisors}) acost"
assumes "wfR R1" "wfR R2"
shows "finite {a. the_acost (R2 x) a * the_acost (R1 a) y ≠ 0}"
proof -
have "{a. the_acost (R2 x) a * the_acost (R1 a) y ≠ 0} = {a. the_acost (R2 x) a ≠ 0 ∧ the_acost (R1 a) y ≠ 0}" by simp
also have "… ⊆ fst ` {(a,a)| a. the_acost (R2 x) a ≠ 0 ∧ the_acost (R1 a) y ≠ 0}" by auto
also have "… ⊆ fst ` ({a. the_acost (R2 x) a ≠ 0} × {a. the_acost (R1 a) y ≠ 0})"
apply(rule image_mono) by auto
finally
show ?thesis apply(rule finite_subset)
apply(rule finite_imageI)
apply(rule finite_cartesian_product)
apply(rule wfR_snd[where R=R2]) apply fact
apply(rule wfR_fst) by fact
qed
lemma wfR_finite_mult_left2:
fixes R2 :: "('b ⇒ ('c, 'd::mult_zero) acost)"
assumes "wfR'' R2"
shows "finite {a. the_acost Mc a * the_acost (R2 a) ac ≠ 0}"
proof -
have "{a. the_acost Mc a * the_acost (R2 a) ac ≠ 0} ⊆ {a. the_acost (R2 a) ac ≠ 0}"
apply(cases Mc) by (auto simp: zero_acost_def)
then
show ?thesis
apply(rule finite_subset)
using assms unfolding wfR''_def by simp
qed
lemma wfR_finite_mult_left:
fixes R2 :: "('b ⇒ ('c, 'd::mult_zero) acost)"
assumes "wfR R2"
shows "finite {a. the_acost Mc a * the_acost (R2 a) ac ≠ 0}"
proof -
have "{a. the_acost Mc a * the_acost (R2 a) ac ≠ 0} ⊆ {a. the_acost (R2 a) ac ≠ 0}"
apply(cases Mc) by (auto simp: zero_acost_def)
then
show ?thesis
apply(rule finite_subset)
apply(rule wfR_fst) by fact
qed
lemma
wfR_finite_crossprod:
assumes "wfR R2"
shows "finite ({a. ∃b. the_acost Mc a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0} × {b. ∃a. the_acost Mc a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0})"
proof -
have i: "{a. ∃b. the_acost Mc a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0} ⊆ fst ` ({(a,b). the_acost (R2 a) b ≠ 0} ∩ {(a,b). the_acost (R1 b) cc ≠ 0})"
apply safe
by (metis (mono_tags, lifting) Int_iff arith_simps(62) arith_simps(63) case_prodI image_eqI mem_Collect_eq prod.sel(1))
have ii: "{b. ∃a. the_acost Mc a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0} ⊆ snd ` ({(a,b). the_acost (R2 a) b ≠ 0} ∩ {(a,b). the_acost (R1 b) cc ≠ 0})"
apply safe
by (metis (mono_tags, lifting) Int_iff arith_simps(62) arith_simps(63) case_prodI image_eqI mem_Collect_eq prod.sel(2))
show ?thesis
apply(rule finite_cartesian_product)
subgoal apply(rule finite_subset[OF i]) apply(rule finite_imageI)
apply(rule finite_Int) using assms wfR_def by auto
subgoal apply(rule finite_subset[OF ii]) apply(rule finite_imageI)
apply(rule finite_Int) using assms wfR_def by auto
done
qed
lemma wfR_finite_Sum_any:
assumes *: "wfR R"
shows "finite {x. ((Sum_any (λac. (the_acost Mc ac * (the_acost (R ac) x)))) ≠ 0)}"
proof -
{fix x
have "((Sum_any (λac. ((the_acost Mc ac) * (the_acost (R ac) x)))) ≠ 0)
⟹ ∃ac. (the_acost Mc ac) * (the_acost (R ac) x) ≠ 0"
using Sum_any.not_neutral_obtains_not_neutral by blast
} then
have "{x. ((Sum_any (λac. ((the_acost Mc ac) * (the_acost (R ac) x)))) ≠ 0)}
⊆ {x. ∃ac. ((the_acost Mc ac) * (the_acost (R ac) x)) ≠ 0}" by blast
also have "… ⊆ snd ` {(ac,x). ((the_acost Mc ac) * (the_acost (R ac) x)) ≠ 0}" by auto
also have "… ⊆ snd ` {(ac,x). (the_acost (R ac) x) ≠ 0}" by auto
finally show ?thesis
apply(rule finite_subset )
apply(rule finite_imageI) using * unfolding wfR_def by auto
qed
lemma wfn_timerefine: "wfn m ⟹ wfR R ⟹ wfn (⇓⇩C R m)"
proof -
assume "wfR R"
then show "wfn (⇓⇩C R m)"
unfolding wfn_def timerefine_def
apply(auto split: nrest.splits option.splits)
apply(rule wfR_finite_Sum_any) by simp
qed
lemma [simp]: "⇓⇩C R FAILT = FAILT" by(auto simp: timerefine_def)
definition pp where
"pp R2 R1 = (λa. acostC (λc. Sum_any (%b. the_acost (R1 a) b * the_acost (R2 b) c ) ))"
lemma pp_fun_upd: "pp A (B(a:=b))
= (pp A B)(a:=timerefineA A b)"
unfolding pp_def timerefineA_def
apply(rule ext) by simp
term case_nrest
thm case_nrest_def
term map_nrest
lemma timerefine_timerefineA:
"⇓⇩C R m =
case_nrest FAILi
(λM. REST (λr. (case_option None
(λcm. Some (timerefineA R cm)) (M r)))) m"
unfolding timerefine_def timerefineA_def by simp
lemma wfR''_ppI_aux: "(⋀s. finite {b. f s b ≠ 0}) ⟹ {s. Sum_any (f s) ≠ (0::enat)} = {s. (∃b. f s b ≠ 0)}"
apply auto
subgoal using Sum_any.not_neutral_obtains_not_neutral by blast
subgoal
by (simp add: Sum_any.expand_set)
done
thm Sum_any.not_neutral_obtains_not_neutral
lemma wfR''_ppI_aux2: "(a::enat) * b ≠ 0 ⟷ a ≠ 0 ∧ b ≠ 0"
by auto
lemma wfR''D: "wfR'' R ⟹ finite {s. the_acost (R s) f ≠ 0}"
by (auto simp: wfR''_def)
lemma
wfR_finite_crossprod2:
fixes Mc :: "('a, enat) acost"
assumes "wfR'' R1" "wfR'' R2"
shows "finite ({a. ∃b. the_acost Mc a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0} × {b. ∃a. the_acost Mc a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0})"
proof -
have **: "{a. ∃b. the_acost Mc a ≠ 0 ∧ the_acost (R2 a) b ≠ 0 ∧ the_acost (R1 b) cc ≠ 0}
⊆ (⋃b∈{b. the_acost (R1 b) cc ≠ 0}. {a. the_acost Mc a ≠ 0 ∧ the_acost (R2 a) b ≠ 0 })"
by auto
show ?thesis
apply(rule finite_cartesian_product)
subgoal
apply(subst wfR''_ppI_aux2)
apply(subst wfR''_ppI_aux2)
apply(rule finite_subset[OF **])
apply(rule finite_Union)
subgoal apply(rule finite_imageI) using assms(1)[THEN wfR''D] by simp
subgoal apply auto subgoal for b apply(rule finite_subset[where B="{s. the_acost (R2 s) b ≠ 0}"])
using assms(2)[THEN wfR''D] by auto
done
done
subgoal
apply(subst wfR''_ppI_aux2)
apply(subst wfR''_ppI_aux2)
apply(rule finite_subset[where B="{b. the_acost (R1 b) cc ≠ 0}"])
subgoal by auto
subgoal using assms(1)[THEN wfR''D] by simp
done
done
qed
lemma timerefineA_iter2:
fixes R1 :: "_ ⇒ ('a, enat) acost"
assumes "wfR'' R1" "wfR'' R2"
shows "timerefineA R1 (timerefineA R2 c) = timerefineA (pp R1 R2) c"
unfolding timerefineA_def pp_def
apply (auto simp: le_fun_def pp_def split: option.splits) apply (rule ext)
apply(subst Sum_any_right_distrib)
subgoal apply(rule wfR''_finite_mult_left[of R1]) using assms by simp_all
subgoal for cc
apply (subst Sum_any.swap[where C="{a. ∃b. the_acost c a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0} × {b. ∃a. the_acost c a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0}"])
subgoal
apply(rule wfR_finite_crossprod2) using assms by auto
subgoal by simp
apply(subst Sum_any_left_distrib)
subgoal apply(rule wfR_finite_mult_left2) using assms by simp
apply(rule Sum_any.cong)
by (meson mult.assoc)
done
lemma pp_assoc:
fixes A :: "'d ⇒ ('b, enat) acost"
assumes A: "wfR'' A"
assumes B: "wfR'' B"
shows "pp A (pp B C) = pp (pp A B) C"
unfolding pp_def
apply(rule ext)
apply simp
apply(rule ext)
apply(subst Sum_any_left_distrib)
subgoal for a c aa
apply(rule finite_subset[where B="{s. the_acost (B s) aa ≠ 0}"])
using assms(2)[THEN wfR''D] by auto
apply(subst Sum_any_right_distrib)
subgoal for a c aa
apply(rule finite_subset[where B="{s. the_acost (A s) c ≠ 0}"])
using assms(1)[THEN wfR''D] by auto
subgoal for a c
apply(subst Sum_any.swap)
prefer 2 apply(rule subset_refl)
apply(rule finite_cartesian_product)
subgoal
apply(rule finite_subset[where B="{b. the_acost (A b) c ≠ 0}"])
subgoal apply auto done
using assms(1)[THEN wfR''D] by blast
subgoal
apply(subst wfR''_ppI_aux2)
apply(subst wfR''_ppI_aux2)
apply(rule finite_subset[where B="(⋃b∈{b. the_acost (A b) c ≠ 0}. {d. the_acost (C a) d ≠ 0 ∧ the_acost (B d) b ≠ 0 })"])
subgoal by auto
apply(rule finite_Union)
subgoal apply(rule finite_imageI) using assms(1)[THEN wfR''D] by simp
subgoal apply auto subgoal for b apply(rule finite_subset[where B="{s. the_acost (B s) b ≠ 0}"])
using assms(2)[THEN wfR''D] by auto
done
done
apply (simp add: mult.assoc)
done
done
subsubsection ‹monotonicity lemmas›
lemma Sum_any_mono:
fixes f :: "('c ⇒ 'b::{nonneg,comm_monoid_add,order,ordered_comm_monoid_add})"
assumes fg: "⋀x. f x ≤ g x"
and finG: "finite {x. g x ≠ 0}"
shows "Sum_any f ≤ Sum_any g"
proof -
have "{x. f x ≠ 0} ⊆ {x. g x ≠ 0}"
apply auto
subgoal for x using fg[of x] needname_nonneg[of " f x"] by auto
done
with finG have "finite {x. f x ≠ 0}"
using finite_subset by blast
thm sum_mono sum_mono2
thm sum_mono2
have "sum f {x. f x ≠ 0} ≤ sum f {x. g x ≠ 0}"
apply(rule sum_mono2) apply fact apply fact
by simp
also have "… ≤ sum g {x. g x ≠ 0}"
apply(rule sum_mono) using fg by simp
finally show ?thesis unfolding Sum_any.expand_set .
qed
lemma finite_support_mult:
fixes R1 :: "('a, 'b::{semiring_no_zero_divisors}) acost"
assumes "finite {xa. the_acost R1 xa ≠ 0}"
and "finite {xa. the_acost R2 xa ≠ 0}"
shows "finite {xa. the_acost R2 xa * the_acost R1 xa ≠ 0}"
proof -
have "{(xa,xa)|xa. the_acost R2 xa * the_acost R1 xa ≠ 0} = {(xa,xa)|xa. the_acost R2 xa ≠ 0 ∧ the_acost R1 xa ≠ 0}" by auto
also have "… ⊆ {(xa,xb)|xa xb. the_acost R2 xa ≠ 0 ∧ the_acost R1 xb ≠ 0}" by auto
also have "… = {xa. the_acost R2 xa ≠ 0} × {xb. the_acost R1 xb ≠ 0}" by auto
finally have k: "{xa. the_acost R2 xa * the_acost R1 xa ≠ 0} ⊆ fst ` ({xa. the_acost R2 xa ≠ 0} × {xb. the_acost R1 xb ≠ 0})" by blast
show ?thesis
apply(rule finite_subset[OF k])
apply(rule finite_imageI)
apply(rule finite_cartesian_product) by fact+
qed
lemma timerefine_mono:
fixes R :: "_ ⇒ ('a, 'b::{complete_lattice,nonneg,mult_zero,ordered_semiring}) acost"
assumes "wfR R"
shows "c≤c' ⟹ ⇓⇩C R c ≤ ⇓⇩C R c'"
apply(cases c) apply simp
apply(cases c') apply (auto simp: less_eq_acost_def timerefine_def split: nrest.splits option.splits simp: le_fun_def)
subgoal by (metis le_some_optE)
proof (goal_cases)
case (1 x2 x2a x x2b x2c xa)
then have l: "⋀ac. the_acost x2b ac ≤ the_acost x2c ac"
apply(cases x2b; cases x2c) unfolding less_eq_acost_def
apply auto
by (metis acost.sel less_eq_acost_def less_eq_option_Some)
show ?case
apply(rule Sum_any_mono)
subgoal using l apply(rule ordered_semiring_class.mult_right_mono) by (simp add: needname_nonneg)
apply(rule wfR_finite_mult_left) by fact
qed
lemma timerefine_mono2:
fixes R :: "_ ⇒ ('a, 'b::{complete_lattice,nonneg,mult_zero,ordered_semiring}) acost"
assumes "wfR'' R"
shows "c≤c' ⟹ ⇓⇩C R c ≤ ⇓⇩C R c'"
apply(cases c) apply simp
apply(cases c') apply (auto simp: less_eq_acost_def timerefine_def split: nrest.splits option.splits simp: le_fun_def)
subgoal by (metis le_some_optE)
proof (goal_cases)
case (1 x2 x2a x x2b x2c xa)
then have l: "⋀ac. the_acost x2b ac ≤ the_acost x2c ac"
apply(cases x2b; cases x2c) unfolding less_eq_acost_def
apply auto
by (metis acost.sel less_eq_acost_def less_eq_option_Some)
show ?case
apply(rule Sum_any_mono)
subgoal using l apply(rule ordered_semiring_class.mult_right_mono) by (simp add: needname_nonneg)
apply(rule wfR_finite_mult_left2) by fact
qed
thm wfR''_def
lemma timerefine_mono3:
fixes R :: "_ ⇒ ('a, enat) acost"
assumes "wfR'' R"
shows "c≤c' ⟹ R=R' ⟹ timerefine R c ≤ timerefine R' c'"
apply simp
apply(rule timerefine_mono2)
using assms by auto
lemma timerefine_mono_both:
fixes R :: "_ ⇒ ('c, 'd::{complete_lattice,nonneg,mult_zero,ordered_semiring}) acost"
assumes "wfR'' R'"
and "R≤R'"
shows "c≤c' ⟹ timerefine R c ≤ timerefine R' c'"
apply(cases c) apply simp
apply(cases c') apply (auto simp: less_eq_acost_def timerefine_def split: nrest.splits option.splits simp: le_fun_def)
subgoal by (metis le_some_optE)
proof (goal_cases)
case (1 x2 x2a x x2b x2c xa)
then have l: "⋀ac. the_acost x2b ac ≤ the_acost x2c ac"
apply(cases x2b; cases x2c) unfolding less_eq_acost_def
apply auto
by (metis acost.sel less_eq_acost_def less_eq_option_Some)
show ?case
apply(rule Sum_any_mono)
subgoal using l apply(rule ordered_semiring_class.mult_mono)
subgoal using assms(2) unfolding le_fun_def
by (simp add: the_acost_mono)
subgoal by (simp add: needname_nonneg)
subgoal
by (simp add: needname_nonneg)
done
apply(rule wfR_finite_mult_left2) by fact
qed
lemma wfR''_ppI:
fixes R1 :: "'a ⇒ ('b, enat) acost"
assumes R1: "wfR'' R1" and R2: "wfR'' R2"
shows "wfR'' (pp R1 R2)"
unfolding pp_def wfR''_def
apply simp apply safe
proof -
fix f
have "⋀s. finite {b. the_acost (R2 s) b * the_acost (R1 b) f ≠ 0}"
apply(rule wfR_finite_mult_left2) by fact
have l: "{s. ∃b. the_acost (R2 s) b ≠ 0 ∧ the_acost (R1 b) f ≠ 0}
= (⋃b∈{b. the_acost (R1 b) f ≠ 0}. {s. the_acost (R2 s) b ≠ 0 })"
by auto
show "finite {s. (∑b. the_acost (R2 s) b * the_acost (R1 b) f) ≠ 0}"
apply(subst wfR''_ppI_aux) apply fact
apply(subst wfR''_ppI_aux2)
apply(subst l)
apply(rule finite_Union)
subgoal apply(rule finite_imageI) by (rule R1[THEN wfR''D])
subgoal
using R2
by (auto simp: wfR''_def)
done
qed
lemma
fixes R1 :: "_ ⇒ ('a, enat) acost"
assumes "wfR'' R1" "wfR'' R2"
shows timerefine_iter2: "⇓⇩C R1 (⇓⇩C R2 c) = ⇓⇩C (pp R1 R2) c"
unfolding timerefine_timerefineA
apply(subst timerefineA_iter2[OF assms, symmetric])
by (auto split: nrest.splits option.splits)
lemma
fixes R1 :: "_ ⇒ ('a, 'b::{complete_lattice,nonneg,ordered_semiring,semiring_no_zero_divisors}) acost"
assumes "wfR R1" "wfR R2"
shows timerefine_iter: "⇓⇩C R1 (⇓⇩C R2 c) = ⇓⇩C (pp R1 R2) c"
unfolding timerefine_def
apply(cases c)
subgoal by simp
apply (auto simp: le_fun_def pp_def split: option.splits) apply (rule ext)
apply (auto simp: le_fun_def pp_def split: option.splits)
apply(subst Sum_any_right_distrib)
subgoal apply(rule finite_wfR_middle_mult[of R1 R2]) using assms by simp_all
apply (rule ext)
subgoal for mc r Mc cc
apply (subst Sum_any.swap[where C="{a. ∃b. the_acost Mc a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0} × {b. ∃a. the_acost Mc a * (the_acost (R2 a) b * the_acost (R1 b) cc) ≠ 0}"])
subgoal apply(rule wfR_finite_crossprod) using assms by simp
subgoal by simp
apply(subst Sum_any_left_distrib)
subgoal apply(rule wfR_finite_mult_left) using assms by simp
apply(rule Sum_any.cong)
by (meson mult.assoc)
done
lemma timerefine_trans:
fixes R1 :: "_ ⇒ ('a, 'b::{complete_lattice,nonneg,ordered_semiring,semiring_no_zero_divisors}) acost"
assumes "wfR R1" "wfR R2" shows
"a ≤ ⇓⇩C R1 b ⟹ b ≤ ⇓⇩C R2 c ⟹ a ≤ ⇓⇩C (pp R1 R2) c"
apply(subst timerefine_iter[symmetric, OF assms])
apply(rule order.trans) apply simp
apply(rule timerefine_mono) using assms by auto
subsection ‹Timerefine with monadic operations›
lemma timerefine_RETURNT: "⇓⇩C E (RETURNT x') = RETURNT x'"
by (auto simp: timerefine_def RETURNT_def zero_acost_def)
lemma timerefine_SPECT_map: "⇓⇩C E (SPECT [x'↦t]) = SPECT [x'↦timerefineA E t]"
by (auto simp: timerefine_def timerefineA_def intro!: ext)
subsection ‹enum setup›
lemma (in enum) sum_to_foldr: "sum f UNIV
= foldr (λx a. a + f x) enum 0"
unfolding UNIV_enum using enum_distinct
apply(simp add: sum.distinct_set_conv_list )
apply(simp only: sum_list.eq_foldr foldr_map)
by (metis add.commute comp_apply)
lemma (in enum) Sum_any_to_foldr: "Sum_any f
= foldr (λx a. a + f x) enum 0"
apply(subst Sum_any.expand_superset[where A=UNIV])
by (simp_all add: sum_to_foldr)
subsection ‹Time Refinement and bind›
lemma nofailT_timerefine[refine_pw_simps]: "nofailT (⇓⇩C R m) ⟷ nofailT m"
unfolding nofailT_def timerefine_def by (auto split: nrest.splits)
definition inresTf' :: "('a,('b,enat)acost) nrest ⇒ 'a ⇒ (('b,enat)acost) ⇒ bool" where
"inresTf' S x t ≡ (∀b. (case S of FAILi ⇒ True | REST X ⇒ (∃t'. X x = Some t' ∧ (the_acost t b) ≤ the_acost t' b)) )"
lemma pw_bindT_nofailTf' : "nofailT (bindT M f) ⟷ (nofailT M ∧ (∀x t. inresTf' M x t ⟶ nofailT (f x)))"
unfolding bindT_def
apply (auto elim: no_FAILTE simp: refine_pw_simps split: nrest.splits )
subgoal
by (smt inresTf'_def nofailT_simps(2) nrest.simps(5))
subgoal for M x t unfolding inresTf'_def apply auto
proof (goal_cases)
case 1
then have "⋀t. ∀b. ∃t'. M x = Some t' ∧ (the_acost t b) ≤ the_acost t' b ⟹ nofailT (f x)" by blast
with 1(1,3,4) show ?case
by auto
qed
done
lemmas limit_bindT = project_acost_bindT
definition "limRef b R m = (case m of FAILi ⇒ FAILi | REST M ⇒ SPECT (λr. case M r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b))))"
lemma limRef_limit_timerefine: "(project_acost b (⇓⇩C R m)) = limRef b R m"
unfolding limRef_def project_acost_def timerefine_def apply(cases m) by (auto split: option.splits)
lemma inresTf'_timerefine: "inresTf' (⇓⇩C R m) x t ⟹ ∃t'. inresTf' m x t'"
unfolding inresTf'_def timerefine_def by (auto split: nrest.splits option.splits)
lemma ff: "c≤a ⟹ inresT c x t ⟹ inresT a x t"
unfolding inresT_def by (auto split: nrest.splits)
lemma pl2:
fixes R ::"_ ⇒ ('a, enat) acost"
assumes "Ra ≠ {}" and "wfR'' R"
shows " Sup { Some (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra}
≤ Some (Sum_any (λac. (SUP f∈Ra. the_acost f ac) * the_acost (R ac) b))"
proof -
have *: "{ Some (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra} =
Some ` { (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra}" by blast
have *: "Sup { Some (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra}
= SUPREMUM { (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra} Some "
unfolding * by simp
have a: "⋀ac. (SUP f∈Ra. the_acost f ac) * the_acost (R ac) b = (SUP f∈Ra. the_acost f ac * the_acost (R ac) b)"
apply(subst enat_mult_cont') by simp
have e: "finite {x. the_acost (R x) b ≠ 0}" using assms(2) unfolding wfR''_def by simp
show ?thesis unfolding *
apply(subst Some_Sup[symmetric]) using assms apply simp
apply simp
unfolding a apply(rule order.trans[OF _ enat_Sum_any_cont])
subgoal by (simp add: setcompr_eq_image)
subgoal apply(rule finite_subset[OF _ e]) by auto
done
qed
lemma pl:
fixes R ::"_ ⇒ ('a, enat) acost"
assumes "Ra ≠ {}" and "wfR R"
shows " Sup { Some (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra}
≤ Some (Sum_any (λac. (SUP f∈Ra. the_acost f ac) * the_acost (R ac) b))"
proof -
have *: "{ Some (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra} =
Some ` { (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra}" by blast
have *: "Sup { Some (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra}
= SUPREMUM { (Sum_any (λac. the_acost x ac * the_acost (R ac) b)) |x. x ∈ Ra} Some "
unfolding * by simp
have a: "⋀ac. (SUP f∈Ra. the_acost f ac) * the_acost (R ac) b = (SUP f∈Ra. the_acost f ac * the_acost (R ac) b)"
apply(subst enat_mult_cont') by simp
have e: "finite {x. the_acost (R x) b ≠ 0}" apply(rule wfR_fst) by fact
show ?thesis unfolding *
apply(subst Some_Sup[symmetric]) using assms apply simp
apply simp
unfolding a apply(rule order.trans[OF _ enat_Sum_any_cont])
subgoal by (simp add: setcompr_eq_image)
subgoal apply(rule finite_subset[OF _ e]) by auto
done
qed
lemma oo: "Option.these (Ra - {None}) = Option.these (Ra)"
by (metis insert_Diff_single these_insert_None)
lemma Sup_wo_None: "Ra ≠ {} ∧ Ra ≠ {None} ⟹ Sup Ra = Sup (Ra-{None})"
unfolding Sup_option_def apply auto unfolding oo by simp
term continuous
thm continuous_option
lemma kkk2:
fixes R ::"_ ⇒ ('a,enat) acost"
assumes "wfR'' R"
shows
" (case SUP x∈Ra. x of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b)))
≥ Sup {case x of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b)) |x. x ∈ Ra}"
apply(cases "Ra={} ∨ Ra = {None}")
subgoal by (auto split: option.splits simp: bot_option_def)
subgoal apply(subst (2) Sup_option_def) apply simp unfolding Sup_acost_def apply simp
proof -
assume r: "Ra ≠ {} ∧ Ra ≠ {None}"
then obtain x where x: "Some x ∈ Ra"
by (metis everywhereNone not_None_eq)
have kl: "Sup {case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}
= Sup ({case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}-{None})"
apply(subst Sup_wo_None)
subgoal apply safe subgoal using x by auto subgoal using x by force
done by simp
also have "({case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}-{None})
= ({case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra ∧ x≠None})"
by (auto split: option.splits)
also have "… = ({ Some (∑ac. the_acost x ac * the_acost (R ac) b) |x. x∈Option.these Ra})"
by (force split: option.splits simp: Option.these_def)
finally have rrr: "Sup {case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}
= Sup ({ Some (∑ac. the_acost x ac * the_acost (R ac) b) |x. x∈Option.these Ra})" .
show "Sup {case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}
≤ Some (∑ac. (SUP f∈Option.these Ra. the_acost f ac) * the_acost (R ac) b)"
unfolding rrr apply(subst pl2)
subgoal using x unfolding Option.these_def by auto
subgoal by fact
apply simp done
qed
done
lemma kkk:
fixes R ::"_ ⇒ ('a,enat) acost"
assumes "wfR R"
shows
" (case SUP x∈Ra. x of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b)))
≥ Sup {case x of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b)) |x. x ∈ Ra}"
apply(cases "Ra={} ∨ Ra = {None}")
subgoal by (auto split: option.splits simp: bot_option_def)
subgoal apply(subst (2) Sup_option_def) apply simp unfolding Sup_acost_def apply simp
proof -
assume r: "Ra ≠ {} ∧ Ra ≠ {None}"
then obtain x where x: "Some x ∈ Ra"
by (metis everywhereNone not_None_eq)
have kl: "Sup {case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}
= Sup ({case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}-{None})"
apply(subst Sup_wo_None)
subgoal apply safe subgoal using x by auto subgoal using x by force
done by simp
also have "({case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}-{None})
= ({case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra ∧ x≠None})"
by (auto split: option.splits)
also have "… = ({ Some (∑ac. the_acost x ac * the_acost (R ac) b) |x. x∈Option.these Ra})"
by (force split: option.splits simp: Option.these_def)
finally have rrr: "Sup {case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}
= Sup ({ Some (∑ac. the_acost x ac * the_acost (R ac) b) |x. x∈Option.these Ra})" .
show "Sup {case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}
≤ Some (∑ac. (SUP f∈Option.these Ra. the_acost f ac) * the_acost (R ac) b)"
unfolding rrr apply(subst pl)
subgoal using x unfolding Option.these_def by auto
subgoal by fact
apply simp done
qed
done
lemma
aaa: fixes R ::"_ ⇒ ('a,enat) acost"
assumes "wfR'' R"
shows
"(case SUP x∈Ra. x r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b)))
≥ Sup {case x r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b)) |x. x∈Ra}"
proof -
have *: "{case x r of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}
= {case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ (λf. f r) ` Ra}"
by auto
have **: "⋀f. (case SUP x∈Ra. x r of None ⇒ None | Some cm ⇒ f cm)
= (case SUP x∈(λf. f r) ` Ra. x of None ⇒ None | Some cm ⇒ f cm)"
by auto
show ?thesis unfolding * ** apply(rule kkk2) by fact
qed
lemma
***: fixes R ::"_ ⇒ ('a,enat) acost"
assumes "wfR R"
shows
"(case SUP x∈Ra. x r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b)))
≥ Sup {case x r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b)) |x. x∈Ra}"
proof -
have *: "{case x r of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ Ra}
= {case x of None ⇒ None | Some cm ⇒ Some (∑ac. the_acost cm ac * the_acost (R ac) b) |x. x ∈ (λf. f r) ` Ra}"
by auto
have **: "⋀f. (case SUP x∈Ra. x r of None ⇒ None | Some cm ⇒ f cm)
= (case SUP x∈(λf. f r) ` Ra. x of None ⇒ None | Some cm ⇒ f cm)"
by auto
show ?thesis unfolding * ** apply(rule kkk) by fact
qed
lemma nofail'': "x ≠ FAILT ⟷ (∃m. x=SPECT m)"
unfolding nofailT_def
using nrest_noREST_FAILT by blast
lemma limRef_bindT_le2:
fixes R ::"_ ⇒ ('a,enat) acost" assumes "wfR'' R"
shows "limRef b R (bindT m f) ≥ (case m of FAILi ⇒ FAILT | REST X ⇒ Sup {case f x of FAILi ⇒ FAILT | REST m2 ⇒ SPECT (λr. case (map_option ((+) t1) ∘ m2) r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b))) |x t1. X x = Some t1})"
unfolding limRef_def bindT_def apply(cases m) apply auto
unfolding Sup_nrest_def apply (auto split: nrest.splits)
apply(rule le_funI) apply simp unfolding Sup_fun_def
subgoal
apply(rule order.trans) defer
apply(subst aaa[OF assms]) apply simp
apply(rule Sup_least)
apply auto
apply(subst (asm) nofail'') apply (auto split: option.splits)
apply(rule Sup_upper)
apply auto
subgoal for xa t1 ma x2
apply(rule exI[where x="map_option ((+) t1) ∘ ma"])
apply safe subgoal apply simp done
subgoal by auto
apply(rule exI[where x=xa])
by simp
done
done
lemma limRef_bindT_le:
fixes R ::"_ ⇒ ('a,enat) acost" assumes "wfR R"
shows "limRef b R (bindT m f) ≥ (case m of FAILi ⇒ FAILT | REST X ⇒ Sup {case f x of FAILi ⇒ FAILT | REST m2 ⇒ SPECT (λr. case (map_option ((+) t1) ∘ m2) r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b))) |x t1. X x = Some t1})"
unfolding limRef_def bindT_def apply(cases m) apply auto
unfolding Sup_nrest_def apply (auto split: nrest.splits)
apply(rule le_funI) apply simp unfolding Sup_fun_def
subgoal
apply(rule order.trans) defer
apply(subst ***[OF assms]) apply simp
apply(rule Sup_least)
apply auto
apply(subst (asm) nofail'') apply (auto split: option.splits)
apply(rule Sup_upper)
apply auto
subgoal for xa t1 ma x2
apply(rule exI[where x="map_option ((+) t1) ∘ ma"])
apply safe subgoal apply simp done
subgoal by auto
apply(rule exI[where x=xa])
by simp
done
done
lemma nofailT_limRef: "nofailT (limRef b R m) ⟷ nofailT m"
unfolding limRef_def nofailT_def by (auto split: nrest.splits)
lemma inresT_limRef_D: "inresT (limRef b R (SPECT x2)) r' t' ⟹ (∃x2a. x2 r' = Some x2a ∧ enat t' ≤ (Sum_any (λac. the_acost x2a ac * the_acost (R ac) b)))"
unfolding limRef_def apply simp
by (auto split: option.splits)
lemma zzz: fixes A B :: "('a, enat) acost"
shows "the_acost (case A of acostC a ⇒ case B of acostC b ⇒ acostC (λx. a x + b x)) a *
the_acost (R a) b =
the_acost A a * the_acost (R a) b + the_acost B a * the_acost (R a) b"
apply(cases A; cases B) apply auto
by (simp add: comm_semiring_class.distrib)
lemma timerefine_bindT_ge:
fixes R :: "_ ⇒ ('a,enat) acost"
assumes wfR: "wfR R"
shows "bindT (⇓⇩C R m) (λx. ⇓⇩C R (f x)) ≤ ⇓⇩C R (bindT m f)"
unfolding pw_acost_le_iff'
apply safe
subgoal apply (simp add: nofailT_timerefine nofailT_project_acost pw_bindT_nofailTf')
apply auto apply(frule inresTf'_timerefine) by simp
subgoal for b x t
unfolding limit_bindT
unfolding pw_inresT_bindT
unfolding limRef_limit_timerefine
apply(rule ff[OF limRef_bindT_le]) using assms apply simp
apply(simp add: nofailT_limRef)
apply(cases m) subgoal by auto
apply simp
unfolding pw_inresT_Sup apply auto
apply(drule inresT_limRef_D) apply auto
subgoal for x2 r' t' t'' x2a
apply(rule exI[where x="(case f r' of FAILi ⇒ FAILT | REST m2 ⇒ SPECT (λr. case (map_option ((+) x2a) ∘ m2) r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b))))"])
apply safe
apply(rule exI[where x=r'])
apply(rule exI[where x=x2a])
apply simp
apply (cases "f r'") subgoal by auto
apply simp
apply(drule inresT_limRef_D) apply auto
apply(rule exI[where x="t' + t''"]) apply (simp add: zzz comm_semiring_class.distrib plus_acost_alt )
apply(subst Sum_any.distrib)
subgoal apply(rule wfR_finite_mult_left) using wfR by simp
subgoal apply(rule wfR_finite_mult_left) using wfR by simp
subgoal
using add_mono by fastforce
done
done
done
lemma timerefine_bindT_ge2:
fixes R :: "_ ⇒ ('a,enat) acost"
assumes wfR'': "wfR'' R"
shows "bindT (⇓⇩C R m) (λx. ⇓⇩C R (f x)) ≤ ⇓⇩C R (bindT m f)"
unfolding pw_acost_le_iff'
apply safe
subgoal apply (simp add: nofailT_timerefine nofailT_project_acost pw_bindT_nofailTf')
apply auto apply(frule inresTf'_timerefine) by simp
subgoal for b x t
unfolding limit_bindT
unfolding pw_inresT_bindT
unfolding limRef_limit_timerefine
apply(rule ff[OF limRef_bindT_le2])
using assms
apply simp
apply(simp add: nofailT_limRef)
apply(cases m) subgoal by auto
apply simp
unfolding pw_inresT_Sup apply auto
apply(drule inresT_limRef_D) apply auto
subgoal for x2 r' t' t'' x2a
apply(rule exI[where x="(case f r' of FAILi ⇒ FAILT | REST m2 ⇒ SPECT (λr. case (map_option ((+) x2a) ∘ m2) r of None ⇒ None | Some cm ⇒ Some (Sum_any (λac. the_acost cm ac * the_acost (R ac) b))))"])
apply safe
apply(rule exI[where x=r'])
apply(rule exI[where x=x2a])
apply simp
apply (cases "f r'") subgoal by auto
apply simp
apply(drule inresT_limRef_D) apply auto
apply(rule exI[where x="t' + t''"]) apply (simp add: zzz comm_semiring_class.distrib plus_acost_alt )
apply(subst Sum_any.distrib)
subgoal apply(rule wfR''_finite_mult_left) using wfR'' by simp
subgoal apply(rule wfR''_finite_mult_left) using wfR'' by simp
subgoal
using add_mono by fastforce
done
done
done
lemma timerefine_R_mono:
fixes R :: "_ ⇒ ('a, enat) acost"
assumes "wfR R'"
shows "R≤R' ⟹ ⇓⇩C R c ≤ ⇓⇩C R' c"
unfolding timerefine_def apply(cases c)
apply (auto intro!: le_funI simp: less_eq_acost_def split: option.splits)
apply(rule Sum_any_mono)
apply(rule mult_left_mono) apply(auto simp: le_fun_def)
subgoal premises prems for x2 x x2a xa xb
using prems(1)[rule_format, of xb] apply(cases "R xb"; cases "R' xb") apply auto
unfolding less_eq_acost_def by auto
subgoal for x2 x x2a xa using assms(1) unfolding wfR_def
apply -
apply(rule finite_subset[where B="{x. the_acost (R' x) xa ≠ 0}"]) apply auto
apply(rule wfR_fst) apply (rule assms) done
done
lemma timerefine_R_mono_wfR'':
fixes R :: "_ ⇒ ('a, enat) acost"
assumes "wfR'' R'"
shows "R≤R' ⟹ ⇓⇩C R c ≤ ⇓⇩C R' c"
unfolding timerefine_def apply(cases c)
apply (auto intro!: le_funI simp: less_eq_acost_def split: option.splits)
apply(rule Sum_any_mono)
apply(rule mult_left_mono) apply(auto simp: le_fun_def)
subgoal premises prems for x2 x x2a xa xb
using prems(1)[rule_format, of xb] apply(cases "R xb"; cases "R' xb") apply auto
unfolding less_eq_acost_def by auto
subgoal for x2 x x2a xa using assms(1) unfolding wfR_def
apply -
apply(rule finite_subset[where B="{x. the_acost (R' x) xa ≠ 0}"]) apply auto
using assms[unfolded wfR''_def] apply simp done
done
subsection ‹Structure Preserving›
definition "struct_preserving E ≡ (∀t. cost ''call'' t ≤ timerefineA E (cost ''call'' t))
∧ (∀t. cost ''if'' t ≤ timerefineA E (cost ''if'' t))"
lemma struct_preservingI:
assumes "⋀t. cost ''call'' t ≤ timerefineA E (cost ''call'' t)"
"⋀t. cost ''if'' t ≤ timerefineA E (cost ''if'' t)"
shows "struct_preserving E"
using assms unfolding struct_preserving_def by auto
lemma struct_preservingD:
assumes "struct_preserving E"
shows "⋀t. cost ''call'' t ≤ timerefineA E (cost ''call'' t)"
"⋀t. cost ''if'' t ≤ timerefineA E (cost ''if'' t)"
using assms unfolding struct_preserving_def by auto
lemma struct_preserving_upd_I[intro]:
fixes F:: "char list ⇒ (char list, enat) acost"
shows "struct_preserving F ⟹ x≠''if''⟹ x≠''call'' ⟹ struct_preserving (F(x:=y))"
by (auto simp: struct_preserving_def)
subsection ‹preserving currency›
definition "preserves_curr R n ⟷ (R n = (cost n 1))"
lemma preserves_curr_other_updI:
"preserves_curr R m ⟹ n≠m ⟹ preserves_curr (R(n:=t)) m"
by(auto simp: preserves_curr_def)
lemma preserves_curr_D: "preserves_curr R n ⟹ R n = (cost n 1)"
unfolding preserves_curr_def by metis
subsection ‹TId›
definition "TId = (λx. acostC (λy. (if x=y then 1 else 0)))"
lemma TId_apply: "TId x = cost x 1"
by (auto simp add: cost_def TId_def zero_acost_def)
lemma preserves_curr_TId[simp]: "preserves_curr TId n"
by(auto simp: preserves_curr_def TId_def cost_def zero_acost_def)
lemma cost_n_leq_TId_n: "cost n (1::enat) ≤ TId n"
by(auto simp: TId_def cost_def zero_acost_def less_eq_acost_def)
lemma timerefine_id:
fixes M :: "(_,(_,enat)acost) nrest"
shows "⇓⇩C TId M = M"
apply(cases M; auto simp: timerefine_def TId_def)
apply(rule ext) apply(auto split: option.splits)
subgoal for x2 r x2a apply(cases x2a) apply simp
apply(rule ext) apply(simp add: if_distrib)
apply(subst mult_zero_right)
apply(subst Sum_any.delta) by simp
done
lemma timerefineA_TId:
fixes T :: "(_,enat) acost"
shows "T ≤ T' ⟹ T ≤ timerefineA TId T'"
unfolding timerefineA_def TId_def
apply(simp add: if_distrib)
apply(subst mult_zero_right)
apply(subst Sum_any.delta) by(cases T; cases T'; auto)
lemma sp_TId[simp]: "struct_preserving (TId::_⇒(string, enat) acost)"
by (auto intro!: struct_preservingI simp: timerefineA_upd timerefineA_TId)
lemma timerefineA_TId_aux: "the_acost x a * (if b then (1::enat) else 0)
= (if b then the_acost x a else 0)"
apply(cases b) by auto
lemma pp_TId_absorbs_right:
fixes A :: "'b ⇒ ('c, enat) acost"
shows "pp A TId = A"
unfolding pp_def TId_def apply simp
apply(rule ext) apply(subst timerefineA_upd_aux)
by simp
lemma pp_TId_absorbs_left:
fixes A :: "'b ⇒ ('c, enat) acost"
shows "pp TId A = A"
unfolding pp_def TId_def apply simp
apply(rule ext) apply(subst timerefineA_TId_aux)
by simp
lemma timerefineA_TId_eq[simp]:
shows "timerefineA TId x = (x:: ('b, enat) acost)"
unfolding timerefineA_def TId_def
by (simp add: timerefineA_TId_aux)
lemma wfR_TId: "wfR TId"
unfolding TId_def wfR_def apply simp
oops
lemma "wfR' TId"
unfolding TId_def wfR'_def by simp
lemma wfR''_TId[simp]: "wfR'' TId"
unfolding TId_def wfR''_def by simp
subsection ‹Stuff about integrating functional Specification (with top time)›
lemma getDiff: assumes "A ⊆ C"
shows "∃B. C = A ∪ B ∧ A ∩ B = {}"
using assms
by (metis Diff_disjoint Diff_partition)
lemma sum_extend_zeros:
assumes "finite B" "{x. f x≠0} ⊆ B"
shows "sum f B = sum f {x. f x≠0}"
proof -
from assms(2) obtain A where B: "B = A ∪ {x. f x≠0}" and disj[simp]: "A ∩ {x. f x≠0} = {}"
by (metis Int_commute getDiff sup_commute)
from assms(1) B have [simp]: "finite A" "finite {x. f x≠0}" by auto
have *: "sum f A = 0"
apply(rule sum.neutral)
using disj by blast
show ?thesis
unfolding B
by(simp add: * sum.union_disjoint)
qed
lemma inf_acost: "inf (acostC a) (acostC b) = acostC (inf a b)"
unfolding inf_acost_def by auto
lemma inf_absorbs_top_aux1: "⋀a. a ≠ 0 ⟹ a * top = (top::enat)"
unfolding top_enat_def
by (simp add: imult_is_infinity)
lemma inf_absorbs_top_aux2: "⋀a. a ≠ 0 ⟹ top * a = (top::enat)"
unfolding top_enat_def
by (simp add: imult_is_infinity)
lemma inf_absorbs_top:
fixes a b :: enat
shows "inf (a * b) (a * top) = a * b"
apply(cases "a=0"; cases "b=0") by (auto simp: inf_absorbs_top_aux1)
lemma inf_absorbs_top2:
fixes a b :: enat
shows "inf (b * a) (top * a) = b * a"
apply(cases "a=0"; cases "b=0") by (auto simp: inf_absorbs_top_aux2)
lemma timerefine_inf_top_distrib_aux1:
fixes f :: "_ ⇒ enat"
assumes F: "finite {x. f x ≠ 0}"
shows " Sum_any (inf (λx. f x * g x) (λx. f x * top))
= inf (Sum_any (λx. f x * g x)) (Sum_any (λx. f x * top))"
proof (cases "{x. f x ≠ 0} = {}")
case True
then show ?thesis
unfolding Sum_any.expand_set by simp
next
case False
with F have cn0: "card {x. f x ≠ 0} ≠ 0" by simp
have 1: "{a. inf (λx. (f x * g x)) (λx. (f x) * top) a ≠ 0}
⊆ {x. f x ≠ 0}" by auto
have 2: "{a. f a * g a ≠ 0} ⊆ {x. f x ≠ 0}" by auto
have 3: "{a. f a * top ≠ 0} ⊆ {x. f x ≠ 0}" by auto
{ fix a b :: enat
have "inf (a * b) (a * top) = a * b"
apply(cases "a=0"; cases "b=0") by (auto simp: inf_absorbs_top_aux1)
} note * = this
have "(∑a∈{x. f x ≠ 0}. f a * top) = (∑a∈{x. f x ≠ 0}. top)"
apply(rule sum.cong) apply simp by (auto simp: top_enat_def imult_is_infinity)
also have "… = top"
using False cn0 by (simp add: top_enat_def imult_is_infinity)
finally have i: "(∑a∈{x. f x ≠ 0}. f a * top) = top" .
show ?thesis
unfolding Sum_any.expand_set
apply(subst sum_extend_zeros[symmetric, OF _ 1]) apply fact
apply(subst sum_extend_zeros[symmetric, OF _ 2]) apply fact
apply(subst sum_extend_zeros[symmetric, OF _ 3]) apply fact
by (simp add: * i)
qed
lemma timerefine_inf_top_distrib_aux2:
fixes f :: "_ ⇒ enat"
assumes F: "finite {x. f x ≠ 0}"
shows "inf (Sum_any (λx. g x * f x)) (Sum_any (λx. top * f x))
= Sum_any (inf (λx. g x * f x) (λx. top * f x))"
apply(subst (1) mult.commute)
apply(subst (2) mult.commute)
apply(subst timerefine_inf_top_distrib_aux1[symmetric]) apply fact
by(simp add: mult.commute)
lemma timerefine_inf_top_distrib:
fixes m :: "('a, ('d, enat) acost) nrest"
assumes a: "⋀cc. finite {x. the_acost (R x) cc ≠ 0}"
shows "⇓⇩C R (inf m (SPEC P (λ_. top)))
= inf (⇓⇩C R m) (⇓⇩C R (SPEC P (λ_. top)))"
unfolding timerefine_def SPEC_def
apply(cases m) apply simp apply simp apply(rule ext)
apply auto
subgoal for x2 r
apply(cases "x2 r") apply simp
apply simp
unfolding inf_acost apply simp apply(rule ext)
apply (simp add: top_acost_def)
apply(subst timerefine_inf_top_distrib_aux2) apply (rule a)
apply(subst inf_fun_def)
using inf_absorbs_top2
apply(subst inf_absorbs_top2) by simp
done
lemma
SPEC_timerefine:
"A ≤ A' ⟹ (⋀x. B x ≤ timerefineA R (B' x)) ⟹ SPEC A B ≤ ⇓⇩C R (SPEC A' B')"
apply(auto simp: SPEC_def)
unfolding timerefine_SPECT
apply (simp add: le_fun_def) apply auto
unfolding timerefineF_def timerefineA_def
by auto
lemma SPECT_emb'_timerefine:
"
(⋀x. Q x ⟹ Q' x)
⟹
(⋀x. T x ≤ timerefineA E (T' x))
⟹
SPECT (emb' Q T) ≤ ⇓⇩C E (SPECT (emb' Q' T'))"
unfolding SPEC_REST_emb'_conv[symmetric]
apply(rule SPEC_timerefine) by (auto intro: le_funI)
lemma
SPEC_timerefine_eq:
"(⋀x. B x = timerefineA R (B' x)) ⟹ SPEC A B = ⇓⇩C R (SPEC A B')"
apply(auto simp: SPEC_def)
unfolding timerefine_SPECT
apply auto
unfolding timerefineF_def timerefineA_def
by auto
lemma finite_sum_nonzero_cost:
"finite {a. the_acost (cost n m) a ≠ 0}"
unfolding cost_def by (auto simp: zero_acost_def)
lemma finite_sum_nonzero_if_summands_finite_nonzero:
"finite {a. f a ≠ 0} ⟹ finite {a. g a ≠ 0} ⟹ finite {a. (f a ::nat) + g a ≠ 0}"
apply(rule finite_subset[where B="{a. f a ≠ 0} ∪ {a. g a ≠ 0}"])
by auto
end