# HG changeset patch
# User kleing
# Date 1003172672 -7200
# Node ID 85b3735a51e17af3e97072ede06de9138bbdb64b
# Parent  51ce34ef51136b6589d67aa052435cd3669c8952
canonical 'cases'/'induct' rules for n-tuples (n=3..7)
(really belongs to theory Product_Type, but doesn't work there yet)

diff -r 51ce34ef5113 -r 85b3735a51e1 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Mon Oct 15 20:42:06 2001 +0200
+++ b/src/HOL/PreList.thy	Mon Oct 15 21:04:32 2001 +0200
@@ -21,6 +21,62 @@
 hide const Node Atom Leaf Numb Lim Funs Split Case
 hide type node item
 
+(*belongs to theory Product_Type; canonical case/induct rules for 3-7 tuples*)
+lemma prod_cases3 [cases type: *]: "(!!a b c. y = (a, b, c) ==> P) ==> P"
+apply (cases y)
+apply (case_tac b)
+apply blast
+done
+
+lemma prod_induct3 [induct type: *]: "(!!a b c. P (a, b, c)) ==> P x"
+apply (cases x)
+apply blast
+done
+
+lemma prod_cases4 [cases type: *]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
+apply (cases y)
+apply (case_tac c)
+apply blast
+done
+
+lemma prod_induct4 [induct type: *]: "(!!a b c d. P (a, b, c, d)) ==> P x"
+apply (cases x)
+apply blast
+done
+
+lemma prod_cases5 [cases type: *]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
+apply (cases y)
+apply (case_tac d)
+apply blast
+done
+
+lemma prod_induct5 [induct type: *]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
+apply (cases x)
+apply blast
+done
+
+lemma prod_cases6 [cases type: *]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
+apply (cases y)
+apply (case_tac e)
+apply blast
+done
+
+lemma prod_induct6 [induct type: *]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
+apply (cases x)
+apply blast
+done
+
+lemma prod_cases7 [cases type: *]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
+apply (cases y)
+apply (case_tac f)
+apply blast
+done
+
+lemma prod_induct7 [induct type: *]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
+apply (cases x)
+apply blast
+done
+
 
 (* generic summation indexed over nat *)