Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Bali/State.thy
changeset 14171 0cab06e3bbd0
parent 13688 a0b16d42d489
child 14766 c0401da7726d
equal deleted inserted replaced
14170:edd5a2ea3807 14171:0cab06e3bbd0 
   264 
   264 
   265 subsection "memory allocation"
 
   265 subsection "memory allocation"
 
   266 
   266 
   267 constdefs
 
   267 constdefs
 
   268   new_Addr     :: "heap \<Rightarrow> loc option"
 
   268   new_Addr     :: "heap \<Rightarrow> loc option"
 
   269  "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon>a. h a = None)"
 
   269  "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon> a. h a = None)"
 
   270 
   270 
   271 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
 
   271 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
 
   272 apply (unfold new_Addr_def)
 
   272 apply (unfold new_Addr_def)
 
   273 apply auto
 
   273 apply auto
 
   274 apply (case_tac "h (SOME a\<Colon>loc. h a = None)")
 
   274 apply (case_tac "h (SOME a\<Colon>loc. h a = None)")
isabelle