rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
authorhuffman
Mon Aug 08 10:32:55 2011 -0700 (2011-08-08)
changeset 44066d74182c93f04
parent 44065 eb64ffccfc75
child 44067 5feac96f0e78
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
src/HOL/HOLCF/Fix.thy
src/HOL/HOLCF/IOA/meta_theory/Automata.thy
src/HOL/HOLCF/Product_Cpo.thy
src/HOL/HOLCF/Sprod.thy
src/HOL/HOLCF/Ssum.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/ex/Domain_Proofs.thy
src/HOL/IOA/IOA.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Product_plus.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/HOLCF/Fix.thy	Mon Aug 08 10:26:26 2011 -0700
     1.2 +++ b/src/HOL/HOLCF/Fix.thy	Mon Aug 08 10:32:55 2011 -0700
     1.3 @@ -219,7 +219,7 @@
     1.4      by (rule trans [symmetric, OF fix_eq], simp)
     1.5    have 2: "snd (F\<cdot>(?x, ?y)) = ?y"
     1.6      by (rule trans [symmetric, OF fix_eq], simp)
     1.7 -  from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: Pair_fst_snd_eq)
     1.8 +  from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
     1.9  next
    1.10    fix z assume F_z: "F\<cdot>z = z"
    1.11    obtain x y where z: "z = (x,y)" by (rule prod.exhaust)
     2.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Mon Aug 08 10:26:26 2011 -0700
     2.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Mon Aug 08 10:32:55 2011 -0700
     2.3 @@ -609,7 +609,7 @@
     2.4     (if a:actions(asig_of(D)) then                                             
     2.5        (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                       
     2.6      else snd(snd(snd(t)))=snd(snd(snd(s)))))"
     2.7 -  apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq Let_def ioa_projections)
     2.8 +  apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)
     2.9    done
    2.10  
    2.11  
     3.1 --- a/src/HOL/HOLCF/Product_Cpo.thy	Mon Aug 08 10:26:26 2011 -0700
     3.2 +++ b/src/HOL/HOLCF/Product_Cpo.thy	Mon Aug 08 10:32:55 2011 -0700
     3.3 @@ -46,7 +46,7 @@
     3.4  next
     3.5    fix x y :: "'a \<times> 'b"
     3.6    assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
     3.7 -    unfolding below_prod_def Pair_fst_snd_eq
     3.8 +    unfolding below_prod_def prod_eq_iff
     3.9      by (fast intro: below_antisym)
    3.10  next
    3.11    fix x y z :: "'a \<times> 'b"
    3.12 @@ -142,7 +142,7 @@
    3.13  proof
    3.14    fix x y :: "'a \<times> 'b"
    3.15    show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
    3.16 -    unfolding below_prod_def Pair_fst_snd_eq
    3.17 +    unfolding below_prod_def prod_eq_iff
    3.18      by simp
    3.19  qed
    3.20  
     4.1 --- a/src/HOL/HOLCF/Sprod.thy	Mon Aug 08 10:26:26 2011 -0700
     4.2 +++ b/src/HOL/HOLCF/Sprod.thy	Mon Aug 08 10:32:55 2011 -0700
     4.3 @@ -63,7 +63,7 @@
     4.4  
     4.5  lemmas Rep_sprod_simps =
     4.6    Rep_sprod_inject [symmetric] below_sprod_def
     4.7 -  Pair_fst_snd_eq below_prod_def
     4.8 +  prod_eq_iff below_prod_def
     4.9    Rep_sprod_strict Rep_sprod_spair
    4.10  
    4.11  lemma sprodE [case_names bottom spair, cases type: sprod]:
     5.1 --- a/src/HOL/HOLCF/Ssum.thy	Mon Aug 08 10:26:26 2011 -0700
     5.2 +++ b/src/HOL/HOLCF/Ssum.thy	Mon Aug 08 10:32:55 2011 -0700
     5.3 @@ -52,7 +52,7 @@
     5.4  
     5.5  lemmas Rep_ssum_simps =
     5.6    Rep_ssum_inject [symmetric] below_ssum_def
     5.7 -  Pair_fst_snd_eq below_prod_def
     5.8 +  prod_eq_iff below_prod_def
     5.9    Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
    5.10  
    5.11  subsection {* Properties of \emph{sinl} and \emph{sinr} *}
     6.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Aug 08 10:26:26 2011 -0700
     6.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Aug 08 10:32:55 2011 -0700
     6.3 @@ -721,7 +721,7 @@
     6.4          val rules0 =
     6.5              @{thms iterate_0 Pair_strict} @ take_0_thms
     6.6          val rules1 =
     6.7 -            @{thms iterate_Suc Pair_fst_snd_eq fst_conv snd_conv}
     6.8 +            @{thms iterate_Suc prod_eq_iff fst_conv snd_conv}
     6.9              @ take_Suc_thms
    6.10          val tac =
    6.11              EVERY
     7.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Mon Aug 08 10:26:26 2011 -0700
     7.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Mon Aug 08 10:32:55 2011 -0700
     7.3 @@ -470,7 +470,7 @@
     7.4  apply (rule lub_eq)
     7.5  apply (rule nat.induct)
     7.6  apply (simp only: iterate_0 Pair_strict take_0_thms)
     7.7 -apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
     7.8 +apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv
     7.9                    foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
    7.10  done
    7.11  
     8.1 --- a/src/HOL/IOA/IOA.thy	Mon Aug 08 10:26:26 2011 -0700
     8.2 +++ b/src/HOL/IOA/IOA.thy	Mon Aug 08 10:32:55 2011 -0700
     8.3 @@ -317,7 +317,7 @@
     8.4        (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
     8.5      else snd(snd(snd(t)))=snd(snd(snd(s)))))"
     8.6    (*SLOW*)
     8.7 -  apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq ioa_projections)
     8.8 +  apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff ioa_projections)
     8.9    done
    8.10  
    8.11  lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
     9.1 --- a/src/HOL/Library/Product_Vector.thy	Mon Aug 08 10:26:26 2011 -0700
     9.2 +++ b/src/HOL/Library/Product_Vector.thy	Mon Aug 08 10:32:55 2011 -0700
     9.3 @@ -28,13 +28,13 @@
     9.4  instance proof
     9.5    fix a b :: real and x y :: "'a \<times> 'b"
     9.6    show "scaleR a (x + y) = scaleR a x + scaleR a y"
     9.7 -    by (simp add: expand_prod_eq scaleR_right_distrib)
     9.8 +    by (simp add: prod_eq_iff scaleR_right_distrib)
     9.9    show "scaleR (a + b) x = scaleR a x + scaleR b x"
    9.10 -    by (simp add: expand_prod_eq scaleR_left_distrib)
    9.11 +    by (simp add: prod_eq_iff scaleR_left_distrib)
    9.12    show "scaleR a (scaleR b x) = scaleR (a * b) x"
    9.13 -    by (simp add: expand_prod_eq)
    9.14 +    by (simp add: prod_eq_iff)
    9.15    show "scaleR 1 x = x"
    9.16 -    by (simp add: expand_prod_eq)
    9.17 +    by (simp add: prod_eq_iff)
    9.18  qed
    9.19  
    9.20  end
    9.21 @@ -174,7 +174,7 @@
    9.22  instance proof
    9.23    fix x y :: "'a \<times> 'b"
    9.24    show "dist x y = 0 \<longleftrightarrow> x = y"
    9.25 -    unfolding dist_prod_def expand_prod_eq by simp
    9.26 +    unfolding dist_prod_def prod_eq_iff by simp
    9.27  next
    9.28    fix x y z :: "'a \<times> 'b"
    9.29    show "dist x y \<le> dist x z + dist y z"
    9.30 @@ -373,7 +373,7 @@
    9.31      unfolding norm_prod_def by simp
    9.32    show "norm x = 0 \<longleftrightarrow> x = 0"
    9.33      unfolding norm_prod_def
    9.34 -    by (simp add: expand_prod_eq)
    9.35 +    by (simp add: prod_eq_iff)
    9.36    show "norm (x + y) \<le> norm x + norm y"
    9.37      unfolding norm_prod_def
    9.38      apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
    9.39 @@ -423,7 +423,7 @@
    9.40      unfolding inner_prod_def
    9.41      by (intro add_nonneg_nonneg inner_ge_zero)
    9.42    show "inner x x = 0 \<longleftrightarrow> x = 0"
    9.43 -    unfolding inner_prod_def expand_prod_eq
    9.44 +    unfolding inner_prod_def prod_eq_iff
    9.45      by (simp add: add_nonneg_eq_0_iff)
    9.46    show "norm x = sqrt (inner x x)"
    9.47      unfolding norm_prod_def inner_prod_def
    10.1 --- a/src/HOL/Library/Product_plus.thy	Mon Aug 08 10:26:26 2011 -0700
    10.2 +++ b/src/HOL/Library/Product_plus.thy	Mon Aug 08 10:32:55 2011 -0700
    10.3 @@ -78,39 +78,36 @@
    10.4  lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
    10.5    unfolding uminus_prod_def by simp
    10.6  
    10.7 -lemmas expand_prod_eq = Pair_fst_snd_eq
    10.8 -
    10.9 -
   10.10  subsection {* Class instances *}
   10.11  
   10.12  instance prod :: (semigroup_add, semigroup_add) semigroup_add
   10.13 -  by default (simp add: expand_prod_eq add_assoc)
   10.14 +  by default (simp add: prod_eq_iff add_assoc)
   10.15  
   10.16  instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
   10.17 -  by default (simp add: expand_prod_eq add_commute)
   10.18 +  by default (simp add: prod_eq_iff add_commute)
   10.19  
   10.20  instance prod :: (monoid_add, monoid_add) monoid_add
   10.21 -  by default (simp_all add: expand_prod_eq)
   10.22 +  by default (simp_all add: prod_eq_iff)
   10.23  
   10.24  instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
   10.25 -  by default (simp add: expand_prod_eq)
   10.26 +  by default (simp add: prod_eq_iff)
   10.27  
   10.28  instance prod ::
   10.29    (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
   10.30 -    by default (simp_all add: expand_prod_eq)
   10.31 +    by default (simp_all add: prod_eq_iff)
   10.32  
   10.33  instance prod ::
   10.34    (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   10.35 -    by default (simp add: expand_prod_eq)
   10.36 +    by default (simp add: prod_eq_iff)
   10.37  
   10.38  instance prod ::
   10.39    (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   10.40  
   10.41  instance prod :: (group_add, group_add) group_add
   10.42 -  by default (simp_all add: expand_prod_eq diff_minus)
   10.43 +  by default (simp_all add: prod_eq_iff diff_minus)
   10.44  
   10.45  instance prod :: (ab_group_add, ab_group_add) ab_group_add
   10.46 -  by default (simp_all add: expand_prod_eq)
   10.47 +  by default (simp_all add: prod_eq_iff)
   10.48  
   10.49  lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
   10.50  by (cases "finite A", induct set: finite, simp_all)
    11.1 --- a/src/HOL/Product_Type.thy	Mon Aug 08 10:26:26 2011 -0700
    11.2 +++ b/src/HOL/Product_Type.thy	Mon Aug 08 10:32:55 2011 -0700
    11.3 @@ -436,11 +436,11 @@
    11.4  
    11.5  lemmas surjective_pairing = pair_collapse [symmetric]
    11.6  
    11.7 -lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
    11.8 +lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
    11.9    by (cases s, cases t) simp
   11.10  
   11.11  lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
   11.12 -  by (simp add: Pair_fst_snd_eq)
   11.13 +  by (simp add: prod_eq_iff)
   11.14  
   11.15  lemma split_conv [simp, code]: "split f (a, b) = f a b"
   11.16    by (fact prod.cases)
   11.17 @@ -1226,4 +1226,6 @@
   11.18  
   11.19  lemmas split = split_conv  -- {* for backwards compatibility *}
   11.20  
   11.21 +lemmas Pair_fst_snd_eq = prod_eq_iff
   11.22 +
   11.23  end