Lekhani Ray (Jul 19 2022 at 20:58): Lekhani Ray (Jul 19 2022 at 20:58):I have a lemma
lemma (in th2) addMeaningF_2: "∀m. m ≤ n ⟹ (m = (len x + len y) ⟹ (evalBinNum_1 (addBinNum x y) = plus (evalBinNum_1 x) (evalBinNum_1 y)))"
evalBinNum and addBinNum are recursive functions.
Everytime I apply(induct n) Isabelle prompts that it is unable to figure out the induct rule. Why does this happen?
Maximilian Schaeffeler (Jul 20 2022 at 06:58):In your statement, m is only bound locally in the first premise, it is free in the second one.
Thus the bound m in the first premise is not forced to be of type nat, and therefore also n::'a::ord.
Since there is no general induction rule for orders, the induct method fails.
Lekhani Ray (Jul 21 2022 at 03:27):Maximilian Schaeffeler said:
In your statement,
mis only bound locally in the first premise, it is free in the second one.
Thus the boundmin the first premise is not forced to be of typenat, and therefore alson::'a::ord.
Since there is no general induction rule for orders, the induct method fails.
Thank you!
If I try to bind m over the whole expression (by simple enclosing everything after ∀m. within brackets) I get a parsing error. I was wondering if I'm missing something?
Mathias Fleury (Jul 21 2022 at 04:56):Either !!m. ... ⟹ ... or "∀m. (... --> ...)
Mathias Fleury (Jul 21 2022 at 04:56):The more natural version being no quantifiers and apply (induct n arbitrary: m)
Lekhani Ray (Jul 21 2022 at 12:00):Mathias Fleury said:
The more natural version being no quantifiers and
apply (induct n arbitrary: m)
It cannot quite recognize m in this case. Is it because it is bound?
Mathias Fleury (Jul 21 2022 at 12:01):yes, you have to remove the !!
Notification Bot (Jul 21 2022 at 12:23):Lekhani Ray has marked this topic as resolved.
Last updated: Apr 18 2024 at 20:16 UTC