*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Question on sequential pattern matching*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 30 Dec 2013 12:29:05 +0100*In-reply-to*: <4A70972E-B8DA-432E-BE00-D2B38FA6210E@kestrel.edu>*References*: <4A70972E-B8DA-432E-BE00-D2B38FA6210E@kestrel.edu>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

This is the normal behaviour. Overlapping patterns need to be disambiguated. Minimizing the number of unambiguous patterns is complex (in the complexity theoretic sense) and not attempted by "fun". See Alexander Krauss. Pattern minimization problems over recursive data types. In James Hook and Peter Thiemann, editors, International Conference on Functional Programming (ICFP 2008). ACM, 2008. http://www21.in.tum.de/~krauss/ Tobias On 30/12/2013 00:49, Alessandro Coglio wrote: > In the following artificial example > > datatype T = A | B | C > > fun f :: "T ⇒ T ⇒ bool" > where > "f A A ⟷ True" | > "f B B ⟷ True" | > "f C C ⟷ True" | > "f _ _ ⟷ False" > > ‘fun’ gives a warning about duplicate rewrite rules > > Ignoring duplicate rewrite rule: > f C B ≡ False > Ignoring duplicate rewrite rule: > f B C ≡ False > Ignoring duplicate rewrite rule: > f C B ≡ False > Ignoring duplicate rewrite rule: > f B C ≡ False > > and ‘thm f.simps’ shows 9 distinct rules plus 2 duplicates > > f A A = True > f B B = True > f C C = True > f B A = False > f B C = False + > f C A = False > f C B = False ++ > f A B = False > f C B = False ++ > f A C = False > f B C = False + > > I suppose that the duplicate rules are harmless, but is this the expected/intended behavior? > > Rephrasing as > > fun f :: "T ⇒ T ⇒ bool" > where > "f A A ⟷ True" | > "f A _ ⟷ False" | > "f B B ⟷ True" | > "f B _ ⟷ False" | > "f C C ⟷ True" | > "f C _ ⟷ False" > > avoids the issue but is more verbose. > > I’m using Isabelle 2013-2. > > Thank you in advance. >

**References**:**[isabelle] Question on sequential pattern matching***From:*Alessandro Coglio

- Previous by Date: Re: [isabelle] Question on sequential pattern matching
- Next by Date: [isabelle] Privacy by Design: from Theory to Practice (Postdoc Position at Inria in Lyon)
- Previous by Thread: Re: [isabelle] Question on sequential pattern matching
- Next by Thread: [isabelle] Privacy by Design: from Theory to Practice (Postdoc Position at Inria in Lyon)
- Cl-isabelle-users December 2013 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