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