Email Gateway (Aug 19 2022 at 11:36): Email Gateway (Aug 19 2022 at 11:36):From: René Neumann <rene.neumann@in.tum.de>
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 )
Last updated: Nov 21 2024 at 12:39 UTC