1 signature QUOTIENT_TYPE = |
1 signature QUOTIENT_TYPE = |
2 sig |
2 sig |
3 exception LIFT_MATCH of string |
|
4 |
|
5 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list |
3 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list |
6 -> Proof.context -> Proof.state |
4 -> Proof.context -> Proof.state |
|
5 |
7 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list |
6 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list |
8 -> Proof.context -> Proof.state |
7 -> Proof.context -> Proof.state |
9 end; |
8 end; |
10 |
9 |
11 structure Quotient_Type: QUOTIENT_TYPE = |
10 structure Quotient_Type: QUOTIENT_TYPE = |
12 struct |
11 struct |
13 |
12 |
14 open Quotient_Info; |
13 open Quotient_Info; |
15 |
|
16 exception LIFT_MATCH of string |
|
17 |
14 |
18 (* wrappers for define, note, Attrib.internal and theorem_i *) |
15 (* wrappers for define, note, Attrib.internal and theorem_i *) |
19 fun define (name, mx, rhs) lthy = |
16 fun define (name, mx, rhs) lthy = |
20 let |
17 let |
21 val ((rhs, (_ , thm)), lthy') = |
18 val ((rhs, (_ , thm)), lthy') = |
228 val goals = map (mk_goal o snd) quot_list |
225 val goals = map (mk_goal o snd) quot_list |
229 |
226 |
230 fun after_qed thms lthy = |
227 fun after_qed thms lthy = |
231 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
228 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
232 |
229 |
233 (* sanity check*) |
230 (* sanity check *) |
234 val _ = map sanity_check quot_list |
231 val _ = map sanity_check quot_list |
235 in |
232 in |
236 theorem after_qed goals lthy |
233 theorem after_qed goals lthy |
237 end |
234 end |
238 |
235 |