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