# HG changeset patch # User haftmann # Date 1284533914 -7200 # Node ID 9717ea8d42b313c32dc3cc4879b6f18798c79d82 # Parent 9e544eb396dcc57f0ca771bd86ee2e813ae1c485# Parent 5a2662c1e44a3fdeab1f9583075586f5f581e956 merged diff -r 9e544eb396dc -r 9717ea8d42b3 src/HOL/Library/AssocList.thy --- 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 (\n. (n, vs ! n)) [0..k\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 \ set (map fst xs)" by (simp add: map_of_eq_None_iff) - with set_eq have "k \ 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 \ 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) \ (let ks = map fst xs; ls = map fst ys in (\l\set ls. l \ set ks) \ (\k\set ks. k \ set ls \ map_of xs k = map_of ys k))" proof - - have aux: "\a b xs. (a, b) \ set xs \ a \ fst ` set xs" by (auto simp add: image_def intro!: bexI) + have aux: "\a b xs. (a, b) \ set xs \ a \ 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) diff -r 9e544eb396dc -r 9717ea8d42b3 src/HOL/Library/Dlist.thy --- 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 "[] \ ?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 \ 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 \ dxs = dys" + by (simp add: dlist_eq_iff) text {* Formal, totalized constructor for @{typ "'a dlist"}: *} definition Dlist :: "'a list \ '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 9e544eb396dc -r 9717ea8d42b3 src/HOL/Library/Fset.thy --- 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 \ A = B" by (simp add: Fset_inject) +lemma fset_eq_iff: + "A = B \ member A = member B" + by (simp add: member_inject) + lemma fset_eqI: "member A = member B \ 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 \ A \ B \ B \ (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 9e544eb396dc -r 9717ea8d42b3 src/HOL/Library/Mapping.thy --- 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 \ f = g" by (simp add: Mapping_inject) +lemma mapping_eq_iff: + "m = n \ 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 \ m = n" + by (simp add: mapping_eq_iff) definition empty :: "('a, 'b) mapping" where "empty = Mapping (\_. None)" @@ -287,7 +288,7 @@ "HOL.equal m n \ lookup m = lookup n" instance proof -qed (simp add: equal_mapping_def) +qed (simp add: equal_mapping_def mapping_eq_iff) end diff -r 9e544eb396dc -r 9717ea8d42b3 src/HOL/Library/RBT.thy --- 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 \ impl_of t1 = impl_of t2" + by (simp add: impl_of_inject) + +lemma rbt_eqI: + "impl_of t1 = impl_of t2 \ 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 \ 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 \ 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 \ t = RBT_Impl.Empty" @@ -184,7 +188,7 @@ lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping t) \ 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)" diff -r 9e544eb396dc -r 9717ea8d42b3 src/HOL/Map.thy --- 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 \ map_of (map (\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: "\k\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 \ set (map fst xs)" by (simp add: map_of_eq_None_iff) + with set_eq have "k \ 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 \ 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} *} diff -r 9e544eb396dc -r 9717ea8d42b3 src/Pure/Isar/class.ML --- 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 "" diff -r 9e544eb396dc -r 9717ea8d42b3 src/Pure/Isar/overloading.ML --- 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,