author  kleing 
Mon, 15 Oct 2001 21:04:32 +0200  
changeset 11787  85b3735a51e1 
parent 10733  59f82484e000 
child 11803  30f2104953a1 
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 

10261  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] 

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 

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

24 
(*belongs to theory Product_Type; canonical case/induct rules for 37 tuples*) 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

25 
lemma prod_cases3 [cases type: *]: "(!!a b c. y = (a, b, c) ==> P) ==> P" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

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

30 

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

31 
lemma prod_induct3 [induct type: *]: "(!!a b c. P (a, b, c)) ==> P x" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

35 

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

36 
lemma prod_cases4 [cases type: *]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

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

41 

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

42 
lemma prod_induct4 [induct type: *]: "(!!a b c d. P (a, b, c, d)) ==> P x" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

46 

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

47 
lemma prod_cases5 [cases type: *]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

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

52 

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

53 
lemma prod_induct5 [induct type: *]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

57 

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

58 
lemma prod_cases6 [cases type: *]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

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

63 

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

64 
lemma prod_induct6 [induct type: *]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

68 

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

69 
lemma prod_cases7 [cases type: *]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

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

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

74 

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

75 
lemma prod_induct7 [induct type: *]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" 
85b3735a51e1
canonical 'cases'/'induct' rules for ntuples (n=3..7)
kleing
parents:
10733
diff
changeset

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

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

78 
done 
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 

83 
(*FIXME move to Ring_and_Field, when it is made part of main HOL (!?)*) 

84 
(*FIXME port theorems from Algebra/abstract/NatSum*) 

85 

10671  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 

8490  101 
end 