I know that questions like these seem to be looked down upon, but I haven't been able to find answers on the internet. I have the following function:
fun count :: "'a ⇒ 'a list ⇒ nat" where
"count a [] = 0"
| "count a (b # xs) = (count a xs) + (if a = b then 1 else 0)"
It counts the number of elements in a list that match with the given item. Simple enough, however, when I do the following:
value "count x [x,x,y,x,y]"
I get this as the output
"(if x = y then 1 else 0) + 1 + (if x = y then 1 else 0) + 1 + 1" :: "nat"
So you can see that there are hanging "if" statements and unevaluated additions in the output. Is it possible to make Isabelle simplify this?
I don't think so. The value command is more of a purely diagnostic tool and it is mostly meant for evaluation of ground terms (i.e. no free variables). The reason why you get a result at all is that it falls back from its standard method (compiling to ML, running the ML code, and converting the result back to HOL terms) to NBE (normalisation by evaluation, which is much slower and, at least in my experience, not that useful most of the time).
One trick that I do sometimes is to set up a lemma
lemma "count x [x, x, y, x, y] = myresult"
where the myresult on the right-hand side is just a dummy variable. Then I do
apply simp
and look at the resulting proof state (in case you don't see anything: try switching on "Editor Output State" in the options):
proof (prove)
goal (1 subgoal):
1. (x = y ⟶ Suc (Suc (Suc (Suc (Suc 0)))) = myresult) ∧
(x ≠ y ⟶ Suc (Suc (Suc 0)) = myresult)
It's a bit messy, but you can read of the result fairly well: if x = y, then the result is 5, otherwise it's 3. A simple hack to get rid of the Suc in the output is to cast to int, i.e. lemma "int (count x [x, x, y, x, y]) = myresult". Then you get:
(x = y ⟶ myresult = 5) ∧ (x ≠ y ⟶ myresult = 3)