905 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)

   906 ML {*

   907 fun exchange_ty lthy rty qty ty =

   908   let

   909     val thy = ProofContext.theory_of lthy

   910   in

   911     if Sign.typ_instance thy (ty, rty) then

   912       let

   913         val inst = Sign.typ_match thy (rty, ty) Vartab.empty

   914       in

   915         Envir.subst_type inst qty

   916       end

   917     else

   918       let

   919         val (s, tys) = dest_Type ty

   920       in

   921         Type (s, map (exchange_ty lthy rty qty) tys)

   922       end

   923   end

   924   handle TYPE _ => ty (* for dest_Type *)

   925 *}

   926 

   927 

   928 ML {*

   929 fun find_matching_types rty ty =

   930   if Type.raw_instance (Logic.varifyT ty, rty)

   931   then [ty]

   932   else

   933     let val (s, tys) = dest_Type ty in

   934     flat (map (find_matching_types rty) tys)

   935     end

   936     handle TYPE _ => []

   937 *}

   938 

   939 ML {*

   940 fun negF absF = repF

   941   | negF repF = absF

   942 

   943 fun get_fun flag qenv lthy ty =

   944 let

   945   

   946   fun get_fun_aux s fs =

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

   948       SOME info => list_comb (Const (#mapfun info, dummyT), fs)

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

   950 

   951   fun get_const flag qty =

   952   let 

   953     val thy = ProofContext.theory_of lthy

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

   955   in

   956     case flag of

   957       absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)

   958     | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)

   959   end

   960 

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

   962 

   963 in

   964   if (AList.defined (op=) qenv ty)

   965   then (get_const flag ty)

   966   else (case ty of

   967           TFree _ => mk_identity ty

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

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

   970             let

   971               val fs_ty1 = get_fun (negF flag) qenv lthy ty1

   972               val fs_ty2 = get_fun flag qenv lthy ty2

   973             in  

   974               get_fun_aux "fun" [fs_ty1, fs_ty2]

   975             end 

   976         | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)

   977         | _ => error ("no type variables allowed"))

   978 end

   979 *}

   980 

   981 ML {*

   982 fun get_fun_OLD flag (rty, qty) lthy ty =

   983   let

   984     val tys = find_matching_types rty ty;

   985     val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;

   986     val xchg_ty = exchange_ty lthy rty qty ty

   987   in

   988     get_fun flag qenv lthy xchg_ty

   989   end

   990 *}

   991 

   992 ML {*

   993 fun applic_prs_old lthy rty qty absrep ty =

   994   let

   995     val rty = Logic.varifyT rty;

   996     val qty = Logic.varifyT qty;

   997     fun absty ty =

   998       exchange_ty lthy rty qty ty

   999     fun mk_rep tm =

  1000       let

  1001         val ty = exchange_ty lthy qty rty (fastype_of tm)

  1002       in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;

  1003     fun mk_abs tm =

  1004       let

  1005         val ty = fastype_of tm

  1006       in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end

  1007     val (l, ltl) = Term.strip_type ty;

  1008     val nl = map absty l;

  1009     val vs = map (fn _ => "x") l;

  1010     val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;

  1011     val args = map Free (vfs ~~ nl);

  1012     val lhs = list_comb((Free (fname, nl ---> ltl)), args);

  1013     val rargs = map mk_rep args;

  1014     val f = Free (fname, nl ---> ltl);

  1015     val rhs = mk_abs (list_comb((mk_rep f), rargs));

  1016     val eq = Logic.mk_equals (rhs, lhs);

  1017     val ceq = cterm_of (ProofContext.theory_of lthy') eq;

  1018     val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});

  1019     val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)

  1020     val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;

  1021   in

  1022     singleton (ProofContext.export lthy' lthy) t_id

  1023   end

  1024 *}

  1025