1 (* Code for getting the goal *)

     2 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})

     3 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}

     4 

     5 

   495 ML {*

   496 fun applic_prs lthy absrep (rty, qty) =

   497   let

   498     fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;

   499     fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;

   500     val (raty, rgty) = Term.strip_type rty;

   501     val (qaty, qgty) = Term.strip_type qty;

   502     val vs = map (fn _ => "x") qaty;

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

   504     val f = Free (fname, qaty ---> qgty);

   505     val args = map Free (vfs ~~ qaty);

   506     val rhs = list_comb(f, args);

   507     val largs = map2 mk_rep (raty ~~ qaty) args;

   508     val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));

   509     val llhs = Syntax.check_term lthy lhs;

   510     val eq = Logic.mk_equals (llhs, rhs);

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

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

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

   514     val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;

   515   in

   516     singleton (ProofContext.export lthy' lthy) t_id

   517   end

   518 *}

   519 

   520 ML {*

   521 fun find_aps_all rtm qtm =

   522   case (rtm, qtm) of

   523     (Abs(_, T1, s1), Abs(_, T2, s2)) =>

   524       find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))

   525   | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>

   526       let

   527         val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)

   528       in

   529         if T1 = T2 then sub else (T1, T2) :: sub

   530       end

   531   | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)

   532   | _ => [];

   533 

   534 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)

   535 *}

   536 

   537