# [isabelle] What is sumC?

`As a first example of explaining to my students what a subproof is,
``without complicating the matter by doing one with cases or with
``induction, I prepared the following (contrived) proof that 6 is the
``factorial of 3:
`lemma "fact(3::nat) = 6" proof-
have "(3::nat) = (2::nat)+1" by simp
then have "fact(3::nat) = fact((2::nat)+1)" by (rule arg_cong)
also have 1: "... = ((2::nat)+1)*fact(2) by (rule fact_plus_one_nat)
have "fact(2::nat) = 2" proof-
have "(2::nat) = 1+(1::nat)" by simp
then have "fact(2::nat)=fact(1+(1::nat))" by (rule arg_cong)
also have "... = (1+1)*fact(1)" by (rule fact_plus_one_nat)
finally show ?thesis by simp
qed
with 1 have "fact(3::nat) = ((2::nat)+1)*2" by simp
then show ?thesis by simp
qed

`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. 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? I searched for it in
``"Isabelle/HOL --- Higher-Order Logic" and in the Isabelle/Isar
``Reference Manual, and it wasn't in either place. -Douglas
`--
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875

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