guard combinator
authorhaftmann
Fri Jul 09 09:48:53 2010 +0200 (2010-07-09)
changeset 37754683d1e1bc234
parent 37753 3ac6867279f0
child 37755 7086b7feaaa5
guard combinator
src/HOL/Imperative_HOL/Heap_Monad.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 09:48:53 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 09:48:53 2010 +0200
     1.3 @@ -37,6 +37,14 @@
     1.4    "execute (heap f) = Some \<circ> f"
     1.5    by (simp add: heap_def)
     1.6  
     1.7 +definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
     1.8 +  [code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
     1.9 +
    1.10 +lemma execute_guard [simp]:
    1.11 +  "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
    1.12 +  "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
    1.13 +  by (simp_all add: guard_def)
    1.14 +
    1.15  lemma heap_cases [case_names succeed fail]:
    1.16    fixes f and h
    1.17    assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
    1.18 @@ -58,7 +66,7 @@
    1.19    "execute (raise s) = (\<lambda>_. None)"
    1.20    by (simp add: raise_def)
    1.21  
    1.22 -definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
    1.23 +definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where (*FIXME just bind*)
    1.24    [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
    1.25                    Some (x, h') \<Rightarrow> execute (g x) h'
    1.26                  | None \<Rightarrow> None)"
    1.27 @@ -74,6 +82,12 @@
    1.28    "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
    1.29    by (simp add: bindM_def split_def)
    1.30    
    1.31 +lemma execute_eq_SomeI:
    1.32 +  assumes "Heap_Monad.execute f h = Some (x, h')"
    1.33 +    and "Heap_Monad.execute (g x) h' = Some (y, h'')"
    1.34 +  shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
    1.35 +  using assms by (simp add: bindM_def)
    1.36 +
    1.37  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
    1.38    by (rule Heap_eqI) simp
    1.39  
    1.40 @@ -86,10 +100,10 @@
    1.41  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
    1.42    by (rule Heap_eqI) simp
    1.43  
    1.44 -abbreviation chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
    1.45 +abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
    1.46    "f >> g \<equiv> f >>= (\<lambda>_. g)"
    1.47  
    1.48 -notation chainM (infixl "\<guillemotright>" 54)
    1.49 +notation chain (infixl "\<guillemotright>" 54)
    1.50  
    1.51  
    1.52  subsubsection {* do-syntax *}
    1.53 @@ -105,9 +119,9 @@
    1.54  syntax
    1.55    "_do" :: "do_expr \<Rightarrow> 'a"
    1.56      ("(do (_)//done)" [12] 100)
    1.57 -  "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.58 +  "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.59      ("_ <- _;//_" [1000, 13, 12] 12)
    1.60 -  "_chainM" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.61 +  "_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.62      ("_;//_" [13, 12] 12)
    1.63    "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.64      ("let _ = _;//_" [1000, 13, 12] 12)
    1.65 @@ -115,13 +129,13 @@
    1.66      ("_" [12] 12)
    1.67  
    1.68  syntax (xsymbols)
    1.69 -  "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.70 +  "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
    1.71      ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
    1.72  
    1.73  translations
    1.74    "_do f" => "f"
    1.75 -  "_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
    1.76 -  "_chainM f g" => "f \<guillemotright> g"
    1.77 +  "_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
    1.78 +  "_chain f g" => "f \<guillemotright> g"
    1.79    "_let x t f" => "CONST Let t (\<lambda>x. f)"
    1.80    "_nil f" => "f"
    1.81  
    1.82 @@ -142,12 +156,12 @@
    1.83            val v_used = fold_aterms
    1.84              (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
    1.85          in if v_used then
    1.86 -          Const (@{syntax_const "_bindM"}, dummyT) $ v $ f $ unfold_monad g'
    1.87 +          Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g'
    1.88          else
    1.89 -          Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g'
    1.90 +          Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g'
    1.91          end
    1.92 -    | unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) =
    1.93 -        Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g
    1.94 +    | unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) =
    1.95 +        Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g
    1.96      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    1.97          let
    1.98            val (v, g') = dest_abs_eta g;
    1.99 @@ -155,14 +169,14 @@
   1.100      | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
   1.101          Const (@{const_syntax return}, dummyT) $ f
   1.102      | unfold_monad f = f;
   1.103 -  fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true
   1.104 -    | contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   1.105 -        contains_bindM t;
   1.106 +  fun contains_bind (Const (@{const_syntax bindM}, _) $ _ $ _) = true
   1.107 +    | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
   1.108 +        contains_bind t;
   1.109    fun bindM_monad_tr' (f::g::ts) = list_comb
   1.110      (Const (@{syntax_const "_do"}, dummyT) $
   1.111        unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts);
   1.112    fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
   1.113 -    if contains_bindM g' then list_comb
   1.114 +    if contains_bind g' then list_comb
   1.115        (Const (@{syntax_const "_do"}, dummyT) $
   1.116          unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
   1.117      else raise Match;
   1.118 @@ -180,31 +194,55 @@
   1.119  definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
   1.120    "assert P x = (if P x then return x else raise ''assert'')"
   1.121  
   1.122 +lemma execute_assert [simp]:
   1.123 +  "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   1.124 +  "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
   1.125 +  by (simp_all add: assert_def)
   1.126 +
   1.127  lemma assert_cong [fundef_cong]:
   1.128    assumes "P = P'"
   1.129    assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
   1.130    shows "(assert P x >>= f) = (assert P' x >>= f')"
   1.131 -  using assms by (auto simp add: assert_def return_bind raise_bind)
   1.132 +  by (rule Heap_eqI) (insert assms, simp add: assert_def)
   1.133  
   1.134 -definition liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
   1.135 -  "liftM f = return o f"
   1.136 +definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
   1.137 +  "lift f = return o f"
   1.138  
   1.139 -lemma liftM_collapse [simp]:
   1.140 -  "liftM f x = return (f x)"
   1.141 -  by (simp add: liftM_def)
   1.142 +lemma lift_collapse [simp]:
   1.143 +  "lift f x = return (f x)"
   1.144 +  by (simp add: lift_def)
   1.145  
   1.146 -lemma bind_liftM:
   1.147 -  "(f \<guillemotright>= liftM g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   1.148 -  by (simp add: liftM_def comp_def)
   1.149 +lemma bind_lift:
   1.150 +  "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   1.151 +  by (simp add: lift_def comp_def)
   1.152  
   1.153 -primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   1.154 +primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where (*FIXME just map?*)
   1.155    "mapM f [] = return []"
   1.156 -| "mapM f (x#xs) = do
   1.157 +| "mapM f (x # xs) = do
   1.158       y \<leftarrow> f x;
   1.159       ys \<leftarrow> mapM f xs;
   1.160       return (y # ys)
   1.161     done"
   1.162  
   1.163 +lemma mapM_append:
   1.164 +  "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   1.165 +  by (induct xs) simp_all
   1.166 +
   1.167 +lemma execute_mapM_unchanged_heap:
   1.168 +  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
   1.169 +  shows "execute (mapM f xs) h =
   1.170 +    Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   1.171 +using assms proof (induct xs)
   1.172 +  case Nil show ?case by simp
   1.173 +next
   1.174 +  case (Cons x xs)
   1.175 +  from Cons.prems obtain y
   1.176 +    where y: "execute (f x) h = Some (y, h)" by auto
   1.177 +  moreover from Cons.prems Cons.hyps have "execute (mapM f xs) h =
   1.178 +    Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   1.179 +  ultimately show ?case by (simp, simp only: execute_bind(1), simp)
   1.180 +qed
   1.181 +
   1.182  
   1.183  subsubsection {* A monadic combinator for simple recursive functions *}
   1.184  
   1.185 @@ -371,7 +409,7 @@
   1.186  code_const return (SML "!(fn/ ()/ =>/ _)")
   1.187  code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
   1.188  
   1.189 -code_type Heap (OCaml "_")
   1.190 +code_type Heap (OCaml "unit/ ->/ _")
   1.191  code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
   1.192  code_const return (OCaml "!(fun/ ()/ ->/ _)")
   1.193  code_const Heap_Monad.raise' (OCaml "failwith/ _")
   1.194 @@ -388,7 +426,7 @@
   1.195      fun is_const c = case lookup_const naming c
   1.196       of SOME c' => (fn c'' => c' = c'')
   1.197        | NONE => K false;
   1.198 -    val is_bindM = is_const @{const_name bindM};
   1.199 +    val is_bind = is_const @{const_name bindM};
   1.200      val is_return = is_const @{const_name return};
   1.201      val dummy_name = "";
   1.202      val dummy_type = ITyVar dummy_name;
   1.203 @@ -412,13 +450,13 @@
   1.204          val ((v, ty), t) = dest_abs (t2, ty2);
   1.205        in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
   1.206      and tr_bind'' t = case unfold_app t
   1.207 -         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bindM c
   1.208 +         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
   1.209                then tr_bind' [(x1, ty1), (x2, ty2)]
   1.210                else force t
   1.211            | _ => force t;
   1.212      fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type),
   1.213        [(unitt, tr_bind' ts)]), dummy_case_term)
   1.214 -    and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys)
   1.215 +    and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
   1.216         of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
   1.217          | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
   1.218          | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
   1.219 @@ -489,6 +527,6 @@
   1.220  code_const return (Haskell "return")
   1.221  code_const Heap_Monad.raise' (Haskell "error/ _")
   1.222  
   1.223 -hide_const (open) Heap heap execute raise'
   1.224 +hide_const (open) Heap heap guard execute raise'
   1.225  
   1.226  end