Theory MMonad
section ‹State-Exception-Nondeterminism Monad with Access Reports›
theory MMonad
imports NEMonad Generic_Memory
begin
lemma fresh_freed_not_valid[simp]:
"is_FRESH s (addr.block a) ⟹ ¬is_valid_addr s a"
"is_FREED s (addr.block a) ⟹ ¬is_valid_addr s a"
"is_FRESH s (addr.block a) ⟹ ¬is_valid_ptr_addr s a"
"is_FREED s (addr.block a) ⟹ ¬is_valid_ptr_addr s a"
by (auto simp: is_valid_addr_def is_valid_ptr_addr_def split: addr.split)
text ‹We define this Monad directly over our memory model,
but still generic in the stored values.
The definition of the operations is done in two layers: first, we define the operations in the
ne-monad, prove that they preserve the consistency and non-emptiness invariant, and then
lift them to the subtype for the actual M-monad.
›
subsection ‹Invariant and Subtype›
text ‹
Our monad requires the following invariants, which will be enforced by a subtype
▸ the reported ACC_REPORT is consistent with the observable changes on the state.
This is a sanity check property, which also enables us to show commutativity of par.
▸ each program returns at least one possible result.
This is a sanity check property, which ensures that we don't accidentally verify a
'magic' program.
▸ the memory manager can choose any available addresses.
This is required to give it enough flexibility to always leave non-conflicting choices
for parallel composition.
›
definition "consistentM m ≡ ∀s. wlp (m s) (λ(_,i,s'). acc_consistent s i s')"
definition "consistentM_pw s m ≡ wlp m (λ(_,i,s'). acc_consistent s i s')"
definition "non_emptyM_pw s m ≡ ¬is_fail m ⟶
(∀B. finite B ⟶ (∃x i s'. is_res m (x,i,s') ∧ acc.a i ∩ B = {} ))"
definition "non_emptyM m ≡ ∀s. ¬is_fail (m s) ⟶
(∀B. finite B ⟶ (∃x i s'. is_res (m s) (x,i,s') ∧ acc.a i ∩ B = {} ))"
lemma non_emptyM_pw: "non_emptyM m = (∀s. non_emptyM_pw s (m s))"
unfolding non_emptyM_def non_emptyM_pw_def by simp
lemma consistentM_pw: "consistentM m ⟷ (∀s. consistentM_pw s (m s))"
unfolding consistentM_def consistentM_pw_def by auto
definition "invarM m ≡ consistentM m ∧ non_emptyM m"
definition "invarM_pw s m ≡ consistentM_pw s m ∧ non_emptyM_pw s m"
lemma invarM_pw: "invarM m = (∀s. invarM_pw s (m s))"
unfolding invarM_def invarM_pw_def
by (auto simp add: consistentM_pw non_emptyM_pw)
lemma "invarM c = (∀μ P. c μ = SPEC P ⟶
(∀x ρ μ'. P (x,ρ,μ') ⟶ acc_consistent μ ρ μ')
∧ (∀B. finite B ⟶ (∃x ρ μ'. P (x,ρ,μ') ∧ acc.a ρ ∩ B = {} ))
)"
unfolding invarM_def consistentM_def non_emptyM_def wlp_def
unfolding is_fail_def is_res_def
apply (safe;clarsimp)
apply (metis neM.sel neM.simps(3))
by (metis neM.collapse)
lemma
assumes "ρ=ACC_REPORT r w a f"
shows "acc_consistent μ ρ μ' ⟷ (
(∀addr∈r ∪ w. addr.block addr ∉ a ⟶ is_valid_addr μ addr) ∧
(∀addr∈r ∪ w. addr.block addr ∉ f ⟶ is_valid_addr μ' addr) ∧
(∀b. valid_block_trans μ μ' b) ∧
a = alloc_blocks μ μ' ∧
f = freed_blocks μ μ' ∧
(∀addr. is_valid_addr μ addr ∧ is_valid_addr μ' addr ∧ addr ∉ w ⟶ get_addr μ addr = get_addr μ' addr))"
unfolding acc_consistent_def valid_block_trans_def alloc_blocks_def freed_blocks_def assms
apply (clarsimp simp: is_ALLOC_conv)
apply (safe)
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply (smt (verit, best) UnI1 addr.case_eq_if block.disc(1) block.distinct(1) is_valid_addr_alt mem_Collect_eq)
subgoal by (simp add: addr.case_eq_if is_valid_addr_alt)
subgoal by (metis (no_types, lifting) UnI2 addr.case_eq_if block.disc(1) block.distinct(1) is_valid_addr_alt mem_Collect_eq)
subgoal by (simp add: addr.case_eq_if is_valid_addr_alt)
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
done
lemma
assumes "ρ=ACC_REPORT r w a f"
shows "acc_consistent μ ρ μ' ⟷ (
(∀addr∈r ∪ w. addr.block addr ∉ a ⟶ is_valid_addr μ addr) ∧
(∀addr∈r ∪ w. addr.block addr ∉ f ⟶ is_valid_addr μ' addr) ∧
(∀b. valid_block_trans μ μ' b) ∧
a = alloc_blocks μ μ' ∧
f = freed_blocks μ μ' ∧
(∀addr. is_valid_addr μ addr ∧ is_valid_addr μ' addr ∧ addr ∉ w ⟶ get_addr μ addr = get_addr μ' addr))"
unfolding acc_consistent_def valid_block_trans_def alloc_blocks_def freed_blocks_def assms
apply (clarsimp simp: is_ALLOC_conv)
apply (safe)
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply (smt (verit, best) UnI1 addr.case_eq_if block.disc(1) block.distinct(1) is_valid_addr_alt mem_Collect_eq)
subgoal by (simp add: addr.case_eq_if is_valid_addr_alt)
subgoal by (metis (no_types, lifting) UnI2 addr.case_eq_if block.disc(1) block.distinct(1) is_valid_addr_alt mem_Collect_eq)
subgoal by (simp add: addr.case_eq_if is_valid_addr_alt)
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
done
lemma consistentMI[intro?]:
assumes "⋀s. wlp (m s) (λ(_,i,s'). acc_consistent s i s')"
shows "consistentM m"
using assms unfolding consistentM_def ..
lemma consistentMD:
assumes "consistentM m"
shows "wlp (m s) (λ(_,i,s'). acc_consistent s i s')"
using assms unfolding consistentM_def ..
lemma consistent_wlp: "consistentM m ⟹ (⋀x i s'. acc_consistent s i s' ⟹ Q (x,i,s')) ⟹ (wlp (m s) Q)"
unfolding consistentM_def by pw
lemma invarM_pw_FAIL[simp]: "invarM_pw s FAIL"
unfolding invarM_pw_def consistentM_pw_def non_emptyM_pw_def
by pw
subsubsection ‹Subtype Definition›
typedef ('r,'v) M = "{m::'v memory ⇒ ('r×acc×'v memory) neM. invarM m}"
morphisms run Abs_M
unfolding invarM_def consistentM_def non_emptyM_def
by pw
setup_lifting type_definition_M
lemma invarM_run: "invarM (run m)"
using run by force
subsection ‹Basic Monad Combinators›
context
includes monad_syntax_ne
begin
qualified named_theorems invarM_lemmas ‹Monad invariant preservation lemmas›
declare invarM_def[invarM_lemmas]
definition "preturn x s = (return (x,0::acc,s))"
definition "pspec P s = (if P≠bot then SPEC (λ(r,i,s'). P r ∧ i=0 ∧ s'=s) else FAIL)"
definition "pbind m f s ≡ do {
(x,i⇩1,s) ← m s;
(r,i⇩2,s) ← f x s;
return (r,i⇩1+i⇩2 ::acc,s)
}"
lemma [invarM_lemmas]: "consistentM (preturn x)"
unfolding consistentM_def preturn_def
apply rule
apply wp
apply auto
unfolding acc_consistent_def
by (auto simp: )
lemma [invarM_lemmas]: "consistentM (pspec P)"
unfolding consistentM_def pspec_def
apply rule
apply wp
apply auto
unfolding acc_consistent_def
apply (auto simp: wlp_FAIL)
done
lemma [invarM_lemmas]: "consistentM m ⟹ (⋀x. consistentM (f x)) ⟹ consistentM (pbind m f)"
supply [wp_recursion_rule] = consistent_wlp
unfolding pbind_def
apply rule
apply wp
apply (clarsimp simp: acc_consistent_trans)
done
lemma [invarM_lemmas]: "non_emptyM (preturn x)"
unfolding non_emptyM_def preturn_def
by pw
lemma [invarM_lemmas]: "non_emptyM (pspec P)"
unfolding non_emptyM_def pspec_def
by pw
lemma [invarM_lemmas]: "non_emptyM m ⟹ (⋀x. non_emptyM (f x)) ⟹ non_emptyM (pbind m f)"
unfolding non_emptyM_def pbind_def
apply pw
by (metis inf_sup_distrib2 acc_plus_simps(3) sup.idem)
lift_definition Mreturn :: "'r ⇒ ('r,'v) M" is preturn by (simp add: invarM_lemmas)
lift_definition Mspec :: "('r⇒bool) ⇒ ('r,'v) M" is pspec by (simp add: invarM_lemmas)
lift_definition Mbind :: "('x,'v) M ⇒ ('x ⇒ ('r,'v) M) ⇒ ('r,'v) M"
is pbind by (auto simp add: invarM_lemmas intro!: invarM_pw[THEN iffD1])
subsection ‹Parallel Combinator›
definition "ppar m⇩1 m⇩2 s ≡ do {
((r⇩1,i⇩1,s⇩1),(r⇩2,i⇩2,s⇩2)) ← m⇩1 s ∥ m⇩2 s;
assert acc_consistent s i⇩1 s⇩1 ∧ acc_consistent s i⇩2 s⇩2;
assume spar_feasible i⇩1 i⇩2;
assert acc_norace i⇩1 i⇩2;
let s = combine_states s⇩1 i⇩2 s⇩2;
return ((r⇩1,r⇩2),i⇩1+i⇩2,s)
}"
lemma [invarM_lemmas]: "consistentM m⇩1 ⟹ consistentM m⇩2 ⟹ consistentM (ppar m⇩1 m⇩2)"
supply [wp_recursion_rule] = consistent_wlp
supply [wp_rule] = wlp_PAR[OF consistentMD consistentMD]
unfolding ppar_def
apply rule
apply wp
apply clarsimp
apply wp
apply simp_all
by (simp add: feasible_parallel_execution.consistent' feasible_parallel_execution.intro)
text ‹To show that our parallel combinator does not rule out all executions,
we need to exploit that, for any finite set of blocks, we always find an execution
that does not allocate this set of blocks.
›
lemma finite_alloc_blocks[simp, intro]: "finite (alloc_blocks s s')"
unfolding alloc_blocks_def
by (simp add: finite_non_fresh)
lemma [invarM_lemmas]: "⟦non_emptyM m⇩1; consistentM m⇩1; non_emptyM m⇩2; consistentM m⇩2 ⟧ ⟹ non_emptyM (ppar m⇩1 m⇩2)"
unfolding non_emptyM_def ppar_def
apply pw
proof goal_cases
case (1 s A)
obtain x⇩1 i⇩1 s⇩1 where R1: "is_res (m⇩1 s) (x⇩1, i⇩1, s⇩1)" and I1: "acc.a i⇩1 ∩ A = {}" using 1 by meson
hence "acc_consistent s i⇩1 s⇩1" using ‹consistentM m⇩1› ‹m⇩1 s ≠ FAIL›
unfolding consistentM_def wlp_def by pw
interpret c1: acc_consistent_loc s i⇩1 s⇩1 apply unfold_locales by fact
have "finite (alloc_blocks s s⇩1 ∪ A)" using 1 by auto
hence "finite (acc.a i⇩1 ∪ A)"
using c1.acc_a_alloc by presburger
then obtain x⇩2 i⇩2 s⇩2 where R2: "is_res (m⇩2 s) (x⇩2, i⇩2, s⇩2)" and I2: "acc.a i⇩2 ∩ (acc.a i⇩1 ∪ A) = {}"
using 1 by metis
hence NF2: "m⇩2 s ≠ FAIL" using 1 by metis
with R2 have "acc_consistent s i⇩2 s⇩2" using ‹consistentM m⇩2›
unfolding consistentM_def wlp_def by pw
interpret c2: acc_consistent_loc s i⇩2 s⇩2 apply unfold_locales by fact
from I2 have "spar_feasible i⇩1 i⇩2"
unfolding spar_feasible_def by (auto simp: c1.acc_a_alloc c2.acc_a_alloc)
with I1 I2 R1 R2 NF2 have NI: "acc_norace i⇩1 i⇩2" using 1
by metis
interpret valid_parallel_execution s s⇩1 i⇩1 s⇩2 i⇩2 apply unfold_locales by fact+
show ?case
apply (rule exI[where x=x⇩1])
apply (rule exI[where x=x⇩2])
apply (rule exI[where x="i⇩1+i⇩2"])
apply (rule conjI)
subgoal
apply (intro exI conjI impI)
apply fact
apply fact
apply (rule NI)
apply fact
apply fact
apply (rule NI)
apply fact
apply fact
apply simp
apply simp
apply simp
done
subgoal using I1 I2 by auto
done
qed
lift_definition Mpar :: "('x,'v) M ⇒ (('y,'v) M) ⇒ ('x×'y,'v) M"
is ppar by (simp add: invarM_lemmas)
subsection ‹Memory Operations›
definition "malloc vs s = do {
b ← spec b. is_FRESH s b;
return (b, acc_a b, addr_alloc vs b s)
}"
definition "mfree b s = do {
assert is_ALLOC s b;
return ((), acc_f b, addr_free b s)
}"
definition "mvalid_addr a s = do {
assert is_valid_addr s a;
return ((), acc_r a, s)
}"
definition "mload a s = do {
assert is_valid_addr s a;
return (get_addr s a, acc_r a, s)
}"
definition "mstore a v s = do {
assert is_valid_addr s a;
return ((), acc_w a, put_addr s a v)
}"
lemma [invarM_lemmas]: "consistentM (malloc v)"
unfolding consistentM_def malloc_def
apply rule
apply wp
apply (auto simp: acc_consistent_def alloc_blocks_def freed_blocks_def)
done
lemma [invarM_lemmas]: "consistentM (mfree a)"
unfolding consistentM_def mfree_def
apply rule
apply wp
apply auto
unfolding acc_consistent_def alloc_blocks_def freed_blocks_def
by (auto)
lemma [invarM_lemmas]: "consistentM (mvalid_addr a)"
unfolding consistentM_def mvalid_addr_def
apply rule
apply wp
apply auto
unfolding acc_consistent_def
by (auto)
lemma [invarM_lemmas]: "consistentM (mload a)"
unfolding consistentM_def mload_def
apply rule
apply wp
apply auto
unfolding acc_consistent_def
by (auto simp: )
lemma [invarM_lemmas]: "consistentM (mstore a v)"
unfolding consistentM_def mstore_def
apply rule
apply wp
apply auto
unfolding acc_consistent_def alloc_blocks_def freed_blocks_def
by (auto split: block.split)
lemma [invarM_lemmas]: "non_emptyM (malloc v)"
unfolding non_emptyM_def malloc_def alloc_blocks_def
apply pw
using ex_fresh by fastforce
lemma [invarM_lemmas]: "non_emptyM (mfree a)"
unfolding non_emptyM_def mfree_def alloc_blocks_def
by pw
lemma [invarM_lemmas]: "non_emptyM (mvalid_addr a)"
unfolding non_emptyM_def mvalid_addr_def alloc_blocks_def
by pw
lemma [invarM_lemmas]: "non_emptyM (mload a)"
unfolding non_emptyM_def mload_def
by pw
lemma [invarM_lemmas]: "non_emptyM (mstore a v)"
unfolding non_emptyM_def mstore_def alloc_blocks_def
by pw
lift_definition Mmalloc :: "('v list) ⇒ (block_idx,'v) M" is malloc by (simp add: invarM_lemmas)
lift_definition Mfree :: "block_idx ⇒ (unit,'v) M" is mfree by (simp add: invarM_lemmas)
lift_definition Mvalid_addr :: "addr ⇒ (unit,'v) M" is mvalid_addr by (simp add: invarM_lemmas)
lift_definition Mload :: "addr ⇒ ('v,'v) M" is mload by (simp add: invarM_lemmas)
lift_definition Mstore :: "addr ⇒ 'v ⇒ (unit,'v) M" is mstore by (simp add: invarM_lemmas)
end
subsection ‹Pointwise Reasoning Setup›
lemma M_eq_iff[pw_init]: "m=m' ⟷ (∀s. run m s = run m' s)"
apply transfer
by auto
lemma pw_Mreturn[pw_simp]:
"run (Mreturn x) s ≠ FAIL"
"is_res (run (Mreturn x) s) r ⟷ r=(x,0,s)"
by (transfer'; unfold preturn_def; pw)+
lemma pw_Mspec[pw_simp]:
"run (Mspec P) s = FAIL ⟷ P=bot"
"is_res (run (Mspec P) s) r ⟷ (∃x. r=(x,0,s) ∧ P x)"
by (transfer'; unfold pspec_def; pw)+
lemma pw_Mbind1[pw_simp]:
"run (Mbind m f) s = FAIL ⟷ is_fail (run m s) ∨ (∃x i s'. is_res (run m s) (x,i,s') ∧ is_fail (run (f x) s'))"
apply transfer
unfolding pbind_def
by pw
lemma pw_Mbind2[pw_simp]:
"is_res (run (Mbind m f) s) ris ⟷ (case ris of (r,i'',s'')
⇒ (∀x i s'. is_res (run m s) (x,i,s') ⟶ ¬is_fail (run (f x) s'))
∧ (∃x i i' s'. is_res (run m s) (x,i,s') ∧ is_res (run (f x) s') (r,i',s'') ∧ i''=i+i')
)"
apply transfer
unfolding pbind_def
apply pw
by blast
lemma invarM_pw_iff: "invarM m ⟷ (∀s.
(∀r i s'. is_res (m s) (r,i,s') ⟶ acc_consistent s i s')
∧ non_emptyM_pw s (m s)
)"
unfolding invarM_def consistentM_def non_emptyM_pw
apply pw
by (metis is_res_def)
lemma pw_Mpar1[pw_simp]:
"run (Mpar m⇩1 m⇩2) s = FAIL ⟷ (is_fail (run m⇩1 s) ∨ is_fail (run m⇩2 s)
∨ (∃r⇩1 i⇩1 s⇩1 r⇩2 i⇩2 s⇩2. is_res (run m⇩1 s) (r⇩1,i⇩1,s⇩1) ∧ is_res (run m⇩2 s) (r⇩2,i⇩2,s⇩2)
∧ spar_feasible i⇩1 i⇩2 ∧ ¬acc_norace i⇩1 i⇩2 ))"
apply transfer
unfolding ppar_def invarM_pw_iff
apply pw
by blast+
lemma pw_Mpar2[pw_simp]:
"is_res (run (Mpar m⇩1 m⇩2) s) ris ⟷ (case ris of (r,i,s') ⇒
(∀r⇩1 i⇩1 s⇩1 r⇩2 i⇩2 s⇩2. is_res (run m⇩1 s) (r⇩1,i⇩1,s⇩1) ∧ is_res (run m⇩2 s) (r⇩2,i⇩2,s⇩2) ∧ spar_feasible i⇩1 i⇩2
⟶ acc_norace i⇩1 i⇩2)
∧ (∃r⇩1 i⇩1 s⇩1 r⇩2 i⇩2 s⇩2. is_res (run m⇩1 s) (r⇩1,i⇩1,s⇩1) ∧ is_res (run m⇩2 s) (r⇩2,i⇩2,s⇩2)
∧ spar_feasible i⇩1 i⇩2 ∧ r=(r⇩1,r⇩2) ∧ i=i⇩1+i⇩2 ∧ s' = combine_states s⇩1 i⇩2 s⇩2 ))"
apply transfer
unfolding ppar_def invarM_pw_iff
apply pw
apply blast+
done
lemma no_result_is_FAIL[pw_simp]: "(∀a b c. ¬is_res (run m s) (a,b,c)) ⟷ run m s = FAIL"
by (metis finite.emptyI invarM_pw_iff invarM_run is_fail_def is_res_def non_emptyM_pw_def)
context
includes monad_syntax_ne
begin
lemma run_Mmalloc[pw_simp]: "run (Mmalloc vs) s = malloc vs s"
apply transfer ..
lemma run_Mfree[pw_simp]: "run (Mfree a) s = mfree a s"
apply transfer ..
lemma run_Mvalid_addr[pw_simp]: "run (Mvalid_addr a) s = mvalid_addr a s"
apply transfer ..
lemma run_Mload[pw_simp]: "run (Mload a) s = mload a s"
apply transfer ..
lemma run_Mstore[pw_simp]: "run (Mstore a v) s = mstore a v s"
apply transfer ..
end
subsection ‹Recursion Setup›
lift_definition Mbot :: "('r,'v) M" is "λ_. FAIL"
by (auto simp: invarM_pw)
context
begin
interpretation FR: flat_rec FAIL .
lift_definition Mle :: "('r,'v) M ⇒ ('r,'v) M ⇒ bool"
is "fun_ord FR.le" .
definition "fun_chain ≡ Complete_Partial_Order.chain (fun_ord FR.le)"
definition "fun_chain' ≡ Complete_Partial_Order.chain Mle"
lemma [transfer_rule]: "(rel_fun (rel_set cr_M) (=)) fun_chain fun_chain'"
unfolding fun_chain_def fun_chain'_def Complete_Partial_Order.chain_def
apply (auto simp: rel_fun_def fun_ord_def rel_set_def)
apply (metis (full_types) Mle.rep_eq cr_M_def fun_ord_def)
by (metis (no_types, lifting) Mle.rep_eq cr_M_def fun_ord_def)
lift_definition Mlub :: "('r,'v) M set ⇒ ('r,'v) M"
is "λC. if fun_chain C then fun_lub FR.lub C else (λ_. FAIL)"
unfolding invarM_pw
apply rule
subgoal for C s
apply (auto simp: FR.fun_lub_apply fun_chain_def)
apply (drule FR.chain_apply[where x=s])
apply (erule FR.chain_cases)
apply auto
by force
done
lemma Mlub_empty_is_fail[pw_simp]: "run (Mlub {}) s = FAIL"
apply transfer
by (auto simp: fun_lub_def)
lemma M_ccpo: "class.ccpo Mlub Mle (mk_lt Mle)"
apply intro_locales
apply (rule preorder_mk_ltI)
apply unfold_locales
apply transfer apply (auto simp: fun_ord_def FR.le_def) []
apply transfer apply (fastforce simp: fun_ord_def FR.le_def) []
apply transfer apply (auto simp: fun_ord_def FR.le_def fun_eq_iff; metis) []
apply (fold fun_chain'_def)
apply transfer
apply (clarsimp simp: fun_ord_def FR.fun_lub_apply fun_chain_def)
subgoal for C f s
apply (drule FR.chain_apply[where x=s])
apply (erule FR.chain_cases)
apply (auto simp: FR.le_def)
done
apply transfer
apply (clarsimp simp: fun_ord_def FR.fun_lub_apply fun_chain_def)
subgoal for C f s
apply (drule FR.chain_apply[where x=s])
apply (erule FR.chain_cases)
apply (auto simp: FR.le_def)
apply force
apply force
done
done
interpretation RS: ccpo Mlub Mle "mk_lt Mle"
by (rule M_ccpo)
interpretation RS: rec_setup Mlub Mle "mk_lt Mle"
by unfold_locales
definition "REC ≡ RS.REC"
abbreviation "M_mono' ≡ gen_is_mono' Mle Mle"
abbreviation "M_mono_body ≡ RS.is_mono_body"
lemma REC_unfold:
assumes MONO: "RS.is_mono_body F"
shows "REC F = F (REC F)"
by (metis REC_def RS.REC_unfold assms)
text ‹Pointwise properties of recursive functions can be proved by well-founded induction
on the arguments.›
lemma REC_wf_induct:
assumes WF: "wf V"
assumes MONO: "RS.is_mono_body F"
assumes STEP: "⋀x D. ⟦⋀y. ⟦(y,x)∈V⟧ ⟹ P y (D y) ⟧ ⟹ P x (F D x)"
shows "P x (REC F x)"
using assms unfolding REC_def
using RS.REC_wf_induct by metis
text ‹For pointwise properties, which hold at non-terminating arguments, we
can use the following induction scheme, which does not require a well-founded ordering.›
lemma REC_pointwise_induct:
fixes P
assumes BOT: "⋀x s. P x s FAIL"
assumes STEP: "⋀D x s. (⋀y s. P y s (run (D y) s)) ⟹ P x s (run (F D x) s)"
shows "P x s (run (REC F x) s)"
proof -
have "∀s. P x s (run (REC F x) s)"
unfolding REC_def
supply R = RS.REC_pointwise_induct[where P="λx m. ∀s. P x s (run m s)"]
apply (rule R)
subgoal for x
apply (transfer fixing: P)
apply (auto simp: fun_chain_def chain_empty fun_lub_def BOT)
done
subgoal for x
unfolding ccpo.admissible_def fun_chain'_def[symmetric]
apply (transfer fixing: P)
apply (clarsimp simp: FR.fun_lub_apply)
subgoal for x C s
unfolding fun_chain_def
apply (drule FR.chain_apply[where x=s])
apply (erule FR.chain_cases)
apply (auto simp: FR.le_def BOT)
by force
done
subgoal using STEP by blast
done
thus ?thesis ..
qed
subsubsection ‹Monotonicity Prover Setup›
qualified lemma Mle_alt: "Mle a b ⟷ (∀s. FR.le (run a s) (run b s))"
apply transfer
by (auto simp: fun_ord_def)
qualified lemma pw_FR_le: "FR.le a b ⟷ a=b ∨ is_fail a"
unfolding FR.le_def is_fail_def by auto
context
notes [pw_init] = Mle_alt pw_FR_le
begin
lemma mono_Mbind1: "
M_mono' (λD. F D) ⟹
M_mono' (λD. Mbind (F D) (G))"
unfolding monotone_def fun_ord_def Mle_alt
apply pw'
apply (safe; simp; blast)
done
lemma mono_Mbind2: "
(⋀y. M_mono' (λD. G y D)) ⟹
M_mono' (λD. Mbind F (λy. G y D))"
unfolding monotone_def fun_ord_def Mle_alt
apply pw
apply blast
apply metis
apply blast
apply blast
done
lemma mono_Mbind[partial_function_mono]:
assumes "M_mono' (λD. F D)"
assumes "⋀y. M_mono' (λD. G y D)"
shows "M_mono' (λD. Mbind (F D) (λy. G y D))"
using mono_Mbind1[OF assms(1)] mono_Mbind2[of G, OF assms(2)]
unfolding monotone_def
apply auto
using RS.order.trans by blast
lemma mono_Mpar1: "
M_mono' (λD. F D) ⟹
M_mono' (λD. Mpar (F D) G)"
unfolding monotone_def fun_ord_def Mle_alt
apply pw'
apply (safe; simp; blast)
done
lemma mono_Mpar2: "
M_mono' (λD. G D) ⟹
M_mono' (λD. Mpar F (G D))"
unfolding monotone_def fun_ord_def Mle_alt
apply pw'
apply (safe; simp; blast)
done
lemma mono_Mpar[partial_function_mono]: "
M_mono' (λD. F D) ⟹
M_mono' (λD. G D) ⟹
M_mono' (λD. Mpar (F D) (G D))"
using mono_Mpar1 mono_Mpar2
unfolding monotone_def
apply auto
using RS.order.trans by blast
lemma mono_REC[partial_function_mono]:
assumes "⋀D. RS.is_mono_body (F D)"
assumes "⋀DD x. M_mono' (λD. F D DD x)"
shows "M_mono' (λD. REC (F D) x)"
using assms
unfolding monotone_def REC_def
apply clarsimp
subgoal for D D'
apply (rule RS.REC_mono[of F D D', unfolded fun_ord_def, rule_format])
subgoal by (simp add: fun_ord_def monotone_def)
subgoal by blast
done
done
end
subsection ‹Partial Function Setup›
lemmas M_partial_function = RS.partial_function_definitions
end
interpretation RSPF: partial_function_definitions Mle Mlub
by (rule M_partial_function)
declaration ‹Partial_Function.init "M" @{term RSPF.fixp_fun}
@{term RSPF.mono_body} @{thm RSPF.fixp_rule_uc} @{thm RSPF.fixp_induct_uc}
(NONE)›
subsection ‹Symmetry of parallel›
definition "mswap m ≡ do⇩n⇩e { ((r⇩1,r⇩2),i,s)←m; return⇩n⇩e ((r⇩2,r⇩1),i,s) }"
lemma pw_mswap[pw_simp]:
"mswap m = FAIL ⟷ is_fail m"
"is_res (mswap m) ab ⟷ (case ab of ((r⇩1,r⇩2),i,s) ⇒ is_res m ((r⇩2,r⇩1),i,s))"
unfolding mswap_def
apply pw
by (cases ab; pw)
lemmas combine_states_sym = valid_parallel_execution.combine_states_sym[OF valid_parallel_execution.intro]
lemma ppar_sym: "invarM m⇩1 ⟹ invarM m⇩2 ⟹ ppar m⇩1 m⇩2 s = mswap (ppar m⇩2 m⇩1 s)"
unfolding ppar_def
apply (cases "m⇩1 s"; cases "m⇩2 s"; simp)
defer
apply pw
apply pw
apply pw
subgoal for P⇩1 P⇩2
apply (subgoal_tac "invarM_pw s (SPEC P⇩1)")
apply (subgoal_tac "invarM_pw s (SPEC P⇩2)")
apply (thin_tac "invarM _")+
apply (thin_tac "_=_")+
subgoal
apply pw
using spar_feasible_sym acc_norace_sym
apply -
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply (smt (verit, best) add.commute combine_states_sym acc_consistent_loc.intro)
apply blast
by (smt (verit, best) add.commute combine_states_sym acc_consistent_loc.intro)
apply (metis invarM_pw)
apply (metis invarM_pw)
done
done
lemma res_run_consistentI: "is_res (run m s) (x,i,s') ⟹ acc_consistent s i s'"
using invarM_pw_iff invarM_run by fastforce
lemma Mpar_sym: "Mpar m⇩1 m⇩2 = Mbind (Mpar m⇩2 m⇩1) (λ(r⇩1,r⇩2). Mreturn (r⇩2,r⇩1))"
apply pw
using spar_feasible_sym acc_norace_sym apply blast
using spar_feasible_sym acc_norace_sym apply blast
using spar_feasible_sym acc_norace_sym apply blast
apply (metis (no_types, opaque_lifting) add.commute combine_states_sym spar_feasible_sym res_run_consistentI)
using spar_feasible_sym acc_norace_sym apply blast
apply (metis (no_types, opaque_lifting) add.commute combine_states_sym spar_feasible_sym res_run_consistentI)
done
lifting_update M.lifting
lifting_forget M.lifting
subsection ‹Syntax›
abbreviation then_doM where "then_doM m f ≡ Mbind m (λ_. f)"
nonterminal doM_binds and doM_bind
syntax
"_doM_block" :: "doM_binds ⇒ 'a" ("do⇩M {//(2 _)//}" [12] 62)
"_doM_bind" :: "[pttrn, 'a] ⇒ doM_bind" ("(2_ ←/ _)" 13)
"_doM_let" :: "[pttrn, 'a] ⇒ doM_bind" ("(2let _ =/ _)" [1000, 13] 13)
"_doM_then" :: "'a ⇒ doM_bind" ("_" [14] 13)
"_doM_final" :: "'a ⇒ doM_binds" ("_")
"_doM_cons" :: "[doM_bind, doM_binds] ⇒ doM_binds" ("_;//_" [13, 12] 12)
syntax (ASCII)
"_doM_block" :: "doM_binds ⇒ 'a" ("doM {//(2 _)//}" [12] 62)
"_doM_bind" :: "[pttrn, 'a] ⇒ doM_bind" ("(2_ <-/ _)" 13)
translations
"_doM_block (_doM_cons (_doM_then t) (_doM_final e))"
⇌ "CONST then_doM t e"
"_doM_block (_doM_cons (_doM_bind p t) (_doM_final e))"
⇌ "CONST Mbind t (λp. e)"
"_doM_block (_doM_cons (_doM_let p t) bs)"
⇌ "let p = t in _doM_block bs"
"_doM_block (_doM_cons b (_doM_cons c cs))"
⇌ "_doM_block (_doM_cons b (_doM_final (_doM_block (_doM_cons c cs))))"
"_doM_cons (_doM_let p t) (_doM_final s)"
⇌ "_doM_final (let p = t in s)"
"_doM_block (_doM_final e)" ⇀ "e"
"(CONST then_doM m n)" ⇀ "(CONST Mbind m (λ_. n))"
notation Mreturn ("return⇩M _" 20)
notation Mspec (binder "spec⇩M " 10)
notation Mpar (infixr "∥⇩M" 50)
subsection ‹Monad Laws›
lemma M_monad_laws[simp]:
"doM {x←return⇩M a; f x} = f a"
"doM {x←m; return⇩M x} = m"
"doM {y←doM {x←m; f x}; g y} = doM { x←m; y←f x; g y }"
apply pw
apply pw
apply pw
apply blast
apply blast
using group_cancel.add1 apply blast
by (metis (no_types, opaque_lifting) add.assoc)
subsubsection ‹Additional simp lemmas›
lemma Mreturn_inj[simp]: "(return⇩M a) = (return⇩M b) ⟷ a=b"
by pw
subsection ‹Derived Constructs›
subsubsection ‹Fail›
text ‹We define fail via least upper bound of the empty set, and show that it behaves as expected›
definition Mfail ("fail⇩M") where "Mfail ≡ Mlub {}"
lemma run_Mfail[pw_simp]: "run Mfail s = FAIL"
unfolding Mfail_def
by pw
lemma M_bind_fail[simp]:
"doM {m; fail⇩M} = fail⇩M"
"doM {fail⇩M; m} = fail⇩M"
by pw+
lemma M_par_fail[simp]:
"(fail⇩M ∥⇩M m⇩2) = fail⇩M"
"(m⇩1 ∥⇩M fail⇩M) = fail⇩M"
by pw+
subsubsection ‹Assert›
definition Massert ("assert⇩m _" 20) where "Massert P ≡ if P then Mreturn () else Mfail"
lemma run_assert[pw_simp]: "run (Massert P) s = do⇩n⇩e {assert⇩n⇩e P; return⇩n⇩e ((),0,s)}"
unfolding Massert_def by pw
lemma assert_True[simp]: "Massert True = Mreturn ()" by pw
subsubsection ‹While›
definition "Mwhile b c ≡ REC (λwhile s. doM {
bb ← b s;
if bb then doM {
s ← c s;
while s
} else return⇩M s
})"
lemma Mwhile_unfold: "Mwhile b c s = doM {
bb ← b s;
if bb then doM {
s ← c s;
Mwhile b c s
} else return⇩M s
}"
unfolding Mwhile_def
apply (subst REC_unfold)
apply pf_mono_prover
..
lemma Mwhile_mono[partial_function_mono]:
assumes "⋀x. M_mono' (λf. b f x)"
assumes "⋀x. M_mono' (λf. c f x)"
shows "M_mono' (λD. Mwhile (b D) (c D) σ)"
unfolding Mwhile_def
using assms by pf_mono_prover
subsection ‹Syntax Bundle›
bundle monad_syntax_M
begin
syntax
"_doM_block" :: "doM_binds ⇒ 'a" ("do {//(2 _)//}" [12] 62)
notation Mfail ("fail")
notation Mreturn ("return _" 20)
notation Mspec (binder "spec " 10)
notation Massert ("assert _" 20)
notation Mpar (infixr "∥" 50)
end
end