Email Gateway (Aug 22 2022 at 16:16): Email Gateway (Aug 22 2022 at 16:16):From: "David E. Narvaez" <den9562@rit.edu>
Hi,
I have a structured proof that right now looks roughly like this:
[...]
case And_bool_expr
then show ?thesis
using assms
proof (cases "partial_val_bool_expr e2 a", simp_all add: models_def)
case (Const_bool_expr b)
then show ?thesis using assms And_bool_expr by (cases b, simp_all add:
models_def)
qed
next
case Or_bool_expr
then show ?thesis
using assms
proof (cases "partial_val_bool_expr e2 a", simp_all add: models_def)
case (Const_bool_expr b)
then show ?thesis using assms Or_bool_expr by (cases b, simp_all add:
models_def)
qed
next
[...]
and it goes on for about 6 cases. Instead of repeating these instructions, I
want Isabelle to try the following for every case:
case $casename
then show ?thesis
using assms
proof (cases "partial_val_bool_expr e2 a", simp_all add: models_def)
case (Const_bool_expr b)
then show ?thesis using assms $casename by (cases b, simp_all add:
models_def)
qed
and discharge those that work using this strategy so that I'm left with those
that really need work.
From what I understand, this is the kind of things Eisbach is supposed to be
for, but Eisbach does not seem to be meant for structured proofs, am I
correct? If that is the case, then what tool could help me here? I have read
about automation using ML but I cannot find much documentation about that, with
examples of things that can automated using ML.
Thanks!
Email Gateway (Aug 22 2022 at 16:17):From: Matthew.Brecknell@data61.csiro.au
Hi David,
It ought to be possible to make an Eisbach method to solve the boring cases,
while keeping the structure of the overall proof. In that case, the overall
proof might look something like this:
proof (induct ...)
case (Interesting_bool_expr arg1 arg2)
show ?case proof ... qed
next
case (AnotherInteresting_bool_expr arg1 arg2 arg3)
show ?case proof ... qed
qed solve_boring_case+
Note the "solve_boring_case+" after the "qed" to handle any cases not yet
proved in the "proof" block.
The tricky part of making the Eisbach method will be obtaining bindings for
the variables "e2", "a" and "b". For that, you might be able to use the
"match" method, also part of Eisbach. Perhaps something like this:
method solve_boring_case =
(match goal in ‹... e2 ... a ...› for e2 a
⇒ ‹cases "partial_val_bool_expr e2 a"; simp add: models_def;
match goal in ‹... b ...› for b
⇒ ‹cases b; simp add: models_def››)
You'll need to figure out what term patterns will allow you to correctly
identify the right "e2", "a" and "b". You might need "match premises"
instead of "match goal", and you might need to bind fact names to matched
premises to wire them into proof fragments ("inner methods" in Eisbach-match
terminology).
Regards,
Matthew
Last updated: Apr 26 2024 at 01:06 UTC