theory Scratch
  imports Main
begin

text ‹Problems in ‹thm.ML›. Tested on Isabelle dev, hg 410b271f3ac4
(committed 2026-10-08).
Line numbers refer to ‹src/Pure/thm.ML› in that revision.›

section ‹Soundness issues›

subsection ‹Case 1: ‹res› drops the rule's flex-flex pairs (L2620)›

lemma flex_rule1: "x True ⟹ x True" . ―‹Important: x here and below must
share the same name.›
lemma flex_rule2: "P True ⟹ ∀x::bool. P True" by simp

lemma "∀y::bool. False" ― ‹Important: name of y must not be equal to x›
  apply (rule flex_rule1[THEN flex_rule2]) ― ‹new subgoal: ‹?y True›,
should be ‹False››
  by (rule TrueI)

text ‹Possible cause: L2620 passes only ‹[BBi]› to ‹newAs›, not the
rule's flex-flex pairs ‹rtpairs›.
So ‹?x›, whose pair got solved, is not protected (L2432--2435) and is
renamed to ‹?y›
(L2439--2442). The binding for ‹?x› then misses ‹?y›.›

subsection ‹Case 2: ‹eres› drops the rule's flex-flex pairs (L2608)›

lemma eres_rule: "P True ⟹ (∀x::bool. ¬ P True) ⟹ False" by simp

lemma "∀y::bool. ¬ False ⟹ False"
  apply (erule flex_rule1[THEN eres_rule, rotated]) ― ‹new subgoal: ‹?y
True›, should be ‹False››
  by (rule TrueI)

text ‹Possible cause: like Case 1, but on the elim-resolution path:
L2608 passes only
‹[BBi, (concl', asm')]› to ‹newAs›.›

subsection ‹Case 3: ‹strip_apply› renames only part of a premise
(L2408--2414)›

definition X :: "prop" where "X ≡ (⋀w::bool. True ⟹ False)"

lemma split_rule: "(⋀z::bool. z = w ⟹ z ≠ w) ⟹ PROP X" ― ‹Important: w
here and in X must share the same name.›
  unfolding X_def by auto

lemma split_aux: "z = True ⟹ z ≠ False" by simp

schematic_goal split_bad: "PROP ?G (λv::nat. v)" ― ‹Important: name of v
must not be equal to w›
  apply (rule split_rule[unfolded X_def]) ― ‹new subgoal: ‹⋀z. z = ?w ⟹
z ≠ ?v››
  apply (rule split_aux)
  apply assumption
  done

lemma False by (rule split_bad) (rule TrueI)

text ‹Possible cause: ‹strip_apply› (L2408--2414, used at L2584) strips
‹⋀›/‹⟹› as long as ‹B› has them,
not just the ‹nlift› lifted ones. With a rule conclusion ‹⋀w. …› it cuts
into the premise, so
‹?w› is renamed in ‹z ≠ ?w› but not in ‹z = ?w›.›

end