# HG changeset patch
# User nipkow
# Date 1449397598 -3600
# Node ID 8dd150a50acc0ad00991333cc7bb7fbecde31efb
# Parent  21502fb1ff0a8c1b8f1b476ba8b0de1dab48af82
tuned

diff -r 21502fb1ff0a -r 8dd150a50acc src/HOL/Data_Structures/Brother12_Map.thy
--- 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
diff -r 21502fb1ff0a -r 8dd150a50acc src/HOL/Data_Structures/Brother12_Set.thy
--- 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