1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory EmptyFailLib
8imports
9  NonDetMonad
10  HaskellLib_H
11begin
12
13(* Collect generic empty_fail lemmas here. naming convention is emtpy_fail_NAME.
14   Unless there is a good reason, they should all be [intro!, simp] *)
15
16lemma empty_fail_when [simp, intro!]:
17  "(P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x)"
18  unfolding when_def by simp
19
20lemma empty_fail_bindD1:
21  "empty_fail (a >>= b) \<Longrightarrow> empty_fail a"
22  unfolding empty_fail_def bind_def
23  apply (clarsimp simp: split_def image_image)
24  apply (drule_tac x = s in spec)
25  apply simp
26  done
27
28lemma empty_fail_liftM [simp, intro!]:
29  "empty_fail (liftM f m) = empty_fail m"
30  unfolding liftM_def
31  apply (rule iffI)
32   apply (erule empty_fail_bindD1)
33  apply (erule empty_fail_bind)
34  apply simp
35  done
36
37lemma empty_fail_assert [simp, intro!]:
38  "empty_fail (assert P)"
39  unfolding empty_fail_def assert_def
40  by (simp add: return_def fail_def)
41
42lemma empty_fail_unless [intro!, simp]:
43  "empty_fail f \<Longrightarrow> empty_fail (unless P f)"
44  by (simp add: unless_def)
45
46lemma empty_fail_stateAssert [intro!, simp]:
47  "empty_fail (stateAssert P l)"
48  by (simp add: stateAssert_def empty_fail_def get_def assert_def
49                return_def fail_def bind_def)
50
51end
52