zombie proof processes

[Peter Lammich]

Another one. veriT. Somewhere in my proof exploration of the below.

I'll try to re-sledgehammer all goals in there, maybe it provokes a 
rogue veriT again...

--

   Peter


imports Complex_Main
begin


lemma upt_fuse: "⟦l≤m; m<h ⟧ ⟹ [l..<m] @ [m..<h] = [l..<h]"
   by (metis less_imp_add_positive upt_add_eq_append)


corollary harmonic_series_unbounded_aux: "n ≤ (∑i←[1..<2^(2*n)+1]. 1/i)"
proof -

   have A: "(real n+1)/2 ≤ (∑i←[1..<2^n+1]. 1/i)" for n
   proof (induction n)
     case 0
     then show ?case by simp
   next
     case (Suc n)

     (* It feels like we're working against the simplifier for [_ ..< 
Suc _], so we disable that rule *)
     find_theorems "[_..<Suc _]"
     note [simp del] = upt_Suc

     have SPLIT: "[1..< 2^Suc n + 1] = [1..< 2^n + 1]@[2^n + 1 ..< 2^Suc 
n + 1]" (is "_ = ?l1@?l2")
       by (simp add: upt_fuse)

     from Suc.IH have "(real n+1)/2 ≤ (∑i←?l1. 1/i)" .
     moreover have "1/2 ≤ (∑i←?l2. 1/i)" proof -
       have 1: "(1/2 :: real) ≤ (∑i←?l2. 1/2^Suc n)" by (simp add: 
sum_list_triv)
       have 2: "(∑i←?l2. 1/2^Suc n) ≤ (∑i←?l2. 1/i)"
         apply (rule sum_list_mono)
         apply (clarsimp simp: less_Suc_eq_le)
         apply (drule of_nat_mono[where j="2*2^_"])
         by (auto simp: field_simps)
       from order_trans[OF 1 2] show ?thesis .
     qed
     ultimately show ?case
       apply (subst SPLIT)
       by simp
   qed

   show ?thesis
     apply (rule order_trans[OF _ A])
     by auto
qed



lemma harmonic_series_unbounded: "∃n. c ≤ (∑i←[1..<n]. 1/i)"
proof -
   have "c ≤ (nat ¦⌈c⌉¦)" by linarith
   also note harmonic_series_unbounded_aux
   finally show ?thesis by blast
qed


On 28/11/2025 17:56, Makarius wrote:
> On 28/11/2025 17:40, Peter Lammich wrote:
>>
>> On 28/11/2025 17:16, Lawrence Paulson wrote:
>>> As it is intermittent, I was wondering whether certain 
>>> characteristics of the goal might cause this.
>>>
>>> Is your example reproducible?
>>
>> Unfortunately not. I only realized that this process was running 7 
>> minutes after it was started ... no idea what I was sledgehammering 
>> at this point :(
>>
>> I typically realize that only when I keep hearing my CPU fan, and my 
>> CPU temperature keeps being high, although no proof or sledgehammer 
>> is running.
>
> Peter,
>
> that is new information: the problem happens on Linux, and for 
> Isabelle2025 already. So it is not specific to macOS 26, nor to any 
> changes towards Isabelle2025-1.
>
> I am still interested to learn about the reasons, but it is now more 
> likely to get ticked-off as "non-regression" towards Isabelle2025.
>
>
>     Makarius
>