[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"
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

--
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
http://pp.info.uni-karlsruhe.de
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.