From b356f65969f1962def8e367f76a78f24cd5e3fe3 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Mon, 13 Jul 2020 11:59:43 +0800
Subject: [PATCH] lib: in_case and find_case methods

We already have find_goal, but the interface is a bit too unwieldy to
casually use frequently. This commit introduces (or moves from RISCV)
two methods on top of find_goal:

 - `in_case x`: asserts the goal has an assumption `?t = x`
 - `find_case x`: finds a goal such that `in_case x`

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
---
 lib/Eisbach_Methods.thy           | 19 ++++++++++++++++---
 proof/refine/RISCV64/Retype_R.thy |  4 ----
 2 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/lib/Eisbach_Methods.thy b/lib/Eisbach_Methods.thy
index 0f01a1e90..90d18649b 100644
--- a/lib/Eisbach_Methods.thy
+++ b/lib/Eisbach_Methods.thy
@@ -354,8 +354,6 @@ section \<open>Utility methods\<close>
 
 subsection \<open>Finding a goal based on successful application of a method\<close>
 
-context begin
-
 method_setup find_goal =
  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    let
@@ -367,7 +365,11 @@ method_setup find_goal =
 
    in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)\<close>
 
-end
+text \<open>Ensure that the proof state is in a certain case of a case distinction:\<close>
+method in_case for x = match premises in "t = x" for t \<Rightarrow> succeed
+
+text \<open>Focus on a case in a case distinction:\<close>
+method find_case for x = find_goal \<open>in_case x\<close>
 
 notepad begin
 
@@ -389,6 +391,17 @@ notepad begin
     apply (rule conjI)
     by (rule A B)+
 
+  fix x::'a and S :: "nat \<Rightarrow> 'a" and T R
+  have
+    "x = T \<Longrightarrow> A"
+    "x = S 10 \<Longrightarrow> B"
+    "x = R \<Longrightarrow> B"
+  apply -
+    apply (find_case "S ?n")
+    apply (fails \<open>in_case R\<close>)
+    apply (in_case "S ?n")
+    by (rule A B)+
+
 end
 
 
diff --git a/proof/refine/RISCV64/Retype_R.thy b/proof/refine/RISCV64/Retype_R.thy
index 46c6f802d..f727a7253 100644
--- a/proof/refine/RISCV64/Retype_R.thy
+++ b/proof/refine/RISCV64/Retype_R.thy
@@ -12,10 +12,6 @@ theory Retype_R
 imports VSpace_R
 begin
 
-(* FIXME RISCV: move way up somewhere *)
-text \<open>To ensure that the proof state is in a certain case of a case distinction:\<close>
-method in_case for x::'a = match premises in "t = x" for t \<Rightarrow> succeed
-
 context begin interpretation Arch . (*FIXME: arch_split*)
 
 definition