Re: [isabelle] Automating a Repetitive Structured Proof



On Sat, 2017-10-14 at 13:42 -0400, David E. Narvaez wrote:
> 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!

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


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