[isabelle] Nitpick Codatatype - No Counterexample found



Dear all,
I am trying to use nitpick to find counterexample over (potentially) infinite lists. While playing with nitpick I encountered a strange behavior:
    Nitpick seems to be unable to find counterexamples, if a message occurs twice in the list
 
An Example:
 
codatatype 'a::type llist = LNil | LCons 'a "'a llist"
 
(* Notice that "a" occurs twice *)
lemma "LCons (a::nat) (LCons a LNil) ≠ z"
  nitpick[expect=none]  (* Should find something! *)
  oops
 
 
(* Allowing different messages, now nitpick can find something *)
lemma "LCons (a::nat) (LCons b LNil) ≠ z"
  nitpick[expect=genuine]   (* is working *)
  oops
 
 
With the normal (finite) list datatype, this problem does not occur.
 
Does anybody know the cause & how to fix it?
 
Sincerely,
Sebastian Stüber
 
 
---------------------------------------------------------------
Sebastian Stüber, M.Sc.RWTH           |    Software Engineering
Lehrstuhl für Software Engineering    |  RWTH Aachen University
Ahornstr. 55, 52074 Aachen, Germany   |  https://www.se-rwth.de
Phone ++49 241 80-21352          
 
 
 

Attachment: nitpick_test.thy
Description: nitpick_test.thy



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