Quellcode-Bibliothek State_Monad.thy Sprache: Isabelle

(*  Title:      HOL/Library/State_Monad.thy
    Author:     Lars Hupel, TU München
*)

section \<open>State monad\<close>

theory State_Monad
imports Monad_Syntax
begin

datatype ('s, 'a) state = State (run_state: "'s \ ('a \ 's)")

lemma set_state_iff: "x \ set_state m \ (\s s'. run_state m s = (x, s'))"
by (cases m) (simp add: prod_set_defs eq_fst_iff)

lemma pred_stateI[intro]:
  assumes "\a s s'. run_state m s = (a, s') \ P a"
  shows "pred_state P m"
proof (subst state.pred_set, rule)
  fix x
  assume "x \ set_state m"
  then obtain s s' where "run_state m s = (x, s')"
    by (auto simp: set_state_iff)
  with assms show "P x" .
qed

lemma pred_stateD[dest]:
  assumes "pred_state P m" "run_state m s = (a, s')"
  shows "P a"
proof (rule state.exhaust[of m])
  fix f
  assume "m = State f"
  with assms have "pred_fun (\_. True) (pred_prod P top) f"
    by (metis state.pred_inject)
  moreover have "f s = (a, s')"
    using assms unfolding \<open>m = _\<close> by auto
  ultimately show "P a"
    unfolding pred_prod_beta pred_fun_def
    by (metis fst_conv)
qed

lemma pred_state_run_state: "pred_state P m \ P (fst (run_state m s))"
by (meson pred_stateD prod.exhaust_sel)

definition state_io_rel :: "('s \ 's \ bool) \ ('s, 'a) state \ bool" where
"state_io_rel P m = (\s. P s (snd (run_state m s)))"

lemma state_io_relI[intro]:
  assumes "\a s s'. run_state m s = (a, s') \ P s s'"
  shows "state_io_rel P m"
using assms unfolding state_io_rel_def
by (metis prod.collapse)

lemma state_io_relD[dest]:
  assumes "state_io_rel P m" "run_state m s = (a, s')"
  shows "P s s'"
using assms unfolding state_io_rel_def
by (metis snd_conv)

lemma state_io_rel_mono[mono]: "P \ Q \ state_io_rel P \ state_io_rel Q"
by blast

lemma state_ext:
  assumes "\s. run_state m s = run_state n s"
  shows "m = n"
using assms
by (cases m; cases n) auto

context begin

qualified definition return :: "'a \ ('s, 'a) state" where
"return a = State (Pair a)"

lemma run_state_return[simp]: "run_state (return x) s = (x, s)"
unfolding return_def
by simp

qualified definition ap :: "('s, 'a \ 'b) state \ ('s, 'a) state \ ('s, 'b) state" where
"ap f x = State (\s. case run_state f s of (g, s') \ case run_state x s' of (y, s'') \ (g y, s''))"

lemma run_state_ap[simp]:
  "run_state (ap f x) s = (case run_state f s of (g, s') \ case run_state x s' of (y, s'') \ (g y, s''))"
unfolding ap_def by auto

qualified definition bind :: "('s, 'a) state \ ('a \ ('s, 'b) state) \ ('s, 'b) state" where
"bind x f = State (\s. case run_state x s of (a, s') \ run_state (f a) s')"

lemma run_state_bind[simp]:
  "run_state (bind x f) s = (case run_state x s of (a, s') \ run_state (f a) s')"
unfolding bind_def by auto

adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind

lemma bind_left_identity[simp]: "bind (return a) f = f a"
unfolding return_def bind_def by simp

lemma bind_right_identity[simp]: "bind m return = m"
unfolding return_def bind_def by simp

lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\x. bind (f x) g)"
unfolding bind_def by (auto split: prod.splits)

lemma bind_predI[intro]:
  assumes "pred_state (\x. pred_state P (f x)) m"
  shows "pred_state P (bind m f)"
apply (rule pred_stateI)
unfolding bind_def
using assms by (auto split: prod.splits)

qualified definition get :: "('s, 's) state" where
"get = State (\s. (s, s))"

lemma run_state_get[simp]: "run_state get s = (s, s)"
unfolding get_def by simp

qualified definition set :: "'s \ ('s, unit) state" where
"set s' = State (\_. ((), s'))"

lemma run_state_set[simp]: "run_state (set s') s = ((), s')"
unfolding set_def by simp

lemma get_set[simp]: "bind get set = return ()"
unfolding bind_def get_def set_def return_def
by simp

lemma set_set[simp]: "bind (set s) (\_. set s') = set s'"
unfolding bind_def set_def
by simp

lemma get_bind_set[simp]: "bind get (\s. bind (set s) (f s)) = bind get (\s. f s ())"
unfolding bind_def get_def set_def
by simp

lemma get_const[simp]: "bind get (\_. m) = m"
unfolding get_def bind_def
by simp

fun traverse_list :: "('a \ ('b, 'c) state) \ 'a list \ ('b, 'c list) state" where
"traverse_list _ [] = return []" |
"traverse_list f (x # xs) = do {
  x \<leftarrow> f x;
  xs \<leftarrow> traverse_list f xs;
  return (x # xs)
}"

lemma traverse_list_app[simp]: "traverse_list f (xs @ ys) = do {
  xs \<leftarrow> traverse_list f xs;
  ys \<leftarrow> traverse_list f ys;
  return (xs @ ys)
}"
by (induction xs) auto

lemma traverse_comp[simp]: "traverse_list (g \ f) xs = traverse_list g (map f xs)"
by (induction xs) auto

abbreviation mono_state :: "('s::preorder, 'a) state \ bool" where
"mono_state \ state_io_rel (\)"

abbreviation strict_mono_state :: "('s::preorder, 'a) state \ bool" where
"strict_mono_state \ state_io_rel (<)"

corollary strict_mono_implies_mono: "strict_mono_state m \ mono_state m"
unfolding state_io_rel_def
by (simp add: less_imp_le)

lemma return_mono[simp, intro]: "mono_state (return x)"
unfolding return_def by auto

lemma get_mono[simp, intro]: "mono_state get"
unfolding get_def by auto

lemma put_mono:
  assumes "\x. s' \ x"
  shows "mono_state (set s')"
using assms unfolding set_def
by auto

lemma map_mono[intro]: "mono_state m \ mono_state (map_state f m)"
by (auto intro!: state_io_relI split: prod.splits simp: map_prod_def state.map_sel)

lemma map_strict_mono[intro]: "strict_mono_state m \ strict_mono_state (map_state f m)"
by (auto intro!: state_io_relI split: prod.splits simp: map_prod_def state.map_sel)

lemma bind_mono_strong:
  assumes "mono_state m"
  assumes "\x s s'. run_state m s = (x, s') \ mono_state (f x)"
  shows "mono_state (bind m f)"
unfolding bind_def
apply (rule state_io_relI)
using assms by (auto split: prod.splits dest!: state_io_relD intro: order_trans)

lemma bind_strict_mono_strong1:
  assumes "mono_state m"
  assumes "\x s s'. run_state m s = (x, s') \ strict_mono_state (f x)"
  shows "strict_mono_state (bind m f)"
unfolding bind_def
apply (rule state_io_relI)
using assms by (auto split: prod.splits dest!: state_io_relD intro: le_less_trans)

lemma bind_strict_mono_strong2:
  assumes "strict_mono_state m"
  assumes "\x s s'. run_state m s = (x, s') \ mono_state (f x)"
  shows "strict_mono_state (bind m f)"
unfolding bind_def
apply (rule state_io_relI)
using assms by (auto split: prod.splits dest!: state_io_relD intro: less_le_trans)

corollary bind_strict_mono_strong:
  assumes "strict_mono_state m"
  assumes "\x s s'. run_state m s = (x, s') \ strict_mono_state (f x)"
  shows "strict_mono_state (bind m f)"
using assms by (auto intro: bind_strict_mono_strong1 strict_mono_implies_mono)

qualified definition update :: "('s \ 's) \ ('s, unit) state" where
"update f = bind get (set \ f)"

lemma update_id[simp]: "update (\x. x) = return ()"
unfolding update_def return_def get_def set_def bind_def
by auto

lemma update_comp[simp]: "bind (update f) (\_. update g) = update (g \ f)"
unfolding update_def return_def get_def set_def bind_def
by auto

lemma set_update[simp]: "bind (set s) (\_. update f) = set (f s)"
unfolding set_def update_def bind_def get_def set_def
by simp

lemma set_bind_update[simp]: "bind (set s) (\_. bind (update f) g) = bind (set (f s)) g"
unfolding set_def update_def bind_def get_def set_def
by simp

lemma update_mono:
  assumes "\x. x \ f x"
  shows "mono_state (update f)"
using assms unfolding update_def get_def set_def bind_def
by (auto intro!: state_io_relI)

lemma update_strict_mono:
  assumes "\x. x < f x"
  shows "strict_mono_state (update f)"
using assms unfolding update_def get_def set_def bind_def
by (auto intro!: state_io_relI)

end

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.26Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.