Re: [isabelle] Question on sequential pattern matching



Le Mon, 30 Dec 2013 00:49:37 +0100, Alessandro Coglio <coglio at kestrel.edu> a écrit:

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

I'm also noticing something else strange aside: with the last two cases, the output pan says “f” is a free variable while it says it's fixed with the first two cases.

[…]

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 don't know how close is the artificial case to the real case, still what about this one:

    fun f :: "T ⇒ T ⇒ bool"
      where "f x y ⟷ x = y"

Then…

    thm f.simps

…just says:

    f ?x ?y = (?x = ?y)

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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