equal
deleted
inserted
replaced
135 end |
135 end |
136 |
136 |
137 |
137 |
138 section {* type definition for the quotient type *} |
138 section {* type definition for the quotient type *} |
139 |
139 |
140 ML {* Proof.theorem_i NONE *} |
|
141 |
|
142 use "quotient.ML" |
140 use "quotient.ML" |
143 |
141 |
144 declare [[map list = (map, LIST_REL)]] |
142 declare [[map list = (map, LIST_REL)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
143 declare [[map * = (prod_fun, prod_rel)]] |
146 declare [[map "fun" = (fun_map, FUN_REL)]] |
144 declare [[map "fun" = (fun_map, FUN_REL)]] |
147 |
145 |
148 ML {* maps_lookup @{theory} "List.list" *} |
146 ML {* maps_lookup @{theory} "List.list" *} |
149 ML {* maps_lookup @{theory} "*" *} |
147 ML {* maps_lookup @{theory} "*" *} |
150 ML {* maps_lookup @{theory} "fun" *} |
148 ML {* maps_lookup @{theory} "fun" *} |
|
149 |
|
150 ML {* |
|
151 fun matches ty1 ty2 = |
|
152 Type.raw_instance (ty1, Logic.varifyT ty2) |
|
153 *} |
|
154 |
|
155 |
151 |
156 |
152 ML {* |
157 ML {* |
153 val quot_def_parser = |
158 val quot_def_parser = |
154 (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- |
159 (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- |
155 ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- |
160 ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- |
161 ML {* |
166 ML {* |
162 fun test (qrtys, (((bind, typstr), mx), (attr, prop))) lthy = lthy |
167 fun test (qrtys, (((bind, typstr), mx), (attr, prop))) lthy = lthy |
163 *} |
168 *} |
164 |
169 |
165 ML {* |
170 ML {* |
166 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition" |
171 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
167 OuterKeyword.thy_decl (quot_def_parser >> test) |
172 OuterKeyword.thy_decl (quot_def_parser >> test) |
168 *} |
173 *} |
169 |
174 |
170 (* FIXME: auxiliary function *) |
175 (* FIXME: auxiliary function *) |
171 ML {* |
176 ML {* |