--- a/src/HOL/HOLCF/Fix.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/HOLCF/Fix.thy Mon Aug 08 10:32:55 2011 -0700
@@ -219,7 +219,7 @@
by (rule trans [symmetric, OF fix_eq], simp)
have 2: "snd (F\<cdot>(?x, ?y)) = ?y"
by (rule trans [symmetric, OF fix_eq], simp)
- from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: Pair_fst_snd_eq)
+ from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
next
fix z assume F_z: "F\<cdot>z = z"
obtain x y where z: "z = (x,y)" by (rule prod.exhaust)
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Mon Aug 08 10:32:55 2011 -0700
@@ -609,7 +609,7 @@
(if a:actions(asig_of(D)) then
(snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
else snd(snd(snd(t)))=snd(snd(snd(s)))))"
- apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq Let_def ioa_projections)
+ apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)
done
--- a/src/HOL/HOLCF/Product_Cpo.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/HOLCF/Product_Cpo.thy Mon Aug 08 10:32:55 2011 -0700
@@ -46,7 +46,7 @@
next
fix x y :: "'a \<times> 'b"
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
- unfolding below_prod_def Pair_fst_snd_eq
+ unfolding below_prod_def prod_eq_iff
by (fast intro: below_antisym)
next
fix x y z :: "'a \<times> 'b"
@@ -142,7 +142,7 @@
proof
fix x y :: "'a \<times> 'b"
show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
- unfolding below_prod_def Pair_fst_snd_eq
+ unfolding below_prod_def prod_eq_iff
by simp
qed
--- a/src/HOL/HOLCF/Sprod.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/HOLCF/Sprod.thy Mon Aug 08 10:32:55 2011 -0700
@@ -63,7 +63,7 @@
lemmas Rep_sprod_simps =
Rep_sprod_inject [symmetric] below_sprod_def
- Pair_fst_snd_eq below_prod_def
+ prod_eq_iff below_prod_def
Rep_sprod_strict Rep_sprod_spair
lemma sprodE [case_names bottom spair, cases type: sprod]:
--- a/src/HOL/HOLCF/Ssum.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/HOLCF/Ssum.thy Mon Aug 08 10:32:55 2011 -0700
@@ -52,7 +52,7 @@
lemmas Rep_ssum_simps =
Rep_ssum_inject [symmetric] below_ssum_def
- Pair_fst_snd_eq below_prod_def
+ prod_eq_iff below_prod_def
Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
subsection {* Properties of \emph{sinl} and \emph{sinr} *}
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 10:32:55 2011 -0700
@@ -721,7 +721,7 @@
val rules0 =
@{thms iterate_0 Pair_strict} @ take_0_thms
val rules1 =
- @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv}
+ @{thms iterate_Suc prod_eq_iff fst_conv snd_conv}
@ take_Suc_thms
val tac =
EVERY
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Mon Aug 08 10:32:55 2011 -0700
@@ -470,7 +470,7 @@
apply (rule lub_eq)
apply (rule nat.induct)
apply (simp only: iterate_0 Pair_strict take_0_thms)
-apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
+apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv
foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
done
--- a/src/HOL/IOA/IOA.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/IOA/IOA.thy Mon Aug 08 10:32:55 2011 -0700
@@ -317,7 +317,7 @@
(snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
else snd(snd(snd(t)))=snd(snd(snd(s)))))"
(*SLOW*)
- apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq ioa_projections)
+ apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff ioa_projections)
done
lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
--- a/src/HOL/Library/Product_Vector.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/Library/Product_Vector.thy Mon Aug 08 10:32:55 2011 -0700
@@ -28,13 +28,13 @@
instance proof
fix a b :: real and x y :: "'a \<times> 'b"
show "scaleR a (x + y) = scaleR a x + scaleR a y"
- by (simp add: expand_prod_eq scaleR_right_distrib)
+ by (simp add: prod_eq_iff scaleR_right_distrib)
show "scaleR (a + b) x = scaleR a x + scaleR b x"
- by (simp add: expand_prod_eq scaleR_left_distrib)
+ by (simp add: prod_eq_iff scaleR_left_distrib)
show "scaleR a (scaleR b x) = scaleR (a * b) x"
- by (simp add: expand_prod_eq)
+ by (simp add: prod_eq_iff)
show "scaleR 1 x = x"
- by (simp add: expand_prod_eq)
+ by (simp add: prod_eq_iff)
qed
end
@@ -174,7 +174,7 @@
instance proof
fix x y :: "'a \<times> 'b"
show "dist x y = 0 \<longleftrightarrow> x = y"
- unfolding dist_prod_def expand_prod_eq by simp
+ unfolding dist_prod_def prod_eq_iff by simp
next
fix x y z :: "'a \<times> 'b"
show "dist x y \<le> dist x z + dist y z"
@@ -373,7 +373,7 @@
unfolding norm_prod_def by simp
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_prod_def
- by (simp add: expand_prod_eq)
+ by (simp add: prod_eq_iff)
show "norm (x + y) \<le> norm x + norm y"
unfolding norm_prod_def
apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
@@ -423,7 +423,7 @@
unfolding inner_prod_def
by (intro add_nonneg_nonneg inner_ge_zero)
show "inner x x = 0 \<longleftrightarrow> x = 0"
- unfolding inner_prod_def expand_prod_eq
+ unfolding inner_prod_def prod_eq_iff
by (simp add: add_nonneg_eq_0_iff)
show "norm x = sqrt (inner x x)"
unfolding norm_prod_def inner_prod_def
--- a/src/HOL/Library/Product_plus.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/Library/Product_plus.thy Mon Aug 08 10:32:55 2011 -0700
@@ -78,39 +78,36 @@
lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
unfolding uminus_prod_def by simp
-lemmas expand_prod_eq = Pair_fst_snd_eq
-
-
subsection {* Class instances *}
instance prod :: (semigroup_add, semigroup_add) semigroup_add
- by default (simp add: expand_prod_eq add_assoc)
+ by default (simp add: prod_eq_iff add_assoc)
instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
- by default (simp add: expand_prod_eq add_commute)
+ by default (simp add: prod_eq_iff add_commute)
instance prod :: (monoid_add, monoid_add) monoid_add
- by default (simp_all add: expand_prod_eq)
+ by default (simp_all add: prod_eq_iff)
instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
- by default (simp add: expand_prod_eq)
+ by default (simp add: prod_eq_iff)
instance prod ::
(cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
- by default (simp_all add: expand_prod_eq)
+ by default (simp_all add: prod_eq_iff)
instance prod ::
(cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
- by default (simp add: expand_prod_eq)
+ by default (simp add: prod_eq_iff)
instance prod ::
(cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
instance prod :: (group_add, group_add) group_add
- by default (simp_all add: expand_prod_eq diff_minus)
+ by default (simp_all add: prod_eq_iff diff_minus)
instance prod :: (ab_group_add, ab_group_add) ab_group_add
- by default (simp_all add: expand_prod_eq)
+ by default (simp_all add: prod_eq_iff)
lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
by (cases "finite A", induct set: finite, simp_all)
--- a/src/HOL/Product_Type.thy Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/Product_Type.thy Mon Aug 08 10:32:55 2011 -0700
@@ -436,11 +436,11 @@
lemmas surjective_pairing = pair_collapse [symmetric]
-lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
+lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
by (cases s, cases t) simp
lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
- by (simp add: Pair_fst_snd_eq)
+ by (simp add: prod_eq_iff)
lemma split_conv [simp, code]: "split f (a, b) = f a b"
by (fact prod.cases)
@@ -1226,4 +1226,6 @@
lemmas split = split_conv -- {* for backwards compatibility *}
+lemmas Pair_fst_snd_eq = prod_eq_iff
+
end