379 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
379 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
380 make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
380 make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
381 make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
381 make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
382 *} |
382 *} |
383 |
383 |
384 (*consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t" |
384 (* |
|
385 |
|
386 Christian: |
|
387 |
|
388 When "get_fun" gets a function type, it should call itself |
|
389 recursively for the right side of the arrow and call itself |
|
390 recursively with the flag swapped for left side. This way |
|
391 for a simple (qt\<Rightarrow>qt) function type it will make a (REP--->ABS). |
|
392 |
|
393 Examples of what it should do from Peter's code follow: |
|
394 |
|
395 - mkabs ``\x : 'a list.x``; |
|
396 > val it = ``(finite_set_REP --> finite_set_ABS) (\x. x)`` : term |
|
397 - mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``; |
|
398 > val it = ``((finite_set_ABS --> finite_set_REP) --> finite_set_ABS) (\x. y)`` |
|
399 - mkabs ``\x : (('a list -> 'a list) -> 'a list). y : 'a list``; |
|
400 > val it = |
|
401 ``(((finite_set_REP --> finite_set_ABS) --> finite_set_REP) --> |
|
402 finite_set_ABS) (\x. y)`` : term |
|
403 |
|
404 It currently doesn't do it, the following code generates a wrong |
|
405 function and the second ML block fails to typecheck for this reason: |
|
406 |
|
407 *) |
385 |
408 |
386 ML {* |
409 ML {* |
387 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
410 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
388 |> fst |
411 |> fst |
389 |> Syntax.string_of_term @{context} |
412 |> Syntax.string_of_term @{context} |
390 |> writeln |
413 |> writeln |
391 *} |
414 *} |
392 |
415 |
|
416 ML {* |
|
417 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"} |
|
418 |> fst |
|
419 |> cterm_of @{theory} |
|
420 *} |
|
421 |
|
422 (* The followng also fails due to incorrect types... *) |
|
423 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t" |
393 local_setup {* |
424 local_setup {* |
394 fn lthy => (Toplevel.program (fn () => |
425 fn lthy => (Toplevel.program (fn () => |
395 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
426 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
396 )) |> snd |
427 )) |> snd |
397 *} |
428 *} |
398 *) |
429 |
399 |
430 |
400 term vr' |
431 term vr' |
401 term ap' |
432 term ap' |
402 term ap' |
433 term ap' |
403 thm VR'_def AP'_def LM'_def |
434 thm VR'_def AP'_def LM'_def |