# [isabelle] Automating a Repetitive Structured Proof

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!
--
David E. Narvaez

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*