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