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