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



(* hide unit's in tuples *)

translations
 "x" <= "(x,())"
 "x" <= "((),x)"


translations
"CONST initial⇩v xs ys" <= "CONST initial⇩v xs ys zs"


end