# HG changeset patch
# User haftmann
# Date 1284389003 -7200
# Node ID 5a2662c1e44a3fdeab1f9583075586f5f581e956
# Parent  ab1b070aa412ab5082e53bb9a6e250c1b7c8b0b9
established emerging canonical names *_eqI and *_eq_iff

diff -r ab1b070aa412 -r 5a2662c1e44a src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Mon Sep 13 16:43:23 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Mon Sep 13 16:43:23 2010 +0200
@@ -14,18 +14,20 @@
   show "[] \<in> ?dlist" by simp
 qed
 
-lemma dlist_ext:
-  assumes "list_of_dlist dxs = list_of_dlist dys"
-  shows "dxs = dys"
-  using assms by (simp add: list_of_dlist_inject)
+lemma dlist_eq_iff:
+  "dxs = dys \<longleftrightarrow> list_of_dlist dxs = list_of_dlist dys"
+  by (simp add: list_of_dlist_inject)
 
+lemma dlist_eqI:
+  "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys"
+  by (simp add: dlist_eq_iff)
 
 text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
 
 definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
   "Dlist xs = Abs_dlist (remdups xs)"
 
-lemma distinct_list_of_dlist [simp]:
+lemma distinct_list_of_dlist [simp, intro]:
   "distinct (list_of_dlist dxs)"
   using list_of_dlist [of dxs] by simp
 
diff -r ab1b070aa412 -r 5a2662c1e44a src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Mon Sep 13 16:43:23 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Mon Sep 13 16:43:23 2010 +0200
@@ -20,15 +20,17 @@
   "Fset (member A) = A"
   by (fact member_inverse)
 
-declare member_inject [simp]
-
 lemma Fset_inject [simp]:
   "Fset A = Fset B \<longleftrightarrow> A = B"
   by (simp add: Fset_inject)
 
+lemma fset_eq_iff:
+  "A = B \<longleftrightarrow> member A = member B"
+  by (simp add: member_inject)
+
 lemma fset_eqI:
   "member A = member B \<Longrightarrow> A = B"
-  by simp
+  by (simp add: fset_eq_iff)
 
 declare mem_def [simp]
 
@@ -116,7 +118,7 @@
   [simp]: "A - B = Fset (member A - member B)"
 
 instance proof
-qed auto
+qed (auto intro: fset_eqI)
 
 end
 
@@ -234,7 +236,7 @@
   "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
 
 instance proof
-qed (simp add: equal_fset_def set_eq [symmetric])
+qed (simp add: equal_fset_def set_eq [symmetric] fset_eq_iff)
 
 end
 
diff -r ab1b070aa412 -r 5a2662c1e44a src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Mon Sep 13 16:43:23 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Mon Sep 13 16:43:23 2010 +0200
@@ -19,16 +19,17 @@
   "Mapping (lookup m) = m"
   by (fact lookup_inverse)
 
-declare lookup_inject [simp]
-
 lemma Mapping_inject [simp]:
   "Mapping f = Mapping g \<longleftrightarrow> f = g"
   by (simp add: Mapping_inject)
 
+lemma mapping_eq_iff:
+  "m = n \<longleftrightarrow> lookup m = lookup n"
+  by (simp add: lookup_inject)
+
 lemma mapping_eqI:
-  assumes "lookup m = lookup n"
-  shows "m = n"
-  using assms by simp
+  "lookup m = lookup n \<Longrightarrow> m = n"
+  by (simp add: mapping_eq_iff)
 
 definition empty :: "('a, 'b) mapping" where
   "empty = Mapping (\<lambda>_. None)"
@@ -287,7 +288,7 @@
   "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
 
 instance proof
-qed (simp add: equal_mapping_def)
+qed (simp add: equal_mapping_def mapping_eq_iff)
 
 end
 
diff -r ab1b070aa412 -r 5a2662c1e44a src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Mon Sep 13 16:43:23 2010 +0200
+++ b/src/HOL/Library/RBT.thy	Mon Sep 13 16:43:23 2010 +0200
@@ -16,15 +16,19 @@
   then show ?thesis ..
 qed
 
+lemma rbt_eq_iff:
+  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
+  by (simp add: impl_of_inject)
+
+lemma rbt_eqI:
+  "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
+  by (simp add: rbt_eq_iff)
+
 lemma is_rbt_impl_of [simp, intro]:
   "is_rbt (impl_of t)"
   using impl_of [of t] by simp
 
-lemma rbt_eq:
-  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
-  by (simp add: impl_of_inject)
-
-lemma [code abstype]:
+lemma RBT_impl_of [simp, code abstype]:
   "RBT (impl_of t) = t"
   by (simp add: impl_of_inverse)
 
@@ -148,7 +152,7 @@
 
 lemma is_empty_empty [simp]:
   "is_empty t \<longleftrightarrow> t = empty"
-  by (simp add: rbt_eq is_empty_def impl_of_empty split: rbt.split)
+  by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
 
 lemma RBT_lookup_empty [simp]: (*FIXME*)
   "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
@@ -184,7 +188,7 @@
 
 lemma is_empty_Mapping [code]:
   "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
-  by (simp add: rbt_eq Mapping.is_empty_empty Mapping_def)
+  by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def)
 
 lemma insert_Mapping [code]:
   "Mapping.update k v (Mapping t) = Mapping (insert k v t)"