316         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;

   316         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;

   317       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)

   317       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)

   318 end

   318 end

   319 *}

   319 *}

   320 

   320 

   321 section {* various tests for quotient types*}

   322 section {* various tests for quotient types*}

   322 datatype trm =

   323 datatype trm =

   323   var  "nat"

   324   var  "nat"

   324 | app  "trm" "trm"

   325 | app  "trm" "trm"

   325 | lam  "nat" "trm"

   326 | lam  "nat" "trm"

   389 text {* information about map-functions for type-constructor *}

   390 text {* information about map-functions for type-constructor *}

   390 ML {*

   391 ML {*

   391 type typ_info = {mapfun: string}

   392 type typ_info = {mapfun: string}

   392 

   393 

   393 local

   394 local

   395   (type T = typ_info Symtab.table

   396   (type T = typ_info Symtab.table

   396    val empty = Symtab.empty

   397    val empty = Symtab.empty

   397    val extend = I

   399    val extend = I

   398    fun merge _ = Symtab.merge (K true))

   400    fun merge _ = Symtab.merge (K true))

   399 in

   401 in

   400   val lookup = Symtab.lookup o Data.get

   402   val lookup = Symtab.lookup o Data.get

   401   fun update k v = Data.map (Symtab.update (k, v))

   403   fun update k v = Data.map (Symtab.update (k, v))

   402 end

   404 end

   403 *}

   405 *}

   404 

   406 

   405 (* mapfuns for some standard types *)

   407 (* mapfuns for some standard types *)

   406 setup {*

   408 setup {*

   413 

   415 

   414 ML {*

   416 ML {*

   415 datatype flag = absF | repF

   417 datatype flag = absF | repF

   416 

   418 

   417 fun get_fun flag rty qty lthy ty =

   419 fun get_fun flag rty qty lthy ty =

   424     val (otys, ntys) = split_list tys

   426     val (otys, ntys) = split_list tys

   425     val oty = Type (s, otys)

   427     val oty = Type (s, otys)

   426     val nty = Type (s, ntys)

   428     val nty = Type (s, ntys)

   427     val ftys = map (op -->) tys

   429     val ftys = map (op -->) tys

   428   in

   430   in

   430       SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))

   432       SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))

   431     | NONE      => raise ERROR ("no map association for type " ^ s))

   433     | NONE      => raise ERROR ("no map association for type " ^ s))

   432   end

   434   end

   433 

   435 

   434   fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))

   436   fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))

   518 term lm

   520 term lm

   519 thm VR_def AP_def LM_def

   521 thm VR_def AP_def LM_def

   520 term LM

   522 term LM

   521 term VR

   523 term VR

   522 term AP

   524 term AP

   524 

   525 

   525 text {* a test with functions *}

   526 text {* a test with functions *}

   526 datatype 'a t' =

   527 datatype 'a t' =

   527   vr' "string"

   528   vr' "string"

   528 | ap' "('a t') * ('a t')"

   529 | ap' "('a t') * ('a t')"