Theory Phi_System.Resource_Template
theory Resource_Template
imports PhiSem_Formalization_Tools Phi_Semantics_Framework.Phi_SemFrame_ex Phi_Fictions
begin
chapter ‹Resource Bases and Templates›
section ‹Preliminary›
interpretation to_share: cancl_share_orthogonal_homo ‹to_share::'a::{discrete_semigroup, sep_carrier} option ⇒ 'a share option›
‹Collect mul_carrier› ..
interpretation pointwise_to_share:
cancl_share_orthogonal_homo ‹(o) (to_share::'a::{discrete_semigroup, sep_carrier} option ⇒ 'a share option)›
‹pointwise_set (Collect mul_carrier)›
by (standard; standard)
section ‹Bases›
subsection ‹Resource Base›
locale resource =
resource_kind RES.DOMAIN Res
for Res :: "'T::sep_algebra resource_entry"
begin
lemma get_res_valid_raw:
‹ res ∈ RES.SPACE
⟹ get res ∈⇩S⇩H domain›
unfolding RES.SPACE_def
by (simp, metis in_DOMAIN proj_inj)
definition [simp]: ‹basic_fiction x = Itself (1(Res #= x))›
lemma basic_fiction_homo_one[simp]:
‹homo_one basic_fiction›
unfolding homo_one_def basic_fiction_def by (simp add: BI_eq_iff)
subsubsection ‹Getter›
definition φR_get_res' :: ‹'T proc›
where ‹φR_get_res' = (λres. Return (φarg (get res)) res)›
lemma φR_get_res'_valid:
‹Valid_Proc φR_get_res'›
unfolding Valid_Proc_def φR_get_res'_def Return_def det_lift_def
by simp
lemma φR_get_res_transition:
‹ Transition_of' φR_get_res' ret = Id_on {s. s ∈ SPACE ∧ ret = Normal (φarg (get s))}›
unfolding Transition_of'_def φR_get_res'_def Return_def det_lift_def
by (cases ret; clarsimp simp add: set_eq_iff Id_on_iff; blast)
subsubsection ‹Setter›
definition φR_set_res :: ‹('T ⇒ 'T set) ⇒ unit proc›
where ‹φR_set_res F = (λres. if updts F res ⊆ SPACE
then Success (φarg ()) ` (updts F res)
else {Invalid})›
lemma setter_transition:
‹ Transition_of' (φR_set_res F) ret
≤ {(x,y). x ∈ SPACE ∧ get x ∈⇩S⇩H domain
∧ (if (∀h∈F (get x). h ∈⇩S⇩H domain)
then y ∈ updts F x ∧ ret = Normal φV_none
else y = x ∧ ret = Crash)}›
unfolding Transition_of'_def φR_set_res_def
apply (cases ret; auto simp add: set_eq_iff φV_none_def if_split_mem2)
using get_res_valid_raw apply fastforce
using get_res_valid_raw apply fastforce
apply (metis 𝗋_valid_split fun_upd_same fun_upd_upd)
using get_res_valid_raw by presburger
lemma setter_valid:
‹Valid_Proc (φR_set_res F)›
unfolding Valid_Proc_def φR_set_res_def bind_def Return_def det_lift_def
by (clarsimp split: option.split simp: subset_iff, blast)
end
subsection ‹Fiction Base›
φreasoner_group Resource_Space = (100, [0,9999]) ‹derived reasoning rules for Resource_Space›
locale basic_fiction =
R: resource Res
+ fiction_kind FIC.DOMAIN INTERPRET Fic ‹R.basic_fiction ⨾ I›
+ homo_one ‹I›
for Res :: "'T::sep_algebra resource_entry"
and I :: "('T, 'U::sep_algebra) φ"
and Fic :: "'U fiction_entry"
begin
subsubsection ‹φ-Type›
φtype_def φ :: ‹('U, 'x) φ ⇒ (fiction, 'x) φ›
where ‹φ T ≡ mk ⨾⇩f T›
deriving Sep_Functor_1
and Abstract_Domain⇩L
and ‹Gen_Br_Join φ φ φ P True›
lemma φ_unit:
‹(1 ⦂ φ Itself) = Void›
by (clarsimp simp add: BI_eq_iff)
paragraph ‹Short-cut of ToA›
φreasoner_group φ_ToA = (1100, [1100, 1120]) in ToA_cut
‹Short-cut transformations for fiction injector›
paragraph ‹Synthesis›
lemma [φreason %φsynthesis_parse for
‹Synthesis_Parse (φ ?T) (?Y::?'ret ⇒ assn)›
]:
‹Synthesis_Parse (φ T) (λ_. x ⦂ φ T :: assn)›
unfolding Synthesis_Parse_def ..
subsubsection ‹Fictional Refinement›
context begin
private lemma from_fictional_refinement':
‹ Valid_Proc f
⟹ (⋀v. Transition_of' f v 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 Rel v 𝗐.𝗋.𝗍 R.basic_fiction ⨾ I 𝗂𝗇 D)
⟹ Valid_Transition Rel
⟹ x ∈ D
⟹ 𝗉𝗋𝗈𝖼 f ⦃ x ⦂ φ Itself ⟼ λv. y ⦂ φ Itself 𝗌𝗎𝖻𝗃 y. (x,y) ∈ Rel (Normal v) ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. y ⦂ φ Itself 𝗌𝗎𝖻𝗃 y. (x,y) ∈ Rel (Abnm e))›
unfolding φProcedure_alt Fictional_Forward_Simulation_def atomize_all Valid_Transition_def
apply (auto simp add: Image_iff subset_iff Bex_def
INTERP_SPEC_subj INTERP_SPEC_ex INTERP_SPEC
Transition_of'_def less_eq_BI_iff
LooseState_def split_sum_all INTERP_RES_def interp_split R.𝗋_valid_split'
R.inj.sep_orthogonal inj.sep_orthogonal prj.homo_mult eval_stat_forall
split: eval_stat.split)
subgoal premises prems for r v y' u y rr
proof -
have t2: ‹∃xa. (∃ua v. xa = ua * v ∧ (∃xa. ua = R.mk xa ∧ xa ⊨ I (x * get r)) ∧ v ⊨ Itself u ∧ ua ## v) ∧
x ## get r ∧ x ∈ D ∧ Success v y' ∈ f xa ∧ R.clean xa ∈ R.SPACE ∧ (∃m. xa R.name = R.inject m ∧ m ∈⇩S⇩H R.domain)›
apply (rule exI[where x=‹(R.mk y * u)›], simp add: prems R.inj.homo_mult[symmetric] )
using prems(12) prems(13) by blast
note prems(4)[THEN spec[where x=v], THEN spec[where x=x], THEN spec[where x=‹get r›], THEN spec[where x=‹Itself u›], THEN spec[where x=‹y'›],
THEN mp, OF this]
then show ?thesis
apply clarsimp
subgoal for yy ya
apply (rule exI[where x=yy], clarsimp simp add: inj.homo_mult[symmetric] prems prj.homo_mult interp_split, rule)
apply (metis R.resource_kind_axioms Valid_Proc_def prems(1) prems(14) resource_kind.𝗋_valid_split t2 times_fupdt_1_apply_sep)
using prems(11) by blast .
qed
subgoal premises prems for r v y' u y rr
proof -
have t2: ‹∃xa. (∃ua v. xa = ua * v ∧ (∃xa. ua = R.mk xa ∧ xa ⊨ I (x * get r)) ∧ v ⊨ Itself u ∧ ua ## v) ∧
x ## get r ∧ x ∈ D ∧ Abnormal v y' ∈ f xa ∧ R.clean xa ∈ R.SPACE ∧ (∃m. xa R.name = R.inject m ∧ m ∈⇩S⇩H R.domain)›
by (metis (no_types, lifting) Itself_expn' R.inj.homo_mult mult_in_sep_homo_set prems(10) prems(12) prems(13) prems(14) prems(15) prems(16) prems(17) prems(3) prems(7) prems(8) sep_disj_get_name times_fupdt_1_apply_sep times_fupdt_1_fupdt_1_sep)
note prems(5)[THEN spec[where x=v], THEN spec[where x=x], THEN spec[where x=‹get r›], THEN spec[where x=‹Itself u›], THEN spec[where x=‹y'›],
THEN mp, OF this]
then show ?thesis
apply clarsimp
subgoal for yy ya
apply (rule exI[where x=yy], clarsimp simp add: inj.homo_mult[symmetric] prems prj.homo_mult interp_split, rule)
apply (metis R.𝗋_valid_split Valid_Proc_def prems(1) prems(14) t2 times_fupdt_1_apply_sep)
using prems(11) by blast .
qed
by (metis (no_types, lifting) R.inj.homo_mult mult_in_sep_homo_set sep_disj_get_name times_fupdt_1_apply_sep times_fupdt_1_fupdt_1_sep)
lemma from_fictional_refinement:
‹ Valid_Proc f
⟹ YY = (λv. y ⦂ φ Itself 𝗌𝗎𝖻𝗃 y. (x,y) ∈ Rel (Normal v))
⟹ EE = (λe. y ⦂ φ Itself 𝗌𝗎𝖻𝗃 y. (x,y) ∈ Rel (Abnm e))
⟹ (⋀v. Transition_of' f v 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 Rel v 𝗐.𝗋.𝗍 R.basic_fiction ⨾ I 𝗂𝗇 D)
⟹ Valid_Transition Rel
⟹ x ∈ D
⟹ 𝗉𝗋𝗈𝖼 f ⦃ x ⦂ φ Itself ⟼ YY ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 EE›
using from_fictional_refinement' by blast
end
lemma "__getter_rule__":
‹ Valid_Proc getter
⟹ (⋀ret. Transition_of' getter ret 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 Id_on (∃⇧sv. {x} 𝗌𝗎𝖻𝗃𝗌 ret = Normal (φarg v) ∧ P v) 𝗐.𝗋.𝗍 R.basic_fiction ⨾ I 𝗂𝗇 {x})
⟹ 𝗉𝗋𝗈𝖼 getter ⦃ x ⦂ φ Itself ⟼ λret. x ⦂ φ Itself 𝗌𝗎𝖻𝗃 v. ret = φarg v ∧ P v ⦄›
by (rule from_fictional_refinement[where Rel = ‹λret. Id_on (∃⇧sv. {x} 𝗌𝗎𝖻𝗃𝗌 ret = Normal (φarg v) ∧ P v)›
and D = ‹{x}›],
assumption,
clarsimp simp add: BI_eq_iff fun_eq_iff Id_on_iff,
simp add: Id_on_iff zero_set_def zero_fun_def,
assumption,
simp add: Valid_Transition_def zero_set_def,
simp)
lemma "__setter_rule__":
‹ Valid_Proc setter
⟹ (⋀ret. Transition_of' setter ret 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 {(x,y) |y. y ∈ Y} 𝗌𝗎𝖻𝗃𝗌 ret = Normal φV_none
𝗐.𝗋.𝗍 R.basic_fiction ⨾ I 𝗂𝗇 {x})
⟹ 𝗉𝗋𝗈𝖼 setter ⦃ x ⦂ φ Itself ⟼ λ_. y ⦂ φ Itself 𝗌𝗎𝖻𝗃 y. y ∈ Y ⦄›
by (rule from_fictional_refinement
[where Rel=‹λret. {(x,y) |y. y ∈ Y} 𝗌𝗎𝖻𝗃𝗌 ret = Normal φV_none› and D = ‹{x}›],
assumption,
clarsimp simp add: set_eq_iff Id_on_iff φarg_All fun_eq_iff φV_none_def,
simp add: Id_on_iff zero_set_def zero_fun_def,
assumption,
simp add: Valid_Transition_def zero_set_def,
simp)
lemma "__allocator_rule__":
‹ Valid_Proc allocator
⟹ (⋀ret. Transition_of' allocator ret 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 (∃⇧sk y. {(1,y)} 𝗌𝗎𝖻𝗃𝗌 ret = Normal (φarg k) ∧ y ∈ Y k ∧ P k)
𝗐.𝗋.𝗍 R.basic_fiction ⨾ I 𝗂𝗇 {1})
⟹ 𝗉𝗋𝗈𝖼 allocator ⦃ Void ⟼ λret. y ⦂ φ Itself 𝗌𝗎𝖻𝗃 k y. ret = φarg k ∧ y ∈ Y k ∧ P k ⦄›
by (rule from_fictional_refinement
[where Rel=‹λret. ∃⇧sk y. {(1,y)} 𝗌𝗎𝖻𝗃𝗌 ret = Normal (φarg k) ∧ y ∈ Y k ∧ P k›
and x=‹1› and D=‹{1}›, unfolded φ_unit],
assumption,
clarsimp simp add: set_eq_iff Id_on_iff φarg_All fun_eq_iff φV_none_def,
simp add: Id_on_iff zero_set_def zero_fun_def,
assumption,
simp add: Valid_Transition_def zero_set_def,
simp)
lemma "__allocator_rule__help_rewr":
‹ (∃⇧su'. {(1, u')} 𝗌𝗎𝖻𝗃𝗌 ret = Normal v ∧ u' ∈ U' v ∧ P v)
= ({(1, u') |u'. u' ∈ U' v} 𝗌𝗎𝖻𝗃𝗌 ret = Normal v ∧ P v) ›
unfolding set_eq_iff
by (simp, blast)
end
section ‹Non-separable Monolithic Resource›
locale discrete_mono_resource =
resource Res
for Res :: "'T discrete option resource_entry"
subsubsection ‹Interp Agreement›
section ‹Mapping Resources›
text ‹Resources based on mapping›
locale mapping_resource =
resource Res
for Res :: "('key ⇒ 'val::sep_algebra) resource_entry"
begin
definition
φR_allocate_res_entry :: ‹('key ⇒ bool)
⇒ ('key ⇒ 'val set)
⇒ 'key proc›
where ‹φR_allocate_res_entry P init =
φR_get_res' ⤜ (λres.
let k = (@k. φarg.dest res k = 1 ∧ P k)
in φR_set_res (λf. {f(k := x) |x. x ∈ init k})
⪢ Return (φarg k)
)›
lemma allocator_transition:
‹ (∀r. r ∈⇩S⇩H domain ⟶ (∃k. k ∉ dom1 r ∧ P k))
⟹ ∀k. P k ⟶ (∀x∈init k. 1(k := x) ∈⇩S⇩H domain)
⟹ Transition_of' (φR_allocate_res_entry P init) ret
≤ (∃⇧s k. Id_on SPACE * {(1, mk (1(k := x))) |x. x ∈ init k} 𝗌𝗎𝖻𝗃𝗌 ret = Normal (φarg k) ∧ P k)›
unfolding Transition_of'_def φR_allocate_res_entry_def φR_get_res'_def bind_def Return_def
det_lift_def φR_set_res_def Let_def
apply (cases ret; clarsimp simp add: zero_set_def set_eq_iff set_mult_expn Subjection_expn Id_on_iff)
apply (case_tac x; clarsimp simp add: zero_set_def set_eq_iff set_mult_expn Subjection_expn Id_on_iff)
subgoal premises prems for r b x
proof -
have t1: ‹get r ∈⇩S⇩H domain›
by (simp add: get_res_valid_raw prems(4))
let ?kk = ‹SOME k. get r k = 1 ∧ P k›
have t2: ‹∃k. get r k = 1 ∧ P k›
using dom1_def prems(1) t1 by fastforce
have t3[simp]: ‹get r ?kk = 1 ∧ P ?kk›
by (insert t2; clarify; rule someI[where P=‹λk. get r k = 1 ∧ P k›]; blast)
have t4 [simp]: ‹a ∈ init k ⟹ (get r)(?kk := a) = 1(?kk := a) * get r› for a k
by (simp add: fun_eq_iff)
have t5[simp]: ‹a ∈ init k ⟹ 1(?kk := a) ## get r› for a k
by (metis (mono_tags, lifting) fun_sep_disj_1_fupdt(2) fun_upd_triv sep_disj_commuteI sep_magma_1_left t3)
have t6[simp]: ‹P ?kk ⟹ a ∈ init ?kk ⟹ r(name := inject ((get r)(?kk := a))) ∈ SPACE› for a
by (metis (mono_tags, lifting) 𝗋_valid_split fun_sep_disj_1_fupdt(2) fun_split_1 fun_upd_same fun_upd_upd mult_in_sep_homo_set prems(2) prems(4) proj_inj sep_magma_1_left)
have t61[simp]: ‹P ?kk ⟹ a ∈ init ?kk ⟹ r(name := inject (1(?kk := a) * get r)) ∈ SPACE› for a
using t6 by auto
have t7: ‹∃a ∈ init ?kk. b = r(name := inject ((get r)(?kk := a)))› for a
using prems[simplified] t4 by (auto simp: if_distrib if_bool_eq_conj)
then obtain a where t8: ‹a ∈ init ?kk›
and [simp]: ‹b = r(name := inject ((get r)(?kk := a)))› by blast
show ?thesis
apply (simp add: fun_eq_iff inj.homo_mult prems)
by (smt (verit, ccfv_threshold) ‹⋀thesis. (⋀a. ⟦a ∈ init ?kk; b = r (name := inject ((get r)(SOME k. get r k = 1 ∧ P k := a)))⟧ ⟹ thesis) ⟹ thesis›
‹b = r(name := inject ((get r)(SOME k. get r k = 1 ∧ P k := a)))› fun_1upd_homo_left1 fun_sep_disj_1_fupdt(1)
fun_upd_apply fun_upd_triv inj.homo_mult inj.sep_disj_homo_semi inj_prj_in_SPACE one_fun prems(4) sep_disj_commuteI sep_mult_commute t4 t5)
qed
subgoal premises prems for r xa proof -
let ?kk = ‹SOME k. get r k = 1 ∧ P k›
have t1: ‹get r ∈⇩S⇩H domain›
by (simp add: get_res_valid_raw prems(6))
have t2: ‹∃k. get r k = 1 ∧ P k›
using dom1_def prems(1) t1 by fastforce
have t3[simp]: ‹get r ?kk = 1 ∧ P ?kk›
by (insert t2; clarify; rule someI[where P=‹λk. get r k = 1 ∧ P k›]; blast)
have t4 [simp]: ‹aa ∈ init ?kk ⟹ (get r)(?kk := aa) = 1(?kk := aa) * get r› for aa
by (simp add: fun_eq_iff)
have t5[simp]: ‹aa ∈ init ?kk ⟹ 1(?kk := aa) ## get r› for aa
by (metis (mono_tags, lifting) fun_sep_disj_1_fupdt(2) fun_upd_triv sep_disj_commuteI sep_magma_1_left t3)
have t7: ‹aa ∈ init ?kk ⟹ r(name := inject ((get r)(?kk := aa))) ∈ SPACE› for aa
by (smt (verit, del_insts) 𝗋_valid_split fun_upd_apply fun_upd_upd mult_in_sep_homo_set prems(2) prems(6) t1 t3 t4 t5)
show ?thesis
using prems(4) prems(5) t7 by blast
qed .
lemma allocator_refinement:
‹ ∀r. r ∈⇩S⇩H domain ⟶ (∃k. k ∉ dom1 r ∧ P k)
⟹ ∀k. P k ⟶ (∀a∈init k. 1(k := a) ∈⇩S⇩H domain)
⟹ Transition_of' (φR_allocate_res_entry P init) ret
𝗋𝖾𝖿𝗂𝗇𝖾𝗌 (∃⇧sk. {(1, 1(k := a)) |a. a ∈ init k} 𝗌𝗎𝖻𝗃𝗌 ret = Normal (φarg k) ∧ P k)
𝗐.𝗋.𝗍 basic_fiction 𝗂𝗇 {1}›
apply (rule refinement_sub_fun[OF allocator_transition], assumption, assumption)
unfolding Fictional_Forward_Simulation_def
apply (cases ret; clarsimp simp add: set_mult_expn mk_homo_mult)
subgoal premises prems for r R k u a
proof -
have [simp]: ‹1(k := a) ## r›
using prems(6) prems(8) sep_disj_commuteI sep_disj_multD1 by blast
show ?thesis
by (smt (verit, del_insts) ‹1(k := a) ## r› mk_homo_mult prems(5) prems(6) prems(8) prems(9)
sep_disj_commuteI sep_disj_multI1 sep_mult_assoc' sep_mult_commute)
qed .
lemma allocator_valid:
‹ ∀r. r ∈⇩S⇩H domain ⟶ (∃k. k ∉ dom1 r ∧ P k)
⟹ ∀k. P k ⟶ (∀a∈init k. 1(k := a) ∈⇩S⇩H domain)
⟹ Valid_Proc (φR_allocate_res_entry P init)›
unfolding Valid_Proc_def φR_allocate_res_entry_def φR_get_res'_def φR_set_res_def
bind_def Return_def det_lift_def Let_def
by (clarsimp split: option.split) blast
end
lemma refinement_ExBI_L:
‹ (⋀v. A 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 B v 𝗐.𝗋.𝗍 I 𝗂𝗇 D)
⟹ A 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 ExSet B 𝗐.𝗋.𝗍 I 𝗂𝗇 D›
unfolding Fictional_Forward_Simulation_def
by (clarsimp simp add: less_eq_BI_iff Image_def Bex_def Id_on_iff, blast)
locale fiction_base_for_mapping_resource =
R: mapping_resource Res
+ fiction_kind FIC.DOMAIN INTERPRET Fic ‹R.basic_fiction ⨾ I›
+ homo_one ‹I›
for Res :: "('key ⇒ 'val::sep_algebra) resource_entry"
and I :: "('key ⇒ 'val, 'T::sep_algebra) φ"
and Fic :: "'T fiction_entry"
begin
sublocale basic_fiction Res I Fic ..
lemma "__allocate_rule_2__":
‹ (⋀k. P k ⟹ {(1, 1(k := u)) |u. u∈U k} * Id_on UNIV 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 {(1, u') |u'. u' ∈ U' k} 𝗐.𝗋.𝗍 I 𝗂𝗇 {1})
⟹ ∀k. P k ⟶ (∀u∈U k. 1(k := u) ∈⇩S⇩H R.domain)
⟹ ∀r. r ∈⇩S⇩H R.domain ⟶ (∃k. k ∉ dom1 r ∧ P k)
⟹ 𝗉𝗋𝗈𝖼 R.φR_allocate_res_entry P U ⦃ Void ⟼ λret. u' ⦂ φ Itself 𝗌𝗎𝖻𝗃 k u'. ret = φarg k ∧ u' ∈ U' k ∧ P k ⦄ ›
by (rule "__allocator_rule__",
rule R.allocator_valid,
assumption,
assumption,
rule sep_refinement_stepwise[
OF R.allocator_refinement[THEN refinement_frame[where R=UNIV]]],
assumption,
assumption,
unfold ExSet_times_left SubjectionSet_times,
rule refinement_ExBI, subst "__allocator_rule__help_rewr",
rule refinement_subjection, blast,
auto simp add: set_mult_expn)
end
section ‹One Level Parital Mapping›
subsection ‹Preliminary›
definition ‹map_fun_at k g f = (λx. if x = k then g (f x) else f x)›
abbreviation ‹map_fun_atS k g h ≡ {h(k := v) |v. v ∈ g (h k)}›
lemma map_fun_at_1[simp]: ‹map_fun_at k g 1 = 1(k := g 1)›
unfolding map_fun_at_def fun_eq_iff by simp
lemma map_fun_at_const[simp]:
‹map_fun_at k (λ_. u) f = f(k := u)›
unfolding map_fun_at_def fun_eq_iff by simp
subsection ‹Resource›
locale partial_map_resource =
mapping_resource Res
for Res :: "('key ⇒ 'val::discrete_semigroup option) resource_entry"
and P :: ‹'key ⇒ 'val::discrete_semigroup set›
+ assumes domain0: ‹domain = sep_homo_set {h. finite (dom h) ∧ (∀k ∈ dom h. h k ∈ Some ` P k)}›
begin
subsubsection ‹Getter›
lemma in_invariant:
‹x ∈⇩S⇩H domain ⟷ x ∈ {h. finite (dom h) ∧ (∀k ∈ dom h. h k ∈ Some ` P k)}›
proof -
have ‹Sep_Homo {h. finite (dom h) ∧ (∀k∈dom h. h k ∈ Some ` P k)}›
proof -
have t2: ‹ {h. finite (dom h) ∧ (∀k∈dom h. h k ∈ Some ` P k)} = {h. finite (dom h)} ∩ {h. (∀k∈dom h. h k ∈ Some ` P k)} ›
by (auto simp add: set_eq_iff)
have t3: ‹(∀k∈dom h. P k) = (∀k. h k ≠ None ⟶ P k)› for h P
by auto
show ?thesis
by (subst t2, rule Sep_Homo_inter, simp, subst t3, rule Sep_Homo_pointwise, auto)
qed
then show ?thesis
by (simp add: domain0)
qed
definition φR_get_res_entry' :: ‹'key ⇒ 'val proc›
where ‹φR_get_res_entry' k =
φR_get_res' ⤜ (λres. case φarg.dest res k of Some v ⇒ Return (φarg v) | _ ⇒ (λ_. {Invalid}))›
lemma getter_transition:
‹ Transition_of' (φR_get_res_entry' k) ret
= Id_on {s. s ∈ SPACE ∧ ret = (case get s k of Some v ⇒ Normal (φarg v) | _ ⇒ Crash)}›
unfolding Transition_of'_def φR_get_res'_def φR_get_res_entry'_def bind_def Return_def det_lift_def
by (cases ret; clarsimp simp add: set_eq_iff Id_on_iff split: option.split; blast)
lemma getter_refinement:
‹Transition_of' (φR_get_res_entry' k) ret
𝗋𝖾𝖿𝗂𝗇𝖾𝗌 (∃⇧su. Id_on ({1(k ↦ u)} 𝗌𝗎𝖻𝗃𝗌 ret = Normal (φarg u) ∧ u ∈ P k ∧ u ∈ S))
𝗐.𝗋.𝗍 basic_fiction 𝗂𝗇 fun_upd 1 k ` Some ` S›
unfolding Fictional_Forward_Simulation_def getter_transition
apply (cases ret; clarsimp split: option.split simp add: set_mult_expn Id_on_iff
prj.homo_mult times_fun set_eq_iff 𝗋_valid_split'
inj.sep_orthogonal[simplified] in_invariant)
by (smt (verit, best) domIff fun_upd_same imageE mult_1_class.mult_1_right option.inject sep_disj_fun_discrete(1) sep_disj_partial_map_not_1_1 sep_mult_assoc times_fupdt_1_apply_sep times_option_not_none(2))
lemma getter_valid:
‹Valid_Proc (φR_get_res_entry' k)›
unfolding Valid_Proc_def φR_get_res_entry'_def φR_get_res'_def bind_def Return_def det_lift_def
by (clarsimp split: option.split)
subsubsection ‹Setter›
lemma setter_refinement:
‹(⋀v. v ∈ S ∧ v ∈ P k ⟹ ∀u∈F v. pred_option (λx. x ∈ P k) u)
⟹ Transition_of' (φR_set_res (map_fun_atS k (F o the))) ret
𝗋𝖾𝖿𝗂𝗇𝖾𝗌 (∃⇧s v. pairself (fun_upd 1 k) ` {(Some v, u) |u. u∈F v} 𝗌𝗎𝖻𝗃𝗌 ret = Normal φV_none ∧ v ∈ S ∧ v ∈ P k)
𝗐.𝗋.𝗍 basic_fiction
𝗂𝗇 fun_upd 1 k ` Some ` S›
apply (rule refinement_sub_fun[OF setter_transition[where F=‹map_fun_atS k (F o the)›]])
unfolding Fictional_Forward_Simulation_def
apply (clarsimp simp add: set_mult_expn
prj.homo_mult 𝗋_valid_split' inj.sep_orthogonal[simplified])
subgoal premises prems for r R x' v u
proof -
have x1: ‹1(k ↦ v) ## r› using prems(4) by blast
have x2: ‹(r * 1(k ↦ v)) ## get u›
using prems(2) prems(3) sep_mult_commute x1 by fastforce
have a1: ‹k ∈ dom ((1(k ↦ v) * r) * get u)›
by (simp add: domIff times_fun_def)
have a3: ‹(1(k ↦ v) * r) * get u ∈⇩S⇩H domain›
using prems(2) prems(3) by fastforce
then have ‹1(k ↦ v) ∈⇩S⇩H domain›
by (metis mult_in_sep_homo_set sep_mult_commute x1 x2)
then have a2: ‹v ∈ P k›
by (clarsimp simp add: in_invariant Ball_def times_fun)
have q3: ‹map_fun_atS k (F ∘ the) ((1(k ↦ v) * r) * get u) = {(1(k := aa) * r) * get u |aa. aa ∈ F v}›
apply (clarsimp simp add: fun_eq_iff map_fun_at_def times_fun set_eq_iff)
by (smt (z3) fun_upd_same mult_1_class.mult_1_right option.sel sep_disj_commuteI sep_disj_partial_map_some_none sep_mult_commute times_fupdt_1_apply_sep times_option_none x1 x2)
have q4: ‹aa ∈ F v ⟹ 1(k := aa) ∈⇩S⇩H domain› for aa
apply (clarsimp simp add: in_invariant)
using a2 prems(1) prems(5) by fastforce
have x3: ‹aa ∈ map_fun_atS k (F ∘ the) ((1(k ↦ v) * r) * get u) ⟹ aa ∈⇩S⇩H domain› for aa
unfolding q3
by (smt (verit, del_insts) a3 discrete_semigroup_sepdisj_fun mem_Collect_eq mult_in_sep_homo_set q4 sep_disj_multD2 sep_disj_multI1 sep_disj_multI2 sep_mult_commute x1 x2)
have x5: ‹1(k ↦ v) * r ## w ⟹
map_fun_atS k (F ∘ the) ((1(k ↦ v) * r) * w) = {((1(k := aa)) * r) * w |aa. aa ∈ F v}› for w
unfolding map_fun_at_def apply (clarsimp simp add: fun_eq_iff times_fun set_eq_iff)
by (smt (z3) mult_1_class.mult_1_right one_fun one_partial_map option.sel sep_disj_commuteI sep_disj_partial_map_not_1_1 times_fupdt_1_apply_sep times_option_not_none(2) x1)
show ?thesis
apply (insert prems, clarsimp simp add: x3 times_fun_upd x5 det_lift_def, simp add: mk_homo_mult)
subgoal premises prems for w aa
proof -
have x8: ‹aa ∈ F v›
by (metis (mono_tags, opaque_lifting) discrete_disj_1 fun_upd_same mult_1_class.mult_1_right one_option_def option.sel option.simps(3) prems(10) prems(12) sep_disj_fun_def times_fun_def x1)
have x4: ‹1(k := aa) ## r›
by (meson discrete_semigroup_sepdisj_fun x1)
have x4': ‹1(k := aa) ## w›
by (metis discrete_semigroup_sepdisj_fun prems(9) proj_inj sep_disj_commute sep_disj_multD2 x1 x2)
have x6: ‹(1(k := aa) * r) ## w›
by (meson discrete_semigroup_sepdisj_fun prems(12) sep_disj_multD2 sep_disj_multI1 sep_disj_multI2 x1)
have x6': ‹(1(k := aa) * w) ## r›
by (metis sep_disj_commute sep_disj_multI2 sep_mult_commute x4 x4' x6)
have x7: ‹mk w * clean u = u›
by (metis fun_split_1 prems(9))
show ?thesis
apply (insert prems, rule exI[where x=‹1(k := aa)›],
auto simp add: x4 x4' x6 x6' mk_homo_mult x8, rule exI[where x=u], clarsimp)
apply (smt (verit, ccfv_threshold) domIff fun_1upd_homo_left1 fun_sep_disj_1_fupdt(2) fun_upd_same fun_upd_upd mk_homo_mult mult_1_class.mult_1_right option.simps(3) sep_disj_mk sep_disj_partial_map_upd x4 x6 x7)
using a2 x8 by blast
qed .
qed .
end
subsection ‹Pointwise Base Fiction›
locale pointwise_base_fiction_for_partial_mapping_resource =
R: partial_map_resource Res RP
+ fiction_kind FIC.DOMAIN INTERPRET Fic ‹R.basic_fiction ⨾ ℱ_pointwise I›
+ homo_one ‹ℱ_pointwise I›
for Res :: "('key ⇒ 'val::discrete_semigroup option) resource_entry"
and I :: ‹'key ⇒ ('val option, 'fic::sep_algebra) φ›
and Fic :: "('key ⇒ 'fic) fiction_entry"
and RP :: ‹'key ⇒ 'val set›
begin
sublocale fiction_base_for_mapping_resource Res ‹ℱ_pointwise I› Fic ..
lemmas "__allocate_rule_3__" =
"__allocate_rule_2__"[
where U'=‹λk. {1(k:=u) |u. u∈U' k}› for U', simplified,
OF ℱ_pointwise_refinement[
where A=‹{(1,u) |u. u ∈ U}› and B=‹{(1,u') |u'. u' ∈ U'}› and D=‹{1}› for U U', simplified]]
lemma "_getter_rule_2_":
‹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 k' = k
⟹ refinement_projection (I k) {x} ⊆ Some ` S * UNIV
⟹ 𝗉𝗋𝗈𝖼 R.φR_get_res_entry' k ⦃ 1(k' := x) ⦂ φ Itself ⟼ λret. 1(k' := x) ⦂ φ Itself 𝗌𝗎𝖻𝗃 v. ret = φarg v ∧ v ∈ RP k' ∧ v ∈ S ⦄›
unfolding Premise_def
subgoal premises prems
proof -
have t1: ‹{Some u |u. u ∈ S} = Some ` S›
unfolding set_eq_iff by (clarsimp simp add: image_iff; blast)
show ?thesis
by (unfold prems(1),
insert prems(2-),
rule "__getter_rule__",
rule R.getter_valid,
rule sep_refinement_stepwise,
rule R.getter_refinement[where S=S, THEN refinement_frame[where R=UNIV]],
unfold SubjectionSet_Id_on SubjectionSet_times ExSet_Id_on ExSet_times_left,
rule refinement_existential[OF refinement_subjection[OF constant_refinement]],
simp,
rule ℱ_pointwise_projection[where D'=‹{x}› and D=‹Some ` S›, simplified],
assumption)
qed .
thm "__setter_rule__"
lemma "_setter_rule_2_":
‹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 k' = k
⟹ ((∃⇧sv. {(Some v, u) |u. u ∈ f v} 𝗌𝗎𝖻𝗃𝗌 v ∈ V ∧ v ∈ RP k) * Id_on UNIV 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 {(v', u') |u'. u' ∈ F v'} 𝗐.𝗋.𝗍 I k 𝗂𝗇 {v'})
⟹ refinement_projection (I k) {v'} ⊆ Some ` V * UNIV
⟹ (⋀v. v ∈ V ∧ v ∈ RP k ⟹ ∀u∈ f v. pred_option (λx. x ∈ RP k) u)
⟹ 𝗉𝗋𝗈𝖼 R.φR_set_res (map_fun_atS k (f o the))
⦃ 1(k' := v') ⦂ φ Itself ⟼ 1(k' := u') ⦂ φ Itself 𝗌𝗎𝖻𝗃 u'. u' ∈ F v' ⦄ ›
unfolding Premise_def
subgoal premises prems proof -
have t1: ‹(∃⇧sv. pairself (fun_upd 1 k) ` {(Some v, u) |u. u ∈ f v} 𝗌𝗎𝖻𝗃𝗌 ret = Normal φV_none ∧ v ∈ V ∧ v ∈ RP k) * Id_on UNIV
= ((pairself (fun_upd 1 k) ` (∃⇧sv. {(Some v, u) |u. u ∈ f v} 𝗌𝗎𝖻𝗃𝗌 v ∈ V ∧ v ∈ RP k )) * Id_on UNIV 𝗌𝗎𝖻𝗃𝗌 ret = Normal φV_none)›
for ret
by (unfold SubjectionSet_Id_on Subjection_times ExSet_Id_on ExBI_times_right ExSet_image
SubjectionSet_image; simp add: set_eq_iff; blast)
show ?thesis
by (unfold prems(1),
insert prems(2-),
rule "__setter_rule__"[where Y=‹{ 1(k:=u) |u. u ∈ F v' }›, simplified],
rule R.setter_valid,
rule sep_refinement_stepwise,
rule R.setter_refinement[THEN refinement_frame[where R=UNIV], unfolded Subjection_times],
assumption,
unfold t1,
rule refinement_subjection[OF ℱ_pointwise_refinement[where B=‹{(v', u) |u. u ∈ F v'}› and D=‹{v'}›, simplified]],
assumption,
simp,
rule ℱ_pointwise_projection[where D'=‹{v'}›, simplified],
assumption)
qed .
end
subsection ‹Pointwise Fiction›
lemma Itself_refinement':
‹{(u,v) |v. v ∈ V} * Id_on top 𝗋𝖾𝖿𝗂𝗇𝖾𝗌 {(u,v) |v. v ∈ V} 𝗐.𝗋.𝗍 Itself 𝗂𝗇 {u}›
for u :: ‹'a::{sep_cancel,sep_semigroup}›
unfolding Fictional_Forward_Simulation_def
by (clarsimp simp add: subset_iff set_mult_expn,
metis sep_cancel sep_disj_multD1 sep_disj_multD2 sep_disj_multI1 sep_disj_multI2 sep_mult_assoc)
locale pointwise_fiction_for_partial_mapping_resource =
R: partial_map_resource Res P
+ fiction_kind FIC.DOMAIN INTERPRET Fic ‹R.basic_fiction ⨾ ℱ_pointwise (λ_. Itself)›
+ homo_one ‹ℱ_pointwise (λ_::'key. Itself::'val discrete option ⇒ 'val discrete option BI)›
for Res :: "('key ⇒ 'val discrete option) resource_entry"
and P :: ‹'key ⇒ 'val discrete set›
and Fic :: "('key ⇒ 'val discrete option) fiction_entry"
begin
sublocale pointwise_base_fiction_for_partial_mapping_resource Res ‹λ_. Itself› Fic P ..
lemma setter_rule:
‹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 k' = k
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 v ∈ P k ⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (∀u∈U. pred_option (λx. x ∈ P k) u))
⟹ 𝗉𝗋𝗈𝖼 R.φR_set_res (map_fun_atS k (λ_. U)) ⦃ 1(k' ↦ v) ⦂ φ Itself ⟼ λ𝗋𝖾𝗍. 1(k' := u) ⦂ φ Itself 𝗌𝗎𝖻𝗃 u. u ∈ U ⦄ ›
unfolding Premise_def
subgoal premises prems
proof -
have [simp]: ‹(λ_. u) ∘ the = (λ_. u)› for u by auto
show ?thesis
by (unfold prems(1),
rule "_setter_rule_2_"[where k=k and k'=k and f=‹λ_. u› and F=‹λ_. u'› and V=‹{v}› for u u' v,
simplified, unfolded refinement_source_subjection,
OF impI,
OF Itself_refinement'
Itself_refinement_projection[where S=S and S'=S for S, simplified],
simplified],
simp add: prems)
qed .
lemma getter_rule:
‹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 k' = k
⟹ 𝗉𝗋𝗈𝖼 R.φR_get_res_entry' k ⦃
1(k' ↦ u) ⦂ φ Itself ⟼
λret. 1(k' ↦ u) ⦂ φ Itself 𝗌𝗎𝖻𝗃 ret = φarg u ∧ u ∈ P k'
⦄ ›
thm "_getter_rule_2_"[where S=‹{u}›, simplified singleton_iff, simplified]
by (rule "_getter_rule_2_"[where S=‹{u}› for u, simplified singleton_iff, simplified],
assumption,
rule Itself_refinement_projection,
simp)
lemmas allocate_rule = "__allocate_rule_2__"
[where U'=‹λk. {1(k:=u) |u. u∈U' k}› for U', simplified,
OF ℱ_pointwise_refinement[where I=‹λ_. Itself›, OF Itself_refinement', where u2=1, simplified]
Premise_D[where mode=default]
Premise_D[where mode=default]]
end
subsection ‹Pointwise Share Fiction›
lemma Ball_image_set:
‹(∀u∈{f u |u. u ∈ U}. P u) ⟷ (∀u∈U. P (f u))›
unfolding set_eq_iff
by auto
locale pointwise_share_fiction_for_partial_mapping_resource =
R: partial_map_resource Res P
+ fiction_kind FIC.DOMAIN INTERPRET Fic ‹R.basic_fiction ⨾ ℱ_pointwise (λ_. ℱ_functional to_share UNIV)›
+ homo_one ‹ℱ_pointwise (λ_. ℱ_functional to_share UNIV)
:: ('key ⇒ 'val discrete share option) ⇒ ('key ⇒ 'val discrete option) BI›
for Res :: "('key ⇒ 'val discrete option) resource_entry"
and Fic :: "('key ⇒ 'val discrete share option) fiction_entry"
and P :: ‹'key ⇒ 'val discrete set›
begin
sublocale pointwise_base_fiction_for_partial_mapping_resource Res ‹λ_. ℱ_functional to_share UNIV› Fic P ..
context notes mul_carrier_option_def[simp] option.pred_True[simp]
begin
lemma setter_rule:
‹ 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 k' = k
⟹ (𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 v ∈ P k ⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 (∀u∈U. pred_option (λx. x ∈ P k) u))
⟹ 𝗉𝗋𝗈𝖼 R.φR_set_res (map_fun_atS k (λx. U))
⦃ 1(k' ↦ Share 1 v) ⦂ φ Itself ⟼ λ𝗋𝖾𝗍. 1(k' := to_share u) ⦂ φ Itself 𝗌𝗎𝖻𝗃 u. u ∈ U ⦄ ›
by (rule "_setter_rule_2_"[where k=k and k'=k' and f=‹λ_. U› and F=‹λ_. u'› and V=‹{v}› for u' v,
simplified, unfolded refinement_source_subjection,
OF _ impI,
where u'3 = ‹{to_share u |u. u∈ u'4}› for u'4, simplified,
OF _ to_share.ℱ_functional_refinement'[where 'a=‹'val discrete›, simplified], simplified,
OF _ to_share.ℱ_functional_projection[where S=‹{Some v}›, simplified]],
simp,
simp add: Premise_def)
lemma getter_rule:
‹𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 k' = k
⟹ 𝗉𝗋𝗈𝖼 R.φR_get_res_entry' k
⦃ 1(k' := to_share (Some u)) ⦂ φ Itself ⟼
λret. 1(k' := to_share (Some u)) ⦂ φ Itself 𝗌𝗎𝖻𝗃 ret = φarg u ∧ u ∈ P k' ⦄ ›
by (rule "_getter_rule_2_"[where S=‹{u}› for u, simplified,
OF _ to_share.ℱ_functional_projection[where S=‹{x}› for x :: ‹'val discrete option›, simplified]],
assumption)
lemmas allocate_rule =
"__allocate_rule_2__"[where U'=‹λk. {1(k := to_share b) |b. b ∈ U k}› for U, simplified,
OF ℱ_pointwise_refinement[where I=‹λ_. ℱ_functional to_share UNIV›,
OF to_share.ℱ_functional_refinement'[where a=‹1::'val discrete option›, simplified],
simplified],
where U = ‹λk. {Some u |u. u∈U k}› for U,
simplified Ball_image_set, simplified]
end
end
end