Email Gateway (Aug 22 2022 at 15:13): Email Gateway (Aug 22 2022 at 15:13):From: "C.A. Watt" <caw77@cam.ac.uk>
Hi all
I've been attempting to define a particular inductive predicate in
Isabelle, only to discover that particular orderings of preconditions in
the inductive rules cause a "Tactic failed" error to be output.
Here is a reduced example. Removing any of the applications of id or
moving the last precondition to any other position will cause the error
to disappear. What's going on?
theory Fails imports Main begin
inductive reduced :: "bool" where
"⟦id vs = (n::nat); id t1s = n; t2s = m; id x = [t1s, t2s]⟧ ⟹ reduced"
end
Output:
Proofs for inductive predicate(s) "reduced"
<...>
Proving the simplification rules ...
Tactic failed
The error(s) above occurred for the goal statement⌂:
(⋀vs n t1s t2s m x. id vs = n ⟹ id t1s = n ⟹ t2s = m ⟹ id x = [t1s, t2s]
⟹ P) ⟹ reduced ≤ P
Best wishes
Conrad Watt
Fails.thy
Last updated: Apr 23 2024 at 20:15 UTC