Problem in AFP / AutoCorres2_Main

[Lawrence Paulson]

Yes I’m fixing them

Larry
On 23 Oct 2025 at 10:08 +0100, Florian Haftmann <florian.haftmann at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251023/faba3d6c/attachment.htm>