1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_Tactic_Helpers
8imports Separation_Algebra
9begin
10
11lemmas sep_curry = sep_conj_sep_impl[rotated]
12
13lemma sep_mp: "((Q \<longrightarrow>* R) \<and>* Q) s \<Longrightarrow> R s"
14  by (rule sep_conj_sep_impl2)
15
16lemma sep_mp_frame: "((Q \<longrightarrow>* R) \<and>* Q \<and>* R') s \<Longrightarrow> (R \<and>* R') s"
17  apply (clarsimp simp: sep_conj_assoc[symmetric])
18  apply (erule sep_conj_impl)
19   apply (erule (1) sep_mp)
20  done
21
22lemma sep_empty_conj: "P s \<Longrightarrow> (\<box> \<and>* P) s"
23  by clarsimp
24
25lemma sep_conj_empty: "(\<box> \<and>* P)  s \<Longrightarrow> P s"
26  by clarsimp
27
28lemma sep_empty_imp: "(\<box> \<longrightarrow>* P) s \<Longrightarrow> P s"
29  apply (clarsimp simp: sep_impl_def)
30  apply (erule_tac x=0 in allE)
31  apply (clarsimp)
32  done
33
34lemma sep_empty_imp': "(\<box> \<longrightarrow>* P) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> Q s) \<Longrightarrow> Q s"
35  apply (clarsimp simp: sep_impl_def)
36  apply (erule_tac x=0 in allE)
37  apply (clarsimp)
38  done
39
40lemma sep_imp_empty: " P s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> Q s) \<Longrightarrow> (\<box> \<longrightarrow>* Q) s"
41  by (erule sep_conj_sep_impl, clarsimp)
42
43end
44