Email Gateway (Aug 22 2022 at 13:06): Email Gateway (Aug 22 2022 at 13:06):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
I currently have a problem defining certain functions where the internal tactics in the
function package fail.
E.g., a quite minimalistic example is
fun foo where
"foo (Suc n) = (let f = n in
if f mod 3 = f then foo n else 0)"
| "foo 0 = Suc 0"
where Isabelle 2016 complains.
Adapting it via „False or"
fun foo where
"foo (Suc n) = (let f = n in
if False ∨ f mod 3 = f then foo n else 0)"
| "foo 0 = Suc 0"
is accepted, but interestingly, „True and“ is again not accepted.
fun foo where
"foo (Suc n) = (let f = n in
if True ∧ f mod 3 = f then foo n else 0)"
| "foo 0 = Suc 0"
Output:
consts
foo :: "nat ⇒ 'a"
Tactic failed
The error(s) above occurred for the goal statement⌂:
(⋀n x. x = n ⟹ True ∧ x mod 3 = x ⟹ P n (Suc n)) ⟹ foo_rel ≤ P
Found termination order: "size <mlex> {}"
Cheers,
René
Last updated: Apr 19 2024 at 08:19 UTC