--- a/src/HOL/Data_Structures/List_Ins_Del.thy Thu Aug 29 14:20:46 2019 +0200
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy Thu Aug 29 19:07:00 2019 +0200
@@ -40,14 +40,9 @@
"ins_list x (a#xs) =
(if x < a then x#a#xs else if x=a then a#xs else a # ins_list x xs)"
-lemma set_ins_list: "set (ins_list x xs) = insert x (set xs)"
+lemma set_ins_list: "set (ins_list x xs) = set xs \<union> {x}"
by(induction xs) auto
-lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
-apply(induction xs rule: induct_list012)
-apply auto
-by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
-
lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
by(induction xs rule: induct_list012) auto
@@ -87,9 +82,9 @@
lemma del_list_idem: "x \<notin> set xs \<Longrightarrow> del_list x xs = xs"
by (induct xs) simp_all
-lemma set_del_list_eq:
- "distinct xs \<Longrightarrow> set (del_list x xs) = set xs - {x}"
-by(induct xs) auto
+lemma set_del_list:
+ "sorted xs \<Longrightarrow> set (del_list x xs) = set xs - {x}"
+by(induct xs) (auto simp: sorted_Cons_iff)
lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
apply(induction xs rule: induct_list012)
--- a/src/HOL/Data_Structures/Set_Specs.thy Thu Aug 29 14:20:46 2019 +0200
+++ b/src/HOL/Data_Structures/Set_Specs.thy Thu Aug 29 19:07:00 2019 +0200
@@ -66,7 +66,7 @@
case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def)
next
case (4 s x) thus ?case
- by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def)
+ by (auto simp: inorder_delete set_del_list invar_def set_def)
next
case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
next