1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Sep_Cancel 8imports Sep_Provers Sep_Tactic_Helpers Sep_Cancel_Set 9begin 10 11(* Sep_Cancel performs cancellative elimination of conjuncts *) 12 13 14lemma sep_curry': "\<lbrakk>(P \<and>* F) s; \<And>s. (Q \<and>* P \<and>* F) s \<Longrightarrow> R s\<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) s" 15 by (metis (full_types) sep.mult_commute sep_curry) 16 17lemma sep_conj_sep_impl_safe: 18 "(P \<longrightarrow>* P') s \<Longrightarrow> (\<And>s. ((P \<longrightarrow>* P') \<and>* Q) s \<Longrightarrow> (Q') s) \<Longrightarrow> (Q \<longrightarrow>* Q') s" 19 by (rule sep_curry) 20 21lemma sep_conj_sep_impl_safe': "P s \<Longrightarrow> (\<And>s. (P \<and>* Q) s \<Longrightarrow> (P \<and>* R) s) \<Longrightarrow> (Q \<longrightarrow>* P \<and>* R) s" 22 by (rule sep_curry) 23 24lemma sep_wand_lens_simple: "(\<And>s. T s = (Q \<and>* R) s) \<Longrightarrow> (P \<longrightarrow>* T) s \<Longrightarrow> (P \<longrightarrow>* Q \<and>* R) s" 25 by (clarsimp simp: sep_impl_def) 26 27schematic_goal schem_impAny: " (?C \<and>* B) s \<Longrightarrow> A s" by (erule sep_mp) 28 29ML \<open> 30 fun sep_cancel_tactic ctxt concl = 31 let val thms = rev (SepCancel_Rules.get ctxt) 32 val tac = assume_tac ctxt ORELSE' 33 eresolve_tac ctxt [@{thm sep_mp}, @{thm sep_conj_empty}, @{thm sep_empty_conj}] ORELSE' 34 sep_erule_tactic ctxt thms 35 val direct_tac = eresolve_tac ctxt thms 36 val safe_sep_wand_tac = rotator' ctxt (resolve0_tac [@{thm sep_wand_lens_simple}]) (eresolve0_tac [@{thm sep_conj_sep_impl_safe'}]) 37 fun sep_cancel_tactic_inner true = sep_erule_full_tac' tac ctxt 38 | sep_cancel_tactic_inner false = sep_erule_full_tac tac ctxt 39 in sep_cancel_tactic_inner concl ORELSE' 40 eresolve_tac ctxt [@{thm sep_curry'}, @{thm sep_conj_sep_impl_safe}, @{thm sep_imp_empty}, @{thm sep_empty_imp'}] ORELSE' 41 safe_sep_wand_tac ORELSE' 42 direct_tac 43 end 44 45 fun sep_cancel_tactic' ctxt concl = 46 let 47 val sep_cancel = sep_cancel_tactic ctxt 48 in 49 (sep_flatten ctxt THEN_ALL_NEW sep_cancel concl) ORELSE' sep_cancel concl 50 end 51 52 fun sep_cancel_method (concl,_) ctxt = SIMPLE_METHOD' (sep_cancel_tactic' ctxt concl) 53 54 val sep_cancel_syntax = 55 Method.sections [Args.add -- Args.colon >> K (Method.modifier SepCancel_Rules.add @{here})]; 56 57 val sep_cancel_syntax' = 58 Scan.lift (Args.mode "concl") -- sep_cancel_syntax 59\<close> 60 61method_setup sep_cancel = 62 \<open>sep_cancel_syntax' >> sep_cancel_method\<close> \<open>Simple elimination of conjuncts\<close> 63 64end 65