# HG changeset patch # User haftmann # Date 1204144868 -3600 # Node ID 66e6b967ccf10521351c8131ebfbb75db6edb613 # Parent 73027318f9ba09ec6b17533cd0326234e80286c5 added theories for imperative HOL diff -r 73027318f9ba -r 66e6b967ccf1 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Feb 27 21:41:07 2008 +0100 +++ b/src/HOL/IsaMakefile Wed Feb 27 21:41:08 2008 +0100 @@ -233,7 +233,9 @@ Library/Code_Index.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ Library/Code_Integer.thy Library/Code_Message.thy \ Library/Abstract_Rat.thy Library/Univ_Poly.thy\ - Library/Numeral_Type.thy Library/Boolean_Algebra.thy + Library/Numeral_Type.thy Library/Boolean_Algebra.thy Library/Countable.thy \ + Library/RType.thy Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy \ + Library/Ref.thy Library/Imperative_HOL.thy @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library diff -r 73027318f9ba -r 66e6b967ccf1 src/HOL/Library/Array.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Array.thy Wed Feb 27 21:41:08 2008 +0100 @@ -0,0 +1,130 @@ +(* Title: HOL/Library/Array.thy + ID: $Id$ + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen +*) + +header {* Monadic arrays *} + +theory Array +imports Heap_Monad +begin + +subsection {* Primitives *} + +definition + new :: "nat \ 'a\heap \ 'a array Heap" where + [code del]: "new n x = Heap_Monad.heap (Heap.array n x)" + +definition + of_list :: "'a\heap list \ 'a array Heap" where + [code del]: "of_list xs = Heap_Monad.heap (Heap.array_of_list xs)" + +definition + length :: "'a\heap array \ nat Heap" where + [code del]: "length arr = Heap_Monad.heap (\h. (Heap.length arr h, h))" + +definition + nth :: "'a\heap array \ nat \ 'a Heap" +where + [code del]: "nth a i = (do len \ length a; + (if i < len + then Heap_Monad.heap (\h. (get_array a h ! i, h)) + else raise (''array lookup: index out of range'')) + done)" + +-- {* FIXME adjustion for List theory *} +no_syntax + nth :: "'a list \ nat \ 'a" (infixl "!" 100) + +abbreviation + nth_list :: "'a list \ nat \ 'a" (infixl "!" 100) +where + "nth_list \ List.nth" + +definition + upd :: "nat \ 'a \ 'a\heap array \ 'a\heap array Heap" +where + [code del]: "upd i x a = (do len \ length a; + (if i < len + then Heap_Monad.heap (\h. ((), Heap.upd a i x h)) + else raise (''array update: index out of range'')); + return a + done)" + +lemma upd_return: + "upd i x a \ return a = upd i x a" + unfolding upd_def by (simp add: monad_simp) + + +subsection {* Derivates *} + +definition + map_entry :: "nat \ ('a\heap \ 'a) \ 'a array \ 'a array Heap" +where + "map_entry i f a = (do + x \ nth a i; + upd i (f x) a + done)" + +definition + swap :: "nat \ 'a \ 'a\heap array \ 'a Heap" +where + "swap i x a = (do + y \ nth a i; + upd i x a; + return x + done)" + +definition + make :: "nat \ (nat \ 'a\heap) \ 'a array Heap" +where + "make n f = of_list (map f [0 ..< n])" + +definition + freeze :: "'a\heap array \ 'a list Heap" +where + "freeze a = (do + n \ length a; + mapM (nth a) [0..heap \ 'a) \ 'a array \ 'a array Heap" +where + "map f a = (do + n \ length a; + foldM (\n. map_entry n f) [0.. ('a\heap) array \ 'a list \ 'a list Heap" where + "list_of_aux 0 a xs = return xs" + | "list_of_aux (Suc n) a xs = (do + x \ Array.nth a n; + list_of_aux n a (x#xs) + done)" + +definition list_of :: "('a\heap) array \ 'a list Heap" where + "list_of a = (do n \ Array.length a; + list_of_aux n a [] + done)" + + +subsection {* Properties *} + +lemma array_make [code func]: + "Array.new n x = make n (\_. x)" + by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def + monad_simp array_of_list_replicate [symmetric] + map_replicate_trivial replicate_append_same + of_list_def) + +lemma array_of_list_make [code func]: + "of_list xs = make (List.length xs) (\n. xs ! n)" + unfolding make_def map_nth .. + +end diff -r 73027318f9ba -r 66e6b967ccf1 src/HOL/Library/Heap.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Heap.thy Wed Feb 27 21:41:08 2008 +0100 @@ -0,0 +1,450 @@ +(* Title: HOL/Library/Heap.thy + ID: $Id$ + Author: John Matthews, Galois Connections; Alexander Krauss, TU Muenchen +*) + +header {* A polymorphic heap based on cantor encodings *} + +theory Heap +imports Main Countable RType +begin + +subsection {* Representable types *} + +text {* The type class of representable types *} + +class heap = rtype + countable + +text {* Instances for common HOL types *} + +instance nat :: heap .. + +instance "*" :: (heap, heap) heap .. + +instance "+" :: (heap, heap) heap .. + +instance list :: (heap) heap .. + +instance option :: (heap) heap .. + +instance int :: heap .. + +instance set :: ("{heap, finite}") heap .. + +instance message_string :: countable + by (rule countable_classI [of "message_string_case to_nat"]) + (auto split: message_string.splits) + +instance message_string :: heap .. + +text {* Reflected types themselves are heap-representable *} + +instantiation rtype :: countable +begin + +lemma list_size_size_append: + "list_size size (xs @ ys) = list_size size xs + list_size size ys" + by (induct xs, auto) + +lemma rtype_size: "t = RType.RType c ts \ t' \ set ts \ size t' < size t" + by (frule split_list) (auto simp add: list_size_size_append) + +function to_nat_rtype :: "rtype \ nat" where + "to_nat_rtype (RType.RType c ts) = to_nat (to_nat c, to_nat (map to_nat_rtype ts))" +by pat_completeness auto + +termination by (relation "measure (\x. size x)") + (simp, simp only: in_measure rtype_size) + +instance proof (rule countable_classI) + fix t t' :: rtype + have "(\t'. to_nat_rtype t = to_nat_rtype t' \ t = t') + \ (\ts'. map to_nat_rtype ts = map to_nat_rtype ts' \ ts = ts')" + proof (induct rule: rtype.induct) + case (RType c ts) show ?case + proof (rule allI, rule impI) + fix t' + assume hyp: "to_nat_rtype (rtype.RType c ts) = to_nat_rtype t'" + then obtain c' ts' where t': "t' = (rtype.RType c' ts')" + by (cases t') auto + with RType hyp have "c = c'" and "ts = ts'" by simp_all + with t' show "rtype.RType c ts = t'" by simp + qed + next + case Nil_rtype then show ?case by simp + next + case (Cons_rtype t ts) then show ?case by auto + qed + then have "to_nat_rtype t = to_nat_rtype t' \ t = t'" by auto + moreover assume "to_nat_rtype t = to_nat_rtype t'" + ultimately show "t = t'" by simp +qed + +end + +instance rtype :: heap .. + + +subsection {* A polymorphic heap with dynamic arrays and references *} + +types addr = nat -- "untyped heap references" + +datatype 'a array = Array addr +datatype 'a ref = Ref addr -- "note the phantom type 'a " + +primrec addr_of_array :: "'a array \ addr" where + "addr_of_array (Array x) = x" + +primrec addr_of_ref :: "'a ref \ addr" where + "addr_of_ref (Ref x) = x" + +lemma addr_of_array_inj [simp]: + "addr_of_array a = addr_of_array a' \ a = a'" + by (cases a, cases a') simp_all + +lemma addr_of_ref_inj [simp]: + "addr_of_ref r = addr_of_ref r' \ r = r'" + by (cases r, cases r') simp_all + +instance array :: (type) countable + by (rule countable_classI [of addr_of_array]) simp + +instance ref :: (type) countable + by (rule countable_classI [of addr_of_ref]) simp + +setup {* + Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat \ 'a\heap array"}) + #> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \ 'a\heap ref"}) + #> Sign.add_const_constraint (@{const_name addr_of_array}, SOME @{typ "'a\heap array \ nat"}) + #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a\heap ref \ nat"}) +*} + +types heap_rep = nat -- "representable values" + +record heap = + arrays :: "rtype \ addr \ heap_rep list" + refs :: "rtype \ addr \ heap_rep" + lim :: addr + +definition empty :: heap where + "empty = \arrays = (\_. arbitrary), refs = (\_. arbitrary), lim = 0\" -- "why arbitrary?" + + +subsection {* Imperative references and arrays *} + +text {* + References and arrays are developed in parallel, + but keeping them seperate makes some later proofs simpler. +*} + +subsubsection {* Primitive operations *} + +definition + new_ref :: "heap \ ('a\heap) ref \ heap" where + "new_ref h = (let l = lim h in (Ref l, h\lim := l + 1\))" + +definition + new_array :: "heap \ ('a\heap) array \ heap" where + "new_array h = (let l = lim h in (Array l, h\lim := l + 1\))" + +definition + ref_present :: "'a\heap ref \ heap \ bool" where + "ref_present r h \ addr_of_ref r < lim h" + +definition + array_present :: "'a\heap array \ heap \ bool" where + "array_present a h \ addr_of_array a < lim h" + +definition + get_ref :: "'a\heap ref \ heap \ 'a" where + "get_ref r h = from_nat (refs h (RTYPE('a)) (addr_of_ref r))" + +definition + get_array :: "'a\heap array \ heap \ 'a list" where + "get_array a h = map from_nat (arrays h (RTYPE('a)) (addr_of_array a))" + +definition + set_ref :: "'a\heap ref \ 'a \ heap \ heap" where + "set_ref r x = + refs_update (\h. h( RTYPE('a) := ((h (RTYPE('a))) (addr_of_ref r:=to_nat x))))" + +definition + set_array :: "'a\heap array \ 'a list \ heap \ heap" where + "set_array a x = + arrays_update (\h. h( RTYPE('a) := ((h (RTYPE('a))) (addr_of_array a:=map to_nat x))))" + +subsubsection {* Interface operations *} + +definition + ref :: "'a \ heap \ 'a\heap ref \ heap" where + "ref x h = (let (r, h') = new_ref h; + h'' = set_ref r x h' + in (r, h''))" + +definition + array :: "nat \ 'a \ heap \ 'a\heap array \ heap" where + "array n x h = (let (r, h') = new_array h; + h'' = set_array r (replicate n x) h' + in (r, h''))" + +definition + array_of_list :: "'a list \ heap \ 'a\heap array \ heap" where + "array_of_list xs h = (let (r, h') = new_array h; + h'' = set_array r xs h' + in (r, h''))" + +definition + upd :: "'a\heap array \ nat \ 'a \ heap \ heap" where + "upd a i x h = set_array a ((get_array a h)[i:=x]) h" + +definition + length :: "'a\heap array \ heap \ nat" where + "length a h = size (get_array a h)" + +definition + array_ran :: "('a\heap) option array \ heap \ 'a set" where + "array_ran a h = {e. Some e \ set (get_array a h)}" + -- {*FIXME*} + + +subsubsection {* Reference equality *} + +text {* + The following relations are useful for comparing arrays and references. +*} + +definition + noteq_refs :: "('a\heap) ref \ ('b\heap) ref \ bool" (infix "=!=" 70) +where + "r =!= s \ RTYPE('a) \ RTYPE('b) \ addr_of_ref r \ addr_of_ref s" + +definition + noteq_arrs :: "('a\heap) array \ ('b\heap) array \ bool" (infix "=!!=" 70) +where + "r =!!= s \ RTYPE('a) \ RTYPE('b) \ addr_of_array r \ addr_of_array s" + +lemma noteq_refs_sym: "r =!= s \ s =!= r" + and noteq_arrs_sym: "a =!!= b \ b =!!= a" + and unequal_refs [simp]: "r \ r' \ r =!= r'" -- "same types!" + and unequal_arrs [simp]: "a \ a' \ a =!!= a'" +unfolding noteq_refs_def noteq_arrs_def by auto + +lemma present_new_ref: "ref_present r h \ r =!= fst (ref v h)" + by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def) + +lemma present_new_arr: "array_present a h \ a =!!= fst (array v x h)" + by (simp add: array_present_def noteq_arrs_def new_array_def array_def Let_def) + + +subsubsection {* Properties of heap containers *} + +text {* Properties of imperative arrays *} + +text {* FIXME: Does there exist a "canonical" array axiomatisation in +the literature? *} + +lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" + by (simp add: get_array_def set_array_def) + +lemma array_get_set_neq [simp]: "r =!!= s \ get_array r (set_array s x h) = get_array r h" + by (simp add: noteq_arrs_def get_array_def set_array_def) + +lemma set_array_same [simp]: + "set_array r x (set_array r y h) = set_array r x h" + by (simp add: set_array_def) + +lemma array_set_set_swap: + "r =!!= r' \ set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" + by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) + +lemma array_ref_set_set_swap: + "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)" + by (simp add: Let_def expand_fun_eq set_array_def set_ref_def) + +lemma get_array_upd_eq [simp]: + "get_array a (upd a i v h) = (get_array a h) [i := v]" + by (simp add: upd_def) + +lemma nth_upd_array_neq_array [simp]: + "a =!!= b \ get_array a (upd b j v h) ! i = get_array a h ! i" + by (simp add: upd_def noteq_arrs_def) + +lemma get_arry_array_upd_elem_neqIndex [simp]: + "i \ j \ get_array a (upd a j v h) ! i = get_array a h ! i" + by simp + +lemma length_upd_eq [simp]: + "length a (upd a i v h) = length a h" + by (simp add: length_def upd_def) + +lemma length_upd_neq [simp]: + "length a (upd b i v h) = length a h" + by (simp add: upd_def length_def set_array_def get_array_def) + +lemma upd_swap_neqArray: + "a =!!= a' \ + upd a i v (upd a' i' v' h) + = upd a' i' v' (upd a i v h)" +apply (unfold upd_def) +apply simp +apply (subst array_set_set_swap, assumption) +apply (subst array_get_set_neq) +apply (erule noteq_arrs_sym) +apply (simp) +done + +lemma upd_swap_neqIndex: + "\ i \ i' \ \ upd a i v (upd a i' v' h) = upd a i' v' (upd a i v h)" +by (auto simp add: upd_def array_set_set_swap list_update_swap) + +lemma get_array_init_array_list: + "get_array (fst (array_of_list ls h)) (snd (array_of_list ls' h)) = ls'" + by (simp add: Let_def split_def array_of_list_def) + +lemma set_array: + "set_array (fst (array_of_list ls h)) + new_ls (snd (array_of_list ls h)) + = snd (array_of_list new_ls h)" + by (simp add: Let_def split_def array_of_list_def) + +lemma array_present_upd [simp]: + "array_present a (upd b i v h) = array_present a h" + by (simp add: upd_def array_present_def set_array_def get_array_def) + +lemma array_of_list_replicate: + "array_of_list (replicate n x) = array n x" + by (simp add: expand_fun_eq array_of_list_def array_def) + + +text {* Properties of imperative references *} + +lemma next_ref_fresh [simp]: + assumes "(r, h') = new_ref h" + shows "\ ref_present r h" + using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def) + +lemma next_ref_present [simp]: + assumes "(r, h') = new_ref h" + shows "ref_present r h'" + using assms by (cases h) (auto simp add: new_ref_def ref_present_def Let_def) + +lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x" + by (simp add: get_ref_def set_ref_def) + +lemma ref_get_set_neq [simp]: "r =!= s \ get_ref r (set_ref s x h) = get_ref r h" + by (simp add: noteq_refs_def get_ref_def set_ref_def) + +(* FIXME: We need some infrastructure to infer that locally generated + new refs (by new_ref(_no_init), new_array(')) are distinct + from all existing refs. +*) + +lemma ref_set_get: "set_ref r (get_ref r h) h = h" +apply (simp add: set_ref_def get_ref_def) +oops + +lemma set_ref_same[simp]: + "set_ref r x (set_ref r y h) = set_ref r x h" + by (simp add: set_ref_def) + +lemma ref_set_set_swap: + "r =!= r' \ set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)" + by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def) + +lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)" + by (simp add: ref_def new_ref_def set_ref_def Let_def) + +lemma ref_get_new [simp]: + "get_ref (fst (ref v h)) (snd (ref v' h)) = v'" + by (simp add: ref_def Let_def split_def) + +lemma ref_set_new [simp]: + "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)" + by (simp add: ref_def Let_def split_def) + +lemma ref_get_new_neq: "r =!= (fst (ref v h)) \ + get_ref r (snd (ref v h)) = get_ref r h" + by (simp add: get_ref_def set_ref_def ref_def Let_def new_ref_def noteq_refs_def) + +lemma lim_set_ref [simp]: + "lim (set_ref r v h) = lim h" + by (simp add: set_ref_def) + +lemma ref_present_new_ref [simp]: + "ref_present r h \ ref_present r (snd (ref v h))" + by (simp add: new_ref_def ref_present_def ref_def Let_def) + +lemma ref_present_set_ref [simp]: + "ref_present r (set_ref r' v h) = ref_present r h" + by (simp add: set_ref_def ref_present_def) + +lemma array_ranI: "\ Some b = get_array a h ! i; i < Heap.length a h \ \ b \ array_ran a h" +unfolding array_ran_def Heap.length_def by simp + +lemma array_ran_upd_array_Some: + assumes "cl \ array_ran a (Heap.upd a i (Some b) h)" + shows "cl \ array_ran a h \ cl = b" +proof - + have "set (get_array a h[i := Some b]) \ insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert) + with assms show ?thesis + unfolding array_ran_def Heap.upd_def by fastsimp +qed + +lemma array_ran_upd_array_None: + assumes "cl \ array_ran a (Heap.upd a i None h)" + shows "cl \ array_ran a h" +proof - + have "set (get_array a h[i := None]) \ insert None (set (get_array a h))" by (rule set_update_subset_insert) + with assms show ?thesis + unfolding array_ran_def Heap.upd_def by auto +qed + + +text {* Non-interaction between imperative array and imperative references *} + +lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h" + by (simp add: get_array_def set_ref_def) + +lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i" + by simp + +lemma get_ref_upd [simp]: "get_ref r (upd a i v h) = get_ref r h" + by (simp add: get_ref_def set_array_def upd_def) + +lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)" + by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def new_ref_def) + +(*not actually true ??? +lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)" +apply (case_tac a) +apply (simp add: Let_def upd_def) +apply auto +done*) + +lemma length_new_ref[simp]: + "length a (snd (ref v h)) = length a h" + by (simp add: get_array_def set_ref_def length_def new_ref_def ref_def Let_def) + +lemma get_array_new_ref [simp]: + "get_array a (snd (ref v h)) = get_array a h" + by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def) + +lemma get_array_new_ref [simp]: + "get_array a (snd (ref v h)) ! i = get_array a h ! i" + by (simp add: get_array_def new_ref_def ref_def set_ref_def Let_def) + +lemma ref_present_upd [simp]: + "ref_present r (upd a i v h) = ref_present r h" + by (simp add: upd_def ref_present_def set_array_def get_array_def) + +lemma array_present_set_ref [simp]: + "array_present a (set_ref r v h) = array_present a h" + by (simp add: array_present_def set_ref_def) + +lemma array_present_new_ref [simp]: + "array_present a h \ array_present a (snd (ref v h))" + by (simp add: array_present_def new_ref_def ref_def Let_def) + +hide (open) const empty array array_of_list upd length ref + +end diff -r 73027318f9ba -r 66e6b967ccf1 src/HOL/Library/Heap_Monad.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Heap_Monad.thy Wed Feb 27 21:41:08 2008 +0100 @@ -0,0 +1,277 @@ +(* Title: HOL/Library/Heap_Monad.thy + ID: $Id$ + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen +*) + +header {* A monad with a polymorphic heap *} + +theory Heap_Monad +imports Heap +begin + +subsection {* The monad *} + +subsubsection {* Monad combinators *} + +datatype exception = Exn + +text {* Monadic heap actions either produce values + and transform the heap, or fail *} +datatype 'a Heap = Heap "heap \ ('a + exception) \ heap" + +primrec + execute :: "'a Heap \ heap \ ('a + exception) \ heap" where + "execute (Heap f) = f" +lemmas [code del] = execute.simps + +lemma Heap_execute [simp]: + "Heap (execute f) = f" by (cases f) simp_all + +lemma Heap_eqI: + "(\h. execute f h = execute g h) \ f = g" + by (cases f, cases g) (auto simp: expand_fun_eq) + +lemma Heap_eqI': + "(\h. (\x. execute (f x) h) = (\y. execute (g y) h)) \ f = g" + by (auto simp: expand_fun_eq intro: Heap_eqI) + +lemma Heap_strip: "(\f. PROP P f) \ (\g. PROP P (Heap g))" +proof + fix g :: "heap \ ('a + exception) \ heap" + assume "\f. PROP P f" + then show "PROP P (Heap g)" . +next + fix f :: "'a Heap" + assume assm: "\g. PROP P (Heap g)" + then have "PROP P (Heap (execute f))" . + then show "PROP P f" by simp +qed + +definition + heap :: "(heap \ 'a \ heap) \ 'a Heap" where + [code del]: "heap f = Heap (\h. apfst Inl (f h))" + +lemma execute_heap [simp]: + "execute (heap f) h = apfst Inl (f h)" + by (simp add: heap_def) + +definition + run :: "'a Heap \ 'a Heap" where + run_drop [code del]: "run f = f" + +definition + bindM :: "'a Heap \ ('a \ 'b Heap) \ 'b Heap" (infixl ">>=" 54) where + [code del]: "f >>= g = Heap (\h. case execute f h of + (Inl x, h') \ execute (g x) h' + | r \ r)" + +notation + bindM (infixl "\=" 54) + +abbreviation + chainM :: "'a Heap \ 'b Heap \ 'b Heap" (infixl ">>" 54) where + "f >> g \ f >>= (\_. g)" + +notation + chainM (infixl "\" 54) + +definition + return :: "'a \ 'a Heap" where + [code del]: "return x = heap (Pair x)" + +lemma execute_return [simp]: + "execute (return x) h = apfst Inl (x, h)" + by (simp add: return_def) + +definition + raise :: "string \ 'a Heap" where -- {* the string is just decoration *} + [code del]: "raise s = Heap (Pair (Inr Exn))" + +notation (latex output) + "raise" ("\<^raw:{\textsf{raise}}>") + +lemma execute_raise [simp]: + "execute (raise s) h = (Inr Exn, h)" + by (simp add: raise_def) + + +subsubsection {* do-syntax *} + +text {* + We provide a convenient do-notation for monadic expressions + well-known from Haskell. @{const Let} is printed + specially in do-expressions. +*} + +nonterminals do_expr + +syntax + "_do" :: "do_expr \ 'a" + ("(do (_)//done)" [12] 100) + "_bindM" :: "pttrn \ 'a \ do_expr \ do_expr" + ("_ <- _;//_" [1000, 13, 12] 12) + "_chainM" :: "'a \ do_expr \ do_expr" + ("_;//_" [13, 12] 12) + "_let" :: "pttrn \ 'a \ do_expr \ do_expr" + ("let _ = _;//_" [1000, 13, 12] 12) + "_nil" :: "'a \ do_expr" + ("_" [12] 12) + +syntax (xsymbols) + "_bindM" :: "pttrn \ 'a \ do_expr \ do_expr" + ("_ \ _;//_" [1000, 13, 12] 12) +syntax (latex output) + "_do" :: "do_expr \ 'a" + ("(\<^raw:{\textsf{do}}> (_))" [12] 100) + "_let" :: "pttrn \ 'a \ do_expr \ do_expr" + ("\<^raw:\textsf{let}> _ = _;//_" [1000, 13, 12] 12) +notation (latex output) + "return" ("\<^raw:{\textsf{return}}>") + +translations + "_do f" => "CONST run f" + "_bindM x f g" => "f \= (\x. g)" + "_chainM f g" => "f \ g" + "_let x t f" => "CONST Let t (\x. f)" + "_nil f" => "f" + +print_translation {* +let + fun dest_abs_eta (Abs (abs as (_, ty, _))) = + let + val (v, t) = Syntax.variant_abs abs; + in ((v, ty), t) end + | dest_abs_eta t = + let + val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0); + in ((v, dummyT), t) end + fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) = + let + val ((v, ty), g') = dest_abs_eta g; + val v_used = fold_aterms + (fn Free (w, _) => (fn s => s orelse v = w) | _ => I) g' false; + in if v_used then + Const ("_bindM", dummyT) $ Free (v, ty) $ f $ unfold_monad g' + else + Const ("_chainM", dummyT) $ f $ unfold_monad g' + end + | unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) = + Const ("_chainM", dummyT) $ f $ unfold_monad g + | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = + let + val ((v, ty), g') = dest_abs_eta g; + in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end + | unfold_monad (Const (@{const_syntax Pair}, _) $ f) = + Const ("return", dummyT) $ f + | unfold_monad f = f; + fun tr' (f::ts) = + list_comb (Const ("_do", dummyT) $ unfold_monad f, ts) +in [(@{const_syntax "run"}, tr')] end; +*} + +subsubsection {* Plain evaluation *} + +definition + evaluate :: "'a Heap \ 'a" +where + [code del]: "evaluate f = (case execute f Heap.empty + of (Inl x, _) \ x)" + + +subsection {* Monad properties *} + +subsubsection {* Superfluous runs *} + +text {* @{term run} is just a doodle *} + +lemma run_simp [simp]: + "\f. run (run f) = run f" + "\f g. run f \= g = f \= g" + "\f g. run f \ g = f \ g" + "\f g. f \= (\x. run g) = f \= (\x. g)" + "\f g. f \ run g = f \ g" + "\f. f = run g \ f = g" + "\f. run f = g \ f = g" + unfolding run_drop by rule+ + +subsubsection {* Monad laws *} + +lemma return_bind: "return x \= f = f x" + by (simp add: bindM_def return_def) + +lemma bind_return: "f \= return = f" +proof (rule Heap_eqI) + fix h + show "execute (f \= return) h = execute f h" + by (auto simp add: bindM_def return_def split: sum.splits prod.splits) +qed + +lemma bind_bind: "(f \= g) \= h = f \= (\x. g x \= h)" + by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits) + +lemma bind_bind': "f \= (\x. g x \= h x) = f \= (\x. g x \= (\y. return (x, y))) \= (\(x, y). h x y)" + by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits) + +lemma raise_bind: "raise e \= f = raise e" + by (simp add: raise_def bindM_def) + + +lemmas monad_simp = return_bind bind_return bind_bind raise_bind + + +subsection {* Generic combinators *} + +definition + liftM :: "('a \ 'b) \ 'a \ 'b Heap" +where + "liftM f = return o f" + +definition + compM :: "('a \ 'b Heap) \ ('b \ 'c Heap) \ 'a \ 'c Heap" (infixl ">>==" 54) +where + "(f >>== g) = (\x. f x \= g)" + +notation + compM (infixl "\==" 54) + +lemma liftM_collapse: "liftM f x = return (f x)" + by (simp add: liftM_def) + +lemma liftM_compM: "liftM f \== g = g o f" + by (auto intro: Heap_eqI' simp add: expand_fun_eq liftM_def compM_def bindM_def) + +lemma compM_return: "f \== return = f" + by (simp add: compM_def monad_simp) + +lemma compM_compM: "(f \== g) \== h = f \== (g \== h)" + by (simp add: compM_def monad_simp) + +lemma liftM_bind: + "(\x. liftM f x \= liftM g) = liftM (\x. g (f x))" + by (rule Heap_eqI') (simp add: monad_simp liftM_def bindM_def) + +lemma liftM_comp: + "liftM f o g = liftM (f o g)" + by (rule Heap_eqI') (simp add: liftM_def) + +lemmas monad_simp' = monad_simp liftM_compM compM_return + compM_compM liftM_bind liftM_comp + +primrec + mapM :: "('a \ 'b Heap) \ 'a list \ 'b list Heap" +where + "mapM f [] = return []" + | "mapM f (x#xs) = do y \ f x; + ys \ mapM f xs; + return (y # ys) + done" + +primrec + foldM :: "('a \ 'b \ 'b Heap) \ 'a list \ 'b \ 'b Heap" +where + "foldM f [] s = return s" + | "foldM f (x#xs) s = f x s \= foldM f xs" + +hide (open) const heap execute + +end diff -r 73027318f9ba -r 66e6b967ccf1 src/HOL/Library/Imperative_HOL.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Imperative_HOL.thy Wed Feb 27 21:41:08 2008 +0100 @@ -0,0 +1,12 @@ +(* Title: HOL/Library/Imperative_HOL.thy + ID: $Id$ + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen +*) + +header {* Entry point into monadic imperative HOL *} + +theory Imperative_HOL +imports Array Ref +begin + +end diff -r 73027318f9ba -r 66e6b967ccf1 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Feb 27 21:41:07 2008 +0100 +++ b/src/HOL/Library/Library.thy Wed Feb 27 21:41:08 2008 +0100 @@ -8,18 +8,22 @@ Binomial Boolean_Algebra Char_ord + Code_Char_chr Code_Index + Code_Integer Code_Message Coinductive_List Commutative_Ring Continuity + Countable Dense_Linear_Order Efficient_Nat - (*Eval*) + Eval Eval_Witness Executable_Set FuncSet GCD + Imperative_HOL Infinite_Set ListSpace Multiset @@ -30,8 +34,6 @@ OptionalSugar Parity Permutation - Code_Integer - Code_Char_chr Primes Quicksort Quotient diff -r 73027318f9ba -r 66e6b967ccf1 src/HOL/Library/Ref.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Ref.thy Wed Feb 27 21:41:08 2008 +0100 @@ -0,0 +1,56 @@ +(* Title: HOL/Library/Ref.thy + ID: $Id$ + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen +*) + +header {* Monadic references *} + +theory Ref +imports Heap_Monad +begin + +text {* + Imperative reference operations; modeled after their ML counterparts. + See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html + and http://www.smlnj.org/doc/Conversion/top-level-comparison.html +*} + +subsection {* Primitives *} + +definition + new :: "'a\heap \ 'a ref Heap" where + [code del]: "new v = Heap_Monad.heap (Heap.ref v)" + +definition + lookup :: "'a\heap ref \ 'a Heap" ("!_" 61) where + [code del]: "lookup r = Heap_Monad.heap (\h. (get_ref r h, h))" + +definition + update :: "'a ref \ ('a\heap) \ unit Heap" ("_ := _" 62) where + [code del]: "update r e = Heap_Monad.heap (\h. ((), set_ref r e h))" + +subsection {* Derivates *} + +definition + change :: "('a\heap \ 'a) \ 'a ref \ 'a Heap" +where + "change f r = (do x \ ! r; + let y = f x; + r := y; + return y + done)" + +hide (open) const new lookup update change + +subsection {* Properties *} + +lemma lookup_chain: + "(!r \ f) = f" + by (cases f) + (auto simp add: Let_def bindM_def lookup_def expand_fun_eq) + +lemma update_change [code func]: + "r := e = Ref.change (\_. e) r \ return ()" + by (auto simp add: monad_simp change_def lookup_chain) + +end \ No newline at end of file