1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Sep_MP
8imports Sep_Tactic_Helpers Sep_Provers Sep_Cancel_Set
9begin
10
11lemma sep_mp_gen: "((Q \<longrightarrow>* R) \<and>* Q') s \<Longrightarrow> (\<And>s. Q' s \<Longrightarrow> Q s) \<Longrightarrow> R s"
12  by (clarsimp simp: sep_conj_def sep_impl_def)
13
14lemma sep_mp_frame_gen: "\<lbrakk>((Q \<longrightarrow>* R) \<and>* Q' \<and>* R') s; (\<And>s. Q' s \<Longrightarrow> Q s)\<rbrakk> \<Longrightarrow> (R \<and>* R') s"
15    by (metis sep_conj_left_commute sep_globalise sep_mp_frame)
16
17lemma sep_impl_simpl:
18     "(P \<and>* Q \<longrightarrow>* R) s \<Longrightarrow> (P \<longrightarrow>* Q \<longrightarrow>* R) s"
19  apply (erule sep_conj_sep_impl)
20  apply (erule sep_conj_sep_impl)
21  apply (clarsimp simp: sep_conj_assoc)
22  apply (erule sep_mp)
23done
24
25lemma sep_wand_frame_lens: "((P \<longrightarrow>* Q) \<and>* R) s \<Longrightarrow> (\<And>s. T s = R s) ==> ((P \<longrightarrow>* Q) \<and>* T) s"
26  by (metis sep_conj_commute sep_conj_impl1)
27
28ML \<open>
29  fun sep_wand_frame_drule ctxt =
30     let val lens  = dresolve_tac ctxt [@{thm sep_wand_frame_lens}]
31         val lens' = dresolve_tac ctxt [@{thm sep_asm_eq}]
32         val r = rotator' ctxt
33         val sep_cancel_thms = rev (SepCancel_Rules.get ctxt)
34      in sep_apply_tactic ctxt (dresolve_tac ctxt [@{thm sep_mp_frame_gen}]) sep_cancel_thms |> r lens |> r lens'
35   end;
36
37   fun sep_mp_solver ctxt  =
38    let val sep_mp = sep_apply_tactic ctxt (dresolve0_tac [@{thm sep_mp_gen}]) ((rev o SepCancel_Rules.get) ctxt)
39        val taclist = [sep_drule_comb_tac false [@{thm sep_empty_imp}] ctxt,
40                       sep_drule_tac sep_mp ctxt,
41                       sep_drule_tac (sep_drule_tactic ctxt [@{thm sep_impl_simpl}]) ctxt,
42                       sep_wand_frame_drule ctxt ]
43        val check = DETERM o (sep_drule_tac (sep_select_tactic (dresolve0_tac [@{thm sep_wand_frame_lens}]) [1] ctxt) ctxt)
44
45   in  CHANGED_PROP o (check THEN_ALL_NEW REPEAT_ALL_NEW ( FIRST' taclist) )
46   end;
47
48   val sep_mp_method = SIMPLE_METHOD' o sep_mp_solver
49\<close>
50
51method_setup sep_mp = \<open>Scan.succeed sep_mp_method\<close>
52
53end
54