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.