--- 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)
--- 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
--- 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)
--- 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
--- 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)
--- 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
--- 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
--- 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)
--- 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
--- 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)
--- 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
--- 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)