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