156 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
156 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
157 (* FIXME: varifyT should not be used *) |
157 (* FIXME: varifyT should not be used *) |
158 (* 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 *) |
159 (* FIXME: to recalculated in for example REGULARIZE *) |
159 (* FIXME: to recalculated in for example REGULARIZE *) |
160 |
160 |
161 (* storing of the equiv_thm under a name *) |
161 in |
162 val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, |
162 lthy3 |
163 [internal_attr equiv_rules_add]) lthy3 |
|
164 |
|
165 (* interpretation *) |
|
166 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
|
167 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
|
168 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
|
169 val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5; |
|
170 val eqn2i = Thm.prop_of (symmetric eqn2pre) |
|
171 |
|
172 val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6)); |
|
173 val exp_term = Morphism.term exp_morphism; |
|
174 val exp = Morphism.thm exp_morphism; |
|
175 |
|
176 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
|
177 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
|
178 val mthdt = Method.Basic (fn _ => mthd) |
|
179 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
180 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
|
181 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
|
182 in |
|
183 lthy6 |
|
184 |> note (quot_thm_name, quot_thm, []) |
163 |> note (quot_thm_name, quot_thm, []) |
185 ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) |
164 ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) |
186 ||> Local_Theory.theory (fn thy => |
165 ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add]) |
187 let |
|
188 val global_eqns = map exp_term [eqn2i, eqn1i]; |
|
189 (* Not sure if the following context should not be used *) |
|
190 val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; |
|
191 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
|
192 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
|
193 end |
166 end |
194 |
167 |
195 |
168 |
196 |
169 |
197 |
170 |