Inductive set predicates not proven · Beginner Questions

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.

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

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

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.

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

Stream: Beginner Questions

Topic: Inductive set predicates not proven

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