src/HOL/Hoare/Pointers0.thy
changeset 35416 d8d7d1b785af
parent 35316 870dfea4f9c0
child 35419 d78659d1723e
     1.1 --- a/src/HOL/Hoare/Pointers0.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Hoare/Pointers0.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -73,8 +73,7 @@
     1.4  
     1.5  subsubsection "Relational abstraction"
     1.6  
     1.7 -constdefs
     1.8 - List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
     1.9 +definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.10  "List h x as == Path h x as Null"
    1.11  
    1.12  lemma [simp]: "List h x [] = (x = Null)"
    1.13 @@ -122,10 +121,10 @@
    1.14  
    1.15  subsection "Functional abstraction"
    1.16  
    1.17 -constdefs
    1.18 - islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
    1.19 +definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where
    1.20  "islist h p == \<exists>as. List h p as"
    1.21 - list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
    1.22 +
    1.23 +definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
    1.24  "list h p == SOME as. List h p as"
    1.25  
    1.26  lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
    1.27 @@ -407,7 +406,7 @@
    1.28  
    1.29  subsection "Storage allocation"
    1.30  
    1.31 -constdefs new :: "'a set \<Rightarrow> 'a::ref"
    1.32 +definition new :: "'a set \<Rightarrow> 'a::ref" where
    1.33  "new A == SOME a. a \<notin> A & a \<noteq> Null"
    1.34  
    1.35