Thomas Sternagel

2016-09-26 11:07:49 UTC

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

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