[isabelle] 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.