5 Performing quotient constructions |
5 Performing quotient constructions |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_DT_QUOT = |
8 signature NOMINAL_DT_QUOT = |
9 sig |
9 sig |
10 val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> |
10 val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> |
11 thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory |
11 thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory |
12 |
12 |
13 val qconst_defs: typ list -> (string * term * mixfix) list -> local_theory -> |
13 val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory -> |
14 Quotient_Info.qconsts_info list * local_theory |
14 Quotient_Info.qconsts_info list * local_theory |
15 |
15 |
16 val qperm_defs: typ list -> string list -> (string * term * mixfix) list -> |
16 val define_qperms: typ list -> string list -> (string * term * mixfix) list -> |
17 thm list -> theory -> theory |
17 thm list -> theory -> theory |
|
18 |
|
19 val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> |
|
20 theory -> theory |
18 end |
21 end |
19 |
22 |
20 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
23 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
21 struct |
24 struct |
22 |
25 |
23 (* defines the quotient types *) |
26 (* defines the quotient types *) |
24 fun qtype_defs qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
27 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = |
25 let |
28 let |
26 val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
29 val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
27 val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms |
30 val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms |
28 in |
31 in |
29 fold_map Quotient_Type.add_quotient_type qty_args2 lthy |
32 fold_map Quotient_Type.add_quotient_type qty_args2 lthy |
30 end |
33 end |
31 |
34 |
32 |
35 |
33 (* defines quotient constants *) |
36 (* defines quotient constants *) |
34 fun qconst_defs qtys consts_specs lthy = |
37 fun define_qconsts qtys consts_specs lthy = |
35 let |
38 let |
36 val (qconst_infos, lthy') = |
39 val (qconst_infos, lthy') = |
37 fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
40 fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy |
38 val phi = ProofContext.export_morphism lthy' lthy |
41 val phi = ProofContext.export_morphism lthy' lthy |
39 in |
42 in |
40 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
43 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
41 end |
44 end |
42 |
45 |
43 |
46 |
44 (* defines the quotient permutations *) |
47 (* defines the quotient permutations and proves pt-class *) |
45 fun qperm_defs qtys full_tnames perm_specs thms thy = |
48 fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws thy = |
46 let |
49 let |
47 val lthy = |
50 val lthy = Class.instantiation (qfull_ty_names, [], @{sort pt}) thy |
48 Class.instantiation (full_tnames, [], @{sort pt}) thy; |
|
49 |
51 |
50 val (_, lthy') = qconst_defs qtys perm_specs lthy; |
52 val (_, lthy') = define_qconsts qtys perm_specs lthy |
51 |
53 |
52 val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; |
54 val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy') raw_perm_laws |
53 |
55 |
54 fun tac _ = |
56 fun tac _ = |
55 Class.intro_classes_tac [] THEN |
57 Class.intro_classes_tac [] THEN |
56 (ALLGOALS (resolve_tac lifted_thms)) |
58 (ALLGOALS (resolve_tac lifted_perm_laws)) |
57 in |
59 in |
58 lthy' |
60 lthy' |
59 |> Class.prove_instantiation_exit tac |
61 |> Class.prove_instantiation_exit tac |
60 end |
62 end |
61 |
63 |
62 |
64 |
|
65 (* defines the size functions and proves size-class *) |
|
66 fun define_qsizes qtys qfull_ty_names size_specs thy = |
|
67 let |
|
68 val lthy = Class.instantiation (qfull_ty_names, [], @{sort size}) thy |
|
69 |
|
70 val (_, lthy') = define_qconsts qtys size_specs lthy |
|
71 |
|
72 fun tac _ = Class.intro_classes_tac [] |
|
73 in |
|
74 lthy' |
|
75 |> Class.prove_instantiation_exit tac |
|
76 end |
|
77 |
63 end (* structure *) |
78 end (* structure *) |
64 |
79 |