72099
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section \<open>2-3 Tree from List\<close>
|
|
4 |
|
|
5 |
theory Tree23_of_List
|
|
6 |
imports Tree23
|
|
7 |
begin
|
|
8 |
|
|
9 |
text \<open>Linear-time bottom up conversion of a list of items into a complete 2-3 tree
|
|
10 |
whose inorder traversal yields the list of items.\<close>
|
|
11 |
|
|
12 |
|
|
13 |
subsection "Code"
|
|
14 |
|
|
15 |
text \<open>Nonempty lists of 2-3 trees alternating with items, starting and ending with a 2-3 tree:\<close>
|
|
16 |
|
|
17 |
datatype 'a tree23s = T "'a tree23" | TTs "'a tree23" "'a" "'a tree23s"
|
|
18 |
|
|
19 |
abbreviation "not_T ts == (\<forall>t. ts \<noteq> T t)"
|
|
20 |
|
|
21 |
fun len :: "'a tree23s \<Rightarrow> nat" where
|
|
22 |
"len (T _) = 1" |
|
|
23 |
"len (TTs _ _ ts) = len ts + 1"
|
|
24 |
|
72100
|
25 |
fun trees :: "'a tree23s \<Rightarrow> 'a tree23 set" where
|
|
26 |
"trees (T t) = {t}" |
|
|
27 |
"trees (TTs t a ts) = {t} \<union> trees ts"
|
72099
|
28 |
|
|
29 |
text \<open>Join pairs of adjacent trees:\<close>
|
|
30 |
|
|
31 |
fun join_adj :: "'a tree23s \<Rightarrow> 'a tree23s" where
|
|
32 |
"join_adj (TTs t1 a (T t2)) = T(Node2 t1 a t2)" |
|
|
33 |
"join_adj (TTs t1 a (TTs t2 b (T t3))) = T(Node3 t1 a t2 b t3)" |
|
72121
|
34 |
"join_adj (TTs t1 a (TTs t2 b ts)) = TTs (Node2 t1 a t2) b (join_adj ts)"
|
72099
|
35 |
|
|
36 |
text \<open>Towards termination of \<open>join_all\<close>:\<close>
|
|
37 |
|
|
38 |
lemma len_ge2:
|
|
39 |
"not_T ts \<Longrightarrow> len ts \<ge> 2"
|
|
40 |
by(cases ts rule: join_adj.cases) auto
|
|
41 |
|
|
42 |
lemma [measure_function]: "is_measure len"
|
|
43 |
by(rule is_measure_trivial)
|
|
44 |
|
|
45 |
lemma len_join_adj_div2:
|
|
46 |
"not_T ts \<Longrightarrow> len(join_adj ts) \<le> len ts div 2"
|
|
47 |
by(induction ts rule: join_adj.induct) auto
|
|
48 |
|
|
49 |
lemma len_join_adj1: "not_T ts \<Longrightarrow> len(join_adj ts) < len ts"
|
|
50 |
using len_join_adj_div2[of ts] len_ge2[of ts] by simp
|
|
51 |
|
|
52 |
corollary len_join_adj2[termination_simp]: "len(join_adj (TTs t a ts)) \<le> len ts"
|
|
53 |
using len_join_adj1[of "TTs t a ts"] by simp
|
|
54 |
|
|
55 |
fun join_all :: "'a tree23s \<Rightarrow> 'a tree23" where
|
|
56 |
"join_all (T t) = t" |
|
72121
|
57 |
"join_all ts = join_all (join_adj ts)"
|
72099
|
58 |
|
|
59 |
fun leaves :: "'a list \<Rightarrow> 'a tree23s" where
|
|
60 |
"leaves [] = T Leaf" |
|
|
61 |
"leaves (a # as) = TTs Leaf a (leaves as)"
|
|
62 |
|
|
63 |
definition tree23_of_list :: "'a list \<Rightarrow> 'a tree23" where
|
|
64 |
"tree23_of_list as = join_all(leaves as)"
|
|
65 |
|
|
66 |
|
|
67 |
subsection \<open>Functional correctness\<close>
|
|
68 |
|
|
69 |
subsubsection \<open>\<open>inorder\<close>:\<close>
|
|
70 |
|
|
71 |
fun inorder2 :: "'a tree23s \<Rightarrow> 'a list" where
|
|
72 |
"inorder2 (T t) = inorder t" |
|
|
73 |
"inorder2 (TTs t a ts) = inorder t @ a # inorder2 ts"
|
|
74 |
|
|
75 |
lemma inorder2_join_adj: "not_T ts \<Longrightarrow> inorder2(join_adj ts) = inorder2 ts"
|
|
76 |
by (induction ts rule: join_adj.induct) auto
|
|
77 |
|
|
78 |
lemma inorder_join_all: "inorder (join_all ts) = inorder2 ts"
|
72121
|
79 |
proof (induction ts rule: join_all.induct)
|
|
80 |
case 1 thus ?case by simp
|
|
81 |
next
|
|
82 |
case (2 t a ts)
|
|
83 |
thus ?case using inorder2_join_adj[of "TTs t a ts"]
|
|
84 |
by (simp add: le_imp_less_Suc)
|
72099
|
85 |
qed
|
|
86 |
|
|
87 |
lemma inorder2_leaves: "inorder2(leaves as) = as"
|
|
88 |
by(induction as) auto
|
|
89 |
|
|
90 |
lemma "inorder(tree23_of_list as) = as"
|
|
91 |
by(simp add: tree23_of_list_def inorder_join_all inorder2_leaves)
|
|
92 |
|
|
93 |
subsubsection \<open>Completeness:\<close>
|
|
94 |
|
|
95 |
lemma complete_join_adj:
|
72100
|
96 |
"\<forall>t \<in> trees ts. complete t \<and> height t = n \<Longrightarrow> not_T ts \<Longrightarrow>
|
|
97 |
\<forall>t \<in> trees (join_adj ts). complete t \<and> height t = Suc n"
|
72099
|
98 |
by (induction ts rule: join_adj.induct) auto
|
|
99 |
|
|
100 |
lemma complete_join_all:
|
72100
|
101 |
"\<forall>t \<in> trees ts. complete t \<and> height t = n \<Longrightarrow> complete (join_all ts)"
|
72121
|
102 |
proof (induction ts arbitrary: n rule: join_all.induct)
|
|
103 |
case 1 thus ?case by simp
|
|
104 |
next
|
|
105 |
case (2 t a ts)
|
|
106 |
thus ?case
|
|
107 |
apply simp using complete_join_adj[of "TTs t a ts" n, simplified] by blast
|
72099
|
108 |
qed
|
|
109 |
|
72100
|
110 |
lemma complete_leaves: "t \<in> trees (leaves as) \<Longrightarrow> complete t \<and> height t = 0"
|
72099
|
111 |
by (induction as) auto
|
|
112 |
|
|
113 |
corollary complete: "complete(tree23_of_list as)"
|
|
114 |
by(simp add: tree23_of_list_def complete_leaves complete_join_all[of _ 0])
|
|
115 |
|
|
116 |
|
|
117 |
subsection "Linear running time"
|
|
118 |
|
|
119 |
fun t_join_adj :: "'a tree23s \<Rightarrow> nat" where
|
|
120 |
"t_join_adj (TTs t1 a (T t2)) = 1" |
|
|
121 |
"t_join_adj (TTs t1 a (TTs t2 b (T t3))) = 1" |
|
|
122 |
"t_join_adj (TTs t1 a (TTs t2 b ts)) = t_join_adj ts + 1"
|
|
123 |
|
|
124 |
fun t_join_all :: "'a tree23s \<Rightarrow> nat" where
|
|
125 |
"t_join_all (T t) = 1" |
|
|
126 |
"t_join_all ts = t_join_adj ts + t_join_all (join_adj ts)"
|
|
127 |
|
|
128 |
fun t_leaves :: "'a list \<Rightarrow> nat" where
|
|
129 |
"t_leaves [] = 1" |
|
|
130 |
"t_leaves (a # as) = t_leaves as + 1"
|
|
131 |
|
|
132 |
definition t_tree23_of_list :: "'a list \<Rightarrow> nat" where
|
|
133 |
"t_tree23_of_list as = t_leaves as + t_join_all(leaves as)"
|
|
134 |
|
|
135 |
lemma t_join_adj: "not_T ts \<Longrightarrow> t_join_adj ts \<le> len ts div 2"
|
|
136 |
by(induction ts rule: t_join_adj.induct) auto
|
|
137 |
|
|
138 |
lemma t_join_all: "t_join_all ts \<le> len ts"
|
72121
|
139 |
proof(induction ts rule: join_all.induct)
|
|
140 |
case 1 thus ?case by simp
|
|
141 |
next
|
|
142 |
case (2 t a ts)
|
|
143 |
let ?ts = "TTs t a ts"
|
|
144 |
have "t_join_all ?ts = t_join_adj ?ts + t_join_all (join_adj ?ts)"
|
|
145 |
by simp
|
|
146 |
also have "\<dots> \<le> len ?ts div 2 + t_join_all (join_adj ?ts)"
|
|
147 |
using t_join_adj[of ?ts] by simp
|
|
148 |
also have "\<dots> \<le> len ?ts div 2 + len (join_adj ?ts)"
|
|
149 |
using "2.IH" by simp
|
|
150 |
also have "\<dots> \<le> len ?ts div 2 + len ?ts div 2"
|
|
151 |
using len_join_adj_div2[of ?ts] by simp
|
|
152 |
also have "\<dots> \<le> len ?ts" by linarith
|
|
153 |
finally show ?case .
|
72099
|
154 |
qed
|
|
155 |
|
|
156 |
lemma t_leaves: "t_leaves as = length as + 1"
|
|
157 |
by(induction as) auto
|
|
158 |
|
|
159 |
lemma len_leaves: "len(leaves as) = length as + 1"
|
|
160 |
by(induction as) auto
|
|
161 |
|
|
162 |
lemma t_tree23_of_list: "t_tree23_of_list as \<le> 2*(length as + 1)"
|
|
163 |
using t_join_all[of "leaves as"] by(simp add: t_tree23_of_list_def t_leaves len_leaves)
|
|
164 |
|
|
165 |
end
|