src/HOL/Library/State_Monad.thy
author Lars Hupel <lars.hupel@mytum.de>
Wed, 12 Jul 2017 18:42:32 +0200
changeset 66275 2c1d223c5417
parent 66271 d157195a468a
child 67399 eab6ce8368fa
permissions -rw-r--r--
additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66271
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     1
(*  Title:      HOL/Library/State_Monad.thy
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     2
    Author:     Lars Hupel, TU M√ľnchen
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     3
*)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     4
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     5
section \<open>State monad\<close>
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     6
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     7
theory State_Monad
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     8
imports Monad_Syntax
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     9
begin
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    10
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    11
datatype ('s, 'a) state = State (run_state: "'s \<Rightarrow> ('a \<times> 's)")
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    12
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    13
lemma set_state_iff: "x \<in> set_state m \<longleftrightarrow> (\<exists>s s'. run_state m s = (x, s'))"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    14
by (cases m) (simp add: prod_set_defs eq_fst_iff)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    15
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    16
lemma pred_stateI[intro]:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    17
  assumes "\<And>a s s'. run_state m s = (a, s') \<Longrightarrow> P a"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    18
  shows "pred_state P m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    19
proof (subst state.pred_set, rule)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    20
  fix x
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    21
  assume "x \<in> set_state m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    22
  then obtain s s' where "run_state m s = (x, s')"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    23
    by (auto simp: set_state_iff)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    24
  with assms show "P x" .
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    25
qed
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    26
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    27
lemma pred_stateD[dest]:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    28
  assumes "pred_state P m" "run_state m s = (a, s')"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    29
  shows "P a"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    30
proof (rule state.exhaust[of m])
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    31
  fix f
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    32
  assume "m = State f"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    33
  with assms have "pred_fun (\<lambda>_. True) (pred_prod P top) f"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    34
    by (metis state.pred_inject)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    35
  moreover have "f s = (a, s')"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    36
    using assms unfolding \<open>m = _\<close> by auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    37
  ultimately show "P a"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    38
    unfolding pred_prod_beta pred_fun_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    39
    by (metis fst_conv)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    40
qed
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    41
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    42
lemma pred_state_run_state: "pred_state P m \<Longrightarrow> P (fst (run_state m s))"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    43
by (meson pred_stateD prod.exhaust_sel)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    44
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    45
definition state_io_rel :: "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s, 'a) state \<Rightarrow> bool" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    46
"state_io_rel P m = (\<forall>s. P s (snd (run_state m s)))"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    47
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    48
lemma state_io_relI[intro]:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    49
  assumes "\<And>a s s'. run_state m s = (a, s') \<Longrightarrow> P s s'"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    50
  shows "state_io_rel P m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    51
using assms unfolding state_io_rel_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    52
by (metis prod.collapse)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    53
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    54
lemma state_io_relD[dest]:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    55
  assumes "state_io_rel P m" "run_state m s = (a, s')"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    56
  shows "P s s'"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    57
using assms unfolding state_io_rel_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    58
by (metis snd_conv)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    59
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    60
lemma state_io_rel_mono[mono]: "P \<le> Q \<Longrightarrow> state_io_rel P \<le> state_io_rel Q"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    61
by blast
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    62
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    63
lemma state_ext:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    64
  assumes "\<And>s. run_state m s = run_state n s"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    65
  shows "m = n"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    66
using assms
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    67
by (cases m; cases n) auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    68
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    69
context begin
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    70
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    71
qualified definition return :: "'a \<Rightarrow> ('s, 'a) state" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    72
"return a = State (Pair a)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    73
66275
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
    74
lemma run_state_return[simp]: "run_state (return x) s = (x, s)"
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
    75
unfolding return_def
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
    76
by simp
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
    77
66271
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    78
qualified definition ap :: "('s, 'a \<Rightarrow> 'b) state \<Rightarrow> ('s, 'a) state \<Rightarrow> ('s, 'b) state" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    79
"ap f x = State (\<lambda>s. case run_state f s of (g, s') \<Rightarrow> case run_state x s' of (y, s'') \<Rightarrow> (g y, s''))"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    80
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    81
qualified definition bind :: "('s, 'a) state \<Rightarrow> ('a \<Rightarrow> ('s, 'b) state) \<Rightarrow> ('s, 'b) state" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    82
"bind x f = State (\<lambda>s. case run_state x s of (a, s') \<Rightarrow> run_state (f a) s')"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    83
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    84
adhoc_overloading Monad_Syntax.bind bind
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    85
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    86
lemma bind_left_identity[simp]: "bind (return a) f = f a"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    87
unfolding return_def bind_def by simp
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    88
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    89
lemma bind_right_identity[simp]: "bind m return = m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    90
unfolding return_def bind_def by simp
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    91
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    92
lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\<lambda>x. bind (f x) g)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    93
unfolding bind_def by (auto split: prod.splits)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    94
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    95
lemma bind_predI[intro]:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    96
  assumes "pred_state (\<lambda>x. pred_state P (f x)) m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    97
  shows "pred_state P (bind m f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    98
apply (rule pred_stateI)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    99
unfolding bind_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   100
using assms by (auto split: prod.splits)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   101
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   102
qualified definition get :: "('s, 's) state" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   103
"get = State (\<lambda>s. (s, s))"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   104
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   105
qualified definition set :: "'s \<Rightarrow> ('s, unit) state" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   106
"set s' = State (\<lambda>_. ((), s'))"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   107
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   108
lemma get_set[simp]: "bind get set = return ()"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   109
unfolding bind_def get_def set_def return_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   110
by simp
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   111
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   112
lemma set_set[simp]: "bind (set s) (\<lambda>_. set s') = set s'"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   113
unfolding bind_def set_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   114
by simp
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   115
66275
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   116
lemma get_bind_set[simp]: "bind get (\<lambda>s. bind (set s) (f s)) = bind get (\<lambda>s. f s ())"
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   117
unfolding bind_def get_def set_def
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   118
by simp
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   119
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   120
lemma get_const[simp]: "bind get (\<lambda>_. m) = m"
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   121
unfolding get_def bind_def
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   122
by simp
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   123
66271
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   124
fun traverse_list :: "('a \<Rightarrow> ('b, 'c) state) \<Rightarrow> 'a list \<Rightarrow> ('b, 'c list) state" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   125
"traverse_list _ [] = return []" |
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   126
"traverse_list f (x # xs) = do {
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   127
  x \<leftarrow> f x;
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   128
  xs \<leftarrow> traverse_list f xs;
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   129
  return (x # xs)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   130
}"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   131
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   132
lemma traverse_list_app[simp]: "traverse_list f (xs @ ys) = do {
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   133
  xs \<leftarrow> traverse_list f xs;
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   134
  ys \<leftarrow> traverse_list f ys;
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   135
  return (xs @ ys)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   136
}"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   137
by (induction xs) auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   138
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   139
lemma traverse_comp[simp]: "traverse_list (g \<circ> f) xs = traverse_list g (map f xs)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   140
by (induction xs) auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   141
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   142
abbreviation mono_state :: "('s::preorder, 'a) state \<Rightarrow> bool" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   143
"mono_state \<equiv> state_io_rel (op \<le>)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   144
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   145
abbreviation strict_mono_state :: "('s::preorder, 'a) state \<Rightarrow> bool" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   146
"strict_mono_state \<equiv> state_io_rel (op <)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   147
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   148
corollary strict_mono_implies_mono: "strict_mono_state m \<Longrightarrow> mono_state m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   149
unfolding state_io_rel_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   150
by (simp add: less_imp_le)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   151
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   152
lemma return_mono[simp, intro]: "mono_state (return x)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   153
unfolding return_def by auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   154
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   155
lemma get_mono[simp, intro]: "mono_state get"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   156
unfolding get_def by auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   157
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   158
lemma put_mono:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   159
  assumes "\<And>x. s' \<ge> x"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   160
  shows "mono_state (set s')"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   161
using assms unfolding set_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   162
by auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   163
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   164
lemma map_mono[intro]: "mono_state m \<Longrightarrow> mono_state (map_state f m)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   165
by (auto intro!: state_io_relI split: prod.splits simp: map_prod_def state.map_sel)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   166
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   167
lemma map_strict_mono[intro]: "strict_mono_state m \<Longrightarrow> strict_mono_state (map_state f m)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   168
by (auto intro!: state_io_relI split: prod.splits simp: map_prod_def state.map_sel)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   169
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   170
lemma bind_mono_strong:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   171
  assumes "mono_state m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   172
  assumes "\<And>x s s'. run_state m s = (x, s') \<Longrightarrow> mono_state (f x)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   173
  shows "mono_state (bind m f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   174
unfolding bind_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   175
apply (rule state_io_relI)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   176
using assms by (auto split: prod.splits dest!: state_io_relD intro: order_trans)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   177
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   178
lemma bind_strict_mono_strong1:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   179
  assumes "mono_state m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   180
  assumes "\<And>x s s'. run_state m s = (x, s') \<Longrightarrow> strict_mono_state (f x)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   181
  shows "strict_mono_state (bind m f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   182
unfolding bind_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   183
apply (rule state_io_relI)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   184
using assms by (auto split: prod.splits dest!: state_io_relD intro: le_less_trans)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   185
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   186
lemma bind_strict_mono_strong2:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   187
  assumes "strict_mono_state m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   188
  assumes "\<And>x s s'. run_state m s = (x, s') \<Longrightarrow> mono_state (f x)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   189
  shows "strict_mono_state (bind m f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   190
unfolding bind_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   191
apply (rule state_io_relI)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   192
using assms by (auto split: prod.splits dest!: state_io_relD intro: less_le_trans)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   193
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   194
corollary bind_strict_mono_strong:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   195
  assumes "strict_mono_state m"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   196
  assumes "\<And>x s s'. run_state m s = (x, s') \<Longrightarrow> strict_mono_state (f x)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   197
  shows "strict_mono_state (bind m f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   198
using assms by (auto intro: bind_strict_mono_strong1 strict_mono_implies_mono)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   199
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   200
qualified definition update :: "('s \<Rightarrow> 's) \<Rightarrow> ('s, unit) state" where
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   201
"update f = bind get (set \<circ> f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   202
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   203
lemma update_id[simp]: "update (\<lambda>x. x) = return ()"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   204
unfolding update_def return_def get_def set_def bind_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   205
by auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   206
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   207
lemma update_comp[simp]: "bind (update f) (\<lambda>_. update g) = update (g \<circ> f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   208
unfolding update_def return_def get_def set_def bind_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   209
by auto
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   210
66275
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   211
lemma set_update[simp]: "bind (set s) (\<lambda>_. update f) = set (f s)"
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   212
unfolding set_def update_def bind_def get_def set_def
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   213
by simp
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   214
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   215
lemma set_bind_update[simp]: "bind (set s) (\<lambda>_. bind (update f) g) = bind (set (f s)) g"
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   216
unfolding set_def update_def bind_def get_def set_def
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   217
by simp
2c1d223c5417 additional lemmas for State_Monad, courtesy of Andreas Lochbihler
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset
   218
66271
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   219
lemma update_mono:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   220
  assumes "\<And>x. x \<le> f x"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   221
  shows "mono_state (update f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   222
using assms unfolding update_def get_def set_def bind_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   223
by (auto intro!: state_io_relI)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   224
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   225
lemma update_strict_mono:
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   226
  assumes "\<And>x. x < f x"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   227
  shows "strict_mono_state (update f)"
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   228
using assms unfolding update_def get_def set_def bind_def
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   229
by (auto intro!: state_io_relI)
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   230
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   231
end
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   232
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
   233
end