# HG changeset patch
# User nipkow
# Date 1528883605 -7200
# Node ID c8101022e52af153e5dbe2a1af0aca62f7e4f836
# Parent  f04d0e75e439c131e5dc3fe85a54fd5d8fb21e6b
more abstract names

diff -r f04d0e75e439 -r c8101022e52a src/HOL/Data_Structures/Set_Specs.thy
--- a/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 10:52:47 2018 +0200
+++ b/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 11:53:25 2018 +0200
@@ -47,23 +47,29 @@
 
 text \<open>It implements the traditional specification:\<close>
 
+definition set :: "'t \<Rightarrow> 'a set" where
+"set == List.set o inorder"
+
+definition invar :: "'t \<Rightarrow> bool" where
+"invar t == inv t \<and> sorted (inorder t)"
+
 sublocale Set
-  empty insert delete isin "set o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
+  empty insert delete isin set invar
 proof(standard, goal_cases)
-  case 1 show ?case by (auto simp: empty)
+  case 1 show ?case by (auto simp: empty set_def)
 next
-  case 2 thus ?case by(simp add: isin)
+  case 2 thus ?case by(simp add: isin invar_def set_def)
 next
-  case 3 thus ?case by(simp add: insert set_ins_list)
+  case 3 thus ?case by(simp add: insert set_ins_list set_def invar_def)
 next
   case (4 s x) thus ?case
-    using delete[OF 4, of x] by (auto simp: distinct_if_sorted set_del_list_eq)
+    by (auto simp: delete distinct_if_sorted set_del_list_eq invar_def set_def)
 next
-  case 5 thus ?case by(simp add: empty inv_empty)
+  case 5 thus ?case by(simp add: empty inv_empty invar_def)
 next
-  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
+  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list invar_def)
 next
-  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
+  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list invar_def)
 qed
 
 end