## Stream: Beginner Questions

### Topic: How do I approach this proof?

#### Lekhani Ray (Jul 18 2022 at 15:08):

I have the following lemma

``````lemma (in th2) addMeaningF: "evalBinNum (addBinNum x y) = plus (evalBinNum x) (evalBinNum y)"
proof(induct)
``````

It gives me the following subgoals

evalBinNum (addBinNum x Zero) = plus (evalBinNum x) (evalBinNum Zero)

1. evalBinNum (addBinNum x One) = plus (evalBinNum x) (evalBinNum One)
2. ⋀xa. evalBinNum (addBinNum x xa) =
plus (evalBinNum x) (evalBinNum xa) ⟹
evalBinNum (addBinNum x (JoinZero xa)) =
plus (evalBinNum x) (evalBinNum (JoinZero xa))

3. ⋀xa. evalBinNum (addBinNum x xa) =
plus (evalBinNum x) (evalBinNum xa) ⟹
evalBinNum (addBinNum x (JoinOne xa)) =
plus (evalBinNum x) (evalBinNum (JoinOne xa))

When I induct inside one of the cases, it gives me the same four subgoals again.

Also, I was wondering if Isabelle allows the use of assumptions [evalBinNum is an assumption inside a locale, as is plus] since I hadn't seen much about it. addBinNum is a 'fun', I was wondering if evalBinNum and plus should be functions as well to make the lemma work?

For more reference

``````locale th2 = th1 +
fixes
plus :: "'a ⇒ 'a ⇒ 'a"
and evalBinNum :: "BinNum ⇒ 'a"
assumes
arith_1: "plus n zero = n"
and plus_suc: "plus n (suc m) = suc ( plus n m)"
and "evalBinNum Zero = zero"
and "evalBinNum One = suc(zero)"
and "evalBinNum (JoinZero x) = plus (evalBinNum x) (evalBinNum x)"
and "evalBinNum (JoinOne x) = plus (plus (evalBinNum x) (evalBinNum x)) (suc zero)"

fun addBinNum :: "BinNum ⇒ BinNum ⇒ BinNum"
where