equal
deleted
inserted
replaced
995 |
995 |
996 lemma case_swap [simp]: |
996 lemma case_swap [simp]: |
997 "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)" |
997 "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)" |
998 by (cases p) simp |
998 by (cases p) simp |
999 |
999 |
|
1000 lemma fst_swap [simp]: "fst (prod.swap x) = snd x" |
|
1001 by(cases x) simp |
|
1002 |
|
1003 lemma snd_swap [simp]: "snd (prod.swap x) = fst x" |
|
1004 by(cases x) simp |
|
1005 |
1000 text \<open> |
1006 text \<open> |
1001 Disjoint union of a family of sets -- Sigma. |
1007 Disjoint union of a family of sets -- Sigma. |
1002 \<close> |
1008 \<close> |
1003 |
1009 |
1004 definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set" where |
1010 definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set" where |