--- a/src/HOL/Library/AssocList.thy Tue Sep 14 23:38:36 2010 +0200
+++ b/src/HOL/Library/AssocList.thy Wed Sep 15 08:58:34 2010 +0200
@@ -701,37 +701,13 @@
"Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
-lemma map_of_eqI: (*FIXME move to Map.thy*)
- assumes set_eq: "set (map fst xs) = set (map fst ys)"
- assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
- shows "map_of xs = map_of ys"
-proof (rule ext)
- fix k show "map_of xs k = map_of ys k"
- proof (cases "map_of xs k")
- case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
- with set_eq have "k \<notin> set (map fst ys)" by simp
- then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
- with None show ?thesis by simp
- next
- case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
- with map_eq show ?thesis by auto
- qed
-qed
-
-lemma map_of_eq_dom: (*FIXME move to Map.thy*)
- assumes "map_of xs = map_of ys"
- shows "fst ` set xs = fst ` set ys"
-proof -
- from assms have "dom (map_of xs) = dom (map_of ys)" by simp
- then show ?thesis by (simp add: dom_map_of_conv_image_fst)
-qed
-
lemma equal_Mapping [code]:
"HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
(let ks = map fst xs; ls = map fst ys
in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
proof -
- have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" by (auto simp add: image_def intro!: bexI)
+ have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
+ by (auto simp add: image_def intro!: bexI)
show ?thesis
by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
(auto dest!: map_of_eq_dom intro: aux)
--- a/src/HOL/Library/Dlist.thy Tue Sep 14 23:38:36 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Wed Sep 15 08:58:34 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
--- a/src/HOL/Library/Fset.thy Tue Sep 14 23:38:36 2010 +0200
+++ b/src/HOL/Library/Fset.thy Wed Sep 15 08:58:34 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
--- a/src/HOL/Library/Mapping.thy Tue Sep 14 23:38:36 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Wed Sep 15 08:58:34 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
--- a/src/HOL/Library/RBT.thy Tue Sep 14 23:38:36 2010 +0200
+++ b/src/HOL/Library/RBT.thy Wed Sep 15 08:58:34 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)"
--- a/src/HOL/Map.thy Tue Sep 14 23:38:36 2010 +0200
+++ b/src/HOL/Map.thy Wed Sep 15 08:58:34 2010 +0200
@@ -568,6 +568,31 @@
"set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m"
by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)
+lemma map_of_eqI:
+ assumes set_eq: "set (map fst xs) = set (map fst ys)"
+ assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
+ shows "map_of xs = map_of ys"
+proof (rule ext)
+ fix k show "map_of xs k = map_of ys k"
+ proof (cases "map_of xs k")
+ case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
+ with set_eq have "k \<notin> set (map fst ys)" by simp
+ then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
+ with None show ?thesis by simp
+ next
+ case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
+ with map_eq show ?thesis by auto
+ qed
+qed
+
+lemma map_of_eq_dom:
+ assumes "map_of xs = map_of ys"
+ shows "fst ` set xs = fst ` set ys"
+proof -
+ from assms have "dom (map_of xs) = dom (map_of ys)" by simp
+ then show ?thesis by (simp add: dom_map_of_conv_image_fst)
+qed
+
subsection {* @{term [source] ran} *}
--- a/src/Pure/Isar/class.ML Tue Sep 14 23:38:36 2010 +0200
+++ b/src/Pure/Isar/class.ML Wed Sep 15 08:58:34 2010 +0200
@@ -293,7 +293,7 @@
|> Variable.declare_term
(Logic.mk_type (TFree (Name.aT, base_sort)))
|> synchronize_class_syntax sort base_sort
- |> Overloading.add_improvable_syntax;
+ |> Overloading.activate_improvable_syntax;
fun init class thy =
thy
@@ -548,7 +548,7 @@
|> fold (Variable.declare_names o Free o snd) params
|> (Overloading.map_improvable_syntax o apfst)
(K ((primary_constraints, []), (((improve, K NONE), false), [])))
- |> Overloading.add_improvable_syntax
+ |> Overloading.activate_improvable_syntax
|> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
|> synchronize_inst_syntax
|> Local_Theory.init NONE ""
--- a/src/Pure/Isar/overloading.ML Tue Sep 14 23:38:36 2010 +0200
+++ b/src/Pure/Isar/overloading.ML Wed Sep 15 08:58:34 2010 +0200
@@ -7,7 +7,7 @@
signature OVERLOADING =
sig
type improvable_syntax
- val add_improvable_syntax: Proof.context -> Proof.context
+ val activate_improvable_syntax: Proof.context -> Proof.context
val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
-> Proof.context -> Proof.context
val set_primary_constraints: Proof.context -> Proof.context
@@ -104,7 +104,7 @@
val { primary_constraints, ... } = ImprovableSyntax.get ctxt;
in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
-val add_improvable_syntax =
+val activate_improvable_syntax =
Context.proof_map
(Syntax.add_term_check 0 "improvement" improve_term_check
#> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck)
@@ -183,7 +183,7 @@
|> ProofContext.init_global
|> Data.put overloading
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
- |> add_improvable_syntax
+ |> activate_improvable_syntax
|> synchronize_syntax
|> Local_Theory.init NONE ""
{define = Generic_Target.define foundation,