1 theory StateMonad

     2 imports 

     3        "~~/src/HOL/Library/Monad_Syntax" 

     4 begin

     5 

     6 datatype ('result, 'state) SM = SM "'state => ('result \<times> 'state) option"

     7 

     8 fun execute :: "('result, 'state) SM \<Rightarrow> 'state \<Rightarrow> ('result \<times> 'state) option" where

     9   "execute (SM f) = f"

    10 

    11 lemma SM_cases [case_names succeed fail]:

    12   fixes f and s

    13   assumes succeed: "\<And>x s'. execute f h = Some (x, s') \<Longrightarrow> P"

    14   assumes fail: "execute f h = None \<Longrightarrow> P"

    15   shows P

    16   using assms by (cases "execute f h") auto

    17 

    18 lemma SM_execute [simp]:

    19   "SM (execute f) = f" by (cases f) simp_all

    20 

    21 lemma SM_eqI:

    22   "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"

    23     by (cases f, cases g) (auto simp: fun_eq_iff)

    24 

    25 ML {* structure Execute_Simps = Named_Thms

    26 (

    27   val name = @{binding execute_simps}

    28   val description = "simplification rules for execute"

    29 ) *}

    30 

    31 setup Execute_Simps.setup

    32 

    33 lemma execute_Let [execute_simps]:

    34   "execute (let x = t in f x) = (let x = t in execute (f x))"

    35   by (simp add: Let_def)

    36 

    37 

    38 subsubsection {* Specialised lifters *}

    39 

    40 definition sm :: "('state \<Rightarrow> 'a \<times> 'state) \<Rightarrow> ('a, 'state) SM" where

    41   "sm f = SM (Some \<circ> f)"

    42 

    43 definition tap :: "('state \<Rightarrow> 'a) \<Rightarrow> ('a, 'state) SM" where

    44   "tap f = SM (\<lambda>s. Some (f s, s))"

    45 

    46 definition "sm_get = tap id"

    47 

    48 definition "sm_map f = sm (\<lambda> s.((), f s))"

    49 

    50 definition "sm_set s' = sm_map (\<lambda> s. s)"

    51 

    52 lemma execute_tap [execute_simps]:

    53   "execute (tap f) h = Some (f h, h)"

    54   by (simp add: tap_def)

    55 

    56 

    57 lemma execute_heap [execute_simps]:

    58   "execute (sm f) = Some \<circ> f"

    59   by (simp add: sm_def)

    60 

    61 definition guard :: "('state \<Rightarrow> bool) \<Rightarrow> ('state \<Rightarrow> 'a \<times> 'state) 

    62                         \<Rightarrow> ('a, 'state) SM" where

    63  "guard P f = SM (\<lambda>h. if P h then Some (f h) else None)"

    64 

    65 lemma execute_guard [execute_simps]:

    66   "\<not> P h \<Longrightarrow> execute (guard P f) h = None"

    67   "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"

    68   by (simp_all add: guard_def)

    69 

    70 

    71 subsubsection {* Predicate classifying successful computations *}

    72 

    73 definition success :: "('a, 'state) SM \<Rightarrow> 'state \<Rightarrow> bool" where

    74   "success f h = (execute f h \<noteq> None)"

    75 

    76 lemma successI:

    77   "execute f h \<noteq> None \<Longrightarrow> success f h"

    78   by (simp add: success_def)

    79 

    80 lemma successE:

    81   assumes "success f h"

    82   obtains r h' where "r = fst (the (execute c h))"

    83     and "h' = snd (the (execute c h))"

    84     and "execute f h \<noteq> None"

    85   using assms by (simp add: success_def)

    86 

    87 ML {* structure Success_Intros = Named_Thms

    88 (

    89   val name = @{binding success_intros}

    90   val description = "introduction rules for success"

    91 ) *}

    92 

    93 setup Success_Intros.setup

    94 

    95 lemma success_tapI [success_intros]:

    96   "success (tap f) h"

    97   by (rule successI) (simp add: execute_simps)

    98 

    99 lemma success_heapI [success_intros]:

   100   "success (sm f) h"

   101   by (rule successI) (simp add: execute_simps)

   102 

   103 lemma success_guardI [success_intros]:

   104   "P h \<Longrightarrow> success (guard P f) h"

   105   by (rule successI) (simp add: execute_guard)

   106 

   107 lemma success_LetI [success_intros]:

   108   "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"

   109   by (simp add: Let_def)

   110 

   111 lemma success_ifI:

   112   "(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow>

   113     success (if c then t else e) h"

   114   by (simp add: success_def)

   115 

   116 subsubsection {* Predicate for a simple relational calculus *}

   117 

   118 text {*

   119   The @{text effect} predicate states that when a computation @{text c}

   120   runs with the state @{text h} will result in return value @{text r}

   121   and a state @{text "h'"}, i.e.~no exception occurs.

   122 *}  

   123 

   124 definition effect :: "('a, 'state) SM \<Rightarrow> 'state \<Rightarrow> 'state \<Rightarrow> 'a \<Rightarrow> bool" where

   125   effect_def: "effect c h h' r = (execute c h = Some (r, h'))"

   126 

   127 lemma effectI:

   128   "execute c h = Some (r, h') \<Longrightarrow> effect c h h' r"

   129   by (simp add: effect_def)

   130 

   131 lemma effectE:

   132   assumes "effect c h h' r"

   133   obtains "r = fst (the (execute c h))"

   134     and "h' = snd (the (execute c h))"

   135     and "success c h"

   136 proof (rule that)

   137   from assms have *: "execute c h = Some (r, h')" by (simp add: effect_def)

   138   then show "success c h" by (simp add: success_def)

   139   from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"

   140     by simp_all

   141   then show "r = fst (the (execute c h))"

   142     and "h' = snd (the (execute c h))" by simp_all

   143 qed

   144 

   145 lemma effect_success:

   146   "effect c h h' r \<Longrightarrow> success c h"

   147   by (simp add: effect_def success_def)

   148 

   149 lemma success_effectE:

   150   assumes "success c h"

   151   obtains r h' where "effect c h h' r"

   152   using assms by (auto simp add: effect_def success_def)

   153 

   154 lemma effect_deterministic:

   155   assumes "effect f h h' a"

   156     and "effect f h h'' b"

   157   shows "a = b" and "h' = h''"

   158   using assms unfolding effect_def by auto

   159 

   160 ML {* structure Effect_Intros = Named_Thms

   161 (

   162   val name = @{binding effect_intros}

   163   val description = "introduction rules for effect"

   164 ) *}

   165 

   166 ML {* structure Effect_Elims = Named_Thms

   167 (

   168   val name = @{binding effect_elims}

   169   val description = "elimination rules for effect"

   170 ) *}

   171 

   172 setup "Effect_Intros.setup #> Effect_Elims.setup"

   173 

   174 lemma effect_LetI [effect_intros]:

   175   assumes "x = t" "effect (f x) h h' r"

   176   shows "effect (let x = t in f x) h h' r"

   177   using assms by simp

   178 

   179 lemma effect_LetE [effect_elims]:

   180   assumes "effect (let x = t in f x) h h' r"

   181   obtains "effect (f t) h h' r"

   182   using assms by simp

   183 

   184 lemma effect_ifI:

   185   assumes "c \<Longrightarrow> effect t h h' r"

   186     and "\<not> c \<Longrightarrow> effect e h h' r"

   187   shows "effect (if c then t else e) h h' r"

   188   by (cases c) (simp_all add: assms)

   189 

   190 lemma effect_ifE:

   191   assumes "effect (if c then t else e) h h' r"

   192   obtains "c" "effect t h h' r"

   193     | "\<not> c" "effect e h h' r"

   194   using assms by (cases c) simp_all

   195 

   196 lemma effect_tapI [effect_intros]:

   197   assumes "h' = h" "r = f h"

   198   shows "effect (tap f) h h' r"

   199   by (rule effectI) (simp add: assms execute_simps)

   200 

   201 lemma effect_tapE [effect_elims]:

   202   assumes "effect (tap f) h h' r"

   203   obtains "h' = h" and "r = f h"

   204   using assms by (rule effectE) (auto simp add: execute_simps)

   205 

   206 lemma effect_heapI [effect_intros]:

   207   assumes "h' = snd (f h)" "r = fst (f h)"

   208   shows "effect (sm f) h h' r"

   209   by (rule effectI) (simp add: assms execute_simps)

   210 

   211 lemma effect_heapE [effect_elims]:

   212   assumes "effect (sm f) h h' r"

   213   obtains "h' = snd (f h)" and "r = fst (f h)"

   214   using assms by (rule effectE) (simp add: execute_simps)

   215 

   216 lemma effect_guardI [effect_intros]:

   217   assumes "P h" "h' = snd (f h)" "r = fst (f h)"

   218   shows "effect (guard P f) h h' r"

   219   by (rule effectI) (simp add: assms execute_simps)

   220 

   221 lemma effect_guardE [effect_elims]:

   222   assumes "effect (guard P f) h h' r"

   223   obtains "h' = snd (f h)" "r = fst (f h)" "P h"

   224   using assms by (rule effectE)

   225     (auto simp add: execute_simps elim!: successE, 

   226         cases "P h", auto simp add: execute_simps)

   227 

   228 

   229 subsubsection {* Monad combinators *}

   230 

   231 definition return :: "'a \<Rightarrow> ('a, 'state) SM" where

   232        "return x = sm (Pair x)"

   233 

   234 lemma execute_return [execute_simps]:

   235   "execute (return x) = Some \<circ> Pair x"

   236   by (simp add: return_def execute_simps)

   237 

   238 lemma success_returnI [success_intros]:

   239   "success (return x) h"

   240   by (rule successI) (simp add: execute_simps)

   241 

   242 lemma effect_returnI [effect_intros]:

   243   "h = h' \<Longrightarrow> effect (return x) h h' x"

   244   by (rule effectI) (simp add: execute_simps)

   245 

   246 lemma effect_returnE [effect_elims]:

   247   assumes "effect (return x) h h' r"

   248   obtains "r = x" "h' = h"

   249   using assms by (rule effectE) (simp add: execute_simps)

   250 

   251 definition raise :: "string \<Rightarrow> ('a, 'state) SM" where 

   252       -- {* the string is just decoration *}

   253                "raise s = SM (\<lambda>_. None)"

   254 

   255 lemma execute_raise [execute_simps]:

   256   "execute (raise s) = (\<lambda>_. None)"

   257   by (simp add: raise_def)

   258 

   259 lemma effect_raiseE [effect_elims]:

   260   assumes "effect (raise x) h h' r"

   261   obtains "False"

   262   using assms by (rule effectE) (simp add: success_def execute_simps)

   263 

   264 definition bind :: "('a, 'state) SM \<Rightarrow> ('a \<Rightarrow> ('b, 'state) SM) \<Rightarrow> ('b, 'state) SM" where

   265   "bind f g = SM (\<lambda>h. case execute f h of

   266                   Some (x, h') \<Rightarrow> execute (g x) h'

   267                 | None \<Rightarrow> None)"

   268 

   269 adhoc_overloading

   270   Monad_Syntax.bind StateMonad.bind

   271 

   272 

   273 lemma execute_bind [execute_simps]:

   274   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"

   275   "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"

   276   by (simp_all add: bind_def)

   277 

   278 lemma execute_bind_case:

   279   "execute (f \<guillemotright>= g) h = (case (execute f h) of

   280     Some (x, h') \<Rightarrow> execute (g x) h' | None \<Rightarrow> None)"

   281   by (simp add: bind_def)

   282 

   283 lemma execute_bind_success:

   284   "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"

   285   by (cases f h rule: SM_cases) (auto elim!: successE simp add: bind_def)

   286 

   287 lemma success_bind_executeI:

   288   "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"

   289   by (auto intro!: successI elim!: successE simp add: bind_def)

   290 

   291 lemma success_bind_effectI [success_intros]:

   292   "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"

   293   by (auto simp add: effect_def success_def bind_def)

   294 

   295 lemma effect_bindI [effect_intros]:

   296   assumes "effect f h h' r" "effect (g r) h' h'' r'"

   297   shows "effect (f \<guillemotright>= g) h h'' r'"

   298   using assms

   299   apply (auto intro!: effectI elim!: effectE successE)

   300   apply (subst execute_bind, simp_all)

   301   done

   302 

   303 lemma effect_bindE [effect_elims]:

   304   assumes "effect (f \<guillemotright>= g) h h'' r'"

   305   obtains h' r where "effect f h h' r" "effect (g r) h' h'' r'"

   306   using assms by (auto simp add: effect_def bind_def split: option.split_asm)

   307 

   308 lemma execute_bind_eq_SomeI:

   309   assumes "execute f h = Some (x, h')"

   310     and "execute (g x) h' = Some (y, h'')"

   311   shows "execute (f \<guillemotright>= g) h = Some (y, h'')"

   312   using assms by (simp add: bind_def)

   313 

   314 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"

   315   by (rule SM_eqI) (simp add: execute_bind execute_simps)

   316 

   317 lemma bind_return [simp]: "f \<guillemotright>= return = f"

   318   by (rule SM_eqI) (simp add: bind_def execute_simps split: option.splits)

   319 

   320 lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = (f :: ('a, 'state) SM) \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"

   321   by (rule SM_eqI) (simp add: bind_def execute_simps split: option.splits)

   322 

   323 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"

   324   by (rule SM_eqI) (simp add: execute_simps)

   325 

   326 

   327 subsection {* Generic combinators *}

   328 

   329 subsubsection {* Assertions *}

   330 

   331 definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> ('a, 'state) SM" where

   332   "assert P x = (if P x then return x else raise ''assert'')"

   333 

   334 lemma execute_assert [execute_simps]:

   335   "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"

   336   "\<not> P x \<Longrightarrow> execute (assert P x) h = None"

   337   by (simp_all add: assert_def execute_simps)

   338 

   339 lemma success_assertI [success_intros]:

   340   "P x \<Longrightarrow> success (assert P x) h"

   341   by (rule successI) (simp add: execute_assert)

   342 

   343 lemma effect_assertI [effect_intros]:

   344   "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> effect (assert P x) h h' r"

   345   by (rule effectI) (simp add: execute_assert)

   346  

   347 lemma effect_assertE [effect_elims]:

   348   assumes "effect (assert P x) h h' r"

   349   obtains "P x" "r = x" "h' = h"

   350   using assms by (rule effectE) (cases "P x", simp_all add: execute_assert success_def)

   351 

   352 lemma assert_cong [fundef_cong]:

   353   assumes "P = P'"

   354   assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"

   355   shows "(assert P x >>= f) = (assert P' x >>= f')"

   356   by (rule SM_eqI) (insert assms, simp add: assert_def)

   357 

   358 

   359 subsubsection {* Plain lifting *}

   360 

   361 definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b, 'state) SM" where

   362   "lift f = return o f"

   363 

   364 lemma lift_collapse [simp]:

   365   "lift f x = return (f x)"

   366   by (simp add: lift_def)

   367 

   368 lemma bind_lift:

   369   "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"

   370   by (simp add: lift_def comp_def)

   371 

   372 

   373 subsubsection {* Iteration -- warning: this is rarely useful! *}

   374 

   375 primrec fold_map :: "('a \<Rightarrow> ('b, 'state) SM) \<Rightarrow> 'a list \<Rightarrow> ('b list, 'state) SM" where

   376   "fold_map f [] = return []"

   377 | "fold_map f (x # xs) = do {

   378      y \<leftarrow> f x;

   379      ys \<leftarrow> fold_map f xs;

   380      return (y # ys)

   381    }"

   382 

   383 lemma fold_map_append:

   384   "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"

   385   by (induct xs) simp_all

   386 

   387 lemma execute_fold_map_unchanged_heap [execute_simps]:

   388   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"

   389   shows "execute (fold_map f xs) h =

   390     Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"

   391 using assms proof (induct xs)

   392   case Nil show ?case by (simp add: execute_simps)

   393 next

   394   case (Cons x xs)

   395   from Cons.prems obtain y

   396     where y: "execute (f x) h = Some (y, h)" by auto

   397   moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =

   398     Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto

   399   ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)

   400 qed

   401 

   402 

   403 subsection {* Partial function definition setup *}

   404 

   405 definition SM_ord :: "('a, 'state) SM \<Rightarrow> ('a, 'state) SM \<Rightarrow> bool" where

   406   "SM_ord = img_ord execute (fun_ord option_ord)"

   407 

   408 definition SM_lub :: "('a , 'state) SM set \<Rightarrow> ('a, 'state) SM" where

   409   "SM_lub = img_lub execute SM (fun_lub (flat_lub None))"

   410 

   411 interpretation sm!: partial_function_definitions SM_ord SM_lub

   412 proof -

   413   have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))"

   414     by (rule partial_function_lift) (rule flat_interpretation)

   415   then have "partial_function_definitions (img_ord execute (fun_ord option_ord))

   416       (img_lub execute SM (fun_lub (flat_lub None)))"

   417     by (rule partial_function_image) (auto intro: SM_eqI)

   418   then show "partial_function_definitions SM_ord SM_lub"

   419     by (simp only: SM_ord_def SM_lub_def)

   420 qed

   421 

   422 declaration {* Partial_Function.init "sm" @{term sm.fixp_fun}

   423   @{term sm.mono_body} @{thm sm.fixp_rule_uc} @{thm sm.fixp_induct_uc}  NONE *}

   424 

   425 

   426 abbreviation "mono_SM \<equiv> monotone (fun_ord SM_ord) SM_ord"

   427 

   428 lemma SM_ordI:

   429   assumes "\<And>h. execute x h = None \<or> execute x h = execute y h"

   430   shows  "SM_ord x y"

   431   using assms unfolding SM_ord_def img_ord_def fun_ord_def flat_ord_def

   432   by blast

   433 

   434 lemma SM_ordE:

   435   assumes "SM_ord x y"

   436   obtains "execute x h = None" | "execute x h = execute y h"

   437   using assms unfolding SM_ord_def img_ord_def fun_ord_def flat_ord_def

   438   by atomize_elim blast

   439 

   440 lemma bind_mono [partial_function_mono]:

   441   assumes mf: "mono_SM B" and mg: "\<And>y. mono_SM (\<lambda>f. C y f)"

   442   shows "mono_SM (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"

   443 proof (rule monotoneI)

   444   fix f g :: "'a \<Rightarrow> ('b, 'c) SM" assume fg: "fun_ord SM_ord f g"

   445   from mf

   446   have 1: "SM_ord (B f) (B g)" by (rule monotoneD) (rule fg)

   447   from mg

   448   have 2: "\<And>y'. SM_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)

   449 

   450   have "SM_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"

   451     (is "SM_ord ?L ?R")

   452   proof (rule SM_ordI)

   453     fix h

   454     from 1 show "execute ?L h = None \<or> execute ?L h = execute ?R h"

   455       by (rule SM_ordE[where h = h]) (auto simp: execute_bind_case)

   456   qed

   457   also

   458   have "SM_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"

   459     (is "SM_ord ?L ?R")

   460   proof (rule SM_ordI)

   461     fix h

   462     show "execute ?L h = None \<or> execute ?L h = execute ?R h"

   463     proof (cases "execute (B g) h")

   464       case None

   465       then have "execute ?L h = None" by (auto simp: execute_bind_case)

   466       thus ?thesis ..

   467     next

   468       case Some

   469       then obtain r h' where "execute (B g) h = Some (r, h')"

   470         by (metis surjective_pairing)

   471       then have "execute ?L h = execute (C r f) h'"

   472         "execute ?R h = execute (C r g) h'"

   473         by (auto simp: execute_bind_case)

   474       with 2[of r] show ?thesis by (auto elim: SM_ordE)

   475     qed

   476   qed

   477   finally (sm.leq_trans)

   478   show "SM_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .

   479 qed

   480 

   481 end