Store.thy

Back to the index of JVM0_ASCII

Store = Map +  

syntax
 value	:: "['a ~=> 'b,'a] => 'b"			("_ !! _")		
translations
 "t !! x"  == "the (t x)"

constdefs
 map_compose :: "['b => 'c,'a  ~=> 'b] => ('a ~=> 'c)"
 "map_compose f m == % k. option_map f (m k)"

 newref :: "('a ~=> 'b) => 'a"
 "newref s == @v. s v = None"

end

Theorems proved in Store.ML:

newref_None

hp x = None ==> hp (newref hp) = None