142 end |
142 end |
143 |
143 |
144 |
144 |
145 section {* type definition for the quotient type *} |
145 section {* type definition for the quotient type *} |
146 |
146 |
147 ML {* Toplevel.theory *} |
|
148 |
|
149 use "quotient.ML" |
147 use "quotient.ML" |
150 |
148 |
151 declare [[map list = (map, LIST_REL)]] |
149 declare [[map list = (map, LIST_REL)]] |
152 declare [[map * = (prod_fun, prod_rel)]] |
150 declare [[map * = (prod_fun, prod_rel)]] |
153 declare [[map "fun" = (fun_map, FUN_REL)]] |
151 declare [[map "fun" = (fun_map, FUN_REL)]] |
154 |
152 |
155 ML {* maps_lookup @{theory} "List.list" *} |
153 ML {* maps_lookup @{theory} "List.list" *} |
156 ML {* maps_lookup @{theory} "*" *} |
154 ML {* maps_lookup @{theory} "*" *} |
157 ML {* maps_lookup @{theory} "fun" *} |
155 ML {* maps_lookup @{theory} "fun" *} |
158 |
156 |
|
157 ML {* |
|
158 val quot_def_parser = |
|
159 (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- |
|
160 ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) -- |
|
161 (OuterParse.binding -- |
|
162 Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- |
|
163 OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) |
|
164 *} |
|
165 |
|
166 ML {* |
|
167 fun test (qrtys, (((bind, typstr), mx), (attr, prop))) lthy = lthy |
|
168 *} |
|
169 |
|
170 ML {* |
|
171 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition" |
|
172 OuterKeyword.thy_decl (quot_def_parser >> test) |
|
173 *} |
|
174 |
|
175 (* FIXME: auxiliary function *) |
159 ML {* |
176 ML {* |
160 val no_vars = Thm.rule_attribute (fn context => fn th => |
177 val no_vars = Thm.rule_attribute (fn context => fn th => |
161 let |
178 let |
162 val ctxt = Variable.set_body false (Context.proof_of context); |
179 val ctxt = Variable.set_body false (Context.proof_of context); |
163 val ((_, [th']), _) = Variable.import true [th] ctxt; |
180 val ((_, [th']), _) = Variable.import true [th] ctxt; |