Theory Zassenhaus_Sanity

section ‹Cross-checks on the Zassenhaus lemma›

theory Zassenhaus_Sanity
  imports "HOL-New_Algebra.Zassenhaus_Lemma"
begin

text ‹Zassenhaus is now ∗‹load-bearing›: ‹Schreier_Refinement› imports it, so the whole Jordan--Hölder
  development inherits any error in it.  Like that development it was merged on structural evidence
  (it builds, contains no ‹sorry›).  The checks below test its content.

  The four wings @{term left_top}, @{term left_bottom}, @{term right_top}, @{term right_bottom} are
  where a plausible-looking but wrong Zassenhaus would come from --- transposing an @{term H} for a
  @{term K}, or an @{term H1} for a @{term K1}, still yields sets and still admits a proof of
  ∗‹some› isomorphism.  The checks pin the wings down by their behaviour in cases where their values
  are forced.

  Note on method: these proofs go through the intro/elim API that ‹Zassenhaus› already exports
  (‹left_top_memE›, ‹left_bottom_memI›, ‹left_bottom_memE›)
  rather than unfolding the @{const image} definitions.  Unfolding and finishing with @{method force}
  does not terminate here.›

context zassenhaus
begin

subsection ‹With ‹H⇩1› trivial the left wing collapses›

text ‹This is the case in which Zassenhaus specialises to the second isomorphism theorem: the left
  quotient becomes @{text "(H ∩ K) / (H ∩ K⇩1)"}.  Getting it right is what makes the general
  statement credible, so it is the sharpest single check available without building a concrete group.

  Only the ∗‹elimination› direction is checked for the top wing, since ‹Zassenhaus› exports no
  @{text left_top_memI}; that is enough to catch a wing that is too large.›

lemma left_top_trivial_H1_subset:
  assumes H1: "H1 = {𝟭}" and x: "x ∈ left_top"
  shows "x ∈ H ∩ K"
proof -
  from x obtain b n where b: "b ∈ H ∩ K" and n: "n ∈ H1" and xeq: "x = b ⋅ n"
    by (rule left_top_memE)
  have "n = 𝟭" using n H1 by simp
  moreover have "b ∈ G" using b H.sub by blast
  ultimately show ?thesis using b xeq by simp
qed

text ‹For the bottom wing both directions are available, so the collapse is an equality.›

lemma left_bottom_trivial_H1:
  assumes H1: "H1 = {𝟭}"
  shows "left_bottom = H ∩ K1"
proof
  show "left_bottom ⊆ H ∩ K1"
  proof
    fix x assume "x ∈ left_bottom"
    then obtain c n where c: "c ∈ H ∩ K1" and n: "n ∈ H1" and xeq: "x = c ⋅ n"
      by (rule left_bottom_memE)
    have "n = 𝟭" using n H1 by simp
    moreover have "c ∈ G" using c H.sub by blast
    ultimately show "x ∈ H ∩ K1" using c xeq by simp
  qed
  show "H ∩ K1 ⊆ left_bottom"
  proof
    fix x assume x: "x ∈ H ∩ K1"
    have xG: "x ∈ G" using x H.sub by blast
    have "𝟭 ∈ H1" using H1 by simp
    then have "x ⋅ 𝟭 ∈ left_bottom" using x by (rule left_bottom_memI[rotated])
    then show "x ∈ left_bottom" using xG by simp
  qed
qed


subsection ‹The symmetric case is genuinely symmetric›

text ‹When the two flags coincide the two wings are literally the same set, so the isomorphism is
  between a quotient and itself.  A wing definition that had transposed an @{term H} for a @{term K}
  would fail this, and unlike the collapse above it is a statement about all four wings at once.›

lemma left_top_eq_right_top_when_flags_agree:
  assumes "H = K" and "H1 = K1"
  shows "left_top = right_top"
  unfolding left_top_def right_top_def using assms by simp

lemma left_bottom_eq_right_bottom_when_flags_agree:
  assumes "H = K" and "H1 = K1"
  shows "left_bottom = right_bottom"
  unfolding left_bottom_def right_bottom_def using assms by simp


subsection ‹The butterfly inclusions hold in the required orientation›

text ‹Collected from ‹Zassenhaus›: each bottom wing sits inside its own top wing, and the middle
  group @{term "H ∩ K"} sits inside both tops.  Recording them together checks that the diagram is
  oriented as the lemma's statement needs --- a transposed wing would break one of the four.›

lemmas butterfly_inclusions =
  left_bottom_subset_top right_bottom_subset_top
  middle_subset_left_top middle_subset_right_top

end

end