theory Drawing_Trees imports Complex_Main begin

section \<open>Algorithm\<close>

datatype 'a tree = Node 'a \<open>'a tree list\<close>

type_synonym extent = \<open>(real * real) list\<close>

fun movetree :: \<open>('a * real) tree * real \<Rightarrow> ('a * real) tree\<close> where
  \<open>movetree ((Node (label, x) subs), x') = Node (label, x + x') subs\<close>

primrec moveextent :: \<open>extent * real \<Rightarrow> extent\<close> where
  \<open>moveextent (e, x) = map (\<lambda> (p, q) \<Rightarrow> (p + x, q + x)) e\<close>

fun merge :: \<open>extent \<Rightarrow> extent \<Rightarrow> extent\<close> where
  \<open>merge [] qs = qs\<close>
| \<open>merge ps [] = ps\<close>
| \<open>merge ((p1, p2) # ps) ((q1, q2) # qs) = (min p1 q1, max p2 q2) # merge ps qs\<close>

primrec mergelist :: \<open>extent list \<Rightarrow> extent\<close> where
  \<open>mergelist [] = []\<close>
| \<open>mergelist (e#es) = merge e (mergelist es)\<close>

fun fit :: \<open>extent \<Rightarrow> extent \<Rightarrow> real\<close> where
  \<open>fit ((p1,p2)#ps) ((q1,q2)#qs) = max (fit ps qs) (max p1 p2 - min q1 q2 + 1)\<close>
| \<open>fit _ _ = 0\<close>

primrec fitlistl' :: \<open>extent \<Rightarrow> extent list \<Rightarrow> real list\<close> where
  \<open>fitlistl' acc [] = []\<close>
| \<open>fitlistl' acc (e#es) = (let x = fit acc e in x # fitlistl' (merge acc (moveextent (e, x))) es)\<close>

definition fitlistl where \<open>fitlistl \<equiv> fitlistl' []\<close>

definition flipextent :: \<open>extent \<Rightarrow> extent\<close> where
  \<open>flipextent = map (\<lambda>(p, q). (-q, -p))\<close>

definition fitlistr :: \<open>extent list \<Rightarrow> real list\<close> where
  \<open>fitlistr = rev o map uminus o fitlistl o map flipextent o rev\<close>

primrec mean where \<open>mean (x, y) = (x + y) / 2\<close>

definition fitlist :: \<open>extent list \<Rightarrow> real list\<close> where
  \<open>fitlist es = map mean (zip (fitlistl es) (fitlistr es))\<close>

fun unzip :: \<open>('a \<times> 'b) list \<Rightarrow> 'a list \<times> 'b list\<close> where
  \<open>unzip [] = ([], [])\<close>
| \<open>unzip ((a, b) # xs) = (case unzip xs of (as, bs) \<Rightarrow> (a # as, b # bs))\<close>

primrec design' :: \<open>'a tree \<Rightarrow> ('a * real) tree * extent\<close> where
  \<open>design' (Node label subtrees) = (
    let (trees, extents) = unzip (map design' subtrees);
        positions = fitlist extents;
        ptrees = map movetree (zip trees positions);
        pextents = map moveextent (zip extents positions);
        resultextent = (0, 0) # mergelist pextents;
        resulttree = Node (label, 0) ptrees
    in (resulttree, resultextent))\<close>

definition design where \<open>design t \<equiv> fst (design' t)\<close>

section \<open>Utility\<close>

lemma unzip [simp]: \<open>unzip xs = (map fst xs, map snd xs)\<close>
  by (induct xs) auto

lemma length_unzip: \<open>(as, bs) = unzip xs \<Longrightarrow> length as = length bs \<and> length as = length xs\<close>
  by simp

lemma zip_unzip [simp]: \<open>(as, bs) = unzip xs \<Longrightarrow> xs = zip as bs\<close>
  by (induct xs arbitrary: as bs) simp_all

lemma fitlistl'_length: \<open>length (fitlistl' xs es) = length es\<close>
proof (induct es arbitrary: xs)
  case (Cons e es)
  then show ?case
    by (metis fitlistl'.simps(2) length_Cons)
qed simp

lemma fitlistl_length: \<open>length (fitlistl es) = length es\<close>
  unfolding fitlistl_def using fitlistl'_length .

lemma fitlistr_length: \<open>length (fitlistr es) = length es\<close>
  unfolding fitlistr_def using fitlistl_length by simp

lemma length_fitlistl_fitlistr: \<open>length (fitlistl es) = length (fitlistr es)\<close>
  using fitlistl_length fitlistr_length by simp

lemma length_fitlist: \<open>length (fitlist es) = length es\<close>
  unfolding fitlist_def using fitlistl_length fitlistr_length by simp

lemma list_induct2' [consumes 0, case_names Cons LNil RNil]:
  \<open>(\<And>x xs y ys. P xs ys \<Longrightarrow> P (x # xs) (y # ys)) \<Longrightarrow>
   (\<And>ys. P [] ys) \<Longrightarrow>
   (\<And>xs. P xs []) \<Longrightarrow> P xs ys\<close>
proof (induct xs arbitrary: ys)
  case (Cons x xs)
  then show ?case proof (induct ys)
    case Nil
    then show ?case
      using list_nonempty_induct by metis
  qed blast
qed

lemma list_induct2_rev [consumes 1, case_names Nil Cons]:
  \<open>length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
   (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs (rev ys) \<Longrightarrow> P (x # xs) (rev (y # ys))) \<Longrightarrow>
  P xs ys\<close>
proof (induct xs arbitrary: ys)
  case (Cons x xs ys)
  then show ?case
    by (cases \<open>rev ys\<close>) simp_all
qed simp

section \<open>Simpler definitions\<close>

fun extent_of_tree :: \<open>('a * real) tree \<Rightarrow> extent\<close> where
  \<open>extent_of_tree (Node (_, offset) subs) =
    (offset, offset) # mergelist (map (\<lambda>t. moveextent (extent_of_tree t, offset)) subs)\<close>

lemma moveextent_merge_distrib:
  \<open>moveextent (merge ps qs, k) = merge (moveextent (ps, k)) (moveextent (qs, k))\<close>
  by (induct ps qs rule: merge.induct) auto

lemma moveextent_mergelist:
  \<open>moveextent (mergelist es, k) = mergelist (map (\<lambda>e. moveextent (e, k)) es)\<close>
  using moveextent_merge_distrib by (induct es) simp_all

lemma moveextent_collapse [simp]:
  \<open>moveextent (moveextent (ps, x), y) = moveextent (ps, x + y)\<close>
  by (induct ps) auto

lemma move_extent_of_tree:
  \<open>moveextent (extent_of_tree t, k) = extent_of_tree (movetree (t, k))\<close>
proof (induct t rule: extent_of_tree.induct)
  case (1 label offset subs)
  then have \<open>moveextent (extent_of_tree (Node (label, offset) subs), k) =
      ((offset + k, offset + k) # mergelist (map ((\<lambda>e. moveextent (e, k)) o
        (\<lambda>t. moveextent (extent_of_tree t, offset))) subs))\<close>
    using moveextent_mergelist by simp
  also have \<open>\<dots> = ((offset + k, offset + k) #
      mergelist (map (\<lambda>t. moveextent (extent_of_tree t, offset + k)) subs))\<close>
    using moveextent_collapse unfolding comp_def by metis
  finally show ?case
    by simp
qed

lemma move_extent_of_trees:
  \<open>map (extent_of_tree o movetree) (zip ts as) =
   map moveextent (zip (map extent_of_tree ts) as)\<close>
proof (induct ts as rule: list_induct2')
  case Cons
  then show ?case
    unfolding comp_def using move_extent_of_tree
    by (metis (no_types, lifting) list.simps(9) zip_Cons_Cons)
qed simp_all

lemma design'_extent_of_tree:
  \<open>(tree, extent) = design' t \<Longrightarrow> extent_of_tree tree = extent\<close>
proof (induct t arbitrary: tree extent)
  case (Node v subs)
  define trees where \<open>trees \<equiv> fst (unzip (map design' subs))\<close>
  define extents where \<open>extents \<equiv> snd (unzip (map design' subs))\<close>
  define positions where \<open>positions \<equiv> fitlist extents\<close>
  have \<open>map extent_of_tree trees = extents\<close>
    unfolding trees_def extents_def using Node by fastforce
  moreover have \<open>?case = (extent_of_tree (Node (v, 0) (map movetree (zip trees positions))) =
      (0, 0) # mergelist (map moveextent (zip extents positions)))\<close>
    unfolding trees_def extents_def positions_def using Node
    by (metis (no_types, lifting) Pair_inject design'.simps split_beta)
  ultimately show ?case
    by (simp add: move_extent_of_trees)
qed

primrec raw_design :: \<open>'a tree \<Rightarrow> ('a * real) tree\<close> where
  \<open>raw_design (Node label subtrees) = (
    let trees = map raw_design subtrees;
        extents = map extent_of_tree trees;
        positions = fitlist extents;
        ptrees = map movetree (zip trees positions)
    in Node (label, 0) ptrees)\<close>

lemma design'_raw_design':
  \<open>let (tree, extent) = design' t in tree = raw_design t \<and> extent = extent_of_tree tree\<close>
proof (induct t)
  case (Node v subs)
  define trees where \<open>trees \<equiv> fst (unzip (map design' subs))\<close>
  define extents where \<open>extents \<equiv> snd (unzip (map design' subs))\<close>

  define trees' where \<open>trees' \<equiv> map raw_design subs\<close>
  define extents' where \<open>extents' \<equiv> map extent_of_tree trees'\<close>

  have \<open>trees = trees'\<close>
    unfolding trees_def trees'_def using Node
    by (induct subs) fastforce+

  have \<open>extents = map extent_of_tree trees\<close>
    unfolding trees_def extents_def using Node by fastforce
  then have \<open>extents = extents'\<close>
    unfolding extents'_def using \<open>trees = trees'\<close> by blast

  have \<open>extent_of_tree (fst (design' (Node v subs))) = snd (design' (Node v subs))\<close>
    using design'_extent_of_tree prod.collapse by blast
  moreover have \<open>zip trees' (fitlist extents') =
      zip (map raw_design subs) (fitlist (map extent_of_tree (map raw_design subs)))\<close>
    unfolding extents'_def trees'_def by simp
  ultimately show ?case
    using \<open>extents = extents'\<close> \<open>trees = trees'\<close> unfolding extents_def trees_def by simp
qed

theorem design'_raw_design:
  \<open>design' t = (raw_design t, extent_of_tree (raw_design t))\<close>
  using design'_raw_design' by fastforce

theorem design_raw_design: \<open>design t = raw_design t\<close>
  unfolding design_def by (simp add: design'_raw_design)

section \<open>Property 0 -- Structure preservation\<close>

fun strip_offsets :: \<open>('a \<times> real) tree \<Rightarrow> 'a tree\<close> where
  \<open>strip_offsets (Node (label, offset) subs) = Node label (map strip_offsets subs)\<close>

lemma strip_offsets_movetree [simp]: \<open>strip_offsets (movetree (t, x)) = strip_offsets t\<close>
  by (induct t rule: strip_offsets.induct) simp_all

lemma strip_offsets_movetrees:
  \<open>length subs' = length xs \<Longrightarrow>
   Node v subs = strip_offsets (Node (v, x) subs') \<Longrightarrow>
   Node v subs = strip_offsets (Node (v, x) (map movetree (zip subs' xs)))\<close>
  by (induct subs' xs arbitrary: subs rule: list_induct2) simp_all

lemma map_fst_unzip:
  assumes \<open>\<forall>x \<in> set xs. f (fst (g x)) = x\<close>
  shows \<open>map f (fst (unzip (map g xs))) = xs\<close>
  using assms by (induct xs) simp_all

lemma strip_offsets_design': \<open>(t', extent) = design' t \<Longrightarrow> t = strip_offsets t'\<close>
proof (induct t arbitrary: t' extent)
  case (Node v subs)
  define subs' where \<open>subs' \<equiv> fst (unzip (map design' subs))\<close>
  define exts where \<open>exts \<equiv> snd (unzip (map design' subs))\<close>
  have \<open>sub \<in> set subs \<Longrightarrow> strip_offsets (fst (design' sub)) = sub\<close> for sub
    using Node by (metis prod.collapse)
  then have \<open>map strip_offsets subs' = subs\<close>
    unfolding subs'_def exts_def using map_fst_unzip by metis
  then have \<open>map strip_offsets (map movetree (zip subs' (fitlist exts))) = subs\<close>
    unfolding subs'_def exts_def using length_fitlist length_unzip strip_offsets_movetrees
    by (metis (no_types, lifting) prod.collapse strip_offsets.simps tree.inject)
  then show ?case
    unfolding subs'_def exts_def using Node(2)
    by (metis (no_types, lifting) design'.simps fst_conv prod.case_eq_if strip_offsets.simps)
qed

theorem strip_offsets_design: \<open>strip_offsets (design t) = t\<close>
  unfolding design_def using strip_offsets_design' by (metis prod.collapse)

theorem design_inj: \<open>t = t' \<longleftrightarrow> design t = design t'\<close>
  using strip_offsets_design by metis

section \<open>Property 1 -- Properly spaced nodes\<close>

subsection \<open>Spaced, fit and merging\<close>

lemma fit_cons_ge: \<open>fit (p # ps) (q # qs) \<ge> fit ps qs\<close>
  by (cases p; cases q) simp_all

fun spaced :: \<open>extent \<Rightarrow> extent \<Rightarrow> bool\<close> where
  \<open>spaced ((p1, p2) # ps) ((q1, q2) # qs) = (q1 - p2 \<ge> 1 \<and> spaced ps qs)\<close>
| \<open>spaced _ _ = True\<close>

lemma spaced_ge:
  \<open>spaced ps (moveextent (qs, k)) \<Longrightarrow> k \<le> k' \<Longrightarrow> spaced ps (moveextent (qs, k'))\<close>
  by (induct ps qs rule: spaced.induct) simp_all

lemma spaced_fit [simp]: \<open>spaced ps (moveextent (qs, fit ps qs))\<close>
  using spaced_ge by (induct ps qs rule: fit.induct) fastforce+

fun within_extent :: \<open>extent \<Rightarrow> extent \<Rightarrow> bool\<close> where
  \<open>within_extent ((p1, p2) # ps) ((q1, q2) # qs) = (q1 \<le> p1 \<and> p2 \<le> q2 \<and> within_extent ps qs)\<close>
| \<open>within_extent [] _ = True\<close>
| \<open>within_extent _ _ = False\<close>

lemma within_self: \<open>within_extent ps ps\<close>
  by (induct ps) auto

lemma within_merge_left: \<open>within_extent ps (merge ps qs)\<close>
  using within_self by (induct ps qs rule: merge.induct) simp_all

lemma within_merge_right: \<open>within_extent qs (merge ps qs)\<close>
  using within_self by (induct ps qs rule: merge.induct) simp_all

fun extent3 :: \<open>extent \<Rightarrow> extent \<Rightarrow> extent \<Rightarrow> unit\<close> where
  \<open>extent3 ((_, _) # xs) ((_, _) # ys) ((_, _) # zs) = extent3 xs ys zs\<close>
| \<open>extent3 _ _ _ = ()\<close>

lemma within_nil: \<open>within_extent ps [] \<Longrightarrow> ps = []\<close>
  by (induct ps) simp_all

lemma within_trans: \<open>within_extent ps qs \<Longrightarrow> within_extent qs rs \<Longrightarrow> within_extent ps rs\<close>
  using within_nil by (induct ps qs rs rule: extent3.induct) fastforce+

lemma spaced_within_left:
  \<open>spaced xs qs \<Longrightarrow> within_extent ps xs \<Longrightarrow> spaced ps qs\<close>
  using within_nil by (induct ps qs xs rule: extent3.induct) fastforce+

lemma spaced_within_right:
  \<open>spaced ps xs \<Longrightarrow> within_extent qs xs \<Longrightarrow> spaced ps qs\<close>
  using within_nil by (induct ps qs xs rule: extent3.induct) fastforce+

lemma spaced_left_merge_left: \<open>spaced (merge ps qs) rs \<Longrightarrow> spaced ps rs\<close>
  using spaced_within_left within_merge_left by blast

lemma spaced_left_merge_right: \<open>spaced (merge ps qs) rs \<Longrightarrow> spaced qs rs\<close>
  using spaced_within_left within_merge_right by blast

lemma spaced_merge_left_left:
  \<open>spaced ps qs \<Longrightarrow> spaced ps (moveextent (rs, fit (merge ps qs) rs))\<close>
  using spaced_fit spaced_left_merge_left by blast

lemma spaced_fit_within:
  \<open>within_extent ps xs \<Longrightarrow> spaced ps (moveextent (qs, fit xs qs))\<close>
  using spaced_fit spaced_within_left by blast

lemma within_extent_merge_right_left: \<open>within_extent y (merge (merge x y) z)\<close>
  using within_merge_left within_merge_right within_trans by blast

subsection \<open>Proper spacing by fitlistl\<close>

lemma fitlistl'_spaced_within:
  \<open>within_extent ps xs \<Longrightarrow> list_all (spaced ps) (map moveextent (zip es (fitlistl' xs es)))\<close>
proof (induct es arbitrary: xs)
  case (Cons e es)
  then have \<open>list_all (spaced ps) (moveextent (e, fit xs e) #
        map moveextent (zip es (fitlistl' (merge xs (moveextent (e, fit xs e))) es)))\<close>
    using spaced_fit spaced_within_left within_merge_left within_trans
    by (metis (no_types) list.pred_inject(2))
  then show ?case
    by (metis fitlistl'.simps(2) list.simps(9) zip_Cons_Cons)
qed simp

lemma fitlistl'_spaced_merge:
  \<open>list_all (spaced ps) (map moveextent (zip es (fitlistl' (merge xs ps) es)))\<close>
  using fitlistl'_spaced_within within_merge_right by blast

primrec all_pairs :: \<open>('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool\<close> where
  \<open>all_pairs _ [] = True\<close>
| \<open>all_pairs p (e # es) = (list_all (p e) es \<and> all_pairs p es)\<close>

definition all_spaced :: \<open>extent list \<Rightarrow> bool\<close> where
  \<open>all_spaced = all_pairs spaced\<close>

lemma all_pairs_drop_last: \<open>all_pairs p (es @ [e']) \<Longrightarrow> all_pairs p es\<close>
  by (induct es) simp_all

lemma all_pairs_last: \<open>all_pairs p (es @ [e]) \<Longrightarrow> list_all (\<lambda>e'. p e' e) es\<close>
  by (induct es) simp_all

lemma all_spaced_fitlistl':
  \<open>all_spaced (map moveextent (zip es (fitlistl' xs es)))\<close>
  unfolding all_spaced_def
proof (induct es arbitrary: xs)
  case (Cons e es)
  then have \<open>all_pairs spaced (moveextent (e, fit xs e) #
      map moveextent (zip es (fitlistl' (merge xs (moveextent (e, fit xs e))) es)))\<close>
    using fitlistl'_spaced_merge by simp
  then show ?case
    by (metis (no_types) fitlistl'.simps(2) list.simps(9) zip_Cons_Cons)
qed simp

lemma all_spaced_fitlistl: \<open>all_spaced (map moveextent (zip es (fitlistl es)))\<close>
  unfolding fitlistl_def using all_spaced_fitlistl' .

subsection \<open>Flipping extents\<close>

lemma spaced_move_flip:
  \<open>spaced (moveextent (flipextent qs, y)) (moveextent (flipextent ps, x)) =
   spaced (moveextent (ps, -x)) (moveextent (qs, -y))\<close>
  unfolding flipextent_def by (induct ps qs rule: spaced.induct) auto

subsection \<open>Geometric digression\<close>

lemma spaced_flip: \<open>spaced (flipextent qs) (flipextent ps) = spaced ps qs\<close>
  unfolding flipextent_def by (induct ps qs rule: spaced.induct) simp_all

lemma all_pairs_map_rev:
  \<open>all_pairs p (map f (rev es)) \<Longrightarrow> (\<forall>e e'. p (f e') (f e) \<longrightarrow> p e e') \<Longrightarrow> all_pairs p es\<close>
proof (induct es)
  case (Cons e es)
  then have *: \<open>all_pairs p (map f (rev es @ [e]))\<close>
    by (metis rev.simps(2))
  then have \<open>all_pairs p (map f (rev es))\<close>
    using all_pairs_drop_last by fastforce
  then have \<open>all_pairs p es\<close>
    using Cons by blast
  moreover have \<open>list_all (\<lambda>e'. p e' (f e)) (map f (rev es))\<close>
    using * all_pairs_last by simp
  then have \<open>list_all (\<lambda>e'. p (f e') (f e)) (rev es)\<close>
    unfolding list_all_def by simp
  then have \<open>list_all (\<lambda>e'. p (f e') (f e)) es\<close>
    by simp
  then have \<open>list_all (p e) es\<close>
    using Cons list_all_iff by metis
  ultimately show ?case
    by simp
qed simp

lemma all_spaced_flip: \<open>all_spaced (map flipextent (rev es)) \<Longrightarrow> all_spaced es\<close>
  unfolding all_spaced_def using all_pairs_map_rev spaced_flip by blast

subsection \<open>Properly spaced fitlistr\<close>

lemma spaced_flip_cons: \<open>length es = length xs \<Longrightarrow>
  list_all (\<lambda>e'. spaced e' (moveextent (flipextent a, k)))
    (map moveextent (zip (map flipextent (rev es)) (rev xs))) \<Longrightarrow>
  list_all (spaced (moveextent (a, -k))) (map moveextent (zip es (map uminus xs)))\<close>
proof (induct es xs rule: list_induct2)
  case (Cons x xs y ys)
  then show ?case
    using spaced_move_flip by simp
qed simp

lemma all_spaced_fitlistr': \<open>length es = length xs \<Longrightarrow>
  all_spaced (map moveextent (zip (map flipextent (rev es)) xs)) \<Longrightarrow>
  all_spaced (map moveextent (zip es (rev (map uminus xs))))\<close>
proof (induct es xs rule: list_induct2_rev)
  case Nil
  then show ?case
    by simp
next
  case (Cons e es x xs)
  then have *: \<open>all_spaced (map moveextent (zip (map flipextent (rev es)) (rev xs) @
      [(flipextent e, x)]))\<close>
    by simp
  then have \<open>all_spaced (map moveextent (zip (map flipextent (rev es)) (rev xs)))\<close>
    unfolding all_spaced_def using all_pairs_drop_last by fastforce
  then have \<open>all_spaced (map moveextent (zip es (rev (map uminus (rev xs)))))\<close>
    using Cons by blast
  then have \<open>all_spaced (map moveextent (zip es (map uminus xs)))\<close>
    by (simp add: rev_map)
  moreover have \<open>all_spaced (map moveextent (zip (map flipextent (rev es)) (rev xs)) @
      [moveextent (flipextent e,x)])\<close>
    using * by simp
  then have \<open>list_all (\<lambda>e'. spaced e' (moveextent (flipextent e, x)))
      (map moveextent (zip (map flipextent (rev es)) (rev xs)))\<close>
    unfolding all_spaced_def using all_pairs_last by fast
  then have \<open>list_all (spaced (moveextent (e, -x))) (map moveextent (zip es (map uminus xs)))\<close>
    using Cons spaced_flip_cons by blast
  ultimately show ?case
    unfolding all_spaced_def by (simp add: rev_map)
qed

lemma all_spaced_fitlistr:
  \<open>all_spaced (map moveextent (zip es (fitlistr es)))\<close>
  unfolding fitlistr_def comp_def using all_spaced_fitlistl all_spaced_fitlistr' fitlistl_length
  by (metis length_map length_rev)

subsection \<open>Properly spaced fitlist\<close>

lemma spaced_mean:
  \<open>spaced (moveextent (ps, x)) (moveextent (qs, y)) \<Longrightarrow>
   spaced (moveextent (ps, a)) (moveextent (qs, b)) \<Longrightarrow>
   spaced (moveextent (ps, mean (x, a))) (moveextent (qs, mean (y, b)))\<close>
  by (induct ps qs rule: spaced.induct) (simp_all add: add_divide_distrib)

fun all_spaced_induct :: \<open>extent list \<Rightarrow> real list \<Rightarrow> real list \<Rightarrow> unit\<close> where
  \<open>all_spaced_induct (e # es) (a # as) (b # bs) = all_spaced_induct es as bs\<close>
| \<open>all_spaced_induct _ _ _ = ()\<close>

lemma all_spaced_mean_cons:
  \<open>list_all (spaced (moveextent (p, a))) (map moveextent (zip es as)) \<Longrightarrow>
   list_all (spaced (moveextent (p, b))) (map moveextent (zip es bs)) \<Longrightarrow>
   list_all (spaced (moveextent (p, mean (a, b)))) (map moveextent (zip es (map mean (zip as bs))))\<close>
  using spaced_mean by (induct es as bs rule: all_spaced_induct.induct) simp_all

lemma all_spaced_mean:
  \<open>all_spaced (map moveextent (zip es as)) \<Longrightarrow>
   all_spaced (map moveextent (zip es bs)) \<Longrightarrow>
   all_spaced (map moveextent (zip es (map mean (zip as bs))))\<close>
proof (induct es as bs rule: all_spaced_induct.induct)
  case (1 e es a as b bs)
  then have \<open>list_all (spaced (moveextent (e, a))) (map moveextent (zip es as))\<close>
    unfolding all_spaced_def by simp
  moreover have \<open>list_all (spaced (moveextent (e, b))) (map moveextent (zip es bs))\<close>
    using 1 unfolding all_spaced_def by simp
  moreover have \<open>list_all (spaced (moveextent (e, mean(a, b))))
      (map moveextent (zip es (map mean (zip as bs))))\<close>
    using all_spaced_mean_cons calculation by blast
  ultimately show ?case
    using 1 unfolding all_spaced_def by simp
qed simp_all

lemma all_spaced_fitlist: \<open>all_spaced (map moveextent (zip es (fitlist es)))\<close>
  unfolding fitlist_def using all_spaced_mean all_spaced_fitlistl all_spaced_fitlistr by fast

subsection \<open>Properly spaced tree\<close>

fun get_offset :: \<open>('a * real) tree \<Rightarrow> real\<close> where
  \<open>get_offset (Node (_, x) _) = x\<close>

definition spaced_offset :: \<open>real \<Rightarrow> real \<Rightarrow> bool\<close> where
  \<open>spaced_offset x y = (x + 1 \<le> y)\<close>

primrec spaced_tree :: \<open>('a * real) tree \<Rightarrow> bool\<close> where
  \<open>spaced_tree (Node _ subs) =
    (all_pairs spaced_offset (map get_offset subs) \<and> list_all spaced_tree subs)\<close>

lemma spaced_extents_offsets:
  assumes \<open>spaced (extent_of_tree s) (extent_of_tree t)\<close>
  shows \<open>spaced_offset (get_offset s) (get_offset t)\<close>
  unfolding spaced_offset_def using assms
  by (cases s rule: get_offset.cases, cases t rule: get_offset.cases) simp_all

lemma all_spaced_tree:
  \<open>all_spaced (map extent_of_tree subs) \<Longrightarrow>
   list_all spaced_tree subs \<Longrightarrow>
   spaced_tree (Node (a, 0) subs)\<close>
proof (induct subs)
  case (Cons sub subs)
  then have \<open>spaced_tree (Node (a, 0) subs)\<close>
    unfolding all_spaced_def by simp
  moreover have \<open>all_spaced (map extent_of_tree (sub # subs))\<close>
    using Cons by simp
  then have \<open>list_all (\<lambda>sub'. spaced (extent_of_tree sub) (extent_of_tree sub')) subs\<close>
    unfolding all_spaced_def by (simp add: list_all_iff)
  then have \<open>list_all (\<lambda>sub'. spaced_offset (get_offset sub) (get_offset sub')) subs\<close>
    using spaced_extents_offsets by (metis (no_types) list_all_iff)
  then have \<open>list_all (spaced_offset (get_offset sub)) (map get_offset subs)\<close>
    by (simp add: list_all_iff)
  ultimately show ?case
    using Cons by simp
qed simp

lemma merge_nil [simp]: \<open>merge ps [] = ps\<close>
  by (induct ps) simp_all

lemma merge_comm: \<open>merge ps qs = merge qs ps\<close>
  by (induct ps qs rule: merge.induct) auto

lemma move_spaced_tree: \<open>spaced_tree t \<Longrightarrow> spaced_tree (movetree (t, k))\<close>
  by (induct t) auto

lemma move_spaced_trees:
  \<open>list_all spaced_tree ts \<Longrightarrow> list_all spaced_tree (map movetree (zip ts as))\<close>
  by (induct ts as rule: list_induct2') (simp_all add: move_spaced_tree)

lemma all_spaced_extent_of_fitted_tree:
  \<open>all_spaced (map moveextent (zip (map extent_of_tree ts) as)) \<Longrightarrow>
   list_all spaced_tree (map movetree (zip ts as)) \<Longrightarrow>
   all_spaced (map extent_of_tree (map movetree (zip ts as)))\<close>
proof (induct ts as rule: list_induct2')
  case Cons
  then show ?case
    using all_spaced_fitlist move_extent_of_trees map_map by metis
qed simp_all

lemma list_all_unzip:
  \<open>list_all (\<lambda>(a, b). f a = g b) xs \<Longrightarrow> (as, bs) = unzip xs \<Longrightarrow> map f as = map g bs\<close>
  by (induct xs arbitrary: as bs rule: unzip.induct) simp_all

lemma spaced_raw_design: \<open>spaced_tree (raw_design t)\<close>
proof (induct t)
  case (Node v subs)
  define trees where \<open>trees \<equiv> map raw_design subs\<close>
  define extents where \<open>extents \<equiv> map extent_of_tree trees\<close>
  define positions where \<open>positions \<equiv> fitlist extents\<close>

  have \<open>list_all spaced_tree trees\<close>
    unfolding trees_def using Node by (induct subs) simp_all
  then have \<open>list_all spaced_tree (map movetree (zip trees positions))\<close>
    using move_spaced_trees by blast
  moreover from this have \<open>all_spaced (map extent_of_tree (map movetree (zip trees positions)))\<close>
    unfolding extents_def positions_def
    using Node all_spaced_fitlist all_spaced_extent_of_fitted_tree by blast
  moreover have \<open>?case = spaced_tree (Node (v, 0) (map movetree (zip trees positions)))\<close>
    unfolding trees_def extents_def positions_def by simp
  ultimately show ?case
    using all_spaced_tree by metis
qed

theorem spaced_design: \<open>spaced_tree (design t)\<close>
  using design_raw_design spaced_raw_design by metis

section \<open>Property 2 -- Centered parent\<close>

primrec listsum :: \<open>real list \<Rightarrow> real\<close> where
  \<open>listsum [] = 0\<close>
| \<open>listsum (x # xs) = x + listsum xs\<close>

definition minlist :: \<open>real list \<Rightarrow> real\<close> where
  \<open>minlist xs \<equiv> Min (set xs)\<close>

definition maxlist :: \<open>real list \<Rightarrow> real\<close> where
  \<open>maxlist xs \<equiv> Max (set xs)\<close>

fun centered :: \<open>('a \<times> real) tree \<Rightarrow> bool\<close> where
  \<open>centered (Node (_, offset) _) = (offset = 0)\<close>

fun centered_parent :: \<open>('a \<times> real) tree \<Rightarrow> bool\<close> where
  \<open>centered_parent (Node _ []) = True\<close>
| \<open>centered_parent (Node (_, offset) subtrees) =
    (offset = 0 \<and> (- get_offset (hd subtrees) = get_offset (last subtrees)))\<close>

lemma min_max_list_bounds: \<open>\<forall>x \<in> set xs. x \<in> {minlist xs .. maxlist xs}\<close>
  unfolding minlist_def maxlist_def by (induct xs) simp_all

lemma fit_nonnegative [simp]: \<open>fit ps qs \<ge> 0\<close>
  by (induct ps qs rule: fit.induct) simp_all

lemma fit_flipextent: \<open>fit ps qs = fit (flipextent qs) (flipextent ps)\<close>
  unfolding flipextent_def by (induct ps qs rule: fit.induct) simp_all

lemma fitlistl'_nonnegative: \<open>list_all (\<lambda>x. x \<ge> 0) (fitlistl' acc es)\<close>
proof (induct es arbitrary: acc)
  case Nil
  then show ?case by simp
next
  case (Cons e es)
  then show ?case
    using fit_nonnegative
    by (metis fitlistl'.simps(2) list_all_simps(1))
qed

lemma fitlistl_nonnegative: \<open>list_all (\<lambda>x. x \<ge> 0) (fitlistl es)\<close>
  unfolding fitlistl_def using fitlistl'_nonnegative by blast

lemma fitlistl_bounded:
  obtains x where \<open>list_all (\<lambda>k. k \<in> {0 .. x}) (fitlistl es)\<close>
proof -
  have \<open>list_all (\<lambda>k. k \<in> {0 .. maxlist (fitlistl es)}) (fitlistl es)\<close>
    using fitlistl_nonnegative min_max_list_bounds list_all_iff
    by (metis (no_types, lifting) atLeastAtMost_iff)
  then show ?thesis
    using that by blast
qed

lemma listsum_append [simp]: \<open>listsum (xs @ ys) = listsum xs + listsum ys\<close>
  by (induct xs arbitrary: ys) simp_all

lemma listsum_rev [simp]: \<open>listsum (rev xs) = listsum xs\<close>
  using listsum_append by (induct xs) simp_all

lemma listsum_uminus: \<open>listsum xs = - listsum (map uminus xs)\<close>
  by (induct xs) simp_all

lemma listsum_mean: \<open>length xs = length ys \<Longrightarrow>
    listsum (map mean (zip xs ys)) = mean (listsum xs, listsum ys)\<close>
  by (induct xs ys rule: list_induct2) simp_all

lemma listsum_opposite: \<open>length xs = length ys \<Longrightarrow> listsum xs = - listsum ys \<Longrightarrow>
    listsum (map mean (zip xs ys)) = 0\<close>
  using listsum_mean by fastforce

lemma get_offset_movetree [simp]: \<open>get_offset (movetree (t, x)) = get_offset t + x\<close>
  by (induct t) auto

lemma minlist_rev: \<open>minlist xs = minlist (rev xs)\<close>
  unfolding minlist_def by simp

lemma maxlist_rev: \<open>maxlist xs = maxlist (rev xs)\<close>
  unfolding maxlist_def by simp

lemma fit_flipextent_right: \<open>fit ps (flipextent qs) = fit qs (flipextent ps)\<close>
  unfolding flipextent_def by (induct ps qs rule: fit.induct) simp_all

lemma fit_flipextent_left: \<open>fit (flipextent ps) qs = fit (flipextent qs) ps\<close>
  unfolding flipextent_def by (induct ps qs rule: fit.induct) simp_all

lemma flipextent_inv [simp]: \<open>flipextent (flipextent ps) = ps\<close>
  unfolding flipextent_def by (induct ps) auto

lemma centered_design':
  assumes \<open>(t', extent) = design' t\<close>
  shows \<open>centered t'\<close>
proof (cases t)
  case (Node v subs)
  then show ?thesis proof (cases \<open>unzip (map design' subs)\<close>)
    case (Pair a b)
    then show ?thesis
      using assms Node by (simp add: Let_def)
  qed
qed

lemma centered_design: \<open>centered (design t)\<close>
  unfolding design_def using centered_design' by (metis prod.collapse)

lemma non_empty_extent_of_tree: \<open>length (extent_of_tree t) > 0\<close>
  by (cases t) auto

lemma length_extent_design':
  assumes \<open>(t', extent) = design' t\<close>
  shows \<open>length extent > 0\<close>
  using assms design'_extent_of_tree non_empty_extent_of_tree by blast

lemma fst_unzip_list_all: \<open>\<forall>x. P (fst (f x)) \<Longrightarrow> list_all P (fst (unzip (map f xs)))\<close>
  by (induct xs) simp_all

lemma snd_unzip_list_all: \<open>\<forall>x. P (snd (f x)) \<Longrightarrow> list_all P (snd (unzip (map f xs)))\<close>
  by (induct xs) simp_all

lemma length_extents_design':
  assumes \<open>(trees', extents) = unzip (map design' trees)\<close>
  shows \<open>list_all (\<lambda>e. length e > 0) extents\<close>
  using assms length_extent_design' snd_unzip_list_all by (metis eq_snd_iff)

lemma get_offset_raw_design: \<open>get_offset (raw_design t) = 0\<close>
  by (cases t) simp

lemma get_offset_design':
  assumes \<open>(t', extent) = design' t\<close>
  shows \<open>get_offset t' = 0\<close>
  using assms get_offset_raw_design design'_raw_design by (metis fstI)

lemma get_offsets_design':
  assumes \<open>(ts, es) = unzip (map design' subs)\<close>
  shows \<open>list_all (\<lambda>t. get_offset t = 0) ts\<close>
  using assms fst_unzip_list_all get_offset_design'
  by (metis (mono_tags, lifting) design'_raw_design fstI)

lemma last_rev: \<open>length xs > 0 \<Longrightarrow> last (rev xs) = hd xs\<close>
  by (induct xs) simp_all

lemma hd_fitlistl: \<open>hd (fitlistl (e # es)) = 0\<close>
  unfolding fitlistl_def by simp

lemma last_fitlistr: \<open>last (fitlistr (e # es)) = 0\<close>
proof -
  have \<open>last (fitlistr (e # es)) =
      last ((rev \<circ> map uminus \<circ> fitlistl \<circ> map flipextent \<circ> rev) (e # es))\<close>
    unfolding fitlistr_def by blast
  also have \<open>\<dots> = hd ((map uminus \<circ> fitlistl \<circ> map flipextent \<circ> rev) (e # es))\<close>
    using fitlistl_length length_map length_rev by (simp add: last_rev)
  also have \<open>\<dots> = - hd ((fitlistl \<circ> map flipextent \<circ> rev) (e # es))\<close>
    unfolding comp_def using length_map length_rev fitlistl_length hd_map
    by (metis length_0_conv list.discI)
  also have \<open>\<dots> = - 0\<close>
    unfolding comp_def using hd_fitlistl
    by (metis list.collapse list.map_disc_iff rev.simps(1) rev_is_rev_conv)
  finally show ?thesis
    by simp
qed

lemma hd_map_zip:
  assumes \<open>length as > 0\<close> \<open>length bs > 0\<close>
  shows \<open>hd (map f (zip as bs)) = f (hd as, hd bs)\<close>
proof (cases \<open>map f (zip as bs)\<close>)
  case Nil
  have \<open>length (map f (zip as bs)) > 0\<close>
    using assms by simp
  then show ?thesis
    using Nil by simp
next
  case (Cons x xs)
  have \<open>zip as bs = zip (hd as # tl as) (hd bs # tl bs)\<close>
    using assms by simp
  then show ?thesis
    using Cons by simp
qed

lemma last_map_zip:
  assumes \<open>length as > 0\<close> \<open>length bs > 0\<close> \<open>length as = length bs\<close>
  shows \<open>last (map f (zip as bs)) = f (last as, last bs)\<close>
proof (cases \<open>map f (zip as bs)\<close>)
  case Nil
  have \<open>length (map f (zip as bs)) > 0\<close>
    using assms by simp
  then show ?thesis
    using Nil by simp
next
  case (Cons x xs)
  have \<open>zip as bs = zip (butlast as @ [last as]) (butlast bs @ [last bs])\<close>
    using assms(1-2) by simp
  then show ?thesis
    using Cons assms(3) by fastforce
qed

lemma last_fitlist:
  assumes \<open>list_all (\<lambda>e. length e > 0) (e # es)\<close>
  shows \<open>last (fitlist (e # es)) = last (fitlistl (e # es)) / 2\<close>
proof -
  have \<open>fitlist (e # es) = map mean (zip (fitlistl (e # es)) (fitlistr (e # es)))\<close>
    unfolding fitlist_def by simp
  also have \<open>last \<dots> = mean (last (fitlistl (e # es)), last (fitlistr (e # es)))\<close>
    using fitlistl_length fitlistr_length by (simp add: last_map_zip)
  also have \<open>\<dots> = mean (last (fitlistl (e # es)), 0)\<close>
    using last_fitlistr by simp
  finally show ?thesis
    by simp
qed

lemma hd_fitlist:
  assumes \<open>list_all (\<lambda>e. length e > 0) (e # es)\<close>
  shows \<open>hd (fitlist (e # es)) = hd (fitlistr (e # es)) / 2\<close>
proof -
  have \<open>fitlist (e # es) = map mean (zip (fitlistl (e # es)) (fitlistr (e # es)))\<close>
    unfolding fitlist_def by simp
  also have \<open>hd \<dots> = mean (hd (fitlistl (e # es)), hd (fitlistr (e # es)))\<close>
    using fitlistl_length fitlistr_length by (simp add: hd_map_zip)
  also have \<open>\<dots> = mean (0, hd (fitlistr (e # es)))\<close>
    using hd_fitlistl by simp
  finally show ?thesis
    by simp
qed

lemma split_list_Cons:
  assumes \<open>length l > 0\<close>
  obtains x xs where \<open>x # xs = l\<close>
  using assms by (metis length_greater_0_conv list.exhaust)

section \<open>Mirror image property\<close>

fun reflect :: \<open>'a tree \<Rightarrow> 'a tree\<close> where
  \<open>reflect (Node v subtrees) = Node v (map reflect (rev subtrees))\<close>

fun reflectpos :: \<open>('a * real) tree \<Rightarrow> ('a * real) tree\<close> where
  \<open>reflectpos (Node (label, offset) subtrees) = Node (label, -offset) (map reflectpos subtrees)\<close>

lemma reflect_inv: \<open>t = reflect (reflect t)\<close>
proof (induct t rule: reflect.induct)
  case (1 v subtrees)
  then show ?case
    by (induct subtrees) simp_all
qed

lemma reflectpos_inv: \<open>t = reflectpos (reflectpos t)\<close>
proof (induct t rule: reflectpos.induct)
  case (1 label offset subtrees)
  then show ?case
    by (induct subtrees) simp_all
qed

lemma reflect_reflectpos: \<open>reflect (reflectpos t) = reflectpos (reflect t)\<close>
proof (induct t rule: reflectpos.induct)
  case (1 label offset subtrees)
  then show ?case by (induct subtrees) simp_all
qed

lemma reflect_movetree: \<open>reflect (movetree (t, k)) = movetree (reflect t, k)\<close>
  by (cases t rule: reflectpos.cases) simp

lemma reflectpos_movetree: \<open>reflectpos (movetree (t, k)) = movetree (reflectpos t, -k)\<close>
  by (cases t rule: reflectpos.cases) simp

lemma map_reflect_movetree:
  assumes \<open>length ts = length xs\<close>
  shows
    \<open>map reflect (map movetree (zip ts xs)) = map movetree (zip (map reflect ts) xs)\<close>
  using assms by (induct ts xs rule: list_induct2) (simp_all add: reflect_movetree)

lemma map_reflectpos_movetree:
  assumes \<open>length ts = length xs\<close>
  shows
    \<open>map reflectpos (map movetree (zip ts xs)) =
   map movetree (zip (map reflectpos ts) (map uminus xs))\<close>
  using assms by (induct ts xs rule: list_induct2) (simp_all add: reflectpos_movetree)

lemma rev_zip:
  assumes \<open>length as = length bs\<close>
  shows \<open>rev (zip as bs) = zip (rev as) (rev bs)\<close>
  using assms by (induct as bs rule: list_induct2) simp_all

section \<open>Property 4 -- Subtree consistency property\<close>

primrec subtrees :: \<open>'a tree \<Rightarrow> ('a tree) set\<close> where
  \<open>subtrees (Node v subs) = {Node v subs} \<union> (\<Union>set (map subtrees subs))\<close>

lemma strip_offsets_design_equal:
  \<open>strip_offsets (design sub) = strip_offsets (design sub') \<Longrightarrow> design sub = design sub'\<close>
  using strip_offsets_design by metis

lemma map_image_subtrees:
  assumes \<open>\<forall>t. image f (subtrees t) = subtrees (f t)\<close>
  shows \<open>map (image f) (map subtrees ts) = map subtrees (map f ts)\<close>
  using assms by (induct ts) simp_all

lemma strip_offsets_subtrees: \<open>image strip_offsets (subtrees t) = subtrees (strip_offsets t)\<close>
  by (induct t rule: strip_offsets.induct) fastforce

lemma map_strip_offsets_movetree:
  assumes \<open>length ts = length xs\<close>
  shows \<open>map strip_offsets (map movetree (zip ts xs)) = map strip_offsets ts\<close>
  using assms by (induct ts xs rule: list_induct2) simp_all

lemma strip_offsets_raw_design: \<open>strip_offsets (raw_design t) = t\<close>
  using design_raw_design strip_offsets_design by metis

section \<open>Counterexample to property 3 as stated in paper\<close>

lemma "\<not>(\<forall>t. design t = reflect (reflectpos (design t)))"
proof -
  let ?t = "Node undefined [Node undefined [Node undefined [Node undefined [], Node undefined []]],
                Node undefined [Node undefined []]]"
  have "\<not> (design ?t = reflect (reflectpos (design ?t)))"
    by normalization
  then show ?thesis
    by blast
qed

value \<open>
let t = Node ''a'' [Node ''b'' [Node ''c'' [Node ''d'' [], Node ''e'' []]],
                Node ''f'' [Node ''g'' []]]
in (design t, reflectpos (design (reflect t)))
\<close>

end