author  wenzelm 
Tue, 16 Oct 2001 17:51:50 +0200  
changeset 11803  30f2104953a1 
parent 11787  85b3735a51e1 
child 11955  5818c5abb415 
permissions  rwrr 
10519  1 
(* Title: HOL/PreList.thy 
8563  2 
ID: $Id$ 
10733  3 
Author: Tobias Nipkow and Markus Wenzel 
8563  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 
*) 

8490  9 

10 
theory PreList = 

10212  11 
Option + Wellfounded_Relations + NatSimprocs + Recdef + Record + 
10261  12 
Relation_Power + Calculation + SVC_Oracle: 
8490  13 

11803  14 
(*belongs to theory Datatype*) 
10261  15 
declare case_split [cases type: bool] 
16 

17 
(*belongs to theory Wellfounded_Recursion*) 

18 
declare wf_induct [induct set: wf] 

9066  19 

10519  20 
(*belongs to theory Datatype_Universe; hides popular names *) 
21 
hide const Node Atom Leaf Numb Lim Funs Split Case 

10733  22 
hide type node item 
10519  23 

11803  24 
(*belongs to theory Datatype; canonical case/induct rules for 37 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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

30 

11803  31 
lemma prod_induct3 [induct type]: "(!!a b c. P (a, b, c)) ==> P x" 
32 
apply (cases x) 

33 
apply blast 

34 
done 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

35 

11803  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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

41 

11803  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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

46 

11803  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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

52 

11803  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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

57 

11803  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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

63 

11803  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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

68 

11803  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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

74 

11803  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 

11787
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

79 

10671  80 

10680  81 
(* generic summation indexed over nat *) 
82 

10671  83 
consts 
11803  84 
Summation :: "(nat => 'a::{zero, plus}) => nat => 'a" 
10671  85 
primrec 
86 
"Summation f 0 = 0" 

87 
"Summation f (Suc n) = Summation f n + f n" 

88 

89 
syntax 

90 
"_Summation" :: "idt => nat => 'a => nat" ("\<Sum>_<_. _" [0, 51, 10] 10) 

91 
translations 

92 
"\<Sum>i < n. b" == "Summation (\<lambda>i. b) n" 

93 

94 
theorem Summation_step: 

95 
"0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n  1. f i) + f (n  1)" 

96 
by (induct n) simp_all 

97 

8490  98 
end 