Stream: Beginner Questions

Topic: How do I approach this proof?


view this post on Zulip 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
  "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)"

Last updated: Feb 27 2024 at 08:17 UTC