|
7293
|
1 |
(* Title: HOL/Datatype.ML
|
|
|
2 |
ID: $Id$
|
|
11954
|
3 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
|
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
7293
|
5 |
*)
|
|
|
6 |
|
|
11954
|
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 |
|
|
|
65 |
|
|
7293
|
66 |
(** sum_case -- the selection operator for sums **)
|
|
|
67 |
|
|
|
68 |
(*compatibility*)
|
|
|
69 |
val [sum_case_Inl, sum_case_Inr] = sum.cases;
|
|
9108
|
70 |
bind_thm ("sum_case_Inl", sum_case_Inl);
|
|
|
71 |
bind_thm ("sum_case_Inr", sum_case_Inr);
|
|
7293
|
72 |
|
|
|
73 |
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
|
|
11954
|
74 |
by (EVERY1 [res_inst_tac [("s","s")] sumE,
|
|
7293
|
75 |
etac ssubst, rtac sum_case_Inl,
|
|
|
76 |
etac ssubst, rtac sum_case_Inr]);
|
|
|
77 |
qed "surjective_sum";
|
|
|
78 |
|
|
|
79 |
(*Prevents simplification of f and g: much faster*)
|
|
|
80 |
Goal "s=t ==> sum_case f g s = sum_case f g t";
|
|
|
81 |
by (etac arg_cong 1);
|
|
|
82 |
qed "sum_case_weak_cong";
|
|
|
83 |
|
|
|
84 |
val [p1,p2] = Goal
|
|
|
85 |
"[| sum_case f1 f2 = sum_case g1 g2; \
|
|
|
86 |
\ [| f1 = g1; f2 = g2 |] ==> P |] \
|
|
|
87 |
\ ==> P";
|
|
|
88 |
by (rtac p2 1);
|
|
|
89 |
by (rtac ext 1);
|
|
|
90 |
by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
|
|
|
91 |
by (Asm_full_simp_tac 1);
|
|
|
92 |
by (rtac ext 1);
|
|
|
93 |
by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
|
|
|
94 |
by (Asm_full_simp_tac 1);
|
|
|
95 |
qed "sum_case_inject";
|