equal
deleted
inserted
replaced
28 fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where |
28 fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where |
29 "del_list x [] = []" | |
29 "del_list x [] = []" | |
30 "del_list x ((a,b)#ps) = (if x = a then ps else (a,b) # del_list x ps)" |
30 "del_list x ((a,b)#ps) = (if x = a then ps else (a,b) # del_list x ps)" |
31 |
31 |
32 |
32 |
33 subsection \<open>Lemmas for @{const map_of}\<close> |
33 subsection \<open>Lemmas for \<^const>\<open>map_of\<close>\<close> |
34 |
34 |
35 lemma map_of_ins_list: "map_of (upd_list x y ps) = (map_of ps)(x := Some y)" |
35 lemma map_of_ins_list: "map_of (upd_list x y ps) = (map_of ps)(x := Some y)" |
36 by(induction ps) auto |
36 by(induction ps) auto |
37 |
37 |
38 lemma map_of_append: "map_of (ps @ qs) x = |
38 lemma map_of_append: "map_of (ps @ qs) x = |
59 |
59 |
60 lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc |
60 lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc |
61 lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds |
61 lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds |
62 |
62 |
63 |
63 |
64 subsection \<open>Lemmas for @{const upd_list}\<close> |
64 subsection \<open>Lemmas for \<^const>\<open>upd_list\<close>\<close> |
65 |
65 |
66 lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list x y ps)" |
66 lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list x y ps)" |
67 apply(induction ps) |
67 apply(induction ps) |
68 apply simp |
68 apply simp |
69 apply(case_tac ps) |
69 apply(case_tac ps) |
87 upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)" |
87 upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)" |
88 by (auto simp: upd_list_sorted) |
88 by (auto simp: upd_list_sorted) |
89 |
89 |
90 lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2 |
90 lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2 |
91 |
91 |
92 text\<open>Splay trees need two additional @{const upd_list} lemmas:\<close> |
92 text\<open>Splay trees need two additional \<^const>\<open>upd_list\<close> lemmas:\<close> |
93 |
93 |
94 lemma upd_list_Cons: |
94 lemma upd_list_Cons: |
95 "sorted1 ((x,y) # xs) \<Longrightarrow> upd_list x y xs = (x,y) # xs" |
95 "sorted1 ((x,y) # xs) \<Longrightarrow> upd_list x y xs = (x,y) # xs" |
96 by (induction xs) auto |
96 by (induction xs) auto |
97 |
97 |
98 lemma upd_list_snoc: |
98 lemma upd_list_snoc: |
99 "sorted1 (xs @ [(x,y)]) \<Longrightarrow> upd_list x y xs = xs @ [(x,y)]" |
99 "sorted1 (xs @ [(x,y)]) \<Longrightarrow> upd_list x y xs = xs @ [(x,y)]" |
100 by(induction xs) (auto simp add: sorted_mid_iff2) |
100 by(induction xs) (auto simp add: sorted_mid_iff2) |
101 |
101 |
102 |
102 |
103 subsection \<open>Lemmas for @{const del_list}\<close> |
103 subsection \<open>Lemmas for \<^const>\<open>del_list\<close>\<close> |
104 |
104 |
105 lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)" |
105 lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)" |
106 apply(induction ps) |
106 apply(induction ps) |
107 apply simp |
107 apply simp |
108 apply(case_tac ps) |
108 apply(case_tac ps) |
151 del_list_sorted2 |
151 del_list_sorted2 |
152 del_list_sorted3 |
152 del_list_sorted3 |
153 del_list_sorted4 |
153 del_list_sorted4 |
154 del_list_sorted5 |
154 del_list_sorted5 |
155 |
155 |
156 text\<open>Splay trees need two additional @{const del_list} lemmas:\<close> |
156 text\<open>Splay trees need two additional \<^const>\<open>del_list\<close> lemmas:\<close> |
157 |
157 |
158 lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs" |
158 lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs" |
159 by(induction xs)(fastforce simp: sorted_wrt_Cons)+ |
159 by(induction xs)(fastforce simp: sorted_wrt_Cons)+ |
160 |
160 |
161 lemma del_list_sorted_app: |
161 lemma del_list_sorted_app: |