canonical 'cases'/'induct' rules for n-tuples (n=3..7)
authorkleing
Mon Oct 15 21:04:32 2001 +0200 (2001-10-15)
changeset 1178785b3735a51e1
parent 11786 51ce34ef5113
child 11788 60054fee3c16
canonical 'cases'/'induct' rules for n-tuples (n=3..7)
(really belongs to theory Product_Type, but doesn't work there yet)
src/HOL/PreList.thy
     1.1 --- a/src/HOL/PreList.thy	Mon Oct 15 20:42:06 2001 +0200
     1.2 +++ b/src/HOL/PreList.thy	Mon Oct 15 21:04:32 2001 +0200
     1.3 @@ -21,6 +21,62 @@
     1.4  hide const Node Atom Leaf Numb Lim Funs Split Case
     1.5  hide type node item
     1.6  
     1.7 +(*belongs to theory Product_Type; canonical case/induct rules for 3-7 tuples*)
     1.8 +lemma prod_cases3 [cases type: *]: "(!!a b c. y = (a, b, c) ==> P) ==> P"
     1.9 +apply (cases y)
    1.10 +apply (case_tac b)
    1.11 +apply blast
    1.12 +done
    1.13 +
    1.14 +lemma prod_induct3 [induct type: *]: "(!!a b c. P (a, b, c)) ==> P x"
    1.15 +apply (cases x)
    1.16 +apply blast
    1.17 +done
    1.18 +
    1.19 +lemma prod_cases4 [cases type: *]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    1.20 +apply (cases y)
    1.21 +apply (case_tac c)
    1.22 +apply blast
    1.23 +done
    1.24 +
    1.25 +lemma prod_induct4 [induct type: *]: "(!!a b c d. P (a, b, c, d)) ==> P x"
    1.26 +apply (cases x)
    1.27 +apply blast
    1.28 +done
    1.29 +
    1.30 +lemma prod_cases5 [cases type: *]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    1.31 +apply (cases y)
    1.32 +apply (case_tac d)
    1.33 +apply blast
    1.34 +done
    1.35 +
    1.36 +lemma prod_induct5 [induct type: *]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    1.37 +apply (cases x)
    1.38 +apply blast
    1.39 +done
    1.40 +
    1.41 +lemma prod_cases6 [cases type: *]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    1.42 +apply (cases y)
    1.43 +apply (case_tac e)
    1.44 +apply blast
    1.45 +done
    1.46 +
    1.47 +lemma prod_induct6 [induct type: *]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
    1.48 +apply (cases x)
    1.49 +apply blast
    1.50 +done
    1.51 +
    1.52 +lemma prod_cases7 [cases type: *]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
    1.53 +apply (cases y)
    1.54 +apply (case_tac f)
    1.55 +apply blast
    1.56 +done
    1.57 +
    1.58 +lemma prod_induct7 [induct type: *]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
    1.59 +apply (cases x)
    1.60 +apply blast
    1.61 +done
    1.62 +
    1.63  
    1.64  (* generic summation indexed over nat *)
    1.65