# Re: [isabelle] What is sumC?

Hello,
> This works, but it's ugly. I would much rather have a proof that somehow
> proceeds automatically from fact(3) = 6 to fact(Suc 2) = 6 to (Suc
> 2)*fact(2) = 6 to (Suc 2)*fact(Suc 1) = 6 to (Suc 2)*(Suc 1)*fact(1) = 6
> to (Suc 2)*(Suc 1)*fact(Suc 0) = 6 to (Suc 2)*(Suc 1)*(Suc 0)*fact(0) =
> 6 to 3*2*1*1 = 6, all in one step.
I'm not sure I fully understand the requirement. Are you looking for a
proof method which can solve the full goal automatically? If so, you can
try 'code_simp' or 'eval'.
Perhaps a better way to understand what's going on internally is to
first convert the numeral notation to 'Suc ... 0' notation of natural
numbers:
lemma "fact 3 = 6"
unfolding eval_nat_numeral BitM.simps
At this point, the subgoal looks like this:
fact (Suc (Suc (Suc 0))) = Suc (Suc (Suc (Suc (Suc (Suc 0)))))
This goal can be solved 'by simp'. Of course, you can also add that rule
to the simpset:
lemma "fact 3 = 6"
by (simp add: eval_nat_numeral)
Does that help?
> As a first try, after a few
> iterations, I wrote:
> theory FactDef imports Main Fact begin
> lemma "fact(3::nat) = 6" by (auto simp add: fact_nat_def)
> end
> which didn't work (I didn't necessarily expect it to), but the message I
> got was:
> Failed to finish proof: goal (1 subgoal): 1. fact_nat_sumC 3 = 6
> So my question now is: What is this sumC?
It's an internal definition of the function command. See here for an
older discussion:
<http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/10667>.
Cheers
Lars

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