[isabelle] Attributes consumes and case_conclusion ignores unnamed context

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"

coinductive foo where
  p: "foo p"
| Suc: "foo n ==> foo (Suc n)"

inductive bar where
  p: "bar p"
| Suc: "bar n ==> bar (Suc n)"


  assumes "p > 0" "bar p n"
  shows "p <= n"
using assms
proof(induct) (* 1 *)

  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.


Karlsruher Institut für Technologie
IPD Snelting

Dr. Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.