Stream: Beginner Questions

Topic: Inductive set predicates not proven

Johannes Hauschild (Aug 15 2023 at 17:48):

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?

Johannes

Mathias Fleury (Aug 15 2023 at 19:16):

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*)
``````

Mathias Fleury (Aug 15 2023 at 19:17):

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

Johannes Hauschild (Aug 16 2023 at 11:49):

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

Wolfgang Jeltsch (Aug 16 2023 at 12:22):

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.

Wolfgang Jeltsch (Aug 16 2023 at 12:25):

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.

Wolfgang Jeltsch (Aug 16 2023 at 12:30):

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).

Johannes Hauschild (Aug 16 2023 at 12:31):

Thank you for the comprehensive explanation! :smile:

Wolfgang Jeltsch (Aug 16 2023 at 12:31):

You’re welcome. :smile:

Last updated: Dec 07 2023 at 20:16 UTC