--- a/src/HOL/Data_Structures/Binomial_Heap.thy Sun Jun 24 22:13:23 2018 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Mon Jun 25 14:45:05 2018 +0200
@@ -8,7 +8,7 @@
imports
Base_FDS
Complex_Main
- Priority_Queue
+ Priority_Queue_Specs
begin
text \<open>
--- a/src/HOL/Data_Structures/Leftist_Heap.thy Sun Jun 24 22:13:23 2018 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Mon Jun 25 14:45:05 2018 +0200
@@ -6,7 +6,7 @@
imports
Base_FDS
Tree2
- Priority_Queue
+ Priority_Queue_Specs
Complex_Main
begin
--- a/src/HOL/Data_Structures/Map_Specs.thy Sun Jun 24 22:13:23 2018 +0200
+++ b/src/HOL/Data_Structures/Map_Specs.thy Mon Jun 25 14:45:05 2018 +0200
@@ -21,6 +21,9 @@
and invar_update: "invar m \<Longrightarrow> invar(update a b m)"
and invar_delete: "invar m \<Longrightarrow> invar(delete a m)"
+lemmas (in Map) map_specs =
+ map_empty map_update map_delete invar_empty invar_update invar_delete
+
text \<open>The basic map interface with \<open>inorder\<close>-based specification:\<close>
@@ -41,6 +44,7 @@
and inorder_inv_empty: "inv empty"
and inorder_inv_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)"
and inorder_inv_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(delete a t)"
+
begin
text \<open>It implements the traditional specification:\<close>
--- a/src/HOL/Data_Structures/Priority_Queue.thy Sun Jun 24 22:13:23 2018 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* Author: Tobias Nipkow, Peter Lammich *)
-
-section \<open>Priority Queue Interface\<close>
-
-theory Priority_Queue
-imports "HOL-Library.Multiset"
-begin
-
-text \<open>Priority queue interface:\<close>
-
-locale Priority_Queue =
-fixes empty :: "'q"
-and is_empty :: "'q \<Rightarrow> bool"
-and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
-and get_min :: "'q \<Rightarrow> 'a"
-and del_min :: "'q \<Rightarrow> 'q"
-and invar :: "'q \<Rightarrow> bool"
-and mset :: "'q \<Rightarrow> 'a multiset"
-assumes mset_empty: "mset empty = {#}"
-and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
-and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
-and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
- mset (del_min q) = mset q - {# get_min q #}"
-and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
-and invar_empty: "invar empty"
-and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
-and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
-
-text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
-
-locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
-fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
-assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
-and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Priority_Queue_Specs.thy Mon Jun 25 14:45:05 2018 +0200
@@ -0,0 +1,36 @@
+(* Author: Tobias Nipkow, Peter Lammich *)
+
+section \<open>Priority Queue Specifications\<close>
+
+theory Priority_Queue_Specs
+imports "HOL-Library.Multiset"
+begin
+
+text \<open>Priority queue interface + specification:\<close>
+
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> 'a"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> 'a multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+ mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
+
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
+
+end
--- a/src/HOL/Data_Structures/Set_Specs.thy Sun Jun 24 22:13:23 2018 +0200
+++ b/src/HOL/Data_Structures/Set_Specs.thy Mon Jun 25 14:45:05 2018 +0200
@@ -23,6 +23,8 @@
assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
+lemmas (in Set) set_specs =
+ set_empty set_isin set_insert set_delete invar_empty invar_insert invar_delete
text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>
@@ -43,6 +45,7 @@
assumes inorder_inv_empty: "inv empty"
assumes inorder_inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
assumes inorder_inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
+
begin
text \<open>It implements the traditional specification:\<close>