1 (* Title: HOL/Datatype.ML |
1 (* Title: HOL/Datatype.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
4 Copyright 1999 TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
5 *) |
|
6 |
|
7 (** legacy ML bindings **) |
|
8 |
|
9 structure bool = |
|
10 struct |
|
11 val distinct = thms "bool.distinct"; |
|
12 val inject = thms "bool.inject"; |
|
13 val exhaust = thm "bool.exhaust"; |
|
14 val cases = thms "bool.cases"; |
|
15 val split = thm "bool.split"; |
|
16 val split_asm = thm "bool.split_asm"; |
|
17 val induct = thm "bool.induct"; |
|
18 val recs = thms "bool.recs"; |
|
19 val simps = thms "bool.simps"; |
|
20 val size = thms "bool.size"; |
|
21 end; |
|
22 |
|
23 structure sum = |
|
24 struct |
|
25 val distinct = thms "sum.distinct"; |
|
26 val inject = thms "sum.inject"; |
|
27 val exhaust = thm "sum.exhaust"; |
|
28 val cases = thms "sum.cases"; |
|
29 val split = thm "sum.split"; |
|
30 val split_asm = thm "sum.split_asm"; |
|
31 val induct = thm "sum.induct"; |
|
32 val recs = thms "sum.recs"; |
|
33 val simps = thms "sum.simps"; |
|
34 val size = thms "sum.size"; |
|
35 end; |
|
36 |
|
37 structure unit = |
|
38 struct |
|
39 val distinct = thms "unit.distinct"; |
|
40 val inject = thms "unit.inject"; |
|
41 val exhaust = thm "unit.exhaust"; |
|
42 val cases = thms "unit.cases"; |
|
43 val split = thm "unit.split"; |
|
44 val split_asm = thm "unit.split_asm"; |
|
45 val induct = thm "unit.induct"; |
|
46 val recs = thms "unit.recs"; |
|
47 val simps = thms "unit.simps"; |
|
48 val size = thms "unit.size"; |
|
49 end; |
|
50 |
|
51 structure prod = |
|
52 struct |
|
53 val distinct = thms "prod.distinct"; |
|
54 val inject = thms "prod.inject"; |
|
55 val exhaust = thm "prod.exhaust"; |
|
56 val cases = thms "prod.cases"; |
|
57 val split = thm "prod.split"; |
|
58 val split_asm = thm "prod.split_asm"; |
|
59 val induct = thm "prod.induct"; |
|
60 val recs = thms "prod.recs"; |
|
61 val simps = thms "prod.simps"; |
|
62 val size = thms "prod.size"; |
|
63 end; |
|
64 |
6 |
65 |
7 (** sum_case -- the selection operator for sums **) |
66 (** sum_case -- the selection operator for sums **) |
8 |
67 |
9 (*compatibility*) |
68 (*compatibility*) |
10 val [sum_case_Inl, sum_case_Inr] = sum.cases; |
69 val [sum_case_Inl, sum_case_Inr] = sum.cases; |
11 bind_thm ("sum_case_Inl", sum_case_Inl); |
70 bind_thm ("sum_case_Inl", sum_case_Inl); |
12 bind_thm ("sum_case_Inr", sum_case_Inr); |
71 bind_thm ("sum_case_Inr", sum_case_Inr); |
13 |
72 |
14 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; |
73 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; |
15 by (EVERY1 [res_inst_tac [("s","s")] sumE, |
74 by (EVERY1 [res_inst_tac [("s","s")] sumE, |
16 etac ssubst, rtac sum_case_Inl, |
75 etac ssubst, rtac sum_case_Inl, |
17 etac ssubst, rtac sum_case_Inr]); |
76 etac ssubst, rtac sum_case_Inr]); |
18 qed "surjective_sum"; |
77 qed "surjective_sum"; |
19 |
78 |
20 (*Prevents simplification of f and g: much faster*) |
79 (*Prevents simplification of f and g: much faster*) |