--- a/src/HOL/Data_Structures/Tree23_of_List.thy Thu Aug 06 17:11:33 2020 +0200
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy Thu Aug 06 17:39:57 2020 +0200
@@ -22,9 +22,9 @@
"len (T _) = 1" |
"len (TTs _ _ ts) = len ts + 1"
-fun trees :: "'a tree23s \<Rightarrow> 'a tree23 list" where
-"trees (T t) = [t]" |
-"trees (TTs t a ts) = t # trees ts"
+fun trees :: "'a tree23s \<Rightarrow> 'a tree23 set" where
+"trees (T t) = {t}" |
+"trees (TTs t a ts) = {t} \<union> trees ts"
text \<open>Join pairs of adjacent trees:\<close>
@@ -97,12 +97,12 @@
subsubsection \<open>Completeness:\<close>
lemma complete_join_adj:
- "\<forall>t \<in> set(trees ts). complete t \<and> height t = n \<Longrightarrow> not_T ts \<Longrightarrow>
- \<forall>t \<in> set(trees (join_adj ts)). complete t \<and> height t = Suc n"
+ "\<forall>t \<in> trees ts. complete t \<and> height t = n \<Longrightarrow> not_T ts \<Longrightarrow>
+ \<forall>t \<in> trees (join_adj ts). complete t \<and> height t = Suc n"
by (induction ts rule: join_adj.induct) auto
lemma complete_join_all:
- "\<forall>t \<in> set(trees ts). complete t \<and> height t = n \<Longrightarrow> complete (join_all ts)"
+ "\<forall>t \<in> trees ts. complete t \<and> height t = n \<Longrightarrow> complete (join_all ts)"
proof (induction ts arbitrary: n rule: measure_induct_rule[where f = "len"])
case (less ts)
show ?case
@@ -116,7 +116,7 @@
qed
qed
-lemma complete_leaves: "t \<in> set(trees (leaves as)) \<Longrightarrow> complete t \<and> height t = 0"
+lemma complete_leaves: "t \<in> trees (leaves as) \<Longrightarrow> complete t \<and> height t = 0"
by (induction as) auto
corollary complete: "complete(tree23_of_list as)"
--- a/src/HOL/Data_Structures/document/root.bib Thu Aug 06 17:11:33 2020 +0200
+++ b/src/HOL/Data_Structures/document/root.bib Thu Aug 06 17:39:57 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.},
--- a/src/HOL/Data_Structures/document/root.tex Thu Aug 06 17:11:33 2020 +0200
+++ b/src/HOL/Data_Structures/document/root.tex Thu Aug 06 17:39:57 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}.