[isabelle] Regression with finite_Collect


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"

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.