Re: [isabelle] Question on sequential pattern matching



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.
> 




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