src/HOL/Product_Type.thy
changeset 35822 67e4de90d2c2
parent 35427 ad039d29e01c
child 35831 e31ec41a551b
equal deleted inserted replaced
35821:ee34f03a7d26 35822:67e4de90d2c2
   995    insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
   995    insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
   996 by blast
   996 by blast
   997 
   997 
   998 lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
   998 lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
   999   by (auto, rule_tac p = "f x" in PairE, auto)
   999   by (auto, rule_tac p = "f x" in PairE, auto)
       
  1000 
       
  1001 lemma swap_inj_on:
       
  1002   "inj_on (%(i, j). (j, i)) (A \<times> B)"
       
  1003   by (unfold inj_on_def) fast
       
  1004 
       
  1005 lemma swap_product:
       
  1006   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
       
  1007   by (simp add: split_def image_def) blast
       
  1008 
  1000 
  1009 
  1001 subsubsection {* Code generator setup *}
  1010 subsubsection {* Code generator setup *}
  1002 
  1011 
  1003 lemma [code]:
  1012 lemma [code]:
  1004   "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
  1013   "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)