# HG changeset patch
# User nipkow
# Date 1528896260 -7200
# Node ID 6826718f732dfa65da75d45e5d7819ea2abe9e9a
# Parent  c8101022e52af153e5dbe2a1af0aca62f7e4f836
qualify interpretations to avoid clashes

diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/AA_Set.thy
--- a/src/HOL/Data_Structures/AA_Set.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/AA_Set.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -485,7 +485,7 @@
   (auto simp: del_list_simps inorder_adjust pre_adj_if_postL pre_adj_if_postR 
               post_split_max post_delete split_maxD split: prod.splits)
 
-interpretation I: Set_by_Ordered
+interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
 and inorder = inorder and inv = invar
 proof (standard, goal_cases)
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/AVL_Map.thy
--- a/src/HOL/Data_Structures/AVL_Map.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/AVL_Map.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -25,12 +25,12 @@
 
 subsection \<open>Functional Correctness\<close>
 
-theorem inorder_update_avl:
+theorem inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
 by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR)
 
 
-theorem inorder_delete_avl:
+theorem inorder_delete:
   "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
 by(induction t)
   (auto simp: del_list_simps inorder_balL inorder_balR
@@ -180,7 +180,7 @@
 qed simp_all
 
 
-interpretation Map_by_Ordered
+interpretation M: Map_by_Ordered
 where empty = empty and lookup = lookup and update = update and delete = delete
 and inorder = inorder and inv = avl
 proof (standard, goal_cases)
@@ -188,9 +188,9 @@
 next
   case 2 thus ?case by(simp add: lookup_map_of)
 next
-  case 3 thus ?case by(simp add: inorder_update_avl)
+  case 3 thus ?case by(simp add: inorder_update)
 next
-  case 4 thus ?case by(simp add: inorder_delete_avl)
+  case 4 thus ?case by(simp add: inorder_delete)
 next
   case 5 show ?case by (simp add: empty_def)
 next
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -423,7 +423,7 @@
 
 subsection "Overall correctness"
 
-interpretation Set_by_Ordered
+interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
 and inorder = inorder and inv = avl
 proof (standard, goal_cases)
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/RBT_Map.thy
--- a/src/HOL/Data_Structures/RBT_Map.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/RBT_Map.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -42,7 +42,7 @@
 by(induction x y t rule: upd.induct)
   (auto simp: upd_list_simps inorder_baliL inorder_baliR)
 
-lemma inorder_update_rbt:
+lemma inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
 by(simp add: update_def inorder_upd inorder_paint)
 
@@ -51,7 +51,7 @@
 by(induction x t rule: del.induct)
   (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
 
-lemma inorder_delete_rbt:
+lemma inorder_delete:
   "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
 by(simp add: delete_def inorder_del inorder_paint)
 
@@ -104,7 +104,7 @@
 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
 by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
 
-interpretation Map_by_Ordered
+interpretation M: Map_by_Ordered
 where empty = empty and lookup = lookup and update = update and delete = delete
 and inorder = inorder and inv = rbt
 proof (standard, goal_cases)
@@ -112,9 +112,9 @@
 next
   case 2 thus ?case by(simp add: lookup_map_of)
 next
-  case 3 thus ?case by(simp add: inorder_update_rbt)
+  case 3 thus ?case by(simp add: inorder_update)
 next
-  case 4 thus ?case by(simp add: inorder_delete_rbt)
+  case 4 thus ?case by(simp add: inorder_delete)
 next
   case 5 thus ?case by (simp add: rbt_def empty_def) 
 next
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -256,7 +256,7 @@
 
 text \<open>Overall correctness:\<close>
 
-interpretation Set_by_Ordered
+interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
 and inorder = inorder and inv = rbt
 proof (standard, goal_cases)
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Set_Specs.thy
--- a/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Set_Specs.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -33,16 +33,16 @@
 fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
 fixes inorder :: "'t \<Rightarrow> 'a list"
 fixes inv :: "'t \<Rightarrow> bool"
-assumes empty: "inorder empty = []"
+assumes inorder_empty: "inorder empty = []"
 assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
   isin t x = (x \<in> set (inorder t))"
-assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
+assumes inorder_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
   inorder(insert x t) = ins_list x (inorder t)"
-assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
+assumes inorder_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
   inorder(delete x t) = del_list x (inorder 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)"
+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>
@@ -56,20 +56,20 @@
 sublocale Set
   empty insert delete isin set invar
 proof(standard, goal_cases)
-  case 1 show ?case by (auto simp: empty set_def)
+  case 1 show ?case by (auto simp: inorder_empty set_def)
 next
   case 2 thus ?case by(simp add: isin invar_def set_def)
 next
-  case 3 thus ?case by(simp add: insert set_ins_list set_def invar_def)
+  case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def)
 next
   case (4 s x) thus ?case
-    by (auto simp: delete distinct_if_sorted set_del_list_eq invar_def set_def)
+    by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def)
 next
-  case 5 thus ?case by(simp add: empty inv_empty invar_def)
+  case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
 next
-  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list invar_def)
+  case 6 thus ?case by(simp add: inorder_insert inorder_inv_insert sorted_ins_list invar_def)
 next
-  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list invar_def)
+  case 7 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
 qed
 
 end
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree234_Map.thy
--- a/src/HOL/Data_Structures/Tree234_Map.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Map.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -123,7 +123,7 @@
 by(induction t)
   (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits)
 
-lemma inorder_update_234:
+lemma inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
 by(simp add: update_def inorder_upd)
 
@@ -133,7 +133,7 @@
   (auto simp: del_list_simps inorder_nodes split_minD split!: if_splits prod.splits)
 (* 30 secs (2016) *)
 
-lemma inorder_delete_234: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(delete x t) = del_list x (inorder t)"
 by(simp add: delete_def inorder_del)
 
@@ -160,15 +160,15 @@
 
 subsection \<open>Overall Correctness\<close>
 
-interpretation Map_by_Ordered
+interpretation M: Map_by_Ordered
 where empty = empty and lookup = lookup and update = update and delete = delete
 and inorder = inorder and inv = bal
 proof (standard, goal_cases)
   case 2 thus ?case by(simp add: lookup_map_of)
 next
-  case 3 thus ?case by(simp add: inorder_update_234)
+  case 3 thus ?case by(simp add: inorder_update)
 next
-  case 4 thus ?case by(simp add: inorder_delete_234)
+  case 4 thus ?case by(simp add: inorder_delete)
 next
   case 6 thus ?case by(simp add: bal_update)
 next
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree234_Set.thy
--- a/src/HOL/Data_Structures/Tree234_Set.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Set.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -504,7 +504,7 @@
 
 subsection \<open>Overall Correctness\<close>
 
-interpretation Set_by_Ordered
+interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
 and inorder = inorder and inv = bal
 proof (standard, goal_cases)
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree23_Map.thy
--- a/src/HOL/Data_Structures/Tree23_Map.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Tree23_Map.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -81,7 +81,7 @@
   "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)"
 by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
 
-corollary inorder_update_23:
+corollary inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
 by(simp add: update_def inorder_upd)
 
@@ -91,7 +91,7 @@
 by(induction t rule: del.induct)
   (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
 
-corollary inorder_delete_23: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(delete x t) = del_list x (inorder t)"
 by(simp add: delete_def inorder_del)
 
@@ -119,7 +119,7 @@
 
 subsection \<open>Overall Correctness\<close>
 
-interpretation Map_by_Ordered
+interpretation M: Map_by_Ordered
 where empty = empty and lookup = lookup and update = update and delete = delete
 and inorder = inorder and inv = bal
 proof (standard, goal_cases)
@@ -127,9 +127,9 @@
 next
   case 2 thus ?case by(simp add: lookup_map_of)
 next
-  case 3 thus ?case by(simp add: inorder_update_23)
+  case 3 thus ?case by(simp add: inorder_update)
 next
-  case 4 thus ?case by(simp add: inorder_delete_23)
+  case 4 thus ?case by(simp add: inorder_delete)
 next
   case 5 thus ?case by(simp add: empty_def)
 next
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -379,7 +379,7 @@
 
 subsection \<open>Overall Correctness\<close>
 
-interpretation Set_by_Ordered
+interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
 and inorder = inorder and inv = bal
 proof (standard, goal_cases)
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree_Map.thy
--- a/src/HOL/Data_Structures/Tree_Map.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -34,15 +34,15 @@
   "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
 by (induction t) (auto simp: map_of_simps split: option.split)
 
-lemma inorder_update_tree:
+lemma inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
 by(induction t) (auto simp: upd_list_simps)
 
-lemma inorder_delete_tree:
+lemma inorder_delete:
   "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
 by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
 
-interpretation Map_by_Ordered
+interpretation M: Map_by_Ordered
 where empty = empty and lookup = lookup and update = update and delete = delete
 and inorder = inorder and inv = "\<lambda>_. True"
 proof (standard, goal_cases)
@@ -50,9 +50,9 @@
 next
   case 2 thus ?case by(simp add: lookup_map_of)
 next
-  case 3 thus ?case by(simp add: inorder_update_tree)
+  case 3 thus ?case by(simp add: inorder_update)
 next
-  case 4 thus ?case by(simp add: inorder_delete_tree)
+  case 4 thus ?case by(simp add: inorder_delete)
 qed auto
 
 end
diff -r c8101022e52a -r 6826718f732d src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Wed Jun 13 15:24:20 2018 +0200
@@ -62,7 +62,7 @@
   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
 by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
 
-interpretation Set_by_Ordered
+interpretation S: Set_by_Ordered
 where empty = empty and isin = isin and insert = insert and delete = delete
 and inorder = inorder and inv = "\<lambda>_. True"
 proof (standard, goal_cases)