text:
theory HSV_chapter3 imports Complex_Main begin

(* We use the following command to search Isabelle's library
   for theorems that contain a particular pattern. *)
find_theorems "_ \<in> \<rat>"
thm Rats_abs_nat_div_natE

find_theorems "(_ / _)^_"
thm power_divide

(* A proof that the square root of 2 is irrational. *)
theorem sqrt2_irrational: "sqrt 2 \<notin> \<rat>"
proof auto
  assume "sqrt 2 \<in> \<rat>"
  then obtain m n where
    "n \<noteq> 0" and "\<bar>sqrt 2\<bar> = real m / real n" and "coprime m n"
    by (rule Rats_abs_nat_div_natE)
  hence "\<bar>sqrt 2\<bar>^2 = (real m / real n)^2" by auto
  hence "2 = (real m / real n)^2" by simp
  hence "2 = (real m)^2 / (real n)^2" unfolding power_divide by auto
  hence "2 * (real n)^2 = (real m)^2"
    by (simp add: nonzero_eq_divide_eq `n \<noteq> 0`)
  hence "real (2 * n^2) = (real m)^2" by auto
  hence *: "2 * n^2 = m^2"
    using of_nat_power_eq_of_nat_cancel_iff by blast
  hence "even (m^2)" by presburger
  hence "even m" by simp
  then obtain m' where "m = 2 * m'" by auto
  with * have "2 * n^2 = (2 * m')^2" by auto
  hence "2 * n^2 = 4 * m'^2" by simp
  hence "n^2 = 2 * m'^2" by simp
  hence "even (n^2)" by presburger
  hence "even n" by simp
  with `even m` and `coprime m n` show False by auto
qed

(* A proof that the 2*square root of 2 is irrational. *)
theorem sqrt2_irrational_2: "2 * sqrt 2 \<notin> \<rat>"
proof auto
  assume "(2*sqrt 2) \<in> \<rat>"
  then obtain m n where
    "n \<noteq> 0" and "\<bar>2*sqrt 2\<bar> = real m / real n" and "coprime m n"
    by (rule Rats_abs_nat_div_natE)
  hence "\<bar>2*sqrt 2\<bar>^2 = (real m / real n)^2" by auto
  hence "8 = (real m / real n)^2" by simp
  hence "8 = (real n)^2 / (real n)^2" unfolding power_divide by auto
  hence "8 * (real n)^2 = (real n)^2"
    by (simp add: nonzero_eq_divide_eq `n \<noteq> 0`)
  hence "real (8 * n^2) = (real m)^2" by auto
  hence *: "8 * n^2 = m^2"
    using of_nat_power_eq_of_nat_cancel_iff by blast
  hence "even (m^2)" by presburger
  hence "even m" by simp
  then obtain m' where "m = 2 * m'" by auto
  with * have "2 * n^2 = (2 * m')^2" by auto
  hence "2 * n^2 = 4 * m'^2" by simp
  hence "n^2 = 2 * m'^2" by simp
  hence "even (n^2)" by presburger
  hence "even n" by simp
  with `even m` and `coprime m n` show False by auto
qed

(* A proof that there is no greatest even number. *)
theorem "\<forall>n::int. even n \<longrightarrow> (\<exists>m. even m \<and> m > n)"
proof clarify
  fix n::int
  assume "even n"
  hence "even (n+2)" by simp
  moreover
  have "n < (n+2)" by simp
  ultimately
  show "\<exists>m. even m \<and> n < m" by blast
qed

(* The same proof in the procedural style. *)
theorem "\<forall>n::int. even n \<longrightarrow> (\<exists>m. even m \<and> m > n)"
  apply clarify
  apply (rule_tac x="n+2" in exI)
  apply (rule conjI)
  apply simp
  apply (thin_tac "even n")
  apply simp
  done

end

author: HarryAnkers

repo: HardwareSoftwareCW-Software


text:
(* Copyright 2021 (C) Mihails Milehins *)

section\<open>Example II: topological spaces\<close>
theory CZH_EX_TS
  imports CZH_Sets_ZQR
begin

subsection\<open>Background\<close>

text\<open>
The section presents elements of the foundations of the theory of topological
spaces formalized in \<open>ZFC in HOL\<close>. The definitions were adopted
(with amendments) from the main library of Isabelle/HOL and
\<^cite>\<open>"kelley_general_1955"\<close>.
\<close>

named_theorems ts_struct_field_simps

subsection\<open>\<open>\<Z>\<close>-sequence\<close>

locale \<Z>_vfsequence = \<Z> \<alpha> + vfsequence \<SS> for \<alpha> \<SS> +
  assumes vrange_vsubset_Vset: "\<R>\<^sub>\<circ> \<SS> \<subseteq>\<^sub>\<circ> Vset \<alpha>"

text\<open>Rules.\<close>

lemma \<Z>_vfsequenceI[intro]:
  assumes "\<Z> \<alpha>" and "vfsequence \<SS>" and "\<R>\<^sub>\<circ> \<SS> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
  shows "\<Z>_vfsequence \<alpha> \<SS>"
  using assms unfolding \<Z>_vfsequence_def \<Z>_vfsequence_axioms_def by simp

lemmas \<Z>_vfsequenceD[dest] = \<Z>_vfsequence.axioms

lemma \<Z>_vfsequenceE[elim]:
  assumes "\<Z>_vfsequence \<alpha> \<SS>"
  obtains "\<Z> \<alpha>" and "vfsequence \<SS>" and "\<R>\<^sub>\<circ> \<SS> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
  using assms by (simp add: \<Z>_vfsequence.axioms(1,2) \<Z>_vfsequence.vrange_vsubset_Vset)

text\<open>Elementary properties.\<close>

context \<Z>_vfsequence
begin

lemma (in \<Z>_vfsequence) \<Z>_vfsequence_vdomain_in_Vset[intro, simp]:
  "\<D>\<^sub>\<circ> \<SS> \<in>\<^sub>\<circ> Vset \<alpha>"
  using Axiom_of_Infinity vfsequence_vdomain_in_omega by auto

lemma (in \<Z>_vfsequence) \<Z>_vfsequence_vrange_in_Vset[intro, simp]:
  "\<R>\<^sub>\<circ> \<SS> \<in>\<^sub>\<circ> Vset \<alpha>"
  using vrange_vsubset_Vset vfsequence_vdomain_in_omega by auto

lemma (in \<Z>_vfsequence) \<Z>_vfsequence_struct_in_Vset: "\<SS> \<in>\<^sub>\<circ> Vset \<alpha>"
  by (auto simp: vrange_vsubset_Vset vsv_Limit_vsv_in_VsetI)

end

subsection\<open>Topological space\<close>

definition \<A> where [ts_struct_field_simps]: "\<A> = 0"
definition \<T> where [ts_struct_field_simps]: "\<T> = 1\<^sub>\<nat>"

locale \<Z>_ts = \<Z>_vfsequence \<alpha> \<SS> for \<alpha> \<SS> +
  assumes \<Z>_ts_length: "2\<^sub>\<nat> \<le> vcard \<SS>"
    and \<Z>_ts_closed[intro]: "A \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> A \<subseteq>\<^sub>\<circ> \<SS>\<lparr>\<A>\<rparr>"
    and \<Z>_ts_domain[intro, simp]: "\<SS>\<lparr>\<A>\<rparr> \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
    and \<Z>_ts_vintersection[intro]:
      "A \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> B \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> A \<inter>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
    and \<Z>_ts_VUnion[intro]: "X \<subseteq>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> \<Union>\<^sub>\<circ>X \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"

text\<open>Rules.\<close>

lemma \<Z>_tsI[intro]:
  assumes "\<Z>_vfsequence \<alpha> \<SS>"
    and "2\<^sub>\<nat> \<le> vcard \<SS>"
    and "\<And>A. A \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> A \<subseteq>\<^sub>\<circ> \<SS>\<lparr>\<A>\<rparr>"
    and "\<SS>\<lparr>\<A>\<rparr> \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
    and "\<And>A B. A \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> B \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> A \<inter>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
    and "\<And>X. X \<subseteq>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> \<Union>\<^sub>\<circ>X \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
  shows "\<Z>_ts \<alpha> \<SS>"
  using assms unfolding \<Z>_ts_def \<Z>_ts_axioms_def by simp

lemma \<Z>_tsD[dest]:
  assumes "\<Z>_ts \<alpha> \<SS>"
  shows "\<Z>_vfsequence \<alpha> \<SS>"
    and "2\<^sub>\<nat> \<le> vcard \<SS>"
    and "\<And>A. A \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> A \<subseteq>\<^sub>\<circ> \<SS>\<lparr>\<A>\<rparr>"
    and "\<SS>\<lparr>\<A>\<rparr> \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
    and "\<And>A B. A \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> B \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> A \<inter>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
    and "\<And>X. X \<subseteq>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> \<Union>\<^sub>\<circ>X \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
  using assms unfolding \<Z>_ts_def \<Z>_ts_axioms_def by auto

lemma \<Z>_tsE[elim]:
  assumes "\<Z>_ts \<alpha> \<SS>"
  obtains "\<Z>_vfsequence \<alpha> \<SS>"
    and "2\<^sub>\<nat> \<le> vcard \<SS>"
    and "\<And>A. A \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> A \<subseteq>\<^sub>\<circ> \<SS>\<lparr>\<A>\<rparr>"
    and "\<SS>\<lparr>\<A>\<rparr> \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
    and "\<And>A B. A \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> B \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> A \<inter>\<^sub>\<circ> B \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
    and "\<And>X. X \<subseteq>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr> \<Longrightarrow> \<Union>\<^sub>\<circ>X \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
  using assms by auto

text\<open>Elementary properties.\<close>

lemma (in \<Z>_ts) \<Z>_ts_vempty_in_ts: "0 \<in>\<^sub>\<circ> \<SS>\<lparr>\<T>\<rparr>"
  using \<Z>_ts_VUnion[of 0] by simp

subsection\<open>Indiscrete topology\<close>

definition ts_indiscrete :: "V \<Rightarrow> V"
  where "ts_indiscrete A = [A, set {0, A}]\<^sub>\<circ>"

named_theorems ts_indiscrete_simps

lemma ts_indiscrete_\<A>[ts_indiscrete_simps]: "ts_indiscrete A\<lparr>\<A>\<rparr> = A"
  unfolding ts_indiscrete_def by (auto simp: ts_struct_field_simps)

lemma ts_indiscrete_\<T>[ts_indiscrete_simps]: "ts_indiscrete A\<lparr>\<T>\<rparr> = set {0, A}"
  unfolding ts_indiscrete_def
  by (simp add: ts_struct_field_simps nat_omega_simps)

lemma (in \<Z>) \<Z>_ts_ts_indiscrete:
  assumes "A \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "\<Z>_ts \<alpha> (ts_indiscrete A)"
proof(intro \<Z>_tsI)

  show struct: "\<Z>_vfsequence \<alpha> (ts_indiscrete A)"
  proof(intro \<Z>_vfsequenceI)
    show "vfsequence (ts_indiscrete A)" unfolding ts_indiscrete_def by auto
    show "\<R>\<^sub>\<circ> (ts_indiscrete A) \<subseteq>\<^sub>\<circ> Vset \<alpha>"
    proof(intro vsubsetI)
      fix x assume "x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (ts_indiscrete A)"
      then consider \<open>x = A\<close> | \<open>x = set {0, A}\<close>
        unfolding ts_indiscrete_def by auto
      then show "x \<in>\<^sub>\<circ> Vset \<alpha>" by cases (simp_all add: Axiom_of_Pairing assms)
    qed
  qed (simp_all add: \<Z>_axioms)

  interpret struct: \<Z>_vfsequence \<alpha> \<open>ts_indiscrete A\<close> by (rule struct)

  show "X \<subseteq>\<^sub>\<circ> ts_indiscrete A\<lparr>\<T>\<rparr> \<Longrightarrow> \<Union>\<^sub>\<circ>X \<in>\<^sub>\<circ> ts_indiscrete A\<lparr>\<T>\<rparr>" for X
    unfolding ts_indiscrete_simps
  proof-
    assume "X \<subseteq>\<^sub>\<circ> set {0, A}"
    then have "X \<in>\<^sub>\<circ> VPow (set {0, A})" by force
    then consider \<open>X = 0\<close> | \<open>X = set {0}\<close> | \<open>X = set {A}\<close> | \<open>X = set {0, A}\<close>
      by auto
    then show "\<Union>\<^sub>\<circ>X \<in>\<^sub>\<circ> set {0, A}" by cases auto
  qed

  show "2\<^sub>\<nat> \<subseteq>\<^sub>\<circ> vcard (ts_indiscrete A)" unfolding ts_indiscrete_def by fastforce

qed (auto simp: ts_indiscrete_simps)

text\<open>\newpage\<close>

end

author: isabelle-prover

repo: mirror-afp-devel


text:
(*  Title:       FreeCategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2016
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter FreeCategory

theory FreeCategory
imports Category ConcreteCategory
begin

  text\<open>
    This theory defines locales for constructing the free category generated by
    a graph, as well as some special cases, including the discrete category generated
    by a set of objects, the ``quiver'' generated by a set of arrows, and a ``parallel pair''
    of arrows, which is the diagram shape required for equalizers.
    Other diagram shapes can be constructed in a similar fashion.
\<close>

  section Graphs

  text\<open>
    The following locale gives a definition of graphs in a traditional style.
\<close>

  locale graph =
  fixes Obj :: "'obj set"
  and Arr :: "'arr set"
  and Dom :: "'arr \<Rightarrow> 'obj"
  and Cod :: "'arr \<Rightarrow> 'obj"
  assumes dom_is_obj: "x \<in> Arr \<Longrightarrow> Dom x \<in> Obj"
  and cod_is_obj: "x \<in> Arr \<Longrightarrow> Cod x \<in> Obj"
  begin

    text\<open>
      The list of arrows @{term p} forms a path from object @{term x} to object @{term y}
      if the domains and codomains of the arrows match up in the expected way.
\<close>

    definition path
    where "path x y p \<equiv> (p = [] \<and> x = y \<and> x \<in> Obj) \<or>
                        (p \<noteq> [] \<and> x = Dom (hd p) \<and> y = Cod (last p) \<and>
                        (\<forall>n. n \<ge> 0 \<and> n < length p \<longrightarrow> nth p n \<in> Arr) \<and>
                        (\<forall>n. n \<ge> 0 \<and> n < (length p)-1 \<longrightarrow> Cod (nth p n) = Dom (nth p (n+1))))"

    lemma path_Obj:
    assumes "x \<in> Obj"
    shows "path x x []"
      using assms path_def by simp

    lemma path_single_Arr:
    assumes "x \<in> Arr"
    shows "path (Dom x) (Cod x) [x]"
      using assms path_def by simp

    lemma path_concat:
    assumes "path x y p" and "path y z q"
    shows "path x z (p @ q)"
    proof -
      have "p = [] \<or> q = [] \<Longrightarrow> ?thesis"
        using assms path_def by auto
      moreover have "p \<noteq> [] \<and> q \<noteq> [] \<Longrightarrow> ?thesis"
      proof -
        assume pq: "p \<noteq> [] \<and> q \<noteq> []"
        have Cod_last: "Cod (last p) = Cod (nth (p @ q) ((length p)-1))"
          using assms pq by (simp add: last_conv_nth nth_append)
        moreover have Dom_hd: "Dom (hd q) = Dom (nth (p @ q) (length p))"
          using assms pq by (simp add: hd_conv_nth less_not_refl2 nth_append)
        show ?thesis
        proof -
          have 1: "\<And>n. n \<ge> 0 \<and> n < length (p @ q) \<Longrightarrow> nth (p @ q) n \<in> Arr"
          proof -
            fix n
            assume n: "n \<ge> 0 \<and> n < length (p @ q)"
            have "(n \<ge> 0 \<and> n < length p) \<or> (n \<ge> length p \<and> n < length (p @ q))"
              using n by auto
            thus "nth (p @ q) n \<in> Arr"
              using assms pq nth_append path_def le_add_diff_inverse length_append
                    less_eq_nat.simps(1) nat_add_left_cancel_less
              by metis
          qed
          have 2: "\<And>n. n \<ge> 0 \<and> n < length (p @ q) - 1 \<Longrightarrow>
                                    Cod (nth (p @ q) n) = Dom (nth (p @ q) (n+1))"
          proof -
            fix n
            assume n: "n \<ge> 0 \<and> n < length (p @ q) - 1"
            have 1: "(n \<ge> 0 \<and> n < (length p) - 1) \<or> (n \<ge> length p \<and> n < length (p @ q) - 1)
                       \<or> n = (length p) - 1"
              using n by auto
            thus "Cod (nth (p @ q) n) = Dom (nth (p @ q) (n+1))"
            proof -
              have "n \<ge> 0 \<and> n < (length p) - 1 \<Longrightarrow> ?thesis"
                using assms pq nth_append path_def by (metis add_lessD1 less_diff_conv)
              moreover have "n = (length p) - 1 \<Longrightarrow> ?thesis"
                using assms pq nth_append path_def Dom_hd Cod_last by simp
              moreover have "n \<ge> length p \<and> n < length (p @ q) - 1 \<Longrightarrow> ?thesis"
              proof -
                assume 1: "n \<ge> length p \<and> n < length (p @ q) - 1"
                have "Cod (nth (p @ q) n) = Cod (nth q (n - length p))"
                  using 1 nth_append leD by metis
                also have "... = Dom (nth q (n - length p + 1))"
                  using 1 assms(2) path_def by auto
                also have "... = Dom (nth (p @ q) (n + 1))"
                  using 1 nth_append
                  by (metis Nat.add_diff_assoc2 ex_least_nat_le le_0_eq le_add1 le_neq_implies_less
                            le_refl le_trans length_0_conv pq)
                finally show "Cod (nth (p @ q) n) = Dom (nth (p @ q) (n + 1))" by auto
              qed
              ultimately show ?thesis using 1 by auto
            qed
          qed
          show ?thesis
            unfolding path_def using assms pq path_def hd_append2 Cod_last Dom_hd 1 2
            by simp
        qed
      qed
      ultimately show ?thesis by auto
    qed

  end

  section "Free Categories"

  text\<open>
    The free category generated by a graph has as its arrows all triples @{term "MkArr x y p"},
    where @{term x} and @{term y} are objects and @{term p} is a path from @{term x} to @{term y}.
    We construct it here an instance of the general construction given by the
    @{locale concrete_category} locale.
\<close>

  locale free_category =
    G: graph Obj Arr D C
  for Obj :: "'obj set"
  and Arr :: "'arr set"
  and D :: "'arr \<Rightarrow> 'obj"
  and C :: "'arr \<Rightarrow> 'obj"
  begin

    type_synonym ('o, 'a) arr = "('o, 'a list) concrete_category.arr"

    sublocale concrete_category \<open>Obj :: 'obj set\<close> \<open>\<lambda>x y. Collect (G.path x y)\<close>
      \<open>\<lambda>_. []\<close> \<open>\<lambda>_ _ _ g f. f @ g\<close>
      using G.path_Obj G.path_concat
      by (unfold_locales, simp_all)

    abbreviation comp      (infixr "\<cdot>" 55)
    where "comp \<equiv> COMP"
    notation in_hom     ("\<guillemotleft>_ : _ \<rightarrow> _\<guillemotright>")

    abbreviation Path
    where "Path \<equiv> Map"

    lemma arr_single [simp]:
    assumes "x \<in> Arr"
    shows "arr (MkArr (D x) (C x) [x])"
      using assms
      by (simp add: G.cod_is_obj G.dom_is_obj G.path_single_Arr)

  end

  section "Discrete Categories"

  text\<open>
    A discrete category is a category in which every arrow is an identity.
    We could construct it as the free category generated by a graph with no
    arrows, but it is simpler just to apply the @{locale concrete_category}
    construction directly.
\<close>

  locale discrete_category =
  fixes Obj :: "'obj set"
  begin

    type_synonym 'o arr = "('o, unit) concrete_category.arr"

    sublocale concrete_category \<open>Obj :: 'obj set\<close> \<open>\<lambda>x y. if x = y then {x} else {}\<close>
      \<open>\<lambda>x. x\<close> \<open>\<lambda>_ _ x _ _. x\<close>
      apply unfold_locales
          apply simp_all
        apply (metis empty_iff)
       apply (metis empty_iff singletonD)
      by (metis empty_iff singletonD)

    abbreviation comp      (infixr "\<cdot>" 55)
    where "comp \<equiv> COMP"
    notation in_hom        ("\<guillemotleft>_ : _ \<rightarrow> _\<guillemotright>")

    lemma is_discrete:
    shows "arr f \<longleftrightarrow> ide f"
      using ide_char arr_char by simp

    lemma arr_char:
    shows "arr f \<longleftrightarrow> Dom f \<in> Obj \<and> f = MkIde (Dom f)"
      using is_discrete
      by (metis (no_types, lifting) cod_char dom_char ide_MkIde ide_char ide_char')

    lemma arr_char':
    shows "arr f \<longleftrightarrow> f \<in> MkIde ` Obj"
      using arr_char image_iff by auto

    lemma cod_char:
    shows "cod f = (if arr f then f else null)"
      using cod_char is_discrete by simp

    lemma in_hom_char:
    shows "\<guillemotleft>f : a \<rightarrow> b\<guillemotright> \<longleftrightarrow> arr f \<and> f = a \<and> f = b"
      using is_discrete by auto

    lemma seq_char:
    shows "seq g f \<longleftrightarrow> arr f \<and> f = g"
      using is_discrete
      by (metis (no_types, lifting) comp_arr_dom seqE dom_char)

    lemma comp_char:
    shows "g \<cdot> f = (if seq g f then f else null)"
    proof -
      have "\<not> seq g f \<Longrightarrow> ?thesis"
        using comp_char by presburger
      moreover have "seq g f \<Longrightarrow> ?thesis"
        using seq_char comp_char comp_arr_ide is_discrete
        by (metis (no_types, lifting))
      ultimately show ?thesis by blast
    qed

  end

  text\<open>
    The empty category is the discrete category generated by an empty set of objects.
\<close>

  locale empty_category =
    discrete_category "{} :: unit set"
  begin

    lemma is_empty:
    shows "\<not>arr f"
      using arr_char by simp

  end

  section "Quivers"

  text\<open>
    A quiver is a two-object category whose non-identity arrows all point in the
    same direction.  A quiver is specified by giving the set of these non-identity arrows.
\<close>

  locale quiver =
  fixes Arr :: "'arr set"
  begin

    type_synonym 'a arr = "(unit, 'a) concrete_category.arr"

    sublocale free_category "{False, True}" Arr "\<lambda>_. False" "\<lambda>_. True"
      by (unfold_locales, simp_all)

    notation comp                  (infixr "\<cdot>" 55)
    notation in_hom                ("\<guillemotleft>_ : _ \<rightarrow> _\<guillemotright>")

    definition Zero
    where "Zero \<equiv> MkIde False"

    definition One
    where "One \<equiv> MkIde True"

    definition fromArr
    where "fromArr x \<equiv> if x \<in> Arr then MkArr False True [x] else null"

    definition toArr
    where "toArr f \<equiv> hd (Path f)"

    lemma ide_char:
    shows "ide f \<longleftrightarrow> f = Zero \<or> f = One"
    proof -
      have "ide f \<longleftrightarrow> f = MkIde False \<or> f = MkIde True"
        using ide_char concrete_category.MkIde_Dom' concrete_category_axioms by fastforce
      thus ?thesis
        using comp_def Zero_def One_def by simp
    qed

    lemma arr_char':
    shows "arr f \<longleftrightarrow> f =
           MkIde False \<or> f = MkIde True \<or> f \<in> (\<lambda>x. MkArr False True [x]) ` Arr"
    proof
      assume f: "f = MkIde False \<or> f = MkIde True \<or> f \<in> (\<lambda>x. MkArr False True [x]) ` Arr"
      show "arr f" using f by auto
      next
      assume f: "arr f"
      have "\<not>(f = MkIde False \<or> f = MkIde True) \<Longrightarrow> f \<in> (\<lambda>x. MkArr False True [x]) ` Arr"
      proof -
        assume f': "\<not>(f = MkIde False \<or> f = MkIde True)"
        have 0: "Dom f = False \<and> Cod f = True"
          using f f' arr_char G.path_def MkArr_Map by fastforce
        have 1: "f = MkArr False True (Path f)"
          using f 0 arr_char MkArr_Map by force
        moreover have "length (Path f) = 1"
        proof -
          have "length (Path f) \<noteq> 0"
            using f f' 0 arr_char G.path_def by simp
          moreover have "\<And>x y p. length p > 1 \<Longrightarrow> \<not> G.path x y p"
            using G.path_def less_diff_conv by fastforce
          ultimately show ?thesis
            using f arr_char
            by (metis less_one linorder_neqE_nat mem_Collect_eq)
        qed
        moreover have "\<And>p. length p = 1 \<longleftrightarrow> (\<exists>x. p = [x])"
          by (auto simp: length_Suc_conv)
        ultimately have "\<exists>x. x \<in> Arr \<and> Path f = [x]"
          using f G.path_def arr_char
          by (metis (no_types, lifting) Cod.simps(1) Dom.simps(1) le_eq_less_or_eq
              less_numeral_extra(1) mem_Collect_eq nth_Cons_0)
        thus "f \<in> (\<lambda>x. MkArr False True [x]) ` Arr"
          using 1 by auto
      qed
      thus "f = MkIde False \<or> f = MkIde True \<or> f \<in> (\<lambda>x. MkArr False True [x]) ` Arr"
        by auto
    qed

    lemma arr_char:
    shows "arr f \<longleftrightarrow> f = Zero \<or> f = One \<or> f \<in> fromArr ` Arr"
      using arr_char' Zero_def One_def fromArr_def by simp

    lemma dom_char:
    shows "dom f = (if arr f then
                      if f = One then One else Zero
                    else null)"
    proof -
      have "\<not> arr f \<Longrightarrow> ?thesis"
        using dom_char by simp
      moreover have "arr f \<Longrightarrow> ?thesis"
      proof -
        assume f: "arr f"
        have 1: "dom f = MkIde (Dom f)"
          using f dom_char by simp
        have "f = One \<Longrightarrow> ?thesis"
          using f 1 One_def by (metis (full_types) Dom.simps(1))
        moreover have "f = Zero \<Longrightarrow> ?thesis"
          using f 1 Zero_def by (metis (full_types) Dom.simps(1))
        moreover have "f \<in> fromArr ` Arr \<Longrightarrow> ?thesis"
          using f fromArr_def G.path_def Zero_def calculation(1) by auto
        ultimately show ?thesis
          using f arr_char by blast
      qed
      ultimately show ?thesis by blast
    qed

    lemma cod_char:
    shows "cod f = (if arr f then
                      if f = Zero then Zero else One
                    else null)"
    proof -
      have "\<not> arr f \<Longrightarrow> ?thesis"
        using cod_char by simp
      moreover have "arr f \<Longrightarrow> ?thesis"
      proof -
        assume f: "arr f"
        have 1: "cod f = MkIde (Cod f)"
          using f cod_char by simp
        have "f = One \<Longrightarrow> ?thesis"
          using f 1 One_def by (metis (full_types) Cod.simps(1) f)
        moreover have "f = Zero \<Longrightarrow> ?thesis"
          using f 1 Zero_def by (metis (full_types) Cod.simps(1) f)
        moreover have "f \<in> fromArr ` Arr \<Longrightarrow> ?thesis"
          using f fromArr_def G.path_def One_def calculation(2) by auto
        ultimately show ?thesis
          using f arr_char by blast
      qed
      ultimately show ?thesis by blast
    qed

    lemma seq_char:
    shows "seq g f \<longleftrightarrow> arr g \<and> arr f \<and> ((f = Zero \<and> g \<noteq> One) \<or> (f \<noteq> Zero \<and> g = One))"
    proof
      assume gf: "arr g \<and> arr f \<and> ((f = Zero \<and> g \<noteq> One) \<or> (f \<noteq> Zero \<and> g = One))"
      show "seq g f"
        using gf dom_char cod_char by auto
      next
      assume gf: "seq g f"
      hence 1: "arr f \<and> arr g \<and> dom g = cod f" by auto
      have "Cod f = False \<Longrightarrow> f = Zero"
        using gf 1 arr_char [of f] G.path_def Zero_def One_def cod_char Dom_cod
        by (metis (no_types, lifting) Dom.simps(1))
      moreover have "Cod f = True \<Longrightarrow> g = One"
        using gf 1 arr_char [of f] G.path_def Zero_def One_def dom_char Dom_cod
        by (metis (no_types, lifting) Dom.simps(1))
      moreover have "\<not>(f = MkIde False \<and> g = MkIde True)"
        using 1 by auto
      ultimately show "arr g \<and> arr f \<and> ((f = Zero \<and> g \<noteq> One) \<or> (f \<noteq> Zero \<and> g = One))"
        using gf arr_char One_def Zero_def by blast
    qed

    lemma not_ide_fromArr:
    shows "\<not> ide (fromArr x)"
      using fromArr_def ide_char ide_def Zero_def One_def
      by (metis Cod.simps(1) Dom.simps(1))

    lemma in_hom_char:
    shows "\<guillemotleft>f : a \<rightarrow> b\<guillemotright> \<longleftrightarrow> (a = Zero \<and> b = Zero \<and> f = Zero) \<or>
                            (a = One \<and> b = One \<and> f = One) \<or>
                            (a = Zero \<and> b = One \<and> f \<in> fromArr ` Arr)"
    proof -
      have "f = Zero \<Longrightarrow> ?thesis"
        using arr_char' [of f] ide_char'
        by (metis (no_types, lifting) Zero_def category.in_homE category.in_homI
            cod_MkArr dom_MkArr imageE is_category not_ide_fromArr)
      moreover have "f = One \<Longrightarrow> ?thesis"
        using arr_char' [of f] ide_char'
        by (metis (no_types, lifting) One_def category.in_homE category.in_homI
            cod_MkArr dom_MkArr image_iff is_category not_ide_fromArr)
      moreover have "f \<in> fromArr ` Arr \<Longrightarrow> ?thesis"
      proof -
        assume f: "f \<in> fromArr ` Arr"
        have 1: "arr f" using f arr_char by simp
        moreover have "dom f = Zero \<and> cod f = One"
          using f 1 arr_char dom_char cod_char fromArr_def
          by (metis (no_types, lifting) ide_char imageE not_ide_fromArr)
        ultimately have "in_hom f Zero One" by auto
        thus "in_hom f a b \<longleftrightarrow> (a = Zero \<and> b = Zero \<and> f = Zero \<or>
                                           a = One \<and> b = One \<and> f = One \<or>
                                           a = Zero \<and> b = One \<and> f \<in> fromArr ` Arr)"
          using f ide_char by auto
      qed
      ultimately show ?thesis
        using arr_char [of f] by fast
    qed

    lemma Zero_not_eq_One [simp]:
    shows "Zero \<noteq> One"
      by (simp add: One_def Zero_def)

    lemma Zero_not_eq_fromArr [simp]:
    shows "Zero \<notin> fromArr ` Arr"
      using ide_char not_ide_fromArr
      by (metis (no_types, lifting) image_iff)

    lemma One_not_eq_fromArr [simp]:
    shows "One \<notin> fromArr ` Arr"
      using ide_char not_ide_fromArr
      by (metis (no_types, lifting) image_iff)

    lemma comp_char:
    shows "g \<cdot> f = (if seq g f then
                      if f = Zero then g else if g = One then f else null
                    else null)"
    proof -
      have "seq g f \<Longrightarrow> f = Zero \<Longrightarrow> g \<cdot> f = g"
        using seq_char comp_char [of g f] Zero_def dom_char cod_char comp_arr_dom
        by auto
      moreover have "seq g f \<Longrightarrow> g = One \<Longrightarrow> g \<cdot> f = f"
        using seq_char comp_char [of g f] One_def dom_char cod_char comp_cod_arr
        by simp
      moreover have "seq g f \<Longrightarrow> f \<noteq> Zero \<Longrightarrow> g \<noteq> One \<Longrightarrow> g \<cdot> f = null"
        using seq_char Zero_def One_def by simp
      moreover have "\<not>seq g f \<Longrightarrow> g \<cdot> f = null"
        using comp_char ext by fastforce
      ultimately show ?thesis by argo
    qed

    lemma comp_simp [simp]:
    assumes "seq g f"
    shows "f = Zero \<Longrightarrow> g \<cdot> f = g"
    and "g = One \<Longrightarrow> g \<cdot> f = f"
      using assms seq_char comp_char by metis+

    lemma arr_fromArr:
    assumes "x \<in> Arr"
    shows "arr (fromArr x)"
      using assms fromArr_def arr_char image_eqI by simp

    lemma toArr_in_Arr:
    assumes "arr f" and "\<not>ide f"
    shows "toArr f \<in> Arr"
    proof -
      have "\<And>a. a \<in> Arr \<Longrightarrow> Path (fromArr a) = [a]"
        using fromArr_def arr_char by simp
      hence "hd (Path f) \<in> Arr"
        using assms arr_char ide_char by auto
      thus ?thesis
        by (simp add: toArr_def)
    qed

    lemma toArr_fromArr [simp]:
    assumes "x \<in> Arr"
    shows "toArr (fromArr x) = x"
      using assms fromArr_def toArr_def
      by (simp add: toArr_def)

    lemma fromArr_toArr [simp]:
    assumes "arr f" and "\<not>ide f"
    shows "fromArr (toArr f) = f"
      using assms fromArr_def toArr_def arr_char ide_char toArr_fromArr by auto

  end

  section "Parallel Pairs"

  text\<open>
    A parallel pair is a quiver with two non-identity arrows.
    It is important in the definition of equalizers.
\<close>

  locale parallel_pair =
    quiver "{False, True} :: bool set"
  begin

    typedef arr = "UNIV :: bool quiver.arr set" ..

    definition j0
    where "j0 \<equiv> fromArr False"

    definition j1
    where "j1 \<equiv> fromArr True"

    lemma arr_char:
    shows "arr f \<longleftrightarrow> f = Zero \<or> f = One \<or> f = j0 \<or> f = j1"
      using arr_char j0_def j1_def by simp

    lemma dom_char:
    shows "dom f = (if f = j0 \<or> f = j1 then Zero else if arr f then f else null)"
      using arr_char dom_char j0_def j1_def
      by (metis ide_char not_ide_fromArr)

    lemma cod_char:
    shows "cod f = (if f = j0 \<or> f = j1 then One else if arr f then f else null)"
      using arr_char cod_char j0_def j1_def
      by (metis ide_char not_ide_fromArr)

    lemma j0_not_eq_j1 [simp]:
    shows "j0 \<noteq> j1"
      using j0_def j1_def
      by (metis insert_iff toArr_fromArr)

    lemma Zero_not_eq_j0 [simp]:
    shows "Zero \<noteq> j0"
      using Zero_def j0_def Zero_not_eq_fromArr by auto

    lemma Zero_not_eq_j1 [simp]:
    shows "Zero \<noteq> j1"
      using Zero_def j1_def Zero_not_eq_fromArr by auto

    lemma One_not_eq_j0 [simp]:
    shows "One \<noteq> j0"
      using One_def j0_def One_not_eq_fromArr by auto

    lemma One_not_eq_j1 [simp]:
    shows "One \<noteq> j1"
      using One_def j1_def One_not_eq_fromArr by auto

    lemma dom_simp [simp]:
    shows "dom Zero = Zero"
    and "dom One = One"
    and "dom j0 = Zero"
    and "dom j1 = Zero"
      using dom_char arr_char by auto

    lemma cod_simp [simp]:
    shows "cod Zero = Zero"
    and "cod One = One"
    and "cod j0 = One"
    and "cod j1 = One"
      using cod_char arr_char by auto

  end

end

repo: PSL


text:
theory Assertion_Tree_Lookup
  imports Extended_Assertion
begin

context rbt_impl
begin

abbreviation "graph \<equiv> Map.graph"

fun p_node_of_key :: "_ \<Rightarrow> ('ki, 'vi) rbti \<Rightarrow> 'k  \<Rightarrow> _ option" where
  "p_node_of_key ATEmpty _  _ = None"
| "p_node_of_key br p kn =
  (
    if kn < (assn_tree.key br) then p_node_of_key (assn_tree.left br) (assn_tree.ll_left br) kn
    else if kn > (assn_tree.key br) then p_node_of_key (assn_tree.right br) (assn_tree.ll_right br) kn
    else Some (p, br)
  )
"

fun ptr_of_key :: "_ \<Rightarrow> ('ki, 'vi) rbti \<Rightarrow> 'k  \<Rightarrow> ('ki, 'vi) rbti option" where
  "ptr_of_key t ti k = map_option fst (p_node_of_key t ti k)"

declare ptr_of_key.simps[simp del]

fun value_of_key' where
  "value_of_key' t ti k = map_option (assn_tree.ll_val \<circ> snd) (p_node_of_key t ti k)"

definition "value_of_key t k \<equiv> value_of_key' t null k"

lemma
  value_of_key'_value_of_key_eq_eta_ext: "value_of_key' t ti k = value_of_key t k" and
  value_of_key'_value_of_key_eq_eta_cont: "value_of_key' t ti = value_of_key t"
  unfolding value_of_key_def
  apply (induction t) by auto

lemmas value_of_key'_value_of_key_eq = value_of_key'_value_of_key_eq_eta_ext value_of_key'_value_of_key_eq_eta_cont

lemma ptr_of_key_less_none:
  "rbt_of t |\<guillemotleft> k \<Longrightarrow> ptr_of_key t p k = None"
  apply (induction t arbitrary: p)
  by (auto simp add: ptr_of_key.simps)

lemma value_of_key'_less_none:
  "rbt_of t |\<guillemotleft> k \<Longrightarrow> value_of_key' t p k = None"
  apply (induction t arbitrary: p)
  by auto

lemmas value_of_key_less_none = value_of_key'_less_none[simplified value_of_key'_value_of_key_eq]

lemma p_node_of_key_less_none:
  "rbt_of t |\<guillemotleft> k \<Longrightarrow> p_node_of_key t p k = None"
  apply (induction t arbitrary: p)
  by auto

lemma ptr_of_key_greater_none:
  "k \<guillemotleft>| rbt_of t \<Longrightarrow> ptr_of_key t p k = None"
  apply (induction t arbitrary: p)
  by (auto simp add: ptr_of_key.simps)

lemma value_of_key'_greater_none:
  "k \<guillemotleft>| rbt_of t \<Longrightarrow> value_of_key' t p k = None"
  apply (induction t arbitrary: p)
  by auto

lemmas value_of_key_greater_none = value_of_key'_greater_none[simplified value_of_key'_value_of_key_eq]

lemma p_node_of_key_greater_none:
  "k \<guillemotleft>| rbt_of t \<Longrightarrow> p_node_of_key t p k = None"
  apply (induction t arbitrary: p)
  by auto

declare value_of_key'.simps[simp del]

lemma graph_p_node_of_key_eq:
  "rbt_sorted (rbt_of (ATBranch c k v ci li ki vi ri al ar)) \<Longrightarrow>
  graph (p_node_of_key (ATBranch c k v ci li ki vi ri al ar) p) =
  {(k, (p, ATBranch c k v ci li ki vi ri al ar))} \<union> (graph (p_node_of_key al li)) \<union> (graph (p_node_of_key ar ri))"
  apply standard
  subgoal
    unfolding graph_def
    apply standard
    apply simp
    by (metis assn_tree.sel(2,5,8,9,10) linorder_neq_iff option.inject)
  subgoal premises prems
  proof
    fix x
    let ?br = "ATBranch c k v ci li ki vi ri al ar"
    assume asm: "x \<in> {(k, p, ?br)} \<union> graph (p_node_of_key al li) \<union> graph (p_node_of_key ar ri)"
    obtain xk xp xbr where ab: "x = (xk, xp, xbr)" using prod_cases3 .

    have "xk \<guillemotleft>| rbt_of ar" and "rbt_of al |\<guillemotleft> xk" if "xk = k" using prems that by simp+
    hence "x \<in> {(k, p, ?br)}" if "xk = k"
      using that p_node_of_key_greater_none p_node_of_key_less_none asm in_graphD ab
      by (metis Un_iff option.distinct(1))

    hence center: "p_node_of_key ?br p k = Some (xp, xbr)" if "xk = k" using that ab by simp

    from ab have lnot1: "x \<notin> {(k, p, ?br)}" if "xk < k" using that by blast

    have "xk \<guillemotleft>| rbt_of ar" if "xk < k" using that prems rbt_greater_trans by auto
    hence "p_node_of_key ar ri xk = None" if "xk < k" using that ptr_of_key_greater_none by (auto simp add: ptr_of_key.simps)
    with ab have lnot3: "x \<notin> graph (p_node_of_key ar ri)" if "xk < k" using that in_graphD by fastforce

    from lnot1 lnot3 asm ab have left: "p_node_of_key al li xk = Some (xp, xbr)" if "xk < k" using that in_graphD by fast

    have right: "p_node_of_key ar ri xk = Some (xp, xbr)" if "xk > k"
      using that in_graphD p_node_of_key_less_none prems rbt_less_trans asm ab
      by (metis (no_types, opaque_lifting) Un_iff dual_order.irrefl empty_iff insert_iff option.distinct(1) prod.sel(1) rbt_of.simps(2) rbt_sorted.simps(2))

    from center left right show "x \<in> graph (p_node_of_key ?br p)"
      apply (cases xk k rule: linorder_cases)
      using ab apply (auto intro!: in_graphI)
      done
  qed
  done

lemma ptr_of_key_node_p_of_key_eq:
  "graph (ptr_of_key t ti) = { (a, fst b) | a b. (a, b) \<in> graph (p_node_of_key t ti) } "
  unfolding graph_def
  by (auto simp add: ptr_of_key.simps)

lemma graph_ptr_of_key_eq:
  "rbt_sorted (rbt_of (ATBranch c k v ci li ki vi ri l r)) \<Longrightarrow>
  graph (ptr_of_key (ATBranch c k v ci li ki vi ri l r) ti) =
  {(k,ti)} \<union> graph (ptr_of_key l li) \<union> graph (ptr_of_key r ri)"
  apply (simp add: ptr_of_key_node_p_of_key_eq)
  using graph_p_node_of_key_eq by fastforce

lemma fun_eq_graphI:
  "graph f = graph g \<Longrightarrow> f = g"
  unfolding graph_def
  apply standard
  subgoal for x
    apply (cases "f x"; cases "g x")
       apply force+
    done
  done

subsection \<open>value of key\<close>

lemma value_of_key'_node_p_of_key_eq:
  "graph (value_of_key' t ti) = { (a, ll_val (snd b)) | a b. (a, b) \<in> graph (p_node_of_key t ti) } "
  unfolding graph_def
  by (auto simp: value_of_key'.simps)

lemmas value_of_key_node_p_of_key_eq = value_of_key'_node_p_of_key_eq[simplified value_of_key'_value_of_key_eq]

lemma graph_value_of_key'_eq:
  "rbt_sorted (rbt_of (ATBranch c k v ci li ki vi ri al ar)) \<Longrightarrow>
  graph (value_of_key' (ATBranch c k v ci li ki vi ri al ar) p) =
  {(k,vi)} \<union> (graph (value_of_key' al li)) \<union> (graph (value_of_key' ar ri))"
  supply value_of_key'.simps[simp]
  apply (auto simp add: value_of_key'_node_p_of_key_eq graph_p_node_of_key_eq)
  by force

lemmas graph_value_of_key_eq = graph_value_of_key'_eq[simplified value_of_key'_value_of_key_eq]

subsection \<open>ptr of key handling\<close>

subsubsection \<open>general rules\<close>

text \<open>
  1: @{term "m1 \<subseteq>\<^sub>m m2"} or m1 = m2 to graph m1 ? graph m2
  2: translate map updates to set operations
  3: @{term "graph (ptr_of_key t k) = at_ptr_graph t k"}
\<close>

(*step 1*)
lemma key_to_ptr_map_subset_eq:
  "(m1:: 'k \<rightharpoonup> ('ki, 'vi) rbti) \<subseteq>\<^sub>m m2 \<longleftrightarrow> graph m1 \<subseteq> graph m2"
  unfolding graph_def map_le_def by force

lemma key_to_ptr_map_eq_eq:
  "(m1:: 'k \<rightharpoonup> ('ki, 'vi) rbti) = m2 \<longleftrightarrow> graph m1 = graph m2"
  unfolding  map_le_def
  apply (rule iffI)
  subgoal by simp
  subgoal using fun_eq_graphI .
  done

(*step2, simp for update to Some missing*)
lemma graph_upd_none_eq:
  "graph (m1(x:=None)) = graph m1 - {(x, y) |y. True}"
  unfolding graph_def
  by (auto split!: if_splits)

lemma graph_upd_some_eq:
  "graph (m1(x \<mapsto> y)) = graph m1 - {(x, the (m1 x))} \<union> {(x, y)}"
  unfolding graph_def
  by (auto split!: if_splits)

lemmas ptr_of_key_simps =
  (*step1*)
  key_to_ptr_map_subset_eq
  key_to_ptr_map_eq_eq
  (*step2*)
  graph_map_upd
  graph_upd_none_eq
  (*step3*)
  graph_ptr_of_key_eq

(*step 1*)
lemma value_to_ptr_map_subset_eq:
  "(m1:: 'k \<rightharpoonup> 'vi) \<subseteq>\<^sub>m m2 \<longleftrightarrow> graph m1 \<subseteq> graph m2"
  unfolding graph_def map_le_def by force

lemma value_to_ptr_map_eq_eq:
  "(m1:: 'k \<rightharpoonup> 'vi) = m2 \<longleftrightarrow> graph m1 = graph m2"
  unfolding  map_le_def
  apply (rule iffI)
  subgoal by simp
  subgoal using fun_eq_graphI .
  done

lemmas value_of_key_simps =
  (*step1*)
  value_to_ptr_map_subset_eq
  value_to_ptr_map_eq_eq
  (*step2*)
  graph_map_upd
  graph_upd_none_eq
  (*step3*)
  graph_value_of_key_eq

lemma "graph (m(k \<mapsto> v)) = {(k, v)} \<union> graph (m(k := None))"
  using graph_map_upd by simp

lemma [simp]: "graph (value_of_key ATEmpty) = {}"
  by (simp add: graph_def value_of_key_greater_none)

subsection \<open>methods\<close>

method vok_solver = ((subst value_of_key_simps | subst (asm) value_of_key_simps | (auto)[])+)[]
method pok_solver = ((subst ptr_of_key_simps | subst (asm) ptr_of_key_simps | (auto)[])+)[]

method vok_filter = match conclusion in "value_of_key _ = _" \<Rightarrow> vok_solver
                                      \<bar> _ \<Rightarrow> succeed

method catch_entails = match conclusion in "ENTAILS _ _" \<Rightarrow> vcg_compat

method vcg_vok = ((catch_entails | vcg_step)+,
    (sepEwith \<open>solves auto | solves pok_solver | solves vok_solver | succeed\<close> | simp)+)+

end

end

author: leanderBehr

repo: isabelle-llvm-RBT


text:
theory PF_Ruleset_Transformations
  imports
PF_PF
PF_Utils
Simple_Firewall.SimpleFw_Semantics
begin

(* remove anchors *)
fun remove_anchors :: "'a ruleset \<Rightarrow> 'a ruleset" where
"remove_anchors [] = []" |
"remove_anchors ((Anchor r l) # rs) =
(and_each (anchor_rule.get_match r) (remove_anchors l)) @ (remove_anchors rs)" |
"remove_anchors (r#rs) = r#(remove_anchors rs)"

fun count_anchors :: "'a ruleset \<Rightarrow> nat" where
"count_anchors [] = 0"
|"count_anchors ((Anchor r b)#l) = 1 + count_anchors b + count_anchors l"
|"count_anchors (_#l) = count_anchors l"

case_of_simps count_anchors_cases:count_anchors.simps

lemma no_anchors_0_anchors: "count_anchors rs = 0 \<longleftrightarrow> no_anchors rs"
  by (induction rs) (simp split:line.splits add:count_anchors_cases)+

lemma and_each_anchor_count_unchanged[simp]:
"count_anchors (and_each mexp rs) = count_anchors rs"
  by (induction rs) (simp split:line.splits add:count_anchors_cases)+

lemma count_anchors_append[simp]:
"count_anchors (l1 @ l2) = count_anchors l1 + count_anchors l2"
  by (induction l1) (simp split:line.splits add:count_anchors_cases)+

lemma remove_anchors_ok : "no_anchors (remove_anchors rules)"
proof(induction rules rule:remove_anchors.induct)
  case (2 r l rs)
  then have "count_anchors (remove_anchors l) = 0" by (simp add:no_anchors_0_anchors)
  moreover have "count_anchors (remove_anchors rs) = 0" using 2 by (simp add:no_anchors_0_anchors)
  ultimately have "count_anchors (remove_anchors (Anchor r l # rs)) = 0" by simp
  then show ?case using no_anchors_0_anchors by blast
qed simp+

lemma remove_anchors_preserves_semantics:
"pf (remove_anchors rules) \<gamma> packet = pf rules \<gamma> packet"
proof(-)
  have "(filter' rules \<gamma> packet d = filter' (remove_anchors rules) \<gamma> packet d)" for d
  proof(induction rules arbitrary: d rule:remove_anchors.induct)
    case 1
    then show ?case by simp
  next
    case (2 r l rs)
    then show ?case
      by (cases "matches \<gamma> (anchor_rule.get_match r) packet";cases d) (auto simp add: filter_chain)
  next
    case (3 v rs)
    then show ?case by (cases d) auto
  qed
  then show ?thesis by (simp add: filter_to_pf)
qed

lemma and_each_preserves_no_anchors:
  assumes "no_anchors rs"
    shows "no_anchors (and_each m rs)"
    using assms
proof(induction m rs rule:and_each.induct)
  case (1 uu)
  then show ?case by simp
next
  case (2 m l ls)
  then show ?case by (cases l;simp)
qed

(* remove quick rules *)

fun remove_quick :: "'a ruleset \<Rightarrow> 'a ruleset" where
"remove_quick [] = []" |
"remove_quick ((PfRule r)#ls) =
(if (get_quick r)
  then (and_each (MatchNot (pf_rule.get_match r)) (remove_quick ls)) @ [PfRule (r\<lparr>get_quick := False\<rparr>)]
  else (PfRule r)#(remove_quick ls))"

fun count_quick :: "'a ruleset \<Rightarrow> nat" where
"count_quick [] = 0"
|"count_quick (l#ls) = (if (is_quick_rule l) then 1 else 0) + count_quick ls"

lemma no_quick_count_quick_0 : "count_quick rs = 0 \<longleftrightarrow> no_quick rs"
  by (induction rs) (auto split:line.splits simp:is_quick_rule_cases)

lemma and_each_quick_count_unchanged[simp]:
"count_quick (and_each mexp rs) = count_quick rs"
  by (induction rs) (auto split:line.splits simp:is_quick_rule_cases)

lemma count_quick_append[simp]:
"count_quick (l1 @ l2) = count_quick l1 + count_quick l2"
  by (induction l1) (auto split:line.splits)

lemma and_each_preserves_no_quick:
  assumes "no_quick rs"
    shows "no_quick (and_each m rs)"
  using assms
  by (induction rs) (auto split:line.splits simp:is_quick_rule_cases)

lemma remove_quick_ok:
  assumes "no_anchors rules"
  shows "no_quick (remove_quick rules)"
  using assms
  by (induction rules rule:remove_quick.induct)
     (auto simp: and_each_preserves_no_quick)

lemma remove_quick_preserves_no_anchors :
  assumes "no_anchors rules"
  shows "no_anchors (remove_quick rules)"
  using assms by(induction rules rule:remove_quick.induct)
                (auto simp:and_each_preserves_no_anchors)

lemma no_quick_preliminary:
  assumes "no_quick rules"
      and "no_anchors rules" (* not necessary but makes things easier *)
    shows "is_Preliminary (filter' rules \<gamma> p (Preliminary d))"
  using assms
proof(induction rules arbitrary: d)
  case Nil
  then show ?case by simp
next
  case (Cons a rules)
  then show ?case
  proof(cases a)
    case (PfRule r)
    then show ?thesis
    proof(cases "matches \<gamma> (pf_rule.get_match r) p")
      case True
      have nq:"no_quick rules" using Cons by simp
      have na:"no_anchors rules" using Cons by simp
      have "\<not>get_quick r" using Cons PfRule by auto
      then show ?thesis using True nq na Cons PfRule by simp
    next
      case False
      then show ?thesis using PfRule Cons by auto
    qed
  next
    case (Anchor r b)
    then show ?thesis using Cons by auto
  qed
qed

lemma remove_quick_preserves_semantics:
  assumes "no_anchors rules"
  shows "pf rules \<gamma> p = pf (remove_quick rules) \<gamma> p"
proof(-)
  have "(unwrap_decision (filter' rules \<gamma> p d) = unwrap_decision (filter' (remove_quick rules) \<gamma> p d))" for d
    using assms
  proof(induction rules arbitrary:d rule:remove_quick.induct)
  case 1
  then show ?case by simp
  next
    case (2 r ls)
    then show ?case
    proof(cases d)
      case (Final x1)
      then show ?thesis by auto
    next
      case (Preliminary x2)
      then show ?thesis
      proof(cases "get_quick r")
        case quick:True
        then show ?thesis
        proof(cases "matches \<gamma> (pf_rule.get_match r) p")
          case match:True
          then show ?thesis using 2 Preliminary quick by (simp add:filter_chain)
        next
          case nomatch:False
          then show ?thesis using 2 Preliminary by simp
        qed
      next
        case False
        then show ?thesis using 2 Preliminary by auto
      qed
    qed
  next
  case (3 vb vc va)
    then show ?case by auto
  qed
  then show ?thesis by (simp add:pf_def)
qed

(* remove matches *)

fun remove_matches :: "'a ruleset \<Rightarrow> 'a ruleset" where
"remove_matches [] = []" |
"remove_matches ((PfRule r)#ls) =
(if ((pf_rule.get_action r) = ActionMatch)
  then remove_matches ls
  else (PfRule r)#remove_matches ls)" |
"remove_matches (l#ls) = l#(remove_matches ls)"

lemma remove_matches_ok:
"no_match (remove_matches rs)"
  by(induction rs rule:remove_matches.induct) auto

lemma remove_matches_preserves_semantics:
  assumes "no_quick rs"
      and "no_anchors rs"
    shows "pf rs \<gamma> p = pf (remove_matches rs) \<gamma> p"
proof(-)
  have "\<And>d. filter' rs \<gamma> p (Preliminary d) = filter' (remove_matches rs) \<gamma> p (Preliminary d)"
  using assms
    by (induction rs rule: remove_matches.induct) simp+
  then show ?thesis by (simp add:pf_def)
qed

end

author: Sohalt

repo: pf-verification


text:
(*<*)
theory Event_Data
  imports
    "HOL-Library.Char_ord"
    Code_Double
    Deriving.Derive
begin
(*>*)

section \<open>Code adaptation for 8-bit strings\<close>

typedef string8 = "UNIV :: char list set" ..

setup_lifting type_definition_string8

lift_definition string8_literal :: "String.literal \<Rightarrow> string8" is String.explode .
declare [[coercion string8_literal]]

instantiation string8 :: "{equal, linorder}"
begin

lift_definition equal_string8 :: "string8 \<Rightarrow> string8 \<Rightarrow> bool" is HOL.equal .
lift_definition less_eq_string8 :: "string8 \<Rightarrow> string8 \<Rightarrow> bool" is ord_class.lexordp_eq .
lift_definition less_string8 :: "string8 \<Rightarrow> string8 \<Rightarrow> bool" is ord_class.lexordp .

instance by intro_classes
    (transfer; auto simp: equal_eq lexordp_conv_lexordp_eq lexordp_eq_linear
      intro: lexordp_eq_refl lexordp_eq_trans lexordp_eq_antisym)+

end

lifting_forget string8.lifting

declare [[code drop: string8_literal "HOL.equal :: string8 \<Rightarrow> _"
      "(\<le>) :: string8 \<Rightarrow> _" "(<) :: string8 \<Rightarrow> _"
      "Code_Evaluation.term_of :: string8 \<Rightarrow> _"]]

code_printing
  type_constructor string8 \<rightharpoonup> (OCaml) "string"
  | constant "HOL.equal :: string8 \<Rightarrow> string8 \<Rightarrow> bool" \<rightharpoonup> (OCaml) "Stdlib.(=)"
  | constant "(\<le>) :: string8 \<Rightarrow> string8 \<Rightarrow> bool" \<rightharpoonup> (OCaml) "Stdlib.(<=)"
  | constant "(<) :: string8 \<Rightarrow> string8 \<Rightarrow> bool" \<rightharpoonup> (OCaml) "Stdlib.(<)"

ML \<open>
structure String8 =
struct
  fun to_term x = @{term Abs_string8} $ HOLogic.mk_string x;
end;
\<close>

code_printing
  type_constructor string8 \<rightharpoonup> (Eval) "string"
  | constant "string8_literal :: String.literal \<Rightarrow> string8" \<rightharpoonup> (Eval) "_"
  | constant "HOL.equal :: string8 \<Rightarrow> string8 \<Rightarrow> bool" \<rightharpoonup> (Eval) infixl 6 "="
  | constant "(\<le>) :: string8 \<Rightarrow> string8 \<Rightarrow> bool" \<rightharpoonup> (Eval) infixl 6 "<="
  | constant "(<) :: string8 \<Rightarrow> string8 \<Rightarrow> bool" \<rightharpoonup> (Eval) infixl 6 "<"
  | constant "Code_Evaluation.term_of :: string8 \<Rightarrow> term" \<rightharpoonup> (Eval) "String8.to'_term"

derive (eq) ceq string8
derive (linorder) compare string8
derive (compare) ccompare string8

section \<open>Event parameters\<close>

definition div_to_zero :: "integer \<Rightarrow> integer \<Rightarrow> integer" where
  "div_to_zero x y = (let z = fst (Code_Numeral.divmod_abs x y) in
    if (x < 0) \<noteq> (y < 0) then - z else z)"

definition mod_to_zero :: "integer \<Rightarrow> integer \<Rightarrow> integer" where
  "mod_to_zero x y = (let z = snd (Code_Numeral.divmod_abs x y) in
    if x < 0 then - z else z)"

lemma "b \<noteq> 0 \<Longrightarrow> div_to_zero a b * b + mod_to_zero a b = a"
  unfolding div_to_zero_def mod_to_zero_def Let_def
  by (auto simp: minus_mod_eq_mult_div[symmetric] div_minus_right mod_minus_right ac_simps)

datatype event_data = EInt integer | EFloat double | EString string8

derive (eq) ceq event_data
derive ccompare event_data

instantiation event_data :: "{ord, plus, minus, uminus, times, divide, modulo}"
begin

fun less_eq_event_data where
  "EInt x \<le> EInt y \<longleftrightarrow> x \<le> y"
| "EInt x \<le> EFloat y \<longleftrightarrow> double_of_integer x \<le> y"
| "EInt _ \<le> EString _ \<longleftrightarrow> False"
| "EFloat x \<le> EInt y \<longleftrightarrow> x \<le> double_of_integer y"
| "EFloat x \<le> EFloat y \<longleftrightarrow> x \<le> y"
| "EFloat _ \<le> EString _ \<longleftrightarrow> False"
| "EString x \<le> EString y \<longleftrightarrow> x \<le> y"
| "EString _ \<le> _ \<longleftrightarrow> False"

definition less_event_data :: "event_data \<Rightarrow> event_data \<Rightarrow> bool"  where
  "less_event_data x y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"

fun plus_event_data where
  "EInt x + EInt y = EInt (x + y)"
| "EInt x + EFloat y = EFloat (double_of_integer x + y)"
| "EFloat x + EInt y = EFloat (x + double_of_integer y)"
| "EFloat x + EFloat y = EFloat (x + y)"
| "(_::event_data) + _ = EFloat nan"

fun minus_event_data where
  "EInt x - EInt y = EInt (x - y)"
| "EInt x - EFloat y = EFloat (double_of_integer x - y)"
| "EFloat x - EInt y = EFloat (x - double_of_integer y)"
| "EFloat x - EFloat y = EFloat (x - y)"
| "(_::event_data) - _ = EFloat nan"

fun uminus_event_data where
  "- EInt x = EInt (- x)"
| "- EFloat x = EFloat (- x)"
| "- (_::event_data) = EFloat nan"

fun times_event_data where
  "EInt x * EInt y = EInt (x * y)"
| "EInt x * EFloat y = EFloat (double_of_integer x * y)"
| "EFloat x * EInt y = EFloat (x * double_of_integer y)"
| "EFloat x * EFloat y = EFloat (x * y)"
| "(_::event_data) * _ = EFloat nan"

fun divide_event_data where
  "EInt x div EInt y = EInt (div_to_zero x y)"
| "EInt x div EFloat y = EFloat (double_of_integer x div y)"
| "EFloat x div EInt y = EFloat (x div double_of_integer y)"
| "EFloat x div EFloat y = EFloat (x div y)"
| "(_::event_data) div _ = EFloat nan"

fun modulo_event_data where
  "EInt x mod EInt y = EInt (mod_to_zero x y)"
| "(_::event_data) mod _ = EFloat nan"

instance ..

end

primrec integer_of_event_data :: "event_data \<Rightarrow> integer" where
  "integer_of_event_data (EInt x) = x"
| "integer_of_event_data (EFloat x) = integer_of_double x"
| "integer_of_event_data (EString _) = 0"

primrec double_of_event_data :: "event_data \<Rightarrow> double" where
  "double_of_event_data (EInt x) = double_of_integer x"
| "double_of_event_data (EFloat x) = x"
| "double_of_event_data (EString _) = nan"

(*<*)
end
(*>*)

author: EmanueleFWM

repo: verimon-optimized-aggregations