How do I approach this proof? · Beginner Questions

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

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?

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
  "addBinNum Zero x = x"|
  "addBinNum x Zero = x"|
  "addBinNum One One = JoinZero One"|
  "addBinNum One  (JoinZero x) = JoinOne x"|
  "addBinNum (JoinZero x) One = JoinOne x"|
  "addBinNum One (JoinOne x) = JoinZero(addBinNum One x)"|
  "addBinNum (JoinOne x) One = JoinZero(addBinNum x One)"|
  "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)"

Stream: Beginner Questions

Topic: How do I approach this proof?

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