# HG changeset patch
# User nipkow
# Date 1446745088 -3600
# Node ID 1d2907d0ed73dff4718af177572b959ee8e48c6b
# Parent  c3974cd2d381dd317f2bd9a3a671816393e09e54
tuned

diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -119,7 +119,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and wf = "\<lambda>_. True"
+and inorder = inorder and inv = "\<lambda>_. True"
 proof (standard, goal_cases)
   case 1 show ?case by simp
 next
diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -73,7 +73,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and wf = "\<lambda>_. True"
+and inorder = inorder and inv = "\<lambda>_. True"
 proof (standard, goal_cases)
   case 1 show ?case by simp
 next
diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Set_by_Ordered.thy
--- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -27,21 +27,21 @@
 fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
 fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
 fixes inorder :: "'t \<Rightarrow> 'a list"
-fixes wf :: "'t \<Rightarrow> bool"
+fixes inv :: "'t \<Rightarrow> bool"
 assumes empty: "inorder empty = []"
-assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow>
+assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
   isin t x = (x \<in> elems (inorder t))"
-assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow>
+assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
   inorder(insert x t) = ins_list x (inorder t)"
-assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
+assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
   inorder(delete x t) = del_list x (inorder t)"
-assumes wf_empty:  "wf empty"
-assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert x t)"
-assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete x t)"
+assumes inv_empty:  "inv empty"
+assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
+assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
 begin
 
 sublocale Set
-  empty insert delete isin "elems o inorder" "\<lambda>t. wf t \<and> sorted(inorder t)"
+  empty insert delete isin "elems o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
 proof(standard, goal_cases)
   case 1 show ?case by (auto simp: empty)
 next
@@ -52,11 +52,11 @@
   case (4 s x) show ?case
     using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted)
 next
-  case 5 thus ?case by(simp add: empty wf_empty)
+  case 5 thus ?case by(simp add: empty inv_empty)
 next
-  case 6 thus ?case by(simp add: insert wf_insert sorted_ins_list)
+  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
 next
-  case 7 thus ?case by (auto simp: delete wf_delete sorted_del_list)
+  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
 qed
 
 end
diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Splay_Set.thy
--- a/src/HOL/Data_Structures/Splay_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -198,7 +198,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert
-and delete = delete and inorder = inorder and wf = "\<lambda>_. True"
+and delete = delete and inorder = inorder and inv = "\<lambda>_. True"
 proof (standard, goal_cases)
   case 2 thus ?case by(simp add: isin_set)
 next
diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Tree234_Set.thy
--- a/src/HOL/Data_Structures/Tree234_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/Tree234_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -497,7 +497,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and wf = bal
+and inorder = inorder and inv = bal
 proof (standard, goal_cases)
   case 2 thus ?case by(simp add: isin_set)
 next
diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -356,7 +356,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and wf = bal
+and inorder = inorder and inv = bal
 proof (standard, goal_cases)
   case 2 thus ?case by(simp add: isin_set)
 next
diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -61,7 +61,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and wf = "\<lambda>_. True"
+and inorder = inorder and inv = "\<lambda>_. True"
 proof (standard, goal_cases)
   case 1 show ?case by simp
 next