1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Sep_MP_Example 8imports Sep_MP 9begin 10 11lemma "((P \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* P \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s" 12 (* sep_mp attempts to solve goals that could be solved by careful use of the sep_mp theorem *) 13 apply (sep_mp) 14 apply (clarsimp simp: sep_conj_ac) 15 done 16 17(* Sep_mp uses the sep_cancel set to solve goals *) 18 19axiomatization 20 Moo :: "'a :: stronger_sep_algebra => bool" and 21 Bar :: "'a :: stronger_sep_algebra => bool" 22where Moo_Bar[sep_cancel] : "Moo s \<Longrightarrow> Bar s" 23 24 25lemma "((Bar \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* Moo \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s" 26 apply (sep_mp) 27 apply (clarsimp simp: sep_conj_ac) 28 done 29 30end 31