1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_Cancel_Set
8imports Separation_Algebra Sep_Tactic_Helpers
9begin
10
11ML \<open>
12  structure SepCancel_Rules = Named_Thms (
13    val name = @{binding "sep_cancel"}
14    val description = "sep_cancel rules"
15  )
16\<close>
17
18setup SepCancel_Rules.setup
19
20lemma refl_imp: "P \<Longrightarrow> P" by assumption
21
22declare refl_imp[sep_cancel]
23
24declare sep_conj_empty[sep_cancel]
25lemmas sep_conj_empty' = sep_conj_empty[simplified sep_conj_commute[symmetric]]
26declare sep_conj_empty'[sep_cancel]
27
28
29end
30