equal
deleted
inserted
replaced
138 |
138 |
139 lemma traverse_comp[simp]: "traverse_list (g \<circ> f) xs = traverse_list g (map f xs)" |
139 lemma traverse_comp[simp]: "traverse_list (g \<circ> f) xs = traverse_list g (map f xs)" |
140 by (induction xs) auto |
140 by (induction xs) auto |
141 |
141 |
142 abbreviation mono_state :: "('s::preorder, 'a) state \<Rightarrow> bool" where |
142 abbreviation mono_state :: "('s::preorder, 'a) state \<Rightarrow> bool" where |
143 "mono_state \<equiv> state_io_rel (op \<le>)" |
143 "mono_state \<equiv> state_io_rel (\<le>)" |
144 |
144 |
145 abbreviation strict_mono_state :: "('s::preorder, 'a) state \<Rightarrow> bool" where |
145 abbreviation strict_mono_state :: "('s::preorder, 'a) state \<Rightarrow> bool" where |
146 "strict_mono_state \<equiv> state_io_rel (op <)" |
146 "strict_mono_state \<equiv> state_io_rel (<)" |
147 |
147 |
148 corollary strict_mono_implies_mono: "strict_mono_state m \<Longrightarrow> mono_state m" |
148 corollary strict_mono_implies_mono: "strict_mono_state m \<Longrightarrow> mono_state m" |
149 unfolding state_io_rel_def |
149 unfolding state_io_rel_def |
150 by (simp add: less_imp_le) |
150 by (simp add: less_imp_le) |
151 |
151 |