Re: [isabelle] structured induction proofs using customized induction scheme
the problem is with your induction rule. The two cases that do not work
(UpdR and Obj) both meta-quantify over the variable L that does not
occur in these two cases. When you delete the L in both cases in the
rule, everything should work fine.
To explain the error message: The illegal schematic variable is not a
term variable, but an unbound type variable. If you display your
induction rule with "thm beta_induct" with Show Types in the Settings
menu enabled, you see that beta_induct contains two free type variables
for these quantified term variables.
If you instantiate this type variable in the induction rule explicitly,
your original induction rule works, too:
rule: beta_induct[where ?'a="unit" and ?'b="unit"])
Bianca Lutz schrieb:
On Thu, Feb 4, 2010 at 12:59 PM, Andreas Lochbihler
<andreas.lochbihler at kit.edu> wrote:
3. Your induction rule R_induct involves the free variable P2 that does not
occur in the conclusion nor in the consumed facts. This is usually the cause
for your error message "unbound schematic variable(s) in case 2".
Actually, the error doesn't concern unbound schematic variables but
Which is just odd since there is no schematic variable besides "?case" ...
Anyway, I refactored my code according to your advices.
In addition I updated my Isabelle environment to the latest version
(just in case that my installation was corrupted). Unfortunately, the
error still occurs.
Since Andreas was unable to reproduce the error I assume that the
induction rule doesn't cause the error but something else I missed.
Therefore, I stripped off anything that is not involved in the failing
proof (the corresponding lemma is called beta_lc). Nevertheless, this
minimal version fails on my machine.
Attached you will find the source file including an apply style proof
of beta_lc that works just fine. I would be grateful if anyone could
try to reproduce the error using this.
Karlsruher Institut für Technologie
Adenauerring 20a, Gebäude 50.41, Raum 023
Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales
Großforschungszentrum in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and