2016-09-26 11:07:49 UTC
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