equal
deleted
inserted
replaced
67 ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)" |
67 ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)" |
68 by(auto simp: ins_list_sorted) |
68 by(auto simp: ins_list_sorted) |
69 |
69 |
70 lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 |
70 lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 |
71 |
71 |
72 text\<open>Splay trees need two additional @{const ins_list} lemmas:\<close> |
72 text\<open>Splay trees need two additional \<^const>\<open>ins_list\<close> lemmas:\<close> |
73 |
73 |
74 lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs" |
74 lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs" |
75 by (induction xs) auto |
75 by (induction xs) auto |
76 |
76 |
77 lemma ins_list_snoc: "sorted (xs @ [x]) \<Longrightarrow> ins_list x xs = xs @ [x]" |
77 lemma ins_list_snoc: "sorted (xs @ [x]) \<Longrightarrow> ins_list x xs = xs @ [x]" |
133 del_list_sorted2 |
133 del_list_sorted2 |
134 del_list_sorted3 |
134 del_list_sorted3 |
135 del_list_sorted4 |
135 del_list_sorted4 |
136 del_list_sorted5 |
136 del_list_sorted5 |
137 |
137 |
138 text\<open>Splay trees need two additional @{const del_list} lemmas:\<close> |
138 text\<open>Splay trees need two additional \<^const>\<open>del_list\<close> lemmas:\<close> |
139 |
139 |
140 lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs" |
140 lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs" |
141 by(induction xs)(fastforce simp: sorted_Cons_iff)+ |
141 by(induction xs)(fastforce simp: sorted_Cons_iff)+ |
142 |
142 |
143 lemma del_list_sorted_app: |
143 lemma del_list_sorted_app: |