--- a/src/HOL/Data_Structures/Splay_Set.thy Wed Nov 11 12:57:01 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Set.thy Wed Nov 11 16:39:23 2015 +0100
@@ -136,7 +136,7 @@
subsubsection "Proofs for insert"
-(* more sorted lemmas; unify with basic set? *)
+text\<open>Splay trees need two addition @{const sorted} lemmas:\<close>
lemma sorted_snoc_le:
"ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
@@ -157,6 +157,8 @@
by(induction x t arbitrary: l a r rule: splay.induct)
(auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits)
+text\<open>Splay trees need two addition @{const ins_list} lemmas:\<close>
+
lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs"
by (induction xs) auto
@@ -171,7 +173,7 @@
subsubsection "Proofs for delete"
-(* more del_simp lemmas; unify with basic set? *)
+text\<open>Splay trees need two addition @{const del_list} lemmas:\<close>
lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs"
by(induction xs)(auto simp: sorted_Cons_iff)