*To*: Isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Question on sequential pattern matching*From*: Alessandro Coglio <coglio at kestrel.edu>*Date*: Mon, 30 Dec 2013 00:49:37 +0100

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.

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Question on sequential pattern matching***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Question on sequential pattern matching***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: Re: [isabelle] Question on sequential pattern matching
- Previous by Thread: Re: [isabelle] A problem on ML-like function programming
- Next by Thread: Re: [isabelle] Question on sequential pattern matching
- 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