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) sb (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 @ [Progsb 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 ("_ sbh _" [60,60] 100)

notation (output) 
store_buffer_step ("_ sb _" [60,60] 100)

notation (output)
outstanding_refs ("refs")

notation (output)
is_volatile_Writesb ("volatile'_Write")

abbreviation (output)
"not_volatile_write  Not  is_volatile_Writesb"

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 initialv xs ys" <= "CONST initialv xs ys zs"


end