1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Extract_Conjunct 8imports 9 "Main" 10 "Eisbach_Methods" 11begin 12 13section \<open>Extracting conjuncts in the conclusion\<close> 14 15text \<open> 16Methods for extracting a conjunct from a nest of conjuncts in the conclusion 17of a goal, typically by pattern matching. 18 19When faced with a conclusion which is a big conjunction, it is often the case 20that a small number of conjuncts require special attention, while the rest can 21be solved easily by @{method clarsimp}, @{method auto} or similar. However, 22sometimes the method that would solve the bulk of the conjuncts would put some 23of the conjuncts into a more difficult or unsolvable state. 24 25The higher-order methods defined here provide an efficient way to select a 26conjunct requiring special treatment, so that it can be dealt with first. Once 27all such conjuncts have been removed, the remaining conjuncts can all be solved 28together by some automated method. 29 30Each method takes an inner method as an argument, and selects the leftmost 31conjunct for which that inner method succeeds. The methods differ according to 32what they do with the selected conjunct. See below for more information and 33some simple examples. 34\<close> 35 36context begin 37 38subsection \<open>Focused conjunct with context\<close> 39 40text \<open> 41We define a predicate which allows us to identify a particular sub-tree and its 42context within a nest of conjunctions. We express this sub-tree-with-context using 43a function which reconstructs the original nest of conjunctions. The context 44consists of a list of parent contexts, where each parent context consists of a 45sibling sub-tree, and a tag indicating whether the focused sub-tree is on the left 46or right. Rebuilding the original tree works from the focused sub-tree up towards 47the root of the original structure. This sub-tree-with-context is sometimes known 48as a zipper. 49\<close> 50 51private fun focus_conj :: "bool \<Rightarrow> bool list \<Rightarrow> bool" where 52 "focus_conj current [] = current" 53| "focus_conj current (sibling # parents) = focus_conj (current \<and> sibling) parents" 54 55private definition "focus \<equiv> focus_conj" 56 57private definition "tag t P \<equiv> P" 58private lemmas focus_defs = focus_def tag_def 59 60private abbreviation "left \<equiv> tag Left" 61private abbreviation "right \<equiv> tag Right" 62 63private lemma focus_example: 64 "focus C [right B, left D, left E, right A] \<longleftrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" 65 unfolding focus_defs by auto 66 67subsection \<open>Moving the focus\<close> 68 69text \<open> 70We now prove some rules which allow us to switch between focused and unfocused 71structures, and to move the focus around. Some versions of these rules carry an 72extra conjunct @{term E} outside the structure. Once we find the conjunct we want, 73this @{term E} allows to keep track of it while we reassemble the rest of the 74original structure. 75 76First, we have rules for going between focused and unfocused structures. 77\<close> 78 79private lemma focus_top_iff: "E \<and> focus P [] \<longleftrightarrow> E \<and> P" 80 unfolding focus_def by simp 81 82private lemmas to_focus = focus_top_iff[where E=True, simplified, THEN iffD1] 83private lemmas from_focusE = focus_top_iff[THEN iffD2] 84private lemmas from_focus = from_focusE[where E=True, simplified] 85 86text \<open> 87Next, we have rules for moving the focus to and from the left conjunct. 88\<close> 89 90private lemma focus_left_iff: "E \<and> focus L (left R # P) \<longleftrightarrow> E \<and> focus (L \<and> R) P" 91 unfolding focus_defs by simp 92 93private lemmas focus_left = focus_left_iff[where E=True, simplified, THEN iffD1] 94private lemmas unfocusE_left = focus_left_iff[THEN iffD2] 95private lemmas unfocus_left = unfocusE_left[where E=True, simplified] 96 97text \<open> 98Next, we have rules for moving the focus to and from the right conjunct. 99\<close> 100 101private lemma focus_right_iff: "E \<and> focus R (right L # P) \<longleftrightarrow> E \<and> focus (L \<and> R) P" 102 unfolding focus_defs using conj_commute by simp 103 104private lemmas focus_right = focus_right_iff[where E=True, simplified, THEN iffD1] 105private lemmas unfocusE_right = focus_right_iff[THEN iffD2] 106private lemmas unfocus_right = unfocusE_right[where E=True, simplified] 107 108text \<open> 109Finally, we have rules for extracting the current focus. The sibling of the 110extracted focus becomes the new focus of the remaining structure. 111\<close> 112 113private lemma extract_focus_iff: "focus C (tag t S # P) \<longleftrightarrow> (C \<and> focus S P)" 114 unfolding focus_defs by (induct P arbitrary: S) auto 115 116private lemmas extract_focus = extract_focus_iff[THEN iffD2] 117 118subsection \<open>Primitive methods for navigating a conjunction\<close> 119 120text \<open> 121Using these rules as transitions, we implement a machine which navigates a tree 122of conjunctions, searching from left to right for a conjunct for which a given 123method will succeed. Once a matching conjunct is found, it is extracted, and the 124remaining conjuncts are reassembled. 125\<close> 126 127text \<open>From the current focus, move to the leftmost sub-conjunct.\<close> 128private method focus_leftmost = (intro focus_left)? 129 130text \<open>Find the furthest ancestor for which the current focus is still on the right.\<close> 131private method unfocus_rightmost = (intro unfocus_right)? 132 133text \<open>Move to the immediate-right sibling.\<close> 134private method focus_right_sibling = (rule unfocus_left, rule focus_right) 135 136text \<open>Move to the next conjunct in right-to-left ordering.\<close> 137private method focus_next_conjunct = (unfocus_rightmost, focus_right_sibling, focus_leftmost) 138 139text \<open>Search from current focus toward the right until we find a matching conjunct.\<close> 140private method find_match methods m = (rule extract_focus, m | focus_next_conjunct, find_match m) 141 142text \<open>Search within nest of conjuncts, leaving remaining structure focused.\<close> 143private method extract_match methods m = (rule to_focus, focus_leftmost, find_match m) 144 145text \<open>Move all the way out of focus, keeping track of any extracted conjunct.\<close> 146private method unfocusE = ((intro unfocusE_right unfocusE_left)?, rule from_focusE) 147private method unfocus = ((intro unfocus_right unfocus_left)?, rule from_focus) 148 149subsection \<open>Methods for selecting the leftmost matching conjunct\<close> 150 151text \<open> 152See the introduction at the top of this theory for motivation, and below for 153some simple examples. 154\<close> 155 156text \<open> 157Assuming the conclusion of the goal is a nest of conjunctions, method 158@{text lift_conjunct} finds the leftmost conjunct for which the given method 159succeeds, and moves it to the front of the conjunction in the goal. 160\<close> 161method lift_conjunct methods m = (extract_match \<open>succeeds \<open>rule conjI, m\<close>\<close>, unfocusE) 162 163text \<open> 164Method @{text extract_conjunct} finds the leftmost conjunct for which the 165given method succeeds, and splits it into a fresh subgoal, leaving the remaining 166conjuncts untouched in the second subgoal. It is equivalent to @{method lift_conjunct} 167followed by @{method rule} @{thm conjI}. 168\<close> 169method extract_conjunct methods m = (extract_match \<open>rule conjI, succeeds m\<close>; unfocus?) 170 171text \<open> 172Method @{text apply_conjunct} finds the leftmost conjunct for which the given 173method succeeds, leaving any subgoals created by the application of that method, 174and a subgoal containing the remaining conjuncts untouched. It is equivalent to 175@{method extract_conjunct} followed by the given method, but more efficient. 176\<close> 177method apply_conjunct methods m = (extract_match \<open>rule conjI, m\<close>; unfocus?) 178 179subsection \<open>Examples\<close> 180 181text \<open> 182Given an inner method based on @{method match}, which only succeeds on the desired 183conjunct @{term C}, @{method lift_conjunct} moves the conjunct @{term C} to the 184front. The body of the @{method match} here is irrelevant, since @{method lift_conjunct} 185always discards the effect of the method it is given. 186\<close> 187lemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" 188 apply (lift_conjunct \<open>match conclusion in C \<Rightarrow> \<open>-\<close>\<close>) 189 \<comment> \<open>@{term C} as been moved to the front of the conclusion.\<close> 190 apply (match conclusion in \<open>C \<and> A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) 191 oops 192 193text \<open> 194Method @{method extract_conjunct} works similarly, but peels of the matched conjunct 195as a separate subgoal. As for @{method lift_conjunct}, the effect of the given method 196is discarded, so the body of the @{method match} is irrelevant. 197\<close> 198lemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" 199 apply (extract_conjunct \<open>match conclusion in C \<Rightarrow> \<open>-\<close>\<close>) 200 \<comment> \<open>@{method extract_conjunct} gives us the matched conjunct @{term C} as a separate subgoal.\<close> 201 apply (match conclusion in C \<Rightarrow> \<open>-\<close>) 202 apply blast 203 \<comment> \<open>The other subgoal contains the remaining conjuncts untouched.\<close> 204 apply (match conclusion in \<open>A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) 205 oops 206 207text \<open> 208Method @{method apply_conjunct} goes one step further, and applies the given method 209to the extracted subgoal. 210\<close> 211lemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" 212 apply (apply_conjunct \<open>match conclusion in C \<Rightarrow> \<open>match premises in H: _ \<Rightarrow> \<open>rule H\<close>\<close>\<close>) 213 \<comment> \<open>We get four subgoals from applying the given method to the matched conjunct @{term C}.\<close> 214 apply (match premises in H: A \<Rightarrow> \<open>rule H\<close>) 215 apply (match premises in H: B \<Rightarrow> \<open>rule H\<close>) 216 apply (match premises in H: D \<Rightarrow> \<open>rule H\<close>) 217 apply (match premises in H: E \<Rightarrow> \<open>rule H\<close>) 218 \<comment> \<open>The last subgoal contains the remaining conjuncts untouched.\<close> 219 apply (match conclusion in \<open>A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) 220 oops 221 222end 223 224end 225