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.

For reference :

```
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
```

any help is apreciated, thank you

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.

Thank you so much, it did the trick!

Lekhani Ray has marked this topic as resolved.

Last updated: Feb 27 2024 at 08:17 UTC