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 |
5 |
6 |
6 locale QUOT_TYPE = |
7 locale QUOT_TYPE = |
7 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
8 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
8 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
9 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
9 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
10 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
143 |
144 |
144 section {* type definition for the quotient type *} |
145 section {* type definition for the quotient type *} |
145 |
146 |
146 use "quotient.ML" |
147 use "quotient.ML" |
147 |
148 |
|
149 |
148 ML {* |
150 ML {* |
149 val no_vars = Thm.rule_attribute (fn context => fn th => |
151 val no_vars = Thm.rule_attribute (fn context => fn th => |
150 let |
152 let |
151 val ctxt = Variable.set_body false (Context.proof_of context); |
153 val ctxt = Variable.set_body false (Context.proof_of context); |
152 val ((_, [th']), _) = Variable.import true [th] ctxt; |
154 val ((_, [th']), _) = Variable.import true [th] ctxt; |
221 |
223 |
222 section {* lifting of constants *} |
224 section {* lifting of constants *} |
223 |
225 |
224 text {* information about map-functions for type-constructor *} |
226 text {* information about map-functions for type-constructor *} |
225 ML {* |
227 ML {* |
226 type typ_info = {mapfun: string} |
228 type typ_info = {mapfun: string, relfun: string} |
227 |
229 |
228 local |
230 local |
229 structure Data = TheoryDataFun |
231 structure Data = TheoryDataFun |
230 (type T = typ_info Symtab.table |
232 (type T = typ_info Symtab.table |
231 val empty = Symtab.empty |
233 val empty = Symtab.empty |
238 end |
240 end |
239 *} |
241 *} |
240 |
242 |
241 (* mapfuns for some standard types *) |
243 (* mapfuns for some standard types *) |
242 setup {* |
244 setup {* |
243 update @{type_name "list"} {mapfun = @{const_name "map"}} #> |
245 update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
244 update @{type_name "*"} {mapfun = @{const_name "prod_fun"}} #> |
246 update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = "???"} #> |
245 update @{type_name "fun"} {mapfun = @{const_name "fun_map"}} |
247 update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
246 *} |
248 *} |
247 |
249 |
248 ML {* lookup @{theory} @{type_name list} *} |
250 ML {* lookup @{theory} @{type_name list} *} |
249 |
251 |
250 ML {* |
252 ML {* |
283 ) |
285 ) |
284 end |
286 end |
285 *} |
287 *} |
286 |
288 |
287 ML {* |
289 ML {* |
288 get_fun repF @{typ t} @{typ qt} @{context} @{typ "t * nat"} |
290 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((t \<Rightarrow> t) list) * nat"} |
289 |> fst |
291 |> fst |
290 |> Syntax.string_of_term @{context} |
292 |> Syntax.string_of_term @{context} |
291 |> writeln |
293 |> writeln |
292 *} |
294 *} |
293 |
295 |
295 get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"} |
297 get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"} |
296 |> fst |
298 |> fst |
297 |> Syntax.string_of_term @{context} |
299 |> Syntax.string_of_term @{context} |
298 |> writeln |
300 |> writeln |
299 *} |
301 *} |
|
302 |
|
303 (* |
|
304 ML {* |
|
305 fun tyRel ty rty rel lthy = |
|
306 if ty = rty |
|
307 then rel |
|
308 else (case ty of |
|
309 Type (s, tys) => |
|
310 (case (lookup (ProofContext.theory_of lthy) s) of |
|
311 SOME (info) => list_comb (Const (#relfun info, ?????), map (tyRel ???) tys) |
|
312 NONE => (op =):: tys |
|
313 ) |
|
314 | _ => (op =):: ty) |
|
315 *} |
|
316 |
|
317 ML {* |
|
318 |
|
319 fun regularise trm \<Rightarrow> new_trm |
|
320 (case trm of |
|
321 ?? |
|
322 ) |
|
323 *} |
|
324 |
|
325 fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
|
326 trm == new_trm |
|
327 *) |
300 |
328 |
301 text {* produces the definition for a lifted constant *} |
329 text {* produces the definition for a lifted constant *} |
302 ML {* |
330 ML {* |
303 fun get_const_def nconst oconst rty qty lthy = |
331 fun get_const_def nconst oconst rty qty lthy = |
304 let |
332 let |