equal
deleted
inserted
replaced
78 upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)" |
78 upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)" |
79 by(induction ps) (auto simp: sorted_lems) |
79 by(induction ps) (auto simp: sorted_lems) |
80 |
80 |
81 lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2 |
81 lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2 |
82 |
82 |
83 (* |
|
84 lemma set_ins_list[simp]: "set (ins_list x xs) = insert x (set xs)" |
|
85 by(induction xs) auto |
|
86 |
|
87 lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs" |
|
88 apply(induction xs rule: sorted.induct) |
|
89 apply auto |
|
90 by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2) |
|
91 |
|
92 lemma set_del_list_eq [simp]: "distinct xs ==> set(del_list x xs) = set xs - {x}" |
|
93 apply(induct xs) |
|
94 apply simp |
|
95 apply simp |
|
96 apply blast |
|
97 done |
|
98 *) |
|
99 |
|
100 |
83 |
101 subsection \<open>Lemmas for @{const del_list}\<close> |
84 subsection \<open>Lemmas for @{const del_list}\<close> |
102 |
85 |
103 lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)" |
86 lemma sorted_del_list: "sorted1 ps \<Longrightarrow> sorted1 (del_list x ps)" |
104 apply(induction ps) |
87 apply(induction ps) |