43 val copy = I |
43 val copy = I |
44 val extend = I |
44 val extend = I |
45 fun merge _ = (op @)) |
45 fun merge _ = (op @)) |
46 |
46 |
47 val quotdata_lookup = QuotData.get |
47 val quotdata_lookup = QuotData.get |
|
48 |
48 fun quotdata_update_thy (qty, rty, rel) = |
49 fun quotdata_update_thy (qty, rty, rel) = |
49 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) |
50 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) |
50 |
51 |
51 fun quotdata_update (qty, rty, rel) = ProofContext.theory (quotdata_update_thy (qty, rty, rel)) |
52 fun quotdata_update (qty, rty, rel) = |
|
53 ProofContext.theory (quotdata_update_thy (qty, rty, rel)) |
52 |
54 |
53 fun print_quotdata ctxt = |
55 fun print_quotdata ctxt = |
54 let |
56 let |
55 val quots = QuotData.get (ProofContext.theory_of ctxt) |
57 val quots = QuotData.get (ProofContext.theory_of ctxt) |
56 fun prt_quot {qtyp, rtyp, rel} = |
58 fun prt_quot {qtyp, rtyp, rel} = |
176 val rep_ty = #rep_type typedef_info |
178 val rep_ty = #rep_type typedef_info |
177 val abs_name = #Abs_name typedef_info |
179 val abs_name = #Abs_name typedef_info |
178 val rep_name = #Rep_name typedef_info |
180 val rep_name = #Rep_name typedef_info |
179 val abs = Const (abs_name, rep_ty --> abs_ty) |
181 val abs = Const (abs_name, rep_ty --> abs_ty) |
180 val rep = Const (rep_name, abs_ty --> rep_ty) |
182 val rep = Const (rep_name, abs_ty --> rep_ty) |
181 |
|
182 (* storing the quot-info *) |
|
183 (*val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy)*) |
|
184 |
183 |
185 (* ABS and REP definitions *) |
184 (* ABS and REP definitions *) |
186 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
185 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
187 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
186 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
188 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
187 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
199 |
198 |
200 (* quotient theorem *) |
199 (* quotient theorem *) |
201 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
200 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
202 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
201 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
203 |
202 |
|
203 |
|
204 (* storing the quot-info *) |
|
205 val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2 |
|
206 |
204 (* interpretation *) |
207 (* interpretation *) |
205 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
208 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
206 val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2; |
209 val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; |
207 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
210 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
208 val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3; |
211 val ((_, [eqn2pre]), lthy5) = Variable.import true [REP_def] lthy4; |
209 val eqn2i = Thm.prop_of (symmetric eqn2pre) |
212 val eqn2i = Thm.prop_of (symmetric eqn2pre) |
210 |
213 |
211 val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4)); |
214 val exp_morphism = ProofContext.export_morphism lthy5 (ProofContext.init (ProofContext.theory_of lthy5)); |
212 val exp_term = Morphism.term exp_morphism; |
215 val exp_term = Morphism.term exp_morphism; |
213 val exp = Morphism.thm exp_morphism; |
216 val exp = Morphism.thm exp_morphism; |
214 |
217 |
215 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
218 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
216 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
219 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
217 val mthdt = Method.Basic (fn _ => mthd) |
220 val mthdt = Method.Basic (fn _ => mthd) |
218 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
221 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
219 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
222 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
220 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
223 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
221 in |
224 in |
222 lthy4 |
225 lthy5 |
223 |> note (quot_thm_name, quot_thm) |
226 |> note (quot_thm_name, quot_thm) |
224 ||>> note (quotient_thm_name, quotient_thm) |
227 ||>> note (quotient_thm_name, quotient_thm) |
225 ||> LocalTheory.theory (fn thy => |
228 ||> LocalTheory.theory (fn thy => |
226 let |
229 let |
227 val global_eqns = map exp_term [eqn2i, eqn1i]; |
230 val global_eqns = map exp_term [eqn2i, eqn1i]; |
228 (* Not sure if the following context should not be used *) |
231 (* Not sure if the following context should not be used *) |
229 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
232 val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5; |
230 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
233 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
231 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
234 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
232 end |
235 end |
233 |
236 |
234 |
237 |