haftmann@31870: (* Title: HOL/Imperative_HOL/Array.thy haftmann@26170: Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen haftmann@26170: *) haftmann@26170: haftmann@26170: header {* Monadic arrays *} haftmann@26170: haftmann@26170: theory Array haftmann@31203: imports Heap_Monad haftmann@26170: begin haftmann@26170: haftmann@37752: subsection {* Primitives *} haftmann@37719: haftmann@37752: definition (*FIXME present :: "heap \ 'a\heap array \ bool" where*) haftmann@37719: array_present :: "'a\heap array \ heap \ bool" where haftmann@37719: "array_present a h \ addr_of_array a < lim h" haftmann@37719: haftmann@37752: definition (*FIXME get :: "heap \ 'a\heap array \ 'a list" where*) haftmann@37719: get_array :: "'a\heap array \ heap \ 'a list" where haftmann@37719: "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" haftmann@37719: haftmann@37752: definition (*FIXME set*) haftmann@37719: set_array :: "'a\heap array \ 'a list \ heap \ heap" where haftmann@37719: "set_array a x = haftmann@37719: arrays_update (\h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" haftmann@37719: haftmann@37752: definition (*FIXME alloc*) haftmann@37752: array :: "'a list \ heap \ 'a\heap array \ heap" where haftmann@37719: "array xs h = (let haftmann@37719: l = lim h; haftmann@37719: r = Array l; haftmann@37719: h'' = set_array r xs (h\lim := l + 1\) haftmann@37719: in (r, h''))" haftmann@37719: haftmann@37752: definition (*FIXME length :: "heap \ 'a\heap array \ nat" where*) haftmann@37752: length :: "'a\heap array \ heap \ nat" where haftmann@37719: "length a h = List.length (get_array a h)" haftmann@37719: haftmann@37752: definition (*FIXME update*) haftmann@37752: change :: "'a\heap array \ nat \ 'a \ heap \ heap" where haftmann@37719: "change a i x h = set_array a ((get_array a h)[i:=x]) h" haftmann@37719: haftmann@37752: definition (*FIXME noteq*) haftmann@37752: noteq_arrs :: "'a\heap array \ 'b\heap array \ bool" (infix "=!!=" 70) where haftmann@37752: "r =!!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_array r \ addr_of_array s" haftmann@37752: haftmann@37752: haftmann@37752: subsection {* Monad operations *} haftmann@37752: haftmann@37752: definition new :: "nat \ 'a\heap \ 'a array Heap" where haftmann@37752: [code del]: "new n x = Heap_Monad.heap (array (replicate n x))" haftmann@37752: haftmann@37752: definition of_list :: "'a\heap list \ 'a array Heap" where haftmann@37752: [code del]: "of_list xs = Heap_Monad.heap (array xs)" haftmann@37752: haftmann@37752: definition make :: "nat \ (nat \ 'a\heap) \ 'a array Heap" where haftmann@37752: [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))" haftmann@37752: haftmann@37752: definition len :: "'a\heap array \ nat Heap" where haftmann@37752: [code del]: "len a = Heap_Monad.heap (\h. (length a h, h))" haftmann@37752: haftmann@37752: definition nth :: "'a\heap array \ nat \ 'a Heap" where haftmann@37752: [code del]: "nth a i = Heap_Monad.guard (\h. i < length a h) haftmann@37752: (\h. (get_array a h ! i, h))" haftmann@37752: haftmann@37752: definition upd :: "nat \ 'a \ 'a\heap array \ 'a\heap array Heap" where haftmann@37752: [code del]: "upd i x a = Heap_Monad.guard (\h. i < length a h) haftmann@37752: (\h. (a, change a i x h))" haftmann@37752: haftmann@37752: definition map_entry :: "nat \ ('a\heap \ 'a) \ 'a array \ 'a array Heap" where haftmann@37752: [code del]: "map_entry i f a = Heap_Monad.guard (\h. i < length a h) haftmann@37752: (\h. (a, change a i (f (get_array a h ! i)) h))" haftmann@37752: haftmann@37752: definition swap :: "nat \ 'a \ 'a\heap array \ 'a Heap" where haftmann@37752: [code del]: "swap i x a = Heap_Monad.guard (\h. i < length a h) haftmann@37752: (\h. (get_array a h ! i, change a i x h))" haftmann@37752: haftmann@37752: definition freeze :: "'a\heap array \ 'a list Heap" where haftmann@37752: [code del]: "freeze a = Heap_Monad.heap (\h. (get_array a h, h))" haftmann@37752: haftmann@37752: haftmann@37752: subsection {* Properties *} haftmann@37719: haftmann@37719: text {* FIXME: Does there exist a "canonical" array axiomatisation in haftmann@37719: the literature? *} haftmann@37719: haftmann@37719: lemma noteq_arrs_sym: "a =!!= b \ b =!!= a" haftmann@37719: and unequal_arrs [simp]: "a \ a' \ a =!!= a'" haftmann@37719: unfolding noteq_arrs_def by auto haftmann@37719: haftmann@37719: lemma noteq_arrs_irrefl: "r =!!= r \ False" haftmann@37719: unfolding noteq_arrs_def by auto haftmann@37719: haftmann@37719: lemma present_new_arr: "array_present a h \ a =!!= fst (array xs h)" haftmann@37719: by (simp add: array_present_def noteq_arrs_def array_def Let_def) haftmann@37719: haftmann@37719: lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" haftmann@37719: by (simp add: get_array_def set_array_def o_def) haftmann@37719: haftmann@37719: lemma array_get_set_neq [simp]: "r =!!= s \ get_array r (set_array s x h) = get_array r h" haftmann@37719: by (simp add: noteq_arrs_def get_array_def set_array_def) haftmann@37719: haftmann@37719: lemma set_array_same [simp]: haftmann@37719: "set_array r x (set_array r y h) = set_array r x h" haftmann@37719: by (simp add: set_array_def) haftmann@37719: haftmann@37719: lemma array_set_set_swap: haftmann@37719: "r =!!= r' \ set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" haftmann@37719: by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) haftmann@37719: haftmann@37719: lemma get_array_change_eq [simp]: haftmann@37719: "get_array a (change a i v h) = (get_array a h) [i := v]" haftmann@37719: by (simp add: change_def) haftmann@37719: haftmann@37719: lemma nth_change_array_neq_array [simp]: haftmann@37719: "a =!!= b \ get_array a (change b j v h) ! i = get_array a h ! i" haftmann@37719: by (simp add: change_def noteq_arrs_def) haftmann@37719: haftmann@37719: lemma get_arry_array_change_elem_neqIndex [simp]: haftmann@37719: "i \ j \ get_array a (change a j v h) ! i = get_array a h ! i" haftmann@37719: by simp haftmann@37719: haftmann@37719: lemma length_change [simp]: haftmann@37719: "length a (change b i v h) = length a h" haftmann@37719: by (simp add: change_def length_def set_array_def get_array_def) haftmann@37719: haftmann@37719: lemma change_swap_neqArray: haftmann@37719: "a =!!= a' \ haftmann@37719: change a i v (change a' i' v' h) haftmann@37719: = change a' i' v' (change a i v h)" haftmann@37719: apply (unfold change_def) haftmann@37719: apply simp haftmann@37719: apply (subst array_set_set_swap, assumption) haftmann@37719: apply (subst array_get_set_neq) haftmann@37719: apply (erule noteq_arrs_sym) haftmann@37719: apply (simp) haftmann@37719: done haftmann@37719: haftmann@37719: lemma change_swap_neqIndex: haftmann@37719: "\ i \ i' \ \ change a i v (change a i' v' h) = change a i' v' (change a i v h)" haftmann@37719: by (auto simp add: change_def array_set_set_swap list_update_swap) haftmann@37719: haftmann@37719: lemma get_array_init_array_list: haftmann@37719: "get_array (fst (array ls h)) (snd (array ls' h)) = ls'" haftmann@37719: by (simp add: Let_def split_def array_def) haftmann@37719: haftmann@37719: lemma set_array: haftmann@37719: "set_array (fst (array ls h)) haftmann@37719: new_ls (snd (array ls h)) haftmann@37719: = snd (array new_ls h)" haftmann@37719: by (simp add: Let_def split_def array_def) haftmann@37719: haftmann@37719: lemma array_present_change [simp]: haftmann@37719: "array_present a (change b i v h) = array_present a h" haftmann@37719: by (simp add: change_def array_present_def set_array_def get_array_def) haftmann@37719: haftmann@37752: lemma execute_new [simp]: haftmann@37752: "Heap_Monad.execute (new n x) h = Some (array (replicate n x) h)" haftmann@37752: by (simp add: new_def) haftmann@26170: haftmann@37752: lemma execute_of_list [simp]: haftmann@37752: "Heap_Monad.execute (of_list xs) h = Some (array xs h)" haftmann@37752: by (simp add: of_list_def) haftmann@26170: haftmann@37752: lemma execute_make [simp]: haftmann@37752: "Heap_Monad.execute (make n f) h = Some (array (map f [0 ..< n]) h)" haftmann@37752: by (simp add: make_def) haftmann@26170: haftmann@37752: lemma execute_len [simp]: haftmann@37752: "Heap_Monad.execute (len a) h = Some (length a h, h)" haftmann@37752: by (simp add: len_def) haftmann@37752: haftmann@37752: lemma execute_nth [simp]: haftmann@37752: "i < length a h \ haftmann@37752: Heap_Monad.execute (nth a i) h = Some (get_array a h ! i, h)" haftmann@37752: "i \ length a h \ Heap_Monad.execute (nth a i) h = None" haftmann@37752: by (simp_all add: nth_def) haftmann@26170: haftmann@37752: lemma execute_upd [simp]: haftmann@37752: "i < length a h \ haftmann@37752: Heap_Monad.execute (upd i x a) h = Some (a, change a i x h)" haftmann@37752: "i \ length a h \ Heap_Monad.execute (nth a i) h = None" haftmann@37752: by (simp_all add: upd_def) haftmann@26170: haftmann@37752: lemma execute_map_entry [simp]: haftmann@37752: "i < length a h \ haftmann@37752: Heap_Monad.execute (map_entry i f a) h = haftmann@37752: Some (a, change a i (f (get_array a h ! i)) h)" haftmann@37752: "i \ length a h \ Heap_Monad.execute (nth a i) h = None" haftmann@37752: by (simp_all add: map_entry_def) haftmann@37752: haftmann@37752: lemma execute_swap [simp]: haftmann@37752: "i < length a h \ haftmann@37752: Heap_Monad.execute (swap i x a) h = haftmann@37752: Some (get_array a h ! i, change a i x h)" haftmann@37752: "i \ length a h \ Heap_Monad.execute (nth a i) h = None" haftmann@37752: by (simp_all add: swap_def) haftmann@37752: haftmann@37752: lemma execute_freeze [simp]: haftmann@37752: "Heap_Monad.execute (freeze a) h = Some (get_array a h, h)" haftmann@37752: by (simp add: freeze_def) haftmann@26170: haftmann@26170: lemma upd_return: haftmann@26170: "upd i x a \ return a = upd i x a" haftmann@37752: by (rule Heap_eqI) (simp add: bindM_def guard_def upd_def) haftmann@26170: haftmann@37752: lemma array_make: haftmann@37752: "new n x = make n (\_. x)" haftmann@37752: by (rule Heap_eqI) (simp add: map_replicate_trivial) haftmann@26170: haftmann@37752: lemma array_of_list_make: haftmann@37752: "of_list xs = make (List.length xs) (\n. xs ! n)" haftmann@37752: by (rule Heap_eqI) (simp add: map_nth) haftmann@26170: haftmann@37752: hide_const (open) new map haftmann@26170: haftmann@26182: haftmann@26182: subsection {* Code generator setup *} haftmann@26182: haftmann@26182: subsubsection {* Logical intermediate layer *} haftmann@26182: haftmann@26182: definition new' where haftmann@31205: [code del]: "new' = Array.new o Code_Numeral.nat_of" haftmann@37752: haftmann@28562: lemma [code]: haftmann@37752: "Array.new = new' o Code_Numeral.of_nat" haftmann@26182: by (simp add: new'_def o_def) haftmann@26182: haftmann@26182: definition of_list' where haftmann@31205: [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)" haftmann@37752: haftmann@28562: lemma [code]: haftmann@37752: "Array.of_list xs = of_list' (Code_Numeral.of_nat (List.length xs)) xs" haftmann@26182: by (simp add: of_list'_def) haftmann@26182: haftmann@26182: definition make' where haftmann@31205: [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" haftmann@37752: haftmann@28562: lemma [code]: haftmann@37752: "Array.make n f = make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" haftmann@26182: by (simp add: make'_def o_def) haftmann@26182: haftmann@37719: definition len' where haftmann@37719: [code del]: "len' a = Array.len a \= (\n. return (Code_Numeral.of_nat n))" haftmann@37752: haftmann@28562: lemma [code]: haftmann@37752: "Array.len a = len' a \= (\i. return (Code_Numeral.nat_of i))" haftmann@37719: by (simp add: len'_def) haftmann@26182: haftmann@26182: definition nth' where haftmann@31205: [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" haftmann@37752: haftmann@28562: lemma [code]: haftmann@37752: "Array.nth a n = nth' a (Code_Numeral.of_nat n)" haftmann@26182: by (simp add: nth'_def) haftmann@26182: haftmann@26182: definition upd' where haftmann@31205: [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \ return ()" haftmann@37752: haftmann@28562: lemma [code]: haftmann@37752: "Array.upd i x a = upd' a (Code_Numeral.of_nat i) x \ return a" haftmann@37709: by (simp add: upd'_def upd_return) haftmann@26182: haftmann@37752: lemma [code]: haftmann@37752: "map_entry i f a = (do haftmann@37752: x \ nth a i; haftmann@37752: upd i (f x) a haftmann@37752: done)" haftmann@37752: by (rule Heap_eqI) (simp add: bindM_def guard_def map_entry_def) haftmann@26182: haftmann@37752: lemma [code]: haftmann@37752: "swap i x a = (do haftmann@37752: y \ nth a i; haftmann@37752: upd i x a; haftmann@37752: return y haftmann@37752: done)" haftmann@37752: by (rule Heap_eqI) (simp add: bindM_def guard_def swap_def) haftmann@37752: haftmann@37752: lemma [code]: haftmann@37752: "freeze a = (do haftmann@37752: n \ len a; haftmann@37752: mapM (\i. nth a i) [0..x. fst (the (if x < length a h haftmann@37752: then Some (get_array a h ! x, h) else None))) haftmann@37752: [0.. len a; haftmann@37752: mapM (Array.nth a) [0.. len a; haftmann@37752: mapM (Array.nth a) [0../ Array.array/ ((_),/ (_)))") haftmann@35846: code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)") haftmann@26752: code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") haftmann@37719: code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)") haftmann@26752: code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") haftmann@26752: code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") haftmann@26182: haftmann@26182: code_reserved SML Array haftmann@26182: haftmann@26182: haftmann@37752: text {* OCaml *} haftmann@26182: haftmann@26182: code_type array (OCaml "_/ array") haftmann@26182: code_const Array (OCaml "failwith/ \"bare Array\"") haftmann@32580: code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)") haftmann@35846: code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)") haftmann@37719: code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))") haftmann@32580: code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))") haftmann@32580: code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)") haftmann@26182: haftmann@26182: code_reserved OCaml Array haftmann@26182: haftmann@26182: haftmann@37752: text {* Haskell *} haftmann@26182: haftmann@29793: code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _") haftmann@26182: code_const Array (Haskell "error/ \"bare Array\"") haftmann@29793: code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)") haftmann@29793: code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)") haftmann@37719: code_const Array.len' (Haskell "Heap.lengthArray") haftmann@29793: code_const Array.nth' (Haskell "Heap.readArray") haftmann@29793: code_const Array.upd' (Haskell "Heap.writeArray") haftmann@26182: haftmann@26170: end