# HG changeset patch
# User nipkow
# Date 1596728397 -7200
# Node ID 9fa6dde8d95954f60fed0c794e517859a29500ac
# Parent  f978ecaf119a29917368de371967501118ef8c33
tuned

diff -r f978ecaf119a -r 9fa6dde8d959 src/HOL/Data_Structures/Tree23_of_List.thy
--- 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)"
diff -r f978ecaf119a -r 9fa6dde8d959 src/HOL/Data_Structures/document/root.bib
--- 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.},
diff -r f978ecaf119a -r 9fa6dde8d959 src/HOL/Data_Structures/document/root.tex
--- 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}.