Email Gateway (Aug 19 2022 at 08:53): Email Gateway (Aug 19 2022 at 08:53):From: Makarius <makarius@sketis.net>
After several years of "localizing" most definitional packages to work
with locale, class, interpretation targets, we now have stage two of
nested context localization starting with the Isabelle2012 release.
I will make an effort when converging towards the coming release to sort
out the issues that have been accumulated in the past few months. It will
probably take several release cycles until most packages work again
after introducing this new feature last winter.
Makarius
Email Gateway (Aug 19 2022 at 09:05):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
In Isabelle2012 and the current development version (ID 3259ea7a52af), the
attributes consumes and case_conclusion do not correctly adjust the positions of
assumptions. Here's a small example:
context fixes p :: nat assumes "p > 0"
begin
coinductive foo where
p: "foo p"
| Suc: "foo n ==> foo (Suc n)"
inductive bar where
p: "bar p"
| Suc: "bar n ==> bar (Suc n)"
end
lemma
assumes "p > 0" "bar p n"
shows "p <= n"
using assms
proof(induct) (* 1 *)
oops
lemma
assumes "p > 0" "p <= n"
shows "foo p n"
using assms
proof(coinduct) (* 2 *)
In (* 1 *), there are three goals left, the first being "bar p n", which should
normally be consumed.
In (* 2 *), coinduct raises
*** exception TERM raised (line 87 of "Isar/rule_cases.ML"):
*** Expected 2 binop arguments
*** ?X n
*** At command "proof"
Apparently, coinduct tries to define the short-hands for the case conclusions by
unifying with the coinduction hypothesis.
Andreas
Last updated: Nov 21 2024 at 12:39 UTC