[isabelle] Mutual coinduction



Dear List,

I'm trying to figure out mutual coinduction in a development version of
Isabelle/HOL (d4b89572ae71). In particular I want to use the coinduction
scheme for two sets defined by mutual coinduction, but I'm not even able
to formulate my goal in a way that I can use 'coinduct'.
Consider the following minimal example:

theory Tmp
imports
  Main
begin

coinductive_set X and Y where
  "n â Y â Suc n â X"
| "n â X â Suc n â Y"

lemma tmp:
  shows "(âx. P x â x â X) â (âx. Q x â x â Y)"
proof (coinduct rule: X_Y.coinduct)
sorry

end

In the first line of the proof of lemma 'tmp' the following exception is
raised

exception TERM raised (line 80 of "Isar/rule_cases.ML"):
  Expected 2 binop arguments
  ân. B.0 = Suc n â (Q n â n â Y)

What am I doing wrong? What is 'B.0'? I don't understand what's
happening here.

Tom




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