Stream: Beginner Questions

Topic: Ill typed instantiation

view this post on Zulip Lekhani Ray (Jul 21 2022 at 22:05):

I have a lemma

lemma (in th8b) new_lemma: "plus zero n = n"

However, if I apply induction on n, it gives me an error that says unable to figure out induction rule.

If I try strong induction apply(induction n rule: nat_less_induct) I get an error "Ill-typed instantiation:
n :: 'a" What does this mean?

Edit:
The zero and plus are from locale th1 and th2. While there is a similar assumption (to new_lemma) in th2, I am trying to prove the commutative as well.

locale th1 =
  fixes
    zero :: "'a"
    and suc :: "'a ⇒ 'a"
  assumes
    "suc n ≠ zero"
    and "suc n = suc m ⟶ n = m"

locale th2 = th1 +
  fixes
    plus :: "'a ⇒ 'a ⇒ 'a"
    and evalBinNum :: "BinNum ⇒ 'a"
  assumes
     arith_1: "⋀n. plus n zero = n"
    and plus_suc: "⋀n m. plus n (suc m) = suc ( plus n m)"

locale th3 = th2 +
  fixes
    times :: "'a ⇒ 'a ⇒ 'a"
  assumes
    "times n zero = zero"
    and "times n (suc m) =  plus (times n m) n"
locale th8b = th3 +
 assumes p1:
    "((∀x . p zero ∧ ( p x ⟶ p (suc x))) ⟶ (∀x. p x))"

view this post on Zulip Mathias Fleury (Jul 22 2022 at 04:49):

What is the induction principle you expect on element of the arbitrary type 'a?

view this post on Zulip Mathias Fleury (Jul 22 2022 at 04:52):

And you intended to use p1 with apply (induction n rule: p1) you have to change p1 first:

locale th8b = th3 +
 assumes p1:
    "⋀x. ((⋀x . p zero ∧ ( p x ⟶ p (suc x)))) ⟹ p x"

lemma (in th8b) new_lemma: "plus zero n = n"
  apply (induction n rule: p1)

Last updated: Dec 21 2024 at 16:20 UTC