author nipkow Thu, 29 Aug 2019 19:07:00 +0200 changeset 70631 f14b997da756 parent 70629 2bbd945728e2 child 70632 f54b19ca9994
simplified proofs
```--- 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```