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