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