# [isabelle] Regression with finite_Collect

• To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
• Subject: [isabelle] Regression with finite_Collect
• From: René Neumann <rene.neumann at in.tum.de>
• Date: Thu, 08 Aug 2013 13:18:34 +0200
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130705 Thunderbird/17.0.7

```Hi,

I have encountered something that workes with Isabelle2012 but yields a
"Tactic failed" with Isabelle2013:

lemma LTS_product_finite:
fixes LTS_product :: "('q×'a×'q) set ⇒ ('p×'a×'p) set ⇒
(('q*'p)×'a×('q*'p)) set"
assumes "finite Δ1" and "finite Δ2"
shows "finite (LTS_product Δ1 Δ2)"
proof -
(* note [[simproc del: finite_Collect]] *)
let ?prod = "{((p,a,p'),q,b,q'). (p,a,p') ∈ Δ1 ∧ (q,b,q') ∈ Δ2 ∧ a = b}"
let ?f = "λ((p,a,p'),q,a,q'). ((p,q),a,(p',q'))"

have "?prod ⊆ Δ1 × Δ2" by auto
with assms have "finite ?prod" by (blast intro: finite_subset)
moreover have "LTS_product Δ1 Δ2 = ?f ` ?prod" sorry
ultimately show ?thesis by simp -- "fails when simproc is not deleted"
qed

The error message is (at the final simp):

*** Tactic failed
*** The error(s) above occurred for the goal statement:
*** {((p, a, p'), ab).
***  (p, a, p') ∈ Δ1 ∧ (case ab of (q, b, q') ⇒ (q, b, q') ∈ Δ2 ∧ a = b)} =
*** {((p, a, p'), ab) |p a p' ab.
***  (p, a, p') ∈ Δ1 ∧ (case ab of (q, b, q') ⇒ (q, b, q') ∈ Δ2 ∧ a = b)}

As already lined out in the lemma above, the proof goes through when I
disable the simproc finite_Collect.

(FWIW: Also fails with isabelle-dev rev. 6c89225ddeba )

- René
--
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

```

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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