# HG changeset patch
# User nipkow
# Date 1529930705 -7200
# Node ID c7e0a7bcacaf8894724f711ea392877d0ad34c43
# Parent  f0f83ce0badd797fed176e5e385949e65114a74a
added lemmas; uniform names

diff -r f0f83ce0badd -r c7e0a7bcacaf src/HOL/Data_Structures/Binomial_Heap.thy
--- 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>
diff -r f0f83ce0badd -r c7e0a7bcacaf src/HOL/Data_Structures/Leftist_Heap.thy
--- 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
 
diff -r f0f83ce0badd -r c7e0a7bcacaf src/HOL/Data_Structures/Map_Specs.thy
--- 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>
diff -r f0f83ce0badd -r c7e0a7bcacaf src/HOL/Data_Structures/Priority_Queue.thy
--- 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
diff -r f0f83ce0badd -r c7e0a7bcacaf src/HOL/Data_Structures/Priority_Queue_Specs.thy
--- /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
diff -r f0f83ce0badd -r c7e0a7bcacaf src/HOL/Data_Structures/Set_Specs.thy
--- 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>