equal
deleted
inserted
replaced
1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
3 type maps_info = {mapfun: string, relfun: string} |
3 type maps_info = {mapfun: string, relfun: string} |
|
4 type quotient_info = {qtyp: typ, rtyp: typ, rel: term} |
4 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
5 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
5 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
6 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
6 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
7 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
7 val note: binding * thm -> local_theory -> thm * local_theory |
8 val note: binding * thm -> local_theory -> thm * local_theory |
8 val maps_lookup: theory -> string -> maps_info option |
9 val maps_lookup: theory -> string -> maps_info option |
9 val maps_update: string -> maps_info -> theory -> theory |
10 val maps_update: string -> maps_info -> theory -> theory |
10 val print_quotdata: Proof.context -> unit |
11 val print_quotdata: Proof.context -> unit |
|
12 val quotdata_lookup: theory -> quotient_info list |
|
13 val quotdata_update_thy: (typ * typ * term) -> theory -> theory |
|
14 val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context |
11 end; |
15 end; |
12 |
16 |
13 structure Quotient: QUOTIENT = |
17 structure Quotient: QUOTIENT = |
14 struct |
18 struct |
15 |
19 |
39 val copy = I |
43 val copy = I |
40 val extend = I |
44 val extend = I |
41 fun merge _ = (op @)) |
45 fun merge _ = (op @)) |
42 |
46 |
43 val quotdata_lookup = QuotData.get |
47 val quotdata_lookup = QuotData.get |
44 fun quotdata_update (qty, rty, rel) = |
48 fun quotdata_update_thy (qty, rty, rel) = |
45 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) |
49 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) |
|
50 |
|
51 fun quotdata_update (qty, rty, rel) = ProofContext.theory (quotdata_update_thy (qty, rty, rel)) |
46 |
52 |
47 fun print_quotdata ctxt = |
53 fun print_quotdata ctxt = |
48 let |
54 let |
49 val quots = QuotData.get (ProofContext.theory_of ctxt) |
55 val quots = QuotData.get (ProofContext.theory_of ctxt) |
50 fun prt_quot {qtyp, rtyp, rel} = |
56 fun prt_quot {qtyp, rtyp, rel} = |
172 val rep_name = #Rep_name typedef_info |
178 val rep_name = #Rep_name typedef_info |
173 val abs = Const (abs_name, rep_ty --> abs_ty) |
179 val abs = Const (abs_name, rep_ty --> abs_ty) |
174 val rep = Const (rep_name, abs_ty --> rep_ty) |
180 val rep = Const (rep_name, abs_ty --> rep_ty) |
175 |
181 |
176 (* storing the quot-info *) |
182 (* storing the quot-info *) |
177 val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy) |
183 (*val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy)*) |
178 |
184 |
179 (* ABS and REP definitions *) |
185 (* ABS and REP definitions *) |
180 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
186 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
181 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
187 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
182 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
188 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
209 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
215 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
210 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
216 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
211 val mthdt = Method.Basic (fn _ => mthd) |
217 val mthdt = Method.Basic (fn _ => mthd) |
212 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
218 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
213 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
219 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
214 Expression.Named [ |
220 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] |
215 ("R", rel), |
|
216 ("Abs", abs), |
|
217 ("Rep", rep) |
|
218 ]))] |
|
219 in |
221 in |
220 lthy4 |
222 lthy4 |
221 |> note (quot_thm_name, quot_thm) |
223 |> note (quot_thm_name, quot_thm) |
222 ||>> note (quotient_thm_name, quotient_thm) |
224 ||>> note (quotient_thm_name, quotient_thm) |
223 ||> LocalTheory.theory (fn thy => |
225 ||> LocalTheory.theory (fn thy => |