# HG changeset patch # User huffman # Date 1312824775 25200 # Node ID d74182c93f04072a463d2a92486ae10a2d3b51e9 # Parent eb64ffccfc753826a846a76908610b92c66ad319 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too) diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/HOLCF/Fix.thy --- 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\(?x, ?y)) = ?y" by (rule trans [symmetric, OF fix_eq], simp) - from 1 2 show "F\(?x, ?y) = (?x, ?y)" by (simp add: Pair_fst_snd_eq) + from 1 2 show "F\(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff) next fix z assume F_z: "F\z = z" obtain x y where z: "z = (x,y)" by (rule prod.exhaust) diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/HOLCF/IOA/meta_theory/Automata.thy --- 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 diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/HOLCF/Product_Cpo.thy --- 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 \ 'b" assume "x \ y" "y \ 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 \ 'b" @@ -142,7 +142,7 @@ proof fix x y :: "'a \ 'b" show "x \ y \ x = y" - unfolding below_prod_def Pair_fst_snd_eq + unfolding below_prod_def prod_eq_iff by simp qed diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/HOLCF/Sprod.thy --- 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]: diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/HOLCF/Ssum.thy --- 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} *} diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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 diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/HOLCF/ex/Domain_Proofs.thy --- 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 diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/IOA/IOA.thy --- 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) & diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/Library/Product_Vector.thy --- 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 \ '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 \ 'b" show "dist x y = 0 \ 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 \ 'b" show "dist x y \ dist x z + dist y z" @@ -373,7 +373,7 @@ unfolding norm_prod_def by simp show "norm x = 0 \ x = 0" unfolding norm_prod_def - by (simp add: expand_prod_eq) + by (simp add: prod_eq_iff) show "norm (x + y) \ 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 \ 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 diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/Library/Product_plus.thy --- 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 (\x\A. f x) = (\x\A. fst (f x))" by (cases "finite A", induct set: finite, simp_all) diff -r eb64ffccfc75 -r d74182c93f04 src/HOL/Product_Type.thy --- 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 \ fst s = fst t \ snd s = snd t" +lemma prod_eq_iff: "s = t \ fst s = fst t \ snd s = snd t" by (cases s, cases t) simp lemma prod_eqI [intro?]: "fst p = fst q \ snd p = snd q \ 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