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