1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Sep_Attribs 8imports Separation_Algebra Sep_Tactic_Helpers 9begin 10 11text\<open>Beyond the tactics above, there is also a set of attributes implemented to make proving 12 things in separation logic easier. These rules should be considered internals and are not 13 intended for direct use.\<close> 14 15 16lemma sep_curry_atomised: "\<lbrakk>(\<And>s. (P \<and>* Q) s \<longrightarrow> R s); P s \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) s" 17 by (clarsimp simp: sep_conj_sep_impl) 18 19lemma sep_remove_pure_imp_sep_imp: "( P \<longrightarrow>* (\<lambda>s. P' \<longrightarrow> Q s)) s \<Longrightarrow> P' \<Longrightarrow> (P \<longrightarrow>* Q) s" 20 by (clarsimp) 21 22lemma sep_backward: "\<lbrakk>\<And>s. P s \<longrightarrow> (Q \<and>* T) s; (P \<and>* (Q \<longrightarrow>* R)) s \<rbrakk> \<Longrightarrow> (T \<and>* R) s" 23 by (metis sep_conj_commute sep_conj_impl1 sep_mp_frame) 24 25lemma sep_remove_conj: "\<lbrakk>(P \<and>* R) s ; Q\<rbrakk> \<Longrightarrow> ((\<lambda>s. P s \<and> Q) \<and>* R) s " 26 apply (clarsimp) 27 done 28 29lemma curry: "(P \<longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> (P \<and> Q) \<longrightarrow> R" 30 apply (safe) 31 done 32 33 34ML \<open> 35local 36 fun atomize_thm ctxt thm = Conv.fconv_rule (Object_Logic.atomize ctxt) thm 37 fun setup_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps [(sym OF [@{thm sep_conj_assoc}])] 38 fun simp ctxt thm = simplify (setup_simpset ctxt) thm 39 40 fun REPEAT_TRYOF_N _ thm2 0 = thm2 41 | REPEAT_TRYOF_N thm1 thm2 n = REPEAT_TRYOF_N thm1 (thm1 OF [thm2]) (n-1) 42 43 fun REPEAT_TRYOF'_N thm1 _ 0 = thm1 44 | REPEAT_TRYOF'_N thm1 thm2 n = REPEAT_TRYOF'_N (thm1 OF [thm2]) thm2 (n-1) 45 46 fun attribute_thm ctxt thm thm' = 47 REPEAT_TRYOF_N @{thm sep_remove_pure_imp_sep_imp} (thm OF [atomize_thm ctxt thm']) (Thm.nprems_of thm' - 1) 48 49 fun attribute_thm' thm ctxt thm' = 50 thm OF [REPEAT_TRYOF_N @{thm curry} (thm' |> atomize_thm ctxt o simp ctxt) (Thm.nprems_of thm' - 1)] 51 52in 53 54(* 55 By attributing a theorem with [sep_curry], we can now take a rule (A \<and>* B) \<Longrightarrow> C and turn it into A \<Longrightarrow> (B \<longrightarrow>* C) 56*) 57 58fun sep_curry_inner ctxt = attribute_thm ( ctxt) @{thm sep_curry_atomised} 59val sep_curry = Thm.rule_attribute [] (fn ctxt => sep_curry_inner (Context.proof_of ctxt)) 60 61(* 62 The attribute sep_back takes a rule of the form A \<Longrightarrow> B and returns a rule (A \<and>* (B \<longrightarrow>* R)) \<Longrightarrow> R. 63 The R then matches with any conclusion. If the theorem is of form (A \<and>* B) \<Longrightarrow> C, it is advised to 64 use sep_curry on the theorem first, and then sep_back. This aids sep_cancel in simplifying the result. 65*) 66 67fun backward ctxt thm = 68 REPEAT_TRYOF'_N (attribute_thm' @{thm sep_backward} ctxt thm) @{thm sep_remove_conj} (Thm.nprems_of thm - 1) 69 70fun backward' ctxt thm = backward (Context.proof_of ctxt) thm 71 72val sep_backward = Thm.rule_attribute [] (backward') 73 74end 75\<close> 76 77attribute_setup sep_curry = \<open>Scan.succeed sep_curry\<close> 78attribute_setup sep_backward = \<open>Scan.succeed sep_backward\<close> 79 80end 81