src/HOL/Product_Type.thy
changeset 33271 7be66dee1a5a
parent 33089 4e33c819fced
child 33275 b497b2574bf6
     1.1 --- a/src/HOL/Product_Type.thy	Tue Oct 27 14:46:03 2009 +0000
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 28 11:42:31 2009 +0000
     1.3 @@ -927,6 +927,9 @@
     1.4     insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
     1.5  by blast
     1.6  
     1.7 +lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
     1.8 +  by (auto, rule_tac p = "f x" in PairE, auto)
     1.9 +
    1.10  subsubsection {* Code generator setup *}
    1.11  
    1.12  instance * :: (eq, eq) eq ..