[isabelle] case _ of



Hello,

I have the following equivalent definitions

definition
 "SetMark ij = (case ij of
     (I.init, I.loop)  => inf (dem Q1_0) (dem Q2_0) |
     (I.loop, I.loop)  => inf (dem Q3_0) (dem Q4_0) |
     (I.loop, I.final) => dem Q5_0 |
      _ => top)";

definition
 "SetMark = top(
     (I.init, I.loop)  := inf (dem Q1_0) (dem Q2_0) ,
     (I.loop, I.loop)  := inf (dem Q3_0) (dem Q4_0) ,
     (I.loop, I.final) := dem Q5_0)
I like the style of the first one, however in proofs when I expand SetMark with the second definition everything is expanded and I get to basic cases which are discharged automatically, while using the first definition I have to do case_tac
on both first component and second component until I get the result proved.

Is there a way to split the case term in cases automatically, without using case_tac?

Best regards,

Viorel Preoteasa








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