Theory Abbrevs
theory Abbrevs
imports PIMP SyntaxTweaks
begin
text ‹now we can use dots as a term›
consts dots::"'a" (‹…›)
lemma conj_to_impl: "(P ∧ Q ⟶ R) = (P ⟶ Q ⟶ R)"
by auto
notation (in xvalid_program) (latex output)
barrier_inv (‹flush'_inv›)
abbreviation
"acquire sb owns ≡ acquired True sb owns"
notation (latex output)
direct_memop_step (‹_ \<^latex>‹$\overset{\isa{v}_\isa{d}}{\rightarrow}_{\isa{m}}$› _› [60,60] 100)
notation (latex output)
virtual_memop_step (‹_ \<^latex>‹$\overset{\isa{v}}{\rightarrow}_{\isa{m}}$› _› [60,60] 100)
context program
begin
term "(ts, m) ⇒⇩s⇩b (ts',m')"
notation (latex output) store_buffer.concurrent_step (‹_ \<^latex>‹$\overset{\isa{sb}}{\Rightarrow}$› _› [60,60] 100)
notation (latex output) virtual.concurrent_step (‹_ \<^latex>‹$\overset{\isa{v}}{\Rightarrow}$› _› [60,60] 100)
thm store_buffer.concurrent_step.Program
end
abbreviation (output)
"sbh_global_step ≡ computation.concurrent_step sbh_memop_step flush_step stmt_step (λp p' is sb. sb @ [Prog⇩s⇩b p p' is])"
notation (latex output)
sbh_global_step (‹_ \<^latex>‹$\overset{\isa{sbh}}{\Rightarrow}$› _› [60,60] 100)
notation (latex output)
direct_pimp_step (‹_ \<^latex>‹$\overset{\isa{v}}{\Rightarrow}$› _› [60,60] 100)
notation (latex output)
sbh_memop_step (‹_ \<^latex>‹$\overset{\isa{sbh}}{\rightarrow}_{\isa{m}}$› _› [60,60] 100)
notation (latex output)
sb_memop_step (‹_ \<^latex>‹$\overset{\isa{sb}}{\rightarrow}_{\isa{m}}$› _› [60,60] 100)
notation (output)
sim_direct_config (‹_ ∼ _ › [60,60] 100)
notation (output)
flush_step (‹_ →⇩s⇩b⇩h _› [60,60] 100)
notation (output)
store_buffer_step (‹_ →⇩s⇩b _› [60,60] 100)
notation (output)
outstanding_refs (‹refs›)
notation (output)
is_volatile_Write⇩s⇩b (‹volatile'_Write›)
abbreviation (output)
"not_volatile_write ≡ Not ∘ is_volatile_Write⇩s⇩b"
notation (output)
"flush_all_until_volatile_write" (‹exec'_all'_until'_volatile'_write›)
notation (output)
"share_all_until_volatile_write" (‹share'_all'_until'_volatile'_write›)
notation (output)
stmt_step (‹_⊢ _ →⇩p _› [60,60,60] 100)
notation (output)
augment_rels (‹aug›)
context program
begin
notation (latex output)
direct_concurrent_step (‹_ \<^latex>‹$\overset{\isa{v}_\isa{d}}{\Rightarrow}$› _› [60,60] 100)
notation (latex output)
direct_concurrent_steps (‹_ \<^latex>‹$\overset{\isa{v}_\isa{d}}{\Rightarrow}^{*}$› _› [60,60] 100)
notation (latex output)
sbh_concurrent_step (‹_ \<^latex>‹$\overset{\isa{sbh}}{\Rightarrow}$› _› [60,60] 100)
notation (latex output)
sbh_concurrent_steps (‹_ \<^latex>‹$\overset{\isa{sbh}}{\Rightarrow}^{*}$› _› [60,60] 100)
notation (latex output)
sb_concurrent_step (‹_ \<^latex>‹$\overset{\isa{sb}}{\Rightarrow}$› _› [60,60] 100)
notation (latex output)
sb_concurrent_steps (‹_ \<^latex>‹$\overset{\isa{sb}}{\Rightarrow}^{*}$› _› [60,60] 100)
notation (latex output)
virtual_concurrent_step (‹_ \<^latex>‹$\overset{\isa{v}}{\Rightarrow}$› _› [60,60] 100)
notation (latex output)
virtual_concurrent_steps (‹_ \<^latex>‹$\overset{\isa{v}}{\Rightarrow}^{*}$› _› [60,60] 100)
end
context xvalid_program_progress
begin
abbreviation
"safe_reach_virtual_free_flowing ≡ safe_reach virtual_concurrent_step safe_free_flowing"
notation (latex output)
"safe_reach_virtual_free_flowing" (‹safe'_reach›)
abbreviation
"safe_reach_direct_delayed ≡ safe_reach direct_concurrent_step safe_delayed"
notation (latex output)
"safe_reach_direct_delayed" (‹safe'_reach'_delayed›)
end
translations
"x" <= "(x,())"
"x" <= "((),x)"
translations
"CONST initial⇩v xs ys" <= "CONST initial⇩v xs ys zs"
end