Theory Path_Automation

(*
  File: Path_Automation.thy
  Author: Manuel Eberl, University of Innsbruck

  Notions of equivalence of paths and loops and the subpath relation.
*)
section ‹Automation for paths›
theory Path_Automation
  imports "HOL-Library.Sublist" Path_Equivalence
begin

text ‹
  In this section, we provide some machinery to make certain common arguments about paths easier.
  In particular:

    ▪ Proving the equivalence of some combination of lines and circular arcs modulo
      associativity

    ▪ Proving the equivalence of loops modulo associativity and ``rotation''

    ▪ Proving subpath relationships

    ▪ Decomposing a contour integral over a composite path into the contour integrals of its
      constituent paths

  Equivalence arguments that involve splitting, e.g.\ 
  \<^prop>‹linepath 0 1 +++ linepath 1 2 ≡⇩p linepath 0 2› are not supported.
›

subsection ‹Joining a list of paths together›

text ‹
  The following operation takes a non-empty list of paths and joines them together
  left-to-right, i.e. it is an ‹n›-ary version of \<^const>‹joinpaths›. Associativity is to the right.

  A list of paths is considered well-formed if it is non-empty, each path is indeed a well-formed
  path, and each successive pair of paths has compatible ends.
›

fun joinpaths_list :: "(real ⇒ 'a :: real_normed_vector) list ⇒ real ⇒ 'a" where
  "joinpaths_list [] = linepath 0 0"
| "joinpaths_list [p] = p"
| "joinpaths_list (p # ps) = p +++ joinpaths_list ps"

lemma joinpaths_list_Cons [simp]: "ps ≠ [] ⟹ joinpaths_list (p # ps) = p +++ joinpaths_list ps"
  by (cases ps) auto

fun wf_pathlist :: "(real ⇒ 'a :: real_normed_vector) list ⇒ bool" where
  "wf_pathlist [] ⟷ False"
| "wf_pathlist [p] ⟷ path p"
| "wf_pathlist (p # q # ps) ⟷ path p ∧ path q ∧ pathfinish p = pathstart q ∧ wf_pathlist (q # ps)"

fun weak_wf_pathlist :: "(real ⇒ 'a :: real_normed_vector) list ⇒ bool" where
  "weak_wf_pathlist [] ⟷ False"
| "weak_wf_pathlist [p] ⟷ True"
| "weak_wf_pathlist (p # q # ps) ⟷ pathfinish p = pathstart q ∧ weak_wf_pathlist (q # ps)"

fun arc_joinpaths_list_aux :: "(real ⇒ 'a :: real_normed_vector) list ⇒ bool" where
  "arc_joinpaths_list_aux [] ⟷ False"
| "arc_joinpaths_list_aux [p] ⟷ True"
| "arc_joinpaths_list_aux (p # q # ps) ⟷
     path_image p ∩ path_image q ⊆ {pathfinish p} ∧
     (∀r∈set ps. path_image p ∩ path_image r = {}) ∧
     arc_joinpaths_list_aux (q # ps)"

definition arc_joinpaths_list :: "(real ⇒ 'a :: real_normed_vector) list ⇒ bool" where
  "arc_joinpaths_list ps ⟷ arc_joinpaths_list_aux ps ∧ (∀p∈set ps. arc p)"

fun simple_joinpaths_list :: "(real ⇒ 'a :: real_normed_vector) list ⇒ bool" where
  "simple_joinpaths_list [] ⟷ False"
| "simple_joinpaths_list [p] ⟷ simple_path p"
| "simple_joinpaths_list [p, q] ⟷
     path_image p ∩ path_image q ⊆ {pathfinish p} ∪ ({pathstart p} ∩ {pathfinish q}) ∧ arc p ∧ arc q"
| "simple_joinpaths_list (p # q # ps) ⟷
     path_image p ∩ path_image q ⊆ {pathfinish p} ∧
     (∀r∈set (butlast ps). path_image p ∩ path_image r = {}) ∧
     path_image p ∩ path_image (last ps) ⊆ {pathstart p} ∩ {pathfinish (last ps)} ∧
     arc_joinpaths_list_aux (q # ps) ∧ arc p ∧ (∀r∈set (q#ps). arc r)"

lemma simple_joinpaths_list_Cons [simp]:
  assumes "ps ≠ []"
  shows "simple_joinpaths_list (p # q # ps) ⟷
           path_image p ∩ path_image q ⊆ {pathfinish p} ∧
     (∀r∈set (butlast ps). path_image p ∩ path_image r = {}) ∧
     path_image p ∩ path_image (last ps) ⊆ {pathstart p} ∩ {pathfinish (last ps)} ∧
     arc_joinpaths_list_aux (q # ps) ∧ arc p ∧ (∀q∈set (q#ps). arc q)"
  using assms by (cases ps rule: simple_joinpaths_list.cases) simp_all


lemma wf_pathlist_Cons:
  "wf_pathlist (p # ps) ⟷ path p ∧ (ps = [] ∨ pathfinish p = pathstart (hd ps) ∧ wf_pathlist ps)"
  by (induction ps arbitrary: p) auto

lemma weak_wf_pathlist_Cons:
  "weak_wf_pathlist (p # ps) ⟷ (ps = [] ∨ pathfinish p = pathstart (hd ps) ∧ weak_wf_pathlist ps)"
  by (induction ps arbitrary: p) auto

fun valid_path_pathlist where
  "valid_path_pathlist [] ⟷ False"
| "valid_path_pathlist [p] ⟷ valid_path p"
| "valid_path_pathlist (p # ps) ⟷ valid_path p ∧ valid_path_pathlist ps"

lemma valid_path_pathlist_Cons:
  "valid_path_pathlist (p # ps) ⟷ valid_path p ∧ (ps = [] ∨ valid_path_pathlist ps)"
  by (cases ps) auto

lemma valid_path_pathlist_altdef: "valid_path_pathlist xs ⟷ xs ≠ [] ∧ list_all valid_path xs"
  by (induction xs) (auto simp: valid_path_pathlist_Cons)

lemma valid_path_weak_wf_pathlist_imp_wf:
  "valid_path_pathlist ps ⟹ weak_wf_pathlist ps ⟹ wf_pathlist ps"
  by (induction ps)
     (auto dest: valid_path_imp_path simp: valid_path_pathlist_Cons
                 weak_wf_pathlist_Cons wf_pathlist_Cons)

lemma wf_pathlist_append:
  assumes "ps ≠ []" "qs ≠ []"
  shows   "wf_pathlist (ps @ qs) ⟷
             wf_pathlist ps ∧ wf_pathlist qs ∧ pathfinish (last ps) = pathstart (hd qs)"
  using assms
  by (induction ps arbitrary: qs rule: wf_pathlist.induct) (auto simp: wf_pathlist_Cons)

lemma wf_pathlist_append':
  "wf_pathlist (ps @ qs) ⟷ (ps = [] ∧ wf_pathlist qs) ∨ (qs = [] ∧ wf_pathlist ps) ∨ 
     (wf_pathlist ps ∧ wf_pathlist qs ∧ pathfinish (last ps) = pathstart (hd qs))"
  using wf_pathlist_append[of ps qs] by (cases "ps = []"; cases "qs = []") auto

lemma weak_wf_pathlist_append:
  assumes "ps ≠ []" "qs ≠ []"
  shows   "weak_wf_pathlist (ps @ qs) ⟷
             weak_wf_pathlist ps ∧ weak_wf_pathlist qs ∧ pathfinish (last ps) = pathstart (hd qs)"
  using assms
  by (induction ps arbitrary: qs rule: weak_wf_pathlist.induct) (auto simp: weak_wf_pathlist_Cons)

lemma weak_wf_pathlist_append':
  "weak_wf_pathlist (ps @ qs) ⟷ (ps = [] ∧ weak_wf_pathlist qs) ∨ (qs = [] ∧ weak_wf_pathlist ps) ∨ 
     (weak_wf_pathlist ps ∧ weak_wf_pathlist qs ∧ pathfinish (last ps) = pathstart (hd qs))"
  using weak_wf_pathlist_append[of ps qs] by (cases "ps = []"; cases "qs = []") auto

lemma pathstart_joinpaths_list [simp]:
  "xs ≠ [] ⟹ pathstart (joinpaths_list xs) = pathstart (hd xs)"
  by (induction xs rule: joinpaths_list.induct) auto

lemma pathfinish_joinpaths_list [simp]:
  "xs ≠ [] ⟹ pathfinish (joinpaths_list xs) = pathfinish (last xs)"
  by (induction xs rule: joinpaths_list.induct) auto

lemma path_joinpaths_list [simp, intro]: "wf_pathlist xs ⟹ path (joinpaths_list xs)"
  by (induction xs rule: joinpaths_list.induct) auto

lemma valid_path_joinpaths_list [intro]:
  "valid_path_pathlist xs ⟹ weak_wf_pathlist xs ⟹ valid_path (joinpaths_list xs)"
  by (induction xs rule: joinpaths_list.induct) (auto intro!: valid_path_join)

lemma path_image_joinpaths_list:
  assumes "wf_pathlist ps"
  shows   "path_image (joinpaths_list ps) = (⋃p∈set ps. path_image p)"
  using assms by (induction ps rule: wf_pathlist.induct) (auto simp: path_image_join)

lemma joinpaths_list_append:
  assumes "wf_pathlist xs" "wf_pathlist ys" "pathfinish (last xs) = pathstart (hd ys)"
  shows   "joinpaths_list (xs @ ys) ≡⇩p joinpaths_list xs +++ joinpaths_list ys"
proof -
  from assms(1) have "xs ≠ []"
    by auto
  from assms show ?thesis
  proof (induction xs arbitrary: ys rule: joinpaths_list.induct)
    case (2 p ys)
    have "ys ≠ []"
      using 2 by auto
    then obtain y ys' where [simp]: "ys = y # ys'"
      by (cases ys) auto
    show ?case using 2 by auto
  next
    case (3 p1 p2 ps qs)
    obtain q qs' where [simp]: "qs = q # qs'"
      using 3 by (cases qs) auto
    have "joinpaths_list ((p1 # p2 # ps) @ qs) =
          p1 +++ joinpaths_list ((p2 # ps) @ qs)"
      by simp
    also have "… ≡⇩p p1 +++ joinpaths_list (p2 # ps) +++ joinpaths_list qs"
      using 3 by (intro eq_paths_join eq_paths_refl 3) auto
    also have "… ≡⇩p (p1 +++ joinpaths_list (p2 # ps)) +++ joinpaths_list qs"
      by (intro eq_paths_join_assoc2) (use 3 in auto)
    finally show ?case
      by simp
  qed auto
qed

lemma arc_joinpaths_list_weak_wf_imp_wf:
  assumes "weak_wf_pathlist xs" "arc_joinpaths_list xs"
  shows   "wf_pathlist xs"
  using assms
  by (induction xs rule: wf_pathlist.induct) (auto intro: arc_imp_path simp: arc_joinpaths_list_def)

lemma arc_joinpaths_aux:
  assumes "wf_pathlist xs" "arc_joinpaths_list_aux xs" "∀x∈set xs. arc x"
  shows   "arc (joinpaths_list xs)"
  using assms
proof (induction xs rule: wf_pathlist.induct)
  case (3 p q ps)
  thus ?case 
    by (fastforce intro!: arc_join simp: path_image_joinpaths_list)
qed auto

lemma arc_joinpaths_list [intro?]:
  assumes "weak_wf_pathlist xs" "arc_joinpaths_list xs"
  shows   "arc (joinpaths_list xs)"
  using assms arc_joinpaths_aux[of xs] arc_joinpaths_list_weak_wf_imp_wf[of xs]
  by (auto simp: arc_joinpaths_list_def)

lemma simple_joinpaths_list_weak_wf_imp_wf:
  assumes "weak_wf_pathlist xs" "simple_joinpaths_list xs"
  shows   "wf_pathlist xs"
  using arc_joinpaths_list_weak_wf_imp_wf[of "tl xs"] assms
  by (cases xs rule: simple_joinpaths_list.cases)
     (auto dest: simple_path_imp_path arc_imp_path simp: arc_joinpaths_list_def)

lemma simple_path_joinpaths_list [intro?]:
  assumes "weak_wf_pathlist xs" "simple_joinpaths_list xs"
  shows   "simple_path (joinpaths_list xs)"
proof (cases xs rule: simple_joinpaths_list.cases)
  case (3 p q)
  thus ?thesis using assms
    by (force split: if_splits intro!: simple_path_joinI)
next
  case (4 p q r rs)
  define rs' where "rs' = r # rs"
  have [simp]: "rs' ≠ []"
    by (auto simp: rs'_def)
  have [simp]: "xs = p # q # rs'"
    by (simp add: 4 rs'_def)
  note [simp] = wf_pathlist_Cons

  have "simple_path (p +++ joinpaths_list (q # rs'))"
  proof (rule simple_path_joinI)
    show "arc p" 
      using assms by auto
  next
    show "arc (joinpaths_list (q # rs'))" using assms
      by (intro arc_joinpaths_list) (auto split: if_splits simp: arc_joinpaths_list_def)
  next
    have *: "set rs' = insert (last rs') (set (butlast rs'))"
      by (subst append_butlast_last_id [symmetric]) (auto simp del: append_butlast_last_id)
    have "wf_pathlist (q # rs')"
      using assms arc_joinpaths_list_weak_wf_imp_wf[of "q # rs'"]
      by (auto simp: arc_joinpaths_list_def)
    thus "path_image p ∩ path_image (joinpaths_list (q # rs'))
            ⊆ insert (pathstart (joinpaths_list (q # rs')))
           (if pathstart p = pathfinish (joinpaths_list (q # rs')) then {pathstart p} else {})"
      using assms by (subst path_image_joinpaths_list) (auto simp: *)
  qed (use assms in auto)
  thus ?thesis
    by (simp add: rs'_def)
qed (use assms in auto)

lemma wf_pathlist_sublist:
  assumes "wf_pathlist ys" "sublist xs ys" "xs ≠ []"
  shows   "wf_pathlist xs"
proof -
  from assms(2) obtain as bs where *: "ys = as @ xs @ bs"
    by (auto simp: sublist_def)
  have **: "wf_pathlist xs" if "wf_pathlist (xs @ bs)"
    using that ‹xs ≠ []› by (induction xs rule: wf_pathlist.induct) (auto simp: wf_pathlist_Cons)
  show ?thesis
    using assms(1) ‹xs ≠ []› unfolding *
    by (induction as) (auto simp: ** wf_pathlist_Cons)
qed


lemma is_subpath_joinpaths_list_append_right:
  assumes "wf_pathlist (xs @ ys)" "xs ≠ []"
  shows   "is_subpath (joinpaths_list xs) (joinpaths_list (xs @ ys))"
proof (cases "ys = []")
  case False
  hence "is_subpath (joinpaths_list xs) (joinpaths_list xs +++ joinpaths_list ys)"
    using assms by (intro is_subpath_joinI1 path_joinpaths_list) (auto simp: wf_pathlist_append)
  also have "eq_paths … (joinpaths_list (xs @ ys))"
    using False assms by (intro eq_paths_sym[OF joinpaths_list_append])
                         (auto simp: wf_pathlist_append)
  finally show ?thesis .
qed (use assms in auto)

lemma is_subpath_joinpaths_list_append_left:
  assumes "wf_pathlist (xs @ ys)" "ys ≠ []"
  shows   "is_subpath (joinpaths_list ys) (joinpaths_list (xs @ ys))"
proof (cases "xs = []")
  case False
  hence "is_subpath (joinpaths_list ys) (joinpaths_list xs +++ joinpaths_list ys)"
    using assms by (intro is_subpath_joinI2 path_joinpaths_list) (auto simp: wf_pathlist_append)
  also have "eq_paths … (joinpaths_list (xs @ ys))"
    using False assms by (intro eq_paths_sym[OF joinpaths_list_append])
                         (auto simp: wf_pathlist_append)
  finally show ?thesis .
qed (use assms in auto)

lemma is_subpath_joinpaths_list:
  assumes "wf_pathlist ys" "sublist xs ys" "xs ≠ []"
  shows   "is_subpath (joinpaths_list xs) (joinpaths_list ys)"
proof -
  from assms(2) obtain as bs where *: "ys = as @ xs @ bs"
    by (auto simp: sublist_def)
  have "is_subpath (joinpaths_list xs) (joinpaths_list (xs @ bs))"
    using assms by (intro is_subpath_joinpaths_list_append_right)
                   (auto simp: wf_pathlist_append' *)
  also have "is_subpath … (joinpaths_list (as @ xs @ bs))"
    using assms by (intro is_subpath_joinpaths_list_append_left)
                   (auto simp: wf_pathlist_append' *)    
  finally show ?thesis
    by (simp add: *)
qed

lemma eq_loops_joinpaths_list_append:
  assumes "wf_pathlist (xs @ ys)" "pathfinish (last (xs @ ys)) = pathstart (hd (xs @ ys))"
  shows   "eq_loops (joinpaths_list (xs @ ys)) (joinpaths_list (ys @ xs))"
proof (cases "xs = [] ∨ ys = []")
  case True
  have "xs ≠ [] ∨ ys ≠ []"
    using assms by auto
  with True show ?thesis
    using assms by auto
next
  case False
  have "eq_paths (joinpaths_list (xs @ ys)) (joinpaths_list xs +++ joinpaths_list ys)"
    using assms False by (intro joinpaths_list_append) (auto simp: wf_pathlist_append)
  also have "eq_loops … (joinpaths_list ys +++ joinpaths_list xs)"
    using assms False by (intro eq_loops_joinpaths_commute) (auto simp: wf_pathlist_append)
  also have "eq_paths … (joinpaths_list (ys @ xs))"
    using assms False
    by (intro eq_paths_sym[OF joinpaths_list_append]) (auto simp: wf_pathlist_append)
  finally show ?thesis .
qed

lemma eq_loops_rotate:
  assumes "wf_pathlist xs" "pathfinish (last xs) = pathstart (hd xs)"
  shows   "eq_loops (joinpaths_list xs) (joinpaths_list (rotate n xs))"
proof -
  define m where "m = n mod length xs"
  have "eq_loops (joinpaths_list (take m xs @ drop m xs))
                 (joinpaths_list (drop m xs @ take m xs))"
    using assms by (intro eq_loops_joinpaths_list_append) auto
  thus ?thesis
    by (simp add: m_def rotate_drop_take)
qed

lemma winding_number_joinpaths_list:
  assumes "wf_pathlist ps" "⋀p. p ∈ set ps ⟹ x ∉ path_image p"
  shows   "winding_number (joinpaths_list ps) x = (∑p←ps. winding_number p x)"
  using assms
proof (induction ps rule: wf_pathlist.induct)
  case (3 p q ps)
  have "winding_number (joinpaths_list (p # q # ps)) x =
        winding_number (p +++ joinpaths_list (q # ps)) x"
    by simp
  also have "… = winding_number p x + winding_number (joinpaths_list (q # ps)) x"
    using "3.prems" by (intro winding_number_join) (auto simp: path_image_joinpaths_list)
  also have "winding_number (joinpaths_list (q # ps)) x = (∑r←q#ps. winding_number r x)"
    by (intro "3.IH") (use "3.prems" in auto)
  finally show ?case
    by simp
qed auto

lemma contour_integral_joinpaths_list:
  assumes "weak_wf_pathlist ps" "valid_path_pathlist ps"
          "f contour_integrable_on (joinpaths_list ps)"
  shows   "contour_integral (joinpaths_list ps) f = (∑p←ps. contour_integral p f)"
  using assms
proof (induction ps rule: wf_pathlist.induct)
  case (3 p q ps)
  have wf: "wf_pathlist (p # q # ps)"
    using "3.prems" valid_path_weak_wf_pathlist_imp_wf by blast
  have int: "f contour_integrable_on (p +++ joinpaths_list (q # ps))"
    using "3.prems" by simp
  have int1: "f contour_integrable_on p"
    using contour_integrable_joinD1[OF int] "3.prems" by auto 
  have int2: "f contour_integrable_on joinpaths_list (q # ps)"
    using contour_integrable_joinD2[OF int] "3.prems" by auto

  have "contour_integral (joinpaths_list (p # q # ps)) f =
        contour_integral (p +++ joinpaths_list (q # ps)) f"
    by simp
  also have "… = contour_integral p f + contour_integral (joinpaths_list (q # ps)) f"
    using "3.prems" int1 int2 by (intro contour_integral_join) auto
  also have "contour_integral (joinpaths_list (q # ps)) f = (∑r←q#ps. contour_integral r f)"
    by (intro "3.IH") (use "3.prems" int2 in auto)
  finally show ?case
    by simp
qed auto


subsection ‹Representing a sequence of path joins as a tree›

text ‹
  To deal with the problem that path joining is not associative, we define an expression tree
  to represent all the possible different bracketings of joining ‹n› paths together.

  There is also a ``flattening'' operation to convert the tree to a list of paths, since our
  eventual goal is to show that the order does not matter (up to path equivalence).

  Well-formedness is again defined similarly to the list case.
›

datatype 'a joinpaths_tree =
  Path "real ⇒ 'a" | Reverse "'a joinpaths_tree" | Join "'a joinpaths_tree" "'a joinpaths_tree"

primrec paths_joinpaths_tree :: "'a joinpaths_tree ⇒ (real ⇒ 'a) set" where
  "paths_joinpaths_tree (Path p) = {p}"
| "paths_joinpaths_tree (Reverse p) = paths_joinpaths_tree p"
| "paths_joinpaths_tree (Join l r) = paths_joinpaths_tree l ∪ paths_joinpaths_tree r"

fun start_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ 'a"
and finish_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ 'a" where
  "start_joinpaths_tree (Path p) = pathstart p"
| "start_joinpaths_tree (Reverse p) = finish_joinpaths_tree p"
| "start_joinpaths_tree (Join l r) = start_joinpaths_tree l"
| "finish_joinpaths_tree (Path p) = pathfinish p"
| "finish_joinpaths_tree (Reverse p) = start_joinpaths_tree p"
| "finish_joinpaths_tree (Join l r) = finish_joinpaths_tree r"

primrec eval_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ real ⇒ 'a" where
  "eval_joinpaths_tree (Path p) = p"
| "eval_joinpaths_tree (Reverse t) = reversepath (eval_joinpaths_tree t)"
| "eval_joinpaths_tree (Join l r) = eval_joinpaths_tree l +++ eval_joinpaths_tree r"

primrec flatten_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ (real ⇒ 'a) list" where
  "flatten_joinpaths_tree (Path p) = [p]"
| "flatten_joinpaths_tree (Reverse t) = rev (map reversepath (flatten_joinpaths_tree t))"
| "flatten_joinpaths_tree (Join l r) = flatten_joinpaths_tree l @ flatten_joinpaths_tree r"

primrec wf_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ bool" where
  "wf_joinpaths_tree (Path p) ⟷ path p"
| "wf_joinpaths_tree (Reverse t) ⟷ wf_joinpaths_tree t"
| "wf_joinpaths_tree (Join l r) ⟷
     wf_joinpaths_tree l ∧ wf_joinpaths_tree r ∧ finish_joinpaths_tree l = start_joinpaths_tree r"

primrec weak_wf_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ bool" where
  "weak_wf_joinpaths_tree (Path p) ⟷ True"
| "weak_wf_joinpaths_tree (Reverse t) ⟷ weak_wf_joinpaths_tree t"
| "weak_wf_joinpaths_tree (Join l r) ⟷
     weak_wf_joinpaths_tree l ∧ weak_wf_joinpaths_tree r ∧ finish_joinpaths_tree l = start_joinpaths_tree r"

primrec valid_path_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ bool" where
  "valid_path_joinpaths_tree (Path p) ⟷ valid_path p"
| "valid_path_joinpaths_tree (Reverse p) ⟷ valid_path_joinpaths_tree p"
| "valid_path_joinpaths_tree (Join l r) ⟷
     valid_path_joinpaths_tree l ∧ valid_path_joinpaths_tree r ∧ finish_joinpaths_tree l = start_joinpaths_tree r"

primrec arc_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ bool" where
  "arc_joinpaths_tree (Path p) ⟷ arc p"
| "arc_joinpaths_tree (Reverse p) ⟷ arc_joinpaths_tree p"
| "arc_joinpaths_tree (Join l r) ⟷
     (∀l'∈paths_joinpaths_tree l. ∀r'∈paths_joinpaths_tree r.
          path_image l' ∩ path_image r' ⊆ {finish_joinpaths_tree l}) ∧
     arc_joinpaths_tree l ∧ arc_joinpaths_tree r"

primrec simple_joinpaths_tree :: "'a :: real_normed_vector joinpaths_tree ⇒ bool" where
  "simple_joinpaths_tree (Path p) ⟷ simple_path p"
| "simple_joinpaths_tree (Reverse t) ⟷ simple_joinpaths_tree t"
| "simple_joinpaths_tree (Join l r) ⟷ 
     (∀l'∈paths_joinpaths_tree l. ∀r'∈paths_joinpaths_tree r.
        path_image l' ∩ path_image r' ⊆
           {finish_joinpaths_tree l} ∪ ({start_joinpaths_tree l} ∩ {finish_joinpaths_tree r})) ∧
     arc_joinpaths_tree l ∧ arc_joinpaths_tree r"

lemma flatten_joinpaths_tree_nonempty [simp]: "flatten_joinpaths_tree t ≠ []"
  by (induction t) auto



lemma pathstart_eval_joinpaths_tree [simp]: "pathstart (eval_joinpaths_tree t) = start_joinpaths_tree t"
  and pathfinish_eval_joinpaths_tree [simp]: "pathfinish (eval_joinpaths_tree t) = finish_joinpaths_tree t"
  by (induction t) auto

lemma pathstart_last_flatten_joinpaths_tree [simp]:
        "pathstart (hd (flatten_joinpaths_tree t)) = start_joinpaths_tree t" (is ?th1)
  and pathfinish_last_flatten_joinpaths_tree [simp]:
        "pathfinish (last (flatten_joinpaths_tree t)) = finish_joinpaths_tree t" (is ?th2)
  by (induction t and t rule: start_joinpaths_tree_finish_joinpaths_tree.induct)
     (auto simp: hd_rev last_rev hd_map last_map)

lemma wf_pathlist_map_rev [simp]: "wf_pathlist (map reversepath xs) ⟷ wf_pathlist (rev xs)"
  by (induction xs) (auto simp: wf_pathlist_Cons hd_map wf_pathlist_append' last_rev)

lemma weak_wf_pathlist_map_rev' [simp]: "weak_wf_pathlist (map reversepath xs) ⟷ weak_wf_pathlist (rev xs)"
  by (induction xs) (auto simp: weak_wf_pathlist_Cons weak_wf_pathlist_append' last_rev rev_map hd_map)

lemma weak_wf_pathlist_map_rev [simp]: "weak_wf_pathlist (rev (map reversepath xs)) ⟷ weak_wf_pathlist xs"
  by (induction xs) (auto simp: weak_wf_pathlist_Cons weak_wf_pathlist_append' last_rev rev_map hd_map last_map)

lemma wf_pathlist_map_rev' [simp]: "wf_pathlist (rev (map reversepath xs)) ⟷ wf_pathlist xs"
  by (induction xs) (auto simp: wf_pathlist_Cons hd_map wf_pathlist_append' last_rev)

lemma wf_pathlist_flatten_pathree [simp]: "wf_pathlist (flatten_joinpaths_tree t) ⟷ wf_joinpaths_tree t"
  by (induction t) (auto simp: wf_pathlist_append rev_map)

lemma weak_wf_pathlist_flatten_pathree [simp]:
  "weak_wf_pathlist (flatten_joinpaths_tree t) ⟷ weak_wf_joinpaths_tree t"
  by (induction t) (auto simp: weak_wf_pathlist_append)

lemma reversepath_joinpaths_list:
  assumes "wf_pathlist xs"
  shows   "reversepath (joinpaths_list xs) ≡⇩p joinpaths_list (rev (map reversepath xs))"
  using assms
proof (induction xs rule: wf_pathlist.induct)
  case (3 p q ps)
  have "reversepath (joinpaths_list (p # q # ps)) =
        reversepath (joinpaths_list (q # ps)) +++ reversepath p"
    using 3 by (simp_all add: reversepath_joinpaths)
  also have "… ≡⇩p joinpaths_list (rev (map reversepath (q # ps))) +++ reversepath p"
    using 3 by (intro eq_paths_join) auto
  also have "… = joinpaths_list (rev (map reversepath (q # ps))) +++ joinpaths_list [reversepath p]"
    by simp
  also have "… ≡⇩p joinpaths_list (rev (map reversepath (q # ps)) @ [reversepath p])"
    using 3 by (intro eq_paths_sym[OF joinpaths_list_append])
               (auto simp: wf_pathlist_append' last_rev hd_map wf_pathlist_Cons)
  finally show ?case
    by simp
qed auto

lemma joinpaths_flatten_joinpaths_tree:
  assumes "wf_joinpaths_tree t"
  shows   "eval_joinpaths_tree t ≡⇩p joinpaths_list (flatten_joinpaths_tree t)"
  using assms
proof (induction t)
  case (Path p)
  thus ?case by simp
next
  case (Reverse t)
  have "eval_joinpaths_tree (Reverse t) ≡⇩p
        reversepath (joinpaths_list (flatten_joinpaths_tree t))"
    unfolding eval_joinpaths_tree.simps using Reverse.prems
    by (intro eq_paths_reverse Reverse.IH) auto 
  also have "… ≡⇩p joinpaths_list (rev (map reversepath (flatten_joinpaths_tree t)))"
    by (intro reversepath_joinpaths_list) (use Reverse in auto)
  finally show ?case
    by simp
next
  case (Join l r)
  have "eval_joinpaths_tree l +++ eval_joinpaths_tree r ≡⇩p
          joinpaths_list (flatten_joinpaths_tree l) +++ joinpaths_list (flatten_joinpaths_tree r)"
    using Join by (intro eq_paths_join) auto
  also have "… ≡⇩p joinpaths_list (flatten_joinpaths_tree l @ flatten_joinpaths_tree r)"
    by (rule eq_paths_sym[OF joinpaths_list_append]) (use Join in auto)
  finally show ?case
    by simp
qed

lemma valid_path_joinpaths_tree:
  fixes t :: "'a :: real_normed_field joinpaths_tree"
  shows "valid_path_joinpaths_tree t ⟹ valid_path (eval_joinpaths_tree t)"
  by (induction t) auto

lemma path_image_eval_joinpaths_tree:
  "wf_joinpaths_tree t ⟹
     path_image (eval_joinpaths_tree t) = (⋃p∈paths_joinpaths_tree t. path_image p)"
  by (induction t) (auto simp: path_image_join)

lemma arc_joinpaths_tree [intro?]:
  "wf_joinpaths_tree t ⟹ arc_joinpaths_tree t ⟹ arc (eval_joinpaths_tree t)"
  by (induction t) (auto simp: arc_join_eq path_image_eval_joinpaths_tree intro!: arc_reversepath)

lemma simple_joinpaths_tree [intro?]:
  "wf_joinpaths_tree t ⟹ simple_joinpaths_tree t ⟹ simple_path (eval_joinpaths_tree t)"
  by (induction t)
    (fastforce intro!: simple_path_joinI arc_joinpaths_tree split: if_splits
               simp: path_image_eval_joinpaths_tree simple_path_reversepath_iff)+


subsection ‹Equivalence of two join trees›

text ‹
  Two trees are considered equivalent if they flatten to the same list of paths.
  Equivalence implies that one tree is well-formed if and only if the other one is as well,
  and in that case that their evaluations are equivalent paths.
›

definition equiv_joinpaths_tree ::
  "('a :: real_normed_vector joinpaths_tree) ⇒ 'a joinpaths_tree ⇒ bool" where
  "equiv_joinpaths_tree t1 t2 ⟷ flatten_joinpaths_tree t1 = flatten_joinpaths_tree t2"

lemma equiv_joinpaths_tree_imp_wf_iff:
  "equiv_joinpaths_tree t1 t2 ⟹ wf_joinpaths_tree t1 ⟷ wf_joinpaths_tree t2"
  by (metis equiv_joinpaths_tree_def wf_pathlist_flatten_pathree)

lemma equiv_joinpaths_tree_imp_eval_eq:
  "equiv_joinpaths_tree t1 t2 ⟹ wf_joinpaths_tree t1 ⟹
     eval_joinpaths_tree t1 ≡⇩p eval_joinpaths_tree t2"
  by (metis eq_paths_sym eq_paths_trans equiv_joinpaths_tree_def
            equiv_joinpaths_tree_imp_wf_iff joinpaths_flatten_joinpaths_tree)



subsection ‹Implementation›

named_theorems path_automation_simps
named_theorems path_automation_intros


text ‹
  The following allows us to reify an expression containing join operations into a tree.
  One might be able to incorporate path reversal as well.
›

definition REIFY_JOINPATHS_TAG where "REIFY_JOINPATHS_TAG x = x"

lemma REIFY_JOINPATHS_TAG:
  "REIFY_JOINPATHS_TAG (x :: real ⇒ 'a :: real_normed_vector) = y ⟹ x = y"
  by (simp add: REIFY_JOINPATHS_TAG_def)

named_theorems reify_joinpath_tree

lemma reify_joinpaths_tree [reify_joinpath_tree]:
  "REIFY_JOINPATHS_TAG (reversepath p) = reversepath (REIFY_JOINPATHS_TAG p)"
  "REIFY_JOINPATHS_TAG (p +++ q) = REIFY_JOINPATHS_TAG p +++ REIFY_JOINPATHS_TAG q"
  "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree (Path p)"
  "eval_joinpaths_tree l +++ eval_joinpaths_tree r = eval_joinpaths_tree (Join l r)"
  "reversepath (eval_joinpaths_tree t) = eval_joinpaths_tree (Reverse t)"
  by (simp_all add: REIFY_JOINPATHS_TAG_def)


lemma path_via_joinpaths_tree [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "wf_joinpaths_tree t"
  shows   "path p"
  using assms joinpaths_flatten_joinpaths_tree[of t] by (auto simp: REIFY_JOINPATHS_TAG_def)

lemma valid_path_via_joinpaths_tree [path_automation_intros]:
  fixes p :: "real ⇒ 'a :: real_normed_field"
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "valid_path_joinpaths_tree t"
  shows   "valid_path p"
  using assms valid_path_joinpaths_tree[of t] by (auto simp: REIFY_JOINPATHS_TAG_def)

lemma arc_via_joinpaths_tree [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "arc_joinpaths_list (flatten_joinpaths_tree t) ∧ weak_wf_joinpaths_tree t"
  shows   "arc p"
proof -
  have wf: "wf_joinpaths_tree t"
    using arc_joinpaths_list_weak_wf_imp_wf[of "flatten_joinpaths_tree t"] assms
    by auto
  have "arc (joinpaths_list (flatten_joinpaths_tree t))"
    using assms by (intro arc_joinpaths_list) auto
  moreover have "eval_joinpaths_tree t ≡⇩p joinpaths_list (flatten_joinpaths_tree t)"
    using wf by (intro joinpaths_flatten_joinpaths_tree) auto
  ultimately show ?thesis
    using assms eq_paths_imp_arc_iff unfolding REIFY_JOINPATHS_TAG_def by metis
qed

lemma simple_path_via_joinpaths_tree [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "simple_joinpaths_list (flatten_joinpaths_tree t) ∧ weak_wf_joinpaths_tree t"
  shows   "simple_path p"
proof -
  have wf: "wf_joinpaths_tree t"
    using simple_joinpaths_list_weak_wf_imp_wf[of "flatten_joinpaths_tree t"] assms
    by auto
  have "simple_path (joinpaths_list (flatten_joinpaths_tree t))"
    using assms by (intro simple_path_joinpaths_list) auto
  moreover have "eval_joinpaths_tree t ≡⇩p joinpaths_list (flatten_joinpaths_tree t)"
    using wf by (intro joinpaths_flatten_joinpaths_tree) auto
  ultimately show ?thesis
    using assms eq_paths_imp_simple_path_iff unfolding REIFY_JOINPATHS_TAG_def by metis
qed

lemma eq_paths_via_reify_joinpaths [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t1"
  assumes "REIFY_JOINPATHS_TAG q = eval_joinpaths_tree t2"
  assumes "wf_joinpaths_tree t1 ∧ wf_joinpaths_tree t2 ∧ 
           flatten_joinpaths_tree t1 = flatten_joinpaths_tree t2"
  shows   "eq_paths p q"
  using assms unfolding REIFY_JOINPATHS_TAG_def
  by (simp add: equiv_joinpaths_tree_def equiv_joinpaths_tree_imp_eval_eq)

definition is_rotation_of :: "'a list ⇒ 'a list ⇒ bool" where
  "is_rotation_of xs ys ⟷ (∃n. xs = rotate n ys)"

fun is_rotation_of_aux :: "'a list ⇒ 'a list ⇒ nat ⇒ bool" where
  "is_rotation_of_aux xs ys 0 ⟷ False"
| "is_rotation_of_aux xs [] _ ⟷ xs = []"
| "is_rotation_of_aux xs (y # ys) (Suc n) ⟷
    xs = y # ys ∨ is_rotation_of_aux xs (ys @ [y]) n"

lemma is_rotation_of_aux_correct: "is_rotation_of_aux xs ys n ⟷ (∃k<n. xs = rotate k ys)"
proof (induction xs ys n rule: is_rotation_of_aux.induct)
  case (3 xs y ys n)
  show ?case
  proof
    assume "is_rotation_of_aux xs (y # ys) (Suc n)"
    hence "xs = y # ys ∨ is_rotation_of_aux xs (ys @ [y]) n"
      by auto
    thus "∃k<Suc n. xs = rotate k (y # ys)"
    proof
      assume "xs = y # ys"
      thus ?thesis
        by (intro exI[of _ 0]) auto
    next
      assume "is_rotation_of_aux xs (ys @ [y]) n"
      with 3 obtain k where "k < n" "xs = rotate k (ys @ [y])"
        by blast
      thus "∃k<Suc n. xs = rotate k (y # ys)"
        by (intro exI[of _ "Suc k"]) (auto simp: rotate1_rotate_swap)
    qed
  next
    assume "∃k<Suc n. xs = rotate k (y # ys)"
    then obtain k where k: "k < Suc n" "xs = rotate k (y # ys)"
      by blast
    show "is_rotation_of_aux xs (y # ys) (Suc n)"
    proof (cases k)
      case 0
      with k show ?thesis by simp
    next
      case (Suc k')
      with k have "k' < n" "xs = rotate k' (ys @ [y])"
        by (simp_all add: rotate1_rotate_swap)
      with 3 have "is_rotation_of_aux xs (ys @ [y]) n"
        by blast
      thus ?thesis by simp
    qed
  qed
qed auto

lemma is_rotation_of_code [code]:
  "is_rotation_of xs ys ⟷ length xs = length ys ∧ (xs = [] ∨ is_rotation_of_aux xs ys (length xs))"
proof (intro iffI conjI)
  assume "is_rotation_of xs ys"
  then obtain n where n: "xs = rotate n ys"
    by (auto simp: is_rotation_of_def)
  also have "rotate n ys = rotate (n mod length ys) ys"
    by (simp add: rotate_drop_take)
  also have "length ys = length xs"
    by (simp add: n)
  finally have "xs = rotate (n mod length xs) ys"
    by simp
  moreover have "n mod length xs < length xs" if "xs ≠ []"
    using that by auto
  ultimately show "xs = [] ∨ is_rotation_of_aux xs ys (length xs)"
    unfolding is_rotation_of_aux_correct by blast
qed (auto simp: is_rotation_of_def is_rotation_of_aux_correct)

lemma eq_loops_via_reify_joinpaths [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t1"
  assumes "REIFY_JOINPATHS_TAG q = eval_joinpaths_tree t2"
  assumes "wf_joinpaths_tree t1 ∧ wf_joinpaths_tree t2 ∧ 
           finish_joinpaths_tree t2 = start_joinpaths_tree t2 ∧
           is_rotation_of (flatten_joinpaths_tree t1) (flatten_joinpaths_tree t2)"
  shows   "eq_loops p q"
proof -
  from assms obtain n where n: "flatten_joinpaths_tree t1 = rotate n (flatten_joinpaths_tree t2)"
    unfolding is_rotation_of_def by blast
  have "eq_paths (eval_joinpaths_tree t2) (joinpaths_list (flatten_joinpaths_tree t2))"
    using assms eq_paths_sym_iff joinpaths_flatten_joinpaths_tree by blast
  also have "eq_loops … (joinpaths_list (flatten_joinpaths_tree t1))"
    unfolding n by (intro eq_loops_rotate) (use assms in auto)
  also have "eq_paths … (eval_joinpaths_tree t1)"
    using assms eq_paths_sym_iff joinpaths_flatten_joinpaths_tree by blast
  finally show ?thesis
    using assms by (simp add: eq_loops_sym_iff REIFY_JOINPATHS_TAG_def)
qed

lemma is_subpath_via_reify_joinpaths [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t1"
  assumes "REIFY_JOINPATHS_TAG q = eval_joinpaths_tree t2"
  assumes "wf_joinpaths_tree t1 ∧ wf_joinpaths_tree t2 ∧
           sublist (flatten_joinpaths_tree t1) (flatten_joinpaths_tree t2)"
  shows   "is_subpath p q"
  using assms unfolding REIFY_JOINPATHS_TAG_def
  by (meson eq_paths_sym flatten_joinpaths_tree_nonempty is_subpath_eq_paths_trans
       is_subpath_joinpaths_list joinpaths_flatten_joinpaths_tree wf_pathlist_flatten_pathree)

lemma sum_list_singleton: "sum_list [x] = x"
  by simp

lemma sum_list_Cons_rev: "sum_list (x # y # xs) = sum_list (y # xs) + (x :: 'a :: comm_monoid_add)"
  by (simp add: add_ac)

lemma winding_number_via_joinpaths [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "(∑q←rev (flatten_joinpaths_tree t). winding_number q x) = T ∧ 
           (∀p∈set (flatten_joinpaths_tree t). x ∉ path_image p) ∧
           weak_wf_joinpaths_tree t ∧ valid_path_pathlist (flatten_joinpaths_tree t)"
  shows   "winding_number p x = T"
proof -
  have wf: "wf_joinpaths_tree t"
    using assms valid_path_weak_wf_pathlist_imp_wf weak_wf_pathlist_flatten_pathree
          wf_pathlist_flatten_pathree by blast
  have "p ≡⇩p joinpaths_list (flatten_joinpaths_tree t)"
    using assms wf unfolding REIFY_JOINPATHS_TAG_def
    by (metis joinpaths_flatten_joinpaths_tree)
  hence "winding_number p x = winding_number (joinpaths_list (flatten_joinpaths_tree t)) x"
    using assms wf by (intro eq_paths_imp_winding_number_eq) (auto simp: path_image_joinpaths_list)
  also have "… = (∑p←flatten_joinpaths_tree t. winding_number p x)"
    using wf assms by (subst winding_number_joinpaths_list) auto
  finally show ?thesis using assms by (simp flip: rev_map)
qed

lemma valid_path_pathlist_flatten_imp_valid_path_eval_joinpaths_tree:
  assumes "weak_wf_pathlist (flatten_joinpaths_tree t)"
  assumes "valid_path_pathlist (flatten_joinpaths_tree t)"
  shows   "valid_path (eval_joinpaths_tree t)"
  using assms
  by (induction t)
     (auto intro!: valid_path_join simp: valid_path_pathlist_altdef
                   weak_wf_pathlist_append list.pred_map o_def)

lemma path_image_eval_joinpaths_tree':
  assumes "wf_joinpaths_tree t"
  shows   "path_image (eval_joinpaths_tree t) = (⋃p∈set (flatten_joinpaths_tree t). path_image p)"
  using assms by (induction t) (simp_all add: path_image_join) 


lemma contour_integral_via_joinpaths [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "(∑q←rev (flatten_joinpaths_tree t). contour_integral q f) = T ∧
           f analytic_on (path_image p) ∧
           weak_wf_joinpaths_tree t ∧ valid_path_pathlist (flatten_joinpaths_tree t)"
  shows   "contour_integral p f = T"
proof -
  have valid: "valid_path (eval_joinpaths_tree t)"
    by (intro valid_path_pathlist_flatten_imp_valid_path_eval_joinpaths_tree) (use assms in auto)
  have wf: "wf_joinpaths_tree t"
    using assms valid_path_weak_wf_pathlist_imp_wf weak_wf_pathlist_flatten_pathree
          wf_pathlist_flatten_pathree by blast
  have int: "f contour_integrable_on joinpaths_list (flatten_joinpaths_tree t)"
    using assms wf path_image_eval_joinpaths_tree'[OF wf]
    by (intro analytic_imp_contour_integrable valid_path_joinpaths_list)
       (auto simp: path_image_joinpaths_list REIFY_JOINPATHS_TAG_def)
  have eq: "p ≡⇩p joinpaths_list (flatten_joinpaths_tree t)"
    using assms wf unfolding REIFY_JOINPATHS_TAG_def
    by (metis joinpaths_flatten_joinpaths_tree)
  moreover have "f analytic_on path_image (eval_joinpaths_tree t) ∩ ⋃ (path_image ` set (flatten_joinpaths_tree t))"
  proof (rule analytic_on_subset[of f "path_image p"])
    have "path_image (eval_joinpaths_tree t) = path_image p"
      using assms by (simp add: path_image_joinpaths_list REIFY_JOINPATHS_TAG_def)
    thus "path_image (eval_joinpaths_tree t) ∩ ⋃ (path_image ` set (flatten_joinpaths_tree t))
            ⊆ path_image p" by simp
  qed (use assms in auto)
  ultimately have "contour_integral p f = contour_integral (joinpaths_list (flatten_joinpaths_tree t)) f"
    using assms wf valid
    by (intro eq_paths_imp_contour_integral_eq)
       (auto simp: path_image_joinpaths_list REIFY_JOINPATHS_TAG_def)
  also have "… = (∑p←flatten_joinpaths_tree t. contour_integral p f)"
    using wf assms int by (subst contour_integral_joinpaths_list) auto
  finally show ?thesis 
    using assms by (simp flip: rev_map)
qed

text ‹
  The following is an alternative way to split contour integrals that uses holomorphicity
  w.r.t.\ a user-defined region rather than analyticity on the path. This may sometimes be
  more convenient.
›
lemma contour_integral_via_joinpaths_holo:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "(∑q←rev (flatten_joinpaths_tree t). contour_integral q f) = T ∧
           f holomorphic_on A ∧ open A ∧ path_image p ⊆ A ∧
           weak_wf_joinpaths_tree t ∧ valid_path_pathlist (flatten_joinpaths_tree t)"
  shows   "contour_integral p f = T"
proof (rule contour_integral_via_joinpaths[of _ t], goal_cases)
  case 2
  from assms have "f holomorphic_on A" "open A" "path_image p ⊆ A"
    by blast+
  hence "f analytic_on path_image p"
    using analytic_on_holomorphic by blast
  with assms show ?case
    by blast
qed fact+


fun unions_list :: "('a ⇒ 'b set) ⇒ 'a list ⇒ 'b set" where
  "unions_list f [] = {}"
| "unions_list f [x] = f x"
| "unions_list f (x # xs) = f x ∪ unions_list f xs"

lemma unions_list_eq: "unions_list f xs = (⋃x∈set xs. f x)"
  by (induction f xs rule: unions_list.induct) auto

lemma path_image_via_joinpaths [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "wf_joinpaths_tree t ∧ unions_list path_image (flatten_joinpaths_tree t) = T"
  shows   "path_image p = T"
proof -
  have "path_image p = path_image (eval_joinpaths_tree t)"
    using assms by (simp add: REIFY_JOINPATHS_TAG_def)
  also have "… = path_image (joinpaths_list (flatten_joinpaths_tree t))"
    by (intro eq_paths_imp_path_image_eq joinpaths_flatten_joinpaths_tree) (use assms in auto)
  also have "… = (⋃x∈set (flatten_joinpaths_tree t). path_image x)"
    by (subst path_image_joinpaths_list) (use assms in auto)
  also have "… = unions_list path_image (flatten_joinpaths_tree t)"
    by (rule unions_list_eq [symmetric])
  finally show ?thesis
    using assms by auto
qed

lemma path_image_subset_via_joinpaths [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "wf_joinpaths_tree t ∧ list_all (λp. path_image p ⊆ T) (flatten_joinpaths_tree t)"
  shows   "path_image p ⊆ T"
proof -
  have "path_image p = path_image (eval_joinpaths_tree t)"
    using assms by (simp add: REIFY_JOINPATHS_TAG_def)
  also have "… = path_image (joinpaths_list (flatten_joinpaths_tree t))"
    by (intro eq_paths_imp_path_image_eq joinpaths_flatten_joinpaths_tree) (use assms in auto)
  also have "… = (⋃x∈set (flatten_joinpaths_tree t). path_image x)"
    by (subst path_image_joinpaths_list) (use assms in auto)
  finally show ?thesis
    using assms by (auto simp: list.pred_set)
qed

lemma not_in_path_image_via_joinpaths [path_automation_intros]:
  assumes "REIFY_JOINPATHS_TAG p = eval_joinpaths_tree t"
  assumes "wf_joinpaths_tree t ∧ list_all (λp. x ∉ path_image p) (flatten_joinpaths_tree t)"
  shows   "x ∉ path_image p"
  using path_image_subset_via_joinpaths[of p t "-{x}"] assms by auto

lemma list_all_singleton_iff: "list_all P [x] ⟷ P x"
  by auto
  
lemmas [path_automation_simps] =
  flatten_joinpaths_tree.simps simple_joinpaths_list.simps weak_wf_joinpaths_tree.simps
  append.simps list.sel last.simps butlast.simps list.simps if_False if_True refl
  arc_joinpaths_list_aux.simps arc_joinpaths_list_def ball_simps HOL.simp_thms
  start_joinpaths_tree.simps finish_joinpaths_tree.simps wf_joinpaths_tree.simps
  valid_path_joinpaths_tree.simps sublist_code prefix_code is_rotation_of_code
  is_rotation_of_aux.simps list.size add_Suc_right plus_nat.add_Suc add_0_right add_0_left
  pathstart_linepath pathfinish_linepath pathstart_part_circlepath' pathfinish_part_circlepath'
  pathstart_circlepath pathfinish_circlepath pathstart_rectpath pathfinish_rectpath
  path_linepath path_part_circlepath path_circlepath path_rectpath
  valid_path_linepath valid_path_part_circlepath valid_path_circlepath valid_path_rectpath
  simple_path_part_circlepath simple_path_circlepath sum_list_Cons_rev sum_list_singleton list.map
  valid_path_pathlist.simps rev.simps reversepath_linepath reversepath_part_circlepath
  reversepath_circlepath unions_list.simps path_image_linepath path_image_circlepath
  list.pred_inject(1) list_all_singleton_iff list.pred_inject(2)[of P x "y # xs" for P x y xs]

lemma arc_linepath_iff [path_automation_simps]: "arc (linepath a b) ⟷ a ≠ b"
proof
  assume "arc (linepath a b)"
  thus "a ≠ b"
    by (smt (verit, best) arcD atLeastAtMost_iff linepath_0' linepath_1')
qed auto

lemma simple_path_linepath_iff [path_automation_simps]: "simple_path (linepath a b) ⟷ a ≠ b"
proof
  assume "simple_path (linepath a b)"
  thus "a ≠ b"
    by (metis linepath_1' simple_path_subpath_eq subpath_refl)
qed auto

lemma arc_part_circlepath_iff [path_automation_simps]:
  "arc (part_circlepath x r a b) ⟷ r ≠ 0 ∧ a ≠ b ∧ ¦a - b¦ < 2 * pi"
proof (intro iffI conjI)
  assume *: "arc (part_circlepath x r a b)"
  show "r ≠ 0"
    using * by (auto simp: arc_linepath_iff)
  show "a ≠ b"
    using * by (auto simp: part_circlepath_empty arc_linepath_iff)
  show "¦a - b¦ < 2 * pi"
  proof (rule ccontr)
    assume **: "¬¦a - b¦ < 2 * pi"
    hence "a ≠ b"
      by auto
    have "part_circlepath x r a b (2 * pi / ¦a - b¦) = 
            x + rcis r ((1 - 2 * pi / ¦a - b¦) * a + 2 * pi * b / ¦a - b¦)"
      by (simp add: part_circlepath_altdef linepath_def)
    also have "(1 - 2 * pi / ¦a - b¦) * a + 2 * pi * b / ¦a - b¦ = a + sgn (b - a) * 2 * pi"
      using ** ‹a ≠ b› by (auto simp: divide_simps) (auto simp: field_simps abs_if split: if_splits)?
    also have "x + rcis r (a + sgn (b - a) * 2 * pi) = part_circlepath x r a b 0"
      by (simp add: part_circlepath_altdef linepath_def rcis_def sgn_if flip: cis_mult cis_cnj)
    finally have "part_circlepath x r a b (2 * pi / ¦a - b¦) = part_circlepath x r a b 0" .
    moreover have "0 ∈ {0..(1::real)}" 
      by simp
    moreover have "2 * pi / ¦a - b¦ ∈ {0..1}"
      using ** ‹a ≠ b› by (auto simp: field_simps)
    ultimately show False
      using arcD[OF *, of 0 "2 * pi / ¦a - b¦"] ‹a ≠ b› by fastforce
  qed
qed (auto intro!: arc_part_circlepath)

lemma arc_circlepath_iff [path_automation_simps]: "arc (circlepath x r) ⟷ False"
  unfolding circlepath_def arc_part_circlepath_iff by auto



named_theorems path_automation_unfolds

ML ‹
signature PATH_REIFY = sig
  val do_path_reify_tac : Proof.context -> int -> tactic
  val path_reify_tac : Proof.context -> int -> tactic
  val tac : Proof.context -> int -> tactic
end


structure Path_Reify : PATH_REIFY = struct

val intros = \<^named_theorems>‹path_automation_intros›
val simps = \<^named_theorems>‹path_automation_simps›
val reifies = \<^named_theorems>‹reify_joinpath_tree›
val unfolds = \<^named_theorems>‹path_automation_unfolds›

fun do_path_reify_tac ctxt i =
  let 
    val thms = Named_Theorems.get ctxt reifies
  in
    REPEAT (EqSubst.eqsubst_tac ctxt [0] thms i) THEN resolve_tac ctxt @{thms HOL.refl} i
  end

local

fun tac {context = ctxt, concl, ...} =
    case Thm.term_of concl of
      \<^const>‹Trueprop› $ (Const (\<^const_name>‹HOL.eq›, _) $ 
         (Const (\<^const_name>‹REIFY_JOINPATHS_TAG›, _) $ _) $ _) =>
        HEADGOAL (do_path_reify_tac ctxt)
    | _ => all_tac

in

val path_reify_tac = Subgoal.FOCUS_PARAMS tac

end


local

fun tac' {context = ctxt, ...} = 
  let
    val intros = Named_Theorems.get ctxt intros
    val simps = Named_Theorems.get ctxt simps
    val unfolds = Named_Theorems.get ctxt unfolds
    val ctxt' = put_simpset HOL_basic_ss ctxt addsimps simps
  in
    Local_Defs.unfold_tac ctxt unfolds
    THEN HEADGOAL (
      resolve_tac ctxt intros
      THEN_ALL_NEW DETERM o path_reify_tac ctxt
      THEN_ALL_NEW DETERM o Simplifier.simp_tac ctxt'
      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (DETERM o resolve_tac ctxt @{thms conjI}))
    )
    THEN distinct_subgoals_tac
    THEN Local_Defs.fold_tac ctxt unfolds
  end

val sections =
  Method.sections
    [
     Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add intros) ⌂),
     Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del intros) ⌂),
     Args.$$$ "simp" -- Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add simps) ⌂),
     Args.$$$ "simp" -- Args.colon >> K (Method.modifier (Named_Theorems.add simps) ⌂),
     Args.$$$ "simp" -- Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del simps) ⌂),
     Args.$$$ "defs" -- Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add unfolds) ⌂),
     Args.$$$ "defs" -- Args.colon >> K (Method.modifier (Named_Theorems.add unfolds) ⌂),
     Args.$$$ "defs" -- Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del unfolds) ⌂)
    ]

in

val tac = Subgoal.FOCUS_PARAMS tac'
val method = sections >> K (SIMPLE_METHOD' o tac)

val _ =
  Theory.setup
   (Method.setup \<^binding>‹path_reify› method "reification of composite paths into a path tree" #>
    Method.setup \<^binding>‹path› method
      "automation for various common path problems, e.g. path equivalence, splitting integrals");

end

end
›



subsection  ‹Examples›

text ‹
  We now look at some concrete examples of how the method can be used.
›

experiment
begin


text ‹Showing well-formedness:›
lemma "path (linepath 0 1 +++ linepath 1 (1 + 𝗂) +++ linepath (1 + 𝗂) 0)"
  by path

lemma "valid_path (linepath 0 1 +++ linepath 1 (1 + 𝗂) +++ linepath (1 + 𝗂) 0)"
  by path


text ‹Showing that a path is simple:›
lemma "arc (linepath 0 1 +++ linepath 1 (1 + 𝗂) +++ linepath (1 + 𝗂) 𝗂)"
  apply path
         apply (auto simp: closed_segment_def complex_eq_iff)
  done

lemma "simple_path (linepath 0 1 +++ linepath 1 (1 + 𝗂) +++ linepath (1 + 𝗂) 0)"
  apply path
         apply (auto simp: closed_segment_def complex_eq_iff)
  done


text ‹
  Computing the image of a composite path:
›
lemma "path_image (linepath 0 (1::complex) +++ linepath 1 𝗂) = 
         closed_segment 0 1 ∪ closed_segment 1 𝗂"
  by path


text ‹
  Showing equivalence of paths modulo associativity and reversal:
›
lemma "((linepath 0 1 +++ linepath 1 2) +++ linepath 2 3) +++ linepath 3 4 ≡⇩p
       linepath 0 1 +++ (linepath 1 2 +++ (linepath 2 3 +++ linepath 3 4))"
  by path

lemma "linepath 0 1 +++ reversepath (linepath 3 2 +++ linepath 2 1) +++ linepath 3 4 ≡⇩p
       linepath 0 1 +++ (linepath 1 2 +++ (linepath 2 3 +++ linepath 3 4))"
  by path


text ‹
  Subpath relationships can also be shown in the same fashion.
›
lemma "linepath 1 2 +++ linepath 2 3 ≤⇩p
       linepath 0 1 +++ linepath 1 2 +++ linepath 2 3 +++ linepath 3 4"
  by path

lemma "linepath 0 1 +++ reversepath (linepath 3 2 +++ linepath 2 1) ≤⇩p
       linepath 0 1 +++ (linepath 1 2 +++ (linepath 2 3 +++ linepath 3 4))"
  by path


(*
  TODO: One could be a bit more clever here and solve the "sublist" thing in ML in a more
  controlled way. Similarly for eq_paths, and possibly that would also make eq_loops easier.
*)


text ‹
  For loops, one can, in addition to reversal and associativity, also show equivalence modulo
  ``rotation''. Consider e.g.\ a counter-clockwise rectangular path and consider
  paths to be equal modular associativity. Then there are four different ways to write that path,
  corresponding to which corner we start in.

  The automation can prove automatically that all of these four paths are equivalent to one
  another (basically by brute-forcing all 4 possibilities).
›
lemma "linepath 0 1 +++ linepath 1 (1 + 𝗂) +++ linepath (1 + 𝗂) 𝗂 +++ linepath 𝗂 0 ≡⇩○
       linepath 1 (1 + 𝗂) +++ linepath (1 + 𝗂) 𝗂 +++ linepath 𝗂 0 +++ linepath 0 1"
  by path



(* TODO: support reversal *)

text ‹
  For the next few examples, we define a path consisting of three perpendicular lines.
›
definition g where "g = (linepath 0 1 +++ linepath 1 (1 + 𝗂) +++ linepath (1 + 𝗂) 𝗂)"

text ‹
  Contour integrals on such composite paths can be split into integrals on the constituent paths.
  Since the path is often a large, unwieldy expression that is hidden behind a definition,
  one can give that definition theorem to the \emph{path} method with the \emph{defs} keyword.
  Its definition is then unfolded automatically and re-folded in any of the arising proof 
  obligations that contain the full path again, such as the analyticity condition here.
›
lemma "contour_integral g (λx. x) = -1/2"
proof (path defs: g_def)
  show "contour_integral (linepath 0 1) (λx. x) +
        contour_integral (linepath 1 (1 + 𝗂)) (λx. x) +
        contour_integral (linepath (1 + 𝗂) 𝗂) (λx. x) = - 1 / 2"
    by (simp add: field_simps)
next
  show "(λx. x) analytic_on path_image g"
    by auto
qed


text ‹
  Alternatively, one can also show holomorphicity on some open superset of the path's image
  instead of analyticity on exactly the path's image.
›
lemma "contour_integral g (λx. x) = -1/2"
proof (path defs: g_def del: contour_integral_via_joinpaths add: contour_integral_via_joinpaths_holo)
  show "contour_integral (linepath 0 1) (λx. x) +
        contour_integral (linepath 1 (1 + 𝗂)) (λx. x) +
        contour_integral (linepath (1 + 𝗂) 𝗂) (λx. x) = - 1 / 2"
    by (simp add: field_simps)
next
  show "(λx. x) holomorphic_on UNIV"
    by auto
next
  show "open (UNIV :: complex set)"
    by simp
next
  text ‹
    Conditions such as a path being a subset of some other set can also be simplified using
    the ∗‹path› method:
  ›
  show "path_image g ⊆ UNIV"
    apply (path defs: g_def)
      apply auto
    done
qed


text ‹
  Winding numbers can be split into the winding numbers of the constituent paths in the same way
  as integrals. However, for concrete paths it is probably better to use Wenda Li's automation
  rather than this.
›
lemma "winding_number g (1 / 3 + 1 / 3 * 𝗂) = undefined"
  apply (path defs: g_def)
     apply (simp_all add: closed_segment_same_Re closed_segment_same_Im)
  oops

end

end