[isabelle] Nitpick counterexample for true statement

Hi list,

nitpick is a great tool, as long as it does not refute provable lemmas,
as in the case below.

By the way, nunchaku chokes on this with an internal error.

Tested with Isabelle2018 and 9a7f94ab4df9, the result is the same.



theory Scratch
imports "Refine_Monadic.Refine_Monadic"

  definition [to_relAPP]: "lsr R ≡ ⟨R⟩list_rel O {(a,set a) | a. True}"
    assumes "(xs⇩1@xs⇩2,s)∈⟨R⟩lsr"
    shows "(∃s⇩1 s⇩2. s=s⇩1∪s⇩2 ∧ (xs⇩1,s⇩1)∈⟨R⟩lsr ∧
    nunchaku (* Error: broken invariant: variable v_ig_1/448 not bound
in scope (code 1) *)
    nitpick (* 
      Kodkod warning: Matrix too large: requested capacity of
      Nitpick found a counterexample for card 'a = 3 and card 'b = 2:

    (* Here is the proof of this lemma: *)    
    using assms[unfolded lsr_def]
  proof (clarsimp simp: )
    fix ys
    assume "(xs⇩1 @ xs⇩2, ys) ∈ ⟨R⟩list_rel"
    then obtain ys⇩1 ys⇩2 where [simp]: "ys=ys⇩1@ys⇩2" and "(xs⇩1,
ys⇩1) ∈ ⟨R⟩list_rel" "(xs⇩2, ys⇩2) ∈ ⟨R⟩list_rel" 
      using list_rel_append1 by blast
    have "(xs⇩1, set ys⇩1) ∈ ⟨R⟩lsr"
      unfolding lsr_def using ‹(xs⇩1, ys⇩1) ∈ ⟨R⟩list_rel› 
      by (auto simp: )
    moreover have "(xs⇩2, set ys⇩2) ∈ ⟨R⟩lsr"
      unfolding lsr_def using ‹(xs⇩2, ys⇩2) ∈ ⟨R⟩list_rel› 
      by (auto simp: )
    ultimately show "∃s⇩1 s⇩2. set ys = s⇩1 ∪ s⇩2 ∧ (xs⇩1, s⇩1) ∈
⟨R⟩lsr ∧ (xs⇩2, s⇩2) ∈ ⟨R⟩lsr"
      by auto

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