✔ Proof by induction · Beginner Questions

Hello,
I am trying to prove a (seemingly simple) lemma, However, I think I may be missing something

lemma len_check [simp]: "n = len (addBinNum x y) ⟹ n ≤ len x + len y"
proof(induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case sorry (*this is where I get stuck*)
qed

The subgoal says : ⋀n. (n = len (addBinNum x y) ⟹ n ≤ len x + len y) ⟹
Suc n = len (addBinNum x y) ⟹ Suc n ≤ len x + len y

My question : Do I need to induct on n further. Simple methods do not work. If I create another lemma "Suc n = len (addBinNum x y) ⟹ Suc n ≤ len x + len y" it possibly needs to refer to the 1st one. I am extremely confused as to how to proceed. Any help is appreciated.

fun len :: "BinNum ⇒ nat"
  where
    "len Zero = 1"|
    "len One = 1"|
    "len (JoinZero x) = len x + 1"|
    "len (JoinOne x) = len x + 1"

function (domintros) addBinNum :: "BinNum ⇒ BinNum ⇒ BinNum"
where
  "addBinNum Zero Zero = Zero"|
  "addBinNum Zero One = One"|
  "addBinNum One Zero = One"|
  "addBinNum One One = JoinOne Zero"|
  "addBinNum Zero (JoinZero x) = JoinZero x"|
  "addBinNum One (JoinZero x) = JoinOne x"|
  "addBinNum One (JoinOne x) = JoinZero (addBinNum One x)"|
  "addBinNum Zero (JoinOne x) = JoinOne x"|
  "addBinNum (JoinZero x) Zero = JoinZero x"|
  "addBinNum (JoinZero x) One = JoinOne x"|
  "addBinNum (JoinOne x) Zero = JoinOne x"|
  "addBinNum (JoinOne x) One = JoinZero (addBinNum One x)"|
  "addBinNum (JoinZero x) (JoinZero y) = JoinZero(addBinNum x y)"|
  "addBinNum (JoinZero x) (JoinOne y) = JoinOne(addBinNum x y)"|
  "addBinNum (JoinOne x) (JoinZero y) = JoinOne(addBinNum x y)"|
  "addBinNum (JoinOne x) (JoinOne y) = JoinZero(addBinNum(addBinNum x y) One)"
  by pat_completeness auto

Maximilian Schaeffeler (Jul 15 2022 at 18:46):

First, I would simplify the definition of addBinNum:
Swap the arguments in the recursive call in this line: addBinNum (JoinOne x) One = JoinZero (addBinNum One x).
Then you can get rid of function (domintros) and replace it with fun.

Finally for the lemma, get rid of the n, and replace it with addBinNum x y in the conclusion.
Then use computation induction: induction x y rule: addBinNum.induct to prove your goal.

Stream: Beginner Questions

Topic: ✔ Proof by induction

Lekhani Ray (Jul 15 2022 at 16:56):

Maximilian Schaeffeler (Jul 15 2022 at 18:46):

Lekhani Ray (Jul 15 2022 at 20:46):

Notification Bot (Jul 18 2022 at 17:11):