text:
section "Undirected Graphs as symmetric directed graphs"

theory Graph_Definition
  imports
    Dijkstra_Shortest_Path.Graph
    Dijkstra_Shortest_Path.Weight
begin

subsection \<open>Definition\<close>

fun is_path_undir :: "('v, 'w) graph \<Rightarrow> 'v \<Rightarrow> ('v,'w) path \<Rightarrow> 'v \<Rightarrow> bool" where
    "is_path_undir G v [] v' \<longleftrightarrow> v=v' \<and> v'\<in>nodes G" |
    "is_path_undir G v ((v1,w,v2)#p) v'
       \<longleftrightarrow> v=v1 \<and> ((v1,w,v2)\<in>edges G \<or> (v2,w,v1)\<in>edges G) \<and> is_path_undir G v2 p v'"

abbreviation "nodes_connected G a b \<equiv> \<exists>p. is_path_undir G a p b"

definition degree :: "('v, 'w) graph \<Rightarrow> 'v \<Rightarrow> nat" where
  "degree G v = card {e\<in>edges G. fst e = v \<or> snd (snd e) = v}"

locale forest = valid_graph G
  for G :: "('v,'w) graph" +
  assumes cycle_free:
    "\<forall>(a,w,b)\<in>E. \<not> nodes_connected (delete_edge a w b G) a b"

locale connected_graph = valid_graph G
  for G :: "('v,'w) graph" +
  assumes connected:
    "\<forall>v\<in>V. \<forall>v'\<in>V. nodes_connected G v v'"

locale tree = forest + connected_graph

locale finite_graph = valid_graph G
  for G :: "('v,'w) graph" +
  assumes finite_E: "finite E" and
    finite_V: "finite V"

locale finite_weighted_graph = finite_graph G
  for G :: "('v,'w::weight) graph"

definition subgraph :: "('v, 'w) graph \<Rightarrow> ('v, 'w) graph \<Rightarrow> bool" where
  "subgraph G H \<equiv> nodes G = nodes H \<and> edges G \<subseteq> edges H"

definition edge_weight :: "('v, 'w) graph \<Rightarrow> 'w::weight" where
  "edge_weight G \<equiv> sum (fst o snd) (edges G)"

definition edges_less_eq :: "('a \<times> 'w::weight \<times> 'a) \<Rightarrow> ('a \<times> 'w \<times> 'a) \<Rightarrow> bool"
  where "edges_less_eq a b \<equiv> fst(snd a) \<le> fst(snd b)"

definition maximally_connected :: "('v, 'w) graph \<Rightarrow> ('v, 'w) graph \<Rightarrow> bool" where
  "maximally_connected H G \<equiv> \<forall>v\<in>nodes G. \<forall>v'\<in>nodes G.
    (nodes_connected G v v') \<longrightarrow> (nodes_connected H v v')"

definition spanning_forest :: "('v, 'w) graph \<Rightarrow> ('v, 'w) graph \<Rightarrow> bool" where
  "spanning_forest F G \<equiv> forest F \<and> maximally_connected F G \<and> subgraph F G"

definition optimal_forest :: "('v, 'w::weight) graph \<Rightarrow> ('v, 'w) graph \<Rightarrow> bool" where
  "optimal_forest F G \<equiv> (\<forall>F'::('v, 'w) graph.
      spanning_forest F' G \<longrightarrow> edge_weight F \<le> edge_weight F')"

definition minimum_spanning_forest :: "('v, 'w::weight) graph \<Rightarrow> ('v, 'w) graph \<Rightarrow> bool" where
  "minimum_spanning_forest F G \<equiv> spanning_forest F G \<and> optimal_forest F G"

definition spanning_tree :: "('v, 'w) graph \<Rightarrow> ('v, 'w) graph \<Rightarrow> bool" where
  "spanning_tree F G \<equiv> tree F \<and> subgraph F G"

definition optimal_tree :: "('v, 'w::weight) graph \<Rightarrow> ('v, 'w) graph \<Rightarrow> bool" where
  "optimal_tree F G \<equiv> (\<forall>F'::('v, 'w) graph.
      spanning_tree F' G \<longrightarrow> edge_weight F \<le> edge_weight F')"

definition minimum_spanning_tree :: "('v, 'w::weight) graph \<Rightarrow> ('v, 'w) graph \<Rightarrow> bool" where
  "minimum_spanning_tree F G \<equiv> spanning_tree F G \<and> optimal_tree F G"

subsection \<open>Helping lemmas\<close>

lemma nodes_delete_edge[simp]:
  "nodes (delete_edge v e v' G) = nodes G"
  by (simp add: delete_edge_def)

lemma edges_delete_edge[simp]:
  "edges (delete_edge v e v' G) = edges G - {(v,e,v')}"
  by (simp add: delete_edge_def)

lemma subgraph_node:
  assumes "subgraph H G"
  shows "v \<in> nodes G \<longleftrightarrow> v \<in> nodes H"
  using assms
  unfolding subgraph_def
  by simp

lemma delete_add_edge:
  assumes "a \<in> nodes H"
  assumes "c \<in> nodes H"
  assumes "(a, w, c) \<notin> edges H"
  shows "delete_edge a w c (add_edge a w c H) = H"
  using assms unfolding delete_edge_def add_edge_def
  by (simp add: insert_absorb)

lemma swap_delete_add_edge:
  assumes "(a, b, c) \<noteq> (x, y, z)"
  shows "delete_edge a b c (add_edge x y z H) = add_edge x y z (delete_edge a b c H)"
  using assms unfolding delete_edge_def add_edge_def
  by auto

lemma swap_delete_edges: "delete_edge a b c (delete_edge x y z H)
           = delete_edge x y z (delete_edge a b c H)"
  unfolding delete_edge_def
  by auto

context valid_graph
begin
  lemma valid_subgraph:
    assumes "subgraph H G"
    shows "valid_graph H"
    using assms E_valid unfolding subgraph_def valid_graph_def
    by blast

  lemma is_path_undir_simps[simp, intro!]:
    "is_path_undir G v [] v \<longleftrightarrow> v\<in>V"
    "is_path_undir G v [(v,w,v')] v' \<longleftrightarrow> (v,w,v')\<in>E \<or> (v',w,v)\<in>E"
    by (auto dest: E_validD)

  lemma is_path_undir_memb[simp]:
    "is_path_undir G v p v' \<Longrightarrow> v\<in>V \<and> v'\<in>V"
    apply (induct p arbitrary: v)
     apply (auto dest: E_validD)
    done

  lemma is_path_undir_memb_edges:
    assumes "is_path_undir G v p v'"
    shows "\<forall>(a,w,b) \<in> set p. (a,w,b) \<in> E \<or> (b,w,a) \<in> E"
    using assms
    by (induct p arbitrary: v) fastforce+

  lemma is_path_undir_split:
    "is_path_undir G v (p1@p2) v' \<longleftrightarrow> (\<exists>u. is_path_undir G v p1 u \<and> is_path_undir G u p2 v')"
    by (induct p1 arbitrary: v) auto

  lemma is_path_undir_split'[simp]:
    "is_path_undir G v (p1@(u,w,u')#p2) v'
      \<longleftrightarrow> is_path_undir G v p1 u \<and> ((u,w,u')\<in>E \<or> (u',w,u)\<in>E) \<and> is_path_undir G u' p2 v'"
    by (auto simp add: is_path_undir_split)

  lemma is_path_undir_sym:
    assumes "is_path_undir G v p v'"
    shows "is_path_undir G v' (rev (map (\<lambda>(u, w, u'). (u', w, u)) p)) v"
    using assms
    by (induct p arbitrary: v) (auto simp: E_validD)

  lemma is_path_undir_subgraph:
    assumes "is_path_undir H x p y"
    assumes "subgraph H G"
    shows "is_path_undir G x p y"
    using assms is_path_undir.simps
    unfolding subgraph_def
    by (induction p arbitrary: x y) auto

  lemma no_path_in_empty_graph:
    assumes "E = {}"
    assumes "p \<noteq> []"
    shows "\<not>is_path_undir G v p v"
    using assms by (cases p) auto

  lemma is_path_undir_split_distinct:
    assumes "is_path_undir G v p v'"
    assumes "(a, w, b) \<in> set p \<or> (b, w, a) \<in> set p"
    shows "(\<exists>p' p'' u u'.
            is_path_undir G v p' u \<and> is_path_undir G u' p'' v' \<and>
            length p' < length p \<and> length p'' < length p \<and>
            (u \<in> {a, b} \<and> u' \<in> {a, b}) \<and>
            (a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and>
            (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p'')"
    using assms
  proof (induction n == "length p" arbitrary: p v v' rule: nat_less_induct)
    case 1
    then obtain u u' where "(u, w, u') \<in> set p" and u: "u \<in> {a, b} \<and> u' \<in> {a, b}"
      by blast
    with split_list obtain p' p''
      where p: "p = p' @ (u, w, u') # p''"
      by fast
    then have len_p': "length p' < length p" and len_p'': "length p'' < length p"
      by auto
    from 1 p have p': "is_path_undir G v p' u" and p'': "is_path_undir G u' p'' v'"
      by auto
    from 1 len_p' p' have "(a, w, b) \<in> set p' \<or> (b, w, a) \<in> set p' \<longrightarrow> (\<exists>p'2 u2.
            is_path_undir G v p'2 u2 \<and>
            length p'2 < length p' \<and>
            u2 \<in> {a, b} \<and>
            (a, w, b) \<notin> set p'2 \<and> (b, w, a) \<notin> set p'2)"
      by metis
    with len_p' p' u have p': "\<exists>p' u. is_path_undir G v p' u \<and> length p' < length p \<and>
      u \<in> {a,b} \<and> (a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p'"
      by fastforce
    from 1 len_p'' p'' have "(a, w, b) \<in> set p'' \<or> (b, w, a) \<in> set p'' \<longrightarrow> (\<exists>p''2 u'2.
            is_path_undir G u'2 p''2 v' \<and>
            length p''2 < length p'' \<and>
            u'2 \<in> {a, b} \<and>
            (a, w, b) \<notin> set p''2 \<and> (b, w, a) \<notin> set p''2)"
      by metis
    with len_p'' p'' u have "\<exists>p'' u'. is_path_undir G u' p'' v'\<and> length p'' < length p \<and>
      u' \<in> {a,b} \<and> (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''"
      by fastforce
    with p' show ?case by auto
  qed

  lemma add_edge_is_path:
    assumes "is_path_undir G x p y"
    shows "is_path_undir (add_edge a b c G) x p y"
  proof -
    from E_valid have "valid_graph (add_edge a b c G)"
      unfolding valid_graph_def add_edge_def
      by auto
    with assms is_path_undir.simps[of "add_edge a b c G"]
    show "is_path_undir (add_edge a b c G) x p y"
      by (induction p arbitrary: x y) auto
  qed

  lemma add_edge_was_path:
    assumes "is_path_undir (add_edge a b c G) x p y"
    assumes "(a, b, c) \<notin> set p"
    assumes "(c, b, a) \<notin> set p"
    assumes "a \<in> V"
    assumes "c \<in> V"
    shows "is_path_undir G x p y"
  proof -
    from E_valid have "valid_graph (add_edge a b c G)"
      unfolding valid_graph_def add_edge_def
      by auto
    with assms is_path_undir.simps[of "add_edge a b c G"]
    show "is_path_undir G x p y"
      by (induction p arbitrary: x y) auto
  qed

  lemma delete_edge_is_path:
    assumes "is_path_undir G x p y"
    assumes "(a, b, c) \<notin> set p"
    assumes "(c, b, a) \<notin> set p"
    shows "is_path_undir (delete_edge a b c G) x p y"
  proof -
    from E_valid have "valid_graph (delete_edge a b c G)"
      unfolding valid_graph_def delete_edge_def
      by auto
    with assms is_path_undir.simps[of "delete_edge a b c G"]
    show ?thesis
      by (induction p arbitrary: x y) auto
  qed

  lemma delete_node_is_path:
    assumes "is_path_undir G x p y"
    assumes "x \<noteq> v"
    assumes "v \<notin> fst`set p \<union> snd`snd`set p"
    shows "is_path_undir (delete_node v G) x p y"
    using assms
    unfolding delete_node_def
    by (induction p arbitrary: x y) auto

  lemma subset_was_path:
    assumes "is_path_undir H x p y"
    assumes "edges H \<subseteq> E"
    assumes "nodes H \<subseteq> V"
    shows "is_path_undir G x p y"
    using assms
    by (induction p arbitrary: x y) auto

  lemma delete_node_was_path:
    assumes "is_path_undir (delete_node v G) x p y"
    shows "is_path_undir G x p y"
    using assms
    unfolding delete_node_def
    by (induction p arbitrary: x y) auto

  lemma add_edge_preserve_subgraph:
    assumes "subgraph H G"
    assumes "(a, w, b) \<in> E"
    shows "subgraph (add_edge a w b H) G"
  proof -
    from assms E_validD have "a \<in> nodes H \<and> b \<in> nodes H"
      unfolding subgraph_def by simp
    with assms show ?thesis
      unfolding subgraph_def
      by auto
  qed

  lemma delete_edge_preserve_subgraph:
    assumes "subgraph H G"
    shows "subgraph (delete_edge a w b H) G"
    using assms
    unfolding subgraph_def
    by auto

  lemma add_delete_edge:
    assumes "(a, w, c) \<in> E"
    shows "add_edge a w c (delete_edge a w c G) = G"
    using assms E_validD unfolding delete_edge_def add_edge_def
    by (simp add: insert_absorb)

  lemma swap_add_edge_in_path:
    assumes "is_path_undir (add_edge a w b G) v p v'"
    assumes "(a,w',a') \<in> E \<or> (a',w',a) \<in> E"
    shows "\<exists>p. is_path_undir (add_edge a' w'' b G) v p v'"
  using assms(1)
  proof (induction p arbitrary: v)
    case Nil
    with assms(2) E_validD
    have "is_path_undir (add_edge a' w'' b G) v [] v'"
      by auto
    then show ?case
      by blast
  next
    case (Cons e p')
    then obtain v2 x e_w where "e = (v2, e_w, x)"
      using prod_cases3 by blast
    with Cons(2)
    have e: "e = (v, e_w, x)" and
         edge_e: "(v, e_w, x) \<in> edges (add_edge a w b G)
                   \<or> (x, e_w, v) \<in> edges (add_edge a w b G)" and
         p': "is_path_undir (add_edge a w b G) x p' v'"
      by auto
    have "\<exists>p. is_path_undir (add_edge a' w'' b G) v p x"
    proof (cases "e = (a, w, b) \<or> e = (b, w, a)")
      case True
      from True e assms(2) E_validD
      have "is_path_undir (add_edge a' w'' b G) v [(a,w',a'), (a',w'',b)] x
          \<or> is_path_undir (add_edge a' w'' b G) v [(b,w'',a'), (a',w',a)] x"
        by auto
      then show ?thesis
        by blast
    next
      case False
      with edge_e e
      have "is_path_undir (add_edge a' w'' b G) v [e] x"
        by (auto simp: E_validD)
      then show ?thesis
        by auto
    qed
    with p' Cons.IH
     and valid_graph.is_path_undir_split[OF add_edge_valid[OF valid_graph.intro[OF E_valid]]]
    show ?case
      by blast
  qed

  lemma induce_maximally_connected:
    assumes "subgraph H G"
    assumes "\<forall>(a,w,b)\<in>E. nodes_connected H a b"
    shows "maximally_connected H G"
  proof -
    from valid_subgraph[OF \<open>subgraph H G\<close>]
    have valid_H: "valid_graph H" .
    have "(nodes_connected G v v') \<longrightarrow> (nodes_connected H v v')" (is "?lhs \<longrightarrow> ?rhs")
      if "v\<in>V" and "v'\<in>V" for v v'
    proof
      assume ?lhs
      then obtain p where "is_path_undir G v p v'"
        by blast
      then show ?rhs
      proof (induction p arbitrary: v v')
        case Nil
        with subgraph_node[OF assms(1)] show ?case
          by (metis is_path_undir.simps(1))
      next
        case (Cons e p)
        from prod_cases3 obtain a w b where awb: "e = (a, w, b)" .
        with assms Cons.prems valid_graph.is_path_undir_sym[OF valid_H, of b _ a]
        obtain p' where p': "is_path_undir H a p' b"
          by fastforce
        from assms awb Cons.prems Cons.IH[of b v']
        obtain p'' where "is_path_undir H b p'' v'"
          unfolding subgraph_def by auto
        with Cons.prems awb assms p' valid_graph.is_path_undir_split[OF valid_H]
          have "is_path_undir H v (p'@p'') v'"
            by auto
        then show ?case ..
      qed
    qed
    with assms show ?thesis
      unfolding maximally_connected_def
      by auto
  qed

  lemma add_edge_maximally_connected:
    assumes "maximally_connected H G"
    assumes "subgraph H G"
    assumes "(a, w, b) \<in> E"
    shows "maximally_connected (add_edge a w b H) G"
  proof -
    have "(nodes_connected G v v') \<longrightarrow> (nodes_connected (add_edge a w b H) v v')"
      (is "?lhs \<longrightarrow> ?rhs") if vv': "v \<in> V" "v' \<in> V" for v v'
    proof
      assume ?lhs
      with \<open>maximally_connected H G\<close> vv' obtain p where "is_path_undir H v p v'"
        unfolding maximally_connected_def
        by auto
      with valid_graph.add_edge_is_path[OF valid_subgraph[OF \<open>subgraph H G\<close>] this]
      show ?rhs
        by auto
    qed
    then show ?thesis
      unfolding maximally_connected_def
      by auto
  qed

  lemma delete_edge_maximally_connected:
    assumes "maximally_connected H G"
    assumes "subgraph H G"
    assumes pab: "is_path_undir (delete_edge a w b H) a pab b"
    shows "maximally_connected (delete_edge a w b H) G"
  proof -
    from valid_subgraph[OF \<open>subgraph H G\<close>]
    have valid_H: "valid_graph H" .
    have "(nodes_connected G v v') \<longrightarrow> (nodes_connected (delete_edge a w b H) v v')"
      (is "?lhs \<longrightarrow> ?rhs") if vv': "v \<in> V" "v' \<in> V" for v v'
    proof
      assume ?lhs
      with \<open>maximally_connected H G\<close> vv' obtain p where p: "is_path_undir H v p v'"
        unfolding maximally_connected_def
        by auto
      show ?rhs
      proof (cases "(a, w, b) \<in> set p \<or> (b, w, a) \<in> set p")
        case True
        with p valid_graph.is_path_undir_split_distinct[OF valid_H p, of a w b] obtain p' p'' u u'
          where "is_path_undir H v p' u \<and> is_path_undir H u' p'' v'" and
            u: "(u \<in> {a, b} \<and> u' \<in> {a, b})" and
            "(a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and>
            (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p''"
          by auto
        with valid_graph.delete_edge_is_path[OF valid_H] obtain p' p''
          where p': "is_path_undir (delete_edge a w b H) v p' u \<and>
                 is_path_undir (delete_edge a w b H) u' p'' v'"
          by blast
        note dev_H = delete_edge_valid[OF valid_H]
        note * = valid_graph.is_path_undir_split[OF dev_H, of a w b v]
        from valid_graph.is_path_undir_sym[OF delete_edge_valid[OF valid_H] pab] obtain pab'
          where "is_path_undir (delete_edge a w b H) b pab' a"
          by auto
        with assms u p' valid_graph.is_path_undir_split[OF dev_H, of a w b v p' p'' v']
          *[of p' pab b] *[of "p'@pab" p'' v'] *[of p' pab' a] *[of "p'@pab'" p'' v']
        show ?thesis by auto
      next
        case False
        with valid_graph.delete_edge_is_path[OF valid_H p] show ?thesis
          by auto
      qed
    qed
    then show ?thesis
      unfolding maximally_connected_def
      by auto
  qed

  lemma connected_impl_maximally_connected:
    assumes "connected_graph H"
    assumes subgraph: "subgraph H G"
    shows "maximally_connected H G"
    using assms
    unfolding connected_graph_def connected_graph_axioms_def maximally_connected_def
      subgraph_def
    by blast

  lemma add_edge_is_connected:
    "nodes_connected (add_edge a b c G) a c"
    "nodes_connected (add_edge a b c G) c a"
  using valid_graph.is_path_undir_simps(2)[OF
        add_edge_valid[OF valid_graph_axioms], of a b c a b c]
      valid_graph.is_path_undir_simps(2)[OF
        add_edge_valid[OF valid_graph_axioms], of a b c c b a]
  by fastforce+

  lemma swap_edges:
    assumes "nodes_connected (add_edge a w b G) v v'"
    assumes "a \<in> V"
    assumes "b \<in> V"
    assumes "\<not> nodes_connected G v v'"
    shows "nodes_connected (add_edge v w' v' G) a b"
  proof -
    from assms(1) obtain p where p: "is_path_undir (add_edge a w b G) v p v'"
      by auto
    have awb: "(a, w, b) \<in> set p \<or> (b, w, a) \<in> set p"
    proof (rule ccontr)
      assume "\<not> ((a, w, b) \<in> set p \<or> (b, w, a) \<in> set p)"
      with add_edge_was_path[OF p _ _ assms(2,3)] assms(4)
      show False
        by auto
    qed
    from valid_graph.is_path_undir_split_distinct[OF
        add_edge_valid[OF valid_graph_axioms] p awb]
    obtain p' p'' u u' where
         "is_path_undir (add_edge a w b G) v p' u \<and>
          is_path_undir (add_edge a w b G) u' p'' v'" and
          u: "u \<in> {a, b} \<and> u' \<in> {a, b}" and
          "(a, w, b) \<notin> set p' \<and> (b, w, a) \<notin> set p' \<and>
          (a, w, b) \<notin> set p'' \<and> (b, w, a) \<notin> set p'' "
      by auto
    with assms(2,3) add_edge_was_path
    have paths: "is_path_undir G v p' u \<and>
                 is_path_undir G u' p'' v'"
      by blast
    with is_path_undir_split[of v p' p'' v'] assms(4)
    have "u \<noteq> u'"
      by blast
    from paths assms add_edge_is_path
    have paths': "is_path_undir (add_edge v w' v' G) v p' u \<and>
                  is_path_undir (add_edge v w' v' G) u' p'' v'"
      by blast
    note * = add_edge_valid[OF valid_graph_axioms]
    from add_edge_is_connected obtain p''' where
      "is_path_undir (add_edge v w' v' G) v' p''' v"
      by blast
    with paths' valid_graph.is_path_undir_split[OF *, of v w' v' u' p'' p''' v]
    have "is_path_undir (add_edge v w' v' G) u' (p''@p''') v"
        by auto
    with paths' valid_graph.is_path_undir_split[OF *, of v w' v' u' "p''@p'''" p' u]
    have "is_path_undir (add_edge v w' v' G) u' (p''@p'''@p') u"
        by auto
    with u \<open>u \<noteq> u'\<close> valid_graph.is_path_undir_sym[OF * this]
    show ?thesis
      by auto
  qed

  lemma subgraph_impl_connected:
    assumes "connected_graph H"
    assumes subgraph: "subgraph H G"
    shows "connected_graph G"
    using assms is_path_undir_subgraph[OF _ subgraph] valid_graph_axioms
    unfolding connected_graph_def connected_graph_axioms_def maximally_connected_def
      subgraph_def
    by blast

  lemma add_node_connected:
    assumes "\<forall>a\<in>V - {v}. \<forall>b\<in>V - {v}. nodes_connected G a b"
    assumes "(v, w, v') \<in> E \<or> (v', w, v) \<in> E"
    assumes "v \<noteq> v'"
    shows "\<forall>a\<in>V. \<forall>b\<in>V. nodes_connected G a b"
  proof -
    have "nodes_connected G a b" if a: "a\<in>V" and b: "b\<in>V" for a b
    proof (cases "a = v")
      case True
      show ?thesis
      proof (cases "b = v")
        case True
        with \<open>a = v\<close> a is_path_undir_simps(1) show ?thesis
          by blast
      next
        case False
        from assms(2) have "v' \<in> V"
          by (auto simp: E_validD)
        with b assms(1) \<open>b \<noteq> v\<close> \<open>v \<noteq> v'\<close> have "nodes_connected G v' b"
          by blast
        with assms(2) \<open>a = v\<close> is_path_undir.simps(2)[of G v v w v' _ b]
        show ?thesis
          by blast
      qed
    next
      case False
      show ?thesis
      proof (cases "b = v")
        case True
        from assms(2) have "v' \<in> V"
          by (auto simp: E_validD)
        with a assms(1) \<open>a \<noteq> v\<close> \<open>v \<noteq> v'\<close> have "nodes_connected G a v'"
          by blast
        with assms(2) \<open>b = v\<close> is_path_undir.simps(2)[of G v v w v' _ a]
          is_path_undir_sym
        show ?thesis
          by blast
      next
        case False
        with \<open>a \<noteq> v\<close> assms(1) a b show ?thesis
          by simp
      qed
    qed
    then show ?thesis by simp
  qed
end

context connected_graph
begin
  lemma maximally_connected_impl_connected:
    assumes "maximally_connected H G"
    assumes subgraph: "subgraph H G"
    shows "connected_graph H"
    using assms connected_graph_axioms valid_subgraph[OF subgraph]
    unfolding connected_graph_def connected_graph_axioms_def maximally_connected_def
      subgraph_def
    by auto
end

context forest
begin

  lemmas delete_edge_valid' = delete_edge_valid[OF valid_graph_axioms]

  lemma delete_edge_from_path:
    assumes "nodes_connected G a b"
    assumes "subgraph H G"
    assumes "\<not> nodes_connected H a b"
    shows "\<exists>(x, w, y) \<in> E - edges H.  (\<not> nodes_connected (delete_edge x w y G) a b) \<and>
      (nodes_connected (add_edge a w' b (delete_edge x w y G)) x y)"
  proof -
    from assms(1) obtain p where "is_path_undir G a p b"
      by auto
    from this assms(3) show ?thesis
    proof (induction n == "length p" arbitrary: p a b rule: nat_less_induct)
      case 1
      from valid_subgraph[OF assms(2)] have valid_H: "valid_graph H" .
      show ?case
      proof (cases p)
        case Nil
        with 1(2) have "a = b"
          by simp
        with 1(2) assms(2) have "is_path_undir H a [] b"
          unfolding subgraph_def
          by auto
        with 1(3) show ?thesis
          by blast
      next
        case (Cons e p')
        obtain a2 a' w where "e = (a2, w, a')"
          using prod_cases3 by blast
        with 1(2) Cons have e: "e = (a, w, a')"
          by simp
        with 1(2) Cons obtain e1 e2 where e12: "e = (e1, w, e2) \<or> e = (e2, w, e1)" and
          edge_e12: "(e1, w, e2) \<in> E"
          by auto
        from 1(2) Cons e have "is_path_undir G a' p' b"
          by simp
        with is_path_undir_split_distinct[OF this, of a w a'] Cons
        obtain p'_dst u' where  p'_dst: "is_path_undir G u' p'_dst b \<and> u' \<in> {a, a'}" and
            e_not_in_p': "(a, w, a') \<notin> set p'_dst \<and> (a', w, a) \<notin> set p'_dst" and
            len_p': "length p'_dst < length p"
          by fastforce
        show ?thesis
        proof (cases "u' = a'")
          case False
          with 1 len_p' p'_dst show ?thesis
            by auto
        next
          case True
          with p'_dst have path_p': "is_path_undir G a' p'_dst b"
            by auto
          show ?thesis
          proof (cases "(e1, w, e2) \<in> edges H")
            case True
            have "\<not> nodes_connected H a' b"
            proof
              assume "nodes_connected H a' b"
              then obtain p_H where "is_path_undir H a' p_H b"
                by auto
              with True e12 e have "is_path_undir H a (e#p_H) b"
                by auto
              with 1(3) show False
                by simp
            qed
            with path_p' 1(1) len_p' obtain x z y where xy: "(x, z, y) \<in> E - edges H" and
              IH1: "(\<not>nodes_connected (delete_edge x z y G) a' b)" and
              IH2: "(nodes_connected (add_edge a' w' b (delete_edge x z y G)) x y)"
              by blast
            with True have xy_neq_e: "(x,z,y) \<noteq> (e1, w, e2)"
              by auto
            have thm1: "\<not> nodes_connected (delete_edge x z y G) a b"
            proof
              assume "nodes_connected (delete_edge x z y G) a b"
              then obtain p_e where "is_path_undir (delete_edge x z y G) a p_e b"
                by auto
              with edge_e12 e12 e xy_neq_e
              have "is_path_undir (delete_edge x z y G) a' ((a', w, a)#p_e) b"
                by auto
              with IH1 show False
                by blast
            qed
            from IH2 obtain p_xy
              where "is_path_undir (add_edge a' w' b (delete_edge x z y G)) x p_xy y"
              by auto
            from valid_graph.swap_add_edge_in_path[OF delete_edge_valid' this, of w a w'] edge_e12
              e12 e edges_delete_edge[of x z y G] xy_neq_e
            have thm2: "nodes_connected (add_edge a w' b (delete_edge x z y G)) x y"
              by blast
            with thm1 show ?thesis
              using xy by auto
          next
            case False
            have thm1: "\<not> nodes_connected (delete_edge e1 w e2 G) a b"
            proof
              assume "nodes_connected (delete_edge e1 w e2 G) a b"
              then obtain p_e where p_e: "is_path_undir (delete_edge e1 w e2 G) a p_e b"
                by auto
              from delete_edge_is_path[OF path_p', of e1 w e2] e_not_in_p' e12 e
              have "is_path_undir (delete_edge e1 w e2 G) a' p'_dst b"
                by auto
              with valid_graph.is_path_undir_sym[OF delete_edge_valid' this]
              obtain p_rev where "is_path_undir (delete_edge e1 w e2 G) b p_rev a'"
                by auto
              with p_e valid_graph.is_path_undir_split[OF delete_edge_valid']
              have "is_path_undir (delete_edge e1 w e2 G) a (p_e@p_rev) a'"
                by auto
              with cycle_free edge_e12 e12 e
                and valid_graph.is_path_undir_sym[OF delete_edge_valid' this]
              show False
                unfolding valid_graph_def
                by auto
            qed
            note ** = delete_edge_is_path[OF path_p', of e1 w e2]
            from valid_graph.is_path_undir_split[OF add_edge_valid[OF delete_edge_valid']]
              valid_graph.add_edge_is_path[OF delete_edge_valid' **, of a w' b]
              valid_graph.is_path_undir_simps(2)[OF add_edge_valid[OF delete_edge_valid'],
                                                 of a w' b e1 w e2 b w' a]
              e_not_in_p' e12 e
            have "is_path_undir (add_edge a w' b (delete_edge e1 w e2 G)) a' (p'_dst@[(b,w',a)]) a"
              by auto
            with valid_graph.is_path_undir_sym[OF add_edge_valid[OF delete_edge_valid'] this]
              e12 e
            have "nodes_connected (add_edge a w' b (delete_edge e1 w e2 G)) e1 e2"
              by blast
            with thm1 show ?thesis
              using False edge_e12 by auto
          qed
        qed
      qed
    qed
  qed

  lemma forest_add_edge:
    assumes "a \<in> V"
    assumes "b \<in> V"
    assumes "\<not> nodes_connected G a b"
    shows "forest (add_edge a w b G)"
  proof -
    from assms(3) have "\<not> is_path_undir G a [(a, w, b)] b"
      by blast
    with assms(2) have awb: "(a, w, b) \<notin> E \<and> (b, w, a) \<notin> E"
      by auto
    have "\<not> nodes_connected (delete_edge v w' v' (add_edge a w b G)) v v'"
       if e: "(v,w',v')\<in> edges (add_edge a w b G)" for v w' v'
    proof (cases "(v,w',v') = (a, w, b)")
      case True
      with assms awb delete_add_edge[of a G b w]
      show ?thesis by simp
    next
      case False
      with e have e': "(v,w',v')\<in> edges G"
        by auto
      show ?thesis
      proof
        assume asm: "nodes_connected (delete_edge v w' v' (add_edge a w b G)) v v'"
        with swap_delete_add_edge[OF False, of G]
          valid_graph.swap_edges[OF delete_edge_valid', of a w b v w' v' v v' w']
          add_delete_edge[OF e'] cycle_free assms(1,2) e'
        have "nodes_connected G a b"
          by force
        with assms show False
          by simp
      qed
    qed
    with cycle_free add_edge_valid[OF valid_graph_axioms] show ?thesis
      unfolding forest_def forest_axioms_def by auto
  qed

  lemma forest_subsets:
    assumes "valid_graph H"
    assumes "edges H \<subseteq> E"
    assumes "nodes H \<subseteq> V"
    shows "forest H"
  proof -
    have "\<not> nodes_connected (delete_edge a w b H) a b"
      if e: "(a, w, b)\<in>edges H" for a w b
    proof
      assume asm: "nodes_connected (delete_edge a w b H) a b"
      from \<open>edges H \<subseteq> E\<close>
      have edges: "edges (delete_edge a w b H) \<subseteq> edges (delete_edge a w b G)"
        by auto
      from \<open>nodes H \<subseteq> V\<close>
      have nodes: "nodes (delete_edge a w b H) \<subseteq> nodes (delete_edge a w b G)"
        by auto
      from asm valid_graph.subset_was_path[OF delete_edge_valid' _ edges nodes]
      have "nodes_connected (delete_edge a w b G) a b"
        by auto
      with cycle_free e \<open>edges H \<subseteq> E\<close> show False
        by blast
    qed
    with assms(1) show ?thesis
    unfolding forest_def forest_axioms_def
    by auto
  qed

  lemma subgraph_forest:
    assumes "subgraph H G"
    shows "forest H"
    using assms forest_subsets valid_subgraph
    unfolding subgraph_def
    by simp

  lemma forest_delete_edge: "forest (delete_edge a w c G)"
    using forest_subsets[OF delete_edge_valid']
    unfolding delete_edge_def
    by auto

  lemma forest_delete_node: "forest (delete_node n G)"
    using forest_subsets[OF delete_node_valid[OF valid_graph_axioms]]
    unfolding delete_node_def
    by auto
end

context finite_graph
begin

  lemma finite_subgraphs: "finite {T. subgraph T G}"
  proof -
    from finite_E have "finite {E'. E' \<subseteq> E}"
      by simp
    then have "finite {\<lparr>nodes = V, edges = E'\<rparr>| E'. E' \<subseteq> E}"
      by simp
    also have "{\<lparr>nodes = V, edges = E'\<rparr>| E'. E' \<subseteq> E} = {T. subgraph T G}"
      unfolding subgraph_def
      by (metis (mono_tags, lifting) old.unit.exhaust select_convs(1) select_convs(2) surjective)
    finally show ?thesis .
  qed

end

lemma minimum_spanning_forest_impl_tree:
  assumes "minimum_spanning_forest F G"
  assumes valid_G: "valid_graph G"
  assumes "connected_graph F"
  shows "minimum_spanning_tree F G"
  using assms valid_graph.connected_impl_maximally_connected[OF valid_G]
  unfolding minimum_spanning_forest_def minimum_spanning_tree_def
    spanning_forest_def spanning_tree_def tree_def
    optimal_forest_def optimal_tree_def
  by auto

lemma minimum_spanning_forest_impl_tree2:
  assumes "minimum_spanning_forest F G"
  assumes connected_G: "connected_graph G"
  shows "minimum_spanning_tree F G"
  using assms connected_graph.maximally_connected_impl_connected[OF connected_G]
    minimum_spanning_forest_impl_tree connected_graph.axioms(1)[OF connected_G]
  unfolding minimum_spanning_forest_def spanning_forest_def
  by auto

end


text:
(*  Title:      HOL/Auth/n_g2kAbsAfter_lemma_on_inv__16.thy
    Author:     Yongjian Li and Kaiqiang Duan, State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
    Copyright    2016 State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
*)

header{*The n_g2kAbsAfter Protocol Case Study*}

theory n_g2kAbsAfter_lemma_on_inv__16 imports n_g2kAbsAfter_base
begin
section{*All lemmas on causal relation between inv__16 and some rule r*}
lemma n_n_Store_i1Vsinv__16:
assumes a1: "(\<exists> d. d\<le>N\<and>r=n_n_Store_i1  d)" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain d where a1:"d\<le>N\<and>r=n_n_Store_i1  d" apply fastforce done
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Ident ''Cache_1'') ''State'')) (Const E)) (eqn (IVar (Field (Ident ''AChan2_1'') ''Cmd'')) (Const GntS))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_AStore_i1Vsinv__16:
assumes a1: "(\<exists> d. d\<le>N\<and>r=n_n_AStore_i1  d)" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain d where a1:"d\<le>N\<and>r=n_n_AStore_i1  d" apply fastforce done
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Ident ''AChan2_1'') ''Cmd'')) (Const GntS)) (eqn (IVar (Field (Ident ''ACache_1'') ''State'')) (Const E))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_ASendInvE_i1Vsinv__16:
assumes a1: "(r=n_n_ASendInvE_i1  )" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_ASendInvS_i1Vsinv__16:
assumes a1: "(r=n_n_ASendInvS_i1  )" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_ASendInvAck_i1Vsinv__16:
assumes a1: "(r=n_n_ASendInvAck_i1  )" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_ASendGntS_i1Vsinv__16:
assumes a1: "(r=n_n_ASendGntS_i1  )" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Ident ''ExGntd'')) (Const false)) (neg (eqn (IVar (Ident ''MemData'')) (IVar (Ident ''AuxData''))))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_ASendGntE_i1Vsinv__16:
assumes a1: "(r=n_n_ASendGntE_i1  )" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_ARecvGntS_i1Vsinv__16:
assumes a1: "(r=n_n_ARecvGntS_i1  )" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_ARecvGntE_i1Vsinv__16:
assumes a1: "(r=n_n_ARecvGntE_i1  )" and
a2: "(f=inv__16  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_n_RecvReq_i1Vsinv__16:
  assumes a1: "r=n_n_RecvReq_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendInvS_i1Vsinv__16:
  assumes a1: "r=n_n_SendInvS_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendReqEI_i1Vsinv__16:
  assumes a1: "r=n_n_SendReqEI_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_ASendReqEI_i1Vsinv__16:
  assumes a1: "r=n_n_ASendReqEI_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_ASendReqIS_j1Vsinv__16:
  assumes a1: "r=n_n_ASendReqIS_j1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendGntE_i1Vsinv__16:
  assumes a1: "r=n_n_SendGntE_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_ASendReqES_i1Vsinv__16:
  assumes a1: "r=n_n_ASendReqES_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendGntS_i1Vsinv__16:
  assumes a1: "r=n_n_SendGntS_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendReqES_i1Vsinv__16:
  assumes a1: "r=n_n_SendReqES_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendInvE_i1Vsinv__16:
  assumes a1: "r=n_n_SendInvE_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_ASendReqSE_j1Vsinv__16:
  assumes a1: "r=n_n_ASendReqSE_j1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_RecvGntS_i1Vsinv__16:
  assumes a1: "r=n_n_RecvGntS_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendReqEE_i1Vsinv__16:
  assumes a1: "r=n_n_SendReqEE_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_RecvInvAck_i1Vsinv__16:
  assumes a1: "r=n_n_RecvInvAck_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_RecvGntE_i1Vsinv__16:
  assumes a1: "r=n_n_RecvGntE_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_ARecvReq_i1Vsinv__16:
  assumes a1: "r=n_n_ARecvReq_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendReqS_j1Vsinv__16:
  assumes a1: "r=n_n_SendReqS_j1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_ARecvInvAck_i1Vsinv__16:
  assumes a1: "r=n_n_ARecvInvAck_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_n_SendInvAck_i1Vsinv__16:
  assumes a1: "r=n_n_SendInvAck_i1  " and
  a2: "(f=inv__16  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

end

repo: newParaVerifier


text:
theory Tables_real
imports Amortized_Complexity.Amortized_Framework0
begin

(* Final version with l :: real *)

fun \<Psi> :: "bool \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real" where
"\<Psi> b i d x\<^sub>1 x\<^sub>2 n = (if n \<ge> x\<^sub>2 then i*(n - x\<^sub>2) else
  if n \<le> x\<^sub>1 \<and> b then d*(x\<^sub>1 - n) else 0)"

declare of_nat_Suc[simp] of_nat_diff[simp]

text\<open>An automatic proof:\<close>
lemma Psi_diff_Ins:
  "0 < i \<Longrightarrow> 0 < d \<Longrightarrow> \<Psi> b i d x\<^sub>1 x\<^sub>2 (Suc n) - \<Psi> b i d x\<^sub>1 x\<^sub>2 n \<le> i"
by (simp add: add_mono algebra_simps)

lemma assumes [arith]: "0 < i" "0 \<le> d"
shows "\<Psi> b i d x\<^sub>1 x\<^sub>2 (n+1) - \<Psi> b i d x\<^sub>1 x\<^sub>2 n \<le> i" (is "?D \<le> _")
proof cases
  assume "n \<ge> x\<^sub>2"
  hence "?D = i*(n+1-x\<^sub>2) - i*(n-x\<^sub>2)" by (simp)
  also have "\<dots> = i" by (simp add: algebra_simps)
  finally show ?thesis by simp
next
  assume [arith]: "\<not> n \<ge> x\<^sub>2"
  show ?thesis
  proof cases
    assume *[arith]: "n \<le> x\<^sub>1 \<and> b"
    show ?thesis
    proof cases
      assume "n+1 \<ge> x\<^sub>2"
      hence "?D = i*(n+1-x\<^sub>2) - d*(x\<^sub>1-n)" using * by (simp)
      also have "\<dots> = i + i*(n-x\<^sub>2) + -(d*(x\<^sub>1-n))"
        by (simp add: algebra_simps)
      also have "i*(n-x\<^sub>2) \<le> 0" by (simp add: mult_le_0_iff)
      also have "-(d*(x\<^sub>1-n)) \<le> 0" using * by (simp)
      finally show ?thesis by simp
    next
      assume [arith]: "\<not> n+1 \<ge> x\<^sub>2"
      thus ?thesis
      proof cases
         assume "n+1 \<ge> x\<^sub>1"
         hence "?D = -(d*(x\<^sub>1-n))" using * by (simp)
         also have "-(d*(x\<^sub>1-n)) \<le> 0" using * by (simp)
         finally have "?D \<le> 0" by simp
         then show ?thesis by simp
      next
        assume "\<not> n+1 \<ge> x\<^sub>1"
        hence "?D = d*(x\<^sub>1-(n+1)) - d*(x\<^sub>1-n)" using * by (simp)
        also have "\<dots> = -d" by (simp add: algebra_simps)
        finally show ?thesis by (simp)
      qed
    qed
  next
    assume *: "\<not> (n \<le> x\<^sub>1 \<and> b)"
    show ?thesis
    proof cases
      assume "n+1 \<ge> x\<^sub>2"
      hence "?D = i*(n+1-x\<^sub>2)" using * by (auto)
      also have "\<dots> \<le> i" by(simp add: algebra_simps)
      finally show ?thesis by simp
    next
      assume "\<not> n+1 \<ge> x\<^sub>2"
      hence "?D = 0" using * by (auto)
      thus ?thesis by simp
    qed
  qed
qed

lemma Psi_diff_Del: assumes [arith]: "0 < i" "0 \<le> d" "n\<noteq>0" and "x\<^sub>1 \<le> x\<^sub>2"
shows "\<Psi> b i d x\<^sub>1 x\<^sub>2 (n-Suc 0) - \<Psi> b i d x\<^sub>1 x\<^sub>2 (n) \<le> d" (is "?D \<le> _")
proof cases
  assume "real n - 1 \<ge> x\<^sub>2"
  hence "?D = i*(n-1-x\<^sub>2) - i*(n-x\<^sub>2)" by(simp)
  also have "\<dots> = - i" by (simp add: algebra_simps)
  finally show ?thesis by simp
next
  assume [arith]: "\<not> real n - 1 \<ge> x\<^sub>2"
  show ?thesis
  proof cases
    assume *: "n-1 \<le> x\<^sub>1 \<and> b"
    show ?thesis
    proof cases
      assume [arith]: "n \<ge> x\<^sub>2"
      hence f1: "x\<^sub>1 \<le> n" using \<open>x\<^sub>1 \<le> x\<^sub>2\<close> by linarith
      have "?D = d*(x\<^sub>1-(n-1)) - i*(n-x\<^sub>2)" using * by (simp)
      also have "\<dots> = d + d*(x\<^sub>1-n) + -(i*(n-x\<^sub>2))"
        by (simp add: algebra_simps)
      also have "-(i*(n-x\<^sub>2)) \<le> 0" by (simp add: mult_le_0_iff)
      also have "d*(x\<^sub>1-n) \<le> 0" using f1 by (simp add: mult_le_0_iff)
      finally show ?thesis by simp
    next
      assume [arith]: "\<not> n \<ge> x\<^sub>2"
      thus ?thesis (* by (simp add: algebra_simps) *)
      proof cases
        assume [arith]: "n > x\<^sub>1"
        hence "?D = d*(x\<^sub>1-(n-1))" using * by (simp)
        also have "\<dots> = d + -(d*(n-x\<^sub>1))" by (simp add: algebra_simps)
        also have "-(d*(n-x\<^sub>1)) \<le> 0" by (simp add: mult_le_0_iff)
        finally show ?thesis by simp
      next
        assume "\<not> n > x\<^sub>1"
        hence "?D = d*(x\<^sub>1-(n-1)) - d*(x\<^sub>1-n)" using * by (simp)
        also have "\<dots> = d" by (simp add: algebra_simps)
        finally show ?thesis by (simp)
      qed
    qed
  next
    assume *: "\<not> (n-1 \<le> x\<^sub>1 \<and> b)"
    show ?thesis
    proof cases
      assume n: "n \<ge> x\<^sub>2"
      hence "?D = -(i*(n-x\<^sub>2))" using * by(auto)
      also have "-(i*(n-x\<^sub>2)) \<le> 0" using n by(simp)
      finally show ?thesis by simp
    next
      assume "\<not> n \<ge> x\<^sub>2"
      hence "?D = 0" using * by (auto)
      thus ?thesis by simp
    qed
  qed
qed

locale Table0 =
fixes f1 f2 f1' f2' e c :: real
assumes e1[arith]: "e > 1"
assumes c1[arith]: "c > 1"
assumes f1[arith]: "f1 > 0"
assumes f1cf2: "f1*c < f2"
assumes f1f2e: "f1 < f2/e"
assumes f1'_def: "f1' = min (f1*c) (f2/e)"
assumes f2'_def: "f2' = max (f1*c) (f2/e)"
begin

lemma f2[arith]: "0 < f2"
using f1f2e zero_less_divide_iff[of f2 e] by simp

lemma f2'[arith]: "0 < f2'"
by (simp add: f2'_def max_def)

lemma f2'_less_f2: "f2' < f2"
using f1cf2 by(auto simp add: f2'_def field_simps)

lemma f1_less_f1': "f1 < f1'"
using f1f2e by(auto simp add: f1'_def field_simps)

lemma f1'_gr0[arith]: "f1' > 0"
using f1_less_f1' by linarith

lemma f1'_le_f2': "f1' \<le> f2'"
by(auto simp add: f1'_def f2'_def algebra_simps)

lemma f1'c_le_f1: "f1'/c \<le> f1"
by(simp add: f1'_def min_def field_simps)

lemma f2_le_f2'e: "f2 \<le> f2'*e"
by(simp add: f2'_def max_def field_simps)

lemma f1f2'c: "f1 \<le> f2'/c"
using f1f2e by(auto simp add: f2'_def field_simps)

lemma f1'ef2: "f1' * e \<le> f2"
using f1cf2 by(auto simp add: f1'_def field_simps min_def)

end

locale Table = Table0 +
fixes l0 :: real
assumes l0f2e: "l0 \<ge> 1/(f2 * (e-1))"
assumes l0f1c: "l0 \<ge> 1/(f1 * (c-1))"
assumes f2f2': "l0 \<ge> 1/(f2 - f2')"
assumes f1'f1: "l0 \<ge> 1/((f1' - f1)*c)"
begin

definition "ai = f2/(f2-f2')"
definition "ad = f1/(f1'-f1)"

lemma aigr0[arith]: "ai > 1"
using f2'_less_f2 by(simp add: ai_def field_simps)

lemma adgr0[arith]: "ad > 0"
using f1_less_f1' by(simp add: ad_def field_simps)

lemma l0_gr0[arith]: "l0 > 0"
proof -
  have "0 < 1/(f2*(e-1))" by(simp)
  also note l0f2e
  finally show ?thesis .
qed

lemma f1_l0: assumes "l0 \<le> l/c" shows "f1*(l/c) \<le> f1*l - 1"
proof -
  have "1 = f1*((c-1)/c)*(c*(1/(f1*(c-1))))" by(simp add: field_simps)
  also note l0f1c
  also note assms(1)
  finally show ?thesis by(simp add: divide_le_cancel) (simp add: field_simps)
qed

fun nxt :: "op\<^sub>t\<^sub>b \<Rightarrow> nat*real \<Rightarrow> nat*real" where
"nxt Ins (n,l) =
 (n+1, if n+1 \<le> f2*l then l else e*l)" |
"nxt Del (n,l) =
 (n-1, if f1*l \<le> real(n-1) then l else if l0 \<le> l/c then l/c else l)"

fun t :: "op\<^sub>t\<^sub>b \<Rightarrow> nat*real \<Rightarrow> real" where
"t Ins (n,l) = (if n+1 \<le> f2*l then 1 else n+1)" |
"t Del (n,l) = (if f1*l \<le> real(n-1) then 1 else if l0 \<le> l/c then n else 1)"

fun \<Phi> :: "nat * real \<Rightarrow> real" where
"\<Phi> (n,l) = (if n \<ge> f2'*l then ai*(n - f2'*l) else
  if n \<le> f1'*l \<and> l0 \<le> l/c then ad*(f1'*l - n) else 0)"

lemma Phi_Psi: "\<Phi> (n,l) = \<Psi> (l0 \<le> l/c) ai ad (f1'*l) (f2'*l) n"
by(simp)

fun invar where
"invar(n,l) = (l \<ge> l0 \<and> (l/c \<ge> l0 \<longrightarrow> f1*l \<le> n) \<and> n \<le> f2*l)"

abbreviation "U \<equiv> \<lambda>f _. case f of Ins \<Rightarrow> ai+1 | Del \<Rightarrow> ad+1"

interpretation tb: Amortized
  where init = "(0,l0)" and nxt = nxt
  and inv = invar
  and t = t and \<Phi> = \<Phi>
  and U = U
proof (standard, goal_cases)
  case 1 show ?case by (auto simp: field_simps)
next
  case (2 s f)
  obtain n l where [simp]: "s = (n,l)" by fastforce
  from 2 have "l0 \<le> l" and "n \<le> f2*l" by auto
  hence [arith]: "l > 0" by arith
  show ?case
  proof (cases f)
    case [simp]: Ins
    show ?thesis
    proof cases
      assume "n+1 \<le> f2*l" thus ?thesis using 2 by (auto)
    next
      assume 0: "\<not> n+1 \<le> f2*l"
      have f1: "f1 * (e*l) \<le> n+1"
      proof -
        have "f1*e < f2" using f1f2e by(simp add: field_simps)
        hence "f1 * (e*l) \<le> f2*l" by simp
        with 0 show ?thesis by linarith
      qed
      have f2: "n+1 \<le> f2*e*l"
      proof -
        have "n+1 \<le> f2*l+1" using \<open>n \<le> f2*l\<close> by linarith
        also have "1 = f2*(e-1)*(1/(f2*(e-1)))" by(simp)
        also note l0f2e
        also note \<open>l0 \<le> l\<close>
        finally show ?thesis by simp (simp add: algebra_simps)
      qed
      have "l \<le> l*e" by simp
      hence "l0 \<le> l * e" using \<open>l0\<le>l\<close> by linarith
      with 0 f1 f2 show ?thesis by(simp add: field_simps)
    qed
  next
    case [simp]: Del
    show ?thesis
    proof cases
      assume "f1*l \<le> real (n - 1)"
      thus ?thesis using 2 by(auto)
    next
      assume 0: "\<not> f1*l \<le> real (n - 1)"
      show ?thesis
      proof cases
        assume l: "l0 \<le> l/c"
        hence f1: "f1*(l/c) \<le> n-1" using f1_l0[OF l] 2 by simp linarith
        have "n - 1 \<le> f2 * (l/c)"
        proof -
          have "f1*l \<le> f2*(l/c)" using f1cf2 by (simp add: field_simps)
          thus ?thesis using 0 by linarith
        qed
        with l 0 f1 show ?thesis by (auto)
      next
        assume "\<not> l0 \<le> l/c"
        with 2 show ?thesis by (auto simp add: field_simps)
      qed
    qed
  qed
next
  case (3 s) thus ?case by(cases s)(simp split: if_splits)
next
  case 4 show ?case by(simp add: field_simps not_le)
next
  case (5 s f)
  obtain n l where [simp]: "s = (n,l)" by fastforce
  have [arith]: "l \<ge> l0"  "n \<le> f2*l" using 5 by auto
  show ?case
  proof (cases f)
    case [simp]: Ins
    show ?thesis (is "?A \<le> _")
    proof cases
      assume "n+1 \<le> f2*l"
      thus ?thesis by(simp del: \<Phi>.simps \<Psi>.simps add: Phi_Psi Psi_diff_Ins)
    next
      assume [arith]: "\<not> n+1 \<le> f2*l"
      have "(f2 - f2')*l \<ge> 1"
        using mult_mono[OF order_refl \<open>l\<ge>l0\<close>, of "f2-f2'"] f2'_less_f2 f2f2'
        by (simp add: field_simps)
      hence "n \<ge> f2'*l" by(simp add: algebra_simps)
      hence Phi: "\<Phi> s = ai * (n - f2'*l)" by simp
      have "f1'*e*l \<le> f2*l" using f1'ef2 by(simp)
      hence "f1'*e*l < n+1" by linarith
      have "?A \<le> n - ai*(f2 - f2')*l + ai + 1"
      proof cases
        assume "n+1 < f2'*(e*l)"
        hence "?A = n+1 - ai*(n - f2'*l)" using Phi \<open>f1'*e*l < n+1\<close> by simp
        also have "\<dots> = n + ai*(-(n+1) + f2'*l) + ai+1"
          by(simp add: algebra_simps)
        also have "-(n+1) \<le> -f2*l" by linarith
        finally show ?thesis by(simp add: algebra_simps)
      next
        assume "\<not> n+1 < f2'*(e*l)"
        hence "?A = n + ai*(-f2'*e + f2')*l + ai+1" using Phi
          by(simp add: algebra_simps)
        also have "-f2'*e \<le> -f2" using f2_le_f2'e by linarith
        finally show ?thesis by(simp add: algebra_simps)
      qed
      also have "\<dots> = n - f2*l + ai+1" using f2'_less_f2 by(simp add: ai_def)
      finally show ?thesis by simp
    qed
  next
    case [simp]: Del
    show ?thesis (is "?A \<le> _")
    proof cases
      assume "n=0" with 5 show ?thesis
        by(simp add: mult_le_0_iff field_simps)
    next
      assume [arith]: "n\<noteq>0"
      show ?thesis
      proof cases
        assume "real n - 1 \<ge> f1*l \<or> l/c < l0"
        thus ?thesis using f1'_le_f2'
          by(auto simp del: \<Phi>.simps \<Psi>.simps simp add: Phi_Psi Psi_diff_Del)
      next
        assume "\<not> (real n - 1 \<ge> f1*l \<or> l/c < l0)"
        hence [arith]: "real n - 1 < f1*l" "l/c \<ge> l0" by linarith+
        hence "l \<ge> l0*c" and "l/c \<ge> l0" and "f1*l \<le> n" using 5
          by (auto simp: field_simps)
        have "f1*l \<le> f2'*l/c" using f1f2'c by(simp add: field_simps)
        hence f2: "n-1 < f2'*l/c" by linarith
        have "f1'*l \<le> f2'*l" using f1'_le_f2' by simp
        have "(f1' - f1)*l \<ge> 1"
          using mult_mono[OF order_refl \<open>l\<ge>l0*c\<close>, of "f1'-f1"] f1_less_f1' f1'f1
          by (simp add: field_simps)
        hence "n < f1'*l" by(simp add: algebra_simps)
        hence Phi: "\<Phi> s = ad*(f1'*l - n)"
          apply(simp) using \<open>f1'*l \<le> f2'*l\<close> by linarith
        have "?A \<le> n - ad*(f1' - f1)*l + ad"
        proof cases
          assume "n-1 < f1'*l/c \<and> l/(c*c) \<ge> l0"
          hence "\<Phi> (nxt f s) = ad*(f1'*l/c - (n-1))" using f2 by(auto)
          hence "?A = n + ad*(f1'*l/c - (n-1)) - (ad*(f1'*l - n))"
            using Phi by (simp add: algebra_simps)
          also have "\<dots> = n + ad*(f1'/c - f1')*l + ad"
            by(simp add: algebra_simps)
          also note f1'c_le_f1
          finally show ?thesis by(simp add: algebra_simps)
        next
          assume "\<not>(n-1 < f1'*l/c \<and> l/(c*c) \<ge> l0)"
          hence "\<Phi> (nxt f s) = 0" using f2 by(auto)
          hence "?A = n + ad*(n - f1'*l)" using Phi
            by (simp add: algebra_simps)
          also have "\<dots> = n + ad*(n-1 - f1'*l) + ad" by(simp add: algebra_simps)
          also have "n-1 \<le> f1*l" by linarith
          finally show ?thesis by (simp add: algebra_simps)
        qed
        also have "\<dots> = n - f1*l + ad" using f1_less_f1' by(simp add: ad_def)
        finally show ?thesis by simp
      qed
    qed
  qed
qed

end

locale Optimal =
fixes f2 c e :: real and l0 :: nat
assumes e1[arith]: "e > 1"
assumes c1[arith]: "c > 1"
assumes [arith]: "f2 > 0"
assumes l0: "(e*c)/(f2*(min e c - 1)) \<le> l0"
begin

lemma l0e: "(e*c)/(f2*(e-1)) \<le> l0"
proof-
  have 0: "f2 * (l0 * min e c) \<le> e * (f2 * l0)"
    by (simp add: min_def ac_simps mult_right_mono)
  from l0 show ?thesis apply(simp add: field_simps) using 0 by linarith
qed

lemma l0c: "(e*c)/(f2*(c-1)) \<le> l0"
proof-
  have 0: "f2 * (l0 * min e c) \<le> c * (f2 * l0)"
    by (simp add: min_def ac_simps mult_right_mono)
  from l0 show ?thesis apply(simp add: field_simps) using 0 by linarith
qed

interpretation Table
where f1="f2/(e*c)" and f2=f2 and e=e and c=c and f1'="f2/e" and f2'="f2/e" and l0=l0
proof (standard, goal_cases)
  case 1 show ?case by(rule e1)
next
  case 2 show ?case by(rule c1)
next
  case 3 show ?case by(simp)
next
  case 4 show ?case by(simp add: field_simps)
next
  case 5 show ?case by(simp add: field_simps)
next
  case 6 show ?case by(simp)
next
  case 7 show ?case by(simp)
next
  case 8 show ?case using l0e less_1_mult[OF c1 e1] by(simp add: field_simps)
next
  case 9 show ?case using l0c by(simp)
next
  case 10 show ?case
  proof-
    have 1: "c*e>e" by (simp)
    show ?thesis using l0e apply(simp add: field_simps) using 1 by linarith
  qed
next
  case 11 show ?case
  proof-
    have 1: "c*e>e" by (simp)
    show ?thesis using l0c
      apply(simp add: algebra_simps pos_le_divide_eq)
      apply(simp add: field_simps)
      using 1 by linarith
  qed
qed

lemma "ai = e/(e-1)"
unfolding ai_def by(simp add: field_simps)

lemma "ad = 1/(c-1)"
unfolding ad_def by(simp add: field_simps)

end

interpretation I1: Optimal where e=2 and c=2 and f2=1 and l0=4 (* f1=1/4 *)
proof qed simp_all

interpretation I2: Optimal where e=2 and c=2 and f2="3/4" and l0=6 (* f1=3/16 *)
proof qed simp_all

interpretation I3: Optimal where e=2 and c=2 and f2="0.8" and l0=5 (* f1=1/5 *)
proof qed simp_all

interpretation I4: Optimal where e=3 and c=3 and f2="0.9" and l0=5 (* f1=1/10 *)
proof qed simp_all

interpretation I5: Optimal where e=4 and c=4 and f2=1 and l0=6 (* f1=1/16 *)
proof qed simp_all

interpretation I6: Optimal where e="2.5" and c="2.5" and f2=1 and l0=5 (* f1=4/25 *)
proof qed simp_all

interpretation I7: Optimal where f2=1 and c="3/2" and e=2 and l0=6 (* f1=1/3 *)
proof qed (simp_all add: min_def)

interpretation I8: Optimal where f2=1 and e="3/2" and c=2 and l0=6 (* f1=1/3 *)
proof qed (simp_all add: min_def)

end

repo: PSL


text:
(*  Title:       Preliminaries for hybrid systems verification
    Author:      Jonathan Julián Huerta y Munive, 2021
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

section \<open> Hybrid Systems Preliminaries \<close>

text \<open>Hybrid systems combine continuous dynamics with discrete control. This section contains
auxiliary lemmas for verification of hybrid systems.\<close>

theory HS_Preliminaries
  imports "Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative"
begin

\<comment> \<open> Notation \<close>

bundle derivative_notation
begin

no_notation has_vderiv_on (infix "(has'_vderiv'_on)" 50)

notation has_derivative ("(1(D _ \<mapsto> (_))/ _)" [65,65] 61)
     and has_vderiv_on ("(1 D _ = (_)/ on _)" [65,65] 61)

end

bundle derivative_no_notation
begin

notation has_vderiv_on (infix "(has'_vderiv'_on)" 50)

no_notation has_derivative ("(1(D _ \<mapsto> (_))/ _)" [65,65] 61)
     and has_vderiv_on ("(1 D _ = (_)/ on _)" [65,65] 61)

end

unbundle derivative_notation

notation norm ("\<parallel>_\<parallel>")

subsection \<open> Real numbers \<close>

lemma abs_le_eq:
  shows "(r::real) > 0 \<Longrightarrow> (\<bar>x\<bar> < r) = (-r < x \<and> x < r)"
    and "(r::real) > 0 \<Longrightarrow> (\<bar>x\<bar> \<le> r) = (-r \<le> x \<and> x \<le> r)"
  by linarith+

lemma real_ivl_eqs:
  assumes "0 < r"
  shows "ball x r = {x-r<--< x+r}"         and "{x-r<--< x+r} = {x-r<..< x+r}"
    and "ball (r / 2) (r / 2) = {0<--<r}"  and "{0<--<r} = {0<..<r}"
    and "ball 0 r = {-r<--<r}"             and "{-r<--<r} = {-r<..<r}"
    and "cball x r = {x-r--x+r}"           and "{x-r--x+r} = {x-r..x+r}"
    and "cball (r / 2) (r / 2) = {0--r}"   and "{0--r} = {0..r}"
    and "cball 0 r = {-r--r}"              and "{-r--r} = {-r..r}"
  unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl
  using assms by (auto simp: cball_def ball_def dist_norm field_simps)

lemma is_interval_real_nonneg[simp]: "is_interval (Collect ((\<le>) (0::real)))"
  by (auto simp: is_interval_def)

lemma norm_rotate_eq[simp]:
  fixes x :: "'a:: {banach,real_normed_field}"
  shows "(x * cos t - y * sin t)\<^sup>2 + (x * sin t + y * cos t)\<^sup>2 = x\<^sup>2 + y\<^sup>2"
    and "(x * cos t + y * sin t)\<^sup>2 + (y * cos t - x * sin t)\<^sup>2 = x\<^sup>2 + y\<^sup>2"
proof-
  have "(x * cos t - y * sin t)\<^sup>2 = x\<^sup>2 * (cos t)\<^sup>2 + y\<^sup>2 * (sin t)\<^sup>2 - 2 * (x * cos t) * (y * sin t)"
    by(simp add: power2_diff power_mult_distrib)
  also have "(x * sin t + y * cos t)\<^sup>2 = y\<^sup>2 * (cos t)\<^sup>2 + x\<^sup>2 * (sin t)\<^sup>2 + 2 * (x * cos t) * (y * sin t)"
    by(simp add: power2_sum power_mult_distrib)
  ultimately show "(x * cos t - y * sin t)\<^sup>2 + (x * sin t + y * cos t)\<^sup>2 = x\<^sup>2 + y\<^sup>2"
    by (simp add: Groups.mult_ac(2) Groups.mult_ac(3) right_diff_distrib sin_squared_eq)
  thus "(x * cos t + y * sin t)\<^sup>2 + (y * cos t - x * sin t)\<^sup>2 = x\<^sup>2 + y\<^sup>2"
    by (simp add: add.commute add.left_commute power2_diff power2_sum)
qed

lemma sum_eq_Sum:
  assumes "inj_on f A"
  shows "(\<Sum>x\<in>A. f x) = (\<Sum> {f x |x. x \<in> A})"
proof-
  have "(\<Sum> {f x |x. x \<in> A}) = (\<Sum> (f ` A))"
    apply(auto simp: image_def)
    by (rule_tac f=Sum in arg_cong, auto)
  also have "... = (\<Sum>x\<in>A. f x)"
    by (subst sum.image_eq[OF assms], simp)
  finally show "(\<Sum>x\<in>A. f x) = (\<Sum> {f x |x. x \<in> A})"
    by simp
qed

lemma triangle_norm_vec_le_sum: "\<parallel>x\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>x $ i\<parallel>)"
  by (simp add: L2_set_le_sum norm_vec_def)

subsection \<open> Single variable derivatives \<close>

named_theorems poly_derivatives "compilation of optimised miscellaneous derivative rules."

declare has_vderiv_on_const [poly_derivatives]
    and has_vderiv_on_id [poly_derivatives]
    and has_vderiv_on_add[THEN has_vderiv_on_eq_rhs, poly_derivatives]
    and has_vderiv_on_diff[THEN has_vderiv_on_eq_rhs, poly_derivatives]
    and has_vderiv_on_mult[THEN has_vderiv_on_eq_rhs, poly_derivatives]
    and has_vderiv_on_ln[poly_derivatives]

lemma vderiv_on_composeI:
  assumes "D f = f' on g ` T"
    and " D g = g' on T"
    and "h = (\<lambda>t. g' t *\<^sub>R f' (g t))"
  shows "D (\<lambda>t. f (g t)) = h on T"
  apply(subst ssubst[of h], simp)
  using assms has_vderiv_on_compose by auto

lemma vderiv_uminusI[poly_derivatives]:
  "D f = f' on T \<Longrightarrow> g = (\<lambda>t. - f' t) \<Longrightarrow> D (\<lambda>t. - f t) = g on T"
  using has_vderiv_on_uminus by auto

lemma vderiv_npowI[poly_derivatives]:
  fixes f::"real \<Rightarrow> real"
  assumes "n \<ge> 1" and "D f = f' on T" and "g = (\<lambda>t. n * (f' t) * (f t)^(n-1))"
  shows "D (\<lambda>t. (f t)^n) = g on T"
  using assms unfolding has_vderiv_on_def has_vector_derivative_def
  by (auto intro: derivative_eq_intros simp: field_simps)

lemma vderiv_divI[poly_derivatives]:
  assumes "\<forall>t\<in>T. g t \<noteq> (0::real)" and "D f = f' on T"and "D g = g' on T"
    and "h = (\<lambda>t. (f' t * g t - f t * (g' t)) / (g t)^2)"
  shows "D (\<lambda>t. (f t)/(g t)) = h on T"
  apply(subgoal_tac "(\<lambda>t. (f t)/(g t)) = (\<lambda>t. (f t) * (1/(g t)))")
   apply(erule ssubst, rule poly_derivatives(5)[OF assms(2)])
  apply(rule vderiv_on_composeI[where g=g and f="\<lambda>t. 1/t" and f'="\<lambda>t. - 1/t^2", OF _ assms(3)])
  apply(subst has_vderiv_on_def, subst has_vector_derivative_def, clarsimp)
   using assms(1) apply(force intro!: derivative_eq_intros simp: fun_eq_iff power2_eq_square)
   using assms by (auto simp: field_simps power2_eq_square)

lemma vderiv_cosI[poly_derivatives]:
  assumes "D (f::real \<Rightarrow> real) = f' on T" and "g = (\<lambda>t. - (f' t) * sin (f t))"
  shows "D (\<lambda>t. cos (f t)) = g on T"
  apply(rule vderiv_on_composeI[OF _ assms(1), of "\<lambda>t. cos t"])
  unfolding has_vderiv_on_def has_vector_derivative_def
  by (auto intro!: derivative_eq_intros simp: assms)

lemma vderiv_sinI[poly_derivatives]:
  assumes "D (f::real \<Rightarrow> real) = f' on T" and "g = (\<lambda>t. (f' t) * cos (f t))"
  shows "D (\<lambda>t. sin (f t)) = g on T"
  apply(rule vderiv_on_composeI[OF _ assms(1), of "\<lambda>t. sin t"])
  unfolding has_vderiv_on_def has_vector_derivative_def
  by (auto intro!: derivative_eq_intros simp: assms)

lemma vderiv_expI[poly_derivatives]:
  assumes "D (f::real \<Rightarrow> real) = f' on T" and "g = (\<lambda>t. (f' t) * exp (f t))"
  shows "D (\<lambda>t. exp (f t)) = g on T"
  apply(rule vderiv_on_composeI[OF _ assms(1), of "\<lambda>t. exp t"])
  unfolding has_vderiv_on_def has_vector_derivative_def
  by (auto intro!: derivative_eq_intros simp: assms)

\<comment> \<open>Examples for checking derivatives\<close>

lemma "D (*) a = (\<lambda>t. a) on T"
  by (auto intro!: poly_derivatives)

lemma "a \<noteq> 0 \<Longrightarrow> D (\<lambda>t. t/a) = (\<lambda>t. 1/a) on T"
  by (auto intro!: poly_derivatives simp: power2_eq_square)

lemma "(a::real) \<noteq> 0 \<Longrightarrow> D f = f' on T \<Longrightarrow> g = (\<lambda>t. (f' t)/a) \<Longrightarrow> D (\<lambda>t. (f t)/a) = g on T"
  by (auto intro!: poly_derivatives simp: power2_eq_square)

lemma "\<forall>t\<in>T. f t \<noteq> (0::real) \<Longrightarrow> D f = f' on T \<Longrightarrow> g = (\<lambda>t. - a * f' t / (f t)^2) \<Longrightarrow>
  D (\<lambda>t. a/(f t)) = g on T"
  by (auto intro!: poly_derivatives simp: power2_eq_square)

lemma "D (\<lambda>t. a * t\<^sup>2 / 2 + v * t + x) = (\<lambda>t. a * t + v) on T"
  by(auto intro!: poly_derivatives)

lemma "D (\<lambda>t. v * t - a * t\<^sup>2 / 2 + x) = (\<lambda>x. v - a * x) on T"
  by(auto intro!: poly_derivatives)

lemma "D x = x' on (\<lambda>\<tau>. \<tau> + t) ` T \<Longrightarrow> D (\<lambda>\<tau>. x (\<tau> + t)) = (\<lambda>\<tau>. x' (\<tau> + t)) on T"
  by (rule vderiv_on_composeI, auto intro: poly_derivatives)

lemma "a \<noteq> 0 \<Longrightarrow> D (\<lambda>t. t/a) = (\<lambda>t. 1/a) on T"
  by (auto intro!: poly_derivatives simp: power2_eq_square)

lemma "c \<noteq> 0 \<Longrightarrow> D (\<lambda>t. a5 * t^5 + a3 * (t^3 / c) - a2 * exp (t^2) + a1 * cos t + a0) =
  (\<lambda>t. 5 * a5 * t^4 + 3 * a3 * (t^2 / c) - 2 * a2 * t * exp (t^2) - a1 * sin t) on T"
  by(auto intro!: poly_derivatives simp: power2_eq_square)

lemma "c \<noteq> 0 \<Longrightarrow> D (\<lambda>t. - a3 * exp (t^3 / c) + a1 * sin t + a2 * t^2) =
  (\<lambda>t. a1 * cos t + 2 * a2 * t - 3 * a3 * t^2 / c * exp (t^3 / c)) on T"
  by(auto intro!: poly_derivatives simp: power2_eq_square)

lemma "c \<noteq> 0 \<Longrightarrow> D (\<lambda>t. exp (a * sin (cos (t^4) / c))) =
  (\<lambda>t. - 4 * a * t^3 * sin (t^4) / c * cos (cos (t^4) / c) * exp (a * sin (cos (t^4) / c))) on T"
  by (intro poly_derivatives) (auto intro!: poly_derivatives simp: power2_eq_square)

subsection \<open> Intermediate Value Theorem \<close>

lemma IVT_two_functions:
  fixes f :: "('a::{linear_continuum_topology, real_vector}) \<Rightarrow>
  ('b::{linorder_topology,real_normed_vector,ordered_ab_group_add})"
  assumes conts: "continuous_on {a..b} f" "continuous_on {a..b} g"
      and ahyp: "f a < g a" and bhyp: "g b < f b " and "a \<le> b"
    shows "\<exists>x\<in>{a..b}. f x = g x"
proof-
  let "?h x" = "f x - g x"
  have "?h a \<le> 0" and "?h b \<ge> 0"
    using ahyp bhyp by simp_all
  also have "continuous_on {a..b} ?h"
    using conts continuous_on_diff by blast
  ultimately obtain x where "a \<le> x" "x \<le> b" and "?h x = 0"
    using IVT'[of "?h"] \<open>a \<le> b\<close> by blast
  thus ?thesis
    using \<open>a \<le> b\<close> by auto
qed

lemma IVT_two_functions_real_ivl:
  fixes f :: "real \<Rightarrow> real"
  assumes conts: "continuous_on {a--b} f" "continuous_on {a--b} g"
      and ahyp: "f a < g a" and bhyp: "g b < f b "
    shows "\<exists>x\<in>{a--b}. f x = g x"
proof(cases "a \<le> b")
  case True
  then show ?thesis
    using IVT_two_functions assms
    unfolding closed_segment_eq_real_ivl by auto
next
  case False
  hence "a \<ge> b"
    by auto
  hence "continuous_on {b..a} f" "continuous_on {b..a} g"
    using conts False unfolding closed_segment_eq_real_ivl by auto
  hence "\<exists>x\<in>{b..a}. g x = f x"
    using IVT_two_functions[of b a g f] assms(3,4) False by auto
  then show ?thesis
    using \<open>a \<ge> b\<close> unfolding closed_segment_eq_real_ivl by auto force
qed

subsection \<open> Filters \<close>

lemma eventually_at_within_mono:
  assumes "t \<in> interior T" and "T \<subseteq> S"
    and "eventually P (at t within T)"
  shows "eventually P (at t within S)"
  by (meson assms eventually_within_interior interior_mono subsetD)

lemma netlimit_at_within_mono:
  fixes t::"'a::{perfect_space,t2_space}"
  assumes "t \<in> interior T" and "T \<subseteq> S"
  shows "netlimit (at t within S) = t"
  using assms(1) interior_mono[OF \<open>T \<subseteq> S\<close>] netlimit_within_interior by auto

lemma has_derivative_at_within_mono:
  assumes "(t::real) \<in> interior T" and "T \<subseteq> S"
    and "D f \<mapsto> f' at t within T"
  shows "D f \<mapsto> f' at t within S"
  using assms(3) apply(unfold has_derivative_def tendsto_iff, safe)
  unfolding netlimit_at_within_mono[OF assms(1,2)] netlimit_within_interior[OF assms(1)]
  by (rule eventually_at_within_mono[OF assms(1,2)]) simp

lemma eventually_all_finite2:
  fixes P :: "('a::finite) \<Rightarrow> 'b \<Rightarrow> bool"
  assumes h:"\<forall>i. eventually (P i) F"
  shows "eventually (\<lambda>x. \<forall>i. P i x) F"
proof(unfold eventually_def)
  let ?F = "Rep_filter F"
  have obs: "\<forall>i. ?F (P i)"
    using h by auto
  have "?F (\<lambda>x. \<forall>i \<in> UNIV. P i x)"
    apply(rule finite_induct)
    by(auto intro: eventually_conj simp: obs h)
  thus "?F (\<lambda>x. \<forall>i. P i x)"
    by simp
qed

lemma eventually_all_finite_mono:
  fixes P :: "('a::finite) \<Rightarrow> 'b \<Rightarrow> bool"
  assumes h1: "\<forall>i. eventually (P i) F"
      and h2: "\<forall>x. (\<forall>i. (P i x)) \<longrightarrow> Q x"
  shows "eventually Q F"
proof-
  have "eventually (\<lambda>x. \<forall>i. P i x) F"
    using h1 eventually_all_finite2 by blast
  thus "eventually Q F"
    unfolding eventually_def
    using h2 eventually_mono by auto
qed

subsection \<open> Multivariable derivatives \<close>

definition vec_upd :: "('a^'b) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'a^'b"
  where "vec_upd s i a = (\<chi> j. ((($) s)(i := a)) j)"

lemma vec_upd_eq: "vec_upd s i a = (\<chi> j. if j = i then a else s$j)"
  by (simp add: vec_upd_def)

lemma has_derivative_vec_nth[derivative_intros]:
  "D (\<lambda>s. s $ i) \<mapsto> (\<lambda>s. s $ i) (at x within S)"
  by (clarsimp simp: has_derivative_within) standard

lemma bounded_linear_component:
  "(bounded_linear f) \<longleftrightarrow> (\<forall>i. bounded_linear (\<lambda>x. (f x) $ i))" (is "?lhs = ?rhs")
proof
  assume ?lhs
  thus ?rhs
    apply(clarsimp, rule_tac f="(\<lambda>x. x $ i)" in bounded_linear_compose)
     apply(simp_all add: bounded_linear_def bounded_linear_axioms_def linear_iff)
    by (rule_tac x=1 in exI, clarsimp) (meson Finite_Cartesian_Product.norm_nth_le)
next
  assume ?rhs
  hence "(\<forall>i. \<exists>K. \<forall>x. \<parallel>f x $ i\<parallel> \<le> \<parallel>x\<parallel> * K)" "linear f"
    by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_iff vec_eq_iff)
  then obtain F where F: "\<And>i x. \<parallel>f x $ i\<parallel> \<le> \<parallel>x\<parallel> * F i"
    by metis
  have "\<parallel>f x\<parallel> \<le> \<parallel>x\<parallel> * sum F UNIV" for x
  proof -
    have "norm (f x) \<le> (\<Sum>i\<in>UNIV. \<parallel>f x $ i\<parallel>)"
      by (simp add: L2_set_le_sum norm_vec_def)
    also have "... \<le> (\<Sum>i\<in>UNIV. norm x * F i)"
      by (metis F sum_mono)
    also have "... = norm x * sum F UNIV"
      by (simp add: sum_distrib_left)
    finally show ?thesis .
  qed
  then show ?lhs
    by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f\<close>)
qed

lemma open_preimage_nth:
  "open S \<Longrightarrow> open {s::('a::real_normed_vector^'n::finite). s $ i \<in> S}"
  unfolding open_contains_ball apply clarsimp
  apply(erule_tac x="x$i" in ballE; clarsimp)
  apply(rule_tac x=e in exI; clarsimp simp: dist_norm subset_eq ball_def)
  apply(rename_tac x e y, erule_tac x="y$i" in allE)
  using Finite_Cartesian_Product.norm_nth_le
  by (metis le_less_trans vector_minus_component)

lemma tendsto_nth_iff: \<comment> \<open> following @{thm tendsto_componentwise_iff} \<close>
  fixes l::"'a::real_normed_vector^'n::finite"
  defines "m \<equiv> real CARD('n)"
  shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> l $ i) F)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  thus ?rhs
    unfolding tendsto_def
    by (clarify, drule_tac x="{s. s $ i \<in> S}" in spec) (auto simp: open_preimage_nth)
next
  assume ?rhs
  thus ?lhs
  proof(unfold tendsto_iff dist_norm, clarify)
    fix \<epsilon>::real assume "0 < \<epsilon>"
    assume evnt_h: "\<forall>i \<epsilon>. 0 < \<epsilon> \<longrightarrow> (\<forall>\<^sub>F x in F. \<parallel>f x $ i - l $ i\<parallel> < \<epsilon>)"
    {fix x assume hyp: "\<forall>i. \<parallel>f x $ i - l $ i\<parallel> < (\<epsilon>/m)"
      have "\<parallel>f x - l\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>f x $ i - l $ i\<parallel>)"
        using triangle_norm_vec_le_sum[of "f x - l"] by auto
      also have "... < (\<Sum>(i::'n)\<in>UNIV. (\<epsilon>/m))"
        apply(rule sum_strict_mono[of UNIV "\<lambda>i. \<parallel>f x $ i - l $ i\<parallel>" "\<lambda>i. \<epsilon>/m"])
        using hyp by auto
      also have "... = m * (\<epsilon>/m)"
        unfolding assms by simp
      finally have "\<parallel>f x - l\<parallel> < \<epsilon>"
        unfolding assms by simp}
    hence key: "\<And>x. \<forall>i. \<parallel>f x $ i - l $ i\<parallel> < (\<epsilon>/m) \<Longrightarrow> \<parallel>f x - l\<parallel> < \<epsilon>"
      by blast
    have obs: "\<forall>\<^sub>F x in F. \<forall>i. \<parallel>f x $ i - l $ i\<parallel> < (\<epsilon>/m)"
      apply(rule eventually_all_finite)
      using \<open>0 < \<epsilon>\<close> evnt_h unfolding assms by auto
    thus "\<forall>\<^sub>F x in F. \<parallel>f x - l\<parallel> < \<epsilon>"
      by (rule eventually_mono[OF _ key], simp)
  qed
qed

lemma has_derivative_component[simp]: \<comment> \<open> following @{thm has_derivative_componentwise_within} \<close>
  "(D f \<mapsto> f' at x within S) \<longleftrightarrow> (\<forall>i. D (\<lambda>s. f s $ i) \<mapsto> (\<lambda>s. f' s $ i) at x within S)"
  by (simp add: has_derivative_within tendsto_nth_iff
      bounded_linear_component all_conj_distrib)

lemma has_vderiv_on_component[simp]:
  fixes x::"real \<Rightarrow> ('a::banach)^('n::finite)"
  shows "(D x = x' on T) = (\<forall>i. D (\<lambda>t. x t $ i) = (\<lambda>t. x' t $ i) on T)"
  unfolding has_vderiv_on_def has_vector_derivative_def by auto

lemma frechet_tendsto_vec_lambda:
  fixes f::"real \<Rightarrow> ('a::banach)^('m::finite)" and x::real and T::"real set"
  defines "x\<^sub>0 \<equiv> netlimit (at x within T)" and "m \<equiv> real CARD('m)"
  assumes "\<forall>i. ((\<lambda>y. (f y $ i - f x\<^sub>0 $ i - (y - x\<^sub>0) *\<^sub>R f' x $ i) /\<^sub>R (\<parallel>y - x\<^sub>0\<parallel>)) \<longlongrightarrow> 0) (at x within T)"
  shows "((\<lambda>y. (f y - f x\<^sub>0 - (y - x\<^sub>0) *\<^sub>R f' x) /\<^sub>R (\<parallel>y - x\<^sub>0\<parallel>)) \<longlongrightarrow> 0) (at x within T)"
  using assms by (simp add: tendsto_nth_iff)

lemma tendsto_norm_bound:
  "\<forall>x. \<parallel>G x - L\<parallel> \<le> \<parallel>F x - L\<parallel> \<Longrightarrow> (F \<longlongrightarrow> L) net \<Longrightarrow> (G \<longlongrightarrow> L) net"
  apply(unfold tendsto_iff dist_norm, clarsimp)
  apply(rule_tac P="\<lambda>x. \<parallel>F x - L\<parallel> < e" in eventually_mono, simp)
  by (rename_tac e z) (erule_tac x=z in allE, simp)

lemma tendsto_zero_norm_bound:
  "\<forall>x. \<parallel>G x\<parallel> \<le> \<parallel>F x\<parallel> \<Longrightarrow> (F \<longlongrightarrow> 0) net \<Longrightarrow> (G \<longlongrightarrow> 0) net"
  apply(unfold tendsto_iff dist_norm, clarsimp)
  apply(rule_tac P="\<lambda>x. \<parallel>F x\<parallel> < e" in eventually_mono, simp)
  by (rename_tac e z) (erule_tac x=z in allE, simp)

lemma frechet_tendsto_vec_nth:
  fixes f::"real \<Rightarrow> ('a::real_normed_vector)^'m"
  assumes "((\<lambda>x. (f x - f x\<^sub>0 - (x - x\<^sub>0) *\<^sub>R f' t) /\<^sub>R (\<parallel>x - x\<^sub>0\<parallel>)) \<longlongrightarrow> 0) (at t within T)"
  shows "((\<lambda>x. (f x $ i - f x\<^sub>0 $ i - (x - x\<^sub>0) *\<^sub>R f' t $ i) /\<^sub>R (\<parallel>x - x\<^sub>0\<parallel>)) \<longlongrightarrow> 0) (at t within T)"
  apply(rule_tac F="(\<lambda>x. (f x - f x\<^sub>0 - (x - x\<^sub>0) *\<^sub>R f' t) /\<^sub>R (\<parallel>x - x\<^sub>0\<parallel>))" in tendsto_zero_norm_bound)
   apply(clarsimp, rule mult_left_mono)
    apply (metis Finite_Cartesian_Product.norm_nth_le vector_minus_component vector_scaleR_component)
  using assms by simp_all

end

author: isabelle-prover

repo: mirror-afp-devel