# HG changeset patch # User nipkow # Date 1447252861 -3600 # Node ID 6059ce322766f270b3d2d6c5a22fac574df70a5a # Parent c304402cc3df3699a290c2f764ffc3701faa9f41 tuned diff -r c304402cc3df -r 6059ce322766 src/HOL/Data_Structures/Splay_Set.thy --- a/src/HOL/Data_Structures/Splay_Set.thy Tue Nov 10 23:41:20 2015 +0100 +++ b/src/HOL/Data_Structures/Splay_Set.thy Wed Nov 11 15:41:01 2015 +0100 @@ -136,7 +136,7 @@ subsubsection "Proofs for insert" -(* more sorted lemmas; unify with basic set? *) +text\Splay trees need two addition @{const sorted} lemmas:\ lemma sorted_snoc_le: "ASSUMPTION(sorted(xs @ [x])) \ x \ y \ 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\Splay trees need two addition @{const ins_list} lemmas:\ + lemma ins_list_Cons: "sorted (x # xs) \ 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\Splay trees need two addition @{const del_list} lemmas:\ lemma del_list_notin_Cons: "sorted (x # xs) \ del_list x xs = xs" by(induction xs)(auto simp: sorted_Cons_iff)