# 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 *)