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