[isabelle] Question on sequential pattern matching



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
Description: S/MIME cryptographic signature



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