QuotMain.thy
changeset 108 d3a432bd09f0
parent 107 ab53ddefc542
child 109 386671ef36bd
equal deleted inserted replaced
107:ab53ddefc542 108:d3a432bd09f0
   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