Re: [isabelle] structured induction proofs using customized induction scheme



Hi Bianca,

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:

proof
  (induct
    taking: ...
    rule: beta_induct[where ?'a="unit" and ?'b="unit"])
  case UpdR

Best regards,
Andreas

Bianca Lutz schrieb:
Hi all.

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
"illegal" ones.
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.

Thanks,
Bianca.


--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
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 MHonArc.