Theory Ugraph_Properties

section‹Classes and properties of graphs›

theory Ugraph_Properties
imports
  Ugraph_Lemmas
  Girth_Chromatic.Girth_Chromatic
begin

text‹A ``graph property'' is a set of graphs which is closed under isomorphism.›

type_synonym ugraph_class = "ugraph set"

definition ugraph_property :: "ugraph_class ⇒ bool" where
"ugraph_property C ≡ ∀G ∈ C. ∀G'. G ≃ G' ⟶ G' ∈ C"

abbreviation prob_in_class :: "(nat ⇒ real) ⇒ ugraph_class ⇒ nat ⇒ real" where
"prob_in_class p c n ≡ probGn p n (λes. edge_space.edge_ugraph n es ∈ c)"

text‹From now on, we consider random graphs not with fixed edge probabilities but rather with a
probability function depending on the number of vertices. Such a function is called a ``threshold''
for a graph property iff
\begin{itemize}
  \item for asymptotically \emph{larger} probability functions, the probability that a random graph
    is an element of that class tends to \emph{$1$} (``$1$-statement''), and
  \item for asymptotically \emph{smaller} probability functions, the probability that a random graph
    is an element of that class tends to \emph{$0$} (``$0$-statement'').
\end{itemize}›

definition is_threshold :: "ugraph_class ⇒ (nat ⇒ real) ⇒ bool" where
"is_threshold c t ≡ ugraph_property c ∧ (∀p. nonzero_prob_fun p ⟶
  (p ≪ t ⟶ prob_in_class p c ⇢ 0) ∧
  (t ≪ p ⟶ prob_in_class p c ⇢ 1))"

lemma is_thresholdI[intro]:
  assumes "ugraph_property c"
  assumes "⋀p. ⟦ nonzero_prob_fun p; p ≪ t ⟧ ⟹ prob_in_class p c ⇢ 0"
  assumes "⋀p. ⟦ nonzero_prob_fun p; t ≪ p ⟧ ⟹ prob_in_class p c ⇢ 1"
  shows "is_threshold c t"
using assms unfolding is_threshold_def by blast

end