Stream: Beginner Questions

Topic: Qed hangs indefinitely

Lukas Löring (May 02 2023 at 12:12):

Hi everyone,

first of all I am a complete beginner with Isabelle, so please be kind if I missed something obvious.

I have the following function definition:

function UTSS_r :: "Pool_Size ⇒ Rank_Threshold  ⇒ 'a Electoral_Module" where
 "UTSS_r S rt A p  = ((max_count_rule S rt) ▹ (min_sum_rule S rt)) A p"
 proof goal_cases
   case (1 P x)
   then show ?case by (metis prod.exhaust_sel)
 next
   case (2 S rt A p S rt A p)
   then show ?case by blast
 qed

Isabelle hangs on the qed command, and after a few seconds the message
linarith_split_limit exceeded (current value is 9)
is printed to the output repeatedly every few seconds.

Any ideas as to

• what is happening here?
• how to solve this?

Thanks a lot!

Manuel Eberl (May 06 2023 at 18:43):

It would be good if you could post a full working example so that people can actually test this.

From the looks of it I suspect that it isn't really your proof or the qed as such that are causing the problem but probably some internal work that the function package does once you've completed the exhaustiveness/non-overlappingness proof. Maybe the derivation of the function elimination rules?

In any case someone (perhaps me) should investigate this, so please give us enough information to reproduce this.

Last updated: Apr 28 2024 at 12:28 UTC