1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Sep_Forward 8imports 9 Extended_Separation_Algebra 10 Sep_Util 11begin 12 13lemma sep_conj_sep_impl_spec: 14 "\<lbrakk>((Q -* R) \<and>* P) h; \<And>h. (Q -* R) h \<Longrightarrow> (P \<longrightarrow>* R') h\<rbrakk> \<Longrightarrow> R' h" 15 by (metis (full_types) sep_conj_sep_impl2) 16 17 18method sep_invert = ((erule sep_septraction_snake | sep_erule (direct) sep_conj_sep_impl_spec), 19 sep_flatten?; sep_invert?) 20 21lemma sep_conj_coimpl_cancel: "(P \<and>* R) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> P s) \<Longrightarrow> precise P \<Longrightarrow> 22 (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" 23 apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) 24 apply (clarsimp simp: precise_def) 25 apply (erule_tac x=s in allE) 26 apply (erule_tac x=x in allE) 27 apply (erule_tac x=xa in allE) 28 apply (clarsimp, drule mp) 29 apply (intro conjI) 30 apply (fastforce simp: sep_substate_def) 31 apply (fastforce simp: sep_substate_def) 32 apply (clarsimp) 33 by (metis sep_add_cancelD sep_add_commute sep_disj_commuteI) 34 35lemma sep_conj_coimpl_cancel': "(P \<and>* R) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> Q s) \<Longrightarrow> precise Q \<Longrightarrow> 36 (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" 37 apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) 38 apply (clarsimp simp: precise_def) 39 apply (erule_tac x=s in allE) 40 apply (erule_tac x=x in allE) 41 apply (erule_tac x=xa in allE) 42 apply (clarsimp, drule mp) 43 apply (intro conjI) 44 apply (fastforce simp: sep_substate_def) 45 apply (fastforce simp: sep_substate_def) 46 apply (clarsimp) 47 by (metis sep_add_cancelD sep_add_commute sep_disj_commuteI) 48 49lemma sep_conj_coimpl_cancel'': 50 "(\<And>s. pred_imp P Q s) \<Longrightarrow> (P \<and>* R) s \<Longrightarrow> precise Q \<Longrightarrow> 51 (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" 52 by (simp add: sep_conj_coimpl_cancel') 53 54lemma sep_conj_coimpl_cancel''': 55 "(\<And>s. pred_imp Q P s) \<Longrightarrow> (P \<and>* R) s \<Longrightarrow> precise P \<Longrightarrow> 56 (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" 57 by (simp add: sep_conj_coimpl_cancel) 58 59lemma sep_coimpl_cancel': 60 "(\<And>s. pred_imp Q P s) \<Longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> 61 (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" 62 by (metis pred_neg_def sep_coimpl_def sep_conj_def) 63 64definition "pointer P \<equiv> (\<forall>x y. \<forall>s R. (P x \<and>* R) s \<longrightarrow> (P y \<leadsto>* R and (\<lambda>s. x = y)) s)" 65 66lemma sep_conj_pointer_coimpl_cancel: 67 "(P x \<and>* R) s \<Longrightarrow> pointer P \<Longrightarrow> 68 (\<And>s. R s \<Longrightarrow> y = x \<Longrightarrow> R' s) \<Longrightarrow> (P y \<leadsto>* R') s" 69 apply (clarsimp simp: pointer_def) 70 apply (erule_tac x=x in allE) 71 apply (erule_tac x=y in allE) 72 apply (erule_tac x=s in allE) 73 apply (erule_tac x=R in allE) 74 apply (clarsimp simp: pred_conj_def) 75 apply (erule sep_coimpl_cancel'[rotated]; simp) 76 done 77 78named_theorems precise 79 80method septract_cancel declares precise = 81 ((sep_erule (direct) sep_cancel[simplified atomize_imp, THEN sep_conj_coimpl_cancel''], rule precise) | 82 (sep_erule (direct) sep_cancel[simplified atomize_imp, THEN sep_conj_coimpl_cancel'''], rule precise) | 83 erule sep_cancel[simplified atomize_imp, THEN sep_coimpl_cancel'] | 84 (sep_erule (direct) sep_conj_pointer_coimpl_cancel , rule precise)) 85 86method abs_used for P = (match (P) in "\<lambda>s. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>) 87 88method sep_lift = match conclusion in "(_ \<longrightarrow>* _) s" for s :: "_ :: sep_algebra" \<Rightarrow> 89 \<open>((match premises in I[thin]: "P s" for P \<Rightarrow> 90 \<open>abs_used P, rule sep_curry[where h=s and P=P, rotated, OF I]\<close>))\<close> 91 92method sep_snake_uncurry = match conclusion in "(_ \<leadsto>* _) s" for s :: "_ :: sep_algebra" \<Rightarrow> 93 \<open>((match premises in I[thin]: "P s" for P \<Rightarrow> 94 \<open>abs_used P, rule sep_snake_septraction[where s=s and Q=P, OF I]\<close>))\<close> 95 96lemma septract_impl_cancel: "(P -* Q) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> strictly_exact P \<Longrightarrow> (P \<longrightarrow>* Q') s" 97 apply (clarsimp simp: septraction_def sep_impl_def pred_neg_def strictly_exact_def) 98 by (fastforce) 99 100method sep_forward = (sep_cancel | septract_cancel | sep_lift | 101 sep_snake_uncurry ) 102 103method sep_forward_solve = (solves \<open>sep_invert; (sep_forward) +\<close>) 104 105method sep_cancel uses add = (Sep_Cancel.sep_cancel add: add | sep_lift) 106 107lemma septract_mp: "\<lbrakk>(R' \<and>* (R' -* R)) s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'\<rbrakk> \<Longrightarrow> R s" 108 apply (sep_invert) 109 apply (atomize, erule allE, drule (1) mp) 110 using precise_conj_coimpl by blast 111 112end