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>
This commit is contained in:
parent
c3f3656942
commit
b356f65969
|
@ -354,8 +354,6 @@ section \<open>Utility methods\<close>
|
||||||
|
|
||||||
subsection \<open>Finding a goal based on successful application of a method\<close>
|
subsection \<open>Finding a goal based on successful application of a method\<close>
|
||||||
|
|
||||||
context begin
|
|
||||||
|
|
||||||
method_setup find_goal =
|
method_setup find_goal =
|
||||||
\<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
|
\<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
|
||||||
let
|
let
|
||||||
|
@ -367,7 +365,11 @@ method_setup find_goal =
|
||||||
|
|
||||||
in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)\<close>
|
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
|
notepad begin
|
||||||
|
|
||||||
|
@ -389,6 +391,17 @@ notepad begin
|
||||||
apply (rule conjI)
|
apply (rule conjI)
|
||||||
by (rule A B)+
|
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
|
end
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -12,10 +12,6 @@ theory Retype_R
|
||||||
imports VSpace_R
|
imports VSpace_R
|
||||||
begin
|
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*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
|
Loading…
Reference in New Issue