Stream: Mirror: Isabelle Development Mailing List

Topic: Problem in AFP / AutoCorres2_Main

Email Gateway (Oct 23 2025 at 09:08):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
isabelle: ee3a09458665 tip
afp: 3805fcdc2e54 tip

$ isabelle build AutoCorres2_Main
Running AutoCorres2_Main ...
AutoCorres2_Main FAILED (see also "isabelle build_log -H Error
AutoCorres2_Main")
*** Failed to finish proof (line 1810 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
*** 1. length bs = size_td d ⟹
*** ¬ i < size_td d ⟶
*** bs =
*** bs[i := b]
*** At command "by" (line 1810 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")
*** Failed to finish proof (line 1567 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
*** 1. length bs = size_td d ⟹
*** ¬ i < size_td d ⟶
*** bs =
*** bs[i := b]
*** At command "by" (line 1567 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")
*** Failed to finish proof (line 951 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
*** 1. ⟦length bs = size_td s; n ≤ x; x < n + size_td s;
*** size_td s + n ≤ size_of TYPE('a); length pfx = n;
*** length sfx = size_of TYPE('a) - (n + size_td s)⟧
*** ⟹ ¬ x - n < size_td s ⟶
*** bs[0 := b] = bs ∧
*** sfx =
*** sfx[0 := b]
*** At command "by" (line 951 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Email Gateway (Oct 23 2025 at 09:30):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Yes I’m fixing them

Larry
On 23 Oct 2025 at 10:08 +0100, Florian Haftmann <florian.haftmann@cit.tum.de>, wrote:
isabelle: ee3a09458665 tip
afp: 3805fcdc2e54 tip

$ isabelle build AutoCorres2_Main
Running AutoCorres2_Main ...
AutoCorres2_Main FAILED (see also "isabelle build_log -H Error
AutoCorres2_Main")
*** Failed to finish proof (line 1810 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
*** 1. length bs = size_td d ⟹
*** ¬ i < size_td d ⟶
*** bs =
*** bs[i := b]
*** At command "by" (line 1810 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")
*** Failed to finish proof (line 1567 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
*** 1. length bs = size_td d ⟹
*** ¬ i < size_td d ⟶
*** bs =
*** bs[i := b]
*** At command "by" (line 1567 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")
*** Failed to finish proof (line 951 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
*** 1. ⟦length bs = size_td s; n ≤ x; x < n + size_td s;
*** size_td s + n ≤ size_of TYPE('a); length pfx = n;
*** length sfx = size_of TYPE('a) - (n + size_td s)⟧
*** ⟹ ¬ x - n < size_td s ⟶
*** bs[0 := b] = bs ∧
*** sfx =
*** sfx[0 := b]
*** At command "by" (line 951 of
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")

Florian

Last updated: Nov 05 2025 at 08:30 UTC