theory Drawing_Trees imports Complex_Main begin section \Algorithm\ datatype 'a tree = Node 'a \'a tree list\ type_synonym extent = \(real * real) list\ fun movetree :: \('a * real) tree * real \ ('a * real) tree\ where \movetree ((Node (label, x) subs), x') = Node (label, x + x') subs\ primrec moveextent :: \extent * real \ extent\ where \moveextent (e, x) = map (\ (p, q) \ (p + x, q + x)) e\ fun merge :: \extent \ extent \ extent\ where \merge [] qs = qs\ | \merge ps [] = ps\ | \merge ((p1, p2) # ps) ((q1, q2) # qs) = (min p1 q1, max p2 q2) # merge ps qs\ primrec mergelist :: \extent list \ extent\ where \mergelist [] = []\ | \mergelist (e#es) = merge e (mergelist es)\ fun fit :: \extent \ extent \ real\ where \fit ((p1,p2)#ps) ((q1,q2)#qs) = max (fit ps qs) (max p1 p2 - min q1 q2 + 1)\ | \fit _ _ = 0\ primrec fitlistl' :: \extent \ extent list \ real list\ where \fitlistl' acc [] = []\ | \fitlistl' acc (e#es) = (let x = fit acc e in x # fitlistl' (merge acc (moveextent (e, x))) es)\ definition fitlistl where \fitlistl \ fitlistl' []\ definition flipextent :: \extent \ extent\ where \flipextent = map (\(p, q). (-q, -p))\ definition fitlistr :: \extent list \ real list\ where \fitlistr = rev o map uminus o fitlistl o map flipextent o rev\ primrec mean where \mean (x, y) = (x + y) / 2\ definition fitlist :: \extent list \ real list\ where \fitlist es = map mean (zip (fitlistl es) (fitlistr es))\ fun unzip :: \('a \ 'b) list \ 'a list \ 'b list\ where \unzip [] = ([], [])\ | \unzip ((a, b) # xs) = (case unzip xs of (as, bs) \ (a # as, b # bs))\ primrec design' :: \'a tree \ ('a * real) tree * extent\ where \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))\ definition design where \design t \ fst (design' t)\ section \Utility\ lemma unzip [simp]: \unzip xs = (map fst xs, map snd xs)\ by (induct xs) auto lemma length_unzip: \(as, bs) = unzip xs \ length as = length bs \ length as = length xs\ by simp lemma zip_unzip [simp]: \(as, bs) = unzip xs \ xs = zip as bs\ by (induct xs arbitrary: as bs) simp_all lemma fitlistl'_length: \length (fitlistl' xs es) = length es\ proof (induct es arbitrary: xs) case (Cons e es) then show ?case by (metis fitlistl'.simps(2) length_Cons) qed simp lemma fitlistl_length: \length (fitlistl es) = length es\ unfolding fitlistl_def using fitlistl'_length . lemma fitlistr_length: \length (fitlistr es) = length es\ unfolding fitlistr_def using fitlistl_length by simp lemma length_fitlistl_fitlistr: \length (fitlistl es) = length (fitlistr es)\ using fitlistl_length fitlistr_length by simp lemma length_fitlist: \length (fitlist es) = length es\ unfolding fitlist_def using fitlistl_length fitlistr_length by simp lemma list_induct2' [consumes 0, case_names Cons LNil RNil]: \(\x xs y ys. P xs ys \ P (x # xs) (y # ys)) \ (\ys. P [] ys) \ (\xs. P xs []) \ P xs ys\ 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]: \length xs = length ys \ P [] [] \ (\x xs y ys. length xs = length ys \ P xs (rev ys) \ P (x # xs) (rev (y # ys))) \ P xs ys\ proof (induct xs arbitrary: ys) case (Cons x xs ys) then show ?case by (cases \rev ys\) simp_all qed simp section \Simpler definitions\ fun extent_of_tree :: \('a * real) tree \ extent\ where \extent_of_tree (Node (_, offset) subs) = (offset, offset) # mergelist (map (\t. moveextent (extent_of_tree t, offset)) subs)\ lemma moveextent_merge_distrib: \moveextent (merge ps qs, k) = merge (moveextent (ps, k)) (moveextent (qs, k))\ by (induct ps qs rule: merge.induct) auto lemma moveextent_mergelist: \moveextent (mergelist es, k) = mergelist (map (\e. moveextent (e, k)) es)\ using moveextent_merge_distrib by (induct es) simp_all lemma moveextent_collapse [simp]: \moveextent (moveextent (ps, x), y) = moveextent (ps, x + y)\ by (induct ps) auto lemma move_extent_of_tree: \moveextent (extent_of_tree t, k) = extent_of_tree (movetree (t, k))\ proof (induct t rule: extent_of_tree.induct) case (1 label offset subs) then have \moveextent (extent_of_tree (Node (label, offset) subs), k) = ((offset + k, offset + k) # mergelist (map ((\e. moveextent (e, k)) o (\t. moveextent (extent_of_tree t, offset))) subs))\ using moveextent_mergelist by simp also have \\ = ((offset + k, offset + k) # mergelist (map (\t. moveextent (extent_of_tree t, offset + k)) subs))\ using moveextent_collapse unfolding comp_def by metis finally show ?case by simp qed lemma move_extent_of_trees: \map (extent_of_tree o movetree) (zip ts as) = map moveextent (zip (map extent_of_tree ts) as)\ 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: \(tree, extent) = design' t \ extent_of_tree tree = extent\ proof (induct t arbitrary: tree extent) case (Node v subs) define trees where \trees \ fst (unzip (map design' subs))\ define extents where \extents \ snd (unzip (map design' subs))\ define positions where \positions \ fitlist extents\ have \map extent_of_tree trees = extents\ unfolding trees_def extents_def using Node by fastforce moreover have \?case = (extent_of_tree (Node (v, 0) (map movetree (zip trees positions))) = (0, 0) # mergelist (map moveextent (zip extents positions)))\ 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 :: \'a tree \ ('a * real) tree\ where \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)\ lemma design'_raw_design': \let (tree, extent) = design' t in tree = raw_design t \ extent = extent_of_tree tree\ proof (induct t) case (Node v subs) define trees where \trees \ fst (unzip (map design' subs))\ define extents where \extents \ snd (unzip (map design' subs))\ define trees' where \trees' \ map raw_design subs\ define extents' where \extents' \ map extent_of_tree trees'\ have \trees = trees'\ unfolding trees_def trees'_def using Node by (induct subs) fastforce+ have \extents = map extent_of_tree trees\ unfolding trees_def extents_def using Node by fastforce then have \extents = extents'\ unfolding extents'_def using \trees = trees'\ by blast have \extent_of_tree (fst (design' (Node v subs))) = snd (design' (Node v subs))\ using design'_extent_of_tree prod.collapse by blast moreover have \zip trees' (fitlist extents') = zip (map raw_design subs) (fitlist (map extent_of_tree (map raw_design subs)))\ unfolding extents'_def trees'_def by simp ultimately show ?case using \extents = extents'\ \trees = trees'\ unfolding extents_def trees_def by simp qed theorem design'_raw_design: \design' t = (raw_design t, extent_of_tree (raw_design t))\ using design'_raw_design' by fastforce theorem design_raw_design: \design t = raw_design t\ unfolding design_def by (simp add: design'_raw_design) section \Property 0 -- Structure preservation\ fun strip_offsets :: \('a \ real) tree \ 'a tree\ where \strip_offsets (Node (label, offset) subs) = Node label (map strip_offsets subs)\ lemma strip_offsets_movetree [simp]: \strip_offsets (movetree (t, x)) = strip_offsets t\ by (induct t rule: strip_offsets.induct) simp_all lemma strip_offsets_movetrees: \length subs' = length xs \ Node v subs = strip_offsets (Node (v, x) subs') \ Node v subs = strip_offsets (Node (v, x) (map movetree (zip subs' xs)))\ by (induct subs' xs arbitrary: subs rule: list_induct2) simp_all lemma map_fst_unzip: assumes \\x \ set xs. f (fst (g x)) = x\ shows \map f (fst (unzip (map g xs))) = xs\ using assms by (induct xs) simp_all lemma strip_offsets_design': \(t', extent) = design' t \ t = strip_offsets t'\ proof (induct t arbitrary: t' extent) case (Node v subs) define subs' where \subs' \ fst (unzip (map design' subs))\ define exts where \exts \ snd (unzip (map design' subs))\ have \sub \ set subs \ strip_offsets (fst (design' sub)) = sub\ for sub using Node by (metis prod.collapse) then have \map strip_offsets subs' = subs\ unfolding subs'_def exts_def using map_fst_unzip by metis then have \map strip_offsets (map movetree (zip subs' (fitlist exts))) = subs\ 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: \strip_offsets (design t) = t\ unfolding design_def using strip_offsets_design' by (metis prod.collapse) theorem design_inj: \t = t' \ design t = design t'\ using strip_offsets_design by metis section \Property 1 -- Properly spaced nodes\ subsection \Spaced, fit and merging\ lemma fit_cons_ge: \fit (p # ps) (q # qs) \ fit ps qs\ by (cases p; cases q) simp_all fun spaced :: \extent \ extent \ bool\ where \spaced ((p1, p2) # ps) ((q1, q2) # qs) = (q1 - p2 \ 1 \ spaced ps qs)\ | \spaced _ _ = True\ lemma spaced_ge: \spaced ps (moveextent (qs, k)) \ k \ k' \ spaced ps (moveextent (qs, k'))\ by (induct ps qs rule: spaced.induct) simp_all lemma spaced_fit [simp]: \spaced ps (moveextent (qs, fit ps qs))\ using spaced_ge by (induct ps qs rule: fit.induct) fastforce+ fun within_extent :: \extent \ extent \ bool\ where \within_extent ((p1, p2) # ps) ((q1, q2) # qs) = (q1 \ p1 \ p2 \ q2 \ within_extent ps qs)\ | \within_extent [] _ = True\ | \within_extent _ _ = False\ lemma within_self: \within_extent ps ps\ by (induct ps) auto lemma within_merge_left: \within_extent ps (merge ps qs)\ using within_self by (induct ps qs rule: merge.induct) simp_all lemma within_merge_right: \within_extent qs (merge ps qs)\ using within_self by (induct ps qs rule: merge.induct) simp_all fun extent3 :: \extent \ extent \ extent \ unit\ where \extent3 ((_, _) # xs) ((_, _) # ys) ((_, _) # zs) = extent3 xs ys zs\ | \extent3 _ _ _ = ()\ lemma within_nil: \within_extent ps [] \ ps = []\ by (induct ps) simp_all lemma within_trans: \within_extent ps qs \ within_extent qs rs \ within_extent ps rs\ using within_nil by (induct ps qs rs rule: extent3.induct) fastforce+ lemma spaced_within_left: \spaced xs qs \ within_extent ps xs \ spaced ps qs\ using within_nil by (induct ps qs xs rule: extent3.induct) fastforce+ lemma spaced_within_right: \spaced ps xs \ within_extent qs xs \ spaced ps qs\ using within_nil by (induct ps qs xs rule: extent3.induct) fastforce+ lemma spaced_left_merge_left: \spaced (merge ps qs) rs \ spaced ps rs\ using spaced_within_left within_merge_left by blast lemma spaced_left_merge_right: \spaced (merge ps qs) rs \ spaced qs rs\ using spaced_within_left within_merge_right by blast lemma spaced_merge_left_left: \spaced ps qs \ spaced ps (moveextent (rs, fit (merge ps qs) rs))\ using spaced_fit spaced_left_merge_left by blast lemma spaced_fit_within: \within_extent ps xs \ spaced ps (moveextent (qs, fit xs qs))\ using spaced_fit spaced_within_left by blast lemma within_extent_merge_right_left: \within_extent y (merge (merge x y) z)\ using within_merge_left within_merge_right within_trans by blast subsection \Proper spacing by fitlistl\ lemma fitlistl'_spaced_within: \within_extent ps xs \ list_all (spaced ps) (map moveextent (zip es (fitlistl' xs es)))\ proof (induct es arbitrary: xs) case (Cons e es) then have \list_all (spaced ps) (moveextent (e, fit xs e) # map moveextent (zip es (fitlistl' (merge xs (moveextent (e, fit xs e))) es)))\ 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: \list_all (spaced ps) (map moveextent (zip es (fitlistl' (merge xs ps) es)))\ using fitlistl'_spaced_within within_merge_right by blast primrec all_pairs :: \('a \ 'a \ bool) \ 'a list \ bool\ where \all_pairs _ [] = True\ | \all_pairs p (e # es) = (list_all (p e) es \ all_pairs p es)\ definition all_spaced :: \extent list \ bool\ where \all_spaced = all_pairs spaced\ lemma all_pairs_drop_last: \all_pairs p (es @ [e']) \ all_pairs p es\ by (induct es) simp_all lemma all_pairs_last: \all_pairs p (es @ [e]) \ list_all (\e'. p e' e) es\ by (induct es) simp_all lemma all_spaced_fitlistl': \all_spaced (map moveextent (zip es (fitlistl' xs es)))\ unfolding all_spaced_def proof (induct es arbitrary: xs) case (Cons e es) then have \all_pairs spaced (moveextent (e, fit xs e) # map moveextent (zip es (fitlistl' (merge xs (moveextent (e, fit xs e))) es)))\ 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: \all_spaced (map moveextent (zip es (fitlistl es)))\ unfolding fitlistl_def using all_spaced_fitlistl' . subsection \Flipping extents\ lemma spaced_move_flip: \spaced (moveextent (flipextent qs, y)) (moveextent (flipextent ps, x)) = spaced (moveextent (ps, -x)) (moveextent (qs, -y))\ unfolding flipextent_def by (induct ps qs rule: spaced.induct) auto subsection \Geometric digression\ lemma spaced_flip: \spaced (flipextent qs) (flipextent ps) = spaced ps qs\ unfolding flipextent_def by (induct ps qs rule: spaced.induct) simp_all lemma all_pairs_map_rev: \all_pairs p (map f (rev es)) \ (\e e'. p (f e') (f e) \ p e e') \ all_pairs p es\ proof (induct es) case (Cons e es) then have *: \all_pairs p (map f (rev es @ [e]))\ by (metis rev.simps(2)) then have \all_pairs p (map f (rev es))\ using all_pairs_drop_last by fastforce then have \all_pairs p es\ using Cons by blast moreover have \list_all (\e'. p e' (f e)) (map f (rev es))\ using * all_pairs_last by simp then have \list_all (\e'. p (f e') (f e)) (rev es)\ unfolding list_all_def by simp then have \list_all (\e'. p (f e') (f e)) es\ by simp then have \list_all (p e) es\ using Cons list_all_iff by metis ultimately show ?case by simp qed simp lemma all_spaced_flip: \all_spaced (map flipextent (rev es)) \ all_spaced es\ unfolding all_spaced_def using all_pairs_map_rev spaced_flip by blast subsection \Properly spaced fitlistr\ lemma spaced_flip_cons: \length es = length xs \ list_all (\e'. spaced e' (moveextent (flipextent a, k))) (map moveextent (zip (map flipextent (rev es)) (rev xs))) \ list_all (spaced (moveextent (a, -k))) (map moveextent (zip es (map uminus xs)))\ 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': \length es = length xs \ all_spaced (map moveextent (zip (map flipextent (rev es)) xs)) \ all_spaced (map moveextent (zip es (rev (map uminus xs))))\ proof (induct es xs rule: list_induct2_rev) case Nil then show ?case by simp next case (Cons e es x xs) then have *: \all_spaced (map moveextent (zip (map flipextent (rev es)) (rev xs) @ [(flipextent e, x)]))\ by simp then have \all_spaced (map moveextent (zip (map flipextent (rev es)) (rev xs)))\ unfolding all_spaced_def using all_pairs_drop_last by fastforce then have \all_spaced (map moveextent (zip es (rev (map uminus (rev xs)))))\ using Cons by blast then have \all_spaced (map moveextent (zip es (map uminus xs)))\ by (simp add: rev_map) moreover have \all_spaced (map moveextent (zip (map flipextent (rev es)) (rev xs)) @ [moveextent (flipextent e,x)])\ using * by simp then have \list_all (\e'. spaced e' (moveextent (flipextent e, x))) (map moveextent (zip (map flipextent (rev es)) (rev xs)))\ unfolding all_spaced_def using all_pairs_last by fast then have \list_all (spaced (moveextent (e, -x))) (map moveextent (zip es (map uminus xs)))\ using Cons spaced_flip_cons by blast ultimately show ?case unfolding all_spaced_def by (simp add: rev_map) qed lemma all_spaced_fitlistr: \all_spaced (map moveextent (zip es (fitlistr es)))\ unfolding fitlistr_def comp_def using all_spaced_fitlistl all_spaced_fitlistr' fitlistl_length by (metis length_map length_rev) subsection \Properly spaced fitlist\ lemma spaced_mean: \spaced (moveextent (ps, x)) (moveextent (qs, y)) \ spaced (moveextent (ps, a)) (moveextent (qs, b)) \ spaced (moveextent (ps, mean (x, a))) (moveextent (qs, mean (y, b)))\ by (induct ps qs rule: spaced.induct) (simp_all add: add_divide_distrib) fun all_spaced_induct :: \extent list \ real list \ real list \ unit\ where \all_spaced_induct (e # es) (a # as) (b # bs) = all_spaced_induct es as bs\ | \all_spaced_induct _ _ _ = ()\ lemma all_spaced_mean_cons: \list_all (spaced (moveextent (p, a))) (map moveextent (zip es as)) \ list_all (spaced (moveextent (p, b))) (map moveextent (zip es bs)) \ list_all (spaced (moveextent (p, mean (a, b)))) (map moveextent (zip es (map mean (zip as bs))))\ using spaced_mean by (induct es as bs rule: all_spaced_induct.induct) simp_all lemma all_spaced_mean: \all_spaced (map moveextent (zip es as)) \ all_spaced (map moveextent (zip es bs)) \ all_spaced (map moveextent (zip es (map mean (zip as bs))))\ proof (induct es as bs rule: all_spaced_induct.induct) case (1 e es a as b bs) then have \list_all (spaced (moveextent (e, a))) (map moveextent (zip es as))\ unfolding all_spaced_def by simp moreover have \list_all (spaced (moveextent (e, b))) (map moveextent (zip es bs))\ using 1 unfolding all_spaced_def by simp moreover have \list_all (spaced (moveextent (e, mean(a, b)))) (map moveextent (zip es (map mean (zip as bs))))\ 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: \all_spaced (map moveextent (zip es (fitlist es)))\ unfolding fitlist_def using all_spaced_mean all_spaced_fitlistl all_spaced_fitlistr by fast subsection \Properly spaced tree\ fun get_offset :: \('a * real) tree \ real\ where \get_offset (Node (_, x) _) = x\ definition spaced_offset :: \real \ real \ bool\ where \spaced_offset x y = (x + 1 \ y)\ primrec spaced_tree :: \('a * real) tree \ bool\ where \spaced_tree (Node _ subs) = (all_pairs spaced_offset (map get_offset subs) \ list_all spaced_tree subs)\ lemma spaced_extents_offsets: assumes \spaced (extent_of_tree s) (extent_of_tree t)\ shows \spaced_offset (get_offset s) (get_offset t)\ 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: \all_spaced (map extent_of_tree subs) \ list_all spaced_tree subs \ spaced_tree (Node (a, 0) subs)\ proof (induct subs) case (Cons sub subs) then have \spaced_tree (Node (a, 0) subs)\ unfolding all_spaced_def by simp moreover have \all_spaced (map extent_of_tree (sub # subs))\ using Cons by simp then have \list_all (\sub'. spaced (extent_of_tree sub) (extent_of_tree sub')) subs\ unfolding all_spaced_def by (simp add: list_all_iff) then have \list_all (\sub'. spaced_offset (get_offset sub) (get_offset sub')) subs\ using spaced_extents_offsets by (metis (no_types) list_all_iff) then have \list_all (spaced_offset (get_offset sub)) (map get_offset subs)\ by (simp add: list_all_iff) ultimately show ?case using Cons by simp qed simp lemma merge_nil [simp]: \merge ps [] = ps\ by (induct ps) simp_all lemma merge_comm: \merge ps qs = merge qs ps\ by (induct ps qs rule: merge.induct) auto lemma move_spaced_tree: \spaced_tree t \ spaced_tree (movetree (t, k))\ by (induct t) auto lemma move_spaced_trees: \list_all spaced_tree ts \ list_all spaced_tree (map movetree (zip ts as))\ by (induct ts as rule: list_induct2') (simp_all add: move_spaced_tree) lemma all_spaced_extent_of_fitted_tree: \all_spaced (map moveextent (zip (map extent_of_tree ts) as)) \ list_all spaced_tree (map movetree (zip ts as)) \ all_spaced (map extent_of_tree (map movetree (zip ts as)))\ 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: \list_all (\(a, b). f a = g b) xs \ (as, bs) = unzip xs \ map f as = map g bs\ by (induct xs arbitrary: as bs rule: unzip.induct) simp_all lemma spaced_raw_design: \spaced_tree (raw_design t)\ proof (induct t) case (Node v subs) define trees where \trees \ map raw_design subs\ define extents where \extents \ map extent_of_tree trees\ define positions where \positions \ fitlist extents\ have \list_all spaced_tree trees\ unfolding trees_def using Node by (induct subs) simp_all then have \list_all spaced_tree (map movetree (zip trees positions))\ using move_spaced_trees by blast moreover from this have \all_spaced (map extent_of_tree (map movetree (zip trees positions)))\ unfolding extents_def positions_def using Node all_spaced_fitlist all_spaced_extent_of_fitted_tree by blast moreover have \?case = spaced_tree (Node (v, 0) (map movetree (zip trees positions)))\ unfolding trees_def extents_def positions_def by simp ultimately show ?case using all_spaced_tree by metis qed theorem spaced_design: \spaced_tree (design t)\ using design_raw_design spaced_raw_design by metis section \Property 2 -- Centered parent\ primrec listsum :: \real list \ real\ where \listsum [] = 0\ | \listsum (x # xs) = x + listsum xs\ definition minlist :: \real list \ real\ where \minlist xs \ Min (set xs)\ definition maxlist :: \real list \ real\ where \maxlist xs \ Max (set xs)\ fun centered :: \('a \ real) tree \ bool\ where \centered (Node (_, offset) _) = (offset = 0)\ fun centered_parent :: \('a \ real) tree \ bool\ where \centered_parent (Node _ []) = True\ | \centered_parent (Node (_, offset) subtrees) = (offset = 0 \ (- get_offset (hd subtrees) = get_offset (last subtrees)))\ lemma min_max_list_bounds: \\x \ set xs. x \ {minlist xs .. maxlist xs}\ unfolding minlist_def maxlist_def by (induct xs) simp_all lemma fit_nonnegative [simp]: \fit ps qs \ 0\ by (induct ps qs rule: fit.induct) simp_all lemma fit_flipextent: \fit ps qs = fit (flipextent qs) (flipextent ps)\ unfolding flipextent_def by (induct ps qs rule: fit.induct) simp_all lemma fitlistl'_nonnegative: \list_all (\x. x \ 0) (fitlistl' acc es)\ 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: \list_all (\x. x \ 0) (fitlistl es)\ unfolding fitlistl_def using fitlistl'_nonnegative by blast lemma fitlistl_bounded: obtains x where \list_all (\k. k \ {0 .. x}) (fitlistl es)\ proof - have \list_all (\k. k \ {0 .. maxlist (fitlistl es)}) (fitlistl es)\ 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]: \listsum (xs @ ys) = listsum xs + listsum ys\ by (induct xs arbitrary: ys) simp_all lemma listsum_rev [simp]: \listsum (rev xs) = listsum xs\ using listsum_append by (induct xs) simp_all lemma listsum_uminus: \listsum xs = - listsum (map uminus xs)\ by (induct xs) simp_all lemma listsum_mean: \length xs = length ys \ listsum (map mean (zip xs ys)) = mean (listsum xs, listsum ys)\ by (induct xs ys rule: list_induct2) simp_all lemma listsum_opposite: \length xs = length ys \ listsum xs = - listsum ys \ listsum (map mean (zip xs ys)) = 0\ using listsum_mean by fastforce lemma get_offset_movetree [simp]: \get_offset (movetree (t, x)) = get_offset t + x\ by (induct t) auto lemma minlist_rev: \minlist xs = minlist (rev xs)\ unfolding minlist_def by simp lemma maxlist_rev: \maxlist xs = maxlist (rev xs)\ unfolding maxlist_def by simp lemma fit_flipextent_right: \fit ps (flipextent qs) = fit qs (flipextent ps)\ unfolding flipextent_def by (induct ps qs rule: fit.induct) simp_all lemma fit_flipextent_left: \fit (flipextent ps) qs = fit (flipextent qs) ps\ unfolding flipextent_def by (induct ps qs rule: fit.induct) simp_all lemma flipextent_inv [simp]: \flipextent (flipextent ps) = ps\ unfolding flipextent_def by (induct ps) auto lemma centered_design': assumes \(t', extent) = design' t\ shows \centered t'\ proof (cases t) case (Node v subs) then show ?thesis proof (cases \unzip (map design' subs)\) case (Pair a b) then show ?thesis using assms Node by (simp add: Let_def) qed qed lemma centered_design: \centered (design t)\ unfolding design_def using centered_design' by (metis prod.collapse) lemma non_empty_extent_of_tree: \length (extent_of_tree t) > 0\ by (cases t) auto lemma length_extent_design': assumes \(t', extent) = design' t\ shows \length extent > 0\ using assms design'_extent_of_tree non_empty_extent_of_tree by blast lemma fst_unzip_list_all: \\x. P (fst (f x)) \ list_all P (fst (unzip (map f xs)))\ by (induct xs) simp_all lemma snd_unzip_list_all: \\x. P (snd (f x)) \ list_all P (snd (unzip (map f xs)))\ by (induct xs) simp_all lemma length_extents_design': assumes \(trees', extents) = unzip (map design' trees)\ shows \list_all (\e. length e > 0) extents\ using assms length_extent_design' snd_unzip_list_all by (metis eq_snd_iff) lemma get_offset_raw_design: \get_offset (raw_design t) = 0\ by (cases t) simp lemma get_offset_design': assumes \(t', extent) = design' t\ shows \get_offset t' = 0\ using assms get_offset_raw_design design'_raw_design by (metis fstI) lemma get_offsets_design': assumes \(ts, es) = unzip (map design' subs)\ shows \list_all (\t. get_offset t = 0) ts\ using assms fst_unzip_list_all get_offset_design' by (metis (mono_tags, lifting) design'_raw_design fstI) lemma last_rev: \length xs > 0 \ last (rev xs) = hd xs\ by (induct xs) simp_all lemma hd_fitlistl: \hd (fitlistl (e # es)) = 0\ unfolding fitlistl_def by simp lemma last_fitlistr: \last (fitlistr (e # es)) = 0\ proof - have \last (fitlistr (e # es)) = last ((rev \ map uminus \ fitlistl \ map flipextent \ rev) (e # es))\ unfolding fitlistr_def by blast also have \\ = hd ((map uminus \ fitlistl \ map flipextent \ rev) (e # es))\ using fitlistl_length length_map length_rev by (simp add: last_rev) also have \\ = - hd ((fitlistl \ map flipextent \ rev) (e # es))\ unfolding comp_def using length_map length_rev fitlistl_length hd_map by (metis length_0_conv list.discI) also have \\ = - 0\ 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 \length as > 0\ \length bs > 0\ shows \hd (map f (zip as bs)) = f (hd as, hd bs)\ proof (cases \map f (zip as bs)\) case Nil have \length (map f (zip as bs)) > 0\ using assms by simp then show ?thesis using Nil by simp next case (Cons x xs) have \zip as bs = zip (hd as # tl as) (hd bs # tl bs)\ using assms by simp then show ?thesis using Cons by simp qed lemma last_map_zip: assumes \length as > 0\ \length bs > 0\ \length as = length bs\ shows \last (map f (zip as bs)) = f (last as, last bs)\ proof (cases \map f (zip as bs)\) case Nil have \length (map f (zip as bs)) > 0\ using assms by simp then show ?thesis using Nil by simp next case (Cons x xs) have \zip as bs = zip (butlast as @ [last as]) (butlast bs @ [last bs])\ using assms(1-2) by simp then show ?thesis using Cons assms(3) by fastforce qed lemma last_fitlist: assumes \list_all (\e. length e > 0) (e # es)\ shows \last (fitlist (e # es)) = last (fitlistl (e # es)) / 2\ proof - have \fitlist (e # es) = map mean (zip (fitlistl (e # es)) (fitlistr (e # es)))\ unfolding fitlist_def by simp also have \last \ = mean (last (fitlistl (e # es)), last (fitlistr (e # es)))\ using fitlistl_length fitlistr_length by (simp add: last_map_zip) also have \\ = mean (last (fitlistl (e # es)), 0)\ using last_fitlistr by simp finally show ?thesis by simp qed lemma hd_fitlist: assumes \list_all (\e. length e > 0) (e # es)\ shows \hd (fitlist (e # es)) = hd (fitlistr (e # es)) / 2\ proof - have \fitlist (e # es) = map mean (zip (fitlistl (e # es)) (fitlistr (e # es)))\ unfolding fitlist_def by simp also have \hd \ = mean (hd (fitlistl (e # es)), hd (fitlistr (e # es)))\ using fitlistl_length fitlistr_length by (simp add: hd_map_zip) also have \\ = mean (0, hd (fitlistr (e # es)))\ using hd_fitlistl by simp finally show ?thesis by simp qed lemma split_list_Cons: assumes \length l > 0\ obtains x xs where \x # xs = l\ using assms by (metis length_greater_0_conv list.exhaust) section \Mirror image property\ fun reflect :: \'a tree \ 'a tree\ where \reflect (Node v subtrees) = Node v (map reflect (rev subtrees))\ fun reflectpos :: \('a * real) tree \ ('a * real) tree\ where \reflectpos (Node (label, offset) subtrees) = Node (label, -offset) (map reflectpos subtrees)\ lemma reflect_inv: \t = reflect (reflect t)\ proof (induct t rule: reflect.induct) case (1 v subtrees) then show ?case by (induct subtrees) simp_all qed lemma reflectpos_inv: \t = reflectpos (reflectpos t)\ proof (induct t rule: reflectpos.induct) case (1 label offset subtrees) then show ?case by (induct subtrees) simp_all qed lemma reflect_reflectpos: \reflect (reflectpos t) = reflectpos (reflect t)\ proof (induct t rule: reflectpos.induct) case (1 label offset subtrees) then show ?case by (induct subtrees) simp_all qed lemma reflect_movetree: \reflect (movetree (t, k)) = movetree (reflect t, k)\ by (cases t rule: reflectpos.cases) simp lemma reflectpos_movetree: \reflectpos (movetree (t, k)) = movetree (reflectpos t, -k)\ by (cases t rule: reflectpos.cases) simp lemma map_reflect_movetree: assumes \length ts = length xs\ shows \map reflect (map movetree (zip ts xs)) = map movetree (zip (map reflect ts) xs)\ using assms by (induct ts xs rule: list_induct2) (simp_all add: reflect_movetree) lemma map_reflectpos_movetree: assumes \length ts = length xs\ shows \map reflectpos (map movetree (zip ts xs)) = map movetree (zip (map reflectpos ts) (map uminus xs))\ using assms by (induct ts xs rule: list_induct2) (simp_all add: reflectpos_movetree) lemma rev_zip: assumes \length as = length bs\ shows \rev (zip as bs) = zip (rev as) (rev bs)\ using assms by (induct as bs rule: list_induct2) simp_all section \Property 4 -- Subtree consistency property\ primrec subtrees :: \'a tree \ ('a tree) set\ where \subtrees (Node v subs) = {Node v subs} \ (\set (map subtrees subs))\ lemma strip_offsets_design_equal: \strip_offsets (design sub) = strip_offsets (design sub') \ design sub = design sub'\ using strip_offsets_design by metis lemma map_image_subtrees: assumes \\t. image f (subtrees t) = subtrees (f t)\ shows \map (image f) (map subtrees ts) = map subtrees (map f ts)\ using assms by (induct ts) simp_all lemma strip_offsets_subtrees: \image strip_offsets (subtrees t) = subtrees (strip_offsets t)\ by (induct t rule: strip_offsets.induct) fastforce lemma map_strip_offsets_movetree: assumes \length ts = length xs\ shows \map strip_offsets (map movetree (zip ts xs)) = map strip_offsets ts\ using assms by (induct ts xs rule: list_induct2) simp_all lemma strip_offsets_raw_design: \strip_offsets (raw_design t) = t\ using design_raw_design strip_offsets_design by metis section \Counterexample to property 3 as stated in paper\ lemma "\(\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 "\ (design ?t = reflect (reflectpos (design ?t)))" by normalization then show ?thesis by blast qed value \ let t = Node ''a'' [Node ''b'' [Node ''c'' [Node ''d'' [], Node ''e'' []]], Node ''f'' [Node ''g'' []]] in (design t, reflectpos (design (reflect t))) \ end