778 by (simp add: apfst_def) |
778 by (simp add: apfst_def) |
779 |
779 |
780 lemma upd_snd_conv [simp, code]: |
780 lemma upd_snd_conv [simp, code]: |
781 "apsnd f (x, y) = (x, f y)" |
781 "apsnd f (x, y) = (x, f y)" |
782 by (simp add: apsnd_def) |
782 by (simp add: apsnd_def) |
|
783 |
|
784 lemma fst_apfst [simp]: |
|
785 "fst (apfst f x) = f (fst x)" |
|
786 by (cases x) simp |
|
787 |
|
788 lemma fst_apsnd [simp]: |
|
789 "fst (apsnd f x) = fst x" |
|
790 by (cases x) simp |
|
791 |
|
792 lemma snd_apfst [simp]: |
|
793 "snd (apfst f x) = snd x" |
|
794 by (cases x) simp |
|
795 |
|
796 lemma snd_apsnd [simp]: |
|
797 "snd (apsnd f x) = f (snd x)" |
|
798 by (cases x) simp |
|
799 |
|
800 lemma apfst_compose: |
|
801 "apfst f (apfst g x) = apfst (f \<circ> g) x" |
|
802 by (cases x) simp |
|
803 |
|
804 lemma apsnd_compose: |
|
805 "apsnd f (apsnd g x) = apsnd (f \<circ> g) x" |
|
806 by (cases x) simp |
|
807 |
|
808 lemma apfst_apsnd [simp]: |
|
809 "apfst f (apsnd g x) = (f (fst x), g (snd x))" |
|
810 by (cases x) simp |
|
811 |
|
812 lemma apsnd_apfst [simp]: |
|
813 "apsnd f (apfst g x) = (g (fst x), f (snd x))" |
|
814 by (cases x) simp |
|
815 |
|
816 lemma apfst_id [simp] : |
|
817 "apfst id = id" |
|
818 by (simp add: expand_fun_eq) |
|
819 |
|
820 lemma apsnd_id [simp] : |
|
821 "apsnd id = id" |
|
822 by (simp add: expand_fun_eq) |
|
823 |
|
824 lemma apfst_eq_conv [simp]: |
|
825 "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)" |
|
826 by (cases x) simp |
|
827 |
|
828 lemma apsnd_eq_conv [simp]: |
|
829 "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)" |
|
830 by (cases x) simp |
783 |
831 |
784 |
832 |
785 text {* |
833 text {* |
786 Disjoint union of a family of sets -- Sigma. |
834 Disjoint union of a family of sets -- Sigma. |
787 *} |
835 *} |