1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Lemmas and automation for automatically cancelling shared parts of the heap predicate 8 * in a sep_fold 9 *) 10 11theory Sep_Fold_Cancel 12imports 13 Sep_Algebra_L4v 14 Sep_Forward 15begin 16 17lemma sep_fold_cong1: "(\<And>x s. P x s = P' x s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P' Q R xs s" 18 apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) 19 apply (erule sep_conj_impl, fastforce) 20 apply (sep_cancel, sep_mp) 21 by (clarsimp) 22 23lemma sep_fold_cong2: "(\<And>x s. Q x s = Q' x s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P Q' R xs s" 24 apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) 25 apply (erule sep_conj_impl, fastforce) 26 apply (sep_cancel) 27 apply (sep_drule (direct) sep_mp_gen) 28 by (clarsimp) 29 30lemma sep_fold_cong3: "(\<And> s. R s = R' s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P Q R' xs s" 31 apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) 32 apply (erule sep_conj_impl, fastforce) 33 apply (sep_cancel) 34 apply (sep_drule (direct) sep_mp_gen) 35 by (clarsimp) 36 37lemma sep_fold_strengthen_final: 38 "\<lbrakk>\<And>s. R s \<Longrightarrow> R' s; 39 \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s\<rbrakk> 40 \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> xs s" 41 apply (induct xs arbitrary: s) 42 apply (clarsimp simp: sep_fold_def) 43 apply (clarsimp simp: sep_fold_def) 44 apply (sep_cancel)+ 45 apply (sep_mp) 46 apply (clarsimp) 47 done 48 49lemma sep_factor_foldI__: 50 "(\<And>* map P xs \<and>* foldr (\<lambda>x R. Q x \<longrightarrow>* R) xs R) s \<Longrightarrow> sep_fold P Q R xs s" 51 apply (clarsimp simp: sep_fold_def) 52 apply (induct xs arbitrary: s; clarsimp) 53 apply sep_cancel+ 54 apply sep_mp 55 apply (clarsimp simp: sep_conj_ac) 56 done 57 58lemma sep_factor_foldI_: 59 "(\<And>* map (\<lambda>_. I) xs \<and>* sep_fold P Q R xs) s \<Longrightarrow> sep_fold (\<lambda>x. I \<and>* P x) Q R xs s" 60 apply (induct xs arbitrary: s) 61 apply (clarsimp simp: sep_fold_def) 62 apply (clarsimp simp: sep_fold_def) 63 apply (sep_cancel+, clarsimp, sep_mp) 64 apply (clarsimp simp: sep_conj_ac) 65 done 66 67lemma sep_factor_foldI': 68 "(I \<and>* (sep_fold P Q (I \<longrightarrow>* R) xs)) s \<Longrightarrow> sep_fold (\<lambda>x. I \<and>* P x) (\<lambda>x. I \<and>* Q x) R xs s" 69 apply (induct xs arbitrary:s; clarsimp simp: sep_fold_def) 70 apply (sep_solve) 71 apply (sep_cancel)+ 72 apply (sep_mp) 73 apply (clarsimp simp: sep_conj_ac) 74 done 75 76lemma sep_factor_foldI'': 77 "(\<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s) \<Longrightarrow> 78 precise R' \<Longrightarrow> 79 (R' \<and>* sep_fold P Q (R' -* R) xs) s \<Longrightarrow> 80 sep_fold (\<lambda>x. R' \<and>* P x) (\<lambda>x. R' \<and>* Q x) R xs s" 81 apply (induct xs arbitrary:s; clarsimp simp: sep_fold_def) 82 apply (erule septract_mp[where R'=R']) 83 apply (assumption)+ 84 apply (clarsimp simp: sep_conj_ac) 85 apply (sep_cancel)+ 86 apply (sep_mp) 87 by (clarsimp simp: sep_conj_ac) 88 89ML \<open> 90 fun sep_fold_tactic ctxt = 91 rotator' ctxt (resolve_tac ctxt [@{thm sep_fold_cong2 }]) 92 (resolve_tac ctxt [@{thm sep_factor_foldI' }]) |> 93 rotator' ctxt (resolve_tac ctxt [@{thm sep_fold_cong1 }]); 94\<close> 95 96method_setup sep_fold_cancel_inner = 97 \<open>Scan.succeed (SIMPLE_METHOD' o sep_fold_tactic)\<close> \<open>Simple elimination of conjuncts\<close> 98 99(* Cancels out shared resources according to the rule sep_factor_foldI' *) 100 101lemma sep_map_set_sep_foldI: 102 "distinct xs \<Longrightarrow> 103 (sep_map_set_conj P (set xs) \<and>* (sep_map_set_conj Q (set xs) \<longrightarrow>* R)) s \<Longrightarrow> 104 \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s" 105 apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) 106 apply (sep_solve) 107 apply (sep_cancel)+ 108 apply (sep_mp) 109 apply (clarsimp simp: sep_conj_ac) 110 done 111 112lemma sep_fold_pure: "P \<Longrightarrow> sep_fold P' Q R xs s \<Longrightarrow> sep_fold (\<lambda>x s. P \<and> P' x s) Q R xs s " 113 by (clarsimp simp: sep_fold_def) 114 115lemma sep_fold_pure': 116 "sep_fold P' Q R xs s \<Longrightarrow> 117 (\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow> 118 sep_fold (\<lambda>x s. P x \<and> P' x s) Q R xs s " 119 apply (clarsimp simp: sep_fold_def) 120 apply (induct xs arbitrary: s; clarsimp) 121 apply (sep_cancel)+ 122 apply (sep_mp) 123 apply (clarsimp) 124 done 125 126lemma sep_fold_pure'': 127 "sep_fold P' Q R xs s \<Longrightarrow> 128 (\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow> 129 sep_fold (\<lambda>x s. P' x s \<and> P x ) Q R xs s " 130 apply (clarsimp simp: sep_fold_def) 131 apply (induct xs arbitrary: s; clarsimp) 132 apply (sep_cancel)+ 133 apply (sep_mp) 134 apply (clarsimp) 135 done 136 137method sep_fold_cancel = ( 138 sep_flatten?, 139 ((rule sep_fold_pure' sep_fold_pure'')+)?, 140 (sep_fold_cancel_inner, sep_cancel, sep_flatten?)+ 141) 142 143end 144