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