160786Sps(* 260786Sps * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 360786Sps * 460786Sps * SPDX-License-Identifier: BSD-2-Clause 560786Sps *) 660786Sps 760786Spstheory Extract_Conjunct 860786Spsimports 960786Sps "Main" 1060786Sps "Eisbach_Methods" 1160786Spsbegin 1260786Sps 1360786Spssection \<open>Extracting conjuncts in the conclusion\<close> 1460786Sps 1560786Spstext \<open> 1660786SpsMethods for extracting a conjunct from a nest of conjuncts in the conclusion 1760786Spsof a goal, typically by pattern matching. 1860786Sps 1960786SpsWhen faced with a conclusion which is a big conjunction, it is often the case 2060786Spsthat a small number of conjuncts require special attention, while the rest can 2160786Spsbe solved easily by @{method clarsimp}, @{method auto} or similar. However, 2260786Spssometimes the method that would solve the bulk of the conjuncts would put some 2360786Spsof the conjuncts into a more difficult or unsolvable state. 2460786Sps 2560786SpsThe higher-order methods defined here provide an efficient way to select a 2660786Spsconjunct requiring special treatment, so that it can be dealt with first. Once 2760786Spsall such conjuncts have been removed, the remaining conjuncts can all be solved 2860786Spstogether by some automated method. 2960786Sps 3060786SpsEach method takes an inner method as an argument, and selects the leftmost 3160786Spsconjunct for which that inner method succeeds. The methods differ according to 3260786Spswhat they do with the selected conjunct. See below for more information and 3360786Spssome simple examples. 3460786Sps\<close> 3560786Sps 3660786Spscontext begin 3760786Sps 3860786Spssubsection \<open>Focused conjunct with context\<close> 3960786Sps 4060786Spstext \<open> 4160786SpsWe define a predicate which allows us to identify a particular sub-tree and its 4260786Spscontext within a nest of conjunctions. We express this sub-tree-with-context using 4360786Spsa function which reconstructs the original nest of conjunctions. The context 4460786Spsconsists of a list of parent contexts, where each parent context consists of a 4560786Spssibling sub-tree, and a tag indicating whether the focused sub-tree is on the left 4660786Spsor right. Rebuilding the original tree works from the focused sub-tree up towards 4760786Spsthe root of the original structure. This sub-tree-with-context is sometimes known 4860786Spsas a zipper. 4960786Sps\<close> 5060786Sps 5160786Spsprivate fun focus_conj :: "bool \<Rightarrow> bool list \<Rightarrow> bool" where 5260786Sps "focus_conj current [] = current" 5360786Sps| "focus_conj current (sibling # parents) = focus_conj (current \<and> sibling) parents" 5460786Sps 5560786Spsprivate definition "focus \<equiv> focus_conj" 5660786Sps 5760786Spsprivate definition "tag t P \<equiv> P" 5860786Spsprivate lemmas focus_defs = focus_def tag_def 5960786Sps 6060786Spsprivate abbreviation "left \<equiv> tag Left" 6160786Spsprivate abbreviation "right \<equiv> tag Right" 6260786Sps 6360786Spsprivate lemma focus_example: 6460786Sps "focus C [right B, left D, left E, right A] \<longleftrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" 6560786Sps unfolding focus_defs by auto 6660786Sps 6760786Spssubsection \<open>Moving the focus\<close> 6860786Sps 6960786Spstext \<open> 7060786SpsWe now prove some rules which allow us to switch between focused and unfocused 7160786Spsstructures, and to move the focus around. Some versions of these rules carry an 7260786Spsextra conjunct @{term E} outside the structure. Once we find the conjunct we want, 7360786Spsthis @{term E} allows to keep track of it while we reassemble the rest of the 7460786Spsoriginal structure. 7560786Sps 7660786SpsFirst, we have rules for going between focused and unfocused structures. 7760786Sps\<close> 7860786Sps 7960786Spsprivate lemma focus_top_iff: "E \<and> focus P [] \<longleftrightarrow> E \<and> P" 8060786Sps unfolding focus_def by simp 8160786Sps 8260786Spsprivate lemmas to_focus = focus_top_iff[where E=True, simplified, THEN iffD1] 8360786Spsprivate lemmas from_focusE = focus_top_iff[THEN iffD2] 8460786Spsprivate lemmas from_focus = from_focusE[where E=True, simplified] 8560786Sps 8660786Spstext \<open> 8760786SpsNext, we have rules for moving the focus to and from the left conjunct. 8860786Sps\<close> 8960786Sps 9060786Spsprivate lemma focus_left_iff: "E \<and> focus L (left R # P) \<longleftrightarrow> E \<and> focus (L \<and> R) P" 9160786Sps unfolding focus_defs by simp 9260786Sps 9360786Spsprivate lemmas focus_left = focus_left_iff[where E=True, simplified, THEN iffD1] 9460786Spsprivate lemmas unfocusE_left = focus_left_iff[THEN iffD2] 9560786Spsprivate lemmas unfocus_left = unfocusE_left[where E=True, simplified] 9660786Sps 9760786Spstext \<open> 9860786SpsNext, we have rules for moving the focus to and from the right conjunct. 9960786Sps\<close> 10060786Sps 10160786Spsprivate lemma focus_right_iff: "E \<and> focus R (right L # P) \<longleftrightarrow> E \<and> focus (L \<and> R) P" 10260786Sps unfolding focus_defs using conj_commute by simp 10360786Sps 10460786Spsprivate lemmas focus_right = focus_right_iff[where E=True, simplified, THEN iffD1] 10560786Spsprivate lemmas unfocusE_right = focus_right_iff[THEN iffD2] 10660786Spsprivate lemmas unfocus_right = unfocusE_right[where E=True, simplified] 10760786Sps 10860786Spstext \<open> 10960786SpsFinally, we have rules for extracting the current focus. The sibling of the 11060786Spsextracted focus becomes the new focus of the remaining structure. 11160786Sps\<close> 11260786Sps 11360786Spsprivate lemma extract_focus_iff: "focus C (tag t S # P) \<longleftrightarrow> (C \<and> focus S P)" 11460786Sps unfolding focus_defs by (induct P arbitrary: S) auto 11560786Sps 11660786Spsprivate lemmas extract_focus = extract_focus_iff[THEN iffD2] 11760786Sps 11860786Spssubsection \<open>Primitive methods for navigating a conjunction\<close> 11960786Sps 12060786Spstext \<open> 12160786SpsUsing these rules as transitions, we implement a machine which navigates a tree 12260786Spsof conjunctions, searching from left to right for a conjunct for which a given 12360786Spsmethod will succeed. Once a matching conjunct is found, it is extracted, and the 12460786Spsremaining conjuncts are reassembled. 12560786Sps\<close> 12660786Sps 12760786Spstext \<open>From the current focus, move to the leftmost sub-conjunct.\<close> 12860786Spsprivate method focus_leftmost = (intro focus_left)? 12960786Sps 13060786Spstext \<open>Find the furthest ancestor for which the current focus is still on the right.\<close> 13160786Spsprivate method unfocus_rightmost = (intro unfocus_right)? 13260786Sps 13360786Spstext \<open>Move to the immediate-right sibling.\<close> 13460786Spsprivate method focus_right_sibling = (rule unfocus_left, rule focus_right) 13560786Sps 13660786Spstext \<open>Move to the next conjunct in right-to-left ordering.\<close> 13760786Spsprivate method focus_next_conjunct = (unfocus_rightmost, focus_right_sibling, focus_leftmost) 13860786Sps 13960786Spstext \<open>Search from current focus toward the right until we find a matching conjunct.\<close> 14060786Spsprivate method find_match methods m = (rule extract_focus, m | focus_next_conjunct, find_match m) 14160786Sps 14260786Spstext \<open>Search within nest of conjuncts, leaving remaining structure focused.\<close> 14360786Spsprivate method extract_match methods m = (rule to_focus, focus_leftmost, find_match m) 14460786Sps 14560786Spstext \<open>Move all the way out of focus, keeping track of any extracted conjunct.\<close> 14660786Spsprivate method unfocusE = ((intro unfocusE_right unfocusE_left)?, rule from_focusE) 14760786Spsprivate method unfocus = ((intro unfocus_right unfocus_left)?, rule from_focus) 14860786Sps 14960786Spssubsection \<open>Methods for selecting the leftmost matching conjunct\<close> 15060786Sps 15160786Spstext \<open> 15260786SpsSee the introduction at the top of this theory for motivation, and below for 15360786Spssome simple examples. 15460786Sps\<close> 15560786Sps 15660786Spstext \<open> 15760786SpsAssuming the conclusion of the goal is a nest of conjunctions, method 15860786Sps@{text lift_conjunct} finds the leftmost conjunct for which the given method 15960786Spssucceeds, and moves it to the front of the conjunction in the goal. 16060786Sps\<close> 16160786Spsmethod lift_conjunct methods m = (extract_match \<open>succeeds \<open>rule conjI, m\<close>\<close>, unfocusE) 16260786Sps 16360786Spstext \<open> 16460786SpsMethod @{text extract_conjunct} finds the leftmost conjunct for which the 16560786Spsgiven method succeeds, and splits it into a fresh subgoal, leaving the remaining 16660786Spsconjuncts untouched in the second subgoal. It is equivalent to @{method lift_conjunct} 16760786Spsfollowed by @{method rule} @{thm conjI}. 16860786Sps\<close> 16960786Spsmethod extract_conjunct methods m = (extract_match \<open>rule conjI, succeeds m\<close>; unfocus?) 17060786Sps 17160786Spstext \<open> 17260786SpsMethod @{text apply_conjunct} finds the leftmost conjunct for which the given 17360786Spsmethod succeeds, leaving any subgoals created by the application of that method, 17460786Spsand a subgoal containing the remaining conjuncts untouched. It is equivalent to 17560786Sps@{method extract_conjunct} followed by the given method, but more efficient. 17660786Sps\<close> 17760786Spsmethod apply_conjunct methods m = (extract_match \<open>rule conjI, m\<close>; unfocus?) 17860786Sps 17960786Spssubsection \<open>Examples\<close> 18060786Sps 18160786Spstext \<open> 18260786SpsGiven an inner method based on @{method match}, which only succeeds on the desired 18360786Spsconjunct @{term C}, @{method lift_conjunct} moves the conjunct @{term C} to the 18460786Spsfront. The body of the @{method match} here is irrelevant, since @{method lift_conjunct} 18560786Spsalways discards the effect of the method it is given. 18660786Sps\<close> 18760786Spslemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" 18860786Sps apply (lift_conjunct \<open>match conclusion in C \<Rightarrow> \<open>-\<close>\<close>) 18960786Sps \<comment> \<open>@{term C} as been moved to the front of the conclusion.\<close> 19060786Sps apply (match conclusion in \<open>C \<and> A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) 19160786Sps oops 19260786Sps 19360786Spstext \<open> 19460786SpsMethod @{method extract_conjunct} works similarly, but peels of the matched conjunct 19560786Spsas a separate subgoal. As for @{method lift_conjunct}, the effect of the given method 19660786Spsis discarded, so the body of the @{method match} is irrelevant. 19760786Sps\<close> 19860786Spslemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" 19960786Sps apply (extract_conjunct \<open>match conclusion in C \<Rightarrow> \<open>-\<close>\<close>) 20060786Sps \<comment> \<open>@{method extract_conjunct} gives us the matched conjunct @{term C} as a separate subgoal.\<close> 20160786Sps apply (match conclusion in C \<Rightarrow> \<open>-\<close>) 20260786Sps apply blast 20360786Sps \<comment> \<open>The other subgoal contains the remaining conjuncts untouched.\<close> 20460786Sps apply (match conclusion in \<open>A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) 20560786Sps oops 20660786Sps 20760786Spstext \<open> 20860786SpsMethod @{method apply_conjunct} goes one step further, and applies the given method 20960786Spsto the extracted subgoal. 21060786Sps\<close> 21160786Spslemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" 21260786Sps apply (apply_conjunct \<open>match conclusion in C \<Rightarrow> \<open>match premises in H: _ \<Rightarrow> \<open>rule H\<close>\<close>\<close>) 21360786Sps \<comment> \<open>We get four subgoals from applying the given method to the matched conjunct @{term C}.\<close> 21460786Sps apply (match premises in H: A \<Rightarrow> \<open>rule H\<close>) 21560786Sps apply (match premises in H: B \<Rightarrow> \<open>rule H\<close>) 21660786Sps apply (match premises in H: D \<Rightarrow> \<open>rule H\<close>) 21760786Sps apply (match premises in H: E \<Rightarrow> \<open>rule H\<close>) 21860786Sps \<comment> \<open>The last subgoal contains the remaining conjuncts untouched.\<close> 21960786Sps apply (match conclusion in \<open>A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) 22060786Sps oops 22160786Sps 22260786Spsend 22360786Sps 22460786Spsend 22560786Sps