[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.