--- a/src/HOL/Data_Structures/List_Ins_Del.thy Thu Nov 05 18:38:08 2015 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy Fri Nov 06 14:43:05 2015 +0100
@@ -55,7 +55,7 @@
"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[simp]: "elems (ins_list x xs) = insert x (elems xs)"
+lemma set_ins_list: "elems (ins_list x xs) = insert x (elems xs)"
by(induction xs) auto
lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
@@ -86,7 +86,7 @@
lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs"
by (induct xs) simp_all
-lemma elems_del_list_eq [simp]:
+lemma elems_del_list_eq:
"distinct xs \<Longrightarrow> elems (del_list x xs) = elems xs - {x}"
apply(induct xs)
apply simp
--- a/src/HOL/Data_Structures/Set_by_Ordered.thy Thu Nov 05 18:38:08 2015 +0100
+++ b/src/HOL/Data_Structures/Set_by_Ordered.thy Fri Nov 06 14:43:05 2015 +0100
@@ -47,10 +47,10 @@
next
case 2 thus ?case by(simp add: isin)
next
- case 3 thus ?case by(simp add: insert)
+ case 3 thus ?case by(simp add: insert set_ins_list)
next
- case (4 s x) show ?case
- using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted)
+ case (4 s x) thus ?case
+ using delete[OF 4, of x] by (auto simp: distinct_if_sorted elems_del_list_eq)
next
case 5 thus ?case by(simp add: empty inv_empty)
next