1 |
|
2 |
|
3 |
1 |
4 structure Quotient = |
2 structure Quotient = |
5 struct |
3 struct |
6 |
4 |
7 (* constructs the term lambda (c::rty => bool). EX x. c= rel x *) |
5 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
8 fun typedef_term rel rty lthy = |
6 fun typedef_term rel rty lthy = |
9 let |
7 let |
10 val [x, c] = [("x", rty), ("c", rty --> @{typ bool})] |
8 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
11 |> Variable.variant_frees lthy [rel] |
9 |> Variable.variant_frees lthy [rel] |
12 |> map Free |
10 |> map Free |
13 in |
11 in |
14 lambda c |
12 lambda c |
15 (HOLogic.exists_const rty $ |
13 (HOLogic.exists_const rty $ |
78 Goal.prove lthy [] [] goal |
76 Goal.prove lthy [] [] goal |
79 (K typedef_quotient_thm_tac) |
77 (K typedef_quotient_thm_tac) |
80 end |
78 end |
81 |
79 |
82 (* two wrappers for define and note *) |
80 (* two wrappers for define and note *) |
83 fun make_def (name, mx, rhs) lthy = |
81 fun define (name, mx, rhs) lthy = |
84 let |
82 let |
85 val ((rhs, (_ , thm)), lthy') = |
83 val ((rhs, (_ , thm)), lthy') = |
86 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
84 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
87 in |
85 in |
88 ((rhs, thm), lthy') |
86 ((rhs, thm), lthy') |
89 end |
87 end |
90 |
88 |
91 fun note_thm (name, thm) lthy = |
89 fun note (name, thm) lthy = |
92 let |
90 let |
93 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
91 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
94 in |
92 in |
95 (thm', lthy') |
93 (thm', lthy') |
96 end |
94 end |
115 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
113 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
116 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
114 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
117 val ABS_name = Binding.prefix_name "ABS_" qty_name |
115 val ABS_name = Binding.prefix_name "ABS_" qty_name |
118 val REP_name = Binding.prefix_name "REP_" qty_name |
116 val REP_name = Binding.prefix_name "REP_" qty_name |
119 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
117 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
120 lthy1 |> make_def (ABS_name, NoSyn, ABS_trm) |
118 lthy1 |> define (ABS_name, NoSyn, ABS_trm) |
121 ||>> make_def (REP_name, NoSyn, REP_trm) |
119 ||>> define (REP_name, NoSyn, REP_trm) |
122 |
120 |
123 (* quot_type theorem *) |
121 (* quot_type theorem *) |
124 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
122 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
125 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
123 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
126 |
124 |
149 ("Abs", abs), |
147 ("Abs", abs), |
150 ("Rep", rep) |
148 ("Rep", rep) |
151 ]))] |
149 ]))] |
152 in |
150 in |
153 lthy4 |
151 lthy4 |
154 |> note_thm (quot_thm_name, quot_thm) |
152 |> note (quot_thm_name, quot_thm) |
155 ||>> note_thm (quotient_thm_name, quotient_thm) |
153 ||>> note (quotient_thm_name, quotient_thm) |
156 ||> LocalTheory.theory (fn thy => |
154 ||> LocalTheory.theory (fn thy => |
157 let |
155 let |
158 val global_eqns = map exp_term [eqn2i, eqn1i]; |
156 val global_eqns = map exp_term [eqn2i, eqn1i]; |
159 (* Not sure if the following context should not be used *) |
157 (* Not sure if the following context should not be used *) |
160 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
158 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
163 end |
161 end |
164 |
162 |
165 (* syntax setup *) |
163 (* syntax setup *) |
166 local structure P = OuterParse in |
164 local structure P = OuterParse in |
167 |
165 |
|
166 fun mk_typedef (qty, mx, rty, rel_trm) lthy = |
|
167 let |
|
168 val (qty_name, _) = Term.dest_Type qty |
|
169 |
|
170 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
|
171 val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm) |
|
172 |
|
173 val _ = [Syntax.string_of_term lthy EQUIV_goal, |
|
174 Syntax.string_of_typ lthy (fastype_of rel_trm), |
|
175 Syntax.string_of_typ lthy EQUIV_ty] |
|
176 |> cat_lines |
|
177 |> tracing |
|
178 |
|
179 fun after_qed thms lthy = |
|
180 let |
|
181 val thm = the_single (flat thms) |
|
182 in |
|
183 typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd |
|
184 end |
|
185 in |
|
186 Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy |
|
187 end |
|
188 |
168 val quottype_parser = |
189 val quottype_parser = |
169 (P.type_args -- P.binding) -- |
190 P.typ -- P.opt_infix -- |
170 P.opt_infix -- |
191 (P.$$$ "=" |-- P.typ) -- |
171 (P.$$$ "=" |-- P.term) -- |
|
172 (P.$$$ "/" |-- P.term) |
192 (P.$$$ "/" |-- P.term) |
173 |
193 |
174 (* |
194 fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = |
175 val _ = |
195 let |
176 OuterSyntax.command "quotient" "quotient type definition (requires equivalence proof)" |
196 val qty = Syntax.parse_typ lthy qstr |
177 OuterKeyword.thy_goal |
197 val rty = Syntax.parse_typ lthy rstr |
178 (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); |
198 val rel_trm = Syntax.parse_term lthy rel_str |
179 |
199 |> Syntax.check_term lthy |
180 end; |
200 in |
181 *) |
201 mk_typedef (qty, mx, rty, rel_trm) lthy |
182 |
202 end |
183 end; |
203 |
184 |
204 val _ = OuterKeyword.keyword "/" |
185 end; |
205 |
|
206 val _ = |
|
207 OuterSyntax.local_theory_to_proof "quotient" |
|
208 "quotient type definition (requires equivalence proof)" |
|
209 OuterKeyword.thy_goal (quottype_parser >> mk_typedef_cmd) |
|
210 |
|
211 end; (* local *) |
|
212 |
|
213 end; (* structure *) |
186 |
214 |
187 open Quotient |
215 open Quotient |