1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_Provers_Example
8imports Sep_Provers
9begin
10
11axiomatization
12  Moo :: "'a :: stronger_sep_algebra => bool" and
13  Bar :: "'a :: stronger_sep_algebra => bool"
14where  Moo_Bar : "Moo s \<Longrightarrow> Bar s"
15
16(* sep_rule is 'rule' with rotations of the conjuncts in the conclusions *)
17lemma "(A \<and>* B \<and>* C \<and>* Bar) s"
18  apply (sep_rule Moo_Bar)
19  oops
20
21(* sep_drule is 'drule' with rotations of the conjuncts in the assumptions *)
22lemma "(A \<and>* B \<and>* C \<and>* Moo) s \<Longrightarrow> R"
23  apply (sep_drule Moo_Bar)
24  oops
25
26(* sep_erule is 'erule' with rotations of the conjuncts in either the assumptions,
27   the conclusions, or both. These are sep_erule, sep_erule_concl, and sep_erule_full respectively
28    *)
29lemma "(A \<and>* B \<and>* C \<and>* Moo) s \<Longrightarrow> (A \<and>* B \<and>* C \<and>* Bar) s"
30   (* In this case we need to rotate both, so we use sep_erule_full *)
31  apply (sep_erule_full Moo_Bar)
32  apply (assumption)
33  done
34
35axiomatization where Moo_Bar_R: "(Moo \<and>* R) s \<Longrightarrow> (Bar \<and>* R) s"
36
37(* When we have theorems with the frame explicitly mentioned, we have to invoke our tactics with
38   (direct) option *)
39
40lemma "(A \<and>* B \<and>* C \<and>* Moo) s \<Longrightarrow> (A \<and>* B \<and>* C \<and>* Bar) s"
41  apply (sep_erule_full (direct) Moo_Bar_R)
42  done
43
44end
45