Theory Expander_Graphs.Expander_Graphs_Strongly_Explicit

section ‹Strongly Explicit Expander Graphs\label{sec:see}›

text ‹In some applications, representing an expander graph using a data structure (for example
as an adjacency lists) would be prohibitive. For such cases strongly explicit expander graphs (SEE)
are relevant. These are expander graphs, which can be represented implicitly using a function that
computes for each vertex its neighbors in space and time logarithmic w.r.t. to the size of the
graph. An application can for example sample a random walk, from a SEE using such a function
efficiently. An example of such a graph is the Margulis construction from
Section~\ref{sec:margulis}. This section presents the latter as a SEE but also shows that two graph
operations that preserve the SEE property, in particular the graph power construction from
Section~\ref{sec:graph_power} and a compression scheme introduced by
Murtagh et al.~\cite[Theorem~20]{murtagh2019}. Combining all of the above it is possible to construct
strongly explicit expander graphs of \emph{every size} and spectral gap.›

theory Expander_Graphs_Strongly_Explicit
  imports Expander_Graphs_Power_Construction Expander_Graphs_MGG
begin

unbundle intro_cong_syntax
no_notation Digraph.dominates (‹_ →ı _› [100,100] 40)

record strongly_explicit_expander =
  see_size :: nat
  see_degree :: nat
  see_step :: "nat ⇒ nat ⇒ nat"

definition graph_of :: "strongly_explicit_expander ⇒ (nat, (nat,nat) arc) pre_digraph"
  where "graph_of e =
    ⦇ verts = {..<see_size e},
      arcs = (λ(v, i). Arc v (see_step e i v) i) ` ({..<see_size e} × {..<see_degree e}),
      tail = arc_tail,
      head = arc_head ⦈"

definition "is_expander e Λ⇩a ⟷
  regular_graph (graph_of e) ∧ regular_graph.Λ⇩a (graph_of e) ≤ Λ⇩a"

lemma is_expander_mono:
  assumes "is_expander e a" "a ≤ b"
  shows "is_expander e b"
  using assms unfolding is_expander_def by auto

lemma graph_of_finI:
  assumes "see_step e ∈ ({..<see_degree e} → ({..<see_size e} → {..<see_size e}))"
  shows "fin_digraph (graph_of e)"
proof -
  let ?G = "graph_of e"

  have "head ?G a ∈ verts ?G ∧ tail ?G a ∈ verts ?G" if "a ∈ arcs ?G" for a
    using assms that unfolding graph_of_def by (auto simp add:Pi_def)

  hence 0: "wf_digraph ?G"
    unfolding wf_digraph_def by auto

  have 1: "finite (verts ?G)"
    unfolding graph_of_def by simp

  have 2: "finite (arcs ?G)"
    unfolding graph_of_def by simp
  show ?thesis
    using 0 1 2 unfolding fin_digraph_def fin_digraph_axioms_def by  auto
qed

lemma edges_graph_of:
  "edges(graph_of e)={#(v,see_step e i v). (v,i)∈#mset_set ({..<see_size e}×{..<see_degree e})#}"
proof -
  have 0:"mset_set ((λ(v, i). Arc v (see_step e i v) i) ` ({..<see_size e} × {..<see_degree e}))
    = {# Arc v (see_step e i v) i. (v,i) ∈# mset_set ( {..<see_size e} × {..<see_degree e})#}"
    by (intro image_mset_mset_set[symmetric] inj_onI) auto

  have "edges (graph_of e) =
    {#(fst p, see_step e (snd p) (fst p)). p ∈# mset_set ({..<see_size e} × {..<see_degree e})#}"
    unfolding edges_def graph_of_def arc_to_ends_def using 0
    by (simp add:image_mset.compositionality comp_def case_prod_beta)
  also have "... = {#(v, see_step e i v). (v,i) ∈# mset_set ({..<see_size e} × {..<see_degree e})#}"
    by (intro image_mset_cong) auto
  finally show ?thesis by simp
qed

lemma out_degree_see:
  assumes "v ∈ verts (graph_of e)"
  shows "out_degree (graph_of e) v = see_degree e" (is "?L = ?R")
proof -
  let ?d = "see_degree e"
  let ?n = "see_size e"
  have 0: "v < ?n"
    using assms unfolding graph_of_def by simp

  have "?L = card {a. (∃x∈{..<?n}. ∃y∈{..<?d}. a = Arc x (see_step e y x) y) ∧ arc_tail a = v}"
    unfolding out_degree_def out_arcs_def graph_of_def by (simp add:image_iff)
  also have "... = card {a. (∃y∈{..<?d}. a = Arc v (see_step e y v) y)}"
    using 0 by (intro arg_cong[where f="card"]) auto
  also have "... = card ((λy. Arc v (see_step e y v) y) ` {..<?d})"
    by (intro arg_cong[where f="card"] iffD2[OF set_eq_iff]) (simp add:image_iff)
  also have "... = card {..<?d}"
    by (intro card_image inj_onI) auto
  also have "... = ?d" by simp
  finally show ?thesis by simp
qed

lemma card_arc_walks_see:
  assumes "fin_digraph (graph_of e)"
  shows "card (arc_walks (graph_of e) n) = see_degree e^n * see_size e" (is "?L = ?R")
proof -
  let ?G = "graph_of e"
  interpret fin_digraph ?G
    using assms by auto
  have "?L = card (⋃v ∈ verts ?G. {x. fst x = v ∧ is_arc_walk ?G v (snd x) ∧ length (snd x) = n})"
    unfolding arc_walks_def by (intro arg_cong[where f="card"]) auto
  also have "... = (∑v ∈ verts ?G. card {x. fst x=v∧is_arc_walk ?G v (snd x)∧length (snd x) = n})"
    using is_arc_walk_set[where G="?G"]
    by (intro card_UN_disjoint ballI finite_cartesian_product subsetI finite_lists_length_eq
        finite_subset[where B="verts ?G × {x. set x ⊆ arcs ?G ∧ length x = n}"]) force+
  also have "... = (∑v ∈ verts ?G. out_degree (graph_power ?G n) v)"
    unfolding out_degree_def graph_power_def out_arcs_def arc_walks_def
    by (intro sum.cong arg_cong[where f="card"]) auto
  also have "... = (∑v ∈ verts ?G. see_degree e^n)"
    by (intro sum.cong graph_power_out_degree' out_degree_see refl) (simp_all add: graph_power_def)
  also have "... = ?R"
    by (simp add:graph_of_def)
  finally show ?thesis by simp
qed

lemma regular_graph_degree_eq_see_degree:
  assumes "regular_graph (graph_of e)"
  shows "regular_graph.d (graph_of e) = see_degree e" (is "?L = ?R")
proof -
  interpret regular_graph "graph_of e"
    using assms(1) by simp
  obtain v where v_set: "v ∈ verts (graph_of e)"
    using verts_non_empty by auto
  hence "?L = out_degree (graph_of e) v"
    using v_set reg by auto
  also have "... = see_degree e"
    by (intro out_degree_see v_set)
  finally show ?thesis by simp
qed

text ‹The following introduces the compression scheme, described in \cite[Theorem 20]{murtagh2019}.›

fun see_compress :: "nat ⇒ strongly_explicit_expander ⇒ strongly_explicit_expander"
  where "see_compress m e =
    ⦇ see_size = m, see_degree = see_degree e * 2
    , see_step = (λk v.
      if k < see_degree e
        then (see_step e k v) mod m
        else (if v+m < see_size e then (see_step e (k-see_degree e) (v+m)) mod m else v)) ⦈"

lemma edges_of_compress:
  fixes e m
  assumes "2*m ≥ see_size e" "m ≤ see_size e"
  defines "A ≡ {# (x mod m, y mod m). (x,y) ∈# edges (graph_of e)#}"
  defines "B ≡ repeat_mset (see_degree e) {# (x,x). x ∈# (mset_set {see_size e - m..<m})#}"
  shows "edges (graph_of (see_compress m e)) = A + B" (is "?L = ?R")
proof -
  let ?d = "see_degree e"
  let ?c = "see_step (see_compress m e)"
  let ?n = "see_size e"
  let ?s = "see_step e"

  have 7:"m ≤ v ⟹ v < ?n ⟹ v - m = v mod m" for v
    using assms by (simp add: le_mod_geq)

  let ?M = "mset_set ({..<m}×{..<2*?d})"
  define M1 where "M1 = mset_set ({..<m} × {..<?d})"
  define M2 where "M2 = mset_set ({..<?n-m} × {?d..<2*?d})"
  define M3 where "M3 = mset_set ({?n-m..<m} × {?d..<2*?d})"

  have "M2 = mset_set ((λ(x,y). (x-m,y+?d)) ` ({m..<?n} × {..<?d}))"
    using assms(2) unfolding M2_def map_prod_def[symmetric] atLeast0LessThan[symmetric]
    by (intro arg_cong[where f="mset_set"] map_prod_surj_on[symmetric])
      (simp_all add:  image_minus_const_atLeastLessThan_nat mult_2)
  also have "... = image_mset (λ(x,y). (x-m,y+?d)) (mset_set ({m..<?n} × {..<?d}))"
    by (intro image_mset_mset_set[symmetric] inj_onI) auto
  finally have M2_eq: "M2 = image_mset (λ(x,y). (x-m,y+?d)) (mset_set ({m..<?n} × {..<?d}))"
    by simp

  have "?M = mset_set ({..<m}×{..<?d} ∪ {..<?n-m}×{?d..<2*?d} ∪ {?n-m..<m}×{?d..<2*?d})"
    using assms(1,2) by (intro arg_cong[where f="mset_set"]) auto
  also have "... = mset_set ({..<m}×{..<?d} ∪ {..<?n-m}×{?d..<2*?d}) + M3"
    unfolding M3_def by (intro mset_set_Union) auto
  also have "... = M1 + M2 + M3"
    unfolding M1_def M2_def
    by (intro arg_cong2[where f="(+)"] mset_set_Union) auto
  finally have 0:"mset_set ({..<m} × {..<2*?d}) = M1 + M2 + M3" by simp

  have 1:"{#(v,?c i v). (v,i)∈#M1#}={#(v mod m,?s i v mod m). (v,i)∈#mset_set ({..<m}×{..<?d})#}"
    unfolding M1_def by (intro image_mset_cong) auto

  have "{#(v,?c i v).(v,i)∈#M2#}={#(fst x-m,?c(snd x+?d)(fst x-m)).x∈#mset_set({m..<?n}×{..<?d})#}"
    unfolding M2_eq
    by (simp add:image_mset.compositionality comp_def case_prod_beta del:see_compress.simps)
  also have "... = {#(v - m,?s i v mod m). (v,i)∈#mset_set ({m..<?n}×{..<?d})#}"
    by (intro image_mset_cong) auto
  also have "... = {#(v mod m,?s i v mod m). (v,i)∈#mset_set ({m..<?n}×{..<?d})#}"
    using 7 by (intro image_mset_cong) auto
  finally have 2:
    "{#(v,?c i v). (v,i)∈#M2#}={#(v mod m,?s i v mod m). (v,i)∈#mset_set ({m..<?n}×{..<?d})#}"
    by simp

  have "{#(v,?c i v). (v,i)∈#M3#} = {#(v,v). (v,i) ∈#  mset_set ({?n-m..<m} × {?d..<2*?d})#}"
    unfolding M3_def by (intro image_mset_cong) auto
  also have "... = concat_mset {#{#(x, x). xa ∈# mset_set {?d..<2 * ?d}#}. x ∈# mset_set {?n - m..<m}#}"
    by (subst mset_prod_eq) (auto simp:image_mset.compositionality image_concat_mset comp_def)
  also have "... = concat_mset {#replicate_mset ?d (x, x). x ∈# mset_set {?n - m..<m}#}"
    unfolding image_mset_const_eq by simp
  also have "... = B"
    unfolding B_def repeat_image_concat_mset by simp
  finally have 3:"{#(v,?c i v). (v,i)∈#M3#}=B" by simp

  have "A = {#(fst x mod m, ?s (snd x) (fst x) mod m). x ∈# mset_set ({..<?n} × {..<?d})#}"
    unfolding A_def edges_graph_of by (simp add:image_mset.compositionality comp_def case_prod_beta)
  also have "... = {#(v mod m,?s i v mod m). (v,i)∈#mset_set({..<?n}×{..<?d})#}"
    by (intro image_mset_cong) auto
  finally have 4: "A = {#(v mod m,?s i v mod m). (v,i)∈#mset_set({..<?n}×{..<?d})#}"
    by simp

  have "?L = {# (v, ?c i v). (v,i) ∈# ?M #}"
    unfolding edges_graph_of by (simp add:ac_simps)
  also have "... = {#(v,?c i v). (v,i)∈#M1#}+{#(v,?c i v). (v,i)∈#M2#}+{#(v,?c i v). (v,i)∈#M3#}"
    unfolding 0 image_mset_union by simp
  also have "...={#(v mod m,?s i v mod m). (v,i)∈#mset_set({..<m}×{..<?d}∪{m..<?n}×{..<?d})#}+B"
    unfolding 1 2 3 image_mset_union[symmetric]
    by (intro_cong "[σ⇩2 (+), σ⇩2 image_mset]" more: mset_set_Union[symmetric]) auto
  also have "...={#(v mod m,?s i v mod m). (v,i)∈#mset_set({..<?n}×{..<?d})#}+B"
    using assms(2) by (intro_cong "[σ⇩2 (+), σ⇩2 image_mset, σ⇩1 mset_set]") auto
  also have "... = A + B"
    unfolding 4 by simp
  finally show ?thesis by simp
qed

lemma see_compress_sym:
  assumes "2*m ≥ see_size e" "m ≤ see_size e"
  assumes "symmetric_multi_graph (graph_of e)"
  shows "symmetric_multi_graph (graph_of (see_compress m e))"
proof -
  let ?c = "see_compress m e"
  let ?d = "see_degree e"
  let ?G = "graph_of e"
  let ?H = "graph_of (see_compress m e)"

  interpret G:"fin_digraph" "?G"
    by (intro symmetric_multi_graphD2[OF assms(3)])
  interpret H:"fin_digraph" "?H"
    by (intro graph_of_finI) simp

  have deg_compres: "see_degree ?c = 2 * see_degree e"
    by simp

  have 1: "card (arcs_betw ?H v w) = card (arcs_betw ?H w v)" (is "?L = ?R")
    if "v ∈ verts ?H" "w ∈ verts ?H" for v w
  proof -
    define b where "b =count {#(x, x). x ∈# mset_set {see_size e - m..<m}#} (v, w)"

    have b_alt_def: "b = count {#(x, x). x ∈# mset_set {see_size e - m..<m}#} (w, v)"
      unfolding b_def count_mset_exp
      by (simp add:case_prod_beta image_mset_filter_mset_swap[symmetric] ac_simps)

    have "?L = count (edges ?H) (v,w)"
      unfolding H.count_edges by simp
    also have "... = count {#(x mod m, y mod m). (x, y) ∈# edges (graph_of e)#} (v, w) + ?d * b"
      unfolding edges_of_compress[OF assms(1,2)] b_def by simp
    also have "... = count {#(snd e mod m, fst e mod m). e ∈# edges (graph_of e)#} (v, w) + ?d * b"
      by (subst G.edges_sym[OF assms(3),symmetric])
        (simp add:image_mset.compositionality comp_def case_prod_beta)
    also have "... = count {#(x mod m, y mod m). (x,y) ∈# edges (graph_of e)#} (w, v) + ?d * b"
      unfolding count_mset_exp
      by (simp add:image_mset_filter_mset_swap[symmetric] ac_simps case_prod_beta)
    also have "... = count (edges ?H) (w,v)"
      unfolding edges_of_compress[OF assms(1,2)] b_alt_def by simp
    also have "... = ?R"
      unfolding H.count_edges by simp
    finally show ?thesis by simp
  qed

  show ?thesis
    using 1 H.fin_digraph_axioms
    unfolding symmetric_multi_graph_def by auto
qed

lemma see_compress:
  assumes "is_expander e Λ⇩a"
  assumes "2*m ≥ see_size e" "m ≤ see_size e"
  shows "is_expander (see_compress m e) (Λ⇩a/2 + 1/2)"
proof -
  let ?H = "graph_of (see_compress m e)"
  let ?G = "graph_of e"
  let ?d = "see_degree e"
  let ?n = "see_size e"

  interpret G:regular_graph "graph_of e"
    using assms(1) is_expander_def by simp

  have d_eq: "?d = G.d"
    using regular_graph_degree_eq_see_degree[OF G.regular_graph_axioms] by simp

  have n_eq: "G.n = ?n"
    unfolding G.n_def by (simp add:graph_of_def)

  have n_gt_1: "?n > 0"
    using G.n_gt_0 n_eq by auto

  have "symmetric_multi_graph (graph_of (see_compress m e))"
    by (intro see_compress_sym assms(2,3) G.sym)
  moreover have "see_size e > 0"
    using G.verts_non_empty unfolding graph_of_def by auto
  hence "m > 0" using assms(2) by simp
  hence "verts (graph_of (see_compress m e)) ≠ {}"
    unfolding graph_of_def by auto
  moreover have 1:"0 < see_degree e"
    using d_eq G.d_gt_0 by auto
  hence "0 < see_degree (see_compress m e)" by simp
  ultimately have 0:"regular_graph ?H"
    by (intro regular_graphI[where d="see_degree (see_compress m e)"] out_degree_see) auto
  interpret H:regular_graph ?H
    using 0 by auto

  have "¦∑a∈arcs ?H. f (head ?H a) * f (tail ?H a)¦ ≤ (real G.d * G.Λ⇩a + G.d) * (H.g_norm f)⇧2"
    (is "?L ≤ ?R") if "H.g_inner f (λ_. 1) = 0" for f
  proof -
    define f' where "f' x = f (x mod m)" for x
    let ?L1 = "G.g_norm f'^2 + ¦∑x=?n-m..<m. f x^2¦"
    let ?L2 = "G.g_inner f' (λ_.1)^2/ G.n + ¦∑x=?n-m..<m. f x^2¦"

    have "?L1 = (∑x<?n. f (x mod m)^2) + ¦∑x=?n-m..<m. f x^2¦"
      unfolding G.g_norm_sq G.g_inner_def f'_def by (simp add:graph_of_def power2_eq_square)
    also have "... = (∑x∈{0..<m} ∪ {m..<?n}. f (x mod m)^2) + (∑x=?n-m..<m. f x^2)"
      using assms(3) by (intro_cong "[σ⇩2 (+)]" more:sum.cong abs_of_nonneg sum_nonneg) auto
    also have "...=(∑x=0..<m. f (x mod m)^2) + (∑x=m..<?n. f (x mod m)^2) + (∑x=?n-m..<m. f x^2)"
      by (intro_cong "[σ⇩2 (+)]" more:sum.union_disjoint) auto
    also have "...  = (∑x=0..<m. f (x mod m)^2) + (∑x=0..<?n-m. f x^2) + (∑x=?n-m..<m. f x^2)"
      using assms(2,3)
      by (intro_cong "[σ⇩2 (+)]" more: sum.reindex_bij_betw bij_betwI[where g="(λx. x+m)"])
       (auto simp add:le_mod_geq)
    also have "... = (∑x=0..<m. f x^2) + (∑x=0..<?n-m. f x^2) + (∑x=?n-m..<m. f x^2)"
      by (intro sum.cong arg_cong2[where f="(+)"]) auto
    also have "... = (∑x=0..<m. f x^2) + ((∑x=0..<?n-m. f x^2) + (∑x=?n-m..<m. f x^2))"
      by simp
    also have "... = (∑x=0..<m. f x^2) + (∑x∈{0..<?n-m}∪{?n-m..<m}. f x^2)"
      by (intro sum.union_disjoint[symmetric] arg_cong2[where f="(+)"]) auto
    also have "... = (∑x<m. f x^2) + (∑x<m. f x^2)"
      using assms(2,3) by (intro arg_cong2[where f="(+)"] sum.cong) auto
    also have " ... = 2 * H.g_norm f^2"
      unfolding mult_2 H.g_norm_sq H.g_inner_def by (simp add:graph_of_def power2_eq_square)
    finally have 2:"?L1 = 2 * H.g_norm f^2" by simp

    have "?L2 = (∑x∈{..<m}∪{m..<?n}. f (x mod m))^2/G.n + (∑x=?n-m..<m. f x^2)"
      unfolding G.g_inner_def f'_def using assms(2,3)
      by (intro_cong "[σ⇩2 (+), σ⇩2 (/), σ⇩2 (power)]" more: sum.cong abs_of_nonneg sum_nonneg)
       (auto simp add:graph_of_def)
    also have "...=((∑x<m. f (x mod m))+(∑x=m..<?n. f (x mod m)))^2/G.n + (∑x=?n-m..<m. f x^2)"
      by (intro_cong "[σ⇩2 (+), σ⇩2 (/), σ⇩2 (power)]" more:sum.union_disjoint) auto
    also have "...=((∑x<m. f (x mod m))+(∑x=0..<?n-m. f x))^2/G.n + (∑x=?n-m..<m. f x^2)"
      using assms(2,3) by (intro_cong "[σ⇩2 (+), σ⇩2 (/), σ⇩2 (power)]"
          more:sum.reindex_bij_betw bij_betwI[where g="(λx. x+m)"]) (auto simp add:le_mod_geq)
    also have "...=(H.g_inner f (λ_. 1) +(∑x<?n-m. f x))^2/G.n + (∑x=?n-m..<m. f x^2)"
      unfolding H.g_inner_def
      by (intro_cong "[σ⇩2 (+), σ⇩2 (/), σ⇩2 (power)]" more: sum.cong) (auto simp:graph_of_def)
    also have "...=(∑x<?n-m. f x)^2/G.n + (∑x=?n-m..<m. f x^2)"
      unfolding that by simp
    also have "...≤ (∑x<?n-m. ¦f x¦ * ¦1¦)^2/G.n + (∑x=?n-m..<m. f x^2)"
      by (intro add_mono divide_right_mono iffD1[OF abs_le_square_iff]) auto
    also have "... ≤ (L2_set f {..<?n-m} * L2_set (λ_. 1) {..<?n-m})^2/G.n + (∑x=?n-m..<m. f x^2)"
      by (intro add_mono divide_right_mono power_mono L2_set_mult_ineq sum_nonneg) auto
    also have "... = ((∑x <?n-m. f x^2) * (?n-m))/G.n + (∑x=?n-m..<m. f x^2)"
      unfolding power_mult_distrib L2_set_def real_sqrt_mult
      by (intro_cong "[σ⇩2 (+), σ⇩2 (/),σ⇩2 (*)]" more:real_sqrt_pow2 sum_nonneg) auto
    also have "... = (∑x <?n-m. f x^2) * ((?n-m)/?n) + (∑x=?n-m..<m. f x^2)"
      unfolding n_eq by simp
    also have "... ≤ (∑x <?n-m. f x^2) * 1 + (∑x=?n-m..<m. f x^2)"
      using assms(3) n_gt_1 by (intro mult_left_mono add_mono sum_nonneg) auto
    also have "... = (∑x∈{..<?n-m}∪{?n-m..<m}. f x^2)"
      unfolding mult_1_right by (intro sum.union_disjoint[symmetric]) auto
    also have "... = H.g_norm f^2"
      using assms(2,3) unfolding H.g_norm_sq H.g_inner_def
      by (intro sum.cong) (auto simp add:graph_of_def power2_eq_square)
    finally have 3:"?L2 ≤ H.g_norm f^2" by simp

    have "?L = ¦∑(u, v)∈#edges ?H. f v * f u¦"
      unfolding edges_def arc_to_ends_def sum_unfold_sum_mset
      by (simp add:image_mset.compositionality comp_def del:see_compress.simps)
    also have "...=¦(∑x ∈# edges ?G.f(snd x mod m)*f(fst x mod m))+(∑x=?n-m..<m.?d*(f x^2))¦"
      unfolding edges_of_compress[OF assms(2,3)]  sum_unfold_sum_mset
      by (simp add:image_mset.compositionality sum_mset_repeat comp_def
          case_prod_beta power2_eq_square del:see_compress.simps)
    also have "...=¦(∑(u,v) ∈# edges ?G.f(u mod m)*f(v mod m))+(∑x=?n-m..<m.?d*(f x^2))¦"
      by (intro_cong "[σ⇩1 abs, σ⇩2 (+), σ⇩1 sum_mset]" more:image_mset_cong)
       (simp_all add:case_prod_beta)
    also have "... ≤ ¦∑(u,v) ∈# edges ?G.f(u mod m)*f(v mod m)¦+¦∑x=?n-m..<m.?d*(f x^2)¦ "
      by (intro abs_triangle_ineq)
    also have "... = ?d * (¦∑(u,v) ∈# edges ?G.f(v mod m)*f(u mod m)¦/G.d+¦∑x=?n-m..<m.(f x^2)¦)"
      unfolding d_eq using G.d_gt_0
      by (simp add:divide_simps ac_simps sum_distrib_left[symmetric] abs_mult)
    also have "... = ?d * (¦G.g_inner f' (G.g_step f')¦ + ¦∑x=?n-m..<m. f x^2¦)"
      unfolding G.g_inner_step_eq sum_unfold_sum_mset edges_def arc_to_ends_def f'_def
      by (simp add:image_mset.compositionality comp_def del:see_compress.simps)
    also have "...≤ ?d * ((G.Λ⇩a * G.g_norm f'^2 + (1-G.Λ⇩a)*G.g_inner f' (λ_.1)^2/ G.n)
      + ¦∑x=?n-m..<m. f x^2¦)"
      by (intro add_mono G.expansionD3 mult_left_mono) auto
    also have "... = ?d * (G.Λ⇩a * ?L1 + (1 - G.Λ⇩a) * ?L2)"
      by (simp add:algebra_simps)
    also have "... ≤ ?d * (G.Λ⇩a * (2 * H.g_norm f^2) + (1-G.Λ⇩a) * H.g_norm f^2)"
      unfolding 2 using G.Λ_ge_0 G.Λ_le_1 by (intro mult_left_mono add_mono 3) auto
    also have "... = ?R"
      unfolding d_eq[symmetric] by (simp add:algebra_simps)
    finally show ?thesis by simp
  qed

  hence "H.Λ⇩a ≤ (G.d*G.Λ⇩a+G.d)/H.d"
    using G.d_gt_0 G.Λ_ge_0 by (intro H.expander_intro) (auto simp del:see_compress.simps)
  also have "... = (see_degree e * G.Λ⇩a + see_degree e) / (2* see_degree e)"
    unfolding d_eq[symmetric] regular_graph_degree_eq_see_degree[OF H.regular_graph_axioms]
    by simp
  also have "... = G.Λ⇩a/2 + 1/2"
    using 1 by (simp add:field_simps)
  also have "... ≤ Λ⇩a/2 + 1/2"
    using assms(1) unfolding is_expander_def by simp
  finally have "H.Λ⇩a ≤ Λ⇩a/2 + 1/2" by simp
  thus ?thesis unfolding is_expander_def using 0 by simp
qed

text ‹The graph power of a strongly explicit expander graph is itself a strongly explicit expander
graph.›

fun to_digits :: "nat ⇒ nat ⇒ nat ⇒ nat list"
  where
    "to_digits _ 0 _ = []" |
    "to_digits b (Suc l) k = (k mod b)# to_digits b l (k div b)"

fun from_digits :: "nat ⇒ nat list ⇒ nat"
  where
    "from_digits b [] = 0" |
    "from_digits b (x#xs) = x + b * from_digits b xs"

lemma to_from_digits:
  assumes "length xs = n" "set xs ⊆ {..<b}"
  shows "to_digits b n (from_digits b xs) = xs"
proof -
  have "to_digits b (length xs) (from_digits b xs) = xs"
    using assms(2) by (induction xs, auto)
  thus ?thesis unfolding assms(1) by auto
qed

lemma from_digits_range:
  assumes "length xs = n" "set xs ⊆ {..<b}"
  shows "from_digits b xs < b^n"
proof (cases "b > 0")
  case True
  have "from_digits b xs ≤ b^length xs - 1"
    using assms(2)
  proof (induction xs)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    have "from_digits b (a # xs) =  a + b * from_digits b xs"
      by simp
    also have "... ≤ (b-1) + b * from_digits b xs"
      using Cons by (intro add_mono) auto
    also have "... ≤ (b-1) + b * (b^length xs-1)"
      using Cons(2) by (intro add_mono mult_left_mono Cons(1)) auto
    also have "... = b^length (a#xs) - 1"
      using True by (simp add:algebra_simps)
    finally show "from_digits b (a # xs) ≤ b^length (a#xs) - 1" by simp
  qed
  also have "... < b^n"
    using True assms(1) by simp
  finally show ?thesis by simp
next
  case False
  hence "b = 0" by simp
  hence "xs = []"
    using assms(2) by simp
  thus ?thesis using assms(1) by simp
qed

lemma from_digits_inj:
  "inj_on (from_digits b) {xs. set xs ⊆ {..<b} ∧ length xs = n}"
  by (intro inj_on_inverseI[where g="to_digits b n"] to_from_digits) auto

fun see_power :: "nat ⇒ strongly_explicit_expander ⇒ strongly_explicit_expander"
  where "see_power l e =
    ⦇ see_size = see_size e, see_degree = see_degree e^l
    , see_step = (λk v. foldl (λy x. see_step e x y) v (to_digits (see_degree e) l k)) ⦈"

lemma graph_power_iso_see_power:
  assumes "fin_digraph (graph_of e)"
  shows "digraph_iso (graph_power (graph_of e) n) (graph_of (see_power n e))"
proof -
  let ?G = "graph_of e"
  let ?P = "graph_power (graph_of e) n"
  let ?H = "graph_of (see_power n e)"
  let ?d = "see_degree e"
  let ?n = "see_size e"

  interpret fin_digraph "(graph_of e)"
    using assms by auto

  interpret P:fin_digraph ?P
    by (intro graph_power_fin)

  define φ where
    "φ = (λ(u,v). Arc u (arc_walk_head ?G (u, v)) (from_digits ?d (map arc_label v)))"

  define iso where "iso =
    ⦇ iso_verts = id, iso_arcs = φ, iso_head = arc_head, iso_tail = arc_tail ⦈"

  have "xs = ys" if "length xs = length ys" "map arc_label xs = map arc_label ys"
    "is_arc_walk ?G u xs ∧ is_arc_walk ?G u ys ∧ u ∈ verts ?G" for xs ys u
    using that
  proof (induction xs ys arbitrary: u rule:list_induct2)
    case Nil
    then show ?case by simp
  next
    case (Cons x xs y ys)
    have "arc_label x = arc_label y" "u ∈ verts ?G" "x ∈ out_arcs ?G u" "y ∈ out_arcs ?G u"
      using Cons by auto
    hence a:"x = y"
      unfolding graph_of_def by auto
    moreover have "head ?G y ∈ verts ?G" using Cons by auto
    ultimately have "xs = ys"
      using Cons(3,4) by (intro Cons(2)[of "head ?G y"]) auto
    thus ?case using a by auto
  qed
  hence 5:"inj_on (λ(u,v). (u, map arc_label v)) (arc_walks ?G n)"
    unfolding arc_walks_def by (intro inj_onI) auto
  have 3:"set (map arc_label (snd xs)) ⊆ {..<?d}" "length (snd xs) = n"
    if "xs ∈ arc_walks ?G n" for xs
  proof -
    show "length (snd xs) = n"
      using subsetD[OF is_arc_walk_set[where G="?G"]] that unfolding arc_walks_def by auto
    have "set (snd xs) ⊆ arcs ?G"
      using subsetD[OF is_arc_walk_set[where G="?G"]] that unfolding arc_walks_def by auto
    thus "set (map arc_label (snd xs)) ⊆ {..<?d}"
      unfolding graph_of_def by auto
  qed

  hence 7:"inj_on (λ(u,v). (u, from_digits ?d (map arc_label v))) (arc_walks ?G n)"
    using inj_onD[OF 5] inj_onD[OF from_digits_inj] by (intro inj_onI) auto

  hence "inj_on φ (arc_walks ?G n)"
    unfolding inj_on_def φ_def by auto
  hence "inj_on (iso_arcs iso) (arcs (graph_power (graph_of e) n))"
    unfolding iso_def graph_power_def by simp
  moreover have "inj_on (iso_verts iso) (verts (graph_power (graph_of e) n))"
    unfolding iso_def by simp
  moreover have
    "iso_verts iso (tail ?P a) = iso_tail iso (iso_arcs iso a)"
    "iso_verts iso (head ?P a) = iso_head iso (iso_arcs iso a)" if "a ∈ arcs ?P" for a
    unfolding φ_def iso_def graph_power_def by (simp_all add:case_prod_beta)
  ultimately have 0:"P.digraph_isomorphism iso"
    unfolding P.digraph_isomorphism_def by (intro conjI ballI P.wf_digraph_axioms) auto

  have "card((λ(u, v).(u,from_digits ?d (map arc_label v)))`arc_walks ?G n)=card(arc_walks ?G n)"
    by (intro card_image 7)
  also have "... = ?d^n * ?n"
    by (intro card_arc_walks_see fin_digraph_axioms)
  finally have "card((λ(u, v).(u,from_digits ?d (map arc_label v)))`arc_walks ?G n) = ?d^n * ?n"
    by simp
  moreover have "fst v ∈ {..<?n}" if "v ∈ arc_walks ?G n" for v
    using that unfolding arc_walks_def graph_of_def by auto
  moreover have "from_digits ?d (map arc_label (snd v)) < ?d ^ n" if "v ∈ arc_walks ?G n" for v
    using 3[OF that] by (intro from_digits_range) auto

  ultimately have 2:
    "{..<?n}×{..<?d^n} = (λ(u,v). (u, from_digits ?d (map arc_label v))) ` arc_walks ?G n"
    by (intro card_subset_eq[symmetric]) auto

  have "foldl (λy x. see_step e x y) u (map arc_label w) = arc_walk_head ?G (u,w)"
    if "is_arc_walk ?G u w" "u ∈ verts ?G" for u w
    using that
  proof (induction w rule:rev_induct)
    case Nil
    then show ?case by (simp add:arc_walk_head_def)
  next
    case (snoc x xs)
    hence "x ∈ arcs ?G" by (simp add:is_arc_walk_snoc)
    hence "see_step e (arc_label x) (tail ?G x) = (head ?G x)"
      unfolding graph_of_def by (auto simp add:image_iff)
    also have "... = arc_walk_head (graph_of e) (u, xs @ [x])"
      unfolding arc_walk_head_def by simp
    finally have "see_step e (arc_label x) (tail ?G x) =  arc_walk_head (graph_of e) (u, xs @ [x])"
      by simp
    thus ?case using snoc by (simp add:is_arc_walk_snoc)
  qed

  hence 4: "foldl (λy x. see_step e x y) (fst x) (map arc_label (snd x)) = arc_walk_head ?G x"
    if "x ∈ arc_walks (graph_of e) n" for x
    using that unfolding arc_walks_def by (simp add:case_prod_beta)

  have "arcs ?H = (λ(v, i). Arc v (see_step (see_power n e) i v) i) ` ({..<?n}×{..<?d^n})"
    unfolding graph_of_def by simp
  also have "... = (λ(v,w). Arc v (see_step (see_power n e) (from_digits ?d (map arc_label w)) v)
    (from_digits ?d (map arc_label w))) ` arc_walks ?G n"
    unfolding 2 image_image by (simp del:see_power.simps add: case_prod_beta comp_def)
  also have "... = (λ(v,w). Arc v (foldl (λy x. see_step e x y) v (map arc_label w))
    (from_digits ?d (map arc_label w))) ` arc_walks ?G n"
    using 3  by (intro image_cong refl) (simp add:case_prod_beta to_from_digits)
  also have "... = φ ` arc_walks ?G n"
    unfolding φ_def using 4 by (simp add:case_prod_beta)
  also have "... = iso_arcs iso ` arcs ?P"
    unfolding iso_def graph_power_def by simp
  finally have "arcs ?H = iso_arcs iso ` arcs ?P"
    by simp
  moreover have "verts ?H = iso_verts iso ` verts ?P"
    unfolding iso_def graph_of_def graph_power_def by simp
  moreover have "tail ?H = iso_tail iso"
    unfolding iso_def graph_of_def by simp
  moreover have "head ?H = iso_head iso"
    unfolding iso_def graph_of_def by simp
  ultimately have 1:"?H = app_iso iso ?P"
    unfolding app_iso_def
    by (intro pre_digraph.equality) (simp_all del:see_power.simps)

  show ?thesis
    using 0 1 unfolding digraph_iso_def by auto
qed

lemma see_power:
  assumes "is_expander e Λ⇩a"
  shows "is_expander (see_power n e) (Λ⇩a^n)"
proof -
  interpret G: "regular_graph" "graph_of e"
    using assms unfolding is_expander_def by auto

  interpret H:"regular_graph" "graph_power (graph_of e) n"
    by (intro G.graph_power_regular)

  have 0:"digraph_iso (graph_power (graph_of e) n) (graph_of (see_power n e))"
    by (intro graph_power_iso_see_power) auto

  have "regular_graph.Λ⇩a (graph_of (see_power n e)) = H.Λ⇩a"
    using H.regular_graph_iso_expansion[OF 0] by auto
  also have "... ≤ G.Λ⇩a^n"
    by (intro G.graph_power_expansion)
  also have "... ≤ Λ⇩a^n"
    using assms(1) unfolding is_expander_def
    by (intro power_mono G.Λ_ge_0)  auto
  finally have "regular_graph.Λ⇩a (graph_of (see_power n e)) ≤ Λ⇩a^n"
    by simp
  moreover have "regular_graph (graph_of (see_power n e))"
    using H.regular_graph_iso[OF 0] by auto
  ultimately show ?thesis
    unfolding is_expander_def by auto
qed

text ‹The Margulis Construction from Section~\ref{sec:margulis} is a strongly explicit expander
graph.›

definition mgg_vert :: "nat ⇒ nat ⇒ (int × int)"
  where "mgg_vert n x = (x mod n, x div n)"

definition mgg_vert_inv :: "nat ⇒ (int × int) ⇒ nat"
  where "mgg_vert_inv n x = nat (fst x) + nat (snd x) * n"

lemma mgg_vert_inv:
  assumes "n > 0" "x ∈ {0..<int n}×{0..<int n}"
  shows "mgg_vert n (mgg_vert_inv n x) = x"
  using assms unfolding mgg_vert_def mgg_vert_inv_def by auto

definition mgg_arc :: "nat ⇒ (nat × int)"
  where "mgg_arc k = (k mod 4, if k ≥ 4 then (-1) else 1)"

definition mgg_arc_inv :: "(nat × int) ⇒ nat"
  where "mgg_arc_inv x = (nat (fst x) + 4 * of_bool (snd x < 0))"

lemma mgg_arc_inv:
  assumes  "x ∈ {..<4}×{-1,1}"
  shows "mgg_arc (mgg_arc_inv x) = x"
  using assms unfolding mgg_arc_def mgg_arc_inv_def by auto

definition see_mgg :: "nat ⇒ strongly_explicit_expander" where
  "see_mgg n = ⦇ see_size = n^2, see_degree = 8,
    see_step = (λi v. mgg_vert_inv n (mgg_graph_step n (mgg_vert n v) (mgg_arc i))) ⦈"

lemma mgg_graph_iso:
  assumes "n > 0"
  shows "digraph_iso (mgg_graph n) (graph_of (see_mgg n))"
proof -
  let ?v = "mgg_vert n" let ?vi = "mgg_vert_inv n"
  let ?a = "mgg_arc" let ?ai = "mgg_arc_inv"
  let ?G = "graph_of (see_mgg n)" let ?s = "mgg_graph_step n"

  define φ where "φ a = Arc (?vi (arc_tail a)) (?vi (arc_head a)) (?ai (arc_label a))" for a

  define iso where "iso =
    ⦇ iso_verts = mgg_vert_inv n, iso_arcs = φ, iso_head = arc_head, iso_tail = arc_tail ⦈"

  interpret M: margulis_gaber_galil n
    using assms by unfold_locales

  have inj_vi: "inj_on ?vi (verts M.G)"
    unfolding mgg_graph_def mgg_vert_inv_def
    by (intro inj_on_inverseI[where g="mgg_vert n"]) (auto simp:mgg_vert_def)
  have "card (?vi ` verts M.G) = card (verts M.G)"
    by (intro card_image inj_vi)
  moreover have "card (verts M.G) = n⇧2"
    unfolding mgg_graph_def by (auto simp:power2_eq_square)
  moreover have "mgg_vert_inv n x ∈ {..<n⇧2}" if "x ∈ verts M.G" for x
  proof -
    have "mgg_vert_inv n x = nat (fst x) + nat (snd x) * n"
      unfolding mgg_vert_inv_def by simp
    also have "... ≤ (n-1) + (n-1) * n"
      using that unfolding mgg_graph_def
      by (intro add_mono mult_right_mono) auto
    also have "... = n * n - 1" using assms by (simp add:algebra_simps)
    also have "... < n^2"
      using assms by (simp add: power2_eq_square)
    finally have "mgg_vert_inv n x < n^2" by simp
    thus ?thesis by simp
  qed
  ultimately have 0:"{..<n^2} = ?vi ` verts M.G"
    by (intro card_subset_eq[symmetric] image_subsetI) auto

  have inj_ai: "inj_on ?ai ({..<4} × {-1,1})"
    unfolding mgg_arc_inv_def by (intro inj_onI) auto
  have "card (?ai ` ({..<4} × {- 1, 1})) = card ({..<4::nat} × {-1,1::int})"
    by (intro card_image inj_ai)
  hence 1:"{..<8} = ?ai ` ({..<4} × {-1,1})"
    by (intro card_subset_eq[symmetric] image_subsetI) (auto simp add:mgg_arc_inv_def)

  have "arcs ?G = (λ(v, i). Arc v (?vi (?s (?v v) (?a i))) i) ` ({..<n⇧2} × {..<8})"
    by (simp add:see_mgg_def graph_of_def)
  also have "... = (λ(v, i). Arc (?vi v) (?vi (?s (?v (?vi v)) (?a (?ai i)))) (?ai i)) `
    (verts M.G × ({..<4} × {-1,1}))"
    unfolding 0 1 mgg_arc_inv by (auto simp add:image_iff)
  also have "... = (λ(v, i). Arc (?vi v) (?vi (?s v i)) (?ai i)) ` (verts M.G × ({..<4} × {-1,1}))"
    using mgg_vert_inv[OF assms] mgg_arc_inv unfolding mgg_graph_def by (intro image_cong) auto
  also have "... = (φ ∘ (λ(t, l). Arc t (?s t l) l)) ` (verts M.G × ({..<4} × {-1,1}))"
    unfolding φ_def by (intro image_cong refl) ( simp add:comp_def case_prod_beta )
  also have "... = φ ` arcs M.G"
    unfolding mgg_graph_def by (simp add:image_image)
  also have "... = iso_arcs iso ` arcs (mgg_graph n)"
    unfolding iso_def by simp
  finally have "arcs (graph_of (see_mgg n)) = iso_arcs iso ` arcs (mgg_graph n)"
    by simp
  moreover have "verts ?G = iso_verts iso ` verts (mgg_graph n)"
    unfolding iso_def graph_of_def see_mgg_def using 0 by simp
  moreover have "tail ?G = iso_tail iso"
    unfolding iso_def graph_of_def by simp
  moreover have "head ?G = iso_head iso"
    unfolding iso_def graph_of_def by simp
  ultimately have 0:"?G = app_iso iso (mgg_graph n)"
    unfolding app_iso_def   by (intro pre_digraph.equality) simp_all

  have "inj_on φ (arcs M.G)"
  proof (rule inj_onI)
    fix x y assume assms': "x ∈ arcs M.G" "y ∈ arcs M.G" "φ x = φ y"

    have "?vi (head M.G x) = ?vi (head M.G y)"
      using assms'(3) unfolding φ_def mgg_graph_def by auto
    hence "head M.G x = head M.G y"
      using assms'(1,2) by (intro inj_onD[OF inj_vi]) auto
    hence "arc_head x = arc_head y"
      unfolding mgg_graph_def by simp

    moreover have "?vi (tail M.G x) = ?vi (tail M.G y)"
      using assms'(3) unfolding φ_def mgg_graph_def by auto
    hence "tail M.G x = tail M.G y"
      using assms'(1,2) by (intro inj_onD[OF inj_vi]) auto
    hence "arc_tail x = arc_tail y"
      unfolding mgg_graph_def by simp

    moreover have "?ai (arc_label x) = ?ai (arc_label y)"
      using assms'(3) unfolding φ_def by auto
    hence "arc_label x = arc_label y"
      using assms'(1,2) unfolding mgg_graph_def
      by (intro inj_onD[OF inj_ai]) (auto simp del:mgg_graph_step.simps)

    ultimately show "x = y"
      by (intro arc.expand) auto
  qed
  hence "inj_on (iso_arcs iso) (arcs M.G)"
    unfolding iso_def by simp
  moreover have "inj_on (iso_verts iso) (verts M.G)"
    using inj_vi unfolding iso_def by simp
  moreover have
    "iso_verts iso (tail M.G a) = iso_tail iso (iso_arcs iso a)"
    "iso_verts iso (head M.G a) = iso_head iso (iso_arcs iso a)"  if "a ∈ arcs M.G" for a
    unfolding iso_def φ_def mgg_graph_def by auto
  ultimately have 1:"M.digraph_isomorphism iso"
    unfolding M.digraph_isomorphism_def by (intro conjI ballI M.wf_digraph_axioms) auto

  show ?thesis unfolding digraph_iso_def using 0 1 by auto
qed

lemma see_mgg:
  assumes "n > 0"
  shows "is_expander (see_mgg n) (5* sqrt 2 / 8)"
proof -
  interpret G: "margulis_gaber_galil" "n"
    using assms by unfold_locales auto

  note 0 = mgg_graph_iso[OF assms]

  have "regular_graph.Λ⇩a (graph_of (see_mgg n)) = G.Λ⇩a"
    using G.regular_graph_iso_expansion[OF 0] by auto
  also have "... ≤ (5* sqrt 2 / 8)"
    using G.mgg_numerical_radius unfolding G.MGG_bound_def by simp
  finally have "regular_graph.Λ⇩a (graph_of (see_mgg n)) ≤ (5* sqrt 2 / 8)"
    by simp
  moreover have "regular_graph (graph_of (see_mgg n))"
    using G.regular_graph_iso[OF 0] by auto
  ultimately show ?thesis
    unfolding is_expander_def by auto
qed

text ‹Using all of the above it is possible to construct strongly explicit expanders of every
size and spectral gap with asymptotically optimal degree.›

definition see_standard_aux
  where "see_standard_aux n = see_compress n (see_mgg (nat ⌈sqrt n⌉))"

lemma see_standard_aux:
  assumes "n > 0"
  shows
    "is_expander (see_standard_aux n) ((8+5 * sqrt 2) / 16)" (is "?A")
    "see_degree (see_standard_aux n) = 16" (is "?B")
    "see_size (see_standard_aux n) = n" (is "?C")
proof -
  have 2:"sqrt (real n) > -1"
    by (rule less_le_trans[where y="0"]) auto

  have 0:"real n ≤ of_int ⌈sqrt (real n)⌉^2"
    by (simp add:sqrt_le_D)

  consider (a) "n = 1" | (b) "n ≥ 2 ∧ n ≤ 4" | (c) "n ≥ 5 ∧ n ≤ 9" | (d) "n ≥ 10"
    using assms by linarith
  hence 1:"of_int ⌈sqrt (real n)⌉^2 ≤ 2 * real n"
  proof (cases)
    case a then show ?thesis by simp
  next
    case b
    hence "real_of_int ⌈sqrt (real n)⌉^2 ≤ of_int ⌈sqrt (real 4)⌉^2"
      using 2
      by (intro power_mono iffD2[OF of_int_le_iff] ceiling_mono iffD2[OF real_sqrt_le_iff]) auto
    also have "... = 2 * real 2" by simp
    also have "... ≤ 2 * real n"
      using b by (intro mult_left_mono) auto
    finally show ?thesis by simp
  next
    case c
    hence "real_of_int ⌈sqrt (real n)⌉^2 ≤ of_int ⌈sqrt (real 9)⌉^2"
      using 2
      by (intro power_mono iffD2[OF of_int_le_iff] ceiling_mono iffD2[OF real_sqrt_le_iff]) auto
    also have "... = 9" by simp
    also have "... ≤ 2 * real 5" by simp
    also have "... ≤ 2 * real n"
      using c by (intro mult_left_mono) auto
    finally show ?thesis by simp
  next
    case d
    have "real_of_int ⌈sqrt (real n)⌉^2 ≤ (sqrt (real n)+1)^2"
      using 2 by (intro power_mono) auto
    also have "... = real n + sqrt (4 * real n + 0) + 1"
      using real_sqrt_pow2 by (simp add:power2_eq_square algebra_simps real_sqrt_mult)
    also have "... ≤ real n + sqrt (4 * real n + (real n * (real n - 6) + 1)) + 1"
      using d by (intro add_mono iffD2[OF real_sqrt_le_iff]) auto
    also have "... = real n + sqrt ((real n-1)^2) + 1"
      by (intro_cong "[σ⇩2 (+), σ⇩1 sqrt]") (auto simp add:power2_eq_square algebra_simps)
    also have "... = 2 * real n"
      using d by simp
    finally show ?thesis by simp
  qed

  have "nat ⌈sqrt (real n)⌉^2 ∈ {n..2*n}"
    by (simp add: approximation_preproc_nat(13) sqrt_le_D 1)
  hence "see_size (see_mgg (nat ⌈sqrt (real n)⌉)) ∈ {n..2*n}"
    by (simp add:see_mgg_def)
  moreover have "sqrt (real n) > 0" using assms by simp
  hence "0 < nat ⌈sqrt (real n)⌉" by simp
  ultimately have "is_expander (see_standard_aux n) ((5* sqrt 2 / 8)/2 + 1/2)"
    unfolding see_standard_aux_def by (intro see_compress see_mgg) auto
  thus ?A
    by (auto simp add:field_simps)
  show ?B
    unfolding see_standard_aux_def by (simp add:see_mgg_def)
  show ?C
    unfolding see_standard_aux_def by simp
qed

definition see_standard_power
  where "see_standard_power x  = (if x ≤ (0::real) then 0 else nat ⌈ln x / ln 0.95⌉)"

lemma see_standard_power:
  assumes "Λ⇩a > 0"
  shows "0.95^(see_standard_power Λ⇩a) ≤ Λ⇩a" (is "?L ≤ ?R")
proof (cases "Λ⇩a ≤ 1")
  case True
  hence "0 ≤ ln Λ⇩a / ln 0.95"
    using assms by (intro divide_nonpos_neg) auto
  hence 1:"0 ≤ ⌈ln Λ⇩a / ln 0.95⌉"
    by simp
  have "?L = 0.95^nat ⌈ln Λ⇩a / ln 0.95⌉"
    using assms unfolding see_standard_power_def by simp
  also have "... = 0.95 powr (of_nat (nat (⌈ln Λ⇩a / ln 0.95⌉)))"
    by (subst powr_realpow) auto
  also have "... = 0.95 powr ⌈ln Λ⇩a / ln 0.95⌉"
    using 1 by (subst of_nat_nat) auto
  also have "... ≤ 0.95 powr (ln Λ⇩a / ln 0.95)"
    by (intro powr_mono_rev) auto
  also have "... = ?R"
    using assms unfolding powr_def by simp
  finally show ?thesis by simp
next
  case False
  hence "ln Λ⇩a / ln 0.95 ≤ 0"
    by (subst neg_divide_le_eq) auto
  hence "see_standard_power Λ⇩a = 0"
    unfolding see_standard_power_def by simp
  then show ?thesis using False by simp
qed

lemma see_standard_power_eval[code]:
  "see_standard_power x = (if x ≤ 0 ∨ x ≥ 1 then 0 else (1+see_standard_power (x/0.95)))"
proof (cases "x ≤ 0 ∨ x ≥ 1")
  case True
  have "ln x / ln (19 / 20) ≤ 0" if "x > 0"
  proof -
    have "x ≥ 1" using that True by auto
    thus ?thesis
      by (intro divide_nonneg_neg) auto
  qed
  then show ?thesis using True unfolding see_standard_power_def by simp
next
  case False
  hence x_range: "x > 0" "x < 1" by auto

  have "ln (x / 0.95) < ln (1/0.95)"
    using x_range by (intro iffD2[OF ln_less_cancel_iff]) auto
  also have "... = - ln 0.95"
    by (subst ln_div) auto
  finally have "ln (x / 0.95) < - ln 0.95" by simp
  hence 0: "-1 < ln (x / 0.95) / ln 0.95"
    by (subst neg_less_divide_eq)  auto

  have "see_standard_power x = nat ⌈ln x / ln 0.95⌉"
    using x_range unfolding see_standard_power_def by simp
  also have "... = nat ⌈ln (x/0.95) / ln 0.95 + 1⌉"
    by (subst ln_divide_pos[OF x_range(1)]) (simp_all add:field_simps )
  also have "... = nat (⌈ln (x/0.95) / ln 0.95⌉+1)"
    by (intro arg_cong[where f="nat"]) simp
  also have "... = 1 + nat ⌈ln (x/0.95) / ln 0.95⌉"
    using 0 by (subst nat_add_distrib) auto
  also have "... = (if x ≤ 0 ∨ 1 ≤ x then 0 else 1 + see_standard_power (x/0.95))"
    unfolding see_standard_power_def using x_range by auto
  finally show ?thesis by simp
qed

definition see_standard :: "nat ⇒ real ⇒ strongly_explicit_expander"
  where "see_standard n Λ⇩a = see_power (see_standard_power Λ⇩a) (see_standard_aux n)"

theorem see_standard:
  assumes "n > 0" "Λ⇩a > 0"
  shows "is_expander (see_standard n Λ⇩a) Λ⇩a"
    and "see_size (see_standard n Λ⇩a) = n"
    and "see_degree (see_standard n Λ⇩a) = 16 ^ (nat ⌈ln Λ⇩a / ln 0.95⌉)" (is "?C")
proof -
  have 0:"is_expander (see_standard_aux n) 0.95"
    by (intro see_standard_aux(1)[OF assms(1)] is_expander_mono[where a="(8+5 * sqrt 2) / 16"])
     (approximation 10)

  show "is_expander (see_standard n Λ⇩a) Λ⇩a"
    unfolding see_standard_def
    by (intro see_power 0 is_expander_mono[where a="0.95^(see_standard_power Λ⇩a)"]
      see_standard_power assms(2))
  show "see_size (see_standard n Λ⇩a) = n"
    unfolding see_standard_def using see_standard_aux[OF assms(1)] by simp

  have "see_degree (see_standard n Λ⇩a) = 16 ^ (see_standard_power Λ⇩a)"
    unfolding see_standard_def using see_standard_aux[OF assms(1)] by simp
  also have "... = 16 ^ (nat ⌈ln Λ⇩a / ln 0.95⌉)"
    unfolding see_standard_power_def using assms(2) by simp
  finally show ?C by simp
qed

fun see_sample_walk :: "strongly_explicit_expander ⇒ nat ⇒ nat ⇒ nat list"
  where
    "see_sample_walk e 0 x = [x]" |
    "see_sample_walk e (Suc l) x = (let w = see_sample_walk e l (x div (see_degree e)) in
      w@[see_step e (x mod (see_degree e)) (last w)])"

theorem see_sample_walk:
  fixes e l
  assumes "fin_digraph (graph_of e)"
  defines "r ≡ see_size e * see_degree e ^l"
  shows "{# see_sample_walk e l k. k ∈# mset_set {..<r} #} = walks' (graph_of e) l"
  unfolding r_def
proof (induction l)
  case 0
  then show ?case unfolding graph_of_def by simp
next
  case (Suc l)
  interpret fin_digraph "graph_of e"
    using assms(1) by auto

  let ?d = "see_degree e"
  let ?n = "see_size e"
  let ?w = "see_sample_walk e"
  let ?G = "graph_of e"
  define r where "r = ?n * ?d^l"

  have 1: "{i * ?d..<(i + 1) * ?d} ∩ {j * ?d..<(j + 1) * ?d} = {}" if "i ≠ j" for i j
    using that index_div_eq by blast

  have 2:"vertices_from ?G x = {# see_step e i x. i ∈# mset_set {..<?d}#}" (is "?L = ?R")
    if "x ∈ verts ?G" for x
  proof -
    have "x < ?n"
      using that unfolding graph_of_def by simp
    hence 1:"out_arcs ?G x = (λi. Arc x (see_step e i x) i) ` {..<?d}"
      unfolding out_arcs_def graph_of_def by (auto simp add:image_iff set_eq_iff)

    have "?L = {# arc_head a. a ∈# mset_set (out_arcs ?G x) #}"
      unfolding verts_from_alt by (simp add:graph_of_def)
    also have "... = {# arc_head a. a ∈# {# Arc x (see_step e i x) i. i ∈# mset_set {..<?d}#}#} "
      unfolding 1
      by (intro arg_cong2[where f= "image_mset"] image_mset_mset_set[symmetric] inj_onI) auto
    also have "... = ?R"
      by (simp add:image_mset.compositionality comp_def)
    finally show ?thesis by simp
  qed

  have "card (⋃w<r. {w * ?d..<(w + 1) *?d}) = (∑w < r. card {w * ?d..<(w + 1) *?d})"
    using 1 by (intro card_UN_disjoint) auto
  also have "... = r * ?d" by simp
  finally have "card (⋃w<r. {w * ?d..<(w + 1) *?d}) = card {..<?d * r}" by simp
  moreover  have "?d + z * ?d ≤ ?d * r" if "z < r" for z
  proof -
    have "?d + z * ?d = ?d * (z + 1)" by simp
    also have "... ≤ ?d * r"
      using that by (intro mult_left_mono) auto
    finally show ?thesis by simp
  qed
  ultimately have 0: "(⋃w<r. {w * ?d..<(w + 1) *?d}) = {..<?d * r}"
    using order_less_le_trans by (intro card_subset_eq subsetI) auto

  have "{# ?w (l+1) k. k ∈# mset_set {..<?n * ?d^(l+1)} #} = {#?w (l+1) k. k ∈# mset_set {..<?d * r}#}"
    unfolding r_def by (simp add:ac_simps)
  also have "... = {# ?w (l+1) x. x ∈# mset_set (⋃w<r. {w * ?d..<(w + 1) * ?d})#}"
    unfolding 0 by simp
  also have "... = image_mset (?w (l+1)) (concat_mset
     (image_mset (mset_set ∘ (λw. {w * ?d..<(w + 1) * ?d})) (mset_set {..<r})))"
    by (intro arg_cong2[where f="image_mset"] concat_disjoint_union_mset refl 1) auto
  also have "... = concat_mset{#{#?w (l+1) i. i∈#mset_set {w*?d..<(w+1)*?d}#}. w∈#mset_set {..<r}#}"
    by (simp add:image_concat_mset image_mset.compositionality comp_def del:see_sample_walk.simps)
  also have "...=concat_mset {#{#?w(l+1)i. i∈#mset_set ((+)(w*?d)`{..<?d})#}. w∈#mset_set {..<r}#}"
    by (intro_cong "[σ⇩1 concat_mset, σ⇩2 image_mset, σ⇩1 mset_set]" more:ext)
     (simp add:  atLeast0LessThan[symmetric])
  also have "... = concat_mset
    {#{#?w (l+1) i. i∈#image_mset ((+) (w*?d)) (mset_set {..<?d})#}. w∈#mset_set {..<r}#}"
    by (intro_cong "[σ⇩1 concat_mset, σ⇩2 image_mset]" more:image_mset_cong
        image_mset_mset_set[symmetric] inj_onI) auto
  also have "... = concat_mset {#{#?w (l+1) (w*?d+i).i∈#mset_set {..<?d}#}. w∈#mset_set {..<r}#}"
    by (simp add:image_mset.compositionality comp_def del:see_sample_walk.simps)
  also have "... = concat_mset
    {#{#?w l w@[see_step e i (last (?w l w))].i∈#mset_set {..<?d}#}.w∈#mset_set {..<r}#}"
    by (intro_cong "[σ⇩1 concat_mset]" more:image_mset_cong) (simp add:Let_def)
  also have "... = concat_mset {#{#w@[see_step e i (last w)].i∈#mset_set {..<?d}#}.w∈#walks' ?G l#}"
    unfolding r_def Suc[symmetric] image_mset.compositionality comp_def by simp
  also have "... = concat_mset
    {#{#w@[x].x∈#{# see_step e i (last w). i∈#mset_set {..<?d}#}#}. w ∈# walks' ?G l#}"
    unfolding image_mset.compositionality comp_def by simp
  also have "... = concat_mset {#{#w@[x].x∈#vertices_from ?G (last w)#}. w ∈# walks' ?G l#}"
    using last_in_set set_walks_2(1,2)
    by (intro_cong "[σ⇩1 concat_mset, σ⇩2 image_mset]" more:image_mset_cong 2[symmetric]) blast
  also have "... = walks' (graph_of e) (l+1)"
    by (simp add:image_mset.compositionality comp_def)
  finally show ?case by simp
qed

unbundle no intro_cong_syntax

end