*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] case _ of*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Fri, 12 Mar 2010 12:03:12 +0200*In-reply-to*: <4B98E4D5.40100@abo.fi>*References*: <cc2478ab1003061009r64142752u7d2d64a7d128953c@mail.gmail.com> <83424616-031E-4D84-AC94-E2A74D416BC2@cam.ac.uk> <4B92EB83.2040704@abo.fi> <cc2478ab1003070725t4953c6a4x463eaa94faeec212@mail.gmail.com> <4B94073E.1030603@abo.fi> <4B95F1E6.2010702@informatik.tu-muenchen.de> <4B98E4D5.40100@abo.fi>*User-agent*: Thunderbird 2.0.0.23 (Windows/20090812)

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)

on both first component and second component until I get the result proved.

Best regards, Viorel Preoteasa

**Follow-Ups**:**Re: [isabelle] case _ of***From:*Tobias Nipkow

**References**:**[isabelle] argument order of List.foldr***From:*Brian Huffman

**Re: [isabelle] argument order of List.foldr***From:*Lawrence Paulson

**[isabelle] Question about classes***From:*Viorel Preoteasa

**Re: [isabelle] Question about classes***From:*Brian Huffman

**Re: [isabelle] Question about classes***From:*Viorel Preoteasa

**Re: [isabelle] Question about classes***From:*Florian Haftmann

**Re: [isabelle] Question about classes***From:*Viorel Preoteasa

- Previous by Date: [isabelle] CFP: SSV'10 @ USENIX OSDI 2010
- Next by Date: Re: [isabelle] Symmetric Difference of sets
- Previous by Thread: Re: [isabelle] Question about classes
- Next by Thread: Re: [isabelle] case _ of
- Cl-isabelle-users March 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list