# HG changeset patch
# User nipkow
# Date 1567098429 -7200
# Node ID f54b19ca9994a986fc5c6d8fe2ea2c056055926d
# Parent  2402aa499ffe8a9b2d86c30e3feb6c2ee8c3fec7# Parent  f14b997da756bd313ebfa8567551d87a86db0ab5
merged

diff -r 2402aa499ffe -r f54b19ca9994 src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Thu Aug 29 12:59:10 2019 +0000
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Thu Aug 29 19:07:09 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)
diff -r 2402aa499ffe -r f54b19ca9994 src/HOL/Data_Structures/Set_Specs.thy
--- a/src/HOL/Data_Structures/Set_Specs.thy	Thu Aug 29 12:59:10 2019 +0000
+++ b/src/HOL/Data_Structures/Set_Specs.thy	Thu Aug 29 19:07:09 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