author nipkow Sun, 06 Dec 2015 11:26:38 +0100 changeset 61792 8dd150a50acc parent 61791 21502fb1ff0a child 61793 4c9e1e5a240e
tuned
```--- a/src/HOL/Data_Structures/Brother12_Map.thy	Sat Dec 05 17:23:50 2015 +0100
+++ b/src/HOL/Data_Structures/Brother12_Map.thy	Sun Dec 06 11:26:38 2015 +0100
@@ -82,10 +82,13 @@
begin

lemma inorder_del:
-  "t \<in> B h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
-  "t \<in> U h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
-by(induction h arbitrary: t)
-  (auto simp: del_list_simps inorder_n2 inorder_del_min split: option.splits)
+  "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
+by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
+     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
+
+lemma inorder_delete:
+  "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
+by(simp add: delete_def inorder_del inorder_tree)

end

@@ -199,8 +202,7 @@
next
case 3 thus ?case by(auto intro!: update.inorder_update)
next
-  case 4 thus ?case
-    by(auto simp: delete.delete_def delete.inorder_tree delete.inorder_del)
+  case 4 thus ?case by(auto intro!: delete.inorder_delete)
next
case 6 thus ?case using update.update_type by (metis Un_iff)
next```
```--- a/src/HOL/Data_Structures/Brother12_Set.thy	Sat Dec 05 17:23:50 2015 +0100
+++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sun Dec 06 11:26:38 2015 +0100
@@ -193,17 +193,18 @@
by(induction l a r rule: n2.induct) (auto)

lemma inorder_del_min:
-shows "t \<in> B h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
-  (del_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
-and "t \<in> U h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
+  "t \<in> T h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
(del_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)

lemma inorder_del:
-  "t \<in> B h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del a t) = del_list a (inorder t)"
-  "t \<in> U h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del a t) = del_list a (inorder t)"
-by(induction h arbitrary: t)
-  (auto simp: del_list_simps inorder_n2 inorder_del_min split: option.splits)
+  "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
+by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
+     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
+
+lemma inorder_delete:
+  "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
+by(simp add: delete_def inorder_del inorder_tree)

end

@@ -481,8 +482,7 @@
next
case 3 thus ?case by(auto intro!: insert.inorder_insert)
next
-  case 4 thus ?case
-    by(auto simp: delete.delete_def delete.inorder_tree delete.inorder_del)
+  case 4 thus ?case by(auto intro!: delete.inorder_delete)
next
case 6 thus ?case using insert.insert_type by blast
next```