1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Imperative_HOL/Array.thy Thu Jan 08 17:10:41 2009 +0100
1.3 @@ -0,0 +1,209 @@
1.4 +(* Title: HOL/Library/Array.thy
1.5 + ID: $Id$
1.6 + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
1.7 +*)
1.8 +
1.9 +header {* Monadic arrays *}
1.10 +
1.11 +theory Array
1.12 +imports Heap_Monad Code_Index
1.13 +begin
1.14 +
1.15 +subsection {* Primitives *}
1.16 +
1.17 +definition
1.18 + new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
1.19 + [code del]: "new n x = Heap_Monad.heap (Heap.array n x)"
1.20 +
1.21 +definition
1.22 + of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
1.23 + [code del]: "of_list xs = Heap_Monad.heap (Heap.array_of_list xs)"
1.24 +
1.25 +definition
1.26 + length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
1.27 + [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
1.28 +
1.29 +definition
1.30 + nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
1.31 +where
1.32 + [code del]: "nth a i = (do len \<leftarrow> length a;
1.33 + (if i < len
1.34 + then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
1.35 + else raise (''array lookup: index out of range''))
1.36 + done)"
1.37 +
1.38 +-- {* FIXME adjustion for List theory *}
1.39 +no_syntax
1.40 + nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
1.41 +
1.42 +abbreviation
1.43 + nth_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
1.44 +where
1.45 + "nth_list \<equiv> List.nth"
1.46 +
1.47 +definition
1.48 + upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
1.49 +where
1.50 + [code del]: "upd i x a = (do len \<leftarrow> length a;
1.51 + (if i < len
1.52 + then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
1.53 + else raise (''array update: index out of range''))
1.54 + done)"
1.55 +
1.56 +lemma upd_return:
1.57 + "upd i x a \<guillemotright> return a = upd i x a"
1.58 +proof (rule Heap_eqI)
1.59 + fix h
1.60 + obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
1.61 + by (cases "Heap_Monad.execute (Array.length a) h")
1.62 + then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
1.63 + by (auto simp add: upd_def bindM_def split: sum.split)
1.64 +qed
1.65 +
1.66 +
1.67 +subsection {* Derivates *}
1.68 +
1.69 +definition
1.70 + map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
1.71 +where
1.72 + "map_entry i f a = (do
1.73 + x \<leftarrow> nth a i;
1.74 + upd i (f x) a
1.75 + done)"
1.76 +
1.77 +definition
1.78 + swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap"
1.79 +where
1.80 + "swap i x a = (do
1.81 + y \<leftarrow> nth a i;
1.82 + upd i x a;
1.83 + return y
1.84 + done)"
1.85 +
1.86 +definition
1.87 + make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap"
1.88 +where
1.89 + "make n f = of_list (map f [0 ..< n])"
1.90 +
1.91 +definition
1.92 + freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
1.93 +where
1.94 + "freeze a = (do
1.95 + n \<leftarrow> length a;
1.96 + mapM (nth a) [0..<n]
1.97 + done)"
1.98 +
1.99 +definition
1.100 + map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
1.101 +where
1.102 + "map f a = (do
1.103 + n \<leftarrow> length a;
1.104 + mapM (\<lambda>n. map_entry n f a) [0..<n];
1.105 + return a
1.106 + done)"
1.107 +
1.108 +hide (open) const new map -- {* avoid clashed with some popular names *}
1.109 +
1.110 +
1.111 +subsection {* Properties *}
1.112 +
1.113 +lemma array_make [code]:
1.114 + "Array.new n x = make n (\<lambda>_. x)"
1.115 + by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
1.116 + monad_simp array_of_list_replicate [symmetric]
1.117 + map_replicate_trivial replicate_append_same
1.118 + of_list_def)
1.119 +
1.120 +lemma array_of_list_make [code]:
1.121 + "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
1.122 + unfolding make_def map_nth ..
1.123 +
1.124 +
1.125 +subsection {* Code generator setup *}
1.126 +
1.127 +subsubsection {* Logical intermediate layer *}
1.128 +
1.129 +definition new' where
1.130 + [code del]: "new' = Array.new o nat_of_index"
1.131 +hide (open) const new'
1.132 +lemma [code]:
1.133 + "Array.new = Array.new' o index_of_nat"
1.134 + by (simp add: new'_def o_def)
1.135 +
1.136 +definition of_list' where
1.137 + [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
1.138 +hide (open) const of_list'
1.139 +lemma [code]:
1.140 + "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
1.141 + by (simp add: of_list'_def)
1.142 +
1.143 +definition make' where
1.144 + [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
1.145 +hide (open) const make'
1.146 +lemma [code]:
1.147 + "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
1.148 + by (simp add: make'_def o_def)
1.149 +
1.150 +definition length' where
1.151 + [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
1.152 +hide (open) const length'
1.153 +lemma [code]:
1.154 + "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
1.155 + by (simp add: length'_def monad_simp',
1.156 + simp add: liftM_def comp_def monad_simp,
1.157 + simp add: monad_simp')
1.158 +
1.159 +definition nth' where
1.160 + [code del]: "nth' a = Array.nth a o nat_of_index"
1.161 +hide (open) const nth'
1.162 +lemma [code]:
1.163 + "Array.nth a n = Array.nth' a (index_of_nat n)"
1.164 + by (simp add: nth'_def)
1.165 +
1.166 +definition upd' where
1.167 + [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
1.168 +hide (open) const upd'
1.169 +lemma [code]:
1.170 + "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
1.171 + by (simp add: upd'_def monad_simp upd_return)
1.172 +
1.173 +
1.174 +subsubsection {* SML *}
1.175 +
1.176 +code_type array (SML "_/ array")
1.177 +code_const Array (SML "raise/ (Fail/ \"bare Array\")")
1.178 +code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
1.179 +code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
1.180 +code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
1.181 +code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
1.182 +code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
1.183 +code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
1.184 +
1.185 +code_reserved SML Array
1.186 +
1.187 +
1.188 +subsubsection {* OCaml *}
1.189 +
1.190 +code_type array (OCaml "_/ array")
1.191 +code_const Array (OCaml "failwith/ \"bare Array\"")
1.192 +code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
1.193 +code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
1.194 +code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
1.195 +code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
1.196 +code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
1.197 +code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
1.198 +
1.199 +code_reserved OCaml Array
1.200 +
1.201 +
1.202 +subsubsection {* Haskell *}
1.203 +
1.204 +code_type array (Haskell "STArray/ RealWorld/ _")
1.205 +code_const Array (Haskell "error/ \"bare Array\"")
1.206 +code_const Array.new' (Haskell "newArray/ (0,/ _)")
1.207 +code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
1.208 +code_const Array.length' (Haskell "lengthArray")
1.209 +code_const Array.nth' (Haskell "readArray")
1.210 +code_const Array.upd' (Haskell "writeArray")
1.211 +
1.212 +end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Imperative_HOL/Heap.thy Thu Jan 08 17:10:41 2009 +0100
2.3 @@ -0,0 +1,434 @@
2.4 +(* Title: HOL/Library/Heap.thy
2.5 + ID: $Id$
2.6 + Author: John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
2.7 +*)
2.8 +
2.9 +header {* A polymorphic heap based on cantor encodings *}
2.10 +
2.11 +theory Heap
2.12 +imports Plain "~~/src/HOL/List" Countable Typerep
2.13 +begin
2.14 +
2.15 +subsection {* Representable types *}
2.16 +
2.17 +text {* The type class of representable types *}
2.18 +
2.19 +class heap = typerep + countable
2.20 +
2.21 +text {* Instances for common HOL types *}
2.22 +
2.23 +instance nat :: heap ..
2.24 +
2.25 +instance "*" :: (heap, heap) heap ..
2.26 +
2.27 +instance "+" :: (heap, heap) heap ..
2.28 +
2.29 +instance list :: (heap) heap ..
2.30 +
2.31 +instance option :: (heap) heap ..
2.32 +
2.33 +instance int :: heap ..
2.34 +
2.35 +instance message_string :: countable
2.36 + by (rule countable_classI [of "message_string_case to_nat"])
2.37 + (auto split: message_string.splits)
2.38 +
2.39 +instance message_string :: heap ..
2.40 +
2.41 +text {* Reflected types themselves are heap-representable *}
2.42 +
2.43 +instantiation typerep :: countable
2.44 +begin
2.45 +
2.46 +fun to_nat_typerep :: "typerep \<Rightarrow> nat" where
2.47 + "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
2.48 +
2.49 +instance
2.50 +proof (rule countable_classI)
2.51 + fix t t' :: typerep and ts
2.52 + have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')
2.53 + \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')"
2.54 + proof (induct rule: typerep.induct)
2.55 + case (Typerep c ts) show ?case
2.56 + proof (rule allI, rule impI)
2.57 + fix t'
2.58 + assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"
2.59 + then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"
2.60 + by (cases t') auto
2.61 + with Typerep hyp have "c = c'" and "ts = ts'" by simp_all
2.62 + with t' show "Typerep.Typerep c ts = t'" by simp
2.63 + qed
2.64 + next
2.65 + case Nil_typerep then show ?case by simp
2.66 + next
2.67 + case (Cons_typerep t ts) then show ?case by auto
2.68 + qed
2.69 + then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto
2.70 + moreover assume "to_nat_typerep t = to_nat_typerep t'"
2.71 + ultimately show "t = t'" by simp
2.72 +qed
2.73 +
2.74 +end
2.75 +
2.76 +instance typerep :: heap ..
2.77 +
2.78 +
2.79 +subsection {* A polymorphic heap with dynamic arrays and references *}
2.80 +
2.81 +types addr = nat -- "untyped heap references"
2.82 +
2.83 +datatype 'a array = Array addr
2.84 +datatype 'a ref = Ref addr -- "note the phantom type 'a "
2.85 +
2.86 +primrec addr_of_array :: "'a array \<Rightarrow> addr" where
2.87 + "addr_of_array (Array x) = x"
2.88 +
2.89 +primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where
2.90 + "addr_of_ref (Ref x) = x"
2.91 +
2.92 +lemma addr_of_array_inj [simp]:
2.93 + "addr_of_array a = addr_of_array a' \<longleftrightarrow> a = a'"
2.94 + by (cases a, cases a') simp_all
2.95 +
2.96 +lemma addr_of_ref_inj [simp]:
2.97 + "addr_of_ref r = addr_of_ref r' \<longleftrightarrow> r = r'"
2.98 + by (cases r, cases r') simp_all
2.99 +
2.100 +instance array :: (type) countable
2.101 + by (rule countable_classI [of addr_of_array]) simp
2.102 +
2.103 +instance ref :: (type) countable
2.104 + by (rule countable_classI [of addr_of_ref]) simp
2.105 +
2.106 +setup {*
2.107 + Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap array"})
2.108 + #> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap ref"})
2.109 + #> Sign.add_const_constraint (@{const_name addr_of_array}, SOME @{typ "'a\<Colon>heap array \<Rightarrow> nat"})
2.110 + #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
2.111 +*}
2.112 +
2.113 +types heap_rep = nat -- "representable values"
2.114 +
2.115 +record heap =
2.116 + arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"
2.117 + refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep"
2.118 + lim :: addr
2.119 +
2.120 +definition empty :: heap where
2.121 + "empty = \<lparr>arrays = (\<lambda>_. undefined), refs = (\<lambda>_. undefined), lim = 0\<rparr>" -- "why undefined?"
2.122 +
2.123 +
2.124 +subsection {* Imperative references and arrays *}
2.125 +
2.126 +text {*
2.127 + References and arrays are developed in parallel,
2.128 + but keeping them separate makes some later proofs simpler.
2.129 +*}
2.130 +
2.131 +subsubsection {* Primitive operations *}
2.132 +
2.133 +definition
2.134 + new_ref :: "heap \<Rightarrow> ('a\<Colon>heap) ref \<times> heap" where
2.135 + "new_ref h = (let l = lim h in (Ref l, h\<lparr>lim := l + 1\<rparr>))"
2.136 +
2.137 +definition
2.138 + new_array :: "heap \<Rightarrow> ('a\<Colon>heap) array \<times> heap" where
2.139 + "new_array h = (let l = lim h in (Array l, h\<lparr>lim := l + 1\<rparr>))"
2.140 +
2.141 +definition
2.142 + ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
2.143 + "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
2.144 +
2.145 +definition
2.146 + array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
2.147 + "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
2.148 +
2.149 +definition
2.150 + get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where
2.151 + "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))"
2.152 +
2.153 +definition
2.154 + get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
2.155 + "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
2.156 +
2.157 +definition
2.158 + set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
2.159 + "set_ref r x =
2.160 + refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
2.161 +
2.162 +definition
2.163 + set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
2.164 + "set_array a x =
2.165 + arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
2.166 +
2.167 +subsubsection {* Interface operations *}
2.168 +
2.169 +definition
2.170 + ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
2.171 + "ref x h = (let (r, h') = new_ref h;
2.172 + h'' = set_ref r x h'
2.173 + in (r, h''))"
2.174 +
2.175 +definition
2.176 + array :: "nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
2.177 + "array n x h = (let (r, h') = new_array h;
2.178 + h'' = set_array r (replicate n x) h'
2.179 + in (r, h''))"
2.180 +
2.181 +definition
2.182 + array_of_list :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
2.183 + "array_of_list xs h = (let (r, h') = new_array h;
2.184 + h'' = set_array r xs h'
2.185 + in (r, h''))"
2.186 +
2.187 +definition
2.188 + upd :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
2.189 + "upd a i x h = set_array a ((get_array a h)[i:=x]) h"
2.190 +
2.191 +definition
2.192 + length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
2.193 + "length a h = size (get_array a h)"
2.194 +
2.195 +definition
2.196 + array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
2.197 + "array_ran a h = {e. Some e \<in> set (get_array a h)}"
2.198 + -- {*FIXME*}
2.199 +
2.200 +
2.201 +subsubsection {* Reference equality *}
2.202 +
2.203 +text {*
2.204 + The following relations are useful for comparing arrays and references.
2.205 +*}
2.206 +
2.207 +definition
2.208 + noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70)
2.209 +where
2.210 + "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
2.211 +
2.212 +definition
2.213 + noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70)
2.214 +where
2.215 + "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
2.216 +
2.217 +lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
2.218 + and noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
2.219 + and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
2.220 + and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
2.221 +unfolding noteq_refs_def noteq_arrs_def by auto
2.222 +
2.223 +lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
2.224 + by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)
2.225 +
2.226 +lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array v x h)"
2.227 + by (simp add: array_present_def noteq_arrs_def new_array_def array_def Let_def)
2.228 +
2.229 +
2.230 +subsubsection {* Properties of heap containers *}
2.231 +
2.232 +text {* Properties of imperative arrays *}
2.233 +
2.234 +text {* FIXME: Does there exist a "canonical" array axiomatisation in
2.235 +the literature? *}
2.236 +
2.237 +lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
2.238 + by (simp add: get_array_def set_array_def)
2.239 +
2.240 +lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
2.241 + by (simp add: noteq_arrs_def get_array_def set_array_def)
2.242 +
2.243 +lemma set_array_same [simp]:
2.244 + "set_array r x (set_array r y h) = set_array r x h"
2.245 + by (simp add: set_array_def)
2.246 +
2.247 +lemma array_set_set_swap:
2.248 + "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
2.249 + by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
2.250 +
2.251 +lemma array_ref_set_set_swap:
2.252 + "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)"
2.253 + by (simp add: Let_def expand_fun_eq set_array_def set_ref_def)
2.254 +
2.255 +lemma get_array_upd_eq [simp]:
2.256 + "get_array a (upd a i v h) = (get_array a h) [i := v]"
2.257 + by (simp add: upd_def)
2.258 +
2.259 +lemma nth_upd_array_neq_array [simp]:
2.260 + "a =!!= b \<Longrightarrow> get_array a (upd b j v h) ! i = get_array a h ! i"
2.261 + by (simp add: upd_def noteq_arrs_def)
2.262 +
2.263 +lemma get_arry_array_upd_elem_neqIndex [simp]:
2.264 + "i \<noteq> j \<Longrightarrow> get_array a (upd a j v h) ! i = get_array a h ! i"
2.265 + by simp
2.266 +
2.267 +lemma length_upd_eq [simp]:
2.268 + "length a (upd a i v h) = length a h"
2.269 + by (simp add: length_def upd_def)
2.270 +
2.271 +lemma length_upd_neq [simp]:
2.272 + "length a (upd b i v h) = length a h"
2.273 + by (simp add: upd_def length_def set_array_def get_array_def)
2.274 +
2.275 +lemma upd_swap_neqArray:
2.276 + "a =!!= a' \<Longrightarrow>
2.277 + upd a i v (upd a' i' v' h)
2.278 + = upd a' i' v' (upd a i v h)"
2.279 +apply (unfold upd_def)
2.280 +apply simp
2.281 +apply (subst array_set_set_swap, assumption)
2.282 +apply (subst array_get_set_neq)
2.283 +apply (erule noteq_arrs_sym)
2.284 +apply (simp)
2.285 +done
2.286 +
2.287 +lemma upd_swap_neqIndex:
2.288 + "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> upd a i v (upd a i' v' h) = upd a i' v' (upd a i v h)"
2.289 +by (auto simp add: upd_def array_set_set_swap list_update_swap)
2.290 +
2.291 +lemma get_array_init_array_list:
2.292 + "get_array (fst (array_of_list ls h)) (snd (array_of_list ls' h)) = ls'"
2.293 + by (simp add: Let_def split_def array_of_list_def)
2.294 +
2.295 +lemma set_array:
2.296 + "set_array (fst (array_of_list ls h))
2.297 + new_ls (snd (array_of_list ls h))
2.298 + = snd (array_of_list new_ls h)"
2.299 + by (simp add: Let_def split_def array_of_list_def)
2.300 +
2.301 +lemma array_present_upd [simp]:
2.302 + "array_present a (upd b i v h) = array_present a h"
2.303 + by (simp add: upd_def array_present_def set_array_def get_array_def)
2.304 +
2.305 +lemma array_of_list_replicate:
2.306 + "array_of_list (replicate n x) = array n x"
2.307 + by (simp add: expand_fun_eq array_of_list_def array_def)
2.308 +
2.309 +
2.310 +text {* Properties of imperative references *}
2.311 +
2.312 +lemma next_ref_fresh [simp]:
2.313 + assumes "(r, h') = new_ref h"
2.314 + shows "\<not> ref_present r h"
2.315 + using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def)
2.316 +
2.317 +lemma next_ref_present [simp]:
2.318 + assumes "(r, h') = new_ref h"
2.319 + shows "ref_present r h'"
2.320 + using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def)
2.321 +
2.322 +lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
2.323 + by (simp add: get_ref_def set_ref_def)
2.324 +
2.325 +lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h"
2.326 + by (simp add: noteq_refs_def get_ref_def set_ref_def)
2.327 +
2.328 +(* FIXME: We need some infrastructure to infer that locally generated
2.329 + new refs (by new_ref(_no_init), new_array(')) are distinct
2.330 + from all existing refs.
2.331 +*)
2.332 +
2.333 +lemma ref_set_get: "set_ref r (get_ref r h) h = h"
2.334 +apply (simp add: set_ref_def get_ref_def)
2.335 +oops
2.336 +
2.337 +lemma set_ref_same[simp]:
2.338 + "set_ref r x (set_ref r y h) = set_ref r x h"
2.339 + by (simp add: set_ref_def)
2.340 +
2.341 +lemma ref_set_set_swap:
2.342 + "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)"
2.343 + by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
2.344 +
2.345 +lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
2.346 + by (simp add: ref_def new_ref_def set_ref_def Let_def)
2.347 +
2.348 +lemma ref_get_new [simp]:
2.349 + "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
2.350 + by (simp add: ref_def Let_def split_def)
2.351 +
2.352 +lemma ref_set_new [simp]:
2.353 + "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)"
2.354 + by (simp add: ref_def Let_def split_def)
2.355 +
2.356 +lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow>
2.357 + get_ref r (snd (ref v h)) = get_ref r h"
2.358 + by (simp add: get_ref_def set_ref_def ref_def Let_def new_ref_def noteq_refs_def)
2.359 +
2.360 +lemma lim_set_ref [simp]:
2.361 + "lim (set_ref r v h) = lim h"
2.362 + by (simp add: set_ref_def)
2.363 +
2.364 +lemma ref_present_new_ref [simp]:
2.365 + "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
2.366 + by (simp add: new_ref_def ref_present_def ref_def Let_def)
2.367 +
2.368 +lemma ref_present_set_ref [simp]:
2.369 + "ref_present r (set_ref r' v h) = ref_present r h"
2.370 + by (simp add: set_ref_def ref_present_def)
2.371 +
2.372 +lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
2.373 +unfolding array_ran_def Heap.length_def by simp
2.374 +
2.375 +lemma array_ran_upd_array_Some:
2.376 + assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)"
2.377 + shows "cl \<in> array_ran a h \<or> cl = b"
2.378 +proof -
2.379 + have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
2.380 + with assms show ?thesis
2.381 + unfolding array_ran_def Heap.upd_def by fastsimp
2.382 +qed
2.383 +
2.384 +lemma array_ran_upd_array_None:
2.385 + assumes "cl \<in> array_ran a (Heap.upd a i None h)"
2.386 + shows "cl \<in> array_ran a h"
2.387 +proof -
2.388 + have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
2.389 + with assms show ?thesis
2.390 + unfolding array_ran_def Heap.upd_def by auto
2.391 +qed
2.392 +
2.393 +
2.394 +text {* Non-interaction between imperative array and imperative references *}
2.395 +
2.396 +lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
2.397 + by (simp add: get_array_def set_ref_def)
2.398 +
2.399 +lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i"
2.400 + by simp
2.401 +
2.402 +lemma get_ref_upd [simp]: "get_ref r (upd a i v h) = get_ref r h"
2.403 + by (simp add: get_ref_def set_array_def upd_def)
2.404 +
2.405 +lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
2.406 + by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def new_ref_def)
2.407 +
2.408 +text {*not actually true ???*}
2.409 +lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
2.410 +apply (case_tac a)
2.411 +apply (simp add: Let_def upd_def)
2.412 +apply auto
2.413 +oops
2.414 +
2.415 +lemma length_new_ref[simp]:
2.416 + "length a (snd (ref v h)) = length a h"
2.417 + by (simp add: get_array_def set_ref_def length_def new_ref_def ref_def Let_def)
2.418 +
2.419 +lemma get_array_new_ref [simp]:
2.420 + "get_array a (snd (ref v h)) = get_array a h"
2.421 + by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def)
2.422 +
2.423 +lemma ref_present_upd [simp]:
2.424 + "ref_present r (upd a i v h) = ref_present r h"
2.425 + by (simp add: upd_def ref_present_def set_array_def get_array_def)
2.426 +
2.427 +lemma array_present_set_ref [simp]:
2.428 + "array_present a (set_ref r v h) = array_present a h"
2.429 + by (simp add: array_present_def set_ref_def)
2.430 +
2.431 +lemma array_present_new_ref [simp]:
2.432 + "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
2.433 + by (simp add: array_present_def new_ref_def ref_def Let_def)
2.434 +
2.435 +hide (open) const empty array array_of_list upd length ref
2.436 +
2.437 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jan 08 17:10:41 2009 +0100
3.3 @@ -0,0 +1,425 @@
3.4 +(* Title: HOL/Library/Heap_Monad.thy
3.5 + ID: $Id$
3.6 + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
3.7 +*)
3.8 +
3.9 +header {* A monad with a polymorphic heap *}
3.10 +
3.11 +theory Heap_Monad
3.12 +imports Heap
3.13 +begin
3.14 +
3.15 +subsection {* The monad *}
3.16 +
3.17 +subsubsection {* Monad combinators *}
3.18 +
3.19 +datatype exception = Exn
3.20 +
3.21 +text {* Monadic heap actions either produce values
3.22 + and transform the heap, or fail *}
3.23 +datatype 'a Heap = Heap "heap \<Rightarrow> ('a + exception) \<times> heap"
3.24 +
3.25 +primrec
3.26 + execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a + exception) \<times> heap" where
3.27 + "execute (Heap f) = f"
3.28 +lemmas [code del] = execute.simps
3.29 +
3.30 +lemma Heap_execute [simp]:
3.31 + "Heap (execute f) = f" by (cases f) simp_all
3.32 +
3.33 +lemma Heap_eqI:
3.34 + "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
3.35 + by (cases f, cases g) (auto simp: expand_fun_eq)
3.36 +
3.37 +lemma Heap_eqI':
3.38 + "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
3.39 + by (auto simp: expand_fun_eq intro: Heap_eqI)
3.40 +
3.41 +lemma Heap_strip: "(\<And>f. PROP P f) \<equiv> (\<And>g. PROP P (Heap g))"
3.42 +proof
3.43 + fix g :: "heap \<Rightarrow> ('a + exception) \<times> heap"
3.44 + assume "\<And>f. PROP P f"
3.45 + then show "PROP P (Heap g)" .
3.46 +next
3.47 + fix f :: "'a Heap"
3.48 + assume assm: "\<And>g. PROP P (Heap g)"
3.49 + then have "PROP P (Heap (execute f))" .
3.50 + then show "PROP P f" by simp
3.51 +qed
3.52 +
3.53 +definition
3.54 + heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
3.55 + [code del]: "heap f = Heap (\<lambda>h. apfst Inl (f h))"
3.56 +
3.57 +lemma execute_heap [simp]:
3.58 + "execute (heap f) h = apfst Inl (f h)"
3.59 + by (simp add: heap_def)
3.60 +
3.61 +definition
3.62 + bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
3.63 + [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
3.64 + (Inl x, h') \<Rightarrow> execute (g x) h'
3.65 + | r \<Rightarrow> r)"
3.66 +
3.67 +notation
3.68 + bindM (infixl "\<guillemotright>=" 54)
3.69 +
3.70 +abbreviation
3.71 + chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
3.72 + "f >> g \<equiv> f >>= (\<lambda>_. g)"
3.73 +
3.74 +notation
3.75 + chainM (infixl "\<guillemotright>" 54)
3.76 +
3.77 +definition
3.78 + return :: "'a \<Rightarrow> 'a Heap" where
3.79 + [code del]: "return x = heap (Pair x)"
3.80 +
3.81 +lemma execute_return [simp]:
3.82 + "execute (return x) h = apfst Inl (x, h)"
3.83 + by (simp add: return_def)
3.84 +
3.85 +definition
3.86 + raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
3.87 + [code del]: "raise s = Heap (Pair (Inr Exn))"
3.88 +
3.89 +notation (latex output)
3.90 + "raise" ("\<^raw:{\textsf{raise}}>")
3.91 +
3.92 +lemma execute_raise [simp]:
3.93 + "execute (raise s) h = (Inr Exn, h)"
3.94 + by (simp add: raise_def)
3.95 +
3.96 +
3.97 +subsubsection {* do-syntax *}
3.98 +
3.99 +text {*
3.100 + We provide a convenient do-notation for monadic expressions
3.101 + well-known from Haskell. @{const Let} is printed
3.102 + specially in do-expressions.
3.103 +*}
3.104 +
3.105 +nonterminals do_expr
3.106 +
3.107 +syntax
3.108 + "_do" :: "do_expr \<Rightarrow> 'a"
3.109 + ("(do (_)//done)" [12] 100)
3.110 + "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
3.111 + ("_ <- _;//_" [1000, 13, 12] 12)
3.112 + "_chainM" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
3.113 + ("_;//_" [13, 12] 12)
3.114 + "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
3.115 + ("let _ = _;//_" [1000, 13, 12] 12)
3.116 + "_nil" :: "'a \<Rightarrow> do_expr"
3.117 + ("_" [12] 12)
3.118 +
3.119 +syntax (xsymbols)
3.120 + "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
3.121 + ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
3.122 +syntax (latex output)
3.123 + "_do" :: "do_expr \<Rightarrow> 'a"
3.124 + ("(\<^raw:{\textsf{do}}> (_))" [12] 100)
3.125 + "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
3.126 + ("\<^raw:\textsf{let}> _ = _;//_" [1000, 13, 12] 12)
3.127 +notation (latex output)
3.128 + "return" ("\<^raw:{\textsf{return}}>")
3.129 +
3.130 +translations
3.131 + "_do f" => "f"
3.132 + "_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
3.133 + "_chainM f g" => "f \<guillemotright> g"
3.134 + "_let x t f" => "CONST Let t (\<lambda>x. f)"
3.135 + "_nil f" => "f"
3.136 +
3.137 +print_translation {*
3.138 +let
3.139 + fun dest_abs_eta (Abs (abs as (_, ty, _))) =
3.140 + let
3.141 + val (v, t) = Syntax.variant_abs abs;
3.142 + in (Free (v, ty), t) end
3.143 + | dest_abs_eta t =
3.144 + let
3.145 + val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
3.146 + in (Free (v, dummyT), t) end;
3.147 + fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =
3.148 + let
3.149 + val (v, g') = dest_abs_eta g;
3.150 + val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
3.151 + val v_used = fold_aterms
3.152 + (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
3.153 + in if v_used then
3.154 + Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
3.155 + else
3.156 + Const ("_chainM", dummyT) $ f $ unfold_monad g'
3.157 + end
3.158 + | unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) =
3.159 + Const ("_chainM", dummyT) $ f $ unfold_monad g
3.160 + | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
3.161 + let
3.162 + val (v, g') = dest_abs_eta g;
3.163 + in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
3.164 + | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
3.165 + Const (@{const_syntax return}, dummyT) $ f
3.166 + | unfold_monad f = f;
3.167 + fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true
3.168 + | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
3.169 + contains_bindM t;
3.170 + fun bindM_monad_tr' (f::g::ts) = list_comb
3.171 + (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
3.172 + fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
3.173 + (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
3.174 + else raise Match;
3.175 +in [
3.176 + (@{const_syntax bindM}, bindM_monad_tr'),
3.177 + (@{const_syntax Let}, Let_monad_tr')
3.178 +] end;
3.179 +*}
3.180 +
3.181 +
3.182 +subsection {* Monad properties *}
3.183 +
3.184 +subsubsection {* Monad laws *}
3.185 +
3.186 +lemma return_bind: "return x \<guillemotright>= f = f x"
3.187 + by (simp add: bindM_def return_def)
3.188 +
3.189 +lemma bind_return: "f \<guillemotright>= return = f"
3.190 +proof (rule Heap_eqI)
3.191 + fix h
3.192 + show "execute (f \<guillemotright>= return) h = execute f h"
3.193 + by (auto simp add: bindM_def return_def split: sum.splits prod.splits)
3.194 +qed
3.195 +
3.196 +lemma bind_bind: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
3.197 + by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)
3.198 +
3.199 +lemma bind_bind': "f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h x) = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= (\<lambda>y. return (x, y))) \<guillemotright>= (\<lambda>(x, y). h x y)"
3.200 + by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)
3.201 +
3.202 +lemma raise_bind: "raise e \<guillemotright>= f = raise e"
3.203 + by (simp add: raise_def bindM_def)
3.204 +
3.205 +
3.206 +lemmas monad_simp = return_bind bind_return bind_bind raise_bind
3.207 +
3.208 +
3.209 +subsection {* Generic combinators *}
3.210 +
3.211 +definition
3.212 + liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap"
3.213 +where
3.214 + "liftM f = return o f"
3.215 +
3.216 +definition
3.217 + compM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> ('b \<Rightarrow> 'c Heap) \<Rightarrow> 'a \<Rightarrow> 'c Heap" (infixl ">>==" 54)
3.218 +where
3.219 + "(f >>== g) = (\<lambda>x. f x \<guillemotright>= g)"
3.220 +
3.221 +notation
3.222 + compM (infixl "\<guillemotright>==" 54)
3.223 +
3.224 +lemma liftM_collapse: "liftM f x = return (f x)"
3.225 + by (simp add: liftM_def)
3.226 +
3.227 +lemma liftM_compM: "liftM f \<guillemotright>== g = g o f"
3.228 + by (auto intro: Heap_eqI' simp add: expand_fun_eq liftM_def compM_def bindM_def)
3.229 +
3.230 +lemma compM_return: "f \<guillemotright>== return = f"
3.231 + by (simp add: compM_def monad_simp)
3.232 +
3.233 +lemma compM_compM: "(f \<guillemotright>== g) \<guillemotright>== h = f \<guillemotright>== (g \<guillemotright>== h)"
3.234 + by (simp add: compM_def monad_simp)
3.235 +
3.236 +lemma liftM_bind:
3.237 + "(\<lambda>x. liftM f x \<guillemotright>= liftM g) = liftM (\<lambda>x. g (f x))"
3.238 + by (rule Heap_eqI') (simp add: monad_simp liftM_def bindM_def)
3.239 +
3.240 +lemma liftM_comp:
3.241 + "liftM f o g = liftM (f o g)"
3.242 + by (rule Heap_eqI') (simp add: liftM_def)
3.243 +
3.244 +lemmas monad_simp' = monad_simp liftM_compM compM_return
3.245 + compM_compM liftM_bind liftM_comp
3.246 +
3.247 +primrec
3.248 + mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap"
3.249 +where
3.250 + "mapM f [] = return []"
3.251 + | "mapM f (x#xs) = do y \<leftarrow> f x;
3.252 + ys \<leftarrow> mapM f xs;
3.253 + return (y # ys)
3.254 + done"
3.255 +
3.256 +primrec
3.257 + foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
3.258 +where
3.259 + "foldM f [] s = return s"
3.260 + | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
3.261 +
3.262 +definition
3.263 + assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
3.264 +where
3.265 + "assert P x = (if P x then return x else raise (''assert''))"
3.266 +
3.267 +lemma assert_cong [fundef_cong]:
3.268 + assumes "P = P'"
3.269 + assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
3.270 + shows "(assert P x >>= f) = (assert P' x >>= f')"
3.271 + using assms by (auto simp add: assert_def return_bind raise_bind)
3.272 +
3.273 +hide (open) const heap execute
3.274 +
3.275 +
3.276 +subsection {* Code generator setup *}
3.277 +
3.278 +subsubsection {* Logical intermediate layer *}
3.279 +
3.280 +definition
3.281 + Fail :: "message_string \<Rightarrow> exception"
3.282 +where
3.283 + [code del]: "Fail s = Exn"
3.284 +
3.285 +definition
3.286 + raise_exc :: "exception \<Rightarrow> 'a Heap"
3.287 +where
3.288 + [code del]: "raise_exc e = raise []"
3.289 +
3.290 +lemma raise_raise_exc [code, code inline]:
3.291 + "raise s = raise_exc (Fail (STR s))"
3.292 + unfolding Fail_def raise_exc_def raise_def ..
3.293 +
3.294 +hide (open) const Fail raise_exc
3.295 +
3.296 +
3.297 +subsubsection {* SML and OCaml *}
3.298 +
3.299 +code_type Heap (SML "unit/ ->/ _")
3.300 +code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
3.301 +code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
3.302 +code_const return (SML "!(fn/ ()/ =>/ _)")
3.303 +code_const "Heap_Monad.Fail" (SML "Fail")
3.304 +code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)")
3.305 +
3.306 +code_type Heap (OCaml "_")
3.307 +code_const Heap (OCaml "failwith/ \"bare Heap\"")
3.308 +code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
3.309 +code_const return (OCaml "!(fun/ ()/ ->/ _)")
3.310 +code_const "Heap_Monad.Fail" (OCaml "Failure")
3.311 +code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
3.312 +
3.313 +setup {* let
3.314 + open Code_Thingol;
3.315 +
3.316 + fun lookup naming = the o Code_Thingol.lookup_const naming;
3.317 +
3.318 + fun imp_monad_bind'' bind' return' unit' ts =
3.319 + let
3.320 + val dummy_name = "";
3.321 + val dummy_type = ITyVar dummy_name;
3.322 + val dummy_case_term = IVar dummy_name;
3.323 + (*assumption: dummy values are not relevant for serialization*)
3.324 + val unitt = IConst (unit', ([], []));
3.325 + fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
3.326 + | dest_abs (t, ty) =
3.327 + let
3.328 + val vs = Code_Thingol.fold_varnames cons t [];
3.329 + val v = Name.variant vs "x";
3.330 + val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
3.331 + in ((v, ty'), t `$ IVar v) end;
3.332 + fun force (t as IConst (c, _) `$ t') = if c = return'
3.333 + then t' else t `$ unitt
3.334 + | force t = t `$ unitt;
3.335 + fun tr_bind' [(t1, _), (t2, ty2)] =
3.336 + let
3.337 + val ((v, ty), t) = dest_abs (t2, ty2);
3.338 + in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
3.339 + and tr_bind'' t = case Code_Thingol.unfold_app t
3.340 + of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
3.341 + then tr_bind' [(x1, ty1), (x2, ty2)]
3.342 + else force t
3.343 + | _ => force t;
3.344 + in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
3.345 + [(unitt, tr_bind' ts)]), dummy_case_term) end
3.346 + and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
3.347 + of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
3.348 + | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
3.349 + | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
3.350 + else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
3.351 + and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
3.352 + | imp_monad_bind bind' return' unit' (t as IVar _) = t
3.353 + | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
3.354 + of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
3.355 + | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
3.356 + | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t
3.357 + | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
3.358 + (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
3.359 +
3.360 + fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
3.361 + (imp_monad_bind (lookup naming @{const_name bindM})
3.362 + (lookup naming @{const_name return})
3.363 + (lookup naming @{const_name Unity}));
3.364 +
3.365 +in
3.366 +
3.367 + Code_Target.extend_target ("SML_imp", ("SML", imp_program))
3.368 + #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
3.369 +
3.370 +end
3.371 +*}
3.372 +
3.373 +
3.374 +code_reserved OCaml Failure raise
3.375 +
3.376 +
3.377 +subsubsection {* Haskell *}
3.378 +
3.379 +text {* Adaption layer *}
3.380 +
3.381 +code_include Haskell "STMonad"
3.382 +{*import qualified Control.Monad;
3.383 +import qualified Control.Monad.ST;
3.384 +import qualified Data.STRef;
3.385 +import qualified Data.Array.ST;
3.386 +
3.387 +type RealWorld = Control.Monad.ST.RealWorld;
3.388 +type ST s a = Control.Monad.ST.ST s a;
3.389 +type STRef s a = Data.STRef.STRef s a;
3.390 +type STArray s a = Data.Array.ST.STArray s Int a;
3.391 +
3.392 +runST :: (forall s. ST s a) -> a;
3.393 +runST s = Control.Monad.ST.runST s;
3.394 +
3.395 +newSTRef = Data.STRef.newSTRef;
3.396 +readSTRef = Data.STRef.readSTRef;
3.397 +writeSTRef = Data.STRef.writeSTRef;
3.398 +
3.399 +newArray :: (Int, Int) -> a -> ST s (STArray s a);
3.400 +newArray = Data.Array.ST.newArray;
3.401 +
3.402 +newListArray :: (Int, Int) -> [a] -> ST s (STArray s a);
3.403 +newListArray = Data.Array.ST.newListArray;
3.404 +
3.405 +lengthArray :: STArray s a -> ST s Int;
3.406 +lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
3.407 +
3.408 +readArray :: STArray s a -> Int -> ST s a;
3.409 +readArray = Data.Array.ST.readArray;
3.410 +
3.411 +writeArray :: STArray s a -> Int -> a -> ST s ();
3.412 +writeArray = Data.Array.ST.writeArray;*}
3.413 +
3.414 +code_reserved Haskell RealWorld ST STRef Array
3.415 + runST
3.416 + newSTRef reasSTRef writeSTRef
3.417 + newArray newListArray lengthArray readArray writeArray
3.418 +
3.419 +text {* Monad *}
3.420 +
3.421 +code_type Heap (Haskell "ST/ RealWorld/ _")
3.422 +code_const Heap (Haskell "error/ \"bare Heap\"")
3.423 +code_monad "op \<guillemotright>=" Haskell
3.424 +code_const return (Haskell "return")
3.425 +code_const "Heap_Monad.Fail" (Haskell "_")
3.426 +code_const "Heap_Monad.raise_exc" (Haskell "error")
3.427 +
3.428 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy Thu Jan 08 17:10:41 2009 +0100
4.3 @@ -0,0 +1,12 @@
4.4 +(* Title: HOL/Library/Imperative_HOL.thy
4.5 + ID: $Id$
4.6 + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
4.7 +*)
4.8 +
4.9 +header {* Entry point into monadic imperative HOL *}
4.10 +
4.11 +theory Imperative_HOL
4.12 +imports Array Ref Relational
4.13 +begin
4.14 +
4.15 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Imperative_HOL/ROOT.ML Thu Jan 08 17:10:41 2009 +0100
5.3 @@ -0,0 +1,2 @@
5.4 +
5.5 +use_thy "Imperative_HOL";
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Imperative_HOL/Ref.thy Thu Jan 08 17:10:41 2009 +0100
6.3 @@ -0,0 +1,91 @@
6.4 +(* Title: HOL/Library/Ref.thy
6.5 + ID: $Id$
6.6 + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
6.7 +*)
6.8 +
6.9 +header {* Monadic references *}
6.10 +
6.11 +theory Ref
6.12 +imports Heap_Monad
6.13 +begin
6.14 +
6.15 +text {*
6.16 + Imperative reference operations; modeled after their ML counterparts.
6.17 + See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html
6.18 + and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
6.19 +*}
6.20 +
6.21 +subsection {* Primitives *}
6.22 +
6.23 +definition
6.24 + new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
6.25 + [code del]: "new v = Heap_Monad.heap (Heap.ref v)"
6.26 +
6.27 +definition
6.28 + lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
6.29 + [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get_ref r h, h))"
6.30 +
6.31 +definition
6.32 + update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where
6.33 + [code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))"
6.34 +
6.35 +
6.36 +subsection {* Derivates *}
6.37 +
6.38 +definition
6.39 + change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap"
6.40 +where
6.41 + "change f r = (do x \<leftarrow> ! r;
6.42 + let y = f x;
6.43 + r := y;
6.44 + return y
6.45 + done)"
6.46 +
6.47 +hide (open) const new lookup update change
6.48 +
6.49 +
6.50 +subsection {* Properties *}
6.51 +
6.52 +lemma lookup_chain:
6.53 + "(!r \<guillemotright> f) = f"
6.54 + by (cases f)
6.55 + (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
6.56 +
6.57 +lemma update_change [code]:
6.58 + "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
6.59 + by (auto simp add: monad_simp change_def lookup_chain)
6.60 +
6.61 +
6.62 +subsection {* Code generator setup *}
6.63 +
6.64 +subsubsection {* SML *}
6.65 +
6.66 +code_type ref (SML "_/ ref")
6.67 +code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
6.68 +code_const Ref.new (SML "(fn/ ()/ =>/ ref/ _)")
6.69 +code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
6.70 +code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
6.71 +
6.72 +code_reserved SML ref
6.73 +
6.74 +
6.75 +subsubsection {* OCaml *}
6.76 +
6.77 +code_type ref (OCaml "_/ ref")
6.78 +code_const Ref (OCaml "failwith/ \"bare Ref\")")
6.79 +code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)")
6.80 +code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
6.81 +code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
6.82 +
6.83 +code_reserved OCaml ref
6.84 +
6.85 +
6.86 +subsubsection {* Haskell *}
6.87 +
6.88 +code_type ref (Haskell "STRef/ RealWorld/ _")
6.89 +code_const Ref (Haskell "error/ \"bare Ref\"")
6.90 +code_const Ref.new (Haskell "newSTRef")
6.91 +code_const Ref.lookup (Haskell "readSTRef")
6.92 +code_const Ref.update (Haskell "writeSTRef")
6.93 +
6.94 +end
6.95 \ No newline at end of file
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Imperative_HOL/Relational.thy Thu Jan 08 17:10:41 2009 +0100
7.3 @@ -0,0 +1,700 @@
7.4 +theory Relational
7.5 +imports Array Ref
7.6 +begin
7.7 +
7.8 +section{* Definition of the Relational framework *}
7.9 +
7.10 +text {* The crel predicate states that when a computation c runs with the heap h
7.11 + will result in return value r and a heap h' (if no exception occurs). *}
7.12 +
7.13 +definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
7.14 +where
7.15 + crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = (Inl r, h')"
7.16 +
7.17 +lemma crel_def: -- FIXME
7.18 + "crel c h h' r \<longleftrightarrow> (Inl r, h') = Heap_Monad.execute c h"
7.19 + unfolding crel_def' by auto
7.20 +
7.21 +lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
7.22 +unfolding crel_def' by auto
7.23 +
7.24 +section {* Elimination rules *}
7.25 +
7.26 +text {* For all commands, we define simple elimination rules. *}
7.27 +(* FIXME: consumes 1 necessary ?? *)
7.28 +
7.29 +subsection {* Elimination rules for basic monadic commands *}
7.30 +
7.31 +lemma crelE[consumes 1]:
7.32 + assumes "crel (f >>= g) h h'' r'"
7.33 + obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
7.34 + using assms
7.35 + by (auto simp add: crel_def bindM_def Let_def prod_case_beta split_def Pair_fst_snd_eq split add: sum.split_asm)
7.36 +
7.37 +lemma crelE'[consumes 1]:
7.38 + assumes "crel (f >> g) h h'' r'"
7.39 + obtains h' r where "crel f h h' r" "crel g h' h'' r'"
7.40 + using assms
7.41 + by (elim crelE) auto
7.42 +
7.43 +lemma crel_return[consumes 1]:
7.44 + assumes "crel (return x) h h' r"
7.45 + obtains "r = x" "h = h'"
7.46 + using assms
7.47 + unfolding crel_def return_def by simp
7.48 +
7.49 +lemma crel_raise[consumes 1]:
7.50 + assumes "crel (raise x) h h' r"
7.51 + obtains "False"
7.52 + using assms
7.53 + unfolding crel_def raise_def by simp
7.54 +
7.55 +lemma crel_if:
7.56 + assumes "crel (if c then t else e) h h' r"
7.57 + obtains "c" "crel t h h' r"
7.58 + | "\<not>c" "crel e h h' r"
7.59 + using assms
7.60 + unfolding crel_def by auto
7.61 +
7.62 +lemma crel_option_case:
7.63 + assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
7.64 + obtains "x = None" "crel n h h' r"
7.65 + | y where "x = Some y" "crel (s y) h h' r"
7.66 + using assms
7.67 + unfolding crel_def by auto
7.68 +
7.69 +lemma crel_mapM:
7.70 + assumes "crel (mapM f xs) h h' r"
7.71 + assumes "\<And>h h'. P f [] h h' []"
7.72 + assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (mapM f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
7.73 + shows "P f xs h h' r"
7.74 +using assms(1)
7.75 +proof (induct xs arbitrary: h h' r)
7.76 + case Nil with assms(2) show ?case
7.77 + by (auto elim: crel_return)
7.78 +next
7.79 + case (Cons x xs)
7.80 + from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
7.81 + and crel_mapM: "crel (mapM f xs) h1 h' ys"
7.82 + and r_def: "r = y#ys"
7.83 + unfolding mapM.simps
7.84 + by (auto elim!: crelE crel_return)
7.85 + from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
7.86 + show ?case by auto
7.87 +qed
7.88 +
7.89 +lemma crel_heap:
7.90 + assumes "crel (Heap_Monad.heap f) h h' r"
7.91 + obtains "h' = snd (f h)" "r = fst (f h)"
7.92 + using assms
7.93 + unfolding heap_def crel_def apfst_def split_def prod_fun_def by simp_all
7.94 +
7.95 +subsection {* Elimination rules for array commands *}
7.96 +
7.97 +lemma crel_length:
7.98 + assumes "crel (length a) h h' r"
7.99 + obtains "h = h'" "r = Heap.length a h'"
7.100 + using assms
7.101 + unfolding length_def
7.102 + by (elim crel_heap) simp
7.103 +
7.104 +(* Strong version of the lemma for this operation is missing *)
7.105 +lemma crel_new_weak:
7.106 + assumes "crel (Array.new n v) h h' r"
7.107 + obtains "get_array r h' = List.replicate n v"
7.108 + using assms unfolding Array.new_def
7.109 + by (elim crel_heap) (auto simp:Heap.array_def Let_def split_def)
7.110 +
7.111 +lemma crel_nth[consumes 1]:
7.112 + assumes "crel (nth a i) h h' r"
7.113 + obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
7.114 + using assms
7.115 + unfolding nth_def
7.116 + by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
7.117 +
7.118 +lemma crel_upd[consumes 1]:
7.119 + assumes "crel (upd i v a) h h' r"
7.120 + obtains "r = a" "h' = Heap.upd a i v h"
7.121 + using assms
7.122 + unfolding upd_def
7.123 + by (elim crelE crel_if crel_return crel_raise
7.124 + crel_length crel_heap) auto
7.125 +
7.126 +(* Strong version of the lemma for this operation is missing *)
7.127 +lemma crel_of_list_weak:
7.128 + assumes "crel (Array.of_list xs) h h' r"
7.129 + obtains "get_array r h' = xs"
7.130 + using assms
7.131 + unfolding of_list_def
7.132 + by (elim crel_heap) (simp add:get_array_init_array_list)
7.133 +
7.134 +lemma crel_map_entry:
7.135 + assumes "crel (Array.map_entry i f a) h h' r"
7.136 + obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
7.137 + using assms
7.138 + unfolding Array.map_entry_def
7.139 + by (elim crelE crel_upd crel_nth) auto
7.140 +
7.141 +lemma crel_swap:
7.142 + assumes "crel (Array.swap i x a) h h' r"
7.143 + obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
7.144 + using assms
7.145 + unfolding Array.swap_def
7.146 + by (elim crelE crel_upd crel_nth crel_return) auto
7.147 +
7.148 +(* Strong version of the lemma for this operation is missing *)
7.149 +lemma crel_make_weak:
7.150 + assumes "crel (Array.make n f) h h' r"
7.151 + obtains "i < n \<Longrightarrow> get_array r h' ! i = f i"
7.152 + using assms
7.153 + unfolding Array.make_def
7.154 + by (elim crel_of_list_weak) auto
7.155 +
7.156 +lemma upt_conv_Cons':
7.157 + assumes "Suc a \<le> b"
7.158 + shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
7.159 +proof -
7.160 + from assms have l: "b - Suc a < b" by arith
7.161 + from assms have "Suc (b - Suc a) = b - a" by arith
7.162 + with l show ?thesis by (simp add: upt_conv_Cons)
7.163 +qed
7.164 +
7.165 +lemma crel_mapM_nth:
7.166 + assumes
7.167 + "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' xs"
7.168 + assumes "n \<le> Heap.length a h"
7.169 + shows "h = h' \<and> xs = drop (Heap.length a h - n) (get_array a h)"
7.170 +using assms
7.171 +proof (induct n arbitrary: xs h h')
7.172 + case 0 thus ?case
7.173 + by (auto elim!: crel_return simp add: Heap.length_def)
7.174 +next
7.175 + case (Suc n)
7.176 + from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
7.177 + by (simp add: upt_conv_Cons')
7.178 + with Suc(2) obtain r where
7.179 + crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
7.180 + and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
7.181 + by (auto elim!: crelE crel_nth crel_return)
7.182 + from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)"
7.183 + by arith
7.184 + with Suc.hyps[OF crel_mapM] xs_def show ?case
7.185 + unfolding Heap.length_def
7.186 + by (auto simp add: nth_drop')
7.187 +qed
7.188 +
7.189 +lemma crel_freeze:
7.190 + assumes "crel (Array.freeze a) h h' xs"
7.191 + obtains "h = h'" "xs = get_array a h"
7.192 +proof
7.193 + from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
7.194 + unfolding freeze_def
7.195 + by (auto elim: crelE crel_length)
7.196 + hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
7.197 + by simp
7.198 + from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
7.199 +qed
7.200 +
7.201 +lemma crel_mapM_map_entry_remains:
7.202 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
7.203 + assumes "i < Heap.length a h - n"
7.204 + shows "get_array a h ! i = get_array a h' ! i"
7.205 +using assms
7.206 +proof (induct n arbitrary: h h' r)
7.207 + case 0
7.208 + thus ?case
7.209 + by (auto elim: crel_return)
7.210 +next
7.211 + case (Suc n)
7.212 + let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
7.213 + from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
7.214 + by (simp add: upt_conv_Cons')
7.215 + from Suc(2) this obtain r where
7.216 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
7.217 + by (auto simp add: elim!: crelE crel_map_entry crel_return)
7.218 + have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
7.219 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
7.220 + by simp
7.221 + from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
7.222 +qed
7.223 +
7.224 +lemma crel_mapM_map_entry_changes:
7.225 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
7.226 + assumes "n \<le> Heap.length a h"
7.227 + assumes "i \<ge> Heap.length a h - n"
7.228 + assumes "i < Heap.length a h"
7.229 + shows "get_array a h' ! i = f (get_array a h ! i)"
7.230 +using assms
7.231 +proof (induct n arbitrary: h h' r)
7.232 + case 0
7.233 + thus ?case
7.234 + by (auto elim!: crel_return)
7.235 +next
7.236 + case (Suc n)
7.237 + let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
7.238 + from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
7.239 + by (simp add: upt_conv_Cons')
7.240 + from Suc(2) this obtain r where
7.241 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
7.242 + by (auto simp add: elim!: crelE crel_map_entry crel_return)
7.243 + have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
7.244 + from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
7.245 + from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
7.246 + from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
7.247 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
7.248 + by simp
7.249 + from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
7.250 + crel_mapM_map_entry_remains[OF this, of "Heap.length a h - Suc n", symmetric] less less2
7.251 + show ?case
7.252 + by (auto simp add: nth_list_update_eq Heap.length_def)
7.253 +qed
7.254 +
7.255 +lemma crel_mapM_map_entry_length:
7.256 + assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
7.257 + assumes "n \<le> Heap.length a h"
7.258 + shows "Heap.length a h' = Heap.length a h"
7.259 +using assms
7.260 +proof (induct n arbitrary: h h' r)
7.261 + case 0
7.262 + thus ?case by (auto elim!: crel_return)
7.263 +next
7.264 + case (Suc n)
7.265 + let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
7.266 + from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
7.267 + by (simp add: upt_conv_Cons')
7.268 + from Suc(2) this obtain r where
7.269 + crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
7.270 + by (auto elim!: crelE crel_map_entry crel_return)
7.271 + have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
7.272 + from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
7.273 + by simp
7.274 + from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
7.275 +qed
7.276 +
7.277 +lemma crel_mapM_map_entry:
7.278 +assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Heap.length a h]) h h' r"
7.279 + shows "get_array a h' = List.map f (get_array a h)"
7.280 +proof -
7.281 + from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - Heap.length a h..<Heap.length a h]) h h' r" by simp
7.282 + from crel_mapM_map_entry_length[OF this]
7.283 + crel_mapM_map_entry_changes[OF this] show ?thesis
7.284 + unfolding Heap.length_def
7.285 + by (auto intro: nth_equalityI)
7.286 +qed
7.287 +
7.288 +lemma crel_map_weak:
7.289 + assumes crel_map: "crel (Array.map f a) h h' r"
7.290 + obtains "r = a" "get_array a h' = List.map f (get_array a h)"
7.291 +proof
7.292 + from assms crel_mapM_map_entry show "get_array a h' = List.map f (get_array a h)"
7.293 + unfolding Array.map_def
7.294 + by (fastsimp elim!: crelE crel_length crel_return)
7.295 + from assms show "r = a"
7.296 + unfolding Array.map_def
7.297 + by (elim crelE crel_return)
7.298 +qed
7.299 +
7.300 +subsection {* Elimination rules for reference commands *}
7.301 +
7.302 +(* TODO:
7.303 +maybe introduce a new predicate "extends h' h x"
7.304 +which means h' extends h with a new reference x.
7.305 +Then crel_new: would be
7.306 +assumes "crel (Ref.new v) h h' x"
7.307 +obtains "get_ref x h' = v"
7.308 +and "extends h' h x"
7.309 +
7.310 +and we would need further rules for extends:
7.311 +extends h' h x \<Longrightarrow> \<not> ref_present x h
7.312 +extends h' h x \<Longrightarrow> ref_present x h'
7.313 +extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> ref_present y h'
7.314 +extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> get_ref y h = get_ref y h'
7.315 +extends h' h x \<Longrightarrow> lim h' = Suc (lim h)
7.316 +*)
7.317 +
7.318 +lemma crel_Ref_new:
7.319 + assumes "crel (Ref.new v) h h' x"
7.320 + obtains "get_ref x h' = v"
7.321 + and "\<not> ref_present x h"
7.322 + and "ref_present x h'"
7.323 + and "\<forall>y. ref_present y h \<longrightarrow> get_ref y h = get_ref y h'"
7.324 + (* and "lim h' = Suc (lim h)" *)
7.325 + and "\<forall>y. ref_present y h \<longrightarrow> ref_present y h'"
7.326 + using assms
7.327 + unfolding Ref.new_def
7.328 + apply (elim crel_heap)
7.329 + unfolding Heap.ref_def
7.330 + apply (simp add: Let_def)
7.331 + unfolding Heap.new_ref_def
7.332 + apply (simp add: Let_def)
7.333 + unfolding ref_present_def
7.334 + apply auto
7.335 + unfolding get_ref_def set_ref_def
7.336 + apply auto
7.337 + done
7.338 +
7.339 +lemma crel_lookup:
7.340 + assumes "crel (!ref) h h' r"
7.341 + obtains "h = h'" "r = get_ref ref h"
7.342 +using assms
7.343 +unfolding Ref.lookup_def
7.344 +by (auto elim: crel_heap)
7.345 +
7.346 +lemma crel_update:
7.347 + assumes "crel (ref := v) h h' r"
7.348 + obtains "h' = set_ref ref v h" "r = ()"
7.349 +using assms
7.350 +unfolding Ref.update_def
7.351 +by (auto elim: crel_heap)
7.352 +
7.353 +lemma crel_change:
7.354 + assumes "crel (Ref.change f ref) h h' r"
7.355 + obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
7.356 +using assms
7.357 +unfolding Ref.change_def Let_def
7.358 +by (auto elim!: crelE crel_lookup crel_update crel_return)
7.359 +
7.360 +subsection {* Elimination rules for the assert command *}
7.361 +
7.362 +lemma crel_assert[consumes 1]:
7.363 + assumes "crel (assert P x) h h' r"
7.364 + obtains "P x" "r = x" "h = h'"
7.365 + using assms
7.366 + unfolding assert_def
7.367 + by (elim crel_if crel_return crel_raise) auto
7.368 +
7.369 +lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
7.370 +unfolding crel_def bindM_def Let_def assert_def
7.371 + raise_def return_def prod_case_beta
7.372 +apply (cases f)
7.373 +apply simp
7.374 +apply (simp add: expand_fun_eq split_def)
7.375 +apply auto
7.376 +apply (case_tac "fst (fun x)")
7.377 +apply (simp_all add: Pair_fst_snd_eq)
7.378 +apply (erule_tac x="x" in meta_allE)
7.379 +apply fastsimp
7.380 +done
7.381 +
7.382 +section {* Introduction rules *}
7.383 +
7.384 +subsection {* Introduction rules for basic monadic commands *}
7.385 +
7.386 +lemma crelI:
7.387 + assumes "crel f h h' r" "crel (g r) h' h'' r'"
7.388 + shows "crel (f >>= g) h h'' r'"
7.389 + using assms by (simp add: crel_def' bindM_def)
7.390 +
7.391 +lemma crelI':
7.392 + assumes "crel f h h' r" "crel g h' h'' r'"
7.393 + shows "crel (f >> g) h h'' r'"
7.394 + using assms by (intro crelI) auto
7.395 +
7.396 +lemma crel_returnI:
7.397 + shows "crel (return x) h h x"
7.398 + unfolding crel_def return_def by simp
7.399 +
7.400 +lemma crel_raiseI:
7.401 + shows "\<not> (crel (raise x) h h' r)"
7.402 + unfolding crel_def raise_def by simp
7.403 +
7.404 +lemma crel_ifI:
7.405 + assumes "c \<longrightarrow> crel t h h' r"
7.406 + "\<not>c \<longrightarrow> crel e h h' r"
7.407 + shows "crel (if c then t else e) h h' r"
7.408 + using assms
7.409 + unfolding crel_def by auto
7.410 +
7.411 +lemma crel_option_caseI:
7.412 + assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
7.413 + assumes "x = None \<Longrightarrow> crel n h h' r"
7.414 + shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
7.415 +using assms
7.416 +by (auto split: option.split)
7.417 +
7.418 +lemma crel_heapI:
7.419 + shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
7.420 + by (simp add: crel_def apfst_def split_def prod_fun_def)
7.421 +
7.422 +lemma crel_heapI':
7.423 + assumes "h' = snd (f h)" "r = fst (f h)"
7.424 + shows "crel (Heap_Monad.heap f) h h' r"
7.425 + using assms
7.426 + by (simp add: crel_def split_def apfst_def prod_fun_def)
7.427 +
7.428 +lemma crelI2:
7.429 + assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
7.430 + shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
7.431 + oops
7.432 +
7.433 +lemma crel_ifI2:
7.434 + assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
7.435 + "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
7.436 + shows "\<exists> h' r. crel (if c then t else e) h h' r"
7.437 + oops
7.438 +
7.439 +subsection {* Introduction rules for array commands *}
7.440 +
7.441 +lemma crel_lengthI:
7.442 + shows "crel (length a) h h (Heap.length a h)"
7.443 + unfolding length_def
7.444 + by (rule crel_heapI') auto
7.445 +
7.446 +(* thm crel_newI for Array.new is missing *)
7.447 +
7.448 +lemma crel_nthI:
7.449 + assumes "i < Heap.length a h"
7.450 + shows "crel (nth a i) h h ((get_array a h) ! i)"
7.451 + using assms
7.452 + unfolding nth_def
7.453 + by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
7.454 +
7.455 +lemma crel_updI:
7.456 + assumes "i < Heap.length a h"
7.457 + shows "crel (upd i v a) h (Heap.upd a i v h) a"
7.458 + using assms
7.459 + unfolding upd_def
7.460 + by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
7.461 + crel_lengthI crel_heapI')
7.462 +
7.463 +(* thm crel_of_listI is missing *)
7.464 +
7.465 +(* thm crel_map_entryI is missing *)
7.466 +
7.467 +(* thm crel_swapI is missing *)
7.468 +
7.469 +(* thm crel_makeI is missing *)
7.470 +
7.471 +(* thm crel_freezeI is missing *)
7.472 +
7.473 +(* thm crel_mapI is missing *)
7.474 +
7.475 +subsection {* Introduction rules for reference commands *}
7.476 +
7.477 +lemma crel_lookupI:
7.478 + shows "crel (!ref) h h (get_ref ref h)"
7.479 + unfolding lookup_def by (auto intro!: crel_heapI')
7.480 +
7.481 +lemma crel_updateI:
7.482 + shows "crel (ref := v) h (set_ref ref v h) ()"
7.483 + unfolding update_def by (auto intro!: crel_heapI')
7.484 +
7.485 +lemma crel_changeI:
7.486 + shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
7.487 +unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
7.488 +
7.489 +subsection {* Introduction rules for the assert command *}
7.490 +
7.491 +lemma crel_assertI:
7.492 + assumes "P x"
7.493 + shows "crel (assert P x) h h x"
7.494 + using assms
7.495 + unfolding assert_def
7.496 + by (auto intro!: crel_ifI crel_returnI crel_raiseI)
7.497 +
7.498 +section {* Defintion of the noError predicate *}
7.499 +
7.500 +text {* We add a simple definitional setting for crel intro rules
7.501 + where we only would like to show that the computation does not result in a exception for heap h,
7.502 + but we do not care about statements about the resulting heap and return value.*}
7.503 +
7.504 +definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
7.505 +where
7.506 + "noError c h \<longleftrightarrow> (\<exists>r h'. (Inl r, h') = Heap_Monad.execute c h)"
7.507 +
7.508 +lemma noError_def': -- FIXME
7.509 + "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = (Inl r, h'))"
7.510 + unfolding noError_def apply auto proof -
7.511 + fix r h'
7.512 + assume "(Inl r, h') = Heap_Monad.execute c h"
7.513 + then have "Heap_Monad.execute c h = (Inl r, h')" ..
7.514 + then show "\<exists>r h'. Heap_Monad.execute c h = (Inl r, h')" by blast
7.515 +qed
7.516 +
7.517 +subsection {* Introduction rules for basic monadic commands *}
7.518 +
7.519 +lemma noErrorI:
7.520 + assumes "noError f h"
7.521 + assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
7.522 + shows "noError (f \<guillemotright>= g) h"
7.523 + using assms
7.524 + by (auto simp add: noError_def' crel_def' bindM_def)
7.525 +
7.526 +lemma noErrorI':
7.527 + assumes "noError f h"
7.528 + assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
7.529 + shows "noError (f \<guillemotright> g) h"
7.530 + using assms
7.531 + by (auto simp add: noError_def' crel_def' bindM_def)
7.532 +
7.533 +lemma noErrorI2:
7.534 +"\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
7.535 +\<Longrightarrow> noError (f \<guillemotright>= g) h"
7.536 +by (auto simp add: noError_def' crel_def' bindM_def)
7.537 +
7.538 +lemma noError_return:
7.539 + shows "noError (return x) h"
7.540 + unfolding noError_def return_def
7.541 + by auto
7.542 +
7.543 +lemma noError_if:
7.544 + assumes "c \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
7.545 + shows "noError (if c then t else e) h"
7.546 + using assms
7.547 + unfolding noError_def
7.548 + by auto
7.549 +
7.550 +lemma noError_option_case:
7.551 + assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
7.552 + assumes "noError n h"
7.553 + shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
7.554 +using assms
7.555 +by (auto split: option.split)
7.556 +
7.557 +lemma noError_mapM:
7.558 +assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)"
7.559 +shows "noError (mapM f xs) h"
7.560 +using assms
7.561 +proof (induct xs)
7.562 + case Nil
7.563 + thus ?case
7.564 + unfolding mapM.simps by (intro noError_return)
7.565 +next
7.566 + case (Cons x xs)
7.567 + thus ?case
7.568 + unfolding mapM.simps
7.569 + by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
7.570 +qed
7.571 +
7.572 +lemma noError_heap:
7.573 + shows "noError (Heap_Monad.heap f) h"
7.574 + by (simp add: noError_def' apfst_def prod_fun_def split_def)
7.575 +
7.576 +subsection {* Introduction rules for array commands *}
7.577 +
7.578 +lemma noError_length:
7.579 + shows "noError (Array.length a) h"
7.580 + unfolding length_def
7.581 + by (intro noError_heap)
7.582 +
7.583 +lemma noError_new:
7.584 + shows "noError (Array.new n v) h"
7.585 +unfolding Array.new_def by (intro noError_heap)
7.586 +
7.587 +lemma noError_upd:
7.588 + assumes "i < Heap.length a h"
7.589 + shows "noError (Array.upd i v a) h"
7.590 + using assms
7.591 + unfolding upd_def
7.592 + by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
7.593 +
7.594 +lemma noError_nth:
7.595 +assumes "i < Heap.length a h"
7.596 + shows "noError (Array.nth a i) h"
7.597 + using assms
7.598 + unfolding nth_def
7.599 + by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
7.600 +
7.601 +lemma noError_of_list:
7.602 + shows "noError (of_list ls) h"
7.603 + unfolding of_list_def by (rule noError_heap)
7.604 +
7.605 +lemma noError_map_entry:
7.606 + assumes "i < Heap.length a h"
7.607 + shows "noError (map_entry i f a) h"
7.608 + using assms
7.609 + unfolding map_entry_def
7.610 + by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
7.611 +
7.612 +lemma noError_swap:
7.613 + assumes "i < Heap.length a h"
7.614 + shows "noError (swap i x a) h"
7.615 + using assms
7.616 + unfolding swap_def
7.617 + by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
7.618 +
7.619 +lemma noError_make:
7.620 + shows "noError (make n f) h"
7.621 + unfolding make_def
7.622 + by (auto intro: noError_of_list)
7.623 +
7.624 +(*TODO: move to HeapMonad *)
7.625 +lemma mapM_append:
7.626 + "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
7.627 + by (induct xs) (simp_all add: monad_simp)
7.628 +
7.629 +lemma noError_freeze:
7.630 + shows "noError (freeze a) h"
7.631 +unfolding freeze_def
7.632 +by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
7.633 + noError_nth crel_nthI elim: crel_length)
7.634 +
7.635 +lemma noError_mapM_map_entry:
7.636 + assumes "n \<le> Heap.length a h"
7.637 + shows "noError (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h"
7.638 +using assms
7.639 +proof (induct n arbitrary: h)
7.640 + case 0
7.641 + thus ?case by (auto intro: noError_return)
7.642 +next
7.643 + case (Suc n)
7.644 + from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
7.645 + by (simp add: upt_conv_Cons')
7.646 + with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
7.647 + by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
7.648 +qed
7.649 +
7.650 +lemma noError_map:
7.651 + shows "noError (Array.map f a) h"
7.652 +using noError_mapM_map_entry[of "Heap.length a h" a h]
7.653 +unfolding Array.map_def
7.654 +by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
7.655 +
7.656 +subsection {* Introduction rules for the reference commands *}
7.657 +
7.658 +lemma noError_Ref_new:
7.659 + shows "noError (Ref.new v) h"
7.660 +unfolding Ref.new_def by (intro noError_heap)
7.661 +
7.662 +lemma noError_lookup:
7.663 + shows "noError (!ref) h"
7.664 + unfolding lookup_def by (intro noError_heap)
7.665 +
7.666 +lemma noError_update:
7.667 + shows "noError (ref := v) h"
7.668 + unfolding update_def by (intro noError_heap)
7.669 +
7.670 +lemma noError_change:
7.671 + shows "noError (Ref.change f ref) h"
7.672 + unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
7.673 +
7.674 +subsection {* Introduction rules for the assert command *}
7.675 +
7.676 +lemma noError_assert:
7.677 + assumes "P x"
7.678 + shows "noError (assert P x) h"
7.679 + using assms
7.680 + unfolding assert_def
7.681 + by (auto intro: noError_if noError_return)
7.682 +
7.683 +section {* Cumulative lemmas *}
7.684 +
7.685 +lemmas crel_elim_all =
7.686 + crelE crelE' crel_return crel_raise crel_if crel_option_case
7.687 + crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze crel_map_weak
7.688 + crel_Ref_new crel_lookup crel_update crel_change
7.689 + crel_assert
7.690 +
7.691 +lemmas crel_intro_all =
7.692 + crelI crelI' crel_returnI crel_raiseI crel_ifI crel_option_caseI
7.693 + crel_lengthI (* crel_newI *) crel_nthI crel_updI (* crel_of_listI crel_map_entryI crel_swapI crel_makeI crel_freezeI crel_mapI *)
7.694 + (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
7.695 + crel_assert
7.696 +
7.697 +lemmas noError_intro_all =
7.698 + noErrorI noErrorI' noError_return noError_if noError_option_case
7.699 + noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze noError_map
7.700 + noError_Ref_new noError_lookup noError_update noError_change
7.701 + noError_assert
7.702 +
7.703 +end
7.704 \ No newline at end of file
8.1 --- a/src/HOL/IsaMakefile Thu Jan 08 10:53:48 2009 +0100
8.2 +++ b/src/HOL/IsaMakefile Thu Jan 08 17:10:41 2009 +0100
8.3 @@ -23,6 +23,7 @@
8.4 HOL-IMP \
8.5 HOL-IMPP \
8.6 HOL-IOA \
8.7 + HOL-Imperative_HOL \
8.8 HOL-Induct \
8.9 HOL-Isar_examples \
8.10 HOL-Lambda \
8.11 @@ -325,9 +326,7 @@
8.12 Library/Code_Char_chr.thy Library/Code_Integer.thy \
8.13 Library/Numeral_Type.thy \
8.14 Library/Boolean_Algebra.thy Library/Countable.thy \
8.15 - Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy \
8.16 - Library/Relational.thy Library/Sublist.thy Library/Subarray.thy \
8.17 - Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy \
8.18 + Library/RBT.thy \
8.19 Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
8.20 @cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
8.21
8.22 @@ -625,6 +624,17 @@
8.23 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck
8.24
8.25
8.26 +## HOL-Imperative_HOL
8.27 +
8.28 +HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
8.29 +
8.30 +$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \
8.31 + Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \
8.32 + Imperative_HOL/Relational.thy \
8.33 + Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy
8.34 + @$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
8.35 +
8.36 +
8.37 ## HOL-SizeChange
8.38
8.39 HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
8.40 @@ -796,8 +806,9 @@
8.41 ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
8.42 ex/Reflected_Presburger.thy ex/coopertac.ML \
8.43 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
8.44 - ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy \
8.45 - ex/Unification.thy ex/document/root.bib \
8.46 + ex/Subarray.thy ex/Sublist.thy \
8.47 + ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Term_Of_Syntax.thy \
8.48 + ex/Unification.thy ex/document/root.bib \
8.49 ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy \
8.50 ex/svc_funcs.ML ex/svc_test.thy \
8.51 ex/ImperativeQuicksort.thy \
9.1 --- a/src/HOL/Library/Array.thy Thu Jan 08 10:53:48 2009 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,209 +0,0 @@
9.4 -(* Title: HOL/Library/Array.thy
9.5 - ID: $Id$
9.6 - Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
9.7 -*)
9.8 -
9.9 -header {* Monadic arrays *}
9.10 -
9.11 -theory Array
9.12 -imports Heap_Monad Code_Index
9.13 -begin
9.14 -
9.15 -subsection {* Primitives *}
9.16 -
9.17 -definition
9.18 - new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
9.19 - [code del]: "new n x = Heap_Monad.heap (Heap.array n x)"
9.20 -
9.21 -definition
9.22 - of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
9.23 - [code del]: "of_list xs = Heap_Monad.heap (Heap.array_of_list xs)"
9.24 -
9.25 -definition
9.26 - length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
9.27 - [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
9.28 -
9.29 -definition
9.30 - nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
9.31 -where
9.32 - [code del]: "nth a i = (do len \<leftarrow> length a;
9.33 - (if i < len
9.34 - then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
9.35 - else raise (''array lookup: index out of range''))
9.36 - done)"
9.37 -
9.38 --- {* FIXME adjustion for List theory *}
9.39 -no_syntax
9.40 - nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
9.41 -
9.42 -abbreviation
9.43 - nth_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
9.44 -where
9.45 - "nth_list \<equiv> List.nth"
9.46 -
9.47 -definition
9.48 - upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
9.49 -where
9.50 - [code del]: "upd i x a = (do len \<leftarrow> length a;
9.51 - (if i < len
9.52 - then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
9.53 - else raise (''array update: index out of range''))
9.54 - done)"
9.55 -
9.56 -lemma upd_return:
9.57 - "upd i x a \<guillemotright> return a = upd i x a"
9.58 -proof (rule Heap_eqI)
9.59 - fix h
9.60 - obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
9.61 - by (cases "Heap_Monad.execute (Array.length a) h")
9.62 - then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
9.63 - by (auto simp add: upd_def bindM_def split: sum.split)
9.64 -qed
9.65 -
9.66 -
9.67 -subsection {* Derivates *}
9.68 -
9.69 -definition
9.70 - map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
9.71 -where
9.72 - "map_entry i f a = (do
9.73 - x \<leftarrow> nth a i;
9.74 - upd i (f x) a
9.75 - done)"
9.76 -
9.77 -definition
9.78 - swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap"
9.79 -where
9.80 - "swap i x a = (do
9.81 - y \<leftarrow> nth a i;
9.82 - upd i x a;
9.83 - return y
9.84 - done)"
9.85 -
9.86 -definition
9.87 - make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap"
9.88 -where
9.89 - "make n f = of_list (map f [0 ..< n])"
9.90 -
9.91 -definition
9.92 - freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
9.93 -where
9.94 - "freeze a = (do
9.95 - n \<leftarrow> length a;
9.96 - mapM (nth a) [0..<n]
9.97 - done)"
9.98 -
9.99 -definition
9.100 - map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
9.101 -where
9.102 - "map f a = (do
9.103 - n \<leftarrow> length a;
9.104 - mapM (\<lambda>n. map_entry n f a) [0..<n];
9.105 - return a
9.106 - done)"
9.107 -
9.108 -hide (open) const new map -- {* avoid clashed with some popular names *}
9.109 -
9.110 -
9.111 -subsection {* Properties *}
9.112 -
9.113 -lemma array_make [code]:
9.114 - "Array.new n x = make n (\<lambda>_. x)"
9.115 - by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
9.116 - monad_simp array_of_list_replicate [symmetric]
9.117 - map_replicate_trivial replicate_append_same
9.118 - of_list_def)
9.119 -
9.120 -lemma array_of_list_make [code]:
9.121 - "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
9.122 - unfolding make_def map_nth ..
9.123 -
9.124 -
9.125 -subsection {* Code generator setup *}
9.126 -
9.127 -subsubsection {* Logical intermediate layer *}
9.128 -
9.129 -definition new' where
9.130 - [code del]: "new' = Array.new o nat_of_index"
9.131 -hide (open) const new'
9.132 -lemma [code]:
9.133 - "Array.new = Array.new' o index_of_nat"
9.134 - by (simp add: new'_def o_def)
9.135 -
9.136 -definition of_list' where
9.137 - [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
9.138 -hide (open) const of_list'
9.139 -lemma [code]:
9.140 - "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
9.141 - by (simp add: of_list'_def)
9.142 -
9.143 -definition make' where
9.144 - [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
9.145 -hide (open) const make'
9.146 -lemma [code]:
9.147 - "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
9.148 - by (simp add: make'_def o_def)
9.149 -
9.150 -definition length' where
9.151 - [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
9.152 -hide (open) const length'
9.153 -lemma [code]:
9.154 - "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
9.155 - by (simp add: length'_def monad_simp',
9.156 - simp add: liftM_def comp_def monad_simp,
9.157 - simp add: monad_simp')
9.158 -
9.159 -definition nth' where
9.160 - [code del]: "nth' a = Array.nth a o nat_of_index"
9.161 -hide (open) const nth'
9.162 -lemma [code]:
9.163 - "Array.nth a n = Array.nth' a (index_of_nat n)"
9.164 - by (simp add: nth'_def)
9.165 -
9.166 -definition upd' where
9.167 - [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
9.168 -hide (open) const upd'
9.169 -lemma [code]:
9.170 - "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
9.171 - by (simp add: upd'_def monad_simp upd_return)
9.172 -
9.173 -
9.174 -subsubsection {* SML *}
9.175 -
9.176 -code_type array (SML "_/ array")
9.177 -code_const Array (SML "raise/ (Fail/ \"bare Array\")")
9.178 -code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
9.179 -code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
9.180 -code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
9.181 -code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
9.182 -code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
9.183 -code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
9.184 -
9.185 -code_reserved SML Array
9.186 -
9.187 -
9.188 -subsubsection {* OCaml *}
9.189 -
9.190 -code_type array (OCaml "_/ array")
9.191 -code_const Array (OCaml "failwith/ \"bare Array\"")
9.192 -code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
9.193 -code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
9.194 -code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
9.195 -code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
9.196 -code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
9.197 -code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
9.198 -
9.199 -code_reserved OCaml Array
9.200 -
9.201 -
9.202 -subsubsection {* Haskell *}
9.203 -
9.204 -code_type array (Haskell "STArray/ RealWorld/ _")
9.205 -code_const Array (Haskell "error/ \"bare Array\"")
9.206 -code_const Array.new' (Haskell "newArray/ (0,/ _)")
9.207 -code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
9.208 -code_const Array.length' (Haskell "lengthArray")
9.209 -code_const Array.nth' (Haskell "readArray")
9.210 -code_const Array.upd' (Haskell "writeArray")
9.211 -
9.212 -end
10.1 --- a/src/HOL/Library/Heap.thy Thu Jan 08 10:53:48 2009 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,434 +0,0 @@
10.4 -(* Title: HOL/Library/Heap.thy
10.5 - ID: $Id$
10.6 - Author: John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
10.7 -*)
10.8 -
10.9 -header {* A polymorphic heap based on cantor encodings *}
10.10 -
10.11 -theory Heap
10.12 -imports Plain "~~/src/HOL/List" Countable Typerep
10.13 -begin
10.14 -
10.15 -subsection {* Representable types *}
10.16 -
10.17 -text {* The type class of representable types *}
10.18 -
10.19 -class heap = typerep + countable
10.20 -
10.21 -text {* Instances for common HOL types *}
10.22 -
10.23 -instance nat :: heap ..
10.24 -
10.25 -instance "*" :: (heap, heap) heap ..
10.26 -
10.27 -instance "+" :: (heap, heap) heap ..
10.28 -
10.29 -instance list :: (heap) heap ..
10.30 -
10.31 -instance option :: (heap) heap ..
10.32 -
10.33 -instance int :: heap ..
10.34 -
10.35 -instance message_string :: countable
10.36 - by (rule countable_classI [of "message_string_case to_nat"])
10.37 - (auto split: message_string.splits)
10.38 -
10.39 -instance message_string :: heap ..
10.40 -
10.41 -text {* Reflected types themselves are heap-representable *}
10.42 -
10.43 -instantiation typerep :: countable
10.44 -begin
10.45 -
10.46 -fun to_nat_typerep :: "typerep \<Rightarrow> nat" where
10.47 - "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
10.48 -
10.49 -instance
10.50 -proof (rule countable_classI)
10.51 - fix t t' :: typerep and ts
10.52 - have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')
10.53 - \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')"
10.54 - proof (induct rule: typerep.induct)
10.55 - case (Typerep c ts) show ?case
10.56 - proof (rule allI, rule impI)
10.57 - fix t'
10.58 - assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"
10.59 - then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"
10.60 - by (cases t') auto
10.61 - with Typerep hyp have "c = c'" and "ts = ts'" by simp_all
10.62 - with t' show "Typerep.Typerep c ts = t'" by simp
10.63 - qed
10.64 - next
10.65 - case Nil_typerep then show ?case by simp
10.66 - next
10.67 - case (Cons_typerep t ts) then show ?case by auto
10.68 - qed
10.69 - then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto
10.70 - moreover assume "to_nat_typerep t = to_nat_typerep t'"
10.71 - ultimately show "t = t'" by simp
10.72 -qed
10.73 -
10.74 -end
10.75 -
10.76 -instance typerep :: heap ..
10.77 -
10.78 -
10.79 -subsection {* A polymorphic heap with dynamic arrays and references *}
10.80 -
10.81 -types addr = nat -- "untyped heap references"
10.82 -
10.83 -datatype 'a array = Array addr
10.84 -datatype 'a ref = Ref addr -- "note the phantom type 'a "
10.85 -
10.86 -primrec addr_of_array :: "'a array \<Rightarrow> addr" where
10.87 - "addr_of_array (Array x) = x"
10.88 -
10.89 -primrec addr_of_ref :: "'a ref \<Rightarrow> addr" where
10.90 - "addr_of_ref (Ref x) = x"
10.91 -
10.92 -lemma addr_of_array_inj [simp]:
10.93 - "addr_of_array a = addr_of_array a' \<longleftrightarrow> a = a'"
10.94 - by (cases a, cases a') simp_all
10.95 -
10.96 -lemma addr_of_ref_inj [simp]:
10.97 - "addr_of_ref r = addr_of_ref r' \<longleftrightarrow> r = r'"
10.98 - by (cases r, cases r') simp_all
10.99 -
10.100 -instance array :: (type) countable
10.101 - by (rule countable_classI [of addr_of_array]) simp
10.102 -
10.103 -instance ref :: (type) countable
10.104 - by (rule countable_classI [of addr_of_ref]) simp
10.105 -
10.106 -setup {*
10.107 - Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap array"})
10.108 - #> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>heap ref"})
10.109 - #> Sign.add_const_constraint (@{const_name addr_of_array}, SOME @{typ "'a\<Colon>heap array \<Rightarrow> nat"})
10.110 - #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\<Colon>heap ref \<Rightarrow> nat"})
10.111 -*}
10.112 -
10.113 -types heap_rep = nat -- "representable values"
10.114 -
10.115 -record heap =
10.116 - arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"
10.117 - refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep"
10.118 - lim :: addr
10.119 -
10.120 -definition empty :: heap where
10.121 - "empty = \<lparr>arrays = (\<lambda>_. undefined), refs = (\<lambda>_. undefined), lim = 0\<rparr>" -- "why undefined?"
10.122 -
10.123 -
10.124 -subsection {* Imperative references and arrays *}
10.125 -
10.126 -text {*
10.127 - References and arrays are developed in parallel,
10.128 - but keeping them separate makes some later proofs simpler.
10.129 -*}
10.130 -
10.131 -subsubsection {* Primitive operations *}
10.132 -
10.133 -definition
10.134 - new_ref :: "heap \<Rightarrow> ('a\<Colon>heap) ref \<times> heap" where
10.135 - "new_ref h = (let l = lim h in (Ref l, h\<lparr>lim := l + 1\<rparr>))"
10.136 -
10.137 -definition
10.138 - new_array :: "heap \<Rightarrow> ('a\<Colon>heap) array \<times> heap" where
10.139 - "new_array h = (let l = lim h in (Array l, h\<lparr>lim := l + 1\<rparr>))"
10.140 -
10.141 -definition
10.142 - ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where
10.143 - "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h"
10.144 -
10.145 -definition
10.146 - array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
10.147 - "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
10.148 -
10.149 -definition
10.150 - get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where
10.151 - "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))"
10.152 -
10.153 -definition
10.154 - get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
10.155 - "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
10.156 -
10.157 -definition
10.158 - set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
10.159 - "set_ref r x =
10.160 - refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
10.161 -
10.162 -definition
10.163 - set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
10.164 - "set_array a x =
10.165 - arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
10.166 -
10.167 -subsubsection {* Interface operations *}
10.168 -
10.169 -definition
10.170 - ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where
10.171 - "ref x h = (let (r, h') = new_ref h;
10.172 - h'' = set_ref r x h'
10.173 - in (r, h''))"
10.174 -
10.175 -definition
10.176 - array :: "nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
10.177 - "array n x h = (let (r, h') = new_array h;
10.178 - h'' = set_array r (replicate n x) h'
10.179 - in (r, h''))"
10.180 -
10.181 -definition
10.182 - array_of_list :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
10.183 - "array_of_list xs h = (let (r, h') = new_array h;
10.184 - h'' = set_array r xs h'
10.185 - in (r, h''))"
10.186 -
10.187 -definition
10.188 - upd :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
10.189 - "upd a i x h = set_array a ((get_array a h)[i:=x]) h"
10.190 -
10.191 -definition
10.192 - length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
10.193 - "length a h = size (get_array a h)"
10.194 -
10.195 -definition
10.196 - array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
10.197 - "array_ran a h = {e. Some e \<in> set (get_array a h)}"
10.198 - -- {*FIXME*}
10.199 -
10.200 -
10.201 -subsubsection {* Reference equality *}
10.202 -
10.203 -text {*
10.204 - The following relations are useful for comparing arrays and references.
10.205 -*}
10.206 -
10.207 -definition
10.208 - noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70)
10.209 -where
10.210 - "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
10.211 -
10.212 -definition
10.213 - noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70)
10.214 -where
10.215 - "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
10.216 -
10.217 -lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
10.218 - and noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
10.219 - and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
10.220 - and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
10.221 -unfolding noteq_refs_def noteq_arrs_def by auto
10.222 -
10.223 -lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
10.224 - by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)
10.225 -
10.226 -lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array v x h)"
10.227 - by (simp add: array_present_def noteq_arrs_def new_array_def array_def Let_def)
10.228 -
10.229 -
10.230 -subsubsection {* Properties of heap containers *}
10.231 -
10.232 -text {* Properties of imperative arrays *}
10.233 -
10.234 -text {* FIXME: Does there exist a "canonical" array axiomatisation in
10.235 -the literature? *}
10.236 -
10.237 -lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
10.238 - by (simp add: get_array_def set_array_def)
10.239 -
10.240 -lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
10.241 - by (simp add: noteq_arrs_def get_array_def set_array_def)
10.242 -
10.243 -lemma set_array_same [simp]:
10.244 - "set_array r x (set_array r y h) = set_array r x h"
10.245 - by (simp add: set_array_def)
10.246 -
10.247 -lemma array_set_set_swap:
10.248 - "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
10.249 - by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
10.250 -
10.251 -lemma array_ref_set_set_swap:
10.252 - "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)"
10.253 - by (simp add: Let_def expand_fun_eq set_array_def set_ref_def)
10.254 -
10.255 -lemma get_array_upd_eq [simp]:
10.256 - "get_array a (upd a i v h) = (get_array a h) [i := v]"
10.257 - by (simp add: upd_def)
10.258 -
10.259 -lemma nth_upd_array_neq_array [simp]:
10.260 - "a =!!= b \<Longrightarrow> get_array a (upd b j v h) ! i = get_array a h ! i"
10.261 - by (simp add: upd_def noteq_arrs_def)
10.262 -
10.263 -lemma get_arry_array_upd_elem_neqIndex [simp]:
10.264 - "i \<noteq> j \<Longrightarrow> get_array a (upd a j v h) ! i = get_array a h ! i"
10.265 - by simp
10.266 -
10.267 -lemma length_upd_eq [simp]:
10.268 - "length a (upd a i v h) = length a h"
10.269 - by (simp add: length_def upd_def)
10.270 -
10.271 -lemma length_upd_neq [simp]:
10.272 - "length a (upd b i v h) = length a h"
10.273 - by (simp add: upd_def length_def set_array_def get_array_def)
10.274 -
10.275 -lemma upd_swap_neqArray:
10.276 - "a =!!= a' \<Longrightarrow>
10.277 - upd a i v (upd a' i' v' h)
10.278 - = upd a' i' v' (upd a i v h)"
10.279 -apply (unfold upd_def)
10.280 -apply simp
10.281 -apply (subst array_set_set_swap, assumption)
10.282 -apply (subst array_get_set_neq)
10.283 -apply (erule noteq_arrs_sym)
10.284 -apply (simp)
10.285 -done
10.286 -
10.287 -lemma upd_swap_neqIndex:
10.288 - "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> upd a i v (upd a i' v' h) = upd a i' v' (upd a i v h)"
10.289 -by (auto simp add: upd_def array_set_set_swap list_update_swap)
10.290 -
10.291 -lemma get_array_init_array_list:
10.292 - "get_array (fst (array_of_list ls h)) (snd (array_of_list ls' h)) = ls'"
10.293 - by (simp add: Let_def split_def array_of_list_def)
10.294 -
10.295 -lemma set_array:
10.296 - "set_array (fst (array_of_list ls h))
10.297 - new_ls (snd (array_of_list ls h))
10.298 - = snd (array_of_list new_ls h)"
10.299 - by (simp add: Let_def split_def array_of_list_def)
10.300 -
10.301 -lemma array_present_upd [simp]:
10.302 - "array_present a (upd b i v h) = array_present a h"
10.303 - by (simp add: upd_def array_present_def set_array_def get_array_def)
10.304 -
10.305 -lemma array_of_list_replicate:
10.306 - "array_of_list (replicate n x) = array n x"
10.307 - by (simp add: expand_fun_eq array_of_list_def array_def)
10.308 -
10.309 -
10.310 -text {* Properties of imperative references *}
10.311 -
10.312 -lemma next_ref_fresh [simp]:
10.313 - assumes "(r, h') = new_ref h"
10.314 - shows "\<not> ref_present r h"
10.315 - using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def)
10.316 -
10.317 -lemma next_ref_present [simp]:
10.318 - assumes "(r, h') = new_ref h"
10.319 - shows "ref_present r h'"
10.320 - using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def)
10.321 -
10.322 -lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x"
10.323 - by (simp add: get_ref_def set_ref_def)
10.324 -
10.325 -lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h"
10.326 - by (simp add: noteq_refs_def get_ref_def set_ref_def)
10.327 -
10.328 -(* FIXME: We need some infrastructure to infer that locally generated
10.329 - new refs (by new_ref(_no_init), new_array(')) are distinct
10.330 - from all existing refs.
10.331 -*)
10.332 -
10.333 -lemma ref_set_get: "set_ref r (get_ref r h) h = h"
10.334 -apply (simp add: set_ref_def get_ref_def)
10.335 -oops
10.336 -
10.337 -lemma set_ref_same[simp]:
10.338 - "set_ref r x (set_ref r y h) = set_ref r x h"
10.339 - by (simp add: set_ref_def)
10.340 -
10.341 -lemma ref_set_set_swap:
10.342 - "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)"
10.343 - by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def)
10.344 -
10.345 -lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)"
10.346 - by (simp add: ref_def new_ref_def set_ref_def Let_def)
10.347 -
10.348 -lemma ref_get_new [simp]:
10.349 - "get_ref (fst (ref v h)) (snd (ref v' h)) = v'"
10.350 - by (simp add: ref_def Let_def split_def)
10.351 -
10.352 -lemma ref_set_new [simp]:
10.353 - "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)"
10.354 - by (simp add: ref_def Let_def split_def)
10.355 -
10.356 -lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow>
10.357 - get_ref r (snd (ref v h)) = get_ref r h"
10.358 - by (simp add: get_ref_def set_ref_def ref_def Let_def new_ref_def noteq_refs_def)
10.359 -
10.360 -lemma lim_set_ref [simp]:
10.361 - "lim (set_ref r v h) = lim h"
10.362 - by (simp add: set_ref_def)
10.363 -
10.364 -lemma ref_present_new_ref [simp]:
10.365 - "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))"
10.366 - by (simp add: new_ref_def ref_present_def ref_def Let_def)
10.367 -
10.368 -lemma ref_present_set_ref [simp]:
10.369 - "ref_present r (set_ref r' v h) = ref_present r h"
10.370 - by (simp add: set_ref_def ref_present_def)
10.371 -
10.372 -lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Heap.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
10.373 -unfolding array_ran_def Heap.length_def by simp
10.374 -
10.375 -lemma array_ran_upd_array_Some:
10.376 - assumes "cl \<in> array_ran a (Heap.upd a i (Some b) h)"
10.377 - shows "cl \<in> array_ran a h \<or> cl = b"
10.378 -proof -
10.379 - have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
10.380 - with assms show ?thesis
10.381 - unfolding array_ran_def Heap.upd_def by fastsimp
10.382 -qed
10.383 -
10.384 -lemma array_ran_upd_array_None:
10.385 - assumes "cl \<in> array_ran a (Heap.upd a i None h)"
10.386 - shows "cl \<in> array_ran a h"
10.387 -proof -
10.388 - have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
10.389 - with assms show ?thesis
10.390 - unfolding array_ran_def Heap.upd_def by auto
10.391 -qed
10.392 -
10.393 -
10.394 -text {* Non-interaction between imperative array and imperative references *}
10.395 -
10.396 -lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h"
10.397 - by (simp add: get_array_def set_ref_def)
10.398 -
10.399 -lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i"
10.400 - by simp
10.401 -
10.402 -lemma get_ref_upd [simp]: "get_ref r (upd a i v h) = get_ref r h"
10.403 - by (simp add: get_ref_def set_array_def upd_def)
10.404 -
10.405 -lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
10.406 - by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def new_ref_def)
10.407 -
10.408 -text {*not actually true ???*}
10.409 -lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
10.410 -apply (case_tac a)
10.411 -apply (simp add: Let_def upd_def)
10.412 -apply auto
10.413 -oops
10.414 -
10.415 -lemma length_new_ref[simp]:
10.416 - "length a (snd (ref v h)) = length a h"
10.417 - by (simp add: get_array_def set_ref_def length_def new_ref_def ref_def Let_def)
10.418 -
10.419 -lemma get_array_new_ref [simp]:
10.420 - "get_array a (snd (ref v h)) = get_array a h"
10.421 - by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def)
10.422 -
10.423 -lemma ref_present_upd [simp]:
10.424 - "ref_present r (upd a i v h) = ref_present r h"
10.425 - by (simp add: upd_def ref_present_def set_array_def get_array_def)
10.426 -
10.427 -lemma array_present_set_ref [simp]:
10.428 - "array_present a (set_ref r v h) = array_present a h"
10.429 - by (simp add: array_present_def set_ref_def)
10.430 -
10.431 -lemma array_present_new_ref [simp]:
10.432 - "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
10.433 - by (simp add: array_present_def new_ref_def ref_def Let_def)
10.434 -
10.435 -hide (open) const empty array array_of_list upd length ref
10.436 -
10.437 -end
11.1 --- a/src/HOL/Library/Heap_Monad.thy Thu Jan 08 10:53:48 2009 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,425 +0,0 @@
11.4 -(* Title: HOL/Library/Heap_Monad.thy
11.5 - ID: $Id$
11.6 - Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
11.7 -*)
11.8 -
11.9 -header {* A monad with a polymorphic heap *}
11.10 -
11.11 -theory Heap_Monad
11.12 -imports Heap
11.13 -begin
11.14 -
11.15 -subsection {* The monad *}
11.16 -
11.17 -subsubsection {* Monad combinators *}
11.18 -
11.19 -datatype exception = Exn
11.20 -
11.21 -text {* Monadic heap actions either produce values
11.22 - and transform the heap, or fail *}
11.23 -datatype 'a Heap = Heap "heap \<Rightarrow> ('a + exception) \<times> heap"
11.24 -
11.25 -primrec
11.26 - execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a + exception) \<times> heap" where
11.27 - "execute (Heap f) = f"
11.28 -lemmas [code del] = execute.simps
11.29 -
11.30 -lemma Heap_execute [simp]:
11.31 - "Heap (execute f) = f" by (cases f) simp_all
11.32 -
11.33 -lemma Heap_eqI:
11.34 - "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
11.35 - by (cases f, cases g) (auto simp: expand_fun_eq)
11.36 -
11.37 -lemma Heap_eqI':
11.38 - "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
11.39 - by (auto simp: expand_fun_eq intro: Heap_eqI)
11.40 -
11.41 -lemma Heap_strip: "(\<And>f. PROP P f) \<equiv> (\<And>g. PROP P (Heap g))"
11.42 -proof
11.43 - fix g :: "heap \<Rightarrow> ('a + exception) \<times> heap"
11.44 - assume "\<And>f. PROP P f"
11.45 - then show "PROP P (Heap g)" .
11.46 -next
11.47 - fix f :: "'a Heap"
11.48 - assume assm: "\<And>g. PROP P (Heap g)"
11.49 - then have "PROP P (Heap (execute f))" .
11.50 - then show "PROP P f" by simp
11.51 -qed
11.52 -
11.53 -definition
11.54 - heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
11.55 - [code del]: "heap f = Heap (\<lambda>h. apfst Inl (f h))"
11.56 -
11.57 -lemma execute_heap [simp]:
11.58 - "execute (heap f) h = apfst Inl (f h)"
11.59 - by (simp add: heap_def)
11.60 -
11.61 -definition
11.62 - bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
11.63 - [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
11.64 - (Inl x, h') \<Rightarrow> execute (g x) h'
11.65 - | r \<Rightarrow> r)"
11.66 -
11.67 -notation
11.68 - bindM (infixl "\<guillemotright>=" 54)
11.69 -
11.70 -abbreviation
11.71 - chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
11.72 - "f >> g \<equiv> f >>= (\<lambda>_. g)"
11.73 -
11.74 -notation
11.75 - chainM (infixl "\<guillemotright>" 54)
11.76 -
11.77 -definition
11.78 - return :: "'a \<Rightarrow> 'a Heap" where
11.79 - [code del]: "return x = heap (Pair x)"
11.80 -
11.81 -lemma execute_return [simp]:
11.82 - "execute (return x) h = apfst Inl (x, h)"
11.83 - by (simp add: return_def)
11.84 -
11.85 -definition
11.86 - raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
11.87 - [code del]: "raise s = Heap (Pair (Inr Exn))"
11.88 -
11.89 -notation (latex output)
11.90 - "raise" ("\<^raw:{\textsf{raise}}>")
11.91 -
11.92 -lemma execute_raise [simp]:
11.93 - "execute (raise s) h = (Inr Exn, h)"
11.94 - by (simp add: raise_def)
11.95 -
11.96 -
11.97 -subsubsection {* do-syntax *}
11.98 -
11.99 -text {*
11.100 - We provide a convenient do-notation for monadic expressions
11.101 - well-known from Haskell. @{const Let} is printed
11.102 - specially in do-expressions.
11.103 -*}
11.104 -
11.105 -nonterminals do_expr
11.106 -
11.107 -syntax
11.108 - "_do" :: "do_expr \<Rightarrow> 'a"
11.109 - ("(do (_)//done)" [12] 100)
11.110 - "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
11.111 - ("_ <- _;//_" [1000, 13, 12] 12)
11.112 - "_chainM" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
11.113 - ("_;//_" [13, 12] 12)
11.114 - "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
11.115 - ("let _ = _;//_" [1000, 13, 12] 12)
11.116 - "_nil" :: "'a \<Rightarrow> do_expr"
11.117 - ("_" [12] 12)
11.118 -
11.119 -syntax (xsymbols)
11.120 - "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
11.121 - ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
11.122 -syntax (latex output)
11.123 - "_do" :: "do_expr \<Rightarrow> 'a"
11.124 - ("(\<^raw:{\textsf{do}}> (_))" [12] 100)
11.125 - "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
11.126 - ("\<^raw:\textsf{let}> _ = _;//_" [1000, 13, 12] 12)
11.127 -notation (latex output)
11.128 - "return" ("\<^raw:{\textsf{return}}>")
11.129 -
11.130 -translations
11.131 - "_do f" => "f"
11.132 - "_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
11.133 - "_chainM f g" => "f \<guillemotright> g"
11.134 - "_let x t f" => "CONST Let t (\<lambda>x. f)"
11.135 - "_nil f" => "f"
11.136 -
11.137 -print_translation {*
11.138 -let
11.139 - fun dest_abs_eta (Abs (abs as (_, ty, _))) =
11.140 - let
11.141 - val (v, t) = Syntax.variant_abs abs;
11.142 - in (Free (v, ty), t) end
11.143 - | dest_abs_eta t =
11.144 - let
11.145 - val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
11.146 - in (Free (v, dummyT), t) end;
11.147 - fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =
11.148 - let
11.149 - val (v, g') = dest_abs_eta g;
11.150 - val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
11.151 - val v_used = fold_aterms
11.152 - (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
11.153 - in if v_used then
11.154 - Const ("_bindM", dummyT) $ v $ f $ unfold_monad g'
11.155 - else
11.156 - Const ("_chainM", dummyT) $ f $ unfold_monad g'
11.157 - end
11.158 - | unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) =
11.159 - Const ("_chainM", dummyT) $ f $ unfold_monad g
11.160 - | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
11.161 - let
11.162 - val (v, g') = dest_abs_eta g;
11.163 - in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end
11.164 - | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
11.165 - Const (@{const_syntax return}, dummyT) $ f
11.166 - | unfold_monad f = f;
11.167 - fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true
11.168 - | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
11.169 - contains_bindM t;
11.170 - fun bindM_monad_tr' (f::g::ts) = list_comb
11.171 - (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
11.172 - fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb
11.173 - (Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
11.174 - else raise Match;
11.175 -in [
11.176 - (@{const_syntax bindM}, bindM_monad_tr'),
11.177 - (@{const_syntax Let}, Let_monad_tr')
11.178 -] end;
11.179 -*}
11.180 -
11.181 -
11.182 -subsection {* Monad properties *}
11.183 -
11.184 -subsubsection {* Monad laws *}
11.185 -
11.186 -lemma return_bind: "return x \<guillemotright>= f = f x"
11.187 - by (simp add: bindM_def return_def)
11.188 -
11.189 -lemma bind_return: "f \<guillemotright>= return = f"
11.190 -proof (rule Heap_eqI)
11.191 - fix h
11.192 - show "execute (f \<guillemotright>= return) h = execute f h"
11.193 - by (auto simp add: bindM_def return_def split: sum.splits prod.splits)
11.194 -qed
11.195 -
11.196 -lemma bind_bind: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
11.197 - by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)
11.198 -
11.199 -lemma bind_bind': "f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h x) = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= (\<lambda>y. return (x, y))) \<guillemotright>= (\<lambda>(x, y). h x y)"
11.200 - by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)
11.201 -
11.202 -lemma raise_bind: "raise e \<guillemotright>= f = raise e"
11.203 - by (simp add: raise_def bindM_def)
11.204 -
11.205 -
11.206 -lemmas monad_simp = return_bind bind_return bind_bind raise_bind
11.207 -
11.208 -
11.209 -subsection {* Generic combinators *}
11.210 -
11.211 -definition
11.212 - liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap"
11.213 -where
11.214 - "liftM f = return o f"
11.215 -
11.216 -definition
11.217 - compM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> ('b \<Rightarrow> 'c Heap) \<Rightarrow> 'a \<Rightarrow> 'c Heap" (infixl ">>==" 54)
11.218 -where
11.219 - "(f >>== g) = (\<lambda>x. f x \<guillemotright>= g)"
11.220 -
11.221 -notation
11.222 - compM (infixl "\<guillemotright>==" 54)
11.223 -
11.224 -lemma liftM_collapse: "liftM f x = return (f x)"
11.225 - by (simp add: liftM_def)
11.226 -
11.227 -lemma liftM_compM: "liftM f \<guillemotright>== g = g o f"
11.228 - by (auto intro: Heap_eqI' simp add: expand_fun_eq liftM_def compM_def bindM_def)
11.229 -
11.230 -lemma compM_return: "f \<guillemotright>== return = f"
11.231 - by (simp add: compM_def monad_simp)
11.232 -
11.233 -lemma compM_compM: "(f \<guillemotright>== g) \<guillemotright>== h = f \<guillemotright>== (g \<guillemotright>== h)"
11.234 - by (simp add: compM_def monad_simp)
11.235 -
11.236 -lemma liftM_bind:
11.237 - "(\<lambda>x. liftM f x \<guillemotright>= liftM g) = liftM (\<lambda>x. g (f x))"
11.238 - by (rule Heap_eqI') (simp add: monad_simp liftM_def bindM_def)
11.239 -
11.240 -lemma liftM_comp:
11.241 - "liftM f o g = liftM (f o g)"
11.242 - by (rule Heap_eqI') (simp add: liftM_def)
11.243 -
11.244 -lemmas monad_simp' = monad_simp liftM_compM compM_return
11.245 - compM_compM liftM_bind liftM_comp
11.246 -
11.247 -primrec
11.248 - mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap"
11.249 -where
11.250 - "mapM f [] = return []"
11.251 - | "mapM f (x#xs) = do y \<leftarrow> f x;
11.252 - ys \<leftarrow> mapM f xs;
11.253 - return (y # ys)
11.254 - done"
11.255 -
11.256 -primrec
11.257 - foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
11.258 -where
11.259 - "foldM f [] s = return s"
11.260 - | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
11.261 -
11.262 -definition
11.263 - assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
11.264 -where
11.265 - "assert P x = (if P x then return x else raise (''assert''))"
11.266 -
11.267 -lemma assert_cong [fundef_cong]:
11.268 - assumes "P = P'"
11.269 - assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
11.270 - shows "(assert P x >>= f) = (assert P' x >>= f')"
11.271 - using assms by (auto simp add: assert_def return_bind raise_bind)
11.272 -
11.273 -hide (open) const heap execute
11.274 -
11.275 -
11.276 -subsection {* Code generator setup *}
11.277 -
11.278 -subsubsection {* Logical intermediate layer *}
11.279 -
11.280 -definition
11.281 - Fail :: "message_string \<Rightarrow> exception"
11.282 -where
11.283 - [code del]: "Fail s = Exn"
11.284 -
11.285 -definition
11.286 - raise_exc :: "exception \<Rightarrow> 'a Heap"
11.287 -where
11.288 - [code del]: "raise_exc e = raise []"
11.289 -
11.290 -lemma raise_raise_exc [code, code inline]:
11.291 - "raise s = raise_exc (Fail (STR s))"
11.292 - unfolding Fail_def raise_exc_def raise_def ..
11.293 -
11.294 -hide (open) const Fail raise_exc
11.295 -
11.296 -
11.297 -subsubsection {* SML and OCaml *}
11.298 -
11.299 -code_type Heap (SML "unit/ ->/ _")
11.300 -code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
11.301 -code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
11.302 -code_const return (SML "!(fn/ ()/ =>/ _)")
11.303 -code_const "Heap_Monad.Fail" (SML "Fail")
11.304 -code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)")
11.305 -
11.306 -code_type Heap (OCaml "_")
11.307 -code_const Heap (OCaml "failwith/ \"bare Heap\"")
11.308 -code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
11.309 -code_const return (OCaml "!(fun/ ()/ ->/ _)")
11.310 -code_const "Heap_Monad.Fail" (OCaml "Failure")
11.311 -code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
11.312 -
11.313 -setup {* let
11.314 - open Code_Thingol;
11.315 -
11.316 - fun lookup naming = the o Code_Thingol.lookup_const naming;
11.317 -
11.318 - fun imp_monad_bind'' bind' return' unit' ts =
11.319 - let
11.320 - val dummy_name = "";
11.321 - val dummy_type = ITyVar dummy_name;
11.322 - val dummy_case_term = IVar dummy_name;
11.323 - (*assumption: dummy values are not relevant for serialization*)
11.324 - val unitt = IConst (unit', ([], []));
11.325 - fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
11.326 - | dest_abs (t, ty) =
11.327 - let
11.328 - val vs = Code_Thingol.fold_varnames cons t [];
11.329 - val v = Name.variant vs "x";
11.330 - val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
11.331 - in ((v, ty'), t `$ IVar v) end;
11.332 - fun force (t as IConst (c, _) `$ t') = if c = return'
11.333 - then t' else t `$ unitt
11.334 - | force t = t `$ unitt;
11.335 - fun tr_bind' [(t1, _), (t2, ty2)] =
11.336 - let
11.337 - val ((v, ty), t) = dest_abs (t2, ty2);
11.338 - in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
11.339 - and tr_bind'' t = case Code_Thingol.unfold_app t
11.340 - of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
11.341 - then tr_bind' [(x1, ty1), (x2, ty2)]
11.342 - else force t
11.343 - | _ => force t;
11.344 - in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
11.345 - [(unitt, tr_bind' ts)]), dummy_case_term) end
11.346 - and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
11.347 - of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
11.348 - | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
11.349 - | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
11.350 - else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
11.351 - and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
11.352 - | imp_monad_bind bind' return' unit' (t as IVar _) = t
11.353 - | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
11.354 - of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
11.355 - | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
11.356 - | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t
11.357 - | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
11.358 - (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
11.359 -
11.360 - fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
11.361 - (imp_monad_bind (lookup naming @{const_name bindM})
11.362 - (lookup naming @{const_name return})
11.363 - (lookup naming @{const_name Unity}));
11.364 -
11.365 -in
11.366 -
11.367 - Code_Target.extend_target ("SML_imp", ("SML", imp_program))
11.368 - #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
11.369 -
11.370 -end
11.371 -*}
11.372 -
11.373 -
11.374 -code_reserved OCaml Failure raise
11.375 -
11.376 -
11.377 -subsubsection {* Haskell *}
11.378 -
11.379 -text {* Adaption layer *}
11.380 -
11.381 -code_include Haskell "STMonad"
11.382 -{*import qualified Control.Monad;
11.383 -import qualified Control.Monad.ST;
11.384 -import qualified Data.STRef;
11.385 -import qualified Data.Array.ST;
11.386 -
11.387 -type RealWorld = Control.Monad.ST.RealWorld;
11.388 -type ST s a = Control.Monad.ST.ST s a;
11.389 -type STRef s a = Data.STRef.STRef s a;
11.390 -type STArray s a = Data.Array.ST.STArray s Int a;
11.391 -
11.392 -runST :: (forall s. ST s a) -> a;
11.393 -runST s = Control.Monad.ST.runST s;
11.394 -
11.395 -newSTRef = Data.STRef.newSTRef;
11.396 -readSTRef = Data.STRef.readSTRef;
11.397 -writeSTRef = Data.STRef.writeSTRef;
11.398 -
11.399 -newArray :: (Int, Int) -> a -> ST s (STArray s a);
11.400 -newArray = Data.Array.ST.newArray;
11.401 -
11.402 -newListArray :: (Int, Int) -> [a] -> ST s (STArray s a);
11.403 -newListArray = Data.Array.ST.newListArray;
11.404 -
11.405 -lengthArray :: STArray s a -> ST s Int;
11.406 -lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
11.407 -
11.408 -readArray :: STArray s a -> Int -> ST s a;
11.409 -readArray = Data.Array.ST.readArray;
11.410 -
11.411 -writeArray :: STArray s a -> Int -> a -> ST s ();
11.412 -writeArray = Data.Array.ST.writeArray;*}
11.413 -
11.414 -code_reserved Haskell RealWorld ST STRef Array
11.415 - runST
11.416 - newSTRef reasSTRef writeSTRef
11.417 - newArray newListArray lengthArray readArray writeArray
11.418 -
11.419 -text {* Monad *}
11.420 -
11.421 -code_type Heap (Haskell "ST/ RealWorld/ _")
11.422 -code_const Heap (Haskell "error/ \"bare Heap\"")
11.423 -code_monad "op \<guillemotright>=" Haskell
11.424 -code_const return (Haskell "return")
11.425 -code_const "Heap_Monad.Fail" (Haskell "_")
11.426 -code_const "Heap_Monad.raise_exc" (Haskell "error")
11.427 -
11.428 -end
12.1 --- a/src/HOL/Library/Imperative_HOL.thy Thu Jan 08 10:53:48 2009 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,12 +0,0 @@
12.4 -(* Title: HOL/Library/Imperative_HOL.thy
12.5 - ID: $Id$
12.6 - Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
12.7 -*)
12.8 -
12.9 -header {* Entry point into monadic imperative HOL *}
12.10 -
12.11 -theory Imperative_HOL
12.12 -imports Array Ref Relational
12.13 -begin
12.14 -
12.15 -end
13.1 --- a/src/HOL/Library/Library.thy Thu Jan 08 10:53:48 2009 +0100
13.2 +++ b/src/HOL/Library/Library.thy Thu Jan 08 17:10:41 2009 +0100
13.3 @@ -22,7 +22,6 @@
13.4 Executable_Set
13.5 Float
13.6 FuncSet
13.7 - Imperative_HOL
13.8 Infinite_Set
13.9 ListVector
13.10 Multiset
14.1 --- a/src/HOL/Library/Ref.thy Thu Jan 08 10:53:48 2009 +0100
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,91 +0,0 @@
14.4 -(* Title: HOL/Library/Ref.thy
14.5 - ID: $Id$
14.6 - Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
14.7 -*)
14.8 -
14.9 -header {* Monadic references *}
14.10 -
14.11 -theory Ref
14.12 -imports Heap_Monad
14.13 -begin
14.14 -
14.15 -text {*
14.16 - Imperative reference operations; modeled after their ML counterparts.
14.17 - See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html
14.18 - and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
14.19 -*}
14.20 -
14.21 -subsection {* Primitives *}
14.22 -
14.23 -definition
14.24 - new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
14.25 - [code del]: "new v = Heap_Monad.heap (Heap.ref v)"
14.26 -
14.27 -definition
14.28 - lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
14.29 - [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get_ref r h, h))"
14.30 -
14.31 -definition
14.32 - update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where
14.33 - [code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))"
14.34 -
14.35 -
14.36 -subsection {* Derivates *}
14.37 -
14.38 -definition
14.39 - change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap"
14.40 -where
14.41 - "change f r = (do x \<leftarrow> ! r;
14.42 - let y = f x;
14.43 - r := y;
14.44 - return y
14.45 - done)"
14.46 -
14.47 -hide (open) const new lookup update change
14.48 -
14.49 -
14.50 -subsection {* Properties *}
14.51 -
14.52 -lemma lookup_chain:
14.53 - "(!r \<guillemotright> f) = f"
14.54 - by (cases f)
14.55 - (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
14.56 -
14.57 -lemma update_change [code]:
14.58 - "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
14.59 - by (auto simp add: monad_simp change_def lookup_chain)
14.60 -
14.61 -
14.62 -subsection {* Code generator setup *}
14.63 -
14.64 -subsubsection {* SML *}
14.65 -
14.66 -code_type ref (SML "_/ ref")
14.67 -code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
14.68 -code_const Ref.new (SML "(fn/ ()/ =>/ ref/ _)")
14.69 -code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
14.70 -code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
14.71 -
14.72 -code_reserved SML ref
14.73 -
14.74 -
14.75 -subsubsection {* OCaml *}
14.76 -
14.77 -code_type ref (OCaml "_/ ref")
14.78 -code_const Ref (OCaml "failwith/ \"bare Ref\")")
14.79 -code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)")
14.80 -code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
14.81 -code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
14.82 -
14.83 -code_reserved OCaml ref
14.84 -
14.85 -
14.86 -subsubsection {* Haskell *}
14.87 -
14.88 -code_type ref (Haskell "STRef/ RealWorld/ _")
14.89 -code_const Ref (Haskell "error/ \"bare Ref\"")
14.90 -code_const Ref.new (Haskell "newSTRef")
14.91 -code_const Ref.lookup (Haskell "readSTRef")
14.92 -code_const Ref.update (Haskell "writeSTRef")
14.93 -
14.94 -end
14.95 \ No newline at end of file
15.1 --- a/src/HOL/Library/Relational.thy Thu Jan 08 10:53:48 2009 +0100
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,700 +0,0 @@
15.4 -theory Relational
15.5 -imports Array Ref
15.6 -begin
15.7 -
15.8 -section{* Definition of the Relational framework *}
15.9 -
15.10 -text {* The crel predicate states that when a computation c runs with the heap h
15.11 - will result in return value r and a heap h' (if no exception occurs). *}
15.12 -
15.13 -definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
15.14 -where
15.15 - crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = (Inl r, h')"
15.16 -
15.17 -lemma crel_def: -- FIXME
15.18 - "crel c h h' r \<longleftrightarrow> (Inl r, h') = Heap_Monad.execute c h"
15.19 - unfolding crel_def' by auto
15.20 -
15.21 -lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
15.22 -unfolding crel_def' by auto
15.23 -
15.24 -section {* Elimination rules *}
15.25 -
15.26 -text {* For all commands, we define simple elimination rules. *}
15.27 -(* FIXME: consumes 1 necessary ?? *)
15.28 -
15.29 -subsection {* Elimination rules for basic monadic commands *}
15.30 -
15.31 -lemma crelE[consumes 1]:
15.32 - assumes "crel (f >>= g) h h'' r'"
15.33 - obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
15.34 - using assms
15.35 - by (auto simp add: crel_def bindM_def Let_def prod_case_beta split_def Pair_fst_snd_eq split add: sum.split_asm)
15.36 -
15.37 -lemma crelE'[consumes 1]:
15.38 - assumes "crel (f >> g) h h'' r'"
15.39 - obtains h' r where "crel f h h' r" "crel g h' h'' r'"
15.40 - using assms
15.41 - by (elim crelE) auto
15.42 -
15.43 -lemma crel_return[consumes 1]:
15.44 - assumes "crel (return x) h h' r"
15.45 - obtains "r = x" "h = h'"
15.46 - using assms
15.47 - unfolding crel_def return_def by simp
15.48 -
15.49 -lemma crel_raise[consumes 1]:
15.50 - assumes "crel (raise x) h h' r"
15.51 - obtains "False"
15.52 - using assms
15.53 - unfolding crel_def raise_def by simp
15.54 -
15.55 -lemma crel_if:
15.56 - assumes "crel (if c then t else e) h h' r"
15.57 - obtains "c" "crel t h h' r"
15.58 - | "\<not>c" "crel e h h' r"
15.59 - using assms
15.60 - unfolding crel_def by auto
15.61 -
15.62 -lemma crel_option_case:
15.63 - assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
15.64 - obtains "x = None" "crel n h h' r"
15.65 - | y where "x = Some y" "crel (s y) h h' r"
15.66 - using assms
15.67 - unfolding crel_def by auto
15.68 -
15.69 -lemma crel_mapM:
15.70 - assumes "crel (mapM f xs) h h' r"
15.71 - assumes "\<And>h h'. P f [] h h' []"
15.72 - assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (mapM f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
15.73 - shows "P f xs h h' r"
15.74 -using assms(1)
15.75 -proof (induct xs arbitrary: h h' r)
15.76 - case Nil with assms(2) show ?case
15.77 - by (auto elim: crel_return)
15.78 -next
15.79 - case (Cons x xs)
15.80 - from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
15.81 - and crel_mapM: "crel (mapM f xs) h1 h' ys"
15.82 - and r_def: "r = y#ys"
15.83 - unfolding mapM.simps
15.84 - by (auto elim!: crelE crel_return)
15.85 - from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
15.86 - show ?case by auto
15.87 -qed
15.88 -
15.89 -lemma crel_heap:
15.90 - assumes "crel (Heap_Monad.heap f) h h' r"
15.91 - obtains "h' = snd (f h)" "r = fst (f h)"
15.92 - using assms
15.93 - unfolding heap_def crel_def apfst_def split_def prod_fun_def by simp_all
15.94 -
15.95 -subsection {* Elimination rules for array commands *}
15.96 -
15.97 -lemma crel_length:
15.98 - assumes "crel (length a) h h' r"
15.99 - obtains "h = h'" "r = Heap.length a h'"
15.100 - using assms
15.101 - unfolding length_def
15.102 - by (elim crel_heap) simp
15.103 -
15.104 -(* Strong version of the lemma for this operation is missing *)
15.105 -lemma crel_new_weak:
15.106 - assumes "crel (Array.new n v) h h' r"
15.107 - obtains "get_array r h' = List.replicate n v"
15.108 - using assms unfolding Array.new_def
15.109 - by (elim crel_heap) (auto simp:Heap.array_def Let_def split_def)
15.110 -
15.111 -lemma crel_nth[consumes 1]:
15.112 - assumes "crel (nth a i) h h' r"
15.113 - obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
15.114 - using assms
15.115 - unfolding nth_def
15.116 - by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
15.117 -
15.118 -lemma crel_upd[consumes 1]:
15.119 - assumes "crel (upd i v a) h h' r"
15.120 - obtains "r = a" "h' = Heap.upd a i v h"
15.121 - using assms
15.122 - unfolding upd_def
15.123 - by (elim crelE crel_if crel_return crel_raise
15.124 - crel_length crel_heap) auto
15.125 -
15.126 -(* Strong version of the lemma for this operation is missing *)
15.127 -lemma crel_of_list_weak:
15.128 - assumes "crel (Array.of_list xs) h h' r"
15.129 - obtains "get_array r h' = xs"
15.130 - using assms
15.131 - unfolding of_list_def
15.132 - by (elim crel_heap) (simp add:get_array_init_array_list)
15.133 -
15.134 -lemma crel_map_entry:
15.135 - assumes "crel (Array.map_entry i f a) h h' r"
15.136 - obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
15.137 - using assms
15.138 - unfolding Array.map_entry_def
15.139 - by (elim crelE crel_upd crel_nth) auto
15.140 -
15.141 -lemma crel_swap:
15.142 - assumes "crel (Array.swap i x a) h h' r"
15.143 - obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
15.144 - using assms
15.145 - unfolding Array.swap_def
15.146 - by (elim crelE crel_upd crel_nth crel_return) auto
15.147 -
15.148 -(* Strong version of the lemma for this operation is missing *)
15.149 -lemma crel_make_weak:
15.150 - assumes "crel (Array.make n f) h h' r"
15.151 - obtains "i < n \<Longrightarrow> get_array r h' ! i = f i"
15.152 - using assms
15.153 - unfolding Array.make_def
15.154 - by (elim crel_of_list_weak) auto
15.155 -
15.156 -lemma upt_conv_Cons':
15.157 - assumes "Suc a \<le> b"
15.158 - shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
15.159 -proof -
15.160 - from assms have l: "b - Suc a < b" by arith
15.161 - from assms have "Suc (b - Suc a) = b - a" by arith
15.162 - with l show ?thesis by (simp add: upt_conv_Cons)
15.163 -qed
15.164 -
15.165 -lemma crel_mapM_nth:
15.166 - assumes
15.167 - "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' xs"
15.168 - assumes "n \<le> Heap.length a h"
15.169 - shows "h = h' \<and> xs = drop (Heap.length a h - n) (get_array a h)"
15.170 -using assms
15.171 -proof (induct n arbitrary: xs h h')
15.172 - case 0 thus ?case
15.173 - by (auto elim!: crel_return simp add: Heap.length_def)
15.174 -next
15.175 - case (Suc n)
15.176 - from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
15.177 - by (simp add: upt_conv_Cons')
15.178 - with Suc(2) obtain r where
15.179 - crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
15.180 - and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
15.181 - by (auto elim!: crelE crel_nth crel_return)
15.182 - from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)"
15.183 - by arith
15.184 - with Suc.hyps[OF crel_mapM] xs_def show ?case
15.185 - unfolding Heap.length_def
15.186 - by (auto simp add: nth_drop')
15.187 -qed
15.188 -
15.189 -lemma crel_freeze:
15.190 - assumes "crel (Array.freeze a) h h' xs"
15.191 - obtains "h = h'" "xs = get_array a h"
15.192 -proof
15.193 - from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
15.194 - unfolding freeze_def
15.195 - by (auto elim: crelE crel_length)
15.196 - hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
15.197 - by simp
15.198 - from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
15.199 -qed
15.200 -
15.201 -lemma crel_mapM_map_entry_remains:
15.202 - assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
15.203 - assumes "i < Heap.length a h - n"
15.204 - shows "get_array a h ! i = get_array a h' ! i"
15.205 -using assms
15.206 -proof (induct n arbitrary: h h' r)
15.207 - case 0
15.208 - thus ?case
15.209 - by (auto elim: crel_return)
15.210 -next
15.211 - case (Suc n)
15.212 - let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
15.213 - from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
15.214 - by (simp add: upt_conv_Cons')
15.215 - from Suc(2) this obtain r where
15.216 - crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
15.217 - by (auto simp add: elim!: crelE crel_map_entry crel_return)
15.218 - have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
15.219 - from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
15.220 - by simp
15.221 - from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
15.222 -qed
15.223 -
15.224 -lemma crel_mapM_map_entry_changes:
15.225 - assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
15.226 - assumes "n \<le> Heap.length a h"
15.227 - assumes "i \<ge> Heap.length a h - n"
15.228 - assumes "i < Heap.length a h"
15.229 - shows "get_array a h' ! i = f (get_array a h ! i)"
15.230 -using assms
15.231 -proof (induct n arbitrary: h h' r)
15.232 - case 0
15.233 - thus ?case
15.234 - by (auto elim!: crel_return)
15.235 -next
15.236 - case (Suc n)
15.237 - let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
15.238 - from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
15.239 - by (simp add: upt_conv_Cons')
15.240 - from Suc(2) this obtain r where
15.241 - crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
15.242 - by (auto simp add: elim!: crelE crel_map_entry crel_return)
15.243 - have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
15.244 - from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
15.245 - from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
15.246 - from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
15.247 - from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
15.248 - by simp
15.249 - from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
15.250 - crel_mapM_map_entry_remains[OF this, of "Heap.length a h - Suc n", symmetric] less less2
15.251 - show ?case
15.252 - by (auto simp add: nth_list_update_eq Heap.length_def)
15.253 -qed
15.254 -
15.255 -lemma crel_mapM_map_entry_length:
15.256 - assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
15.257 - assumes "n \<le> Heap.length a h"
15.258 - shows "Heap.length a h' = Heap.length a h"
15.259 -using assms
15.260 -proof (induct n arbitrary: h h' r)
15.261 - case 0
15.262 - thus ?case by (auto elim!: crel_return)
15.263 -next
15.264 - case (Suc n)
15.265 - let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
15.266 - from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
15.267 - by (simp add: upt_conv_Cons')
15.268 - from Suc(2) this obtain r where
15.269 - crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
15.270 - by (auto elim!: crelE crel_map_entry crel_return)
15.271 - have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
15.272 - from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
15.273 - by simp
15.274 - from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
15.275 -qed
15.276 -
15.277 -lemma crel_mapM_map_entry:
15.278 -assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Heap.length a h]) h h' r"
15.279 - shows "get_array a h' = List.map f (get_array a h)"
15.280 -proof -
15.281 - from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - Heap.length a h..<Heap.length a h]) h h' r" by simp
15.282 - from crel_mapM_map_entry_length[OF this]
15.283 - crel_mapM_map_entry_changes[OF this] show ?thesis
15.284 - unfolding Heap.length_def
15.285 - by (auto intro: nth_equalityI)
15.286 -qed
15.287 -
15.288 -lemma crel_map_weak:
15.289 - assumes crel_map: "crel (Array.map f a) h h' r"
15.290 - obtains "r = a" "get_array a h' = List.map f (get_array a h)"
15.291 -proof
15.292 - from assms crel_mapM_map_entry show "get_array a h' = List.map f (get_array a h)"
15.293 - unfolding Array.map_def
15.294 - by (fastsimp elim!: crelE crel_length crel_return)
15.295 - from assms show "r = a"
15.296 - unfolding Array.map_def
15.297 - by (elim crelE crel_return)
15.298 -qed
15.299 -
15.300 -subsection {* Elimination rules for reference commands *}
15.301 -
15.302 -(* TODO:
15.303 -maybe introduce a new predicate "extends h' h x"
15.304 -which means h' extends h with a new reference x.
15.305 -Then crel_new: would be
15.306 -assumes "crel (Ref.new v) h h' x"
15.307 -obtains "get_ref x h' = v"
15.308 -and "extends h' h x"
15.309 -
15.310 -and we would need further rules for extends:
15.311 -extends h' h x \<Longrightarrow> \<not> ref_present x h
15.312 -extends h' h x \<Longrightarrow> ref_present x h'
15.313 -extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> ref_present y h'
15.314 -extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> get_ref y h = get_ref y h'
15.315 -extends h' h x \<Longrightarrow> lim h' = Suc (lim h)
15.316 -*)
15.317 -
15.318 -lemma crel_Ref_new:
15.319 - assumes "crel (Ref.new v) h h' x"
15.320 - obtains "get_ref x h' = v"
15.321 - and "\<not> ref_present x h"
15.322 - and "ref_present x h'"
15.323 - and "\<forall>y. ref_present y h \<longrightarrow> get_ref y h = get_ref y h'"
15.324 - (* and "lim h' = Suc (lim h)" *)
15.325 - and "\<forall>y. ref_present y h \<longrightarrow> ref_present y h'"
15.326 - using assms
15.327 - unfolding Ref.new_def
15.328 - apply (elim crel_heap)
15.329 - unfolding Heap.ref_def
15.330 - apply (simp add: Let_def)
15.331 - unfolding Heap.new_ref_def
15.332 - apply (simp add: Let_def)
15.333 - unfolding ref_present_def
15.334 - apply auto
15.335 - unfolding get_ref_def set_ref_def
15.336 - apply auto
15.337 - done
15.338 -
15.339 -lemma crel_lookup:
15.340 - assumes "crel (!ref) h h' r"
15.341 - obtains "h = h'" "r = get_ref ref h"
15.342 -using assms
15.343 -unfolding Ref.lookup_def
15.344 -by (auto elim: crel_heap)
15.345 -
15.346 -lemma crel_update:
15.347 - assumes "crel (ref := v) h h' r"
15.348 - obtains "h' = set_ref ref v h" "r = ()"
15.349 -using assms
15.350 -unfolding Ref.update_def
15.351 -by (auto elim: crel_heap)
15.352 -
15.353 -lemma crel_change:
15.354 - assumes "crel (Ref.change f ref) h h' r"
15.355 - obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
15.356 -using assms
15.357 -unfolding Ref.change_def Let_def
15.358 -by (auto elim!: crelE crel_lookup crel_update crel_return)
15.359 -
15.360 -subsection {* Elimination rules for the assert command *}
15.361 -
15.362 -lemma crel_assert[consumes 1]:
15.363 - assumes "crel (assert P x) h h' r"
15.364 - obtains "P x" "r = x" "h = h'"
15.365 - using assms
15.366 - unfolding assert_def
15.367 - by (elim crel_if crel_return crel_raise) auto
15.368 -
15.369 -lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
15.370 -unfolding crel_def bindM_def Let_def assert_def
15.371 - raise_def return_def prod_case_beta
15.372 -apply (cases f)
15.373 -apply simp
15.374 -apply (simp add: expand_fun_eq split_def)
15.375 -apply auto
15.376 -apply (case_tac "fst (fun x)")
15.377 -apply (simp_all add: Pair_fst_snd_eq)
15.378 -apply (erule_tac x="x" in meta_allE)
15.379 -apply fastsimp
15.380 -done
15.381 -
15.382 -section {* Introduction rules *}
15.383 -
15.384 -subsection {* Introduction rules for basic monadic commands *}
15.385 -
15.386 -lemma crelI:
15.387 - assumes "crel f h h' r" "crel (g r) h' h'' r'"
15.388 - shows "crel (f >>= g) h h'' r'"
15.389 - using assms by (simp add: crel_def' bindM_def)
15.390 -
15.391 -lemma crelI':
15.392 - assumes "crel f h h' r" "crel g h' h'' r'"
15.393 - shows "crel (f >> g) h h'' r'"
15.394 - using assms by (intro crelI) auto
15.395 -
15.396 -lemma crel_returnI:
15.397 - shows "crel (return x) h h x"
15.398 - unfolding crel_def return_def by simp
15.399 -
15.400 -lemma crel_raiseI:
15.401 - shows "\<not> (crel (raise x) h h' r)"
15.402 - unfolding crel_def raise_def by simp
15.403 -
15.404 -lemma crel_ifI:
15.405 - assumes "c \<longrightarrow> crel t h h' r"
15.406 - "\<not>c \<longrightarrow> crel e h h' r"
15.407 - shows "crel (if c then t else e) h h' r"
15.408 - using assms
15.409 - unfolding crel_def by auto
15.410 -
15.411 -lemma crel_option_caseI:
15.412 - assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
15.413 - assumes "x = None \<Longrightarrow> crel n h h' r"
15.414 - shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
15.415 -using assms
15.416 -by (auto split: option.split)
15.417 -
15.418 -lemma crel_heapI:
15.419 - shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
15.420 - by (simp add: crel_def apfst_def split_def prod_fun_def)
15.421 -
15.422 -lemma crel_heapI':
15.423 - assumes "h' = snd (f h)" "r = fst (f h)"
15.424 - shows "crel (Heap_Monad.heap f) h h' r"
15.425 - using assms
15.426 - by (simp add: crel_def split_def apfst_def prod_fun_def)
15.427 -
15.428 -lemma crelI2:
15.429 - assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
15.430 - shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
15.431 - oops
15.432 -
15.433 -lemma crel_ifI2:
15.434 - assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
15.435 - "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
15.436 - shows "\<exists> h' r. crel (if c then t else e) h h' r"
15.437 - oops
15.438 -
15.439 -subsection {* Introduction rules for array commands *}
15.440 -
15.441 -lemma crel_lengthI:
15.442 - shows "crel (length a) h h (Heap.length a h)"
15.443 - unfolding length_def
15.444 - by (rule crel_heapI') auto
15.445 -
15.446 -(* thm crel_newI for Array.new is missing *)
15.447 -
15.448 -lemma crel_nthI:
15.449 - assumes "i < Heap.length a h"
15.450 - shows "crel (nth a i) h h ((get_array a h) ! i)"
15.451 - using assms
15.452 - unfolding nth_def
15.453 - by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
15.454 -
15.455 -lemma crel_updI:
15.456 - assumes "i < Heap.length a h"
15.457 - shows "crel (upd i v a) h (Heap.upd a i v h) a"
15.458 - using assms
15.459 - unfolding upd_def
15.460 - by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
15.461 - crel_lengthI crel_heapI')
15.462 -
15.463 -(* thm crel_of_listI is missing *)
15.464 -
15.465 -(* thm crel_map_entryI is missing *)
15.466 -
15.467 -(* thm crel_swapI is missing *)
15.468 -
15.469 -(* thm crel_makeI is missing *)
15.470 -
15.471 -(* thm crel_freezeI is missing *)
15.472 -
15.473 -(* thm crel_mapI is missing *)
15.474 -
15.475 -subsection {* Introduction rules for reference commands *}
15.476 -
15.477 -lemma crel_lookupI:
15.478 - shows "crel (!ref) h h (get_ref ref h)"
15.479 - unfolding lookup_def by (auto intro!: crel_heapI')
15.480 -
15.481 -lemma crel_updateI:
15.482 - shows "crel (ref := v) h (set_ref ref v h) ()"
15.483 - unfolding update_def by (auto intro!: crel_heapI')
15.484 -
15.485 -lemma crel_changeI:
15.486 - shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
15.487 -unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
15.488 -
15.489 -subsection {* Introduction rules for the assert command *}
15.490 -
15.491 -lemma crel_assertI:
15.492 - assumes "P x"
15.493 - shows "crel (assert P x) h h x"
15.494 - using assms
15.495 - unfolding assert_def
15.496 - by (auto intro!: crel_ifI crel_returnI crel_raiseI)
15.497 -
15.498 -section {* Defintion of the noError predicate *}
15.499 -
15.500 -text {* We add a simple definitional setting for crel intro rules
15.501 - where we only would like to show that the computation does not result in a exception for heap h,
15.502 - but we do not care about statements about the resulting heap and return value.*}
15.503 -
15.504 -definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
15.505 -where
15.506 - "noError c h \<longleftrightarrow> (\<exists>r h'. (Inl r, h') = Heap_Monad.execute c h)"
15.507 -
15.508 -lemma noError_def': -- FIXME
15.509 - "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = (Inl r, h'))"
15.510 - unfolding noError_def apply auto proof -
15.511 - fix r h'
15.512 - assume "(Inl r, h') = Heap_Monad.execute c h"
15.513 - then have "Heap_Monad.execute c h = (Inl r, h')" ..
15.514 - then show "\<exists>r h'. Heap_Monad.execute c h = (Inl r, h')" by blast
15.515 -qed
15.516 -
15.517 -subsection {* Introduction rules for basic monadic commands *}
15.518 -
15.519 -lemma noErrorI:
15.520 - assumes "noError f h"
15.521 - assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
15.522 - shows "noError (f \<guillemotright>= g) h"
15.523 - using assms
15.524 - by (auto simp add: noError_def' crel_def' bindM_def)
15.525 -
15.526 -lemma noErrorI':
15.527 - assumes "noError f h"
15.528 - assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
15.529 - shows "noError (f \<guillemotright> g) h"
15.530 - using assms
15.531 - by (auto simp add: noError_def' crel_def' bindM_def)
15.532 -
15.533 -lemma noErrorI2:
15.534 -"\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
15.535 -\<Longrightarrow> noError (f \<guillemotright>= g) h"
15.536 -by (auto simp add: noError_def' crel_def' bindM_def)
15.537 -
15.538 -lemma noError_return:
15.539 - shows "noError (return x) h"
15.540 - unfolding noError_def return_def
15.541 - by auto
15.542 -
15.543 -lemma noError_if:
15.544 - assumes "c \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
15.545 - shows "noError (if c then t else e) h"
15.546 - using assms
15.547 - unfolding noError_def
15.548 - by auto
15.549 -
15.550 -lemma noError_option_case:
15.551 - assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
15.552 - assumes "noError n h"
15.553 - shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
15.554 -using assms
15.555 -by (auto split: option.split)
15.556 -
15.557 -lemma noError_mapM:
15.558 -assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)"
15.559 -shows "noError (mapM f xs) h"
15.560 -using assms
15.561 -proof (induct xs)
15.562 - case Nil
15.563 - thus ?case
15.564 - unfolding mapM.simps by (intro noError_return)
15.565 -next
15.566 - case (Cons x xs)
15.567 - thus ?case
15.568 - unfolding mapM.simps
15.569 - by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
15.570 -qed
15.571 -
15.572 -lemma noError_heap:
15.573 - shows "noError (Heap_Monad.heap f) h"
15.574 - by (simp add: noError_def' apfst_def prod_fun_def split_def)
15.575 -
15.576 -subsection {* Introduction rules for array commands *}
15.577 -
15.578 -lemma noError_length:
15.579 - shows "noError (Array.length a) h"
15.580 - unfolding length_def
15.581 - by (intro noError_heap)
15.582 -
15.583 -lemma noError_new:
15.584 - shows "noError (Array.new n v) h"
15.585 -unfolding Array.new_def by (intro noError_heap)
15.586 -
15.587 -lemma noError_upd:
15.588 - assumes "i < Heap.length a h"
15.589 - shows "noError (Array.upd i v a) h"
15.590 - using assms
15.591 - unfolding upd_def
15.592 - by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
15.593 -
15.594 -lemma noError_nth:
15.595 -assumes "i < Heap.length a h"
15.596 - shows "noError (Array.nth a i) h"
15.597 - using assms
15.598 - unfolding nth_def
15.599 - by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
15.600 -
15.601 -lemma noError_of_list:
15.602 - shows "noError (of_list ls) h"
15.603 - unfolding of_list_def by (rule noError_heap)
15.604 -
15.605 -lemma noError_map_entry:
15.606 - assumes "i < Heap.length a h"
15.607 - shows "noError (map_entry i f a) h"
15.608 - using assms
15.609 - unfolding map_entry_def
15.610 - by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
15.611 -
15.612 -lemma noError_swap:
15.613 - assumes "i < Heap.length a h"
15.614 - shows "noError (swap i x a) h"
15.615 - using assms
15.616 - unfolding swap_def
15.617 - by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
15.618 -
15.619 -lemma noError_make:
15.620 - shows "noError (make n f) h"
15.621 - unfolding make_def
15.622 - by (auto intro: noError_of_list)
15.623 -
15.624 -(*TODO: move to HeapMonad *)
15.625 -lemma mapM_append:
15.626 - "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
15.627 - by (induct xs) (simp_all add: monad_simp)
15.628 -
15.629 -lemma noError_freeze:
15.630 - shows "noError (freeze a) h"
15.631 -unfolding freeze_def
15.632 -by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
15.633 - noError_nth crel_nthI elim: crel_length)
15.634 -
15.635 -lemma noError_mapM_map_entry:
15.636 - assumes "n \<le> Heap.length a h"
15.637 - shows "noError (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h"
15.638 -using assms
15.639 -proof (induct n arbitrary: h)
15.640 - case 0
15.641 - thus ?case by (auto intro: noError_return)
15.642 -next
15.643 - case (Suc n)
15.644 - from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
15.645 - by (simp add: upt_conv_Cons')
15.646 - with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
15.647 - by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
15.648 -qed
15.649 -
15.650 -lemma noError_map:
15.651 - shows "noError (Array.map f a) h"
15.652 -using noError_mapM_map_entry[of "Heap.length a h" a h]
15.653 -unfolding Array.map_def
15.654 -by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
15.655 -
15.656 -subsection {* Introduction rules for the reference commands *}
15.657 -
15.658 -lemma noError_Ref_new:
15.659 - shows "noError (Ref.new v) h"
15.660 -unfolding Ref.new_def by (intro noError_heap)
15.661 -
15.662 -lemma noError_lookup:
15.663 - shows "noError (!ref) h"
15.664 - unfolding lookup_def by (intro noError_heap)
15.665 -
15.666 -lemma noError_update:
15.667 - shows "noError (ref := v) h"
15.668 - unfolding update_def by (intro noError_heap)
15.669 -
15.670 -lemma noError_change:
15.671 - shows "noError (Ref.change f ref) h"
15.672 - unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
15.673 -
15.674 -subsection {* Introduction rules for the assert command *}
15.675 -
15.676 -lemma noError_assert:
15.677 - assumes "P x"
15.678 - shows "noError (assert P x) h"
15.679 - using assms
15.680 - unfolding assert_def
15.681 - by (auto intro: noError_if noError_return)
15.682 -
15.683 -section {* Cumulative lemmas *}
15.684 -
15.685 -lemmas crel_elim_all =
15.686 - crelE crelE' crel_return crel_raise crel_if crel_option_case
15.687 - crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze crel_map_weak
15.688 - crel_Ref_new crel_lookup crel_update crel_change
15.689 - crel_assert
15.690 -
15.691 -lemmas crel_intro_all =
15.692 - crelI crelI' crel_returnI crel_raiseI crel_ifI crel_option_caseI
15.693 - crel_lengthI (* crel_newI *) crel_nthI crel_updI (* crel_of_listI crel_map_entryI crel_swapI crel_makeI crel_freezeI crel_mapI *)
15.694 - (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
15.695 - crel_assert
15.696 -
15.697 -lemmas noError_intro_all =
15.698 - noErrorI noErrorI' noError_return noError_if noError_option_case
15.699 - noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze noError_map
15.700 - noError_Ref_new noError_lookup noError_update noError_change
15.701 - noError_assert
15.702 -
15.703 -end
15.704 \ No newline at end of file
16.1 --- a/src/HOL/Library/Subarray.thy Thu Jan 08 10:53:48 2009 +0100
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,66 +0,0 @@
16.4 -theory Subarray
16.5 -imports Array Sublist
16.6 -begin
16.7 -
16.8 -definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
16.9 -where
16.10 - "subarray n m a h \<equiv> sublist' n m (get_array a h)"
16.11 -
16.12 -lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
16.13 -apply (simp add: subarray_def Heap.upd_def)
16.14 -apply (simp add: sublist'_update1)
16.15 -done
16.16 -
16.17 -lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
16.18 -apply (simp add: subarray_def Heap.upd_def)
16.19 -apply (subst sublist'_update2)
16.20 -apply fastsimp
16.21 -apply simp
16.22 -done
16.23 -
16.24 -lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]"
16.25 -unfolding subarray_def Heap.upd_def
16.26 -by (simp add: sublist'_update3)
16.27 -
16.28 -lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
16.29 -by (simp add: subarray_def sublist'_Nil')
16.30 -
16.31 -lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]"
16.32 -by (simp add: subarray_def Heap.length_def sublist'_single)
16.33 -
16.34 -lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
16.35 -by (simp add: subarray_def Heap.length_def length_sublist')
16.36 -
16.37 -lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
16.38 -by (simp add: length_subarray)
16.39 -
16.40 -lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
16.41 -unfolding Heap.length_def subarray_def
16.42 -by (simp add: sublist'_front)
16.43 -
16.44 -lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
16.45 -unfolding Heap.length_def subarray_def
16.46 -by (simp add: sublist'_back)
16.47 -
16.48 -lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
16.49 -unfolding subarray_def
16.50 -by (simp add: sublist'_append)
16.51 -
16.52 -lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
16.53 -unfolding Heap.length_def subarray_def
16.54 -by (simp add: sublist'_all)
16.55 -
16.56 -lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
16.57 -unfolding Heap.length_def subarray_def
16.58 -by (simp add: nth_sublist')
16.59 -
16.60 -lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
16.61 -unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
16.62 -
16.63 -lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
16.64 -unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
16.65 -
16.66 -lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
16.67 -unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
16.68 -
16.69 -end
16.70 \ No newline at end of file
17.1 --- a/src/HOL/Library/Sublist.thy Thu Jan 08 10:53:48 2009 +0100
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,507 +0,0 @@
17.4 -(* $Id$ *)
17.5 -
17.6 -header {* Slices of lists *}
17.7 -
17.8 -theory Sublist
17.9 -imports Multiset
17.10 -begin
17.11 -
17.12 -
17.13 -lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}"
17.14 -apply (induct xs arbitrary: i j k)
17.15 -apply simp
17.16 -apply (simp only: sublist_Cons)
17.17 -apply simp
17.18 -apply safe
17.19 -apply simp
17.20 -apply (erule_tac x="0" in meta_allE)
17.21 -apply (erule_tac x="j - 1" in meta_allE)
17.22 -apply (erule_tac x="k - 1" in meta_allE)
17.23 -apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
17.24 -apply simp
17.25 -apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
17.26 -apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
17.27 -apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
17.28 -apply simp
17.29 -apply fastsimp
17.30 -apply fastsimp
17.31 -apply fastsimp
17.32 -apply fastsimp
17.33 -apply (erule_tac x="i - 1" in meta_allE)
17.34 -apply (erule_tac x="j - 1" in meta_allE)
17.35 -apply (erule_tac x="k - 1" in meta_allE)
17.36 -apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
17.37 -apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
17.38 -apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
17.39 -apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
17.40 -apply simp
17.41 -apply fastsimp
17.42 -apply fastsimp
17.43 -apply fastsimp
17.44 -apply fastsimp
17.45 -done
17.46 -
17.47 -lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
17.48 -apply (induct xs arbitrary: i inds)
17.49 -apply simp
17.50 -apply (case_tac i)
17.51 -apply (simp add: sublist_Cons)
17.52 -apply (simp add: sublist_Cons)
17.53 -done
17.54 -
17.55 -lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
17.56 -proof (induct xs arbitrary: i inds)
17.57 - case Nil thus ?case by simp
17.58 -next
17.59 - case (Cons x xs)
17.60 - thus ?case
17.61 - proof (cases i)
17.62 - case 0 with Cons show ?thesis by (simp add: sublist_Cons)
17.63 - next
17.64 - case (Suc i')
17.65 - with Cons show ?thesis
17.66 - apply simp
17.67 - apply (simp add: sublist_Cons)
17.68 - apply auto
17.69 - apply (auto simp add: nat.split)
17.70 - apply (simp add: card_less)
17.71 - apply (simp add: card_less)
17.72 - apply (simp add: card_less_Suc[symmetric])
17.73 - apply (simp add: card_less_Suc2)
17.74 - done
17.75 - qed
17.76 -qed
17.77 -
17.78 -lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
17.79 -by (simp add: sublist_update1 sublist_update2)
17.80 -
17.81 -lemma sublist_take: "sublist xs {j. j < m} = take m xs"
17.82 -apply (induct xs arbitrary: m)
17.83 -apply simp
17.84 -apply (case_tac m)
17.85 -apply simp
17.86 -apply (simp add: sublist_Cons)
17.87 -done
17.88 -
17.89 -lemma sublist_take': "sublist xs {0..<m} = take m xs"
17.90 -apply (induct xs arbitrary: m)
17.91 -apply simp
17.92 -apply (case_tac m)
17.93 -apply simp
17.94 -apply (simp add: sublist_Cons sublist_take)
17.95 -done
17.96 -
17.97 -lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
17.98 -apply (induct xs)
17.99 -apply simp
17.100 -apply (simp add: sublist_Cons)
17.101 -done
17.102 -
17.103 -lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
17.104 -apply (induct xs)
17.105 -apply simp
17.106 -apply (simp add: sublist_Cons)
17.107 -done
17.108 -
17.109 -lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
17.110 -apply (induct xs arbitrary: a)
17.111 -apply simp
17.112 -apply(case_tac aa)
17.113 -apply simp
17.114 -apply (simp add: sublist_Cons)
17.115 -apply simp
17.116 -apply (simp add: sublist_Cons)
17.117 -done
17.118 -
17.119 -lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []"
17.120 -apply (induct xs arbitrary: inds)
17.121 -apply simp
17.122 -apply (simp add: sublist_Cons)
17.123 -apply auto
17.124 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
17.125 -apply auto
17.126 -done
17.127 -
17.128 -lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
17.129 -apply (induct xs arbitrary: inds)
17.130 -apply simp
17.131 -apply (simp add: sublist_Cons)
17.132 -apply (auto split: if_splits)
17.133 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
17.134 -apply (case_tac x, auto)
17.135 -done
17.136 -
17.137 -lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
17.138 -apply (induct xs arbitrary: inds)
17.139 -apply simp
17.140 -apply (simp add: sublist_Cons)
17.141 -apply auto
17.142 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
17.143 -apply (case_tac x, auto)
17.144 -done
17.145 -
17.146 -lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
17.147 -apply (induct xs arbitrary: ys inds inds')
17.148 -apply simp
17.149 -apply (drule sym, rule sym)
17.150 -apply (simp add: sublist_Nil, fastsimp)
17.151 -apply (case_tac ys)
17.152 -apply (simp add: sublist_Nil, fastsimp)
17.153 -apply (auto simp add: sublist_Cons)
17.154 -apply (erule_tac x="list" in meta_allE)
17.155 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
17.156 -apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
17.157 -apply fastsimp
17.158 -apply (erule_tac x="list" in meta_allE)
17.159 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
17.160 -apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
17.161 -apply fastsimp
17.162 -done
17.163 -
17.164 -lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
17.165 -apply (induct xs arbitrary: ys inds)
17.166 -apply simp
17.167 -apply (rule sym, simp add: sublist_Nil)
17.168 -apply (case_tac ys)
17.169 -apply (simp add: sublist_Nil)
17.170 -apply (auto simp add: sublist_Cons)
17.171 -apply (erule_tac x="list" in meta_allE)
17.172 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
17.173 -apply fastsimp
17.174 -apply (erule_tac x="list" in meta_allE)
17.175 -apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
17.176 -apply fastsimp
17.177 -done
17.178 -
17.179 -lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
17.180 -by (rule sublist_eq, auto)
17.181 -
17.182 -lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
17.183 -apply (induct xs arbitrary: ys inds)
17.184 -apply simp
17.185 -apply (rule sym, simp add: sublist_Nil)
17.186 -apply (case_tac ys)
17.187 -apply (simp add: sublist_Nil)
17.188 -apply (auto simp add: sublist_Cons)
17.189 -apply (case_tac i)
17.190 -apply auto
17.191 -apply (case_tac i)
17.192 -apply auto
17.193 -done
17.194 -
17.195 -section {* Another sublist function *}
17.196 -
17.197 -function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
17.198 -where
17.199 - "sublist' n m [] = []"
17.200 -| "sublist' n 0 xs = []"
17.201 -| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
17.202 -| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
17.203 -by pat_completeness auto
17.204 -termination by lexicographic_order
17.205 -
17.206 -subsection {* Proving equivalence to the other sublist command *}
17.207 -
17.208 -lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
17.209 -apply (induct xs arbitrary: n m)
17.210 -apply simp
17.211 -apply (case_tac n)
17.212 -apply (case_tac m)
17.213 -apply simp
17.214 -apply (simp add: sublist_Cons)
17.215 -apply (case_tac m)
17.216 -apply simp
17.217 -apply (simp add: sublist_Cons)
17.218 -done
17.219 -
17.220 -
17.221 -lemma "sublist' n m xs = sublist xs {n..<m}"
17.222 -apply (induct xs arbitrary: n m)
17.223 -apply simp
17.224 -apply (case_tac n, case_tac m)
17.225 -apply simp
17.226 -apply simp
17.227 -apply (simp add: sublist_take')
17.228 -apply (case_tac m)
17.229 -apply simp
17.230 -apply (simp add: sublist_Cons sublist'_sublist)
17.231 -done
17.232 -
17.233 -
17.234 -subsection {* Showing equivalence to use of drop and take for definition *}
17.235 -
17.236 -lemma "sublist' n m xs = take (m - n) (drop n xs)"
17.237 -apply (induct xs arbitrary: n m)
17.238 -apply simp
17.239 -apply (case_tac m)
17.240 -apply simp
17.241 -apply (case_tac n)
17.242 -apply simp
17.243 -apply simp
17.244 -done
17.245 -
17.246 -subsection {* General lemma about sublist *}
17.247 -
17.248 -lemma sublist'_Nil[simp]: "sublist' i j [] = []"
17.249 -by simp
17.250 -
17.251 -lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow> sublist' i' j xs)"
17.252 -by (cases i) auto
17.253 -
17.254 -lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
17.255 -apply (cases j)
17.256 -apply auto
17.257 -apply (cases i)
17.258 -apply auto
17.259 -done
17.260 -
17.261 -lemma sublist_n_0: "sublist' n 0 xs = []"
17.262 -by (induct xs, auto)
17.263 -
17.264 -lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
17.265 -apply (induct xs arbitrary: n m)
17.266 -apply simp
17.267 -apply (case_tac m)
17.268 -apply simp
17.269 -apply (case_tac n)
17.270 -apply simp
17.271 -apply simp
17.272 -done
17.273 -
17.274 -lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
17.275 -apply (induct xs arbitrary: n m)
17.276 -apply simp
17.277 -apply (case_tac m)
17.278 -apply simp
17.279 -apply (case_tac n)
17.280 -apply simp
17.281 -apply simp
17.282 -done
17.283 -
17.284 -lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
17.285 -apply (induct xs arbitrary: n m)
17.286 -apply simp
17.287 -apply (case_tac m)
17.288 -apply simp
17.289 -apply (case_tac n)
17.290 -apply simp
17.291 -apply simp
17.292 -done
17.293 -
17.294 -lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
17.295 -apply (induct xs arbitrary: n m)
17.296 -apply simp
17.297 -apply (case_tac m)
17.298 -apply simp
17.299 -apply (case_tac n)
17.300 -apply simp
17.301 -apply simp
17.302 -done
17.303 -
17.304 -lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
17.305 -apply (induct xs arbitrary: n)
17.306 -apply simp
17.307 -apply simp
17.308 -apply (case_tac n)
17.309 -apply (simp add: sublist_n_0)
17.310 -apply simp
17.311 -done
17.312 -
17.313 -lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
17.314 -apply (induct xs arbitrary: n m i)
17.315 -apply simp
17.316 -apply simp
17.317 -apply (case_tac i)
17.318 -apply simp
17.319 -apply simp
17.320 -done
17.321 -
17.322 -lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
17.323 -apply (induct xs arbitrary: n m i)
17.324 -apply simp
17.325 -apply simp
17.326 -apply (case_tac i)
17.327 -apply simp
17.328 -apply simp
17.329 -done
17.330 -
17.331 -lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
17.332 -proof (induct xs arbitrary: n m i)
17.333 - case Nil thus ?case by auto
17.334 -next
17.335 - case (Cons x xs)
17.336 - thus ?case
17.337 - apply -
17.338 - apply auto
17.339 - apply (cases i)
17.340 - apply auto
17.341 - apply (cases i)
17.342 - apply auto
17.343 - done
17.344 -qed
17.345 -
17.346 -lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
17.347 -proof (induct xs arbitrary: i j ys n m)
17.348 - case Nil
17.349 - thus ?case
17.350 - apply -
17.351 - apply (rule sym, drule sym)
17.352 - apply (simp add: sublist'_Nil)
17.353 - apply (simp add: sublist'_Nil3)
17.354 - apply arith
17.355 - done
17.356 -next
17.357 - case (Cons x xs i j ys n m)
17.358 - note c = this
17.359 - thus ?case
17.360 - proof (cases m)
17.361 - case 0 thus ?thesis by (simp add: sublist_n_0)
17.362 - next
17.363 - case (Suc m')
17.364 - note a = this
17.365 - thus ?thesis
17.366 - proof (cases n)
17.367 - case 0 note b = this
17.368 - show ?thesis
17.369 - proof (cases ys)
17.370 - case Nil with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
17.371 - next
17.372 - case (Cons y ys)
17.373 - show ?thesis
17.374 - proof (cases j)
17.375 - case 0 with a b Cons.prems show ?thesis by simp
17.376 - next
17.377 - case (Suc j') with a b Cons.prems Cons show ?thesis
17.378 - apply -
17.379 - apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
17.380 - done
17.381 - qed
17.382 - qed
17.383 - next
17.384 - case (Suc n')
17.385 - show ?thesis
17.386 - proof (cases ys)
17.387 - case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
17.388 - next
17.389 - case (Cons y ys) with Suc a Cons.prems show ?thesis
17.390 - apply -
17.391 - apply simp
17.392 - apply (cases j)
17.393 - apply simp
17.394 - apply (cases i)
17.395 - apply simp
17.396 - apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
17.397 - apply simp
17.398 - apply simp
17.399 - apply simp
17.400 - apply simp
17.401 - apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
17.402 - apply simp
17.403 - apply simp
17.404 - apply simp
17.405 - done
17.406 - qed
17.407 - qed
17.408 - qed
17.409 -qed
17.410 -
17.411 -lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
17.412 -by (induct xs arbitrary: i j, auto)
17.413 -
17.414 -lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
17.415 -apply (induct xs arbitrary: a i j)
17.416 -apply simp
17.417 -apply (case_tac j)
17.418 -apply simp
17.419 -apply (case_tac i)
17.420 -apply simp
17.421 -apply simp
17.422 -done
17.423 -
17.424 -lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
17.425 -apply (induct xs arbitrary: a i j)
17.426 -apply simp
17.427 -apply simp
17.428 -apply (case_tac j)
17.429 -apply simp
17.430 -apply auto
17.431 -apply (case_tac nat)
17.432 -apply auto
17.433 -done
17.434 -
17.435 -(* suffices that j \<le> length xs and length ys *)
17.436 -lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
17.437 -proof (induct xs arbitrary: ys i j)
17.438 - case Nil thus ?case by simp
17.439 -next
17.440 - case (Cons x xs)
17.441 - thus ?case
17.442 - apply -
17.443 - apply (cases ys)
17.444 - apply simp
17.445 - apply simp
17.446 - apply auto
17.447 - apply (case_tac i', auto)
17.448 - apply (erule_tac x="Suc i'" in allE, auto)
17.449 - apply (erule_tac x="i' - 1" in allE, auto)
17.450 - apply (case_tac i', auto)
17.451 - apply (erule_tac x="Suc i'" in allE, auto)
17.452 - done
17.453 -qed
17.454 -
17.455 -lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
17.456 -by (induct xs, auto)
17.457 -
17.458 -lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs"
17.459 -by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
17.460 -
17.461 -lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
17.462 -by (induct xs arbitrary: i j k) auto
17.463 -
17.464 -lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
17.465 -apply (induct xs arbitrary: i j k)
17.466 -apply auto
17.467 -apply (case_tac k)
17.468 -apply auto
17.469 -apply (case_tac i)
17.470 -apply auto
17.471 -done
17.472 -
17.473 -lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
17.474 -apply (simp add: sublist'_sublist)
17.475 -apply (simp add: set_sublist)
17.476 -apply auto
17.477 -done
17.478 -
17.479 -lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
17.480 -unfolding set_sublist' by blast
17.481 -
17.482 -lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
17.483 -unfolding set_sublist' by blast
17.484 -
17.485 -
17.486 -lemma multiset_of_sublist:
17.487 -assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
17.488 -assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
17.489 -assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
17.490 -assumes multiset: "multiset_of xs = multiset_of ys"
17.491 - shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
17.492 -proof -
17.493 - from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long")
17.494 - by (simp add: sublist'_append)
17.495 - from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
17.496 - with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long")
17.497 - by (simp add: sublist'_append)
17.498 - from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
17.499 - moreover
17.500 - from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
17.501 - by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
17.502 - moreover
17.503 - from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
17.504 - by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
17.505 - moreover
17.506 - ultimately show ?thesis by (simp add: multiset_of_append)
17.507 -qed
17.508 -
17.509 -
17.510 -end
18.1 --- a/src/HOL/ex/ImperativeQuicksort.thy Thu Jan 08 10:53:48 2009 +0100
18.2 +++ b/src/HOL/ex/ImperativeQuicksort.thy Thu Jan 08 17:10:41 2009 +0100
18.3 @@ -1,5 +1,5 @@
18.4 theory ImperativeQuicksort
18.5 -imports Imperative_HOL Subarray Multiset Efficient_Nat
18.6 +imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
18.7 begin
18.8
18.9 text {* We prove QuickSort correct in the Relational Calculus. *}
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/HOL/ex/Subarray.thy Thu Jan 08 17:10:41 2009 +0100
19.3 @@ -0,0 +1,66 @@
19.4 +theory Subarray
19.5 +imports Array Sublist
19.6 +begin
19.7 +
19.8 +definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list"
19.9 +where
19.10 + "subarray n m a h \<equiv> sublist' n m (get_array a h)"
19.11 +
19.12 +lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
19.13 +apply (simp add: subarray_def Heap.upd_def)
19.14 +apply (simp add: sublist'_update1)
19.15 +done
19.16 +
19.17 +lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h"
19.18 +apply (simp add: subarray_def Heap.upd_def)
19.19 +apply (subst sublist'_update2)
19.20 +apply fastsimp
19.21 +apply simp
19.22 +done
19.23 +
19.24 +lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Heap.upd a i v h) = subarray n m a h[i - n := v]"
19.25 +unfolding subarray_def Heap.upd_def
19.26 +by (simp add: sublist'_update3)
19.27 +
19.28 +lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
19.29 +by (simp add: subarray_def sublist'_Nil')
19.30 +
19.31 +lemma subarray_single: "\<lbrakk> n < Heap.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]"
19.32 +by (simp add: subarray_def Heap.length_def sublist'_single)
19.33 +
19.34 +lemma length_subarray: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
19.35 +by (simp add: subarray_def Heap.length_def length_sublist')
19.36 +
19.37 +lemma length_subarray_0: "m \<le> Heap.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
19.38 +by (simp add: length_subarray)
19.39 +
19.40 +lemma subarray_nth_array_Cons: "\<lbrakk> i < Heap.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
19.41 +unfolding Heap.length_def subarray_def
19.42 +by (simp add: sublist'_front)
19.43 +
19.44 +lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Heap.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
19.45 +unfolding Heap.length_def subarray_def
19.46 +by (simp add: sublist'_back)
19.47 +
19.48 +lemma subarray_append: "\<lbrakk> i < j; j < k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
19.49 +unfolding subarray_def
19.50 +by (simp add: sublist'_append)
19.51 +
19.52 +lemma subarray_all: "subarray 0 (Heap.length a h) a h = get_array a h"
19.53 +unfolding Heap.length_def subarray_def
19.54 +by (simp add: sublist'_all)
19.55 +
19.56 +lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Heap.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
19.57 +unfolding Heap.length_def subarray_def
19.58 +by (simp add: nth_sublist')
19.59 +
19.60 +lemma subarray_eq_samelength_iff: "Heap.length a h = Heap.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
19.61 +unfolding Heap.length_def subarray_def by (rule sublist'_eq_samelength_iff)
19.62 +
19.63 +lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
19.64 +unfolding subarray_def Heap.length_def by (rule all_in_set_sublist'_conv)
19.65 +
19.66 +lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Heap.length a h \<longrightarrow> P (get_array a h ! k))"
19.67 +unfolding subarray_def Heap.length_def by (rule ball_in_set_sublist'_conv)
19.68 +
19.69 +end
19.70 \ No newline at end of file
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/HOL/ex/Sublist.thy Thu Jan 08 17:10:41 2009 +0100
20.3 @@ -0,0 +1,507 @@
20.4 +(* $Id$ *)
20.5 +
20.6 +header {* Slices of lists *}
20.7 +
20.8 +theory Sublist
20.9 +imports Multiset
20.10 +begin
20.11 +
20.12 +
20.13 +lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}"
20.14 +apply (induct xs arbitrary: i j k)
20.15 +apply simp
20.16 +apply (simp only: sublist_Cons)
20.17 +apply simp
20.18 +apply safe
20.19 +apply simp
20.20 +apply (erule_tac x="0" in meta_allE)
20.21 +apply (erule_tac x="j - 1" in meta_allE)
20.22 +apply (erule_tac x="k - 1" in meta_allE)
20.23 +apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
20.24 +apply simp
20.25 +apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
20.26 +apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
20.27 +apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
20.28 +apply simp
20.29 +apply fastsimp
20.30 +apply fastsimp
20.31 +apply fastsimp
20.32 +apply fastsimp
20.33 +apply (erule_tac x="i - 1" in meta_allE)
20.34 +apply (erule_tac x="j - 1" in meta_allE)
20.35 +apply (erule_tac x="k - 1" in meta_allE)
20.36 +apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
20.37 +apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
20.38 +apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
20.39 +apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
20.40 +apply simp
20.41 +apply fastsimp
20.42 +apply fastsimp
20.43 +apply fastsimp
20.44 +apply fastsimp
20.45 +done
20.46 +
20.47 +lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
20.48 +apply (induct xs arbitrary: i inds)
20.49 +apply simp
20.50 +apply (case_tac i)
20.51 +apply (simp add: sublist_Cons)
20.52 +apply (simp add: sublist_Cons)
20.53 +done
20.54 +
20.55 +lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
20.56 +proof (induct xs arbitrary: i inds)
20.57 + case Nil thus ?case by simp
20.58 +next
20.59 + case (Cons x xs)
20.60 + thus ?case
20.61 + proof (cases i)
20.62 + case 0 with Cons show ?thesis by (simp add: sublist_Cons)
20.63 + next
20.64 + case (Suc i')
20.65 + with Cons show ?thesis
20.66 + apply simp
20.67 + apply (simp add: sublist_Cons)
20.68 + apply auto
20.69 + apply (auto simp add: nat.split)
20.70 + apply (simp add: card_less)
20.71 + apply (simp add: card_less)
20.72 + apply (simp add: card_less_Suc[symmetric])
20.73 + apply (simp add: card_less_Suc2)
20.74 + done
20.75 + qed
20.76 +qed
20.77 +
20.78 +lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
20.79 +by (simp add: sublist_update1 sublist_update2)
20.80 +
20.81 +lemma sublist_take: "sublist xs {j. j < m} = take m xs"
20.82 +apply (induct xs arbitrary: m)
20.83 +apply simp
20.84 +apply (case_tac m)
20.85 +apply simp
20.86 +apply (simp add: sublist_Cons)
20.87 +done
20.88 +
20.89 +lemma sublist_take': "sublist xs {0..<m} = take m xs"
20.90 +apply (induct xs arbitrary: m)
20.91 +apply simp
20.92 +apply (case_tac m)
20.93 +apply simp
20.94 +apply (simp add: sublist_Cons sublist_take)
20.95 +done
20.96 +
20.97 +lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
20.98 +apply (induct xs)
20.99 +apply simp
20.100 +apply (simp add: sublist_Cons)
20.101 +done
20.102 +
20.103 +lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
20.104 +apply (induct xs)
20.105 +apply simp
20.106 +apply (simp add: sublist_Cons)
20.107 +done
20.108 +
20.109 +lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
20.110 +apply (induct xs arbitrary: a)
20.111 +apply simp
20.112 +apply(case_tac aa)
20.113 +apply simp
20.114 +apply (simp add: sublist_Cons)
20.115 +apply simp
20.116 +apply (simp add: sublist_Cons)
20.117 +done
20.118 +
20.119 +lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []"
20.120 +apply (induct xs arbitrary: inds)
20.121 +apply simp
20.122 +apply (simp add: sublist_Cons)
20.123 +apply auto
20.124 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
20.125 +apply auto
20.126 +done
20.127 +
20.128 +lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
20.129 +apply (induct xs arbitrary: inds)
20.130 +apply simp
20.131 +apply (simp add: sublist_Cons)
20.132 +apply (auto split: if_splits)
20.133 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
20.134 +apply (case_tac x, auto)
20.135 +done
20.136 +
20.137 +lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
20.138 +apply (induct xs arbitrary: inds)
20.139 +apply simp
20.140 +apply (simp add: sublist_Cons)
20.141 +apply auto
20.142 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
20.143 +apply (case_tac x, auto)
20.144 +done
20.145 +
20.146 +lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
20.147 +apply (induct xs arbitrary: ys inds inds')
20.148 +apply simp
20.149 +apply (drule sym, rule sym)
20.150 +apply (simp add: sublist_Nil, fastsimp)
20.151 +apply (case_tac ys)
20.152 +apply (simp add: sublist_Nil, fastsimp)
20.153 +apply (auto simp add: sublist_Cons)
20.154 +apply (erule_tac x="list" in meta_allE)
20.155 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
20.156 +apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
20.157 +apply fastsimp
20.158 +apply (erule_tac x="list" in meta_allE)
20.159 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
20.160 +apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
20.161 +apply fastsimp
20.162 +done
20.163 +
20.164 +lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
20.165 +apply (induct xs arbitrary: ys inds)
20.166 +apply simp
20.167 +apply (rule sym, simp add: sublist_Nil)
20.168 +apply (case_tac ys)
20.169 +apply (simp add: sublist_Nil)
20.170 +apply (auto simp add: sublist_Cons)
20.171 +apply (erule_tac x="list" in meta_allE)
20.172 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
20.173 +apply fastsimp
20.174 +apply (erule_tac x="list" in meta_allE)
20.175 +apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
20.176 +apply fastsimp
20.177 +done
20.178 +
20.179 +lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
20.180 +by (rule sublist_eq, auto)
20.181 +
20.182 +lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
20.183 +apply (induct xs arbitrary: ys inds)
20.184 +apply simp
20.185 +apply (rule sym, simp add: sublist_Nil)
20.186 +apply (case_tac ys)
20.187 +apply (simp add: sublist_Nil)
20.188 +apply (auto simp add: sublist_Cons)
20.189 +apply (case_tac i)
20.190 +apply auto
20.191 +apply (case_tac i)
20.192 +apply auto
20.193 +done
20.194 +
20.195 +section {* Another sublist function *}
20.196 +
20.197 +function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
20.198 +where
20.199 + "sublist' n m [] = []"
20.200 +| "sublist' n 0 xs = []"
20.201 +| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
20.202 +| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
20.203 +by pat_completeness auto
20.204 +termination by lexicographic_order
20.205 +
20.206 +subsection {* Proving equivalence to the other sublist command *}
20.207 +
20.208 +lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
20.209 +apply (induct xs arbitrary: n m)
20.210 +apply simp
20.211 +apply (case_tac n)
20.212 +apply (case_tac m)
20.213 +apply simp
20.214 +apply (simp add: sublist_Cons)
20.215 +apply (case_tac m)
20.216 +apply simp
20.217 +apply (simp add: sublist_Cons)
20.218 +done
20.219 +
20.220 +
20.221 +lemma "sublist' n m xs = sublist xs {n..<m}"
20.222 +apply (induct xs arbitrary: n m)
20.223 +apply simp
20.224 +apply (case_tac n, case_tac m)
20.225 +apply simp
20.226 +apply simp
20.227 +apply (simp add: sublist_take')
20.228 +apply (case_tac m)
20.229 +apply simp
20.230 +apply (simp add: sublist_Cons sublist'_sublist)
20.231 +done
20.232 +
20.233 +
20.234 +subsection {* Showing equivalence to use of drop and take for definition *}
20.235 +
20.236 +lemma "sublist' n m xs = take (m - n) (drop n xs)"
20.237 +apply (induct xs arbitrary: n m)
20.238 +apply simp
20.239 +apply (case_tac m)
20.240 +apply simp
20.241 +apply (case_tac n)
20.242 +apply simp
20.243 +apply simp
20.244 +done
20.245 +
20.246 +subsection {* General lemma about sublist *}
20.247 +
20.248 +lemma sublist'_Nil[simp]: "sublist' i j [] = []"
20.249 +by simp
20.250 +
20.251 +lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow> sublist' i' j xs)"
20.252 +by (cases i) auto
20.253 +
20.254 +lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
20.255 +apply (cases j)
20.256 +apply auto
20.257 +apply (cases i)
20.258 +apply auto
20.259 +done
20.260 +
20.261 +lemma sublist_n_0: "sublist' n 0 xs = []"
20.262 +by (induct xs, auto)
20.263 +
20.264 +lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
20.265 +apply (induct xs arbitrary: n m)
20.266 +apply simp
20.267 +apply (case_tac m)
20.268 +apply simp
20.269 +apply (case_tac n)
20.270 +apply simp
20.271 +apply simp
20.272 +done
20.273 +
20.274 +lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
20.275 +apply (induct xs arbitrary: n m)
20.276 +apply simp
20.277 +apply (case_tac m)
20.278 +apply simp
20.279 +apply (case_tac n)
20.280 +apply simp
20.281 +apply simp
20.282 +done
20.283 +
20.284 +lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
20.285 +apply (induct xs arbitrary: n m)
20.286 +apply simp
20.287 +apply (case_tac m)
20.288 +apply simp
20.289 +apply (case_tac n)
20.290 +apply simp
20.291 +apply simp
20.292 +done
20.293 +
20.294 +lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
20.295 +apply (induct xs arbitrary: n m)
20.296 +apply simp
20.297 +apply (case_tac m)
20.298 +apply simp
20.299 +apply (case_tac n)
20.300 +apply simp
20.301 +apply simp
20.302 +done
20.303 +
20.304 +lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
20.305 +apply (induct xs arbitrary: n)
20.306 +apply simp
20.307 +apply simp
20.308 +apply (case_tac n)
20.309 +apply (simp add: sublist_n_0)
20.310 +apply simp
20.311 +done
20.312 +
20.313 +lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
20.314 +apply (induct xs arbitrary: n m i)
20.315 +apply simp
20.316 +apply simp
20.317 +apply (case_tac i)
20.318 +apply simp
20.319 +apply simp
20.320 +done
20.321 +
20.322 +lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
20.323 +apply (induct xs arbitrary: n m i)
20.324 +apply simp
20.325 +apply simp
20.326 +apply (case_tac i)
20.327 +apply simp
20.328 +apply simp
20.329 +done
20.330 +
20.331 +lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
20.332 +proof (induct xs arbitrary: n m i)
20.333 + case Nil thus ?case by auto
20.334 +next
20.335 + case (Cons x xs)
20.336 + thus ?case
20.337 + apply -
20.338 + apply auto
20.339 + apply (cases i)
20.340 + apply auto
20.341 + apply (cases i)
20.342 + apply auto
20.343 + done
20.344 +qed
20.345 +
20.346 +lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
20.347 +proof (induct xs arbitrary: i j ys n m)
20.348 + case Nil
20.349 + thus ?case
20.350 + apply -
20.351 + apply (rule sym, drule sym)
20.352 + apply (simp add: sublist'_Nil)
20.353 + apply (simp add: sublist'_Nil3)
20.354 + apply arith
20.355 + done
20.356 +next
20.357 + case (Cons x xs i j ys n m)
20.358 + note c = this
20.359 + thus ?case
20.360 + proof (cases m)
20.361 + case 0 thus ?thesis by (simp add: sublist_n_0)
20.362 + next
20.363 + case (Suc m')
20.364 + note a = this
20.365 + thus ?thesis
20.366 + proof (cases n)
20.367 + case 0 note b = this
20.368 + show ?thesis
20.369 + proof (cases ys)
20.370 + case Nil with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
20.371 + next
20.372 + case (Cons y ys)
20.373 + show ?thesis
20.374 + proof (cases j)
20.375 + case 0 with a b Cons.prems show ?thesis by simp
20.376 + next
20.377 + case (Suc j') with a b Cons.prems Cons show ?thesis
20.378 + apply -
20.379 + apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
20.380 + done
20.381 + qed
20.382 + qed
20.383 + next
20.384 + case (Suc n')
20.385 + show ?thesis
20.386 + proof (cases ys)
20.387 + case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
20.388 + next
20.389 + case (Cons y ys) with Suc a Cons.prems show ?thesis
20.390 + apply -
20.391 + apply simp
20.392 + apply (cases j)
20.393 + apply simp
20.394 + apply (cases i)
20.395 + apply simp
20.396 + apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
20.397 + apply simp
20.398 + apply simp
20.399 + apply simp
20.400 + apply simp
20.401 + apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
20.402 + apply simp
20.403 + apply simp
20.404 + apply simp
20.405 + done
20.406 + qed
20.407 + qed
20.408 + qed
20.409 +qed
20.410 +
20.411 +lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
20.412 +by (induct xs arbitrary: i j, auto)
20.413 +
20.414 +lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
20.415 +apply (induct xs arbitrary: a i j)
20.416 +apply simp
20.417 +apply (case_tac j)
20.418 +apply simp
20.419 +apply (case_tac i)
20.420 +apply simp
20.421 +apply simp
20.422 +done
20.423 +
20.424 +lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
20.425 +apply (induct xs arbitrary: a i j)
20.426 +apply simp
20.427 +apply simp
20.428 +apply (case_tac j)
20.429 +apply simp
20.430 +apply auto
20.431 +apply (case_tac nat)
20.432 +apply auto
20.433 +done
20.434 +
20.435 +(* suffices that j \<le> length xs and length ys *)
20.436 +lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
20.437 +proof (induct xs arbitrary: ys i j)
20.438 + case Nil thus ?case by simp
20.439 +next
20.440 + case (Cons x xs)
20.441 + thus ?case
20.442 + apply -
20.443 + apply (cases ys)
20.444 + apply simp
20.445 + apply simp
20.446 + apply auto
20.447 + apply (case_tac i', auto)
20.448 + apply (erule_tac x="Suc i'" in allE, auto)
20.449 + apply (erule_tac x="i' - 1" in allE, auto)
20.450 + apply (case_tac i', auto)
20.451 + apply (erule_tac x="Suc i'" in allE, auto)
20.452 + done
20.453 +qed
20.454 +
20.455 +lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
20.456 +by (induct xs, auto)
20.457 +
20.458 +lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs"
20.459 +by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
20.460 +
20.461 +lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
20.462 +by (induct xs arbitrary: i j k) auto
20.463 +
20.464 +lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
20.465 +apply (induct xs arbitrary: i j k)
20.466 +apply auto
20.467 +apply (case_tac k)
20.468 +apply auto
20.469 +apply (case_tac i)
20.470 +apply auto
20.471 +done
20.472 +
20.473 +lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
20.474 +apply (simp add: sublist'_sublist)
20.475 +apply (simp add: set_sublist)
20.476 +apply auto
20.477 +done
20.478 +
20.479 +lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
20.480 +unfolding set_sublist' by blast
20.481 +
20.482 +lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
20.483 +unfolding set_sublist' by blast
20.484 +
20.485 +
20.486 +lemma multiset_of_sublist:
20.487 +assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
20.488 +assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
20.489 +assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
20.490 +assumes multiset: "multiset_of xs = multiset_of ys"
20.491 + shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
20.492 +proof -
20.493 + from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long")
20.494 + by (simp add: sublist'_append)
20.495 + from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
20.496 + with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long")
20.497 + by (simp add: sublist'_append)
20.498 + from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
20.499 + moreover
20.500 + from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
20.501 + by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
20.502 + moreover
20.503 + from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
20.504 + by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
20.505 + moreover
20.506 + ultimately show ?thesis by (simp add: multiset_of_append)
20.507 +qed
20.508 +
20.509 +
20.510 +end