--- 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 *}
--- 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
--- 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
--- 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
--- 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