established emerging canonical names *_eqI and *_eq_iff
authorhaftmann
Mon Sep 13 16:43:23 2010 +0200 (2010-09-13)
changeset 393805a2662c1e44a
parent 39379 ab1b070aa412
child 39381 9717ea8d42b3
established emerging canonical names *_eqI and *_eq_iff
src/HOL/Library/Dlist.thy
src/HOL/Library/Fset.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/RBT.thy
     1.1 --- a/src/HOL/Library/Dlist.thy	Mon Sep 13 16:43:23 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Sep 13 16:43:23 2010 +0200
     1.3 @@ -14,18 +14,20 @@
     1.4    show "[] \<in> ?dlist" by simp
     1.5  qed
     1.6  
     1.7 -lemma dlist_ext:
     1.8 -  assumes "list_of_dlist dxs = list_of_dlist dys"
     1.9 -  shows "dxs = dys"
    1.10 -  using assms by (simp add: list_of_dlist_inject)
    1.11 +lemma dlist_eq_iff:
    1.12 +  "dxs = dys \<longleftrightarrow> list_of_dlist dxs = list_of_dlist dys"
    1.13 +  by (simp add: list_of_dlist_inject)
    1.14  
    1.15 +lemma dlist_eqI:
    1.16 +  "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys"
    1.17 +  by (simp add: dlist_eq_iff)
    1.18  
    1.19  text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
    1.20  
    1.21  definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
    1.22    "Dlist xs = Abs_dlist (remdups xs)"
    1.23  
    1.24 -lemma distinct_list_of_dlist [simp]:
    1.25 +lemma distinct_list_of_dlist [simp, intro]:
    1.26    "distinct (list_of_dlist dxs)"
    1.27    using list_of_dlist [of dxs] by simp
    1.28  
     2.1 --- a/src/HOL/Library/Fset.thy	Mon Sep 13 16:43:23 2010 +0200
     2.2 +++ b/src/HOL/Library/Fset.thy	Mon Sep 13 16:43:23 2010 +0200
     2.3 @@ -20,15 +20,17 @@
     2.4    "Fset (member A) = A"
     2.5    by (fact member_inverse)
     2.6  
     2.7 -declare member_inject [simp]
     2.8 -
     2.9  lemma Fset_inject [simp]:
    2.10    "Fset A = Fset B \<longleftrightarrow> A = B"
    2.11    by (simp add: Fset_inject)
    2.12  
    2.13 +lemma fset_eq_iff:
    2.14 +  "A = B \<longleftrightarrow> member A = member B"
    2.15 +  by (simp add: member_inject)
    2.16 +
    2.17  lemma fset_eqI:
    2.18    "member A = member B \<Longrightarrow> A = B"
    2.19 -  by simp
    2.20 +  by (simp add: fset_eq_iff)
    2.21  
    2.22  declare mem_def [simp]
    2.23  
    2.24 @@ -116,7 +118,7 @@
    2.25    [simp]: "A - B = Fset (member A - member B)"
    2.26  
    2.27  instance proof
    2.28 -qed auto
    2.29 +qed (auto intro: fset_eqI)
    2.30  
    2.31  end
    2.32  
    2.33 @@ -234,7 +236,7 @@
    2.34    "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
    2.35  
    2.36  instance proof
    2.37 -qed (simp add: equal_fset_def set_eq [symmetric])
    2.38 +qed (simp add: equal_fset_def set_eq [symmetric] fset_eq_iff)
    2.39  
    2.40  end
    2.41  
     3.1 --- a/src/HOL/Library/Mapping.thy	Mon Sep 13 16:43:23 2010 +0200
     3.2 +++ b/src/HOL/Library/Mapping.thy	Mon Sep 13 16:43:23 2010 +0200
     3.3 @@ -19,16 +19,17 @@
     3.4    "Mapping (lookup m) = m"
     3.5    by (fact lookup_inverse)
     3.6  
     3.7 -declare lookup_inject [simp]
     3.8 -
     3.9  lemma Mapping_inject [simp]:
    3.10    "Mapping f = Mapping g \<longleftrightarrow> f = g"
    3.11    by (simp add: Mapping_inject)
    3.12  
    3.13 +lemma mapping_eq_iff:
    3.14 +  "m = n \<longleftrightarrow> lookup m = lookup n"
    3.15 +  by (simp add: lookup_inject)
    3.16 +
    3.17  lemma mapping_eqI:
    3.18 -  assumes "lookup m = lookup n"
    3.19 -  shows "m = n"
    3.20 -  using assms by simp
    3.21 +  "lookup m = lookup n \<Longrightarrow> m = n"
    3.22 +  by (simp add: mapping_eq_iff)
    3.23  
    3.24  definition empty :: "('a, 'b) mapping" where
    3.25    "empty = Mapping (\<lambda>_. None)"
    3.26 @@ -287,7 +288,7 @@
    3.27    "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
    3.28  
    3.29  instance proof
    3.30 -qed (simp add: equal_mapping_def)
    3.31 +qed (simp add: equal_mapping_def mapping_eq_iff)
    3.32  
    3.33  end
    3.34  
     4.1 --- a/src/HOL/Library/RBT.thy	Mon Sep 13 16:43:23 2010 +0200
     4.2 +++ b/src/HOL/Library/RBT.thy	Mon Sep 13 16:43:23 2010 +0200
     4.3 @@ -16,15 +16,19 @@
     4.4    then show ?thesis ..
     4.5  qed
     4.6  
     4.7 +lemma rbt_eq_iff:
     4.8 +  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
     4.9 +  by (simp add: impl_of_inject)
    4.10 +
    4.11 +lemma rbt_eqI:
    4.12 +  "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
    4.13 +  by (simp add: rbt_eq_iff)
    4.14 +
    4.15  lemma is_rbt_impl_of [simp, intro]:
    4.16    "is_rbt (impl_of t)"
    4.17    using impl_of [of t] by simp
    4.18  
    4.19 -lemma rbt_eq:
    4.20 -  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
    4.21 -  by (simp add: impl_of_inject)
    4.22 -
    4.23 -lemma [code abstype]:
    4.24 +lemma RBT_impl_of [simp, code abstype]:
    4.25    "RBT (impl_of t) = t"
    4.26    by (simp add: impl_of_inverse)
    4.27  
    4.28 @@ -148,7 +152,7 @@
    4.29  
    4.30  lemma is_empty_empty [simp]:
    4.31    "is_empty t \<longleftrightarrow> t = empty"
    4.32 -  by (simp add: rbt_eq is_empty_def impl_of_empty split: rbt.split)
    4.33 +  by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
    4.34  
    4.35  lemma RBT_lookup_empty [simp]: (*FIXME*)
    4.36    "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
    4.37 @@ -184,7 +188,7 @@
    4.38  
    4.39  lemma is_empty_Mapping [code]:
    4.40    "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
    4.41 -  by (simp add: rbt_eq Mapping.is_empty_empty Mapping_def)
    4.42 +  by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def)
    4.43  
    4.44  lemma insert_Mapping [code]:
    4.45    "Mapping.update k v (Mapping t) = Mapping (insert k v t)"