1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Sep_Provers 8imports Sep_Rotate 9begin 10 11(* Constrained lens for sep_erule tactic *) 12lemma sep_asm_eq_erule: 13 "(P \<and>* R) s \<Longrightarrow> (\<And>s. T s = (P \<and>* R) s) \<Longrightarrow> (T s \<Longrightarrow> (P' \<and>* R') s) \<Longrightarrow> (P' \<and>* R') s" 14 by (clarsimp) 15 16lemma sep_rule: 17 "(\<And>s. T s \<Longrightarrow> P s) \<Longrightarrow> (T \<and>* R) s \<Longrightarrow> (P \<and>* R) s" 18 by (rule sep_conj_impl1) 19 20lemma sep_erule: 21 "(T \<and>* R') s \<Longrightarrow> (\<And>s. T s \<Longrightarrow> P s) \<Longrightarrow> (\<And>s. R' s \<Longrightarrow> R s) \<Longrightarrow> (P \<and>* R) s" 22 by (rule sep_conj_impl) 23 24(* Construct analogues to rule/drule etc, for separation logic *) 25 26ML \<open> 27fun sep_select ctxt = resolve_tac ctxt [@{thm sep_eq}] 28fun sep_asm_select ctxt = dresolve_tac ctxt [@{thm sep_asm_eq}] 29fun sep_asm_erule_select ctxt = eresolve_tac ctxt [@{thm sep_asm_eq_erule}] 30 31fun sep_rule_tactic ctxt thms = 32 let val sep_rule = resolve_tac ctxt [@{thm sep_rule}] 33 in sep_apply_tactic ctxt sep_rule thms end 34 35fun sep_drule_tactic ctxt thms = 36 let val sep_drule = dresolve_tac ctxt [rotate_prems ~1 @{thm sep_rule}] 37 in sep_apply_tactic ctxt sep_drule thms end 38 39fun sep_frule_tactic ctxt thms = 40 let val sep_frule = forward_tac ctxt [rotate_prems ~1 @{thm sep_rule}] 41 in sep_apply_tactic ctxt sep_frule thms end 42 43fun sep_erule_tactic ctxt thms = 44 let val sep_erule = (eresolve_tac ctxt [@{thm sep_erule}]) 45 in sep_apply_tactic ctxt sep_erule thms end 46 47fun sep_rule_tac tac ctxt = rotator (sep_select ctxt) tac ctxt 48fun sep_drule_tac tac ctxt = rotator (sep_asm_select ctxt) tac ctxt 49fun sep_erule_tac tac ctxt = rotator (sep_asm_select ctxt) tac ctxt 50fun sep_erule_concl_tac tac ctxt = rotator (sep_select ctxt) tac ctxt 51 52fun sep_erule_full_tac tac ctxt = 53 let val r = rotator' ctxt 54 in 55 tac |> r (sep_asm_erule_select ctxt) |> r (sep_select ctxt) 56 end 57 58fun sep_erule_full_tac' tac ctxt = 59 let val r = rotator' ctxt 60 in 61 tac |> r (sep_select ctxt) |> r (sep_asm_erule_select ctxt) 62 end 63 64fun sep_rule_comb_tac true thms ctxt = sep_rule_tac (resolve_tac ctxt thms) ctxt 65 | sep_rule_comb_tac false thms ctxt = sep_rule_tac (sep_rule_tactic ctxt thms) ctxt 66 67fun sep_rule_method bool thms ctxt = SIMPLE_METHOD' (sep_rule_comb_tac bool thms ctxt) 68 69fun sep_drule_comb_tac true thms ctxt = sep_drule_tac (dresolve_tac ctxt thms) ctxt 70 | sep_drule_comb_tac false thms ctxt = sep_drule_tac (sep_drule_tactic ctxt thms) ctxt 71 72fun sep_drule_method bool thms ctxt = SIMPLE_METHOD' (sep_drule_comb_tac bool thms ctxt) 73 74fun sep_frule_method true thms ctxt = SIMPLE_METHOD' (sep_drule_tac (forward_tac ctxt thms) ctxt) 75 | sep_frule_method false thms ctxt = SIMPLE_METHOD' (sep_drule_tac (sep_frule_tactic ctxt thms) ctxt) 76 77fun sep_erule_method true thms ctxt = SIMPLE_METHOD' (sep_erule_tac (eresolve_tac ctxt thms) ctxt) 78 | sep_erule_method false thms ctxt = SIMPLE_METHOD' (sep_erule_tac (sep_erule_tactic ctxt thms) ctxt) 79 80fun sep_erule_concl_method true thms ctxt = 81 SIMPLE_METHOD' (sep_erule_concl_tac (eresolve_tac ctxt thms) ctxt) 82 | sep_erule_concl_method false thms ctxt = 83 SIMPLE_METHOD' (sep_erule_concl_tac (sep_erule_tactic ctxt thms) ctxt) 84 85fun sep_erule_full_method true thms ctxt = 86 SIMPLE_METHOD' (sep_erule_full_tac (eresolve_tac ctxt thms) ctxt) 87 | sep_erule_full_method false thms ctxt = 88 SIMPLE_METHOD' (sep_erule_full_tac (sep_erule_tactic ctxt thms) ctxt) 89\<close> 90 91method_setup sep_rule = \<open> 92 Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_rule_method 93\<close> 94 95method_setup sep_drule = \<open> 96 Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_drule_method 97\<close> 98 99method_setup sep_frule = \<open> 100 Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_frule_method 101\<close> 102 103method_setup sep_erule = \<open> 104 Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_erule_method 105\<close> 106 107method_setup sep_erule_concl = \<open> 108 Scan.lift (Args.mode "direct") -- Attrib.thms >> uncurry sep_erule_concl_method 109\<close> 110 111method_setup sep_erule_full = \<open> 112 Scan.lift (Args.mode "direct") -- Attrib.thms>> uncurry sep_erule_full_method 113\<close> 114 115end 116