author  wenzelm 
Sat, 03 Nov 2001 01:40:28 +0100  
changeset 12029  7df1d840d01d 
parent 11954  3d1780208bf3 
child 12918  bca45be2d25b 
permissions  rwrr 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Datatype.thy 
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

2 
ID: $Id$ 
11954  3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

5 
*) 
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

6 

12029  7 
header {* Final stage of datatype setup *} 
11954  8 

9 
theory Datatype = Datatype_Universe: 

10 

12029  11 
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} 
11954  12 
hide const Node Atom Leaf Numb Lim Funs Split Case 
13 
hide type node item 

14 

15 

16 
subsection {* Representing primitive types *} 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

17 

5759  18 
rep_datatype bool 
11954  19 
distinct True_not_False False_not_True 
20 
induction bool_induct 

21 

22 
declare case_split [cases type: bool] 

23 
 "prefer plain propositional version" 

24 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

25 
rep_datatype sum 
11954  26 
distinct Inl_not_Inr Inr_not_Inl 
27 
inject Inl_eq Inr_eq 

28 
induction sum_induct 

29 

30 
rep_datatype unit 

31 
induction unit_induct 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

32 

4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

33 
rep_datatype prod 
11954  34 
inject Pair_eq 
35 
induction prod_induct 

36 

37 
text {* Further cases/induct rules for 37 tuples. *} 

38 

39 
lemma prod_cases3 [case_names fields, cases type]: 

40 
"(!!a b c. y = (a, b, c) ==> P) ==> P" 

41 
apply (cases y) 

42 
apply (case_tac b) 

43 
apply blast 

44 
done 

45 

46 
lemma prod_induct3 [case_names fields, induct type]: 

47 
"(!!a b c. P (a, b, c)) ==> P x" 

48 
by (cases x) blast 

49 

50 
lemma prod_cases4 [case_names fields, cases type]: 

51 
"(!!a b c d. y = (a, b, c, d) ==> P) ==> P" 

52 
apply (cases y) 

53 
apply (case_tac c) 

54 
apply blast 

55 
done 

56 

57 
lemma prod_induct4 [case_names fields, induct type]: 

58 
"(!!a b c d. P (a, b, c, d)) ==> P x" 

59 
by (cases x) blast 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

60 

11954  61 
lemma prod_cases5 [case_names fields, cases type]: 
62 
"(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P" 

63 
apply (cases y) 

64 
apply (case_tac d) 

65 
apply blast 

66 
done 

67 

68 
lemma prod_induct5 [case_names fields, induct type]: 

69 
"(!!a b c d e. P (a, b, c, d, e)) ==> P x" 

70 
by (cases x) blast 

71 

72 
lemma prod_cases6 [case_names fields, cases type]: 

73 
"(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P" 

74 
apply (cases y) 

75 
apply (case_tac e) 

76 
apply blast 

77 
done 

78 

79 
lemma prod_induct6 [case_names fields, induct type]: 

80 
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" 

81 
by (cases x) blast 

82 

83 
lemma prod_cases7 [case_names fields, cases type]: 

84 
"(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P" 

85 
apply (cases y) 

86 
apply (case_tac f) 

87 
apply blast 

88 
done 

89 

90 
lemma prod_induct7 [case_names fields, induct type]: 

91 
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" 

92 
by (cases x) blast 

5759  93 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

94 
end 