qualified names for (almost) all array operations
authorhaftmann
Tue Jul 13 16:00:56 2010 +0200 (2010-07-13 ago)
changeset 378040145e59c1f6c
parent 37803 582d0fbd201e
child 37805 0f797d586ce5
qualified names for (almost) all array operations
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Ref.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 15:37:31 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 16:00:56 2010 +0200
     1.3 @@ -10,48 +10,43 @@
     1.4  
     1.5  subsection {* Primitives *}
     1.6  
     1.7 -definition (*FIXME present *)
     1.8 -  array_present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where
     1.9 -  "array_present h a \<longleftrightarrow> addr_of_array a < lim h"
    1.10 +definition present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where
    1.11 +  "present h a \<longleftrightarrow> addr_of_array a < lim h"
    1.12  
    1.13  definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*)
    1.14    get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
    1.15    "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
    1.16  
    1.17 -definition (*FIXME set*)
    1.18 -  set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
    1.19 -  "set_array a x = 
    1.20 -  arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
    1.21 +definition set :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
    1.22 +  "set a x = arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
    1.23  
    1.24 -definition (*FIXME alloc*)
    1.25 -  array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
    1.26 -  "array xs h = (let
    1.27 +definition alloc :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
    1.28 +  "alloc xs h = (let
    1.29       l = lim h;
    1.30       r = Array l;
    1.31 -     h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
    1.32 +     h'' = set r xs (h\<lparr>lim := l + 1\<rparr>)
    1.33     in (r, h''))"
    1.34  
    1.35  definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where
    1.36    "length h a = List.length (get_array a h)"
    1.37    
    1.38  definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
    1.39 -  "update a i x h = set_array a ((get_array a h)[i:=x]) h"
    1.40 +  "update a i x h = set a ((get_array a h)[i:=x]) h"
    1.41  
    1.42 -definition (*FIXME noteq*)
    1.43 -  noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
    1.44 +definition noteq :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
    1.45    "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
    1.46  
    1.47  
    1.48  subsection {* Monad operations *}
    1.49  
    1.50  definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
    1.51 -  [code del]: "new n x = Heap_Monad.heap (array (replicate n x))"
    1.52 +  [code del]: "new n x = Heap_Monad.heap (alloc (replicate n x))"
    1.53  
    1.54  definition of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
    1.55 -  [code del]: "of_list xs = Heap_Monad.heap (array xs)"
    1.56 +  [code del]: "of_list xs = Heap_Monad.heap (alloc xs)"
    1.57  
    1.58  definition make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" where
    1.59 -  [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
    1.60 +  [code del]: "make n f = Heap_Monad.heap (alloc (map f [0 ..< n]))"
    1.61  
    1.62  definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
    1.63    [code del]: "len a = Heap_Monad.tap (\<lambda>h. length h a)"
    1.64 @@ -85,27 +80,27 @@
    1.65  
    1.66  lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
    1.67    and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
    1.68 -  unfolding noteq_arrs_def by auto
    1.69 +  unfolding noteq_def by auto
    1.70  
    1.71  lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
    1.72 -  unfolding noteq_arrs_def by auto
    1.73 +  unfolding noteq_def by auto
    1.74  
    1.75 -lemma present_new_arr: "array_present h a \<Longrightarrow> a =!!= fst (array xs h)"
    1.76 -  by (simp add: array_present_def noteq_arrs_def array_def Let_def)
    1.77 +lemma present_new_arr: "present h a \<Longrightarrow> a =!!= fst (alloc xs h)"
    1.78 +  by (simp add: present_def noteq_def alloc_def Let_def)
    1.79  
    1.80 -lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
    1.81 -  by (simp add: get_array_def set_array_def o_def)
    1.82 +lemma array_get_set_eq [simp]: "get_array r (set r x h) = x"
    1.83 +  by (simp add: get_array_def set_def o_def)
    1.84  
    1.85 -lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
    1.86 -  by (simp add: noteq_arrs_def get_array_def set_array_def)
    1.87 +lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set s x h) = get_array r h"
    1.88 +  by (simp add: noteq_def get_array_def set_def)
    1.89  
    1.90  lemma set_array_same [simp]:
    1.91 -  "set_array r x (set_array r y h) = set_array r x h"
    1.92 -  by (simp add: set_array_def)
    1.93 +  "set r x (set r y h) = set r x h"
    1.94 +  by (simp add: set_def)
    1.95  
    1.96  lemma array_set_set_swap:
    1.97 -  "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
    1.98 -  by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
    1.99 +  "r =!!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
   1.100 +  by (simp add: Let_def expand_fun_eq noteq_def set_def)
   1.101  
   1.102  lemma get_array_update_eq [simp]:
   1.103    "get_array a (update a i v h) = (get_array a h) [i := v]"
   1.104 @@ -113,7 +108,7 @@
   1.105  
   1.106  lemma nth_update_array_neq_array [simp]:
   1.107    "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i"
   1.108 -  by (simp add: update_def noteq_arrs_def)
   1.109 +  by (simp add: update_def noteq_def)
   1.110  
   1.111  lemma get_arry_array_update_elem_neqIndex [simp]:
   1.112    "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i"
   1.113 @@ -121,7 +116,7 @@
   1.114  
   1.115  lemma length_update [simp]: 
   1.116    "length (update b i v h) = length h"
   1.117 -  by (simp add: update_def length_def set_array_def get_array_def expand_fun_eq)
   1.118 +  by (simp add: update_def length_def set_def get_array_def expand_fun_eq)
   1.119  
   1.120  lemma update_swap_neqArray:
   1.121    "a =!!= a' \<Longrightarrow> 
   1.122 @@ -140,32 +135,32 @@
   1.123    by (auto simp add: update_def array_set_set_swap list_update_swap)
   1.124  
   1.125  lemma get_array_init_array_list:
   1.126 -  "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
   1.127 -  by (simp add: Let_def split_def array_def)
   1.128 +  "get_array (fst (alloc ls h)) (snd (alloc ls' h)) = ls'"
   1.129 +  by (simp add: Let_def split_def alloc_def)
   1.130  
   1.131  lemma set_array:
   1.132 -  "set_array (fst (array ls h))
   1.133 -     new_ls (snd (array ls h))
   1.134 -       = snd (array new_ls h)"
   1.135 -  by (simp add: Let_def split_def array_def)
   1.136 +  "set (fst (alloc ls h))
   1.137 +     new_ls (snd (alloc ls h))
   1.138 +       = snd (alloc new_ls h)"
   1.139 +  by (simp add: Let_def split_def alloc_def)
   1.140  
   1.141  lemma array_present_update [simp]: 
   1.142 -  "array_present (update b i v h) = array_present h"
   1.143 -  by (simp add: update_def array_present_def set_array_def get_array_def expand_fun_eq)
   1.144 +  "present (update b i v h) = present h"
   1.145 +  by (simp add: update_def present_def set_def get_array_def expand_fun_eq)
   1.146  
   1.147  lemma array_present_array [simp]:
   1.148 -  "array_present (snd (array xs h)) (fst (array xs h))"
   1.149 -  by (simp add: array_present_def array_def set_array_def Let_def)
   1.150 +  "present (snd (alloc xs h)) (fst (alloc xs h))"
   1.151 +  by (simp add: present_def alloc_def set_def Let_def)
   1.152  
   1.153  lemma not_array_present_array [simp]:
   1.154 -  "\<not> array_present h (fst (array xs h))"
   1.155 -  by (simp add: array_present_def array_def Let_def)
   1.156 +  "\<not> present h (fst (alloc xs h))"
   1.157 +  by (simp add: present_def alloc_def Let_def)
   1.158  
   1.159  
   1.160  text {* Monad operations *}
   1.161  
   1.162  lemma execute_new [execute_simps]:
   1.163 -  "execute (new n x) h = Some (array (replicate n x) h)"
   1.164 +  "execute (new n x) h = Some (alloc (replicate n x) h)"
   1.165    by (simp add: new_def execute_simps)
   1.166  
   1.167  lemma success_newI [success_intros]:
   1.168 @@ -173,18 +168,18 @@
   1.169    by (auto intro: success_intros simp add: new_def)
   1.170  
   1.171  lemma crel_newI [crel_intros]:
   1.172 -  assumes "(a, h') = array (replicate n x) h"
   1.173 +  assumes "(a, h') = alloc (replicate n x) h"
   1.174    shows "crel (new n x) h h' a"
   1.175    by (rule crelI) (simp add: assms execute_simps)
   1.176  
   1.177  lemma crel_newE [crel_elims]:
   1.178    assumes "crel (new n x) h h' r"
   1.179 -  obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
   1.180 -    "get_array r h' = replicate n x" "array_present h' r" "\<not> array_present h r"
   1.181 +  obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" 
   1.182 +    "get_array r h' = replicate n x" "present h' r" "\<not> present h r"
   1.183    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
   1.184  
   1.185  lemma execute_of_list [execute_simps]:
   1.186 -  "execute (of_list xs) h = Some (array xs h)"
   1.187 +  "execute (of_list xs) h = Some (alloc xs h)"
   1.188    by (simp add: of_list_def execute_simps)
   1.189  
   1.190  lemma success_of_listI [success_intros]:
   1.191 @@ -192,18 +187,18 @@
   1.192    by (auto intro: success_intros simp add: of_list_def)
   1.193  
   1.194  lemma crel_of_listI [crel_intros]:
   1.195 -  assumes "(a, h') = array xs h"
   1.196 +  assumes "(a, h') = alloc xs h"
   1.197    shows "crel (of_list xs) h h' a"
   1.198    by (rule crelI) (simp add: assms execute_simps)
   1.199  
   1.200  lemma crel_of_listE [crel_elims]:
   1.201    assumes "crel (of_list xs) h h' r"
   1.202 -  obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
   1.203 -    "get_array r h' = xs" "array_present h' r" "\<not> array_present h r"
   1.204 +  obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" 
   1.205 +    "get_array r h' = xs" "present h' r" "\<not> present h r"
   1.206    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
   1.207  
   1.208  lemma execute_make [execute_simps]:
   1.209 -  "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
   1.210 +  "execute (make n f) h = Some (alloc (map f [0 ..< n]) h)"
   1.211    by (simp add: make_def execute_simps)
   1.212  
   1.213  lemma success_makeI [success_intros]:
   1.214 @@ -211,14 +206,14 @@
   1.215    by (auto intro: success_intros simp add: make_def)
   1.216  
   1.217  lemma crel_makeI [crel_intros]:
   1.218 -  assumes "(a, h') = array (map f [0 ..< n]) h"
   1.219 +  assumes "(a, h') = alloc (map f [0 ..< n]) h"
   1.220    shows "crel (make n f) h h' a"
   1.221    by (rule crelI) (simp add: assms execute_simps)
   1.222  
   1.223  lemma crel_makeE [crel_elims]:
   1.224    assumes "crel (make n f) h h' r"
   1.225 -  obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
   1.226 -    "get_array r h' = map f [0 ..< n]" "array_present h' r" "\<not> array_present h r"
   1.227 +  obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" 
   1.228 +    "get_array r h' = map f [0 ..< n]" "present h' r" "\<not> present h r"
   1.229    using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
   1.230  
   1.231  lemma execute_len [execute_simps]:
   1.232 @@ -355,7 +350,7 @@
   1.233    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   1.234    by (rule Heap_eqI) (simp add: map_nth execute_simps)
   1.235  
   1.236 -hide_const (open) update new of_list make len nth upd map_entry swap freeze
   1.237 +hide_const (open) present (*get*) set alloc length update noteq new of_list make len nth upd map_entry swap freeze
   1.238  
   1.239  
   1.240  subsection {* Code generator setup *}
   1.241 @@ -427,12 +422,12 @@
   1.242  proof (rule Heap_eqI)
   1.243    fix h
   1.244    have *: "List.map
   1.245 -     (\<lambda>x. fst (the (if x < length h a
   1.246 +     (\<lambda>x. fst (the (if x < Array.length h a
   1.247                      then Some (get_array a h ! x, h) else None)))
   1.248 -     [0..<length h a] =
   1.249 -       List.map (List.nth (get_array a h)) [0..<length h a]"
   1.250 +     [0..<Array.length h a] =
   1.251 +       List.map (List.nth (get_array a h)) [0..<Array.length h a]"
   1.252      by simp
   1.253 -  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length h a]) h =
   1.254 +  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<Array.length h a]) h =
   1.255      Some (get_array a h, h)"
   1.256      apply (subst execute_fold_map_unchanged_heap)
   1.257      apply (simp_all add: nth_def guard_def *)
     2.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 15:37:31 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 16:00:56 2010 +0200
     2.3 @@ -228,15 +228,15 @@
     2.4  
     2.5  lemma get_update [simp]:
     2.6    "get (Array.update a i v h) r  = get h r"
     2.7 -  by (simp add: get_def Array.update_def set_array_def)
     2.8 +  by (simp add: get_def Array.update_def Array.set_def)
     2.9  
    2.10  lemma alloc_update:
    2.11    "fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
    2.12 -  by (simp add: Array.update_def get_array_def set_array_def alloc_def Let_def)
    2.13 +  by (simp add: Array.update_def get_array_def Array.set_def alloc_def Let_def)
    2.14  
    2.15  lemma update_set_swap:
    2.16    "Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
    2.17 -  by (simp add: Array.update_def get_array_def set_array_def set_def)
    2.18 +  by (simp add: Array.update_def get_array_def Array.set_def set_def)
    2.19  
    2.20  lemma length_alloc [simp]: 
    2.21    "Array.length (snd (alloc v h)) a = Array.length h a"
    2.22 @@ -248,19 +248,19 @@
    2.23  
    2.24  lemma present_update [simp]: 
    2.25    "present (Array.update a i v h) = present h"
    2.26 -  by (simp add: Array.update_def set_array_def expand_fun_eq present_def)
    2.27 +  by (simp add: Array.update_def Array.set_def expand_fun_eq present_def)
    2.28  
    2.29  lemma array_present_set [simp]:
    2.30 -  "array_present (set r v h) = array_present h"
    2.31 -  by (simp add: array_present_def set_def expand_fun_eq)
    2.32 +  "Array.present (set r v h) = Array.present h"
    2.33 +  by (simp add: Array.present_def set_def expand_fun_eq)
    2.34  
    2.35  lemma array_present_alloc [simp]:
    2.36 -  "array_present h a \<Longrightarrow> array_present (snd (alloc v h)) a"
    2.37 -  by (simp add: array_present_def alloc_def Let_def)
    2.38 +  "Array.present h a \<Longrightarrow> Array.present (snd (alloc v h)) a"
    2.39 +  by (simp add: Array.present_def alloc_def Let_def)
    2.40  
    2.41  lemma set_array_set_swap:
    2.42 -  "set_array a xs (set r x' h) = set r x' (set_array a xs h)"
    2.43 -  by (simp add: set_array_def set_def)
    2.44 +  "Array.set a xs (set r x' h) = set r x' (Array.set a xs h)"
    2.45 +  by (simp add: Array.set_def set_def)
    2.46  
    2.47  hide_const (open) present get set alloc noteq lookup update change
    2.48