# [isabelle] Problem with function definitions

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Problem with function definitions
*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
*Date*: Fri, 8 Apr 2016 17:08:45 +0000
*Accept-language*: de-DE, de-AT, en-US
*Thread-index*: AQHRkblPFpp67/sc50WmZuq6CXEotg==
*Thread-topic*: Problem with function definitions

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Ã

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*