# HG changeset patch
# User haftmann
# Date 1162826916 -3600
# Node ID 0cca8d19557d9a0a95530df84f1debbf9ac0c22e
# Parent  7e48158e50f6a2b225c6862201329f0844e688e1
two further lemmas on split

diff -r 7e48158e50f6 -r 0cca8d19557d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Nov 06 16:28:35 2006 +0100
+++ b/src/HOL/Product_Type.thy	Mon Nov 06 16:28:36 2006 +0100
@@ -759,6 +759,17 @@
 setup SplitRule.setup
 
 
+subsection {* Further lemmas *}
+
+lemma
+  split_Pair: "split Pair x = x"
+  unfolding split_def by auto
+
+lemma
+  split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
+  by (cases x, simp)
+
+
 subsection {* Code generator setup *}
 
 instance unit :: eq ..