# Theory Expander_Graphs_TTS

section ‹Setup for Types to Sets\label{sec:tts}›

theory Expander_Graphs_TTS
imports
Expander_Graphs_Definition
"HOL-Analysis.Cartesian_Space"
"HOL-Types_To_Sets.Types_To_Sets"
begin

text ‹This section sets up a sublocale with the assumption that there is a finite type with the same
cardinality as the vertex set of a regular graph. This allows defining the adjacency matrix for
the graph using type-based linear algebra.

Theorems shown in the sublocale that do not refer to the local type are then lifted to the
@{locale regular_graph} locale using the Types-To-Sets mechanism.›

locale regular_graph_tts = regular_graph +
fixes n_itself :: "('n :: finite) itself"
assumes td: "∃(f :: ('n ⇒ 'a)) g. type_definition f g (verts G)"
begin

definition td_components :: "('n ⇒ 'a) × ('a ⇒ 'n)"
where "td_components = (SOME q. type_definition (fst q) (snd q) (verts G))"

definition enum_verts where "enum_verts = fst td_components"
definition enum_verts_inv where "enum_verts_inv = snd td_components"

sublocale type_definition "enum_verts" "enum_verts_inv" "verts G"
proof -
have 0:"∃q. type_definition ((fst q)::('n ⇒ 'a)) (snd q) (verts G)"
using td by simp
show "type_definition enum_verts enum_verts_inv (verts G)"
unfolding td_components_def enum_verts_def enum_verts_inv_def using someI_ex[OF 0] by simp
qed

lemma enum_verts: "bij_betw enum_verts UNIV (verts G)"
unfolding bij_betw_def by (simp add: Rep_inject Rep_range inj_on_def)

text ‹The stochastic matrix associated to the graph.›

definition A :: "('c::field)^'n^'n" where
"A = (χ i j. of_nat (count (edges G) (enum_verts j,enum_verts i))/of_nat d)"

lemma card_n: "CARD('n) = n"
unfolding n_def card by simp

lemma symmetric_A: "transpose A = A"
proof -
have "A $i$ j = A $j$ i" for i j
unfolding A_def count_edges arcs_betw_def using symmetric_multi_graphD[OF sym]
by auto
thus ?thesis
unfolding transpose_def
by (intro iffD2[OF vec_eq_iff] allI) auto
qed

lemma g_step_conv:
"(χ i. g_step f (enum_verts i)) = A *v (χ i. f (enum_verts i))"
proof -
have "g_step f (enum_verts i) = (∑j∈UNIV. A $i$ j * f (enum_verts j))" (is "?L = ?R") for i
proof -
have "?L = (∑x∈in_arcs G (enum_verts i). f (tail G x) / d)"
unfolding g_step_def by simp
also have "... = (∑x∈#vertices_to G (enum_verts i). f x/d)"
unfolding verts_to_alt sum_unfold_sum_mset by (simp add:image_mset.compositionality comp_def)
also have "... = (∑j∈verts G. (count (vertices_to G (enum_verts i)) j) * (f j / real d))"
by (intro sum_mset_conv_2 set_mset_vertices_to) auto
also have "... = (∑j∈verts G. (count (edges G) (j,enum_verts i)) * (f j / real d))"
unfolding vertices_to_def count_mset_exp
by (intro sum.cong arg_cong[where f="real"] arg_cong2[where f="(*)"])
(auto simp add:filter_filter_mset image_mset_filter_mset_swap[symmetric] prod_eq_iff ac_simps)
also have "...=(∑j∈UNIV.(count(edges G)(enum_verts j,enum_verts i))*(f(enum_verts j)/real d))"
by (intro sum.reindex_bij_betw[symmetric] enum_verts)
also have "... = ?R"
unfolding A_def by simp
finally show ?thesis by simp
qed
thus ?thesis
unfolding matrix_vector_mult_def by (intro iffD2[OF vec_eq_iff] allI) simp
qed

lemma g_inner_conv:
"g_inner f g = (χ i. f (enum_verts i)) ∙ (χ i. g (enum_verts i))"
unfolding inner_vec_def g_inner_def vec_lambda_beta inner_real_def conjugate_real_def
by (intro sum.reindex_bij_betw[symmetric] enum_verts)

lemma g_norm_conv:
"g_norm f = norm (χ i. f (enum_verts i))"
proof -
have "g_norm f^2 = norm (χ i. f (enum_verts i))^2"
unfolding g_norm_sq power2_norm_eq_inner g_inner_conv by simp
thus ?thesis
using g_norm_nonneg norm_ge_zero by simp
qed

end

lemma eg_tts_1:
assumes "regular_graph G"
assumes "∃(f::('n::finite) ⇒ 'a) g. type_definition f g (verts G)"
shows "regular_graph_tts TYPE('n) G"
using assms
unfolding regular_graph_tts_def  regular_graph_tts_axioms_def by auto

context regular_graph
begin

lemma remove_finite_premise_aux:
assumes "∃(Rep :: 'n  ⇒ 'a) Abs. type_definition Rep Abs (verts G)"
shows "class.finite TYPE('n)"
proof -
obtain Rep :: "'n ⇒ 'a" and Abs where d:"type_definition Rep Abs (verts G)"
using assms by auto
interpret type_definition Rep Abs "verts G"
using d by simp

have "finite (verts G)" by simp
thus ?thesis
unfolding class.finite_def univ by auto
qed

lemma remove_finite_premise:
"(class.finite TYPE('n) ⟹ ∃(Rep :: 'n  ⇒ 'a) Abs. type_definition Rep Abs (verts G) ⟹ PROP Q)
≡ (∃(Rep :: 'n  ⇒ 'a) Abs. type_definition Rep Abs (verts G) ⟹ PROP Q)"
(is "?L ≡ ?R")
proof (intro Pure.equal_intr_rule)
assume e:"∃(Rep :: 'n  ⇒ 'a) Abs. type_definition Rep Abs (verts G)" and l:"PROP ?L"
hence f: "class.finite TYPE('n)"
using remove_finite_premise_aux[OF e] by simp

show "PROP ?R"
using l[OF f] by auto
next
assume "∃(Rep :: 'n  ⇒ 'a) Abs. type_definition Rep Abs (verts G)" and l:"PROP ?R"
show "PROP ?L"
using l by auto
qed

end

end