Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error "Tactic failed" in function definition

Email Gateway (Sep 05 2023 at 20:00):

From: Alexandra Graß <alexandra.grass@tum.de>
Hello,

while trying to define a function, I encountered an error Tactic failed when introducing a let-binding using inf and sup operators. This problem was already discussed on Zulip [1] as well.

Thanks to the help of Mathias Fleury, I managed to construct a minimal example highlighting the problem:

function (sequential) foo :: "nat set ⇒ nat set" where
  "foo old = (
      let new = old ∩ old in
      if new = old then
          foo new
      else
        foo new)"
  by pat_completeness auto

does show the Tactic failed error, but

function (sequential) foo :: "nat set ⇒ nat set" where
  "foo old = (
      let new = old ∩ old in
      if new = old then
          foo old ∩ old
      else
        foo new)"
  by pat_completeness auto

does not. Replacing new (i.e. copy-pasting the rhs of the let binding) in any of the other lines does not fix the problem. Other trivial operations such as old ∪ {} do the job (i.e. invoking the error) as well.

Is this a known issue? Copy-pasting definitions is not really an option for the algorithm I'm trying to formalize, as it would seriously clutter the code & obfuscate the algorithm's mechanism.

Any suggestions are highly appreciated.

Thanks in advance,
Alex

[1] https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Mutual.20.26.20partial.20recursion.20.E2.80.93.20Tactic.20failed<https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Mutual.20.26.20partial.20recursion.20.E2.80.93.20Tactic.20failed>

Last updated: Jan 04 2025 at 20:18 UTC