equal
deleted
inserted
replaced
72 |
72 |
73 lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow> |
73 lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow> |
74 ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)" |
74 ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)" |
75 by(induction xs) (auto simp: sorted_lems) |
75 by(induction xs) (auto simp: sorted_lems) |
76 |
76 |
77 lemmas ins_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 |
77 lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 |
78 |
78 |
79 |
79 |
80 subsection \<open>Delete one occurrence of an element from a list:\<close> |
80 subsection \<open>Delete one occurrence of an element from a list:\<close> |
81 |
81 |
82 fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
82 fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
121 "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow> |
121 "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow> |
122 del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) = |
122 del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) = |
123 del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" |
123 del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" |
124 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4) |
124 by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4) |
125 |
125 |
126 lemmas del_simps = sorted_lems |
126 lemmas del_list_simps = sorted_lems |
127 del_list_sorted1 |
127 del_list_sorted1 |
128 del_list_sorted2 |
128 del_list_sorted2 |
129 del_list_sorted3 |
129 del_list_sorted3 |
130 del_list_sorted4 |
130 del_list_sorted4 |
131 del_list_sorted5 |
131 del_list_sorted5 |