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