# HG changeset patch
# User nipkow
# Date 1444748797 -7200
# Node ID 5e19381073712b8f4209224887f8c05124f12ccf
# Parent  3c69ea85f8dd4667525d27efafd5680ccc20ab32
added invar empty

diff -r 3c69ea85f8dd -r 5e1938107371 src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Tue Oct 13 14:49:15 2015 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue Oct 13 17:06:37 2015 +0200
@@ -130,9 +130,7 @@
   case 3 thus ?case by(simp add: inorder_insert)
 next
   case 4 thus ?case by(simp add: inorder_delete)
-next
-  case 5 thus ?case ..
-qed
+qed (rule TrueI)+
 
 
 subsection {* AVL invariants *}
diff -r 3c69ea85f8dd -r 5e1938107371 src/HOL/Data_Structures/Map_by_Ordered.thy
--- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Tue Oct 13 14:49:15 2015 +0100
+++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Tue Oct 13 17:06:37 2015 +0200
@@ -15,6 +15,7 @@
 assumes "map_of empty = (\<lambda>_. None)"
 assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
 assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
+assumes "invar empty"
 assumes "invar m \<Longrightarrow> invar(update a b m)"
 assumes "invar m \<Longrightarrow> invar(delete a m)"
 
@@ -32,6 +33,7 @@
   inorder(update a b t) = upd_list a b (inorder t)"
 assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
   inorder(delete a t) = del_list a (inorder t)"
+assumes wf_empty:  "wf empty"
 assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)"
 assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)"
 begin
@@ -45,9 +47,11 @@
 next
   case 3 thus ?case by(simp add: delete map_of_del_list)
 next
-  case 4 thus ?case by(simp add: update wf_insert sorted_upd_list)
+  case 4 thus ?case by(simp add: empty wf_empty)
 next
-  case 5 thus ?case by (auto simp: delete wf_delete sorted_del_list)
+  case 5 thus ?case by(simp add: update wf_insert sorted_upd_list)
+next
+  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
 qed
 
 end
diff -r 3c69ea85f8dd -r 5e1938107371 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Oct 13 14:49:15 2015 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Tue Oct 13 17:06:37 2015 +0200
@@ -77,8 +77,6 @@
   case 3 thus ?case by(simp add: inorder_insert)
 next
   case 4 thus ?case by(simp add: inorder_delete)
-next
-  case 5 thus ?case ..
-qed
+qed (rule TrueI)+
 
 end
diff -r 3c69ea85f8dd -r 5e1938107371 src/HOL/Data_Structures/Set_by_Ordered.thy
--- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Tue Oct 13 14:49:15 2015 +0100
+++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Tue Oct 13 17:06:37 2015 +0200
@@ -17,6 +17,7 @@
 assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)"
 assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)"
 assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}"
+assumes "invar empty"
 assumes "invar s \<Longrightarrow> invar(insert a s)"
 assumes "invar s \<Longrightarrow> invar(delete a s)"
 
@@ -34,6 +35,7 @@
   inorder(insert a t) = ins_list a (inorder t)"
 assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
   inorder(delete a t) = del_list a (inorder t)"
+assumes wf_empty:  "wf empty"
 assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)"
 assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)"
 begin
@@ -50,9 +52,11 @@
   case (4 s a) show ?case
     using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted)
 next
-  case 5 thus ?case by(simp add: insert wf_insert sorted_ins_list)
+  case 5 thus ?case by(simp add: empty wf_empty)
 next
-  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
+  case 6 thus ?case by(simp add: insert wf_insert sorted_ins_list)
+next
+  case 7 thus ?case by (auto simp: delete wf_delete sorted_del_list)
 qed
 
 end
diff -r 3c69ea85f8dd -r 5e1938107371 src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Tue Oct 13 14:49:15 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Tue Oct 13 17:06:37 2015 +0200
@@ -68,8 +68,6 @@
   case 3 thus ?case by(simp add: inorder_insert)
 next
   case 4 thus ?case by(simp add: inorder_delete)
-next
-  case 5 thus ?case by(simp)
-qed
+qed (rule TrueI)+
 
 end