Re: [isabelle] case _ of



You can instruct simp/auto/fastsimp/force to split all case expressions
of some type t by adding the option "split: t.split". See the 3.1.9 in
the Tutorial.

Tobias

Viorel Preoteasa schrieb:
> 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.