12 |
12 |
13 val define_qconsts: 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 define_qperms: 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 -> local_theory -> local_theory |
18 |
18 |
19 val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> |
19 val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> |
20 theory -> theory |
20 local_theory -> local_theory |
21 end |
21 end |
22 |
22 |
23 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
23 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
24 struct |
24 struct |
25 |
25 |
43 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
43 (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') |
44 end |
44 end |
45 |
45 |
46 |
46 |
47 (* defines the quotient permutations and proves pt-class *) |
47 (* defines the quotient permutations and proves pt-class *) |
48 fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws thy = |
48 fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws lthy = |
49 let |
49 let |
50 val lthy = Class.instantiation (qfull_ty_names, [], @{sort pt}) thy |
50 val lthy' = |
|
51 lthy |
|
52 |> Local_Theory.exit_global |
|
53 |> Class.instantiation (qfull_ty_names, [], @{sort pt}) |
51 |
54 |
52 val (_, lthy') = define_qconsts qtys perm_specs lthy |
55 val (_, lthy'') = define_qconsts qtys perm_specs lthy' |
53 |
56 |
54 val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy') raw_perm_laws |
57 val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy'') raw_perm_laws |
55 |
58 |
56 fun tac _ = |
59 fun tac _ = |
57 Class.intro_classes_tac [] THEN |
60 Class.intro_classes_tac [] THEN |
58 (ALLGOALS (resolve_tac lifted_perm_laws)) |
61 (ALLGOALS (resolve_tac lifted_perm_laws)) |
59 in |
62 in |
60 lthy' |
63 lthy'' |
61 |> Class.prove_instantiation_exit tac |
64 |> Class.prove_instantiation_exit tac |
|
65 |> Named_Target.theory_init |
62 end |
66 end |
63 |
67 |
64 |
68 |
65 (* defines the size functions and proves size-class *) |
69 (* defines the size functions and proves size-class *) |
66 fun define_qsizes qtys qfull_ty_names size_specs thy = |
70 fun define_qsizes qtys qfull_ty_names size_specs lthy = |
67 let |
71 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 [] |
72 fun tac _ = Class.intro_classes_tac [] |
73 in |
73 in |
74 lthy' |
74 lthy |
|
75 |> Local_Theory.exit_global |
|
76 |> Class.instantiation (qfull_ty_names, [], @{sort size}) |
|
77 |> snd o (define_qconsts qtys size_specs) |
75 |> Class.prove_instantiation_exit tac |
78 |> Class.prove_instantiation_exit tac |
|
79 |> Named_Target.theory_init |
76 end |
80 end |
77 |
81 |
78 end (* structure *) |
82 end (* structure *) |
79 |
83 |