3 exception LIFT_MATCH of string |
3 exception LIFT_MATCH of string |
4 |
4 |
5 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
5 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
6 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
6 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
7 |
7 |
8 val note: binding * thm -> local_theory -> thm * local_theory |
|
9 end; |
8 end; |
10 |
9 |
11 structure Quotient: QUOTIENT = |
10 structure Quotient: QUOTIENT = |
12 struct |
11 struct |
13 |
12 |
20 Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy |
19 Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy |
21 in |
20 in |
22 ((rhs, thm), lthy') |
21 ((rhs, thm), lthy') |
23 end |
22 end |
24 |
23 |
25 fun note (name, thm) lthy = |
24 fun note (name, thm, attrs) lthy = |
26 let |
25 let |
27 val ((_,[thm']), lthy') = Local_Theory.note ((name, []), [thm]) lthy |
26 val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy |
28 in |
27 in |
29 (thm', lthy') |
28 (thm', lthy') |
30 end |
29 end |
31 |
30 |
32 fun theorem after_qed goals ctxt = |
31 fun theorem after_qed goals ctxt = |
156 (* FIXME: varifyT should not be used *) |
155 (* FIXME: varifyT should not be used *) |
157 (* FIXME: the relation needs to be a string, since its type needs *) |
156 (* FIXME: the relation needs to be a string, since its type needs *) |
158 (* FIXME: to recalculated in for example REGULARIZE *) |
157 (* FIXME: to recalculated in for example REGULARIZE *) |
159 |
158 |
160 (* storing of the equiv_thm under a name *) |
159 (* storing of the equiv_thm under a name *) |
161 val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3 |
160 val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm, []) lthy3 |
162 |
161 |
163 (* interpretation *) |
162 (* interpretation *) |
164 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
163 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
165 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
164 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
166 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
165 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
177 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
176 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
178 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
177 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
179 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
178 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
180 in |
179 in |
181 lthy6 |
180 lthy6 |
182 |> note (quot_thm_name, quot_thm) |
181 |> note (quot_thm_name, quot_thm, []) |
183 ||>> note (quotient_thm_name, quotient_thm) |
182 ||>> note (quotient_thm_name, quotient_thm, [Attrib.internal (K quotient_rules_add)]) |
184 ||> Local_Theory.theory (fn thy => |
183 ||> Local_Theory.theory (fn thy => |
185 let |
184 let |
186 val global_eqns = map exp_term [eqn2i, eqn1i]; |
185 val global_eqns = map exp_term [eqn2i, eqn1i]; |
187 (* Not sure if the following context should not be used *) |
186 (* Not sure if the following context should not be used *) |
188 val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; |
187 val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; |