25 let |
25 let |
26 val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy |
26 val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy |
27 in |
27 in |
28 (thm', lthy') |
28 (thm', lthy') |
29 end |
29 end |
|
30 |
|
31 fun internal_attr at = Attrib.internal (K at) |
30 |
32 |
31 fun theorem after_qed goals ctxt = |
33 fun theorem after_qed goals ctxt = |
32 let |
34 let |
33 val goals' = map (rpair []) goals |
35 val goals' = map (rpair []) goals |
34 fun after_qed' thms = after_qed (the_single thms) |
36 fun after_qed' thms = after_qed (the_single thms) |
155 (* FIXME: varifyT should not be used *) |
157 (* FIXME: varifyT should not be used *) |
156 (* FIXME: the relation needs to be a string, since its type needs *) |
158 (* FIXME: the relation needs to be a string, since its type needs *) |
157 (* FIXME: to recalculated in for example REGULARIZE *) |
159 (* FIXME: to recalculated in for example REGULARIZE *) |
158 |
160 |
159 (* storing of the equiv_thm under a name *) |
161 (* storing of the equiv_thm under a name *) |
160 val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, []) lthy3 |
162 val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, |
|
163 [internal_attr equiv_rules_add]) lthy3 |
161 |
164 |
162 (* interpretation *) |
165 (* interpretation *) |
163 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
166 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
164 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
167 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
165 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
168 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
177 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
180 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
178 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
181 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
179 in |
182 in |
180 lthy6 |
183 lthy6 |
181 |> note (quot_thm_name, quot_thm, []) |
184 |> note (quot_thm_name, quot_thm, []) |
182 ||>> note (quotient_thm_name, quotient_thm, [Attrib.internal (K quotient_rules_add)]) |
185 ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) |
183 ||> Local_Theory.theory (fn thy => |
186 ||> Local_Theory.theory (fn thy => |
184 let |
187 let |
185 val global_eqns = map exp_term [eqn2i, eqn1i]; |
188 val global_eqns = map exp_term [eqn2i, eqn1i]; |
186 (* Not sure if the following context should not be used *) |
189 (* Not sure if the following context should not be used *) |
187 val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; |
190 val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; |