| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 30 Jun 2010 16:56:37 +0100 | |
| changeset 2341 | f659ce282610 |
| parent 2338 | e1764a73c292 |
| child 2346 | 4c5881455923 |
| permissions | -rw-r--r-- |
|
2337
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* Title: nominal_dt_alpha.ML |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Christian Urban |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
Author: Cezary Kaliszyk |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
Performing quotient constructions |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
*) |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
|
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
signature NOMINAL_DT_QUOT = |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
sig |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
|
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
val qconst_defs: typ list -> (string * term * mixfix) list -> local_theory -> |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
Quotient_Info.qconsts_info list * local_theory |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
end |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
struct |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
|
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
(* defines the quotient types *) |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
fun qtype_defs qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
let |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
in |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
fold_map Quotient_Type.add_quotient_type qty_args2 lthy |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
end |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
|
| 2338 | 29 |
|
|
2337
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
(* defines quotient constants *) |
| 2338 | 31 |
fun qconst_defs qtys consts_specs lthy = |
|
2337
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
let |
| 2338 | 33 |
val (qconst_infos, lthy') = |
34 |
fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
|
|
2337
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
val phi = ProofContext.export_morphism lthy' lthy |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
in |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
(map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
end |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
|
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
|
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
|
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
end (* structure *) |
|
b151399bd2c3
fixed according to changes in quotient
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |