| author | paulson |
| Fri, 14 Aug 1998 13:52:42 +0200 | |
| changeset 5320 | 79b326bceafb |
| parent 5181 | 4ba3787d9709 |
| child 5714 | b4f2e281a907 |
| permissions | -rw-r--r-- |
|
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$ |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
4 |
Copyright 1998 TU Muenchen |
|
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 |
|
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
7 |
Datatype = Univ + |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
8 |
|
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
9 |
rep_datatype sum |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
10 |
distinct "[[Inl_not_Inr, Inr_not_Inl]]" |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
11 |
inject "[[Inl_eq, Inr_eq]]" |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
12 |
induct sum_induct |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
13 |
|
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
14 |
rep_datatype prod |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
15 |
distinct "[[]]" |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
16 |
inject "[[Pair_eq]]" |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
17 |
induct "allI RS (allI RS (split_paired_All RS iffD2)) RS spec" |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
18 |
|
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
19 |
end |