equal
deleted
inserted
replaced
140 qed |
140 qed |
141 |
141 |
142 end |
142 end |
143 |
143 |
144 section {* type definition for the quotient type *} |
144 section {* type definition for the quotient type *} |
145 ML {* Binding.name *} |
|
146 |
|
147 ML {* cat_lines *} |
|
148 |
145 |
149 use "quotient.ML" |
146 use "quotient.ML" |
150 |
147 |
151 ML {* |
|
152 mk_typedef; |
|
153 mk_typedef_cmd; |
|
154 quottype_parser |
|
155 *} |
|
156 |
|
157 ML {* Proof.theorem_i *} |
|
158 |
|
159 term EQUIV |
148 term EQUIV |
160 |
|
161 ML {* quottype_parser *} |
|
162 ML {* OuterSyntax.local_theory_to_proof *} |
|
163 |
149 |
164 ML {* |
150 ML {* |
165 val no_vars = Thm.rule_attribute (fn context => fn th => |
151 val no_vars = Thm.rule_attribute (fn context => fn th => |
166 let |
152 let |
167 val ctxt = Variable.set_body false (Context.proof_of context); |
153 val ctxt = Variable.set_body false (Context.proof_of context); |
181 r_eq: "EQUIV RR" |
167 r_eq: "EQUIV RR" |
182 |
168 |
183 quotient qtrm = "trm" / "RR" |
169 quotient qtrm = "trm" / "RR" |
184 apply(rule r_eq) |
170 apply(rule r_eq) |
185 done |
171 done |
186 |
|
187 (* |
|
188 local_setup {* |
|
189 typedef_main (@{binding "qtrm"}, NoSyn, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd |
|
190 *} |
|
191 *) |
|
192 |
172 |
193 typ qtrm |
173 typ qtrm |
194 term Rep_qtrm |
174 term Rep_qtrm |
195 term REP_qtrm |
175 term REP_qtrm |
196 term Abs_qtrm |
176 term Abs_qtrm |
214 | lam' "'a" "'a trm'" |
194 | lam' "'a" "'a trm'" |
215 |
195 |
216 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool" |
196 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool" |
217 axioms r_eq': "EQUIV R'" |
197 axioms r_eq': "EQUIV R'" |
218 |
198 |
219 (* |
|
220 local_setup {* |
|
221 typedef_main (@{binding "qtrm'"}, NoSyn, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd |
|
222 *} |
|
223 *) |
|
224 |
|
225 quotient "'a qtrm'" = "'a trm'" / "R'" |
199 quotient "'a qtrm'" = "'a trm'" / "R'" |
226 apply(rule r_eq') |
200 apply(rule r_eq') |
227 done |
201 done |
228 |
202 |
229 print_theorems |
203 print_theorems |
241 | ap "t list" |
215 | ap "t list" |
242 | lm "string" "t" |
216 | lm "string" "t" |
243 |
217 |
244 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
218 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
245 axioms t_eq: "EQUIV Rt" |
219 axioms t_eq: "EQUIV Rt" |
246 |
|
247 (* |
|
248 local_setup {* |
|
249 typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd |
|
250 *} |
|
251 *) |
|
252 |
220 |
253 quotient "qt" = "t" / "Rt" |
221 quotient "qt" = "t" / "Rt" |
254 by (rule t_eq) |
222 by (rule t_eq) |
255 |
223 |
256 section {* lifting of constants *} |
224 section {* lifting of constants *} |
438 | lm' "'a" "string \<Rightarrow> ('a t')" |
406 | lm' "'a" "string \<Rightarrow> ('a t')" |
439 |
407 |
440 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool" |
408 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool" |
441 axioms t_eq': "EQUIV Rt'" |
409 axioms t_eq': "EQUIV Rt'" |
442 |
410 |
443 (* |
|
444 local_setup {* |
|
445 typedef_main (@{binding "qt'"}, NoSyn, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd |
|
446 *} |
|
447 *) |
|
448 |
|
449 quotient "'a qt'" = "'a t'" / "Rt'" |
411 quotient "'a qt'" = "'a t'" / "Rt'" |
450 apply(rule t_eq') |
412 apply(rule t_eq') |
451 done |
413 done |
452 |
414 |
453 print_theorems |
415 print_theorems |
488 lemma equiv_list_eq: |
450 lemma equiv_list_eq: |
489 shows "EQUIV list_eq" |
451 shows "EQUIV list_eq" |
490 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
452 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
491 apply(auto intro: list_eq.intros list_eq_refl) |
453 apply(auto intro: list_eq.intros list_eq_refl) |
492 done |
454 done |
493 |
|
494 (* |
|
495 local_setup {* |
|
496 typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
|
497 *} |
|
498 *) |
|
499 |
455 |
500 quotient "'a fset" = "'a list" / "list_eq" |
456 quotient "'a fset" = "'a list" / "list_eq" |
501 apply(rule equiv_list_eq) |
457 apply(rule equiv_list_eq) |
502 done |
458 done |
503 |
459 |