Stream: Beginner Questions

Topic: ✔ Proving a lemma by strong induction

view this post on Zulip Lekhani Ray (Jul 26 2022 at 19:24):

Javier Diaz said:

I think the easiest way to prove your lemma is not by induction on the combined length of the arguments of addBinNum but by computation induction as follows:

lemma (in th2) addMeaningF_4: "evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y)"
  using assoc and commute by (induction rule: addBinNum.induct, auto) (metis arith_1)+

Please note that it's necessary to add both associativity and commutativity lemmas to your definition of plus in th2 as follows (proofs are left as exercises):

lemma (in th2) commute: "plus x y = plus y x"
  sorry

lemma (in th2) assoc: "plus (plus x y) z = plus x (plus y z)"
  sorry

Thank you Javier, super helpful!

view this post on Zulip Notification Bot (Jul 26 2022 at 19:41):

Lekhani Ray has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC