[isabelle] Mutual coinduction
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:
coinductive_set X and Y where
"n â Y â Suc n â X"
| "n â X â Suc n â Y"
shows "(âx. P x â x â X) â (âx. Q x â x â Y)"
proof (coinduct rule: X_Y.coinduct)
In the first line of the proof of lemma 'tmp' the following exception is
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and