952 |
952 |
953 lemma apsnd_apfst_commute: |
953 lemma apsnd_apfst_commute: |
954 "apsnd f (apfst g p) = apfst g (apsnd f p)" |
954 "apsnd f (apfst g p) = apfst g (apsnd f p)" |
955 by simp |
955 by simp |
956 |
956 |
|
957 context |
|
958 begin |
|
959 |
|
960 local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "prod") *} |
|
961 |
957 definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" |
962 definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" |
958 where |
963 where |
959 "swap p = (snd p, fst p)" |
964 "swap p = (snd p, fst p)" |
960 |
965 |
|
966 end |
|
967 |
961 lemma swap_simp [simp]: |
968 lemma swap_simp [simp]: |
962 "swap (x, y) = (y, x)" |
969 "prod.swap (x, y) = (y, x)" |
963 by (simp add: swap_def) |
970 by (simp add: prod.swap_def) |
964 |
971 |
965 lemma pair_in_swap_image [simp]: |
972 lemma pair_in_swap_image [simp]: |
966 "(y, x) \<in> swap ` A \<longleftrightarrow> (x, y) \<in> A" |
973 "(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A" |
967 by (auto intro!: image_eqI) |
974 by (auto intro!: image_eqI) |
968 |
975 |
969 lemma inj_swap [simp]: |
976 lemma inj_swap [simp]: |
970 "inj_on swap A" |
977 "inj_on prod.swap A" |
971 by (rule inj_onI) (auto simp add: swap_def) |
978 by (rule inj_onI) auto |
|
979 |
|
980 lemma swap_inj_on: |
|
981 "inj_on (\<lambda>(i, j). (j, i)) A" |
|
982 by (rule inj_onI) auto |
972 |
983 |
973 lemma case_swap [simp]: |
984 lemma case_swap [simp]: |
974 "(case swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)" |
985 "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)" |
975 by (cases p) simp |
986 by (cases p) simp |
976 |
987 |
977 text {* |
988 text {* |
978 Disjoint union of a family of sets -- Sigma. |
989 Disjoint union of a family of sets -- Sigma. |
979 *} |
990 *} |
1145 done |
1156 done |
1146 |
1157 |
1147 lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)" |
1158 lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)" |
1148 by auto |
1159 by auto |
1149 |
1160 |
1150 lemma swap_inj_on: |
1161 lemma product_swap: |
1151 "inj_on (\<lambda>(i, j). (j, i)) A" |
1162 "prod.swap ` (A \<times> B) = B \<times> A" |
1152 by (auto intro!: inj_onI) |
1163 by (auto simp add: set_eq_iff) |
1153 |
1164 |
1154 lemma swap_product: |
1165 lemma swap_product: |
1155 "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A" |
1166 "(\<lambda>(i, j). (j, i)) ` (A \<times> B) = B \<times> A" |
1156 by (simp add: split_def image_def set_eq_iff) |
1167 by (auto simp add: set_eq_iff) |
1157 |
1168 |
1158 lemma image_split_eq_Sigma: |
1169 lemma image_split_eq_Sigma: |
1159 "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))" |
1170 "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))" |
1160 proof (safe intro!: imageI) |
1171 proof (safe intro!: imageI) |
1161 fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b" |
1172 fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b" |