140 section {* type definition for the quotient type *} |
140 section {* type definition for the quotient type *} |
141 |
141 |
142 (* the auxiliary data for the quotient types *) |
142 (* the auxiliary data for the quotient types *) |
143 use "quotient_info.ML" |
143 use "quotient_info.ML" |
144 |
144 |
145 declare [[map list = (map, list_rel)]] |
|
146 declare [[map * = (prod_fun, prod_rel)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
147 declare [[map "fun" = (fun_map, fun_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
|
147 (* FIXME: This should throw an exception: |
|
148 declare [[map "option" = (bla, blu)]] |
|
149 *) |
148 |
150 |
149 (* identity quotient is not here as it has to be applied first *) |
151 (* identity quotient is not here as it has to be applied first *) |
150 lemmas [quotient_thm] = |
152 lemmas [quotient_thm] = |
151 fun_quotient list_quotient prod_quotient |
153 fun_quotient prod_quotient |
152 |
154 |
153 lemmas [quotient_rsp] = |
155 lemmas [quotient_rsp] = |
154 quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp |
156 quot_rel_rsp pair_rsp |
155 |
157 |
156 (* fun_map is not here since equivp is not true *) |
158 (* fun_map is not here since equivp is not true *) |
157 (* TODO: option, ... *) |
159 (* TODO: option, ... *) |
158 lemmas [quotient_equiv] = |
160 lemmas [quotient_equiv] = |
159 identity_equivp list_equivp prod_equivp |
161 identity_equivp prod_equivp |
160 |
162 |
161 |
|
162 ML {* maps_lookup @{theory} "List.list" *} |
|
163 ML {* maps_lookup @{theory} "*" *} |
163 ML {* maps_lookup @{theory} "*" *} |
164 ML {* maps_lookup @{theory} "fun" *} |
164 ML {* maps_lookup @{theory} "fun" *} |
165 |
165 |
166 |
166 |
167 (* definition of the quotient types *) |
167 (* definition of the quotient types *) |
215 end |
215 end |
216 *} |
216 *} |
217 |
217 |
218 section {* infrastructure about id *} |
218 section {* infrastructure about id *} |
219 |
219 |
|
220 (* TODO: think where should this be *) |
220 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
221 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
221 by (rule eq_reflection) (simp add: prod_fun_def) |
222 by (rule eq_reflection) (simp add: prod_fun_def) |
222 |
223 |
223 lemma map_id: "map id \<equiv> id" |
224 (* FIXME: make it a list and add map_id to it *) |
224 apply (rule eq_reflection) |
|
225 apply (rule ext) |
|
226 apply (rule_tac list="x" in list.induct) |
|
227 apply (simp_all) |
|
228 done |
|
229 |
|
230 lemmas id_simps = |
225 lemmas id_simps = |
231 fun_map_id[THEN eq_reflection] |
226 fun_map_id[THEN eq_reflection] |
232 id_apply[THEN eq_reflection] |
227 id_apply[THEN eq_reflection] |
233 id_def[THEN eq_reflection,symmetric] |
228 id_def[THEN eq_reflection,symmetric] |
234 prod_fun_id map_id |
229 prod_fun_id |
235 |
230 |
236 ML {* |
231 ML {* |
237 fun simp_ids thm = |
232 fun simp_ids thm = |
238 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
233 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
239 *} |
234 *} |