10 structure Quotient: QUOTIENT = |
10 structure Quotient: QUOTIENT = |
11 struct |
11 struct |
12 |
12 |
13 exception LIFT_MATCH of string |
13 exception LIFT_MATCH of string |
14 |
14 |
15 (* wrappers for define, note and theorem_i *) |
15 (* wrappers for define, note, Attrib.internal and theorem_i *) |
16 fun define (name, mx, rhs) lthy = |
16 fun define (name, mx, rhs) lthy = |
17 let |
17 let |
18 val ((rhs, (_ , thm)), lthy') = |
18 val ((rhs, (_ , thm)), lthy') = |
19 Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy |
19 Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy |
20 in |
20 in |
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 |
30 |
31 fun internal_attr at = Attrib.internal (K at) |
31 fun intern_attr at = Attrib.internal (K at) |
32 |
32 |
33 fun theorem after_qed goals ctxt = |
33 fun theorem after_qed goals ctxt = |
34 let |
34 let |
35 val goals' = map (rpair []) goals |
35 val goals' = map (rpair []) goals |
36 fun after_qed' thms = after_qed (the_single thms) |
36 fun after_qed' thms = after_qed (the_single thms) |
115 in |
115 in |
116 Goal.prove lthy [] [] goal |
116 Goal.prove lthy [] [] goal |
117 (K typedef_quotient_thm_tac) |
117 (K typedef_quotient_thm_tac) |
118 end |
118 end |
119 |
119 |
120 (* main function for constructing the quotient type *) |
120 (* main function for constructing a quotient type *) |
121 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
121 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
122 let |
122 let |
123 (* generates typedef *) |
123 (* generates the typedef *) |
124 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
124 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
125 |
125 |
126 (* abs and rep functions *) |
126 (* abs and rep functions from the typedef *) |
127 val abs_ty = #abs_type typedef_info |
127 val abs_ty = #abs_type typedef_info |
128 val rep_ty = #rep_type typedef_info |
128 val rep_ty = #rep_type typedef_info |
129 val abs_name = #Abs_name typedef_info |
129 val abs_name = #Abs_name typedef_info |
130 val rep_name = #Rep_name typedef_info |
130 val rep_name = #Rep_name typedef_info |
131 val abs = Const (abs_name, rep_ty --> abs_ty) |
131 val abs = Const (abs_name, rep_ty --> abs_ty) |
132 val rep = Const (rep_name, abs_ty --> rep_ty) |
132 val rep = Const (rep_name, abs_ty --> rep_ty) |
133 |
133 |
134 (* ABS and REP definitions *) |
134 (* more abstract ABS and REP definitions *) |
135 val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT ) |
135 val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT ) |
136 val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT ) |
136 val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT ) |
137 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
137 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
138 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
138 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
139 val ABS_name = Binding.prefix_name "abs_" qty_name |
139 val ABS_name = Binding.prefix_name "abs_" qty_name |
153 (* storing the quot-info *) |
153 (* storing the quot-info *) |
154 val qty_str = fst (Term.dest_Type abs_ty) |
154 val qty_str = fst (Term.dest_Type abs_ty) |
155 val lthy3 = quotdata_update qty_str |
155 val lthy3 = quotdata_update qty_str |
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 can be any term, that later maybe needs to be given *) |
159 (* FIXME: to recalculated in for example REGULARIZE *) |
159 (* FIXME: a different type (in regularize_trm); how should tis be done? *) |
160 |
160 |
161 in |
161 in |
162 lthy3 |
162 lthy3 |
163 |> note (quot_thm_name, quot_thm, []) |
163 |> note (quot_thm_name, quot_thm, []) |
164 ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) |
164 ||>> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
165 ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add]) |
165 ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add]) |
166 end |
166 end |
167 |
167 |
168 |
168 |
169 |
169 |
170 |
170 |