Email Gateway (Aug 18 2022 at 11:03): Email Gateway (Aug 18 2022 at 11:03):From: George Karabotsos <g_karab@cs.concordia.ca>
Hello,
I am trying to work out the /even/ example for inductively defined sets
using Isabelle2007.
I have also turned on the trace_simp variable.
While trying to discharge the first lemma:
lemma two_times_even[intro!]: "2*k \<in> even"
the trace displays the following:
[1]Adding rewrite rule "??.unknown":
2 * n : even == True
Any idea what the "??.unknown" is? I cannot recall seeing it with the
05 version but I may be wrong.
George
Email Gateway (Aug 18 2022 at 11:03):From: Alexander Krauss <krauss@in.tum.de>
The rule comes from the induction hypothesis (the premise of the second
subgoal), and it is automatically used to simplify the induction step.
Since it is just local and does not have a proper name (like a lemma),
it gets some funny internal name. I am not sure if Isabelle2005
displayed the names like this but it certainly behaved in the same way.
Alex
Last updated: Nov 21 2024 at 12:39 UTC