Stream: Beginner Questions

Topic: Inductive set predicates not proven


view this post on Zulip 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?

Many thanks in advance,
Johannes

view this post on Zulip 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*)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Johannes Hauschild (Aug 16 2023 at 12:31):

Thank you for the comprehensive explanation! :smile:

view this post on Zulip Wolfgang Jeltsch (Aug 16 2023 at 12:31):

You’re welcome. :smile:


Last updated: Feb 27 2024 at 08:17 UTC