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