author nipkow Thu, 06 Aug 2020 17:39:57 +0200 changeset 72100 9fa6dde8d959 parent 72099 f978ecaf119a child 72101 c65614b556b2
tuned
```--- 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>

-  "\<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)