# HG changeset patch # User nipkow # Date 1596729097 -7200 # Node ID c65614b556b2c9e46590e875ecedf07210cb4c65 # Parent 8c547eac8381b722dc88a9c8ed6f6ff7a891fd98# Parent 9fa6dde8d95954f60fed0c794e517859a29500ac merged diff -r 8c547eac8381 -r c65614b556b2 src/HOL/Data_Structures/Tree23_of_List.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Tree23_of_List.thy Thu Aug 06 17:51:37 2020 +0200 @@ -0,0 +1,178 @@ +(* Author: Tobias Nipkow *) + +section \2-3 Tree from List\ + +theory Tree23_of_List +imports Tree23 +begin + +text \Linear-time bottom up conversion of a list of items into a complete 2-3 tree +whose inorder traversal yields the list of items.\ + + +subsection "Code" + +text \Nonempty lists of 2-3 trees alternating with items, starting and ending with a 2-3 tree:\ + +datatype 'a tree23s = T "'a tree23" | TTs "'a tree23" "'a" "'a tree23s" + +abbreviation "not_T ts == (\t. ts \ T t)" + +fun len :: "'a tree23s \ nat" where +"len (T _) = 1" | +"len (TTs _ _ ts) = len ts + 1" + +fun trees :: "'a tree23s \ 'a tree23 set" where +"trees (T t) = {t}" | +"trees (TTs t a ts) = {t} \ trees ts" + +text \Join pairs of adjacent trees:\ + +fun join_adj :: "'a tree23s \ 'a tree23s" where +"join_adj (TTs t1 a (T t2)) = T(Node2 t1 a t2)" | +"join_adj (TTs t1 a (TTs t2 b (T t3))) = T(Node3 t1 a t2 b t3)" | +"join_adj (TTs t1 a (TTs t2 b tas)) = TTs (Node2 t1 a t2) b (join_adj tas)" + +text \Towards termination of \join_all\:\ + +lemma len_ge2: + "not_T ts \ len ts \ 2" +by(cases ts rule: join_adj.cases) auto + +lemma [measure_function]: "is_measure len" +by(rule is_measure_trivial) + +lemma len_join_adj_div2: + "not_T ts \ len(join_adj ts) \ len ts div 2" +by(induction ts rule: join_adj.induct) auto + +lemma len_join_adj1: "not_T ts \ len(join_adj ts) < len ts" +using len_join_adj_div2[of ts] len_ge2[of ts] by simp + +corollary len_join_adj2[termination_simp]: "len(join_adj (TTs t a ts)) \ len ts" +using len_join_adj1[of "TTs t a ts"] by simp + +fun join_all :: "'a tree23s \ 'a tree23" where +"join_all (T t) = t" | +"join_all tas = join_all (join_adj tas)" + +fun leaves :: "'a list \ 'a tree23s" where +"leaves [] = T Leaf" | +"leaves (a # as) = TTs Leaf a (leaves as)" + +definition tree23_of_list :: "'a list \ 'a tree23" where +"tree23_of_list as = join_all(leaves as)" + + +subsection \Functional correctness\ + +subsubsection \\inorder\:\ + +fun inorder2 :: "'a tree23s \ 'a list" where +"inorder2 (T t) = inorder t" | +"inorder2 (TTs t a ts) = inorder t @ a # inorder2 ts" + +lemma inorder2_join_adj: "not_T ts \ inorder2(join_adj ts) = inorder2 ts" +by (induction ts rule: join_adj.induct) auto + +lemma inorder_join_all: "inorder (join_all ts) = inorder2 ts" +proof (induction ts rule: measure_induct_rule[where f = "len"]) + case (less ts) + show ?case + proof (cases ts) + case T thus ?thesis by simp + next + case (TTs t a ts) + then show ?thesis using less inorder2_join_adj[of "TTs t a ts"] + by (simp add: le_imp_less_Suc len_join_adj2) + qed +qed + +lemma inorder2_leaves: "inorder2(leaves as) = as" +by(induction as) auto + +lemma "inorder(tree23_of_list as) = as" +by(simp add: tree23_of_list_def inorder_join_all inorder2_leaves) + +subsubsection \Completeness:\ + +lemma complete_join_adj: + "\t \ trees ts. complete t \ height t = n \ not_T ts \ + \t \ trees (join_adj ts). complete t \ height t = Suc n" +by (induction ts rule: join_adj.induct) auto + +lemma complete_join_all: + "\t \ trees ts. complete t \ height t = n \ complete (join_all ts)" +proof (induction ts arbitrary: n rule: measure_induct_rule[where f = "len"]) + case (less ts) + show ?case + proof (cases ts) + case T thus ?thesis using less.prems by simp + next + case (TTs t a ts) + then show ?thesis + using less.prems apply simp + using complete_join_adj[of "TTs t a ts" n, simplified] less.IH len_join_adj1 by blast + qed +qed + +lemma complete_leaves: "t \ trees (leaves as) \ complete t \ height t = 0" +by (induction as) auto + +corollary complete: "complete(tree23_of_list as)" +by(simp add: tree23_of_list_def complete_leaves complete_join_all[of _ 0]) + + +subsection "Linear running time" + +fun t_join_adj :: "'a tree23s \ nat" where +"t_join_adj (TTs t1 a (T t2)) = 1" | +"t_join_adj (TTs t1 a (TTs t2 b (T t3))) = 1" | +"t_join_adj (TTs t1 a (TTs t2 b ts)) = t_join_adj ts + 1" + +fun t_join_all :: "'a tree23s \ nat" where +"t_join_all (T t) = 1" | +"t_join_all ts = t_join_adj ts + t_join_all (join_adj ts)" + +fun t_leaves :: "'a list \ nat" where +"t_leaves [] = 1" | +"t_leaves (a # as) = t_leaves as + 1" + +definition t_tree23_of_list :: "'a list \ nat" where +"t_tree23_of_list as = t_leaves as + t_join_all(leaves as)" + +lemma t_join_adj: "not_T ts \ t_join_adj ts \ len ts div 2" +by(induction ts rule: t_join_adj.induct) auto + +lemma t_join_all: "t_join_all ts \ len ts" +proof(induction ts rule: measure_induct_rule[where f = len]) + case (less ts) + show ?case + proof (cases ts) + case T thus ?thesis by simp + next + case TTs + have 0: "\t. ts \ T t" using TTs by simp + have "t_join_all ts = t_join_adj ts + t_join_all (join_adj ts)" + using TTs by simp + also have "\ \ len ts div 2 + t_join_all (join_adj ts)" + using t_join_adj[OF 0] by linarith + also have "\ \ len ts div 2 + len (join_adj ts)" + using less.IH[of "join_adj ts"] len_join_adj1[OF 0] by simp + also have "\ \ len ts div 2 + len ts div 2" + using len_join_adj_div2[OF 0] by linarith + also have "\ \ len ts" by linarith + finally show ?thesis . + qed +qed + +lemma t_leaves: "t_leaves as = length as + 1" +by(induction as) auto + +lemma len_leaves: "len(leaves as) = length as + 1" +by(induction as) auto + +lemma t_tree23_of_list: "t_tree23_of_list as \ 2*(length as + 1)" +using t_join_all[of "leaves as"] by(simp add: t_tree23_of_list_def t_leaves len_leaves) + +end diff -r 8c547eac8381 -r c65614b556b2 src/HOL/Data_Structures/document/root.bib --- a/src/HOL/Data_Structures/document/root.bib Thu Aug 06 16:45:35 2020 +0200 +++ b/src/HOL/Data_Structures/document/root.bib Thu Aug 06 17:51:37 2020 +0200 @@ -41,6 +41,16 @@ journal={J. Functional Programming}, volume=19,number={6},pages={633--644},year=2009} +@article{jfp/Hinze18, + author = {Ralf Hinze}, + title = {On constructing 2-3 trees}, + journal = {J. Funct. Program.}, + volume = {28}, + pages = {e19}, + year = {2018}, + url = {https://doi.org/10.1017/S0956796818000187}, +} + @article{HoffmannOD-TOPLAS82, author={Christoph M. Hoffmann and Michael J. O'Donnell}, title={Programming with Equations},journal={{ACM} Trans. Program. Lang. Syst.}, diff -r 8c547eac8381 -r c65614b556b2 src/HOL/Data_Structures/document/root.tex --- a/src/HOL/Data_Structures/document/root.tex Thu Aug 06 16:45:35 2020 +0200 +++ b/src/HOL/Data_Structures/document/root.tex Thu Aug 06 17:51:37 2020 +0200 @@ -51,7 +51,7 @@ O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion) and Reade \cite{Reade-SCP92}. Our formalisation is based on the teaching material by -Turbak~\cite{Turbak230} . +Turbak~\cite{Turbak230} and the article by Hinze~\cite{jfp/Hinze18}. \paragraph{1-2 brother trees} They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}. diff -r 8c547eac8381 -r c65614b556b2 src/HOL/ROOT --- a/src/HOL/ROOT Thu Aug 06 16:45:35 2020 +0200 +++ b/src/HOL/ROOT Thu Aug 06 17:51:37 2020 +0200 @@ -273,6 +273,7 @@ RBT_Set2 RBT_Map Tree23_Map + Tree23_of_List Tree234_Map Brother12_Map AA_Map