equal
deleted
inserted
replaced
1 theory QuotMain |
1 theory QuotMain |
2 imports QuotScript QuotList Prove |
2 imports QuotScript QuotList Prove |
3 uses ("quotient.ML") |
3 uses ("quotient.ML") |
4 begin |
4 begin |
5 |
|
6 |
5 |
7 locale QUOT_TYPE = |
6 locale QUOT_TYPE = |
8 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
7 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
9 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
8 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
10 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
9 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
141 qed |
140 qed |
142 |
141 |
143 end |
142 end |
144 |
143 |
145 section {* type definition for the quotient type *} |
144 section {* type definition for the quotient type *} |
|
145 ML {* Binding.name *} |
|
146 |
|
147 ML {* cat_lines *} |
146 |
148 |
147 use "quotient.ML" |
149 use "quotient.ML" |
148 |
150 |
|
151 ML {* |
|
152 mk_typedef; |
|
153 mk_typedef_cmd; |
|
154 quottype_parser |
|
155 *} |
|
156 |
|
157 ML {* Proof.theorem_i *} |
|
158 |
|
159 term EQUIV |
|
160 |
|
161 ML {* quottype_parser *} |
|
162 ML {* OuterSyntax.local_theory_to_proof *} |
149 |
163 |
150 ML {* |
164 ML {* |
151 val no_vars = Thm.rule_attribute (fn context => fn th => |
165 val no_vars = Thm.rule_attribute (fn context => fn th => |
152 let |
166 let |
153 val ctxt = Variable.set_body false (Context.proof_of context); |
167 val ctxt = Variable.set_body false (Context.proof_of context); |
164 axiomatization |
178 axiomatization |
165 RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" |
179 RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" |
166 where |
180 where |
167 r_eq: "EQUIV RR" |
181 r_eq: "EQUIV RR" |
168 |
182 |
|
183 quotient qtrm = "trm" / "RR" |
|
184 apply(rule r_eq) |
|
185 done |
|
186 |
|
187 (* |
169 local_setup {* |
188 local_setup {* |
170 typedef_main (@{binding "qtrm"}, NoSyn, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd |
189 typedef_main (@{binding "qtrm"}, NoSyn, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd |
171 *} |
190 *} |
172 |
191 *) |
|
192 |
|
193 typ qtrm |
173 term Rep_qtrm |
194 term Rep_qtrm |
174 term REP_qtrm |
195 term REP_qtrm |
175 term Abs_qtrm |
196 term Abs_qtrm |
176 term ABS_qtrm |
197 term ABS_qtrm |
177 thm QUOT_TYPE_qtrm |
198 thm QUOT_TYPE_qtrm |
178 thm QUOTIENT_qtrm |
199 thm QUOTIENT_qtrm |
|
200 thm REP_qtrm_def |
179 |
201 |
180 (* Test interpretation *) |
202 (* Test interpretation *) |
181 thm QUOT_TYPE_I_qtrm.thm11 |
203 thm QUOT_TYPE_I_qtrm.thm11 |
182 thm QUOT_TYPE.thm11 |
204 thm QUOT_TYPE.thm11 |
183 |
205 |
192 | lam' "'a" "'a trm'" |
214 | lam' "'a" "'a trm'" |
193 |
215 |
194 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool" |
216 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool" |
195 axioms r_eq': "EQUIV R'" |
217 axioms r_eq': "EQUIV R'" |
196 |
218 |
197 |
219 (* |
198 local_setup {* |
220 local_setup {* |
199 typedef_main (@{binding "qtrm'"}, NoSyn, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd |
221 typedef_main (@{binding "qtrm'"}, NoSyn, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd |
200 *} |
222 *} |
|
223 *) |
|
224 |
|
225 quotient "'a qtrm'" = "'a trm'" / "R'" |
|
226 apply(rule r_eq') |
|
227 done |
201 |
228 |
202 print_theorems |
229 print_theorems |
203 |
230 |
204 term ABS_qtrm' |
231 term ABS_qtrm' |
205 term REP_qtrm' |
232 term REP_qtrm' |
215 | lm "string" "t" |
242 | lm "string" "t" |
216 |
243 |
217 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
244 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
218 axioms t_eq: "EQUIV Rt" |
245 axioms t_eq: "EQUIV Rt" |
219 |
246 |
|
247 (* |
220 local_setup {* |
248 local_setup {* |
221 typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd |
249 typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd |
222 *} |
250 *} |
|
251 *) |
|
252 |
|
253 quotient "qt" = "t" / "Rt" |
|
254 by (rule t_eq) |
223 |
255 |
224 section {* lifting of constants *} |
256 section {* lifting of constants *} |
225 |
257 |
226 text {* information about map-functions for type-constructor *} |
258 text {* information about map-functions for type-constructor *} |
227 ML {* |
259 ML {* |
379 val oconst_ty = fastype_of oconst |
411 val oconst_ty = fastype_of oconst |
380 val nconst_ty = exchange_ty rty qty oconst_ty |
412 val nconst_ty = exchange_ty rty qty oconst_ty |
381 val nconst = Const (Binding.name_of nconst_bname, nconst_ty) |
413 val nconst = Const (Binding.name_of nconst_bname, nconst_ty) |
382 val def_trm = get_const_def nconst oconst rty qty lthy |
414 val def_trm = get_const_def nconst oconst rty qty lthy |
383 in |
415 in |
384 make_def (nconst_bname, mx, def_trm) lthy |
416 define (nconst_bname, mx, def_trm) lthy |
385 end |
417 end |
386 *} |
418 *} |
387 |
419 |
388 local_setup {* |
420 local_setup {* |
389 make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> |
421 make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> |
406 | lm' "'a" "string \<Rightarrow> ('a t')" |
438 | lm' "'a" "string \<Rightarrow> ('a t')" |
407 |
439 |
408 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool" |
440 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool" |
409 axioms t_eq': "EQUIV Rt'" |
441 axioms t_eq': "EQUIV Rt'" |
410 |
442 |
411 |
443 (* |
412 local_setup {* |
444 local_setup {* |
413 typedef_main (@{binding "qt'"}, NoSyn, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd |
445 typedef_main (@{binding "qt'"}, NoSyn, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd |
414 *} |
446 *} |
|
447 *) |
|
448 |
|
449 quotient "'a qt'" = "'a t'" / "Rt'" |
|
450 apply(rule t_eq') |
|
451 done |
415 |
452 |
416 print_theorems |
453 print_theorems |
417 |
454 |
418 local_setup {* |
455 local_setup {* |
419 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
456 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
452 shows "EQUIV list_eq" |
489 shows "EQUIV list_eq" |
453 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
490 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
454 apply(auto intro: list_eq.intros list_eq_refl) |
491 apply(auto intro: list_eq.intros list_eq_refl) |
455 done |
492 done |
456 |
493 |
|
494 (* |
457 local_setup {* |
495 local_setup {* |
458 typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
496 typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
459 *} |
497 *} |
|
498 *) |
|
499 |
|
500 quotient "'a fset" = "'a list" / "list_eq" |
|
501 apply(rule equiv_list_eq) |
|
502 done |
460 |
503 |
461 print_theorems |
504 print_theorems |
462 |
505 |
463 typ "'a fset" |
506 typ "'a fset" |
464 thm "Rep_fset" |
507 thm "Rep_fset" |