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