equal
deleted
inserted
replaced
6 properties: injectivity / distinctness of constructors and induction). |
6 properties: injectivity / distinctness of constructors and induction). |
7 *) |
7 *) |
8 |
8 |
9 signature DATATYPE_ABS_PROOFS = |
9 signature DATATYPE_ABS_PROOFS = |
10 sig |
10 sig |
11 include DATATYPE_COMMON |
11 type config = Datatype_Aux.config |
|
12 type descr = Datatype_Aux.descr |
12 val prove_casedist_thms : config -> string list -> descr list -> thm -> |
13 val prove_casedist_thms : config -> string list -> descr list -> thm -> |
13 attribute list -> theory -> thm list * theory |
14 attribute list -> theory -> thm list * theory |
14 val prove_primrec_thms : config -> string list -> descr list -> |
15 val prove_primrec_thms : config -> string list -> descr list -> |
15 (string -> thm list) -> thm list list -> thm list list * thm list list -> |
16 (string -> thm list) -> thm list list -> thm list list * thm list list -> |
16 thm -> theory -> (string list * thm list) * theory |
17 thm -> theory -> (string list * thm list) * theory |
27 end; |
28 end; |
28 |
29 |
29 structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS = |
30 structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS = |
30 struct |
31 struct |
31 |
32 |
|
33 type config = Datatype_Aux.config; |
|
34 type descr = Datatype_Aux.descr; |
|
35 |
|
36 |
32 (************************ case distinction theorems ***************************) |
37 (************************ case distinction theorems ***************************) |
33 |
38 |
34 fun prove_casedist_thms (config : Datatype_Aux.config) |
39 fun prove_casedist_thms (config : config) new_type_names descr induct case_names_exhausts thy = |
35 new_type_names descr induct case_names_exhausts thy = |
|
36 let |
40 let |
37 val _ = Datatype_Aux.message config "Proving case distinction theorems ..."; |
41 val _ = Datatype_Aux.message config "Proving case distinction theorems ..."; |
38 |
42 |
39 val descr' = flat descr; |
43 val descr' = flat descr; |
40 val recTs = Datatype_Aux.get_rec_types descr'; |
44 val recTs = Datatype_Aux.get_rec_types descr'; |
77 end; |
81 end; |
78 |
82 |
79 |
83 |
80 (*************************** primrec combinators ******************************) |
84 (*************************** primrec combinators ******************************) |
81 |
85 |
82 fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr |
86 fun prove_primrec_thms (config : config) new_type_names descr |
83 injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy = |
87 injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy = |
84 let |
88 let |
85 val _ = Datatype_Aux.message config "Constructing primrec combinators ..."; |
89 val _ = Datatype_Aux.message config "Constructing primrec combinators ..."; |
86 |
90 |
87 val big_name = space_implode "_" new_type_names; |
91 val big_name = space_implode "_" new_type_names; |
273 end; |
277 end; |
274 |
278 |
275 |
279 |
276 (***************************** case combinators *******************************) |
280 (***************************** case combinators *******************************) |
277 |
281 |
278 fun prove_case_thms (config : Datatype_Aux.config) |
282 fun prove_case_thms (config : config) new_type_names descr reccomb_names primrec_thms thy = |
279 new_type_names descr reccomb_names primrec_thms thy = |
|
280 let |
283 let |
281 val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ..."; |
284 val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ..."; |
282 |
285 |
283 val thy1 = Sign.add_path (space_implode "_" new_type_names) thy; |
286 val thy1 = Sign.add_path (space_implode "_" new_type_names) thy; |
284 |
287 |
348 end; |
351 end; |
349 |
352 |
350 |
353 |
351 (******************************* case splitting *******************************) |
354 (******************************* case splitting *******************************) |
352 |
355 |
353 fun prove_split_thms (config : Datatype_Aux.config) |
356 fun prove_split_thms (config : config) |
354 new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy = |
357 new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy = |
355 let |
358 let |
356 val _ = Datatype_Aux.message config "Proving equations for case splitting ..."; |
359 val _ = Datatype_Aux.message config "Proving equations for case splitting ..."; |
357 |
360 |
358 val descr' = flat descr; |
361 val descr' = flat descr; |
397 |
400 |
398 in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end; |
401 in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end; |
399 |
402 |
400 (************************* additional theorems for TFL ************************) |
403 (************************* additional theorems for TFL ************************) |
401 |
404 |
402 fun prove_nchotomys (config : Datatype_Aux.config) new_type_names descr casedist_thms thy = |
405 fun prove_nchotomys (config : config) new_type_names descr casedist_thms thy = |
403 let |
406 let |
404 val _ = Datatype_Aux.message config "Proving additional theorems for TFL ..."; |
407 val _ = Datatype_Aux.message config "Proving additional theorems for TFL ..."; |
405 |
408 |
406 fun prove_nchotomy (t, exhaustion) = |
409 fun prove_nchotomy (t, exhaustion) = |
407 let |
410 let |
447 map prove_case_cong |
450 map prove_case_cong |
448 (Datatype_Prop.make_case_congs case_names descr thy ~~ nchotomys ~~ case_thms); |
451 (Datatype_Prop.make_case_congs case_names descr thy ~~ nchotomys ~~ case_thms); |
449 |
452 |
450 in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end; |
453 in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end; |
451 |
454 |
452 |
|
453 open Datatype_Aux; |
|
454 |
|
455 end; |
455 end; |