488 

   489 ML {*

   490 fun negF absF = repF

   491   | negF repF = absF

   492 

   493 fun get_fun_noexchange flag (rty, qty) lthy ty =

   494 let

   495   fun get_fun_aux s fs_tys =

   496   let

   497     val (fs, tys) = split_list fs_tys

   498     val (otys, ntys) = split_list tys

   499     val oty = Type (s, otys)

   500     val nty = Type (s, ntys)

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

   502   in

   503    (case (maps_lookup (ProofContext.theory_of lthy) s) of

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

   505     | NONE      => error ("no map association for type " ^ s))

   506   end

   507 

   508   fun get_fun_fun fs_tys =

   509   let

   510     val (fs, tys) = split_list fs_tys

   511     val ([oty1, oty2], [nty1, nty2]) = split_list tys

   512     val oty = nty1 --> oty2

   513     val nty = oty1 --> nty2

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

   515   in

   516     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))

   517   end

   518 

   519   val thy = ProofContext.theory_of lthy

   520 

   521   fun get_const flag (rty, qty) =

   522   let 

   523     val qty_name = Long_Name.base_name (fst (dest_Type qty))

   524   in

   525     case flag of

   526       absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))

   527     | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))

   528   end

   529 

   530   fun mk_identity ty = Abs ("", ty, Bound 0)

   531 

   532 in

   533   if (Sign.typ_instance thy (ty, rty))

   534   then (get_const flag (ty, (exchange_ty lthy rty qty ty)))

   535   else (case ty of

   536           TFree _ => (mk_identity ty, (ty, ty))

   537         | Type (_, []) => (mk_identity ty, (ty, ty))

   538         | Type ("fun" , [ty1, ty2]) =>

   539                  get_fun_fun [get_fun_noexchange (negF flag) (rty, qty) lthy ty1,

   540                  get_fun_noexchange flag (rty, qty) lthy ty2]

   541         | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys)

   542         | _ => raise ERROR ("no type variables"))

   543 end

   544 fun get_fun_noex flag (rty, qty) lthy ty =

   545   fst (get_fun_noexchange flag (rty, qty) lthy ty)

   546 *}

   547 

   624 

   625 (*

   626 consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

   627 axioms Rl_eq: "EQUIV Rl"

   628 

   629 quotient ql = "'a list" / "Rl"

   630   by (rule Rl_eq)

   631 

   632 ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *}

   633 ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *}

   634 ML {* val ttt = term_of @{cterm "f :: bool list \<Rightarrow> nat list"} *}

   635 

   636 ML {*

   637   get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt)

   638 *}

   639 ML {*

   640   get_fun_new absF al aq @{context} (fastype_of ttt)

   641 *}

   642 ML {*

   643   fun mk_abs tm =

   644     let

   645       val ty = fastype_of tm

   646     in (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end

   647   fun mk_repabs tm =

   648     let

   649       val ty = fastype_of tm

   650     in (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end

   651 *}

   652 ML {*

   653   cterm_of @{theory} (mk_repabs ttt)

   654 *}

   655 *)