1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_Solve_Example
8imports Sep_Solve
9begin
10
11(* sep_solve invokes sep_cancel and sep_mp repeatedly to solve the goal, and fails if it can't
12   completely discharge it *)
13axiomatization
14  Moo :: "'a :: stronger_sep_algebra => bool" and
15  Bar :: "'a :: stronger_sep_algebra => bool"
16where  Moo_Bar[sep_cancel] : "Moo s \<Longrightarrow> Bar s"
17
18lemma "((Bar \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* Moo \<and>* A \<and>* R \<and>* Q) s \<Longrightarrow> (A \<and>* B) s"
19  apply (sep_solve)
20  done
21
22(* encouraging better proof style with different command for schematics in assumption *)
23
24schematic_goal "((Bar \<and>* Q \<and>* R \<longrightarrow>* B) \<and>* Moo \<and>* A \<and>* R \<and>* ?Q) s \<Longrightarrow> (A \<and>* B) s"
25  apply (sep_schem)
26  done
27
28end
29