|
1 signature QUOTIENT = |
|
2 sig |
|
3 exception LIFT_MATCH of string |
|
4 |
|
5 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
|
6 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
|
7 |
|
8 end; |
|
9 |
|
10 structure Quotient: QUOTIENT = |
|
11 struct |
|
12 |
|
13 exception LIFT_MATCH of string |
|
14 |
|
15 (* wrappers for define, note and theorem_i *) |
|
16 fun define (name, mx, rhs) lthy = |
|
17 let |
|
18 val ((rhs, (_ , thm)), lthy') = |
|
19 Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy |
|
20 in |
|
21 ((rhs, thm), lthy') |
|
22 end |
|
23 |
|
24 fun note (name, thm, attrs) lthy = |
|
25 let |
|
26 val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy |
|
27 in |
|
28 (thm', lthy') |
|
29 end |
|
30 |
|
31 fun internal_attr at = Attrib.internal (K at) |
|
32 |
|
33 fun theorem after_qed goals ctxt = |
|
34 let |
|
35 val goals' = map (rpair []) goals |
|
36 fun after_qed' thms = after_qed (the_single thms) |
|
37 in |
|
38 Proof.theorem_i NONE after_qed' [goals'] ctxt |
|
39 end |
|
40 |
|
41 |
|
42 (* definition of quotient types *) |
|
43 (********************************) |
|
44 |
|
45 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
|
46 fun typedef_term rel rty lthy = |
|
47 let |
|
48 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
|
49 |> Variable.variant_frees lthy [rel] |
|
50 |> map Free |
|
51 in |
|
52 lambda c |
|
53 (HOLogic.exists_const rty $ |
|
54 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
|
55 end |
|
56 |
|
57 (* makes the new type definitions and proves non-emptyness*) |
|
58 fun typedef_make (qty_name, mx, rel, rty) lthy = |
|
59 let |
|
60 val typedef_tac = |
|
61 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
|
62 rtac @{thm exI}, |
|
63 rtac @{thm exI}, |
|
64 rtac @{thm refl}] |
|
65 val tfrees = map fst (Term.add_tfreesT rty []) |
|
66 in |
|
67 Local_Theory.theory_result |
|
68 (Typedef.add_typedef false NONE |
|
69 (qty_name, tfrees, mx) |
|
70 (typedef_term rel rty lthy) |
|
71 NONE typedef_tac) lthy |
|
72 end |
|
73 |
|
74 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
|
75 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
|
76 let |
|
77 val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}] |
|
78 val rep_thm = #Rep typedef_info |> unfold_mem |
|
79 val rep_inv = #Rep_inverse typedef_info |
|
80 val abs_inv = #Abs_inverse typedef_info |> unfold_mem |
|
81 val rep_inj = #Rep_inject typedef_info |
|
82 in |
|
83 EVERY1 [rtac @{thm QUOT_TYPE.intro}, |
|
84 rtac equiv_thm, |
|
85 rtac rep_thm, |
|
86 rtac rep_inv, |
|
87 rtac abs_inv, |
|
88 rtac @{thm exI}, |
|
89 rtac @{thm refl}, |
|
90 rtac rep_inj] |
|
91 end |
|
92 |
|
93 (* proves the QUOT_TYPE theorem *) |
|
94 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
|
95 let |
|
96 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
|
97 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
|
98 |> Syntax.check_term lthy |
|
99 in |
|
100 Goal.prove lthy [] [] goal |
|
101 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
|
102 end |
|
103 |
|
104 (* proves the quotient theorem *) |
|
105 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
|
106 let |
|
107 val quotient_const = Const (@{const_name "Quotient"}, dummyT) |
|
108 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
|
109 |> Syntax.check_term lthy |
|
110 |
|
111 val typedef_quotient_thm_tac = |
|
112 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), |
|
113 rtac @{thm QUOT_TYPE.Quotient}, |
|
114 rtac quot_type_thm] |
|
115 in |
|
116 Goal.prove lthy [] [] goal |
|
117 (K typedef_quotient_thm_tac) |
|
118 end |
|
119 |
|
120 (* main function for constructing the quotient type *) |
|
121 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
|
122 let |
|
123 (* generates typedef *) |
|
124 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
|
125 |
|
126 (* abs and rep functions *) |
|
127 val abs_ty = #abs_type typedef_info |
|
128 val rep_ty = #rep_type typedef_info |
|
129 val abs_name = #Abs_name typedef_info |
|
130 val rep_name = #Rep_name typedef_info |
|
131 val abs = Const (abs_name, rep_ty --> abs_ty) |
|
132 val rep = Const (rep_name, abs_ty --> rep_ty) |
|
133 |
|
134 (* ABS and REP definitions *) |
|
135 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
|
136 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
|
137 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
|
138 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
|
139 val ABS_name = Binding.prefix_name "ABS_" qty_name |
|
140 val REP_name = Binding.prefix_name "REP_" qty_name |
|
141 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
|
142 lthy1 |> define (ABS_name, NoSyn, ABS_trm) |
|
143 ||>> define (REP_name, NoSyn, REP_trm) |
|
144 |
|
145 (* quot_type theorem *) |
|
146 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
|
147 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
|
148 |
|
149 (* quotient theorem *) |
|
150 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
|
151 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
|
152 |
|
153 (* storing the quot-info *) |
|
154 val qty_str = fst (Term.dest_Type abs_ty) |
|
155 val lthy3 = quotdata_update qty_str |
|
156 (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 |
|
157 (* FIXME: varifyT should not be used *) |
|
158 (* FIXME: the relation needs to be a string, since its type needs *) |
|
159 (* FIXME: to recalculated in for example REGULARIZE *) |
|
160 |
|
161 (* storing of the equiv_thm under a name *) |
|
162 val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, |
|
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, []) |
|
185 ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add]) |
|
186 ||> Local_Theory.theory (fn thy => |
|
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 |
|
194 |
|
195 |
|
196 |
|
197 |
|
198 (* interface and syntax setup *) |
|
199 |
|
200 (* the ML-interface takes a list of 4-tuples consisting of *) |
|
201 (* *) |
|
202 (* - the name of the quotient type *) |
|
203 (* - its mixfix annotation *) |
|
204 (* - the type to be quotient *) |
|
205 (* - the relation according to which the type is quotient *) |
|
206 |
|
207 fun quotient_type quot_list lthy = |
|
208 let |
|
209 fun mk_goal (rty, rel) = |
|
210 let |
|
211 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
|
212 in |
|
213 HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) |
|
214 end |
|
215 |
|
216 val goals = map (mk_goal o snd) quot_list |
|
217 |
|
218 fun after_qed thms lthy = |
|
219 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
|
220 in |
|
221 theorem after_qed goals lthy |
|
222 end |
|
223 |
|
224 fun quotient_type_cmd spec lthy = |
|
225 let |
|
226 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
|
227 let |
|
228 val qty_name = Binding.name qty_str |
|
229 val rty = Syntax.read_typ lthy rty_str |
|
230 val rel = Syntax.read_term lthy rel_str |
|
231 in |
|
232 ((qty_name, mx), (rty, rel)) |
|
233 end |
|
234 in |
|
235 quotient_type (map parse_spec spec) lthy |
|
236 end |
|
237 |
|
238 val quotspec_parser = |
|
239 OuterParse.and_list1 |
|
240 (OuterParse.short_ident -- OuterParse.opt_infix -- |
|
241 (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
|
242 (OuterParse.$$$ "/" |-- OuterParse.term)) |
|
243 |
|
244 val _ = OuterKeyword.keyword "/" |
|
245 |
|
246 val _ = |
|
247 OuterSyntax.local_theory_to_proof "quotient" |
|
248 "quotient type definitions (requires equivalence proofs)" |
|
249 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
|
250 |
|
251 end; (* structure *) |
|
252 |
|
253 open Quotient |