swap with qualifier;
authorhaftmann
Mon Apr 21 21:16:05 2014 +0200 (2014-04-21)
changeset 566266532efd66a70
parent 56625 54505623a8ef
child 56627 cb912b7de3cf
swap with qualifier;
tuned
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Sun Apr 20 00:25:05 2014 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Apr 21 21:16:05 2014 +0200
     1.3 @@ -954,24 +954,35 @@
     1.4    "apsnd f (apfst g p) = apfst g (apsnd f p)"
     1.5    by simp
     1.6  
     1.7 +context
     1.8 +begin
     1.9 +
    1.10 +local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "prod") *}
    1.11 +
    1.12  definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
    1.13  where
    1.14    "swap p = (snd p, fst p)"
    1.15  
    1.16 +end
    1.17 +
    1.18  lemma swap_simp [simp]:
    1.19 -  "swap (x, y) = (y, x)"
    1.20 -  by (simp add: swap_def)
    1.21 +  "prod.swap (x, y) = (y, x)"
    1.22 +  by (simp add: prod.swap_def)
    1.23  
    1.24  lemma pair_in_swap_image [simp]:
    1.25 -  "(y, x) \<in> swap ` A \<longleftrightarrow> (x, y) \<in> A"
    1.26 +  "(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A"
    1.27    by (auto intro!: image_eqI)
    1.28  
    1.29  lemma inj_swap [simp]:
    1.30 -  "inj_on swap A"
    1.31 -  by (rule inj_onI) (auto simp add: swap_def)
    1.32 +  "inj_on prod.swap A"
    1.33 +  by (rule inj_onI) auto
    1.34 +
    1.35 +lemma swap_inj_on:
    1.36 +  "inj_on (\<lambda>(i, j). (j, i)) A"
    1.37 +  by (rule inj_onI) auto
    1.38  
    1.39  lemma case_swap [simp]:
    1.40 -  "(case swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
    1.41 +  "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
    1.42    by (cases p) simp
    1.43  
    1.44  text {*
    1.45 @@ -1147,13 +1158,13 @@
    1.46  lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
    1.47    by auto
    1.48  
    1.49 -lemma swap_inj_on:
    1.50 -  "inj_on (\<lambda>(i, j). (j, i)) A"
    1.51 -  by (auto intro!: inj_onI)
    1.52 +lemma product_swap:
    1.53 +  "prod.swap ` (A \<times> B) = B \<times> A"
    1.54 +  by (auto simp add: set_eq_iff)
    1.55  
    1.56  lemma swap_product:
    1.57 -  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
    1.58 -  by (simp add: split_def image_def set_eq_iff)
    1.59 +  "(\<lambda>(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
    1.60 +  by (auto simp add: set_eq_iff)
    1.61  
    1.62  lemma image_split_eq_Sigma:
    1.63    "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"