Hello,

I ran into an issue defining an inductive set like this:

```
theory induct_set
imports
Main
begin
inductive_set Fin :: ‹'a set ⇒ 'a set set› for A :: ‹'a set›
where
empty: ‹{} ∈ Fin A›
| insert: ‹a ∈ A ⟹ B ∈ Fin A ⟹ insert a B ∈ Fin A›
end
```

Isabelle2022 seems to accept the definition, but the proofs for the inductive predicates do not terminate.

Since the inductive definition was taken from the *Isar reference manual* I do assume that the issue does not lie in the definition itself.

The induction rule doesn't show up in `print_theorems`

output either. `thm Fin.induct`

is know to Isabelle though.

I think slow hardware is not the issue.

What am I missing?

Many thanks in advance,

Johannes

It works instantly for me and `print_theorems`

includes the theorems

```
theorems:
Fin.cases: ?a ∈ Fin ?A ⟹ (?a = {} ⟹ ?P) ⟹ (⋀a B. ?a = insert a B ⟹ a ∈ ?A ⟹ B ∈ Fin ?A ⟹ ?P) ⟹ ?P
Fin.empty: {} ∈ Fin ?A
Fin.induct: ?x ∈ Fin ?A ⟹ ?P {} ⟹ (⋀a B. a ∈ ?A ⟹ B ∈ Fin ?A ⟹ ?P B ⟹ ?P (insert a B)) ⟹ ?P ?x
Fin.inducts: ?x ∈ Fin ?A ⟹ ?P {} ⟹ (⋀a B. a ∈ ?A ⟹ B ∈ Fin ?A ⟹ ?P B ⟹ ?P (insert a B)) ⟹ ?P ?x
(*followed by many others*)
```

I find it doubtful that the termination proofs fails because there is no termination proof involved at all in an inductive predicate

Thank you for you quick reply!

I could resolve the `print_theorems`

issue.

But there is a misunderstanding regarding the termination proofs. Please excuse.

I wanted to say, that the proofs for e.g. Fin.induct are displayed as pending by following output when moving the caret below the definition:

`Proving the induction rule ...`

accompanied by grey squiggles below the `inductive_set`

statement.

What confuses me, is that this does not change over time, as if Isabelle would be unable to proof theses predicates.

Is this behavior also observable for you?

I attached a screeshot for reference:

proofs_pending.png

Your interpretation is wrong. :smile: When Isabelle processes the inductive set definition, it outputs these lines with the three dots at their ends to indicate that it is doing these activities at the moment. If performing these activities would take rather long, you might see these lines appear one by one as the respective tasks are undertaken. Isabelle/jEdit associates this output with the `inductive_set`

keyword as the inductive set definition is what produced them, and whenever you place the cursor onto or just below this definition you’ll be able to see them again. The gray, squiggled line below `inductive_set`

just means that there is output related to this keyword available.

So the point is that this is not a popup window that only tells you what Isabelle is doing *at the moment* but rather like a terminal to which output is written successively, only that you don’t see all the output but only the output produced by the command the cursor is on or below.

The indication that Isabelle is still working on, for example, an inductive set definition is that the background of the respective code block is magenta (and a sort of rosy background means that it has not yet started processing the command).

Thank you for the comprehensive explanation! :smile:

You’re welcome. :smile:

Last updated: Sep 11 2024 at 16:22 UTC