src/HOL/PreList.thy
author kleing
Mon Oct 15 21:04:32 2001 +0200 (2001-10-15)
changeset 11787 85b3735a51e1
parent 10733 59f82484e000
child 11803 30f2104953a1
permissions -rw-r--r--
canonical 'cases'/'induct' rules for n-tuples (n=3..7)
(really belongs to theory Product_Type, but doesn't work there yet)
     1 (*  Title:      HOL/PreList.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel
     4     Copyright   2000 TU Muenchen
     5 
     6 A basis for building theory List on. Is defined separately to serve as a
     7 basis for theory ToyList in the documentation.
     8 *)
     9 
    10 theory PreList =
    11   Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
    12   Relation_Power + Calculation + SVC_Oracle:
    13 
    14 (*belongs to theory HOL*)
    15 declare case_split [cases type: bool]
    16 
    17 (*belongs to theory Wellfounded_Recursion*)
    18 declare wf_induct [induct set: wf]
    19 
    20 (*belongs to theory Datatype_Universe; hides popular names *)
    21 hide const Node Atom Leaf Numb Lim Funs Split Case
    22 hide type node item
    23 
    24 (*belongs to theory Product_Type; canonical case/induct rules for 3-7 tuples*)
    25 lemma prod_cases3 [cases type: *]: "(!!a b c. y = (a, b, c) ==> P) ==> P"
    26 apply (cases y)
    27 apply (case_tac b)
    28 apply blast
    29 done
    30 
    31 lemma prod_induct3 [induct type: *]: "(!!a b c. P (a, b, c)) ==> P x"
    32 apply (cases x)
    33 apply blast
    34 done
    35 
    36 lemma prod_cases4 [cases type: *]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    37 apply (cases y)
    38 apply (case_tac c)
    39 apply blast
    40 done
    41 
    42 lemma prod_induct4 [induct type: *]: "(!!a b c d. P (a, b, c, d)) ==> P x"
    43 apply (cases x)
    44 apply blast
    45 done
    46 
    47 lemma prod_cases5 [cases type: *]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    48 apply (cases y)
    49 apply (case_tac d)
    50 apply blast
    51 done
    52 
    53 lemma prod_induct5 [induct type: *]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    54 apply (cases x)
    55 apply blast
    56 done
    57 
    58 lemma prod_cases6 [cases type: *]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    59 apply (cases y)
    60 apply (case_tac e)
    61 apply blast
    62 done
    63 
    64 lemma prod_induct6 [induct type: *]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
    65 apply (cases x)
    66 apply blast
    67 done
    68 
    69 lemma prod_cases7 [cases type: *]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
    70 apply (cases y)
    71 apply (case_tac f)
    72 apply blast
    73 done
    74 
    75 lemma prod_induct7 [induct type: *]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
    76 apply (cases x)
    77 apply blast
    78 done
    79 
    80 
    81 (* generic summation indexed over nat *)
    82 
    83 (*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*)
    84 (*FIXME port theorems from Algebra/abstract/NatSum*)
    85 
    86 consts
    87   Summation :: "(nat => 'a::{zero,plus}) => nat => 'a"
    88 primrec
    89   "Summation f 0 = 0"
    90   "Summation f (Suc n) = Summation f n + f n"
    91 
    92 syntax
    93   "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    94 translations
    95   "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
    96 
    97 theorem Summation_step:
    98     "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
    99   by (induct n) simp_all
   100 
   101 end