diff --git a/thys/Applicative_Lifting/applicative.ML b/thys/Applicative_Lifting/applicative.ML
--- a/thys/Applicative_Lifting/applicative.ML
+++ b/thys/Applicative_Lifting/applicative.ML
@@ -1,1368 +1,1370 @@
 (* Author: Joshua Schneider, ETH Zurich *)
 
 signature APPLICATIVE =
 sig
   type afun
   val intern: Context.generic -> xstring -> string
   val extern: Context.generic -> string -> xstring
   val afun_of_generic: Context.generic -> string -> afun
   val afun_of: Proof.context -> string -> afun
   val afuns_of_term_generic: Context.generic -> term -> afun list
   val afuns_of_term: Proof.context -> term -> afun list
   val afuns_of_typ_generic: Context.generic -> typ -> afun list
   val afuns_of_typ: Proof.context -> typ -> afun list
   val name_of_afun: afun -> binding
   val unfolds_of_afun: afun -> thm list
 
   type afun_inst
   val match_afun_inst: Proof.context -> afun -> term * int -> afun_inst
   val import_afun_inst: afun -> Proof.context -> afun_inst * Proof.context
   val inner_sort_of: afun_inst -> sort
   val mk_type: afun_inst -> typ -> typ
   val mk_pure: afun_inst -> typ -> term
   val lift_term: afun_inst -> term -> term
   val mk_ap: afun_inst -> typ * typ -> term
   val mk_comb: afun_inst -> typ -> term * term -> term
   val mk_set: afun_inst -> typ -> term
   val dest_type: Proof.context -> afun_inst -> typ -> typ option
   val dest_type': Proof.context -> afun_inst -> typ -> typ
   val dest_pure: Proof.context -> afun_inst -> term -> term
   val dest_comb: Proof.context -> afun_inst -> term -> term * term
   val infer_comb: Proof.context -> afun_inst -> term * term -> term
   val subst_lift_term: afun_inst -> (term * term) list -> term -> term
   val generalize_lift_terms: afun_inst -> term list -> Proof.context -> term list * Proof.context
 
   val afun_unfold_tac: Proof.context -> afun -> int -> tactic
   val afun_fold_tac: Proof.context -> afun -> int -> tactic
   val unfold_all_tac: Proof.context -> int -> tactic
   val normalform_conv: Proof.context -> afun -> conv
   val normalize_rel_tac: Proof.context -> afun -> int -> tactic
   val general_normalform_conv: Proof.context -> afun -> cterm * cterm -> thm * thm
   val general_normalize_rel_tac: Proof.context -> afun -> int -> tactic
   val forward_lift_rule: Proof.context -> afun -> thm -> thm
   val unfold_wrapper_tac: Proof.context -> afun option -> int -> tactic
   val fold_wrapper_tac: Proof.context -> afun option -> int -> tactic
   val normalize_wrapper_tac: Proof.context -> afun option -> int -> tactic
   val lifting_wrapper_tac: Proof.context -> afun option -> int -> tactic
 
   val setup_combinators: (string * thm) list -> local_theory -> local_theory
   val combinator_rule_attrib: string list option -> attribute
   val parse_opt_afun: afun option context_parser
   val applicative_cmd: (((((binding * string list) * string) * string) * string option) * string option) ->
     local_theory -> Proof.state
   val print_afuns: Proof.context -> unit
   val add_unfold_attrib: xstring option -> attribute
   val forward_lift_attrib: xstring -> attribute
 end;
 
 structure Applicative : APPLICATIVE =
 struct
 
 open Ctr_Sugar_Util
 
 (** General utilities **)
 
 fun fold_options xs = fold (fn x =>
   (case x of
     SOME x' => cons x'
   | NONE => I)) xs [];
 
 fun the_pair [x, y] = (x, y)
   | the_pair _ = raise General.Size;
 
 fun strip_comb2 (f $ x $ y) = (f, (x, y))
   | strip_comb2 t = raise TERM ("strip_comb2", [t]);
 
 fun mk_comb_pattern (t, n) =
   let
     val Ts = take n (binder_types (fastype_of t));
     val maxidx = maxidx_of_term t;
     val vars = map (fn (T, i) => ((Name.uu, maxidx + i), T)) (Ts ~~ (1 upto n));
   in (vars, Term.betapplys (t, map Var vars)) end;
 
 fun match_comb_pattern ctxt tn u =
   let
     val thy = Proof_Context.theory_of ctxt;
     val (vars, pat) = mk_comb_pattern tn;
     val envs = Pattern.match thy (pat, u) (Vartab.empty, Vartab.empty)
       handle Pattern.MATCH => raise TERM ("match_comb_pattern", [u, pat]);
   in (vars, envs) end;
 
 fun dest_comb_pattern ctxt tn u =
   let val (vars, (_, env)) = match_comb_pattern ctxt tn u;
   in map (the o Envir.lookup1 env) vars end;
 
 fun norm_term_types tyenv t = Term_Subst.map_types_same (Envir.norm_type_same tyenv) t
   handle Same.SAME => t;
 
 val mk_TFrees_of = mk_TFrees' oo replicate;
 
 fun mk_Free name typ ctxt = yield_singleton Variable.variant_fixes name ctxt
   |>> (fn name' => Free (name', typ));
 
 (*tuples with explicit sentinel*)
 fun mk_tuple' ts = fold_rev (curry HOLogic.mk_prod) ts HOLogic.unit;
 fun strip_tuple' (Const (@{const_name Unity}, _)) = []
   | strip_tuple' (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: strip_tuple' t2
   | strip_tuple' t = raise TERM ("strip_tuple'", [t]);
 
 fun mk_eq_on S =
   let val (SA, ST) = `HOLogic.dest_setT (fastype_of S);
   in Const (@{const_name eq_on}, ST --> BNF_Util.mk_pred2T SA SA) $ S end;
 
 
 (* Polymorphic terms and term groups *)
 
 type poly_type = typ list * typ;
 type poly_term = typ list * term;
 
 fun instantiate_poly_type (tvars, T) insts = typ_subst_atomic (tvars ~~ insts) T;
 fun instantiate_poly_term (tvars, t) insts = subst_atomic_types (tvars ~~ insts) t;
 
 fun dest_poly_type ctxt (tvars, T) U =
   let
     val thy = Proof_Context.theory_of ctxt;
     val tyenv = Sign.typ_match thy (T, U) Vartab.empty
       handle Type.TYPE_MATCH => raise TYPE ("dest_poly_type", [U, T], []);
   in map (Type.lookup tyenv o dest_TVar) tvars end;
 
 fun poly_type_to_term (tvars, T) = (tvars, Logic.mk_type T);
 fun poly_type_of_term (tvars, t) = (tvars, Logic.dest_type t);
 
 (*
   Schematic variables are treated uniformly in packed terms, thus forming an ad hoc context
   of type variables. Otherwise, morphisms are allowed to rename schematic variables
   non-consistently in separate terms, and occasionally will do so.
 *)
 fun pack_poly_term (tvars, t) = HOLogic.mk_prod (mk_tuple' (map Logic.mk_type tvars), t);
 fun unpack_poly_term t =
   let val (tvars, t') = HOLogic.dest_prod t;
   in (map Logic.dest_type (strip_tuple' tvars), t') end;
 
 val pack_poly_terms = mk_tuple' o map pack_poly_term;
 val unpack_poly_terms = map unpack_poly_term o strip_tuple';
 
 (*match and instantiate schematic type variables which are not "quantified" in the packed term*)
 fun match_poly_terms_type ctxt (pt, i) (U, maxidx) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val pt' = Logic.incr_indexes ([], [], maxidx + 1) pt;
     val (tvars, T) = poly_type_of_term (nth (unpack_poly_terms pt') i);
     val tyenv = Sign.typ_match thy (T, U) Vartab.empty
       handle Type.TYPE_MATCH => raise TYPE ("match_poly_terms", [U, T], []);
     val tyenv' = fold Vartab.delete_safe (map (#1 o dest_TVar) tvars) tyenv;
     val pt'' = Envir.subst_term_types tyenv' pt';
   in unpack_poly_terms pt'' end;
 
 fun match_poly_terms ctxt (pt, i) (t, maxidx) =
   match_poly_terms_type ctxt (pt, i) (fastype_of t, maxidx);
 
 (*fix schematic type variables which are not "quantified", as well as schematic term variables*)
 fun import_poly_terms pt ctxt =
   let
     fun insert_paramTs (tvars, t) = fold_types (fold_atyps
       (fn TVar v => if member (op =) tvars (TVar v) then I else insert (op =) v
         | _ => I)) t;
     val paramTs = rev (fold insert_paramTs (unpack_poly_terms pt) []);
     val (tfrees, ctxt') = Variable.invent_types (map #2 paramTs) ctxt;
-    val instT = paramTs ~~ map TFree tfrees;
+    val instT = Term_Subst.TVars.table (paramTs ~~ map TFree tfrees);
     val params = map (apsnd (Term_Subst.instantiateT instT)) (rev (Term.add_vars pt []));
     val (frees, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) params) ctxt';
-    val inst = params ~~ map Free (frees ~~ map #2 params);
+    val inst = Term_Subst.Vars.table (params ~~ map Free (frees ~~ map #2 params));
     val pt' = Term_Subst.instantiate (instT, inst) pt;
   in (unpack_poly_terms pt', ctxt'') end;
 
 
 (** Internal representation **)
 
 (* Applicative functors *)
 
 type rel_thms = {
   pure_transfer: thm,
   ap_rel_fun: thm
 };
 
 fun map_rel_thms f {pure_transfer, ap_rel_fun} =
   {pure_transfer = f pure_transfer, ap_rel_fun = f ap_rel_fun};
 
 type afun_thms = {
   hom: thm,
   ichng: thm,
   reds: thm Symtab.table,
   rel_thms: rel_thms option,
   rel_intros: thm list,
   pure_comp_conv: thm
 };
 
 fun map_afun_thms f {hom, ichng, reds, rel_thms, rel_intros, pure_comp_conv} =
   {hom = f hom, ichng = f ichng, reds = Symtab.map (K f) reds,
     rel_thms = Option.map (map_rel_thms f) rel_thms, rel_intros = map f rel_intros,
     pure_comp_conv = f pure_comp_conv};
 
 datatype afun = AFun of {
   name: binding,
   terms: term,
   rel: term option,
   thms: afun_thms,
   unfolds: thm Item_Net.T
 };
 
 fun rep_afun (AFun af) = af;
 val name_of_afun = #name o rep_afun;
 val terms_of_afun = #terms o rep_afun;
 val rel_of_afun = #rel o rep_afun;
 val thms_of_afun = #thms o rep_afun;
 val unfolds_of_afun = Item_Net.content o #unfolds o rep_afun;
 
 val red_of_afun = Symtab.lookup o #reds o thms_of_afun;
 val has_red_afun = is_some oo red_of_afun;
 
 fun mk_afun name terms rel thms =
   AFun {name = name, terms = terms, rel = rel, thms = thms, unfolds = Thm.item_net};
 
 fun map_afun f1 f2 f3 f4 f5 (AFun {name, terms, rel, thms, unfolds}) =
   AFun {name = f1 name, terms = f2 terms, rel = f3 rel, thms = f4 thms, unfolds = f5 unfolds};
 
 fun map_unfolds f thms = fold Item_Net.update (map f (Item_Net.content thms)) Thm.item_net;
 
 fun morph_afun phi =
   let
     val binding = Morphism.binding phi;
     val term = Morphism.term phi;
     val thm = Morphism.thm phi;
   in map_afun binding term (Option.map term) (map_afun_thms thm) (map_unfolds thm) end;
 
 val transfer_afun = morph_afun o Morphism.transfer_morphism;
 
 fun add_unfolds_afun thms = map_afun I I I I (fold Item_Net.update thms);
 
 fun patterns_of_afun af =
   let
     val [Tt, (_, pure), (_, ap), _] = unpack_poly_terms (terms_of_afun af);
     val (_, T) = poly_type_of_term Tt;
   in [#2 (mk_comb_pattern (pure, 1)), #2 (mk_comb_pattern (ap, 2)), Net.encode_type T] end;
 
 
 (* Combinator rules *)
 
 datatype combinator_rule = Combinator_Rule of {
   strong_premises: string Ord_List.T,
   weak_premises: bool,
   conclusion: string,
   eq_thm: thm
 };
 
 fun rep_combinator_rule (Combinator_Rule rule) = rule;
 val conclusion_of_rule = #conclusion o rep_combinator_rule;
 val thm_of_rule = #eq_thm o rep_combinator_rule;
 
 fun eq_combinator_rule (rule1, rule2) =
   pointer_eq (rule1, rule2) orelse Thm.eq_thm (thm_of_rule rule1, thm_of_rule rule2);
 
 fun is_applicable_rule rule have_weak have_premises =
   let val {strong_premises, weak_premises, ...} = rep_combinator_rule rule;
   in (have_weak orelse not weak_premises) andalso have_premises strong_premises end;
 
 fun map_combinator_rule f1 f2 f3 f4
   (Combinator_Rule {strong_premises, weak_premises, conclusion, eq_thm}) =
     Combinator_Rule {strong_premises = f1 strong_premises, weak_premises = f2 weak_premises,
       conclusion = f3 conclusion, eq_thm = f4 eq_thm};
 
 fun transfer_combinator_rule thy = map_combinator_rule I I I (Thm.transfer thy);
 
 fun mk_combinator_rule comb_names weak_premises thm =
   let
     val (lhs, rhs) = Logic.dest_equals (Thm.prop_of thm);
     val conclusion = the (Symtab.lookup comb_names (#1 (dest_Const lhs)));
     val premises = Ord_List.make fast_string_ord
       (fold_options (map (Symtab.lookup comb_names o #1) (Term.add_consts rhs [])));
     val weak_premises' = Ord_List.make fast_string_ord (these weak_premises);
     val strong_premises = Ord_List.subtract fast_string_ord weak_premises' premises;
   in Combinator_Rule {strong_premises = strong_premises, weak_premises = is_some weak_premises,
     conclusion = conclusion, eq_thm = thm} end;
 
 
 (* Generic data *)
 
 (*FIXME: needs tests, especially around theory merging*)
 
 fun merge_afuns _ (af1, af2) = if pointer_eq (af1, af2)
   then raise Change_Table.SAME
   else map_afun I I I I (fn thms1 => Item_Net.merge (thms1, #unfolds (rep_afun af2))) af1;
 
 structure Data = Generic_Data
 (
   type T = {
     combinators: thm Symtab.table * combinator_rule list,
     afuns: afun Name_Space.table,
     patterns: (string * term list) Item_Net.T
   };
   val empty = {
     combinators = (Symtab.empty, []),
     afuns = Name_Space.empty_table "applicative functor",
     patterns = Item_Net.init (op = o apply2 #1) #2
   };
   val extend = I;
   fun merge ({combinators = (cd1, cr1), afuns = a1, patterns = p1},
              {combinators = (cd2, cr2), afuns = a2, patterns = p2}) =
     {combinators = (Symtab.merge (K true) (cd1, cd2), Library.merge eq_combinator_rule (cr1, cr2)),
       afuns = Name_Space.join_tables merge_afuns (a1, a2),
       patterns = Item_Net.merge (p1, p2)};
 );
 
 fun get_combinators context =
   let
     val thy = Context.theory_of context;
     val {combinators = (defs, rules), ...} = Data.get context;
   in (Symtab.map (K (Thm.transfer thy)) defs, map (transfer_combinator_rule thy) rules) end;
 
 val get_afun_table = #afuns o Data.get;
 val get_afun_space = Name_Space.space_of_table o get_afun_table;
 val get_patterns = #patterns o Data.get;
 
 fun map_data f1 f2 f3 {combinators, afuns, patterns} =
   {combinators = f1 combinators, afuns = f2 afuns, patterns = f3 patterns};
 
 val intern = Name_Space.intern o get_afun_space;
 fun extern context = Name_Space.extern (Context.proof_of context) (get_afun_space context);
 
 local fun undeclared name = error ("Undeclared applicative functor " ^ quote name);
 in
 
 fun afun_of_generic context name = case Name_Space.lookup (get_afun_table context) name of
     SOME af => transfer_afun (Context.theory_of context) af
   | NONE => undeclared name;
 
 val afun_of = afun_of_generic o Context.Proof;
 
 fun update_afun name f context = if Name_Space.defined (get_afun_table context) name
   then Data.map (map_data I (Name_Space.map_table_entry name f) I) context
   else undeclared name;
 
 end;
 
 fun match_term context = map #1 o Item_Net.retrieve_matching (get_patterns context);
 fun match_typ context = match_term context o Net.encode_type;
 
 (*works only with terms which are combinations of pure and ap*)
 fun afuns_of_term_generic context = map (afun_of_generic context) o match_term context;
 val afuns_of_term = afuns_of_term_generic o Context.Proof;
 
 fun afuns_of_typ_generic context = map (afun_of_generic context) o match_typ context;
 val afuns_of_typ = afuns_of_typ_generic o Context.Proof;
 
 fun all_unfolds_of_generic context =
   let val unfolds_of = map (Thm.transfer'' context) o unfolds_of_afun;
   in Name_Space.fold_table (fn (_, af) => append (unfolds_of af)) (get_afun_table context) [] end;
 
 val all_unfolds_of = all_unfolds_of_generic o Context.Proof;
 
 
 (** Term construction and destruction **)
 
 type afun_inst = {
   T: poly_type,
   pure: poly_term,
   ap: poly_term,
   set: poly_term
 };
 
 fun mk_afun_inst [T, pure, ap, set] = {T = poly_type_of_term T, pure = pure, ap = ap, set = set};
 fun pack_afun_inst {T, pure, ap, set} = pack_poly_terms [poly_type_to_term T, pure, ap, set];
 
 fun match_afun_inst ctxt af = match_poly_terms ctxt (terms_of_afun af, 0) #> mk_afun_inst;
 fun import_afun_inst_raw terms = import_poly_terms terms #>> mk_afun_inst;
 val import_afun_inst = import_afun_inst_raw o terms_of_afun;
 
 fun inner_sort_of {T = (tvars, _), ...} = Type.sort_of_atyp (the_single tvars);
 
 fun mk_type {T, ...} = instantiate_poly_type T o single;
 fun mk_pure {pure, ...} = instantiate_poly_term pure o single;
 fun mk_ap {ap, ...} (T1, T2) = instantiate_poly_term ap [T1, T2];
 fun mk_set {set, ...} = instantiate_poly_term set o single;
 
 fun lift_term af_inst t = Term.betapply (mk_pure af_inst (Term.fastype_of t), t);
 fun mk_comb af_inst funT (t1, t2) = Term.betapplys (mk_ap af_inst (dest_funT funT), [t1, t2]);
 
 fun dest_type ctxt {T, ...} = the_single o dest_poly_type ctxt T;
 val dest_type' = the_default HOLogic.unitT ooo dest_type;
 
 fun dest_pure ctxt {pure = (_, pure), ...} = the_single o dest_comb_pattern ctxt (pure, 1);
 fun dest_comb ctxt {ap = (_, ap), ...} = the_pair o dest_comb_pattern ctxt (ap, 2);
 
 fun infer_comb ctxt af_inst (t1, t2) =
   let val funT = the_default (dummyT --> dummyT) (dest_type ctxt af_inst (fastype_of t1));
   in mk_comb af_inst funT (t1, t2) end;
 
 (*lift a term, except for non-combination subterms mapped by subst*)
 fun subst_lift_term af_inst subst tm =
   let
     fun subst_lift (s $ t) =
         (case (subst_lift s, subst_lift t) of
           (NONE, NONE) => NONE
         | (SOME s', NONE) => SOME (mk_comb af_inst (fastype_of s) (s', lift_term af_inst t))
         | (NONE, SOME t') => SOME (mk_comb af_inst (fastype_of s) (lift_term af_inst s, t'))
         | (SOME s', SOME t') => SOME (mk_comb af_inst (fastype_of s) (s', t')))
       | subst_lift t = AList.lookup (op aconv) subst t;
   in
     (case subst_lift tm of
       NONE => lift_term af_inst tm
     | SOME tm' => tm')
   end;
 
 fun add_lifted_vars (s $ t) = add_lifted_vars s #> add_lifted_vars t
   | add_lifted_vars (Abs (_, _, t)) = Term.add_vars t
   | add_lifted_vars _ = I;
 
 (*lift terms, where schematic variables are generalized to the functor and then fixed*)
 fun generalize_lift_terms af_inst ts ctxt =
   let
     val vars = subtract (op =) (fold add_lifted_vars ts []) (fold Term.add_vars ts []);
     val (var_names, Ts) = split_list vars;
     val (free_names, ctxt') = Variable.variant_fixes (map #1 var_names) ctxt;
     val Ts' = map (mk_type af_inst) Ts;
     val subst = map Var vars ~~ map Free (free_names ~~ Ts');
   in (map (subst_lift_term af_inst subst) ts, ctxt') end;
 
 
 (** Reasoning with applicative functors **)
 
 (* Utilities *)
 
 val clean_name = perhaps (perhaps_apply [try Name.dest_skolem, try Name.dest_internal]);
 
 (*based on term_name from Pure/term.ML*)
 fun term_to_vname (Const (x, _)) = Long_Name.base_name x
   | term_to_vname (Free (x, _)) = clean_name x
   | term_to_vname (Var ((x, _), _)) = clean_name x
   | term_to_vname _ = "x";
 
 fun afuns_of_rel precise ctxt t =
   let val (_, (lhs, rhs)) = Variable.focus NONE t ctxt
     |> #1 |> #2
     |> Logic.strip_imp_concl
     |> Envir.beta_eta_contract
     |> HOLogic.dest_Trueprop
     |> strip_comb2;
   in if precise
     then (case afuns_of_term ctxt lhs of
         [] => afuns_of_term ctxt rhs
       | afs => afs)
     else afuns_of_typ ctxt (fastype_of lhs) end;
 
 fun AUTO_AFUNS precise tac ctxt opt_af = case opt_af of
     SOME af => tac [af]
   | NONE => SUBGOAL (fn (goal, i) => (case afuns_of_rel precise ctxt goal of
       [] => no_tac
     | afs => tac afs i) handle TERM _ => no_tac);
 
 fun AUTO_AFUN precise tac = AUTO_AFUNS precise (tac o hd);
 
 fun binop_par_conv cv ct =
   let
     val ((binop, arg1), arg2) = Thm.dest_comb ct |>> Thm.dest_comb;
     val (th1, th2) = cv (arg1, arg2);
   in Drule.binop_cong_rule binop th1 th2 end;
 
 fun binop_par_conv_tac cv = CONVERSION (HOLogic.Trueprop_conv (binop_par_conv cv));
 
 val fold_goal_tac = SELECT_GOAL oo Raw_Simplifier.fold_goals_tac;
 
 
 (* Unfolding of lifted constants *)
 
 fun afun_unfold_tac ctxt af = Raw_Simplifier.rewrite_goal_tac ctxt (unfolds_of_afun af);
 fun afun_fold_tac ctxt af = fold_goal_tac ctxt (unfolds_of_afun af);
 
 fun unfold_all_tac ctxt = Raw_Simplifier.rewrite_goal_tac ctxt (all_unfolds_of ctxt);
 
 
 (* Basic conversions *)
 
 fun pure_conv ctxt {pure = (_, pure), ...} cv ct =
   let
     val ([var], (tyenv, env)) = match_comb_pattern ctxt (pure, 1) (Thm.term_of ct);
     val arg = the (Envir.lookup1 env var);
     val thm = cv (Thm.cterm_of ctxt arg);
   in
     if Thm.is_reflexive thm then Conv.all_conv ct
     else
       let val pure_inst = Envir.subst_term_types tyenv pure;
       in Drule.arg_cong_rule (Thm.cterm_of ctxt pure_inst) thm end
   end;
 
 fun ap_conv ctxt {ap = (_, ap), ...} cv1 cv2 ct =
   let
     val ([var1, var2], (tyenv, env)) = match_comb_pattern ctxt (ap, 2) (Thm.term_of ct);
     val (arg1, arg2) = apply2 (the o Envir.lookup1 env) (var1, var2);
     val thm1 = cv1 (Thm.cterm_of ctxt arg1);
     val thm2 = cv2 (Thm.cterm_of ctxt arg2);
   in
     if Thm.is_reflexive thm1 andalso Thm.is_reflexive thm2 then Conv.all_conv ct
     else
       let val ap_inst = Envir.subst_term_types tyenv ap;
       in Drule.binop_cong_rule (Thm.cterm_of ctxt ap_inst) thm1 thm2 end
   end;
 
 
 (* Normal form conversion *)
 
 (*convert a term into applicative normal form*)
 fun normalform_conv ctxt af ct =
   let
     val {hom, ichng, pure_comp_conv, ...} = thms_of_afun af;
     val the_red = the o red_of_afun af;
     val leaf_conv = Conv.rewr_conv (mk_meta_eq (the_red "I") |> Thm.symmetric);
     val merge_conv = Conv.rewr_conv (mk_meta_eq hom);
     val swap_conv = Conv.rewr_conv (mk_meta_eq ichng);
     val rotate_conv = Conv.rewr_conv (mk_meta_eq (the_red "B") |> Thm.symmetric);
     val pure_rotate_conv = Conv.rewr_conv (mk_meta_eq pure_comp_conv);
 
     val af_inst = match_afun_inst ctxt af (Thm.term_of ct, Thm.maxidx_of_cterm ct);
     fun left_conv cv = ap_conv ctxt af_inst cv Conv.all_conv;
 
     fun norm_pure_nf ct =
       ((pure_rotate_conv then_conv left_conv norm_pure_nf) else_conv merge_conv) ct;
     val norm_nf_pure = swap_conv then_conv norm_pure_nf;
     fun norm_nf_nf ct = ((rotate_conv then_conv
         left_conv (left_conv norm_pure_nf then_conv norm_nf_nf)) else_conv
       norm_nf_pure) ct;
     fun normalize ct = ((ap_conv ctxt af_inst normalize normalize then_conv norm_nf_nf) else_conv
       pure_conv ctxt af_inst Conv.all_conv else_conv
       leaf_conv) ct;
   in normalize ct end;
 
 val normalize_rel_tac = binop_par_conv_tac o apply2 oo normalform_conv;
 
 
 (* Bracket abstraction and generalized unlifting *)
 
 (*TODO: use proper conversions*)
 
 datatype apterm =
     Pure of term  (*includes pure application*)
   | ApVar of int * term  (*unique index, instantiated term*)
   | Ap of apterm * apterm;
 
 fun apterm_vars (Pure _) = I
   | apterm_vars (ApVar v) = cons v
   | apterm_vars (Ap (t1, t2)) = apterm_vars t1 #> apterm_vars t2;
 
 fun occurs_any _ (Pure _) = false
   | occurs_any vs (ApVar (i, _)) = exists (fn j => i = j) vs
   | occurs_any vs (Ap (t1, t2)) = occurs_any vs t1 orelse occurs_any vs t2;
 
 fun term_of_apterm ctxt af_inst t =
   let
     fun tm_of (Pure t) = t
       | tm_of (ApVar (_, t)) = t
       | tm_of (Ap (t1, t2)) = infer_comb ctxt af_inst (tm_of t1, tm_of t2);
   in tm_of t end;
 
 fun apterm_of_term ctxt af_inst t =
   let
     fun aptm_of t i = case try (dest_comb ctxt af_inst) t of
         SOME (t1, t2) => i |> aptm_of t1 ||>> aptm_of t2 |>> Ap
       | NONE => if can (dest_pure ctxt af_inst) t
           then (Pure t, i)
           else (ApVar (i, t), i + 1);
   in aptm_of t end;
 
 (*find a common variable sequence for two applicative terms, depending on available combinators*)
 fun consolidate ctxt af (t1, t2) =
   let
     fun common_inst (i, t) (j, insts) = case Termtab.lookup insts t of
         SOME k => (((i, t), k), (j, insts))
       | NONE => (((i, t), j), (j + 1, Termtab.update (t, j) insts));
 
     val (vars, _) = (0, Termtab.empty)
       |> fold_map common_inst (apterm_vars t1 [])
       ||>> fold_map common_inst (apterm_vars t2 []);
 
     fun merge_adjacent (([], _), _) [] = []
       | merge_adjacent ((is, t), d) [] = [((is, t), d)]
       | merge_adjacent (([], _), _) (((i, t), d)::xs) = merge_adjacent (([i], t), d) xs
       | merge_adjacent ((is, t), d) (((i', t'), d')::xs) = if d = d'
           then merge_adjacent ((i'::is, t), d) xs
           else ((is, t), d) :: merge_adjacent (([i'], t'), d') xs;
 
     fun align _ [] = NONE
       | align ((i, t), d) (((i', t'), d')::xs) = if d = d'
           then SOME ([((i @ i', t), d)], xs)
           else Option.map (apfst (cons ((i', t'), d'))) (align ((i, t), d) xs);
     fun merge ([], ys) = ys
       | merge (xs, []) = xs
       | merge ((xs as ((is1, t1), d1)::xs'), ys as (((is2, t2), d2)::ys')) = if d1 = d2
           then ((is1 @ is2, t1), d1) :: merge (xs', ys')
           else case (align ((is2, t2), d2) xs, align ((is1, t1), d1) ys) of
               (SOME (zs, xs''), NONE) => zs @ merge (xs'', ys')
             | (NONE, SOME (zs, ys'')) => zs @ merge (xs', ys'')
             | _ => ((is1, t1), d1) :: ((is2, t2), d2) :: merge (xs', ys');
 
     fun unbalanced vs = error ("Unbalanced opaque terms " ^
       commas_quote (map (Syntax.string_of_term ctxt o #2 o #1) vs));
     fun mismatch (t1, t2) = error ("Mismatched opaque terms " ^
       quote (Syntax.string_of_term ctxt t1) ^ " and " ^ quote (Syntax.string_of_term ctxt t2));
     fun same ([], []) = []
       | same ([], ys) = unbalanced ys
       | same (xs, []) = unbalanced xs
       | same ((((i1, t1), d1)::xs), (((i2, t2), d2)::ys)) = if d1 = d2
           then ((i1 @ i2, t1), d1) :: same (xs, ys)
           else mismatch (t1, t2);
   in vars
     |> has_red_afun af "C" ? apply2 (sort (int_ord o apply2 #2))
     |> apply2 (if has_red_afun af "W"
         then merge_adjacent (([], Term.dummy), 0)
         else map (apfst (apfst single)))
     |> (if has_red_afun af "K" then merge else same)
     |> map #1
   end;
 
 fun ap_cong ctxt af_inst thm1 thm2 =
   let
     val funT = the_default (dummyT --> dummyT)
       (dest_type ctxt af_inst (Thm.typ_of_cterm (Thm.lhs_of thm1)));
     val ap_inst = Thm.cterm_of ctxt (mk_ap af_inst (dest_funT funT));
   in Drule.binop_cong_rule ap_inst thm1 thm2 end;
 
 fun rewr_subst_ap ctxt af_inst rewr thm1 thm2 =
   let
     val rule1 = ap_cong ctxt af_inst thm1 thm2;
     val rule2 = Conv.rewr_conv rewr (Thm.rhs_of rule1);
   in Thm.transitive rule1 rule2 end;
 
 fun merge_pures ctxt af_inst merge_thm tt =
   let
     fun merge (Pure t) = SOME (Thm.reflexive (Thm.cterm_of ctxt t))
       | merge (ApVar _) = NONE
       | merge (Ap (tt1, tt2)) = case merge tt1 of
           NONE => NONE
         | SOME thm1 => case merge tt2 of
             NONE => NONE
           | SOME thm2 => SOME (rewr_subst_ap ctxt af_inst merge_thm thm1 thm2);
   in merge tt end;
 
 exception ASSERT of string;
 
 (*abstract over a variable (opaque subterm)*)
 fun eliminate ctxt (af, af_inst) tt (v, v_tm) =
   let
     val {hom, ichng, ...} = thms_of_afun af;
     val the_red = the o red_of_afun af;
     val hom_conv = mk_meta_eq hom;
     val ichng_conv = mk_meta_eq ichng;
     val mk_combI = Thm.symmetric o mk_meta_eq;
     val id_conv = mk_combI (the_red "I");
     val comp_conv = mk_combI (the_red "B");
     val flip_conv = Option.map mk_combI (red_of_afun af "C");
     val const_conv = Option.map mk_combI (red_of_afun af "K");
     val dup_conv = Option.map mk_combI (red_of_afun af "W");
 
     val rewr_subst_ap = rewr_subst_ap ctxt af_inst;
     fun extract_comb n thm = Pure (thm |> Thm.rhs_of |> funpow n Thm.dest_arg1 |> Thm.term_of);
     fun refl_step tt = (tt, Thm.reflexive (Thm.cterm_of ctxt (term_of_apterm ctxt af_inst tt)));
     fun comb2_step def (tt1, thm1) (tt2, thm2) =
       let val thm = rewr_subst_ap def thm1 thm2;
       in (Ap (Ap (extract_comb 3 thm, tt1), tt2), thm) end;
     val B_step = comb2_step comp_conv;
     fun swap_B_step (tt1, thm1) thm2 =
       let
         val thm3 = rewr_subst_ap ichng_conv thm1 thm2;
         val thm4 = Thm.transitive thm3 (Conv.rewr_conv comp_conv (Thm.rhs_of thm3));
       in (Ap (Ap (extract_comb 3 thm4, extract_comb 1 thm3), tt1), thm4) end;
     fun I_step tm =
       let val thm = Conv.rewr_conv id_conv (Thm.cterm_of ctxt tm)
       in (extract_comb 1 thm, thm) end;
     fun W_step s1 s2 =
       let
         val (Ap (Ap (tt1, tt2), tt3), thm1) = B_step s1 s2;
         val thm2 = Conv.rewr_conv comp_conv (Thm.rhs_of thm1 |> funpow 2 Thm.dest_arg1);
         val thm3 = merge_pures ctxt af_inst hom_conv tt3 |> the;
         val (tt4, thm4) = swap_B_step (Ap (Ap (extract_comb 3 thm2, tt1), tt2), thm2) thm3;
         val var = Thm.rhs_of thm1 |> Thm.dest_arg;
         val thm5 = rewr_subst_ap (the dup_conv) thm4 (Thm.reflexive var);
         val thm6 = Thm.transitive thm1 thm5;
       in (Ap (extract_comb 2 thm6, tt4), thm6) end;
     fun S_step s1 s2 =
       let
         val (Ap (Ap (tt1, tt2), tt3), thm1) = comb2_step (the flip_conv) s1 s2;
         val thm2 = Conv.rewr_conv comp_conv (Thm.rhs_of thm1 |> Thm.dest_arg1);
         val var = Thm.rhs_of thm1 |> Thm.dest_arg;
         val thm3 = rewr_subst_ap (the dup_conv) thm2 (Thm.reflexive var);
         val thm4 = Thm.transitive thm1 thm3;
         val tt = Ap (extract_comb 2 thm4, Ap (Ap (extract_comb 3 thm2, Ap (tt1, tt2)), tt3));
       in (tt, thm4) end;
     fun K_step tt tm =
       let
         val ct = Thm.cterm_of ctxt tm;
         val T_opt = Term.fastype_of tm |> dest_type ctxt af_inst |> Option.map (Thm.ctyp_of ctxt);
         val thm = Thm.instantiate' [T_opt] [SOME ct]
           (Conv.rewr_conv (the const_conv) (term_of_apterm ctxt af_inst tt |> Thm.cterm_of ctxt))
       in (Ap (extract_comb 2 thm, tt), thm) end;
     fun unreachable _ = raise ASSERT "eliminate: assertion failed";
     fun elim (Pure _) = unreachable ()
       | elim (ApVar (i, t)) = if exists (fn x => x = i) v then I_step t else unreachable ()
       | elim (Ap (t1, t2)) = (case (occurs_any v t1, occurs_any v t2) of
             (false, false) => unreachable ()
           | (false, true) => B_step (refl_step t1) (elim t2)
           | (true, false) => (case merge_pures ctxt af_inst hom_conv t2 of
                 SOME thm => swap_B_step (elim t1) thm
               | NONE => comb2_step (the flip_conv) (elim t1) (refl_step t2))
           | (true, true) => if is_some flip_conv
               then S_step (elim t1) (elim t2)
               else W_step (elim t1) (elim t2));
   in if occurs_any v tt
     then elim tt
     else K_step tt v_tm
   end;
 
 (*convert a pair of terms into equal canonical forms, modulo pure terms*)
 fun general_normalform_conv ctxt af cts =
   let
     val (t1, t2) = apply2 (Thm.term_of) cts;
     val maxidx = Int.max (apply2 Thm.maxidx_of_cterm cts);
     (* TODO: is there a better strategy for finding the instantiated functor? *)
     val af_inst = match_afun_inst ctxt af (t1, maxidx);
     val ((apt1, apt2), _) = 0 |> apterm_of_term ctxt af_inst t1 ||>> apterm_of_term ctxt af_inst t2;
     val vs = consolidate ctxt af (apt1, apt2);
     val merge_thm = mk_meta_eq (#hom (thms_of_afun af));
     fun elim_all tt [] = the (merge_pures ctxt af_inst merge_thm tt)
       | elim_all tt (v::vs) =
           let
             val (tt', rule1) = eliminate ctxt (af, af_inst) tt v;
             val rule2 = elim_all tt' vs;
             val (_, vartm) = dest_comb ctxt af_inst (Thm.term_of (Thm.rhs_of rule1));
             val rule3 = ap_cong ctxt af_inst rule2 (Thm.reflexive (Thm.cterm_of ctxt vartm));
           in Thm.transitive rule1 rule3 end;
   in (elim_all apt1 vs, elim_all apt2 vs) end;
 
 val general_normalize_rel_tac = binop_par_conv_tac oo general_normalform_conv;
 
 
 (* Reduce canonical forms to base relation *)
 
 fun rename_params names i st =
   let
     val (_, Bs, Bi, C) = Thm.dest_state (st, i);
     val Bi' = Logic.list_rename_params names Bi;
   in Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st end;
 
 (*
   R' (pure f <> x1 <> ... <> xn) (pure g <> x1 <> ... <> xn)
     ===> !!y1 ... yn. [| yi : setF xi ... |] ==> R (f y1 ... yn) (g y1 ... yn),
   where either both R and R' are equality, or R' = relF R for relator relF of the functor.
   The premises yi : setF xi are added only in the latter case and if the set operator is available.
   Succeeds if partial progress can be made. The names of the new parameters yi are derived
   from the arguments xi.
 *)
 fun head_cong_tac ctxt af renames =
   let
     val {rel_intros, ...} = thms_of_afun af;
     fun term_name tm = case AList.lookup (op aconv) renames tm of
         SOME n => n
       | NONE => term_to_vname tm;
     fun gather_vars' af_inst tm = case try (dest_comb ctxt af_inst) tm of
         SOME (t1, t2) => term_name t2 :: gather_vars' af_inst t1
       | NONE => [];
     fun gather_vars prop = case prop of
         Const (@{const_name Trueprop}, _) $ (_ $ rhs) =>
           rev (gather_vars' (match_afun_inst ctxt af (rhs, maxidx_of_term prop)) rhs)
       | _ => [];
   in SUBGOAL (fn (subgoal, i) =>
     (REPEAT_DETERM (resolve_tac ctxt rel_intros i) THEN
       REPEAT_DETERM (resolve_tac ctxt [ext, @{thm rel_fun_eq_onI}] i ORELSE
         eresolve_tac ctxt [@{thm UNIV_E}] i) THEN
       PRIMITIVE (rename_params (gather_vars subgoal) i)))
   end;
 
 
 (* Forward lifting *)
 
 (*
   TODO: add limited support for premises, where used variables are not generalized in the conclusion
 *)
 fun forward_lift_rule ctxt af thm =
   let
     val thm = Object_Logic.rulify ctxt thm;
     val (af_inst, ctxt_inst) = import_afun_inst af ctxt;
     val (prop, ctxt_Ts) = yield_singleton Variable.importT_terms (Thm.prop_of thm) ctxt_inst;
     val (lhs, rhs) = prop |> HOLogic.dest_Trueprop |> HOLogic.dest_eq;
     val ([lhs', rhs'], ctxt_lifted) = generalize_lift_terms af_inst [lhs, rhs] ctxt_Ts;
     val lifted = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'));
     val (lifted', ctxt') = yield_singleton (Variable.import_terms true) lifted ctxt_lifted;
 
     fun tac {prems, context} = HEADGOAL (general_normalize_rel_tac context af THEN'
       head_cong_tac context af [] THEN'
       resolve_tac context [prems MRS thm]);
     val thm' = singleton (Variable.export ctxt' ctxt)
       (Goal.prove ctxt' [] [] lifted' tac);
     val thm'' = Raw_Simplifier.fold_rule ctxt (unfolds_of_afun af) thm';
   in thm'' end;
 
 fun forward_lift_attrib name =
   Thm.rule_attribute [] (fn context => fn thm =>
     let val af = afun_of_generic context (intern context name)  (* FIXME !?!? *)
     in forward_lift_rule (Context.proof_of context) af thm end);
 
 
 (* High-level tactics *)
 
 fun unfold_wrapper_tac ctxt = AUTO_AFUNS false (fn afs =>
   Simplifier.safe_asm_full_simp_tac (ctxt addsimps flat (map unfolds_of_afun afs))) ctxt;
 
 fun fold_wrapper_tac ctxt = AUTO_AFUN true (fold_goal_tac ctxt o unfolds_of_afun) ctxt;
 
 fun WRAPPER tac ctxt opt_af =
   REPEAT_DETERM o resolve_tac ctxt [@{thm allI}] THEN'
   Subgoal.FOCUS (fn {context = ctxt, params, ...} =>
     let val renames = map (swap o apsnd Thm.term_of) params
     in
       AUTO_AFUNS false (EVERY' o map (afun_unfold_tac ctxt)) ctxt opt_af 1 THEN
       AUTO_AFUN true (fn af =>
         afun_unfold_tac ctxt af THEN'
         CONVERSION Drule.beta_eta_conversion THEN'
         tac ctxt af THEN'
         head_cong_tac ctxt af renames) ctxt opt_af 1
     end) ctxt THEN'
   Raw_Simplifier.rewrite_goal_tac ctxt [Drule.triv_forall_equality];
 
 val normalize_wrapper_tac = WRAPPER normalize_rel_tac;
 val lifting_wrapper_tac = WRAPPER general_normalize_rel_tac;
 
 val parse_opt_afun = Scan.peek (fn context =>
   Scan.option Parse.name >> Option.map (intern context #> afun_of_generic context));
 
 
 (** Declaration **)
 
 (* Combinator setup *)
 
 fun declare_combinators combs phi =
   let
     val (names, thms) = split_list combs;
     val thms' = map (Morphism.thm phi) thms;
     fun add_combs (defs, rules) = (fold (Symtab.insert (K false)) (names ~~ thms') defs, rules);
   in Data.map (map_data add_combs I I) end;
 
 val setup_combinators =
   Local_Theory.declaration {syntax = false, pervasive = false} o declare_combinators;
 
 fun combinator_of_red thm =
   let
     val (lhs, _) = Logic.dest_equals (Thm.prop_of thm);
     val (head, _) = strip_comb lhs;
   in #1 (dest_Const head) end;
 
 fun register_combinator_rule weak_premises thm context =
   let
     val (lhs, rhs) = Logic.dest_equals (Thm.prop_of thm);
     val ltvars = Term.add_tvars lhs [];
     val rtvars = Term.add_tvars rhs [];
     val _ = if exists (not o member op = ltvars) rtvars
       then Pretty.breaks
          [Pretty.str "Combinator equation",
           Pretty.quote (Syntax.pretty_term (Context.proof_of context) (Thm.prop_of thm)),
           Pretty.str "has additional type variables on right-hand side."]
         |> Pretty.block |> Pretty.string_of |> error
       else ();
 
     val (defs, _) = #combinators (Data.get context);
     val comb_names =
       Symtab.make (map (fn (name, thm) => (combinator_of_red thm, name)) (Symtab.dest defs));
     val rule = mk_combinator_rule comb_names weak_premises thm;
     fun add_rule (defs, rules) = (defs, insert eq_combinator_rule rule rules);
   in Data.map (map_data add_rule I I) context end;
 
 val combinator_rule_attrib = Thm.declaration_attribute o register_combinator_rule;
 
 
 (* Derivation of combinator reductions *)
 
 fun combinator_closure rules have_weak combs =
   let
     fun apply rule (cs, changed) =
       if not (Ord_List.member fast_string_ord cs (conclusion_of_rule rule)) andalso
         is_applicable_rule rule have_weak (fn prems => Ord_List.subset fast_string_ord (prems, cs))
       then (Ord_List.insert fast_string_ord (conclusion_of_rule rule) cs, true)
       else (cs, changed);
     fun loop cs =
       (case fold apply rules (cs, false) of
         (cs', true) => loop cs'
       | (_, false) => cs);
   in loop combs end;
 
 fun derive_combinator_red ctxt af_inst red_thms (base_thm, eq_thm) =
   let
     val base_prop = Thm.prop_of base_thm;
     val tvars = Term.add_tvars base_prop [];
     val (Ts, ctxt_Ts) = mk_TFrees_of (length tvars) (inner_sort_of af_inst) ctxt;
-    val base_prop' = Term_Subst.instantiate (tvars ~~ Ts, []) base_prop;
+    val base_prop' = base_prop
+      |> Term_Subst.instantiate (Term_Subst.TVars.table (tvars ~~ Ts), Term_Subst.Vars.empty);
     val (lhs, rhs) = Logic.dest_equals base_prop';
     val ([lhs', rhs'], ctxt') = generalize_lift_terms af_inst [lhs, rhs] ctxt_Ts;
     val lifted_prop = (lhs', rhs') |> HOLogic.mk_eq |> HOLogic.mk_Trueprop;
     val unfold_comb_conv = HOLogic.Trueprop_conv
       (HOLogic.eq_conv (Conv.top_sweep_conv (K (Conv.rewr_conv eq_thm)) ctxt') Conv.all_conv);
     val tac = HEADGOAL (CONVERSION unfold_comb_conv THEN'
       Raw_Simplifier.rewrite_goal_tac ctxt' red_thms THEN'
       resolve_tac ctxt' [@{thm refl}]);
   in singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] lifted_prop (K tac)) end;
 
 (*derive all instantiations with pure terms which can be simplified by homomorphism*)
 (*FIXME: more of a workaround than a sensible solution*)
 fun weak_red_closure ctxt (af_inst, merge_thm) strong_red =
   let
     val (lhs, _) = Thm.prop_of strong_red |> Logic.dest_equals;
     val vars = rev (Term.add_vars lhs []);
     fun closure [] prev thms = (prev::thms)
       | closure ((v, af_T)::vs) prev thms =
           (case try (dest_type ctxt af_inst) af_T of
             NONE => closure vs prev thms
           | SOME T_opt =>
             let
               val (T, ctxt') = (case T_opt of
                   NONE => yield_singleton Variable.invent_types (inner_sort_of af_inst) ctxt
                     |>> TFree
                 | SOME T => (T, ctxt));
               val (v', ctxt'') = mk_Free (#1 v) T ctxt';
               val pure_v = Thm.cterm_of ctxt'' (lift_term af_inst v');
               val next = Drule.instantiate_normalize ([], [((v, af_T), pure_v)]) prev;
               val next' = Raw_Simplifier.rewrite_rule ctxt'' [merge_thm] next;
               val next'' = singleton (Variable.export ctxt'' ctxt) next';
             in closure vs next'' (prev::thms) end);
    in closure vars strong_red [] end;
 
 fun combinator_red_closure ctxt (comb_defs, rules) (af_inst, merge_thm) weak_reds combs =
   let
     val have_weak = not (null weak_reds);
     val red_thms0 = Symtab.fold (fn (_, thm) => cons (mk_meta_eq thm)) combs weak_reds;
     val red_thms = flat (map (weak_red_closure ctxt (af_inst, merge_thm)) red_thms0);
     fun apply rule ((cs, rs), changed) =
       if not (Symtab.defined cs (conclusion_of_rule rule)) andalso
         is_applicable_rule rule have_weak (forall (Symtab.defined cs))
       then
         let
           val conclusion = conclusion_of_rule rule;
           val def = the (Symtab.lookup comb_defs conclusion);
           val new_red_thm = derive_combinator_red ctxt af_inst rs (def, thm_of_rule rule);
           val new_red_thms = weak_red_closure ctxt (af_inst, merge_thm) (mk_meta_eq new_red_thm);
         in ((Symtab.update (conclusion, new_red_thm) cs, new_red_thms @ rs), true) end
       else ((cs, rs), changed);
     fun loop xs =
       (case fold apply rules (xs, false) of
         (xs', true) => loop xs'
       | (_, false) => xs);
   in #1 (loop (combs, red_thms)) end;
 
 
 (* Preparation of AFun data *)
 
 fun mk_terms ctxt (raw_pure, raw_ap, raw_rel, raw_set) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val show_typ = quote o Syntax.string_of_typ ctxt;
     val show_term = quote o Syntax.string_of_term ctxt;
 
     fun closed_poly_term t =
       let val poly_t = singleton (Variable.polymorphic ctxt) t;
       in case Term.add_vars (singleton
           (Variable.export_terms (Proof_Context.augment t ctxt) ctxt) t) [] of
           [] => (case (Term.hidden_polymorphism poly_t) of
               [] => poly_t
             | _ => error ("Hidden type variables in term " ^ show_term t))
         | _ => error ("Locally free variables in term " ^ show_term t)
       end;
 
     val pure = closed_poly_term raw_pure;
     val (tvar, T1) = fastype_of pure |> dest_funT |>> dest_TVar
       handle TYPE _ => error ("Bad type for pure: " ^ show_typ (fastype_of pure));
     val maxidx_pure = maxidx_of_term pure;
     val ap = Logic.incr_indexes ([], [], maxidx_pure + 1) (closed_poly_term raw_ap);
     fun bad_ap _ = error ("Bad type for ap: " ^ show_typ (fastype_of ap));
     val (T23, (T2, T3)) = fastype_of ap |> dest_funT ||> dest_funT
       handle TYPE _ => bad_ap ();
     val maxidx_common = Term.maxidx_term ap maxidx_pure;
 
     (*unify type variables, while keeping the live variables separate*)
     fun no_unifier (T, U) = error ("Unable to infer common functor type from " ^
       commas (map show_typ [T, U]));
     fun unify_ap_type T (tyenv, maxidx) =
       let
         val argT = TVar ((Name.aT, maxidx + 1), []);
-        val T1' = Term_Subst.instantiateT [(tvar, argT)] T1;
+        val T1' = Term_Subst.instantiateT (Term_Subst.TVars.table [(tvar, argT)]) T1;
         val (tyenv', maxidx') = Sign.typ_unify thy (T1', T) (tyenv, maxidx + 1)
           handle Type.TUNIFY => no_unifier (T1', T);
       in (argT, (tyenv', maxidx')) end;
     val (ap_args, (ap_env, maxidx_env)) =
       fold_map unify_ap_type [T2, T3, T23] (Vartab.empty, maxidx_common);
     val [T2_arg, T3_arg, T23_arg] = map (Envir.norm_type ap_env) ap_args;
     val (tvar2, tvar3) = (dest_TVar T2_arg, dest_TVar T3_arg) handle TYPE _ => bad_ap ();
     val _ = if T23_arg = T2_arg --> T3_arg then () else bad_ap ();
     val sort = foldl1 (Sign.inter_sort thy) (map #2 [tvar, tvar2, tvar3]);
     val _ = Sign.of_sort thy (Term.aT sort --> Term.aT sort, sort) orelse
       error ("Sort constraint " ^ quote (Syntax.string_of_sort ctxt sort) ^
         " not closed under function types");
     fun update_sort (v, S) (tyenv, maxidx) =
       (Vartab.update_new (v, (S, TVar ((Name.aT, maxidx + 1), sort))) tyenv, maxidx + 1);
     val (common_env, _) = fold update_sort [tvar, tvar2, tvar3] (ap_env, maxidx_env);
 
     val tvar' = Envir.norm_type common_env (TVar tvar);
     val pure' = norm_term_types common_env pure;
     val (tvar2', tvar3') = apply2 (Envir.norm_type common_env) (T2_arg, T3_arg);
     val ap' = norm_term_types common_env ap;
 
     fun bad_set set = error ("Bad type for set: " ^ show_typ (fastype_of set));
     fun mk_set set =
       let
         val tyenv = Sign.typ_match thy (domain_type (fastype_of set), range_type (fastype_of pure'))
           Vartab.empty
           handle Type.TYPE_MATCH => bad_set set;
         val set' = Envir.subst_term_types tyenv set;
         val set_tvar = fastype_of set' |> range_type |> HOLogic.dest_setT |> dest_TVar
           handle TYPE _ => bad_set set;
         val _ = if Term.eq_tvar (dest_TVar tvar', set_tvar) then () else bad_set set;
       in ([tvar'], set') end
     val set = (case raw_set of
         NONE => ([tvar'], Abs ("x", tvar', HOLogic.mk_UNIV tvar'))
       | SOME t => mk_set (closed_poly_term t));
 
     val terms = Term_Subst.zero_var_indexes (pack_poly_terms
       [poly_type_to_term ([tvar'], range_type (fastype_of pure')),
       ([tvar'], pure'), ([tvar2', tvar3'], ap'), set]);
 
     (*TODO: also infer the relator type?*)
     fun bad_rel rel = error ("Bad type for rel: " ^ show_typ (fastype_of rel));
     fun mk_rel rel =
       let
         val ((T1, T2), (T1_af, T2_af)) = fastype_of rel
           |> dest_funT
           |>> BNF_Util.dest_pred2T
           ||> BNF_Util.dest_pred2T;
         val _ = (dest_TVar T1; dest_TVar T2);
         val _ = if T1 = T2 then bad_rel rel else ();
         val af_inst = mk_afun_inst (match_poly_terms_type ctxt (terms, 0) (T1_af, maxidx_of_term rel));
         val (T1', T2') = apply2 (dest_type ctxt af_inst) (T1_af, T2_af);
         val _ = if (is_none T1' andalso is_none T2') orelse (T1' = SOME T1 andalso T2' = SOME T2)
           then () else bad_rel rel;
       in Term_Subst.zero_var_indexes (pack_poly_terms [([T1, T2], rel)]) end
       handle TYPE _ => bad_rel rel;
     val rel = Option.map (mk_rel o closed_poly_term) raw_rel;
   in (terms, rel) end;
 
 fun mk_rel_intros {pure_transfer, ap_rel_fun} =
   let val pure_rel_intro = pure_transfer RS @{thm rel_funD};
   in [pure_rel_intro, ap_rel_fun] end;
 
 fun mk_afun_thms ctxt af_inst (hom_thm, ichng_thm, reds, rel_axioms) =
   let
     val pure_comp_conv =
       let
         val ([T1, T2, T3], ctxt_Ts) = mk_TFrees_of 3 (inner_sort_of af_inst) ctxt;
         val (((g, f), x), ctxt') = ctxt_Ts
           |> mk_Free "g" (T2 --> T3)
           ||>> mk_Free "f" (mk_type af_inst (T1 --> T2))
           ||>> mk_Free "x" (mk_type af_inst T1);
         val comb = mk_comb af_inst;
         val lhs = comb (T2 --> T3) (lift_term af_inst g, comb (T1 --> T2) (f, x));
         val B_g = Abs ("f", T1 --> T2, Abs ("x", T1, Term.betapply (g, Bound 1 $ Bound 0)));
         val rhs = comb (T1 --> T3)
           (comb ((T1 --> T2) --> T1 --> T3) (lift_term af_inst B_g, f), x);
         val prop = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop;
 
         val merge_rule = mk_meta_eq hom_thm;
         val B_intro = the (Symtab.lookup reds "B") |> mk_meta_eq |> Thm.symmetric;
         val tac =
           HEADGOAL (Raw_Simplifier.rewrite_goal_tac ctxt' [B_intro, merge_rule] THEN'
           resolve_tac ctxt' [@{thm refl}]);
       in singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] prop (K tac)) end;
 
     val eq_intros =
       let
         val ([T1, T2], ctxt_Ts) = mk_TFrees_of 2 (inner_sort_of af_inst) ctxt;
         val T12 = mk_type af_inst (T1 --> T2);
         val (((((x, y), x'), f), g), ctxt') = ctxt_Ts
           |> mk_Free "x" T1
           ||>> mk_Free "y" T1
           ||>> mk_Free "x" (mk_type af_inst T1)
           ||>> mk_Free "f" T12
           ||>> mk_Free "g" T12;
         val pure_fun = mk_pure af_inst T1;
         val pure_cong = Drule.infer_instantiate' ctxt'
           (map (SOME o Thm.cterm_of ctxt') [x, y, pure_fun]) @{thm arg_cong};
         val ap_fun = mk_ap af_inst (T1, T2);
         val ap_cong1 = Drule.infer_instantiate' ctxt'
           (map (SOME o Thm.cterm_of ctxt')  [f, g, ap_fun, x']) @{thm arg1_cong};
       in Variable.export ctxt' ctxt [pure_cong, ap_cong1] end;
 
     val rel_intros = case rel_axioms of
         NONE => []
       | SOME axioms => mk_rel_intros axioms;
   in
     {hom = hom_thm,
       ichng = ichng_thm,
       reds = reds,
       rel_thms = rel_axioms,
       rel_intros = eq_intros @ rel_intros,
       pure_comp_conv = pure_comp_conv}
   end;
 
 fun reuse_TFrees n S (ctxt, Ts) =
   let
     val have_n = Int.min (n, length Ts);
     val (more_Ts, ctxt') = mk_TFrees_of (n - have_n) S ctxt;
   in (take have_n Ts @ more_Ts, (ctxt', Ts @ more_Ts)) end;
 
 fun mk_comb_prop lift_pos thm af_inst ctxt_Ts =
   let
     val base = Thm.prop_of thm;
     val tvars = Term.add_tvars base [];
     val (Ts, (ctxt', Ts')) = reuse_TFrees (length tvars) (inner_sort_of af_inst) ctxt_Ts;
-    val base' = Term_Subst.instantiate (tvars ~~ Ts, []) base;
+    val base' = base
+      |> Term_Subst.instantiate (Term_Subst.TVars.table (tvars ~~ Ts), Term_Subst.Vars.empty);
     val (lhs, rhs) = Logic.dest_equals base';
     val (_, lhs_args) = strip_comb lhs;
     val lift_var = Var o apsnd (mk_type af_inst) o dest_Var;
     val (lhs_args', subst) = fold_index (fn (i, v) =>
       if member (op =) lift_pos i then apfst (cons v)
       else map_prod (cons (lift_var v)) (cons (v, lift_var v))) lhs_args ([], []);
     val (lhs', rhs') = apply2 (subst_lift_term af_inst subst) (lhs, rhs);
     val lifted = (lhs', rhs') |> HOLogic.mk_eq |> HOLogic.mk_Trueprop;
   in (fold Logic.all lhs_args' lifted, (ctxt', Ts')) end;
 
 fun mk_homomorphism_prop af_inst ctxt_Ts =
   let
     val ([T1, T2], (ctxt', Ts')) = reuse_TFrees 2 (inner_sort_of af_inst) ctxt_Ts;
     val ((f, x), _) = ctxt'
       |> mk_Free "f" (T1 --> T2)
       ||>> mk_Free "x" T1;
     val lhs = mk_comb af_inst (T1 --> T2) (lift_term af_inst f, lift_term af_inst x);
     val rhs = lift_term af_inst (f $ x);
     val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in (Logic.all f (Logic.all x prop), (ctxt', Ts')) end;
 
 fun mk_interchange_prop af_inst ctxt_Ts =
   let
     val ([T1, T2], (ctxt', Ts')) = reuse_TFrees 2 (inner_sort_of af_inst) ctxt_Ts;
     val ((f, x), _) = ctxt'
       |> mk_Free "f" (mk_type af_inst (T1 --> T2))
       ||>> mk_Free "x" T1;
     val lhs = mk_comb af_inst (T1 --> T2) (f, lift_term af_inst x);
     val T_x = Abs ("f", T1 --> T2, Bound 0 $ x);
     val rhs = mk_comb af_inst ((T1 --> T2) --> T2) (lift_term af_inst T_x, f);
     val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in (Logic.all f (Logic.all x prop), (ctxt', Ts')) end;
 
 fun mk_rel_props (af_inst, rel_inst) ctxt_Ts =
   let
     fun mk_af_rel tm =
       let val (T1, T2) = BNF_Util.dest_pred2T (fastype_of tm);
       in betapply (instantiate_poly_term rel_inst [T1, T2], tm) end;
 
     val ([T1, T2, T3], (ctxt', Ts')) = reuse_TFrees 3 (inner_sort_of af_inst) ctxt_Ts;
     val (pure_R, _) = mk_Free "R" (T1 --> T2 --> @{typ bool}) ctxt';
     val rel_pure = BNF_Util.mk_rel_fun pure_R (mk_af_rel pure_R) $ mk_pure af_inst T1 $
       mk_pure af_inst T2;
     val pure_prop = Logic.all pure_R (HOLogic.mk_Trueprop rel_pure);
 
     val ((((f, g), x), ap_R), _) = ctxt'
       |> mk_Free "f" (mk_type af_inst (T1 --> T2))
       ||>> mk_Free "g" (mk_type af_inst (T1 --> T3))
       ||>> mk_Free "x" (mk_type af_inst T1)
       ||>> mk_Free "R" (T2 --> T3 --> @{typ bool});
     val fun_rel = BNF_Util.mk_rel_fun (mk_eq_on (mk_set af_inst T1 $ x)) ap_R;
     val rel_ap = Logic.mk_implies (HOLogic.mk_Trueprop (mk_af_rel fun_rel $ f $ g),
       HOLogic.mk_Trueprop (mk_af_rel ap_R $ mk_comb af_inst (T1 --> T2) (f, x) $
         mk_comb af_inst (T1 --> T3) (g, x)));
     val ap_prop = fold_rev Logic.all [ap_R, f, g, x] rel_ap;
   in ([pure_prop, ap_prop], (ctxt', Ts')) end;
 
 fun mk_interchange ctxt ((comb_defs, _), comb_unfolds) (af_inst, merge_thm) reds =
   let
     val T_def = the (Symtab.lookup comb_defs "T");
     val T_red = the (Symtab.lookup reds "T");
     val (weak_prop, (ctxt', _)) = mk_comb_prop [0] T_def af_inst (ctxt, []);
     fun tac {context, ...} =
       HEADGOAL (Raw_Simplifier.rewrite_goal_tac context [Thm.symmetric merge_thm] THEN'
       resolve_tac context [T_red]);
     val weak_red = singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] weak_prop tac);
   in Raw_Simplifier.rewrite_rule ctxt (comb_unfolds) weak_red RS sym end;
 
 fun mk_weak_reds ctxt ((comb_defs, _), comb_unfolds) af_inst (hom_thm, ichng_thm, reds) =
   let
     val unfolded_reds =
       Symtab.map (K (Raw_Simplifier.rewrite_rule ctxt comb_unfolds)) reds;
     val af_thms = mk_afun_thms ctxt af_inst (hom_thm, ichng_thm, unfolded_reds, NONE);
     val af = mk_afun Binding.empty (pack_afun_inst af_inst) NONE af_thms;
 
     fun tac {context, ...} = HEADGOAL (normalize_wrapper_tac context (SOME af) THEN'
       Raw_Simplifier.rewrite_goal_tac context comb_unfolds THEN'
       resolve_tac context [refl]);
     fun mk comb lift_pos =
       let
         val def = the (Symtab.lookup comb_defs comb);
         val (prop, (ctxt', _)) = mk_comb_prop lift_pos def af_inst (ctxt, []);
         val hol_thm = singleton (Variable.export ctxt' ctxt) (Goal.prove ctxt' [] [] prop tac);
       in mk_meta_eq hol_thm end;
 
     val uncurry_thm = mk_meta_eq (forward_lift_rule ctxt af @{thm uncurry_pair});
   in
     [mk "C" [1], mk "C" [2], uncurry_thm]
   end;
 
 fun mk_comb_reds ctxt combss af_inst user_combs (hom_thm, user_thms, ichng_thms) =
   let
     val ((comb_defs, comb_rules), comb_unfolds) = combss;
     val merge_thm = mk_meta_eq hom_thm;
     val user_reds = Symtab.make (user_combs ~~ user_thms);
     val reds0 = combinator_red_closure ctxt (comb_defs, comb_rules) (af_inst, merge_thm) [] user_reds;
     val ichng_thm = case ichng_thms of
         [] => singleton (Variable.export ctxt ctxt) (mk_interchange ctxt combss (af_inst, merge_thm) reds0)
       | [thm] => thm;
     val weak_reds = mk_weak_reds ctxt combss af_inst (hom_thm, ichng_thm, reds0);
     val reds1 = combinator_red_closure ctxt (comb_defs, comb_rules) (af_inst, merge_thm) weak_reds reds0;
     val unfold = Raw_Simplifier.rewrite_rule ctxt comb_unfolds;
   in (Symtab.map (K unfold) reds1, ichng_thm) end;
 
 fun note_afun_thms af =
   let
     val thms = thms_of_afun af;
     val named_thms =
       [("homomorphism", [#hom thms]),
         ("interchange", [#ichng thms]),
         ("afun_rel_intros", #rel_intros thms)] @
       map (fn (name, thm) => ("pure_" ^ name ^ "_conv", [thm])) (Symtab.dest (#reds thms)) @
       (case #rel_thms thms of
         NONE => []
       | SOME rel_thms' =>
           [("pure_transfer", [#pure_transfer rel_thms']),
             ("ap_rel_fun_cong", [#ap_rel_fun rel_thms'])]);
 
     val base_name = Binding.name_of (name_of_afun af);
     fun mk_note (name, thms) =
       ((Binding.qualify true base_name (Binding.name name), []), [(thms, [])]);
   in Local_Theory.notes (map mk_note named_thms) #> #2 end;
 
 fun register_afun af =
   let fun decl phi context = Data.map (fn {combinators, afuns, patterns} =>
     let
       val af' = morph_afun phi af;
       val (name, afuns') = Name_Space.define context true (name_of_afun af', af') afuns;
       val patterns' = Item_Net.update (name, patterns_of_afun af') patterns;
     in {combinators = combinators, afuns = afuns', patterns = patterns'} end) context;
   in Local_Theory.declaration {syntax = false, pervasive = false} decl end;
 
 fun applicative_cmd (((((name, flags), raw_pure), raw_ap), raw_rel), raw_set) lthy =
   let
     val comb_unfolds = Named_Theorems.get lthy @{named_theorems combinator_unfold};
     val comb_reprs = Named_Theorems.get lthy @{named_theorems combinator_repr};
     val (comb_defs, comb_rules) = get_combinators (Context.Proof lthy);
 
     val _ = fold (fn name =>
       if Symtab.defined comb_defs name then I else error ("Unknown combinator " ^ quote name))
       flags ();
     val _ = if has_duplicates op = flags
       then warning "Ignoring duplicate combinators"
       else ();
     val user_combs0 = Ord_List.make fast_string_ord flags;
 
     val raw_pure' = Syntax.read_term lthy raw_pure;
     val raw_ap' = Syntax.read_term lthy raw_ap;
     val raw_rel' = Option.map (Syntax.read_term lthy) raw_rel;
     val raw_set' = Option.map (Syntax.read_term lthy) raw_set;
     val (terms, rel) = mk_terms lthy (raw_pure', raw_ap', raw_rel', raw_set');
 
     val derived_combs0 = combinator_closure comb_rules false user_combs0;
     val required_combs = Ord_List.make fast_string_ord ["B", "I"];
     val user_combs = Ord_List.union fast_string_ord user_combs0
       (Ord_List.subtract fast_string_ord derived_combs0 required_combs);
     val derived_combs1 = combinator_closure comb_rules false user_combs;
     val derived_combs2 = combinator_closure comb_rules true derived_combs1;
     fun is_redundant comb = eq_list (op =) (derived_combs2,
       (combinator_closure comb_rules true (Ord_List.remove fast_string_ord comb user_combs)));
     val redundant_combs = filter is_redundant user_combs;
     val _ = if null redundant_combs then () else
       warning ("Redundant combinators: " ^ commas redundant_combs);
     val prove_interchange = not (Ord_List.member fast_string_ord derived_combs1 "T");
 
     val (af_inst, ctxt_af) = import_afun_inst_raw terms lthy;
     (* TODO: reuse TFrees from above *)
     val (rel_insts, ctxt_inst) = (case rel of
         NONE => (NONE, ctxt_af)
       | SOME r =>
           let
             val (rel_inst, ctxt') = import_poly_terms r ctxt_af |>> the_single;
             val T = fastype_of (#2 rel_inst) |> range_type |> domain_type;
             val af_inst = match_poly_terms_type ctxt' (terms, 0) (T, ~1) |> mk_afun_inst;
           in (SOME (af_inst, rel_inst), ctxt') end);
 
     val mk_propss = [apfst single o mk_homomorphism_prop af_inst,
       fold_map (fn comb => mk_comb_prop [] (the (Symtab.lookup comb_defs comb)) af_inst) user_combs,
       if prove_interchange then apfst single o mk_interchange_prop af_inst else pair [],
       if is_some rel then mk_rel_props (the rel_insts) else pair []];
     val (propss, (ctxt_Ts, _)) = fold_map I mk_propss (ctxt_inst, []);
 
     fun repr_tac ctxt = Raw_Simplifier.rewrite_goals_tac ctxt comb_reprs;
     fun after_qed thmss lthy' =
       let
         val [[hom_thm], user_thms, ichng_thms, rel_thms] = map (Variable.export lthy' ctxt_inst) thmss;
         val (reds, ichng_thm) = mk_comb_reds ctxt_inst ((comb_defs, comb_rules), comb_unfolds)
           af_inst user_combs (hom_thm, user_thms, ichng_thms);
         val rel_axioms = case rel_thms of
             [] => NONE
           | [thm1, thm2] => SOME {pure_transfer = thm1, ap_rel_fun = thm2};
         val af_thms = mk_afun_thms ctxt_inst af_inst (hom_thm, ichng_thm, reds, rel_axioms);
         val af_thms = map_afun_thms (singleton (Variable.export ctxt_inst lthy)) af_thms;
         val af = mk_afun name terms rel af_thms;
       in lthy
         |> register_afun af
         |> note_afun_thms af
       end;
   in
     Proof.theorem NONE after_qed ((map o map) (rpair []) propss) ctxt_Ts
     |> Proof.refine (Method.Basic (SIMPLE_METHOD o repr_tac))
     |> Seq.the_result ""
   end;
 
 fun print_afuns ctxt =
   let
     fun pretty_afun (name, af) =
       let
         val [pT, (_, pure), (_, ap), (_, set)] = unpack_poly_terms (terms_of_afun af);
         val ([tvar], T) = poly_type_of_term pT;
         val rel = Option.map (#2 o the_single o unpack_poly_terms) (rel_of_afun af);
         val combinators = Symtab.keys (#reds (thms_of_afun af));
       in Pretty.block (Pretty.fbreaks ([Pretty.block [Pretty.str name, Pretty.str ":", Pretty.brk 1,
           Pretty.quote (Syntax.pretty_typ ctxt T), Pretty.brk 1, Pretty.str "of", Pretty.brk 1,
           Syntax.pretty_typ ctxt tvar],
         Pretty.block [Pretty.str "pure:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt pure)],
         Pretty.block [Pretty.str "ap:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt ap)],
         Pretty.block [Pretty.str "set:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt set)]] @
         (case rel of
           NONE => []
         | SOME rel' => [Pretty.block [Pretty.str "rel:", Pretty.brk 1,
             Pretty.quote (Syntax.pretty_term ctxt rel')]]) @
         [Pretty.block ([Pretty.str "combinators:", Pretty.brk 1] @
           Pretty.commas (map Pretty.str combinators))])) end;
     val afuns = sort_by #1 (Name_Space.fold_table cons (get_afun_table (Context.Proof ctxt)) []);
   in Pretty.writeln (Pretty.big_list "Registered applicative functors:" (map pretty_afun afuns)) end;
 
 
 (* Unfolding *)
 
 fun add_unfold_thm name thm context =
   let
     val (lhs, _) = Thm.prop_of thm |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
       handle TERM _ => error "Not an equation";
     val names = case name of
         SOME n => [intern context n]
       | NONE => case match_typ context (Term.fastype_of lhs) of
           ns as (_::_) => ns
         | [] => error "Unable to determine applicative functor instance";
     val _ = map (afun_of_generic context) names;
     (*TODO: check equation*)
     val thm' = mk_meta_eq thm;
   in fold (fn n => update_afun n (add_unfolds_afun [thm'])) names context end;
 
 fun add_unfold_attrib name = Thm.declaration_attribute (add_unfold_thm name);
 
 (*TODO: attribute to delete unfolds*)
 
 end;
diff --git a/thys/Refine_Imperative_HOL/Sepref_Rules.thy b/thys/Refine_Imperative_HOL/Sepref_Rules.thy
--- a/thys/Refine_Imperative_HOL/Sepref_Rules.thy
+++ b/thys/Refine_Imperative_HOL/Sepref_Rules.thy
@@ -1,1745 +1,1745 @@
 section \<open>Refinement Rule Management\<close>
 theory Sepref_Rules
 imports Sepref_Basic Sepref_Constraints
 begin
   text \<open>This theory contains tools for managing the refinement rules used by Sepref\<close>
 
   text \<open>The theories are based on uncurried functions, i.e.,
     every function has type @{typ "'a\<Rightarrow>'b"}, where @{typ 'a} is the 
     tuple of parameters, or unit if there are none.
     \<close>
 
 
   subsection \<open>Assertion Interface Binding\<close>
   text \<open>Binding of interface types to refinement assertions\<close>
   definition intf_of_assn :: "('a \<Rightarrow> _ \<Rightarrow> assn) \<Rightarrow> 'b itself \<Rightarrow> bool" where
     [simp]: "intf_of_assn a b = True"
 
   lemma intf_of_assnI: "intf_of_assn R TYPE('a)" by simp
   
   named_theorems_rev intf_of_assn \<open>Links between refinement assertions and interface types\<close>  
 
   lemma intf_of_assn_fallback: "intf_of_assn (R :: 'a \<Rightarrow> _ \<Rightarrow> assn) TYPE('a)" by simp
 
   subsection \<open>Function Refinement with Precondition\<close>
   definition fref :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'c) set \<Rightarrow> ('b \<times> 'd) set
            \<Rightarrow> (('a \<Rightarrow> 'b) \<times> ('c \<Rightarrow> 'd)) set"
     ("[_]\<^sub>f _ \<rightarrow> _" [0,60,60] 60)         
   where "[P]\<^sub>f R \<rightarrow> S \<equiv> {(f,g). \<forall>x y. P y \<and> (x,y)\<in>R \<longrightarrow> (f x, g y)\<in>S}"
   
   abbreviation freft ("_ \<rightarrow>\<^sub>f _" [60,60] 60) where "R \<rightarrow>\<^sub>f S \<equiv> ([\<lambda>_. True]\<^sub>f R \<rightarrow> S)"
   
   lemma rel2p_fref[rel2p]: "rel2p (fref P R S) 
     = (\<lambda>f g. (\<forall>x y. P y \<longrightarrow> rel2p R x y \<longrightarrow> rel2p S (f x) (g y)))"  
     by (auto simp: fref_def rel2p_def[abs_def])
 
   lemma fref_cons:  
     assumes "(f,g) \<in> [P]\<^sub>f R \<rightarrow> S"
     assumes "\<And>c a. (c,a)\<in>R' \<Longrightarrow> Q a \<Longrightarrow> P a"
     assumes "R' \<subseteq> R"
     assumes "S \<subseteq> S'"
     shows "(f,g) \<in> [Q]\<^sub>f R' \<rightarrow> S'"
     using assms
     unfolding fref_def
     by fastforce
 
   lemmas fref_cons' = fref_cons[OF _ _ order_refl order_refl]  
 
   lemma frefI[intro?]: 
     assumes "\<And>x y. \<lbrakk>P y; (x,y)\<in>R\<rbrakk> \<Longrightarrow> (f x, g y)\<in>S"
     shows "(f,g)\<in>fref P R S"
     using assms
     unfolding fref_def
     by auto
 
   lemma fref_ncI: "(f,g)\<in>R\<rightarrow>S \<Longrightarrow> (f,g)\<in>R\<rightarrow>\<^sub>fS"  
     apply (rule frefI)
     apply parametricity
     done
 
   lemma frefD: 
     assumes "(f,g)\<in>fref P R S"
     shows "\<lbrakk>P y; (x,y)\<in>R\<rbrakk> \<Longrightarrow> (f x, g y)\<in>S"
     using assms
     unfolding fref_def
     by auto
 
   lemma fref_ncD: "(f,g)\<in>R\<rightarrow>\<^sub>fS \<Longrightarrow> (f,g)\<in>R\<rightarrow>S"  
     apply (rule fun_relI)
     apply (drule frefD)
     apply simp
     apply assumption+
     done
 
 
   lemma fref_compI: 
     "fref P R1 R2 O fref Q S1 S2 \<subseteq>
       fref (\<lambda>x. Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> P y)) (R1 O S1) (R2 O S2)"
     unfolding fref_def
     apply (auto)
     apply blast
     done
 
   lemma fref_compI':
     "\<lbrakk> (f,g)\<in>fref P R1 R2; (g,h)\<in>fref Q S1 S2 \<rbrakk> 
       \<Longrightarrow> (f,h) \<in> fref (\<lambda>x. Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> P y)) (R1 O S1) (R2 O S2)"
     using fref_compI[of P R1 R2 Q S1 S2]   
     by auto
 
   lemma fref_unit_conv:
     "(\<lambda>_. c, \<lambda>_. a) \<in> fref P unit_rel S \<longleftrightarrow> (P () \<longrightarrow> (c,a)\<in>S)"   
     by (auto simp: fref_def)
 
   lemma fref_uncurry_conv:
     "(uncurry c, uncurry a) \<in> fref P (R1\<times>\<^sub>rR2) S 
     \<longleftrightarrow> (\<forall>x1 y1 x2 y2. P (y1,y2) \<longrightarrow> (x1,y1)\<in>R1 \<longrightarrow> (x2,y2)\<in>R2 \<longrightarrow> (c x1 x2, a y1 y2) \<in> S)"
     by (auto simp: fref_def)
 
   lemma fref_mono: "\<lbrakk> \<And>x. P' x \<Longrightarrow> P x; R' \<subseteq> R; S \<subseteq> S' \<rbrakk> 
     \<Longrightarrow> fref P R S \<subseteq> fref P' R' S'"  
     unfolding fref_def
     by auto blast
 
   lemma fref_composeI:
     assumes FR1: "(f,g)\<in>fref P R1 R2"
     assumes FR2: "(g,h)\<in>fref Q S1 S2"
     assumes C1: "\<And>x. P' x \<Longrightarrow> Q x"
     assumes C2: "\<And>x y. \<lbrakk>P' x; (y,x)\<in>S1\<rbrakk> \<Longrightarrow> P y"
     assumes R1: "R' \<subseteq> R1 O S1"
     assumes R2: "R2 O S2 \<subseteq> S'"
     assumes FH: "f'=f" "h'=h"
     shows "(f',h') \<in> fref P' R' S'"
     unfolding FH
     apply (rule subsetD[OF fref_mono fref_compI'[OF FR1 FR2]])
     using C1 C2 apply blast
     using R1 apply blast
     using R2 apply blast
     done
 
   lemma fref_triv: "A\<subseteq>Id \<Longrightarrow> (f,f)\<in>[P]\<^sub>f A \<rightarrow> Id"
     by (auto simp: fref_def)
 
 
   subsection \<open>Heap-Function Refinement\<close>
   text \<open>
     The following relates a heap-function with a pure function.
     It contains a precondition, a refinement assertion for the arguments
     before and after execution, and a refinement relation for the result.
     \<close>
   (* TODO: We only use this with keep/destroy information, so we could model
     the parameter relations as such (('a\<Rightarrow>'ai \<Rightarrow> assn) \<times> bool) *)
   definition hfref 
     :: "
       ('a \<Rightarrow> bool) 
    \<Rightarrow> (('a \<Rightarrow> 'ai \<Rightarrow> assn) \<times> ('a \<Rightarrow> 'ai \<Rightarrow> assn)) 
    \<Rightarrow> ('b \<Rightarrow> 'bi \<Rightarrow> assn) 
    \<Rightarrow> (('ai \<Rightarrow> 'bi Heap) \<times> ('a\<Rightarrow>'b nres)) set"
    ("[_]\<^sub>a _ \<rightarrow> _" [0,60,60] 60)
    where
     "[P]\<^sub>a RS \<rightarrow> T \<equiv> { (f,g) . \<forall>c a.  P a \<longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)}"
 
   abbreviation hfreft ("_ \<rightarrow>\<^sub>a _" [60,60] 60) where "RS \<rightarrow>\<^sub>a T \<equiv> ([\<lambda>_. True]\<^sub>a RS \<rightarrow> T)"
 
   lemma hfrefI[intro?]: 
     assumes "\<And>c a. P a \<Longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)"
     shows "(f,g)\<in>hfref P RS T"
     using assms unfolding hfref_def by blast
 
   lemma hfrefD: 
     assumes "(f,g)\<in>hfref P RS T"
     shows "\<And>c a. P a \<Longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)"
     using assms unfolding hfref_def by blast
 
   lemma hfref_to_ASSERT_conv: 
     "NO_MATCH (\<lambda>_. True) P \<Longrightarrow> (a,b)\<in>[P]\<^sub>a R \<rightarrow> S \<longleftrightarrow> (a,\<lambda>x. ASSERT (P x) \<then> b x) \<in> R \<rightarrow>\<^sub>a S"  
     unfolding hfref_def
     apply (clarsimp; safe; clarsimp?)
     apply (rule hn_refine_nofailI)
     apply (simp add: refine_pw_simps)
     subgoal for xc xa
       apply (drule spec[of _ xc])
       apply (drule spec[of _ xa])
       by simp
     done
 
   text \<open>
     A pair of argument refinement assertions can be created by the 
     input assertion and the information whether the parameter is kept or destroyed
     by the function.
     \<close>  
   primrec hf_pres 
     :: "('a \<Rightarrow> 'b \<Rightarrow> assn) \<Rightarrow> bool \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> assn)\<times>('a \<Rightarrow> 'b \<Rightarrow> assn)"
     where 
       "hf_pres R True = (R,R)" | "hf_pres R False = (R,invalid_assn R)"
 
   abbreviation hfkeep 
     :: "('a \<Rightarrow> 'b \<Rightarrow> assn) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> assn)\<times>('a \<Rightarrow> 'b \<Rightarrow> assn)" 
     ("(_\<^sup>k)" [1000] 999)
     where "R\<^sup>k \<equiv> hf_pres R True"
   abbreviation hfdrop 
     :: "('a \<Rightarrow> 'b \<Rightarrow> assn) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> assn)\<times>('a \<Rightarrow> 'b \<Rightarrow> assn)" 
     ("(_\<^sup>d)" [1000] 999)
     where "R\<^sup>d \<equiv> hf_pres R False"
 
   abbreviation "hn_kede R kd \<equiv> hn_ctxt (snd (hf_pres R kd))"
   abbreviation "hn_keep R \<equiv> hn_kede R True"
   abbreviation "hn_dest R \<equiv> hn_kede R False"
 
   lemma keep_drop_sels[simp]:  
     "fst (R\<^sup>k) = R"
     "snd (R\<^sup>k) = R"
     "fst (R\<^sup>d) = R"
     "snd (R\<^sup>d) = invalid_assn R"
     by auto
 
   lemma hf_pres_fst[simp]: "fst (hf_pres R k) = R" by (cases k) auto
 
   text \<open>
     The following operator combines multiple argument assertion-pairs to
     argument assertion-pairs for the product. It is required to state
     argument assertion-pairs for uncurried functions.
     \<close>  
   definition hfprod :: "
     (('a \<Rightarrow> 'b \<Rightarrow> assn)\<times>('a \<Rightarrow> 'b \<Rightarrow> assn)) 
     \<Rightarrow> (('c \<Rightarrow> 'd \<Rightarrow> assn)\<times>('c \<Rightarrow> 'd \<Rightarrow> assn))
     \<Rightarrow> ((('a\<times>'c) \<Rightarrow> ('b \<times> 'd) \<Rightarrow> assn) \<times> (('a\<times>'c) \<Rightarrow> ('b \<times> 'd) \<Rightarrow> assn))"
     (infixl "*\<^sub>a" 65)
     where "RR *\<^sub>a SS \<equiv> (prod_assn (fst RR) (fst SS), prod_assn (snd RR) (snd SS))"
 
   lemma hfprod_fst_snd[simp]:
     "fst (A *\<^sub>a B) = prod_assn (fst A) (fst B)" 
     "snd (A *\<^sub>a B) = prod_assn (snd A) (snd B)" 
     unfolding hfprod_def by auto
 
 
 
   subsubsection \<open>Conversion from fref to hfref\<close>  
   (* TODO: Variant of import-param! Automate this! *)
   lemma fref_to_pure_hfref':
     assumes "(f,g) \<in> [P]\<^sub>f R\<rightarrow>\<langle>S\<rangle>nres_rel"
     assumes "\<And>x. x\<in>Domain R \<inter> R\<inverse>``Collect P \<Longrightarrow> f x = RETURN (f' x)"
     shows "(return o f', g) \<in> [P]\<^sub>a (pure R)\<^sup>k\<rightarrow>pure S"
     apply (rule hfrefI) apply (rule hn_refineI)
     using assms
     apply ((sep_auto simp: fref_def pure_def pw_le_iff pw_nres_rel_iff
       refine_pw_simps eintros del: exI))
     apply force
     done
 
 
   subsubsection \<open>Conversion from hfref to hnr\<close>  
   text \<open>This section contains the lemmas. The ML code is further down. \<close>
   lemma hf2hnr:
     assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
     shows "\<forall>x xi. P x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)"
     using assms
     unfolding hfref_def 
     by (auto simp: hn_ctxt_def)
 
   (*lemma hf2hnr_new:
     assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
     shows "\<forall>x xi. (\<forall>h. h\<Turnstile>fst R x xi \<longrightarrow> P x) \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f xi) (emp * hn_ctxt (snd R) x xi) S (g$x)"
     using assms
     unfolding hfref_def 
     by (auto simp: hn_ctxt_def intro: hn_refine_preI)
   *)
 
 
   (* Products that stem from currying are tagged by a special refinement relation *)  
   definition [simp]: "to_hnr_prod \<equiv> prod_assn"
 
   lemma to_hnr_prod_fst_snd:
     "fst (A *\<^sub>a B) = to_hnr_prod (fst A) (fst B)" 
     "snd (A *\<^sub>a B) = to_hnr_prod (snd A) (snd B)" 
     unfolding hfprod_def by auto
 
   (* Warning: This lemma is carefully set up to be applicable as an unfold rule,
     for more than one level of uncurrying*)
   lemma hnr_uncurry_unfold: "
     (\<forall>x xi. P x \<longrightarrow> 
       hn_refine 
         (\<Gamma> * hn_ctxt (to_hnr_prod A B) x xi) 
         (fi xi) 
         (\<Gamma>' * hn_ctxt (to_hnr_prod A' B') x xi) 
         R 
         (f x))
 \<longleftrightarrow> (\<forall>b bi a ai. P (a,b) \<longrightarrow>
       hn_refine 
         (\<Gamma> * hn_ctxt B b bi * hn_ctxt A a ai) 
         (fi (ai,bi)) 
         (\<Gamma>' * hn_ctxt B' b bi * hn_ctxt A' a ai)
         R
         (f (a,b))
     )"
     by (auto simp: hn_ctxt_def prod_assn_def star_aci)
     
   lemma hnr_intro_dummy:
     "\<forall>x xi. P x \<longrightarrow> hn_refine (\<Gamma> x xi) (c xi) (\<Gamma>' x xi) R (a x) \<Longrightarrow> \<forall>x xi. P x \<longrightarrow> hn_refine (emp*\<Gamma> x xi) (c xi) (emp*\<Gamma>' x xi) R (a x)" 
     by simp
 
   lemma hn_ctxt_ctxt_fix_conv: "hn_ctxt (hn_ctxt R) = hn_ctxt R"
     by (simp add: hn_ctxt_def[abs_def])
 
   lemma uncurry_APP: "uncurry f$(a,b) = f$a$b" by auto
 
   (* TODO: Replace by more general rule. *)  
   lemma norm_RETURN_o: 
     "\<And>f. (RETURN o f)$x = (RETURN$(f$x))"
     "\<And>f. (RETURN oo f)$x$y = (RETURN$(f$x$y))"
     "\<And>f. (RETURN ooo f)$x$y$z = (RETURN$(f$x$y$z))"
     "\<And>f. (\<lambda>x. RETURN ooo f x)$x$y$z$a = (RETURN$(f$x$y$z$a))"
     "\<And>f. (\<lambda>x y. RETURN ooo f x y)$x$y$z$a$b = (RETURN$(f$x$y$z$a$b))"
     by auto
 
   lemma norm_return_o: 
     "\<And>f. (return o f)$x = (return$(f$x))"
     "\<And>f. (return oo f)$x$y = (return$(f$x$y))"
     "\<And>f. (return ooo f)$x$y$z = (return$(f$x$y$z))"
     "\<And>f. (\<lambda>x. return ooo f x)$x$y$z$a = (return$(f$x$y$z$a))"
     "\<And>f. (\<lambda>x y. return ooo f x y)$x$y$z$a$b = (return$(f$x$y$z$a$b))"
     by auto
 
   
   lemma hn_val_unit_conv_emp[simp]: "hn_val unit_rel x y = emp"
     by (auto simp: hn_ctxt_def pure_def)
 
   subsubsection \<open>Conversion from hnr to hfref\<close>  
   text \<open>This section contains the lemmas. The ML code is further down. \<close>
 
   abbreviation "id_assn \<equiv> pure Id"
   abbreviation "unit_assn \<equiv> id_assn :: unit \<Rightarrow> _"
 
   lemma pure_unit_rel_eq_empty: "unit_assn x y = emp"  
     by (auto simp: pure_def)
 
   lemma uc_hfprod_sel:
     "fst (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \<Rightarrow> fst A a1 c1 * fst B a2 c2)" 
     "snd (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \<Rightarrow> snd A a1 c1 * snd B a2 c2)" 
     unfolding hfprod_def prod_assn_def[abs_def] by auto
 
 
   subsubsection \<open>Conversion from relation to fref\<close>  
   text \<open>This section contains the lemmas. The ML code is further down. \<close>
 
   definition "CURRY R \<equiv> { (f,g). (uncurry f, uncurry g) \<in> R }"
 
   lemma fref_param1: "R\<rightarrow>S = fref (\<lambda>_. True) R S"  
     by (auto simp: fref_def fun_relD)
 
   lemma fref_nest: "fref P1 R1 (fref P2 R2 S) 
     \<equiv> CURRY (fref (\<lambda>(a,b). P1 a \<and> P2 b) (R1\<times>\<^sub>rR2) S)"
     apply (rule eq_reflection)
     by (auto simp: fref_def CURRY_def)
 
   lemma in_CURRY_conv: "(f,g) \<in> CURRY R \<longleftrightarrow> (uncurry f, uncurry g) \<in> R"  
     unfolding CURRY_def by auto
 
   lemma uncurry0_APP[simp]: "uncurry0 c $ x = c" by auto
 
   lemma fref_param0I: "(c,a)\<in>R \<Longrightarrow> (uncurry0 c, uncurry0 a) \<in> fref (\<lambda>_. True) unit_rel R"
     by (auto simp: fref_def)
 
   subsubsection \<open>Composition\<close>
   definition hr_comp :: "('b \<Rightarrow> 'c \<Rightarrow> assn) \<Rightarrow> ('b \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> assn"
     \<comment> \<open>Compose refinement assertion with refinement relation\<close>
     where "hr_comp R1 R2 a c \<equiv> \<exists>\<^sub>Ab. R1 b c * \<up>((b,a)\<in>R2)"
 
   definition hrp_comp 
     :: "('d \<Rightarrow> 'b \<Rightarrow> assn) \<times> ('d \<Rightarrow> 'c \<Rightarrow> assn)
         \<Rightarrow> ('d \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> assn) \<times> ('a \<Rightarrow> 'c \<Rightarrow> assn)"
     \<comment> \<open>Compose argument assertion-pair with refinement relation\<close>    
     where "hrp_comp RR' S \<equiv> (hr_comp (fst RR') S, hr_comp (snd RR') S) "
 
   lemma hr_compI: "(b,a)\<in>R2 \<Longrightarrow> R1 b c \<Longrightarrow>\<^sub>A hr_comp R1 R2 a c"  
     unfolding hr_comp_def
     by sep_auto
 
   lemma hr_comp_Id1[simp]: "hr_comp (pure Id) R = pure R"  
     unfolding hr_comp_def[abs_def] pure_def
     apply (intro ext ent_iffI)
     by sep_auto+
 
   lemma hr_comp_Id2[simp]: "hr_comp R Id = R"  
     unfolding hr_comp_def[abs_def]
     apply (intro ext ent_iffI)
     by sep_auto+
     
   (*lemma hr_comp_invalid[simp]: "hr_comp (\<lambda>a c. true) R a c = true * \<up>(\<exists>b. (b,a)\<in>R)"
     unfolding hr_comp_def[abs_def]
     apply (intro ext ent_iffI)
     apply sep_auto+
     done*)
     
   lemma hr_comp_emp[simp]: "hr_comp (\<lambda>a c. emp) R a c = \<up>(\<exists>b. (b,a)\<in>R)"
     unfolding hr_comp_def[abs_def]
     apply (intro ext ent_iffI)
     apply sep_auto+
     done
 
   lemma hr_comp_prod_conv[simp]:
     "hr_comp (prod_assn Ra Rb) (Ra' \<times>\<^sub>r Rb') 
     = prod_assn (hr_comp Ra Ra') (hr_comp Rb Rb')"  
     unfolding hr_comp_def[abs_def] prod_assn_def[abs_def]
     apply (intro ext ent_iffI)
     apply solve_entails apply clarsimp apply sep_auto
     apply clarsimp apply (intro ent_ex_preI)
     apply (rule ent_ex_postI) apply (sep_auto split: prod.splits)
     done
 
   lemma hr_comp_pure: "hr_comp (pure R) S = pure (R O S)"  
     apply (intro ext)
     apply (rule ent_iffI)
     unfolding hr_comp_def[abs_def] 
     apply (sep_auto simp: pure_def)+
     done
 
   lemma hr_comp_is_pure[safe_constraint_rules]: "is_pure A \<Longrightarrow> is_pure (hr_comp A B)"
     by (auto simp: hr_comp_pure is_pure_conv)
 
   lemma hr_comp_the_pure: "is_pure A \<Longrightarrow> the_pure (hr_comp A B) = the_pure A O B"
     unfolding is_pure_conv
     by (clarsimp simp: hr_comp_pure)
 
   lemma rdomp_hrcomp_conv: "rdomp (hr_comp A R) x \<longleftrightarrow> (\<exists>y. rdomp A y \<and> (y,x)\<in>R)"
     by (auto simp: rdomp_def hr_comp_def)
 
   lemma hn_rel_compI: 
     "\<lbrakk>nofail a; (b,a)\<in>\<langle>R2\<rangle>nres_rel\<rbrakk> \<Longrightarrow> hn_rel R1 b c \<Longrightarrow>\<^sub>A hn_rel (hr_comp R1 R2) a c"
     unfolding hr_comp_def hn_rel_def nres_rel_def
     apply (clarsimp intro!: ent_ex_preI)
     apply (drule (1) order_trans)
     apply (simp add: ret_le_down_conv)
     by sep_auto
 
   lemma hr_comp_precise[constraint_rules]:
     assumes [safe_constraint_rules]: "precise R"
     assumes SV: "single_valued S"
     shows "precise (hr_comp R S)"
     apply (rule preciseI)
     unfolding hr_comp_def
     apply clarsimp
     by (metis SV assms(1) preciseD single_valuedD)
 
   lemma hr_comp_assoc: "hr_comp (hr_comp R S) T = hr_comp R (S O T)"
     apply (intro ext)
     unfolding hr_comp_def
     apply (rule ent_iffI; clarsimp)
     apply sep_auto
     apply (rule ent_ex_preI; clarsimp) (* TODO: 
       sep_auto/solve_entails is too eager splitting the subgoal here! *)
     apply sep_auto
     done
 
 
   lemma hnr_comp:
     assumes R: "\<And>b1 c1. P b1 \<Longrightarrow> hn_refine (R1 b1 c1 * \<Gamma>) (c c1) (R1p b1 c1 * \<Gamma>') R (b b1)"
     assumes S: "\<And>a1 b1. \<lbrakk>Q a1; (b1,a1)\<in>R1'\<rbrakk> \<Longrightarrow> (b b1,a a1)\<in>\<langle>R'\<rangle>nres_rel"
     assumes PQ: "\<And>a1 b1. \<lbrakk>Q a1; (b1,a1)\<in>R1'\<rbrakk> \<Longrightarrow> P b1"
     assumes Q: "Q a1"
     shows "hn_refine 
       (hr_comp R1 R1' a1 c1 * \<Gamma>) 
       (c c1)
       (hr_comp R1p R1' a1 c1 * \<Gamma>') 
       (hr_comp R R') 
       (a a1)"
     unfolding hn_refine_alt
   proof clarsimp
     assume NF: "nofail (a a1)"
     show "
       <hr_comp R1 R1' a1 c1 * \<Gamma>> 
         c c1 
       <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t"
       apply (subst hr_comp_def)
       apply (clarsimp intro!: norm_pre_ex_rule)
     proof -
       fix b1
       assume R1: "(b1, a1) \<in> R1'"
 
       from S R1 Q have R': "(b b1, a a1) \<in> \<langle>R'\<rangle>nres_rel" by blast
       with NF have NFB: "nofail (b b1)" 
         by (simp add: nres_rel_def pw_le_iff refine_pw_simps)
       
       from PQ R1 Q have P: "P b1" by blast
       with NFB R have "<R1 b1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel R (b b1) r * (R1p b1 c1 * \<Gamma>')>\<^sub>t"
         unfolding hn_refine_alt by auto
       thus "<R1 b1 c1 * \<Gamma>> 
         c c1 
         <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t"
         apply (rule cons_post_rule)
         apply (solve_entails)
         by (intro ent_star_mono hn_rel_compI[OF NF R'] hr_compI[OF R1] ent_refl)
     qed
   qed    
 
   lemma hnr_comp1_aux:
     assumes R: "\<And>b1 c1. P b1 \<Longrightarrow> hn_refine (hn_ctxt R1 b1 c1) (c c1) (hn_ctxt R1p b1 c1) R (b$b1)"
     assumes S: "\<And>a1 b1. \<lbrakk>Q a1; (b1,a1)\<in>R1'\<rbrakk> \<Longrightarrow> (b$b1,a$a1)\<in>\<langle>R'\<rangle>nres_rel"
     assumes PQ: "\<And>a1 b1. \<lbrakk>Q a1; (b1,a1)\<in>R1'\<rbrakk> \<Longrightarrow> P b1"
     assumes Q: "Q a1"
     shows "hn_refine 
       (hr_comp R1 R1' a1 c1) 
       (c c1)
       (hr_comp R1p R1' a1 c1) 
       (hr_comp R R') 
       (a a1)"
     using assms hnr_comp[where \<Gamma>=emp and \<Gamma>'=emp and a=a and b=b and c=c and P=P and Q=Q]  
     unfolding hn_ctxt_def
     by auto
 
   lemma hfcomp:
     assumes A: "(f,g) \<in> [P]\<^sub>a RR' \<rightarrow> S"
     assumes B: "(g,h) \<in> [Q]\<^sub>f T \<rightarrow> \<langle>U\<rangle>nres_rel"
     shows "(f,h) \<in> [\<lambda>a. Q a \<and> (\<forall>a'. (a',a)\<in>T \<longrightarrow> P a')]\<^sub>a 
       hrp_comp RR' T \<rightarrow> hr_comp S U"
     using assms  
     unfolding fref_def hfref_def hrp_comp_def
     apply clarsimp
     apply (rule hnr_comp1_aux[of 
         P "fst RR'" f "snd RR'" S g "\<lambda>a. Q a \<and> (\<forall>a'. (a',a)\<in>T \<longrightarrow> P a')" T h U])
     apply (auto simp: hn_ctxt_def)
     done
 
   lemma hfref_weaken_pre_nofail: 
     assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"  
     shows "(f,g) \<in> [\<lambda>x. nofail (g x) \<longrightarrow> P x]\<^sub>a R \<rightarrow> S"
     using assms
     unfolding hfref_def hn_refine_def
     by auto
 
   lemma hfref_cons:
     assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
     assumes "\<And>x. P' x \<Longrightarrow> P x"
     assumes "\<And>x y. fst R' x y \<Longrightarrow>\<^sub>t fst R x y"
     assumes "\<And>x y. snd R x y \<Longrightarrow>\<^sub>t snd R' x y"
     assumes "\<And>x y. S x y \<Longrightarrow>\<^sub>t S' x y"
     shows "(f,g) \<in> [P']\<^sub>a R' \<rightarrow> S'"
     unfolding hfref_def
     apply clarsimp
     apply (rule hn_refine_cons)
     apply (rule assms(3))
     defer
     apply (rule entt_trans[OF assms(4)]; sep_auto)
     apply (rule assms(5))
     apply (frule assms(2))
     using assms(1)
     unfolding hfref_def
     apply auto
     done
 
   subsubsection \<open>Composition Automation\<close>  
   text \<open>This section contains the lemmas. The ML code is further down. \<close>
 
   lemma prod_hrp_comp: 
     "hrp_comp (A *\<^sub>a B) (C \<times>\<^sub>r D) = hrp_comp A C *\<^sub>a hrp_comp B D"
     unfolding hrp_comp_def hfprod_def by simp
   
   lemma hrp_comp_keep: "hrp_comp (A\<^sup>k) B = (hr_comp A B)\<^sup>k"
     by (auto simp: hrp_comp_def)
 
   lemma hr_comp_invalid: "hr_comp (invalid_assn R1) R2 = invalid_assn (hr_comp R1 R2)"
     apply (intro ent_iffI entailsI ext)
     unfolding invalid_assn_def hr_comp_def
     by auto
 
   lemma hrp_comp_dest: "hrp_comp (A\<^sup>d) B = (hr_comp A B)\<^sup>d"
     by (auto simp: hrp_comp_def hr_comp_invalid)
 
 
 
   definition "hrp_imp RR RR' \<equiv> 
     \<forall>a b. (fst RR' a b \<Longrightarrow>\<^sub>t fst RR a b) \<and> (snd RR a b \<Longrightarrow>\<^sub>t snd RR' a b)"
 
   lemma hfref_imp: "hrp_imp RR RR' \<Longrightarrow> [P]\<^sub>a RR \<rightarrow> S \<subseteq> [P]\<^sub>a RR' \<rightarrow> S"  
     apply clarsimp
     apply (erule hfref_cons)
     apply (simp_all add: hrp_imp_def)
     done
     
   lemma hrp_imp_refl: "hrp_imp RR RR"
     unfolding hrp_imp_def by auto
 
   lemma hrp_imp_reflI: "RR = RR' \<Longrightarrow> hrp_imp RR RR'"
     unfolding hrp_imp_def by auto
 
 
   lemma hrp_comp_cong: "hrp_imp A A' \<Longrightarrow> B=B' \<Longrightarrow> hrp_imp (hrp_comp A B) (hrp_comp A' B')"
     by (sep_auto simp: hrp_imp_def hrp_comp_def hr_comp_def entailst_def)
     
   lemma hrp_prod_cong: "hrp_imp A A' \<Longrightarrow> hrp_imp B B' \<Longrightarrow> hrp_imp (A*\<^sub>aB) (A'*\<^sub>aB')"
     by (sep_auto simp: hrp_imp_def prod_assn_def intro: entt_star_mono)
 
   lemma hrp_imp_trans: "hrp_imp A B \<Longrightarrow> hrp_imp B C \<Longrightarrow> hrp_imp A C"  
     unfolding hrp_imp_def
     by (fastforce intro: entt_trans)
 
   lemma fcomp_norm_dflt_init: "x\<in>[P]\<^sub>a R \<rightarrow> T \<Longrightarrow> hrp_imp R S \<Longrightarrow> x\<in>[P]\<^sub>a S \<rightarrow> T"
     apply (erule rev_subsetD)
     by (rule hfref_imp)
 
   definition "comp_PRE R P Q S \<equiv> \<lambda>x. S x \<longrightarrow> (P x \<and> (\<forall>y. (y,x)\<in>R \<longrightarrow> Q x y))"
 
   lemma comp_PRE_cong[cong]: 
     assumes "R\<equiv>R'"
     assumes "\<And>x. P x \<equiv> P' x"
     assumes "\<And>x. S x \<equiv> S' x"
     assumes "\<And>x y. \<lbrakk>P x; (y,x)\<in>R; y\<in>Domain R; S' x \<rbrakk> \<Longrightarrow> Q x y \<equiv> Q' x y"
     shows "comp_PRE R P Q S \<equiv> comp_PRE R' P' Q' S'"
     using assms
     by (fastforce simp: comp_PRE_def intro!: eq_reflection ext)
 
   lemma fref_compI_PRE:
     "\<lbrakk> (f,g)\<in>fref P R1 R2; (g,h)\<in>fref Q S1 S2 \<rbrakk> 
       \<Longrightarrow> (f,h) \<in> fref (comp_PRE S1 Q (\<lambda>_. P) (\<lambda>_. True)) (R1 O S1) (R2 O S2)"
     using fref_compI[of P R1 R2 Q S1 S2]   
     unfolding comp_PRE_def
     by auto
 
   lemma PRE_D1: "(Q x \<and> P x) \<longrightarrow> comp_PRE S1 Q (\<lambda>x _. P x) S x"
     by (auto simp: comp_PRE_def)
 
   lemma PRE_D2: "(Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> S x \<longrightarrow> P x y)) \<longrightarrow> comp_PRE S1 Q P S x"
     by (auto simp: comp_PRE_def)
 
   lemma fref_weaken_pre: 
     assumes "\<And>x. P x \<longrightarrow> P' x"  
     assumes "(f,h) \<in> fref P' R S"
     shows "(f,h) \<in> fref P R S"
     apply (rule rev_subsetD[OF assms(2) fref_mono])
     using assms(1) by auto
     
   lemma fref_PRE_D1:
     assumes "(f,h) \<in> fref (comp_PRE S1 Q (\<lambda>x _. P x) X) R S"  
     shows "(f,h) \<in> fref (\<lambda>x. Q x \<and> P x) R S"
     by (rule fref_weaken_pre[OF PRE_D1 assms])
 
   lemma fref_PRE_D2:
     assumes "(f,h) \<in> fref (comp_PRE S1 Q P X) R S"  
     shows "(f,h) \<in> fref (\<lambda>x. Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> X x \<longrightarrow> P x y)) R S"
     by (rule fref_weaken_pre[OF PRE_D2 assms])
 
   lemmas fref_PRE_D = fref_PRE_D1 fref_PRE_D2
 
   lemma hfref_weaken_pre: 
     assumes "\<And>x. P x \<longrightarrow> P' x"  
     assumes "(f,h) \<in> hfref P' R S"
     shows "(f,h) \<in> hfref P R S"
     using assms
     by (auto simp: hfref_def)
 
   lemma hfref_weaken_pre': 
     assumes "\<And>x. \<lbrakk>P x; rdomp (fst R) x\<rbrakk> \<Longrightarrow> P' x"  
     assumes "(f,h) \<in> hfref P' R S"
     shows "(f,h) \<in> hfref P R S"
     apply (rule hfrefI)
     apply (rule hn_refine_preI)
     using assms
     by (auto simp: hfref_def rdomp_def)
 
   lemma hfref_weaken_pre_nofail': 
     assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"  
     assumes "\<And>x. \<lbrakk>nofail (g x); Q x\<rbrakk> \<Longrightarrow> P x"
     shows "(f,g) \<in> [Q]\<^sub>a R \<rightarrow> S"
     apply (rule hfref_weaken_pre[OF _ assms(1)[THEN hfref_weaken_pre_nofail]])
     using assms(2) 
     by blast
 
   lemma hfref_compI_PRE_aux:
     assumes A: "(f,g) \<in> [P]\<^sub>a RR' \<rightarrow> S"
     assumes B: "(g,h) \<in> [Q]\<^sub>f T \<rightarrow> \<langle>U\<rangle>nres_rel"
     shows "(f,h) \<in> [comp_PRE T Q (\<lambda>_. P) (\<lambda>_. True)]\<^sub>a 
       hrp_comp RR' T \<rightarrow> hr_comp S U"
     apply (rule hfref_weaken_pre[OF _ hfcomp[OF A B]])
     by (auto simp: comp_PRE_def)
 
 
   lemma hfref_compI_PRE:
     assumes A: "(f,g) \<in> [P]\<^sub>a RR' \<rightarrow> S"
     assumes B: "(g,h) \<in> [Q]\<^sub>f T \<rightarrow> \<langle>U\<rangle>nres_rel"
     shows "(f,h) \<in> [comp_PRE T Q (\<lambda>x y. P y) (\<lambda>x. nofail (h x))]\<^sub>a 
       hrp_comp RR' T \<rightarrow> hr_comp S U"
     using hfref_compI_PRE_aux[OF A B, THEN hfref_weaken_pre_nofail]  
     apply (rule hfref_weaken_pre[rotated])
     apply (auto simp: comp_PRE_def)
     done
 
   lemma hfref_PRE_D1:
     assumes "(f,h) \<in> hfref (comp_PRE S1 Q (\<lambda>x _. P x) X) R S"  
     shows "(f,h) \<in> hfref (\<lambda>x. Q x \<and> P x) R S"
     by (rule hfref_weaken_pre[OF PRE_D1 assms])
 
   lemma hfref_PRE_D2:
     assumes "(f,h) \<in> hfref (comp_PRE S1 Q P X) R S"  
     shows "(f,h) \<in> hfref (\<lambda>x. Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> X x \<longrightarrow> P x y)) R S"
     by (rule hfref_weaken_pre[OF PRE_D2 assms])
 
   lemma hfref_PRE_D3:
     assumes "(f,h) \<in> hfref (comp_PRE S1 Q P X) R S"  
     shows "(f,h) \<in> hfref (comp_PRE S1 Q P X) R S"
     using assms .
 
   lemmas hfref_PRE_D = hfref_PRE_D1 hfref_PRE_D3
 
   subsection \<open>Automation\<close>  
   text \<open>Purity configuration for constraint solver\<close>
   lemmas [safe_constraint_rules] = pure_pure
 
   text \<open>Configuration for hfref to hnr conversion\<close>
   named_theorems to_hnr_post \<open>to_hnr converter: Postprocessing unfold rules\<close>
 
   lemma uncurry0_add_app_tag: "uncurry0 (RETURN c) = uncurry0 (RETURN$c)" by simp
 
   lemmas [to_hnr_post] = norm_RETURN_o norm_return_o
     uncurry0_add_app_tag uncurry0_apply uncurry0_APP hn_val_unit_conv_emp
     mult_1[of "x::assn" for x] mult_1_right[of "x::assn" for x]
 
   named_theorems to_hfref_post \<open>to_hfref converter: Postprocessing unfold rules\<close> 
   lemma prod_casesK[to_hfref_post]: "case_prod (\<lambda>_ _. k) = (\<lambda>_. k)" by auto
   lemma uncurry0_hfref_post[to_hfref_post]: "hfref (uncurry0 True) R S = hfref (\<lambda>_. True) R S" 
     apply (fo_rule arg_cong fun_cong)+ by auto
 
 
   (* Currently not used, we keep it in here anyway. *)  
   text \<open>Configuration for relation normalization after composition\<close>
   named_theorems fcomp_norm_unfold \<open>fcomp-normalizer: Unfold theorems\<close>
   named_theorems fcomp_norm_simps \<open>fcomp-normalizer: Simplification theorems\<close>
   named_theorems fcomp_norm_init "fcomp-normalizer: Initialization rules"  
   named_theorems fcomp_norm_trans "fcomp-normalizer: Transitivity rules"  
   named_theorems fcomp_norm_cong "fcomp-normalizer: Congruence rules"  
   named_theorems fcomp_norm_norm "fcomp-normalizer: Normalization rules"  
   named_theorems fcomp_norm_refl "fcomp-normalizer: Reflexivity rules"  
 
   text \<open>Default Setup\<close>
   lemmas [fcomp_norm_unfold] = prod_rel_comp nres_rel_comp Id_O_R R_O_Id
   lemmas [fcomp_norm_unfold] = hr_comp_Id1 hr_comp_Id2
   lemmas [fcomp_norm_unfold] = hr_comp_prod_conv
   lemmas [fcomp_norm_unfold] = prod_hrp_comp hrp_comp_keep hrp_comp_dest hr_comp_pure
   (*lemmas [fcomp_norm_unfold] = prod_casesK uncurry0_hfref_post*)
 
   lemma [fcomp_norm_simps]: "CONSTRAINT is_pure P \<Longrightarrow> pure (the_pure P) = P" by simp
   lemmas [fcomp_norm_simps] = True_implies_equals 
 
   lemmas [fcomp_norm_init] = fcomp_norm_dflt_init
   lemmas [fcomp_norm_trans] = hrp_imp_trans
   lemmas [fcomp_norm_cong] = hrp_comp_cong hrp_prod_cong
   (*lemmas [fcomp_norm_norm] = hrp_comp_dest*)
   lemmas [fcomp_norm_refl] = refl hrp_imp_refl
 
   lemma ensure_fref_nresI: "(f,g)\<in>[P]\<^sub>f R\<rightarrow>S \<Longrightarrow> (RETURN o f, RETURN o g)\<in>[P]\<^sub>f R\<rightarrow>\<langle>S\<rangle>nres_rel" 
     by (auto intro: nres_relI simp: fref_def)
 
   lemma ensure_fref_nres_unfold:
     "\<And>f. RETURN o (uncurry0 f) = uncurry0 (RETURN f)" 
     "\<And>f. RETURN o (uncurry f) = uncurry (RETURN oo f)"
     "\<And>f. (RETURN ooo uncurry) f = uncurry (RETURN ooo f)"
     by auto
 
   text \<open>Composed precondition normalizer\<close>  
   named_theorems fcomp_prenorm_simps \<open>fcomp precondition-normalizer: Simplification theorems\<close>
 
   text \<open>Support for preconditions of the form \<open>_\<in>Domain R\<close>, 
     where \<open>R\<close> is the relation of the next more abstract level.\<close>
   declare DomainI[fcomp_prenorm_simps]
 
   lemma auto_weaken_pre_init_hf: 
     assumes "\<And>x. PROTECT P x \<longrightarrow> P' x"  
     assumes "(f,h) \<in> hfref P' R S"
     shows "(f,h) \<in> hfref P R S"
     using assms
     by (auto simp: hfref_def)
 
   lemma auto_weaken_pre_init_f: 
     assumes "\<And>x. PROTECT P x \<longrightarrow> P' x"  
     assumes "(f,h) \<in> fref P' R S"
     shows "(f,h) \<in> fref P R S"
     using assms
     by (auto simp: fref_def)
 
   lemmas auto_weaken_pre_init = auto_weaken_pre_init_hf auto_weaken_pre_init_f  
 
   lemma auto_weaken_pre_uncurry_step:
     assumes "PROTECT f a \<equiv> f'"
     shows "PROTECT (\<lambda>(x,y). f x y) (a,b) \<equiv> f' b" 
     using assms
     by (auto simp: curry_def dest!: meta_eq_to_obj_eq intro!: eq_reflection)
 
   lemma auto_weaken_pre_uncurry_finish:  
     "PROTECT f x \<equiv> f x" by (auto)
 
   lemma auto_weaken_pre_uncurry_start:
     assumes "P \<equiv> P'"
     assumes "P'\<longrightarrow>Q"
     shows "P\<longrightarrow>Q"
     using assms by (auto)
 
   lemma auto_weaken_pre_comp_PRE_I:
     assumes "S x \<Longrightarrow> P x"
     assumes "\<And>y. \<lbrakk>(y,x)\<in>R; P x; S x\<rbrakk> \<Longrightarrow> Q x y"
     shows "comp_PRE R P Q S x"
     using assms by (auto simp: comp_PRE_def)
 
   lemma auto_weaken_pre_to_imp_nf:
     "(A\<longrightarrow>B\<longrightarrow>C) = (A\<and>B \<longrightarrow> C)"
     "((A\<and>B)\<and>C) = (A\<and>B\<and>C)"
     by auto
 
   lemma auto_weaken_pre_add_dummy_imp:
     "P \<Longrightarrow> True \<longrightarrow> P" by simp
 
 
   text \<open>Synthesis for hfref statements\<close>  
   definition hfsynth_ID_R :: "('a \<Rightarrow> _ \<Rightarrow> assn) \<Rightarrow> 'a \<Rightarrow> bool" where
     [simp]: "hfsynth_ID_R _ _ \<equiv> True"
 
   lemma hfsynth_ID_R_D:
     fixes I :: "'a itself"
     assumes "hfsynth_ID_R R a"
     assumes "intf_of_assn R I"
     shows "a ::\<^sub>i I"
     by simp
 
   lemma hfsynth_hnr_from_hfI:
     assumes "\<forall>x xi. P x \<and> hfsynth_ID_R (fst R) x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)"
     shows "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
     using assms
     unfolding hfref_def 
     by (auto simp: hn_ctxt_def)
 
 
   lemma hfsynth_ID_R_uncurry_unfold: 
     "hfsynth_ID_R (to_hnr_prod R S) (a,b) \<equiv> hfsynth_ID_R R a \<and> hfsynth_ID_R S b" 
     "hfsynth_ID_R (fst (hf_pres R k)) \<equiv> hfsynth_ID_R R"
     by (auto intro!: eq_reflection)
 
   ML \<open>
 
     signature SEPREF_RULES = sig
       (* Analysis of relations, both fref and fun_rel *)
       (* "R1\<rightarrow>...\<rightarrow>Rn\<rightarrow>_" / "[_]\<^sub>f ((R1\<times>\<^sub>rR2)...\<times>\<^sub>rRn)"  \<mapsto>  "[R1,...,Rn]" *)
       val binder_rels: term -> term list 
       (* "_\<rightarrow>...\<rightarrow>_\<rightarrow>S" / "[_]\<^sub>f _ \<rightarrow> S"  \<mapsto>  "S" *)
       val body_rel: term -> term 
       (* Map \<rightarrow>/fref to (precond,args,res). NONE if no/trivial precond. *)
       val analyze_rel: term -> term option * term list * term 
       (* Make trivial ("\<lambda>_. True") precond *)
       val mk_triv_precond: term list -> term 
       (* Make "[P]\<^sub>f ((R1\<times>\<^sub>rR2)...\<times>\<^sub>rRn) \<rightarrow> S". Insert trivial precond if NONE. *)
       val mk_rel: term option * term list * term -> term 
       (* Map relation to (args,res) *)
       val strip_rel: term -> term list * term 
 
       (* Make hfprod (op *\<^sub>a) *)
       val mk_hfprod : term * term -> term
       val mk_hfprods : term list -> term
 
       (* Determine interface type of refinement assertion, using default fallback
         if necessary. Use named_thms intf_of_assn for configuration. *)
       val intf_of_assn : Proof.context -> term -> typ
 
       (*
         Convert a parametricity theorem in higher-order form to
         uncurried fref-form. For functions without arguments, 
         a unit-argument is added.
 
         TODO/FIXME: Currently this only works for higher-order theorems,
           i.e., theorems of the form (f,g)\<in>R1\<rightarrow>\<dots>\<rightarrow>Rn. 
           
           First-order theorems are silently treated as refinement theorems
           for functions with zero arguments, i.e., a unit-argument is added.
       *)
       val to_fref : Proof.context -> thm -> thm
 
       (* Convert a parametricity or fref theorem to first order form *)
       val to_foparam : Proof.context -> thm -> thm
 
       (* Convert schematic hfref goal to hnr-goal *)
       val prepare_hfref_synth_tac : Proof.context -> tactic'
 
       (* Convert theorem in hfref-form to hnr-form *)
       val to_hnr : Proof.context -> thm -> thm
 
       (* Convert theorem in hnr-form to hfref-form *)
       val to_hfref: Proof.context -> thm -> thm
 
       (* Convert theorem to given form, if not yet in this form *)
       val ensure_fref : Proof.context -> thm -> thm
       val ensure_fref_nres : Proof.context -> thm -> thm
       val ensure_hfref : Proof.context -> thm -> thm
       val ensure_hnr : Proof.context -> thm -> thm
 
 
       type hnr_analysis = {
         thm: thm,                     (* Original theorem, may be normalized *)
         precond: term,                (* Precondition, abstracted over abs-arguments *)
         prems : term list,            (* Premises not depending on arguments *)
         ahead: term * bool,           (* Abstract function, has leading RETURN *)
         chead: term * bool,           (* Concrete function, has leading return *)
         argrels: (term * bool) list,  (* Argument relations, preserved (keep-flag) *)
         result_rel: term              (* Result relation *)
       }
   
       val analyze_hnr: Proof.context -> thm -> hnr_analysis
       val pretty_hnr_analysis: Proof.context -> hnr_analysis -> Pretty.T
       val mk_hfref_thm: Proof.context -> hnr_analysis -> thm
   
   
 
       (* Simplify precondition of fref/hfref-theorem *)
       val simplify_precond: Proof.context -> thm -> thm
 
       (* Normalize hfref-theorem after composition *)
       val norm_fcomp_rule: Proof.context -> thm -> thm
 
       (* Replace "pure ?A" by "?A'" and is_pure constraint, then normalize *)
       val add_pure_constraints_rule: Proof.context -> thm -> thm
 
       (* Compose fref/hfref and fref theorem, to produce hfref theorem.
         The input theorems may also be in ho-param or hnr form, and
         are converted accordingly.
       *)
       val gen_compose : Proof.context -> thm -> thm -> thm
 
       (* FCOMP-attribute *)
       val fcomp_attrib: attribute context_parser
     end
 
     structure Sepref_Rules: SEPREF_RULES = struct
 
       local open Refine_Util Relators in
         fun binder_rels @{mpat "?F \<rightarrow> ?G"} = F::binder_rels G
           | binder_rels @{mpat "fref _ ?F _"} = strip_prodrel_left F
           | binder_rels _ = []
     
         local 
           fun br_aux @{mpat "_ \<rightarrow> ?G"} = br_aux G
             | br_aux R = R
         in    
           fun body_rel @{mpat "fref _ _ ?G"} = G
             | body_rel R = br_aux R
         end
     
         fun strip_rel R = (binder_rels R, body_rel R)   
     
         fun analyze_rel @{mpat "fref (\<lambda>_. True) ?R ?S"} = (NONE,strip_prodrel_left R,S)
           | analyze_rel @{mpat "fref ?P ?R ?S"} = (SOME P,strip_prodrel_left R,S)
           | analyze_rel R = let
               val (args,res) = strip_rel R
             in
               (NONE,args,res)
             end
     
         fun mk_triv_precond Rs = absdummy (map rel_absT Rs |> list_prodT_left) @{term True}
     
         fun mk_rel (P,Rs,S) = let 
           val R = list_prodrel_left Rs 
     
           val P = case P of 
               SOME P => P 
             | NONE => mk_triv_precond Rs
     
         in 
           @{mk_term "fref ?P ?R ?S"} 
         end
       end
 
 
       fun mk_hfprod (a, b) = @{mk_term "?a*\<^sub>a?b"}
   
       local 
         fun mk_hfprods_rev [] = @{mk_term "unit_assn\<^sup>k"}
           | mk_hfprods_rev [Rk] = Rk
           | mk_hfprods_rev (Rkn::Rks) = mk_hfprod (mk_hfprods_rev Rks, Rkn)
       in
         val mk_hfprods = mk_hfprods_rev o rev
       end
 
 
       fun intf_of_assn ctxt t = let
         val orig_ctxt = ctxt
         val (t,ctxt) = yield_singleton (Variable.import_terms false) t ctxt
 
         val v = TVar (("T",0),Proof_Context.default_sort ctxt ("T",0)) |> Logic.mk_type
         val goal = @{mk_term "Trueprop (intf_of_assn ?t ?v)"}
 
         val i_of_assn_rls = 
           Named_Theorems_Rev.get ctxt @{named_theorems_rev intf_of_assn}
           @ @{thms intf_of_assn_fallback}
 
         fun tac ctxt = REPEAT_ALL_NEW (resolve_tac ctxt i_of_assn_rls)
 
         val thm = Goal.prove ctxt [] [] goal (fn {context,...} => ALLGOALS (tac context))
         val intf = case Thm.concl_of thm of
             @{mpat "Trueprop (intf_of_assn _ (?v AS\<^sub>p TYPE (_)))"} => v 
           | _ => raise THM("Intf_of_assn: Proved a different theorem?",~1,[thm])
 
         val intf = singleton (Variable.export_terms ctxt orig_ctxt) intf
           |> Logic.dest_type
 
       in
         intf
       end
 
       datatype rthm_type = 
         RT_HOPARAM    (* (_,_) \<in> _ \<rightarrow> \<dots> \<rightarrow> _ *)
       | RT_FREF       (* (_,_) \<in> [_]\<^sub>f _ \<rightarrow> _ *)
       | RT_HNR        (* hn_refine _ _ _ _ _ *)
       | RT_HFREF      (* (_,_) \<in> [_]\<^sub>a _ \<rightarrow> _ *)
       | RT_OTHER
 
       fun rthm_type thm =
         case Thm.concl_of thm |> HOLogic.dest_Trueprop of
           @{mpat "(_,_) \<in> fref _ _ _"} => RT_FREF
         | @{mpat "(_,_) \<in> hfref _ _ _"} => RT_HFREF
         | @{mpat "hn_refine _ _ _ _ _"} => RT_HNR
         | @{mpat "(_,_) \<in> _"} => RT_HOPARAM (* TODO: Distinction between ho-param and fo-param *)
         | _ => RT_OTHER
 
 
       fun to_fref ctxt thm = let
         open Conv
       in  
         case Thm.concl_of thm |> HOLogic.dest_Trueprop of
           @{mpat "(_,_)\<in>_\<rightarrow>_"} =>
             Local_Defs.unfold0 ctxt @{thms fref_param1} thm
             |> fconv_rule (repeat_conv (Refine_Util.ftop_conv (K (rewr_conv @{thm fref_nest})) ctxt))
             |> Local_Defs.unfold0 ctxt @{thms in_CURRY_conv}
         | @{mpat "(_,_)\<in>_"} => thm RS @{thm fref_param0I}   
         | _ => raise THM ("to_fref: Expected theorem of form (_,_)\<in>_",~1,[thm])
       end
 
       fun to_foparam ctxt thm = let
         val unf_thms = @{thms 
           split_tupled_all prod_rel_simp uncurry_apply cnv_conj_to_meta Product_Type.split}
       in
         case Thm.concl_of thm of
           @{mpat "Trueprop ((_,_) \<in> fref _ _ _)"} =>
             (@{thm frefD} OF [thm])
             |> forall_intr_vars
             |> Local_Defs.unfold0 ctxt unf_thms
             |> Variable.gen_all ctxt
         | @{mpat "Trueprop ((_,_) \<in> _)"} =>
             Parametricity.fo_rule thm
         | _ => raise THM("Expected parametricity or fref theorem",~1,[thm])
       end
 
       fun to_hnr ctxt thm =
         (thm RS @{thm hf2hnr})
         |> Local_Defs.unfold0 ctxt @{thms to_hnr_prod_fst_snd keep_drop_sels} (* Resolve fst and snd over *\<^sub>a and R\<^sup>k, R\<^sup>d *)
         |> Local_Defs.unfold0 ctxt @{thms hnr_uncurry_unfold} (* Resolve products for uncurried parameters *)
         |> Local_Defs.unfold0 ctxt @{thms uncurry_apply uncurry_APP assn_one_left split} (* Remove the uncurry modifiers, the emp-dummy, and unfold product cases *)
         |> Local_Defs.unfold0 ctxt @{thms hn_ctxt_ctxt_fix_conv} (* Remove duplicate hn_ctxt tagging *)
         |> Local_Defs.unfold0 ctxt @{thms all_to_meta imp_to_meta HOL.True_implies_equals HOL.implies_True_equals Pure.triv_forall_equality cnv_conj_to_meta} (* Convert to meta-level, remove vacuous condition *)
         |> Local_Defs.unfold0 ctxt (Named_Theorems.get ctxt @{named_theorems to_hnr_post}) (* Post-Processing *)
         |> Goal.norm_result ctxt
         |> Conv.fconv_rule Thm.eta_conversion
 
       (* Convert schematic hfref-goal to hn_refine goal *)  
       fun prepare_hfref_synth_tac ctxt = let
         val i_of_assn_rls = 
           Named_Theorems_Rev.get ctxt @{named_theorems_rev intf_of_assn}
           @ @{thms intf_of_assn_fallback}
 
         val to_hnr_post_rls = 
           Named_Theorems.get ctxt @{named_theorems to_hnr_post}
 
         val i_of_assn_tac = (
           REPEAT' (
             DETERM o dresolve_tac ctxt @{thms hfsynth_ID_R_D}
             THEN' DETERM o SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt i_of_assn_rls))
           )
         )
       in
         (* Note: To re-use the to_hnr infrastructure, we first work with
           $-tags on the abstract function, which are finally removed.
         *)
         resolve_tac ctxt @{thms hfsynth_hnr_from_hfI} THEN_ELSE' (
           SELECT_GOAL (
             unfold_tac ctxt @{thms to_hnr_prod_fst_snd keep_drop_sels hf_pres_fst} (* Distribute fst,snd over product and hf_pres *)
             THEN unfold_tac ctxt @{thms hnr_uncurry_unfold hfsynth_ID_R_uncurry_unfold} (* Curry parameters *)
             THEN unfold_tac ctxt @{thms uncurry_apply uncurry_APP assn_one_left split} (* Curry parameters (II) and remove emp assertion *)
             (*THEN unfold_tac ctxt @{thms hn_ctxt_ctxt_fix_conv} (* Remove duplicate hn_ctxt (Should not be necessary) *)*)
             THEN unfold_tac ctxt @{thms all_to_meta imp_to_meta HOL.True_implies_equals HOL.implies_True_equals Pure.triv_forall_equality cnv_conj_to_meta} (* Convert precondition to meta-level *)
             THEN ALLGOALS i_of_assn_tac (* Generate _::\<^sub>i_ premises*)
             THEN unfold_tac ctxt to_hnr_post_rls (* Postprocessing *)
             THEN unfold_tac ctxt @{thms APP_def} (* Get rid of $ - tags *)
           )
         ,
           K all_tac
         )
       end
 
 
       (************************************)  
       (* Analyze hnr *)
       structure Termtab2 = Table(
         type key = term * term 
         val ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord);
   
       type hnr_analysis = {
         thm: thm,                     
         precond: term,                
         prems : term list,
         ahead: term * bool,           
         chead: term * bool,           
         argrels: (term * bool) list,  
         result_rel: term              
       }
   
     
       fun analyze_hnr (ctxt:Proof.context) thm = let
     
         (* Debug information: Stores string*term pairs, which are pretty-printed on error *)
         val dbg = Unsynchronized.ref []
         fun add_dbg msg ts = (
           dbg := (msg,ts) :: !dbg;
           ()
         )
         fun pretty_dbg (msg,ts) = Pretty.block [
           Pretty.str msg,
           Pretty.str ":",
           Pretty.brk 1,
           Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) ts)
         ]
         fun pretty_dbgs l = map pretty_dbg l |> Pretty.fbreaks |> Pretty.block
     
         fun trace_dbg msg = Pretty.block [Pretty.str msg, Pretty.fbrk, pretty_dbgs (rev (!dbg))] |> Pretty.string_of |> tracing
     
         fun fail msg = (trace_dbg msg; raise THM(msg,~1,[thm])) 
         fun assert cond msg = cond orelse fail msg;
     
     
         (* Heads may have a leading return/RETURN.
           The following code strips off the leading return, unless it has the form
           "return x" for an argument x
         *)
         fun check_strip_leading args t f = (* Handle the case RETURN x, where x is an argument *)
           if Termtab.defined args f then (t,false) else (f,true)
     
         fun strip_leading_RETURN args (t as @{mpat "RETURN$(?f)"}) = check_strip_leading args t f
           | strip_leading_RETURN args (t as @{mpat "RETURN ?f"}) = check_strip_leading args t f
           | strip_leading_RETURN _ t = (t,false)
     
         fun strip_leading_return args (t as @{mpat "return$(?f)"}) = check_strip_leading args t f
             | strip_leading_return args (t as @{mpat "return ?f"}) = check_strip_leading args t f
             | strip_leading_return _ t = (t,false)
     
     
         (* The following code strips the arguments of the concrete or abstract
           function. It knows how to handle APP-tags ($), and stops at PR_CONST-tags.
     
           Moreover, it only strips actual arguments that occur in the 
           precondition-section of the hn_refine-statement. This ensures
           that non-arguments, like maxsize, are treated correctly.
         *)    
         fun strip_fun _ (t as @{mpat "PR_CONST _"}) = (t,[])
           | strip_fun s (t as @{mpat "?f$?x"}) = check_arg s t f x
           | strip_fun s (t as @{mpat "?f ?x"}) = check_arg s t f x
           | strip_fun _ f = (f,[])
         and check_arg s t f x = 
             if Termtab.defined s x then
               strip_fun s f |> apsnd (curry op :: x)
             else (t,[])  
     
         (* Arguments in the pre/postcondition are wrapped into hn_ctxt tags. 
           This function strips them off. *)    
         fun dest_hn_ctxt @{mpat "hn_ctxt ?R ?a ?c"} = ((a,c),R)
           | dest_hn_ctxt _ = fail "Invalid hn_ctxt parameter in pre or postcondition"
     
     
         fun dest_hn_refine @{mpat "(hn_refine ?G ?c ?G' ?R ?a)"} = (G,c,G',R,a) 
           | dest_hn_refine _ = fail "Conclusion is not a hn_refine statement"
     
         (*
           Strip separation conjunctions. Special case for "emp", which is ignored. 
         *)  
         fun is_emp @{mpat emp} = true | is_emp _ = false
   
         val strip_star' = Sepref_Basic.strip_star #> filter (not o is_emp)
   
         (* Compare Termtab2s for equality of keys *)  
         fun pairs_eq pairs1 pairs2 = 
                   Termtab2.forall (Termtab2.defined pairs1 o fst) pairs2
           andalso Termtab2.forall (Termtab2.defined pairs2 o fst) pairs1
     
     
         fun atomize_prem @{mpat "Trueprop ?p"} = p
           | atomize_prem _ = fail "Non-atomic premises"
     
         (* Make HOL conjunction list *)  
         fun mk_conjs [] = @{const True}
           | mk_conjs [p] = p
           | mk_conjs (p::ps) = HOLogic.mk_binop @{const_name "HOL.conj"} (p,mk_conjs ps)
     
     
         (***********************)      
         (* Start actual analysis *)
     
         val _ = add_dbg "thm" [Thm.prop_of thm]
         val prems = Thm.prems_of thm
         val concl = Thm.concl_of thm |> HOLogic.dest_Trueprop
         val (G,c,G',R,a) = dest_hn_refine concl
     
         val pre_pairs = G 
           |> strip_star'
           |> tap (add_dbg "precondition")
           |> map dest_hn_ctxt
           |> Termtab2.make
     
         val post_pairs = G' 
           |> strip_star'
           |> tap (add_dbg "postcondition")
           |> map dest_hn_ctxt
           |> Termtab2.make
     
         val _ = assert (pairs_eq pre_pairs post_pairs) 
           "Parameters in precondition do not match postcondition"
     
         val aa_set = pre_pairs |> Termtab2.keys |> map fst |> Termtab.make_set
         val ca_set = pre_pairs |> Termtab2.keys |> map snd |> Termtab.make_set
     
         val (a,leading_RETURN) = strip_leading_RETURN aa_set a
         val (c,leading_return) = strip_leading_return ca_set c
     
         val _ = add_dbg "stripped abstract term" [a]
         val _ = add_dbg "stripped concrete term" [c]
     
         val (ahead,aargs) = strip_fun aa_set a;
         val (chead,cargs) = strip_fun ca_set c;
     
         val _ = add_dbg "abstract head" [ahead]
         val _ = add_dbg "abstract args" aargs
         val _ = add_dbg "concrete head" [chead]
         val _ = add_dbg "concrete args" cargs
     
     
         val _ = assert (length cargs = length aargs) "Different number of abstract and concrete arguments";
     
         val _ = assert (not (has_duplicates op aconv aargs)) "Duplicate abstract arguments"
         val _ = assert (not (has_duplicates op aconv cargs)) "Duplicate concrete arguments"
     
         val argpairs = aargs ~~ cargs
         val ap_set = Termtab2.make_set argpairs
         val _ = assert (pairs_eq pre_pairs ap_set) "Arguments from pre/postcondition do not match operation's arguments"
     
         val pre_rels = map (the o (Termtab2.lookup pre_pairs)) argpairs
         val post_rels = map (the o (Termtab2.lookup post_pairs)) argpairs
     
         val _ = add_dbg "pre-rels" pre_rels
         val _ = add_dbg "post-rels" post_rels
 
         fun adjust_hf_pres @{mpat "snd (?R\<^sup>k)"} = R
           | adjust_hf_pres t = t
           
         val post_rels = map adjust_hf_pres post_rels
     
         fun is_invalid R @{mpat "invalid_assn ?R'"} = R aconv R'
           | is_invalid _ @{mpat "snd (_\<^sup>d)"} = true
           | is_invalid _ _ = false
     
         fun is_keep (R,R') =
           if R aconv R' then true
           else if is_invalid R R' then false
           else fail "Mismatch between pre and post relation for argument"
     
         val keep = map is_keep (pre_rels ~~ post_rels)
     
         val argrels = pre_rels ~~ keep
 
         val aa_set = Termtab.make_set aargs
         val ca_set = Termtab.make_set cargs
 
         fun is_precond t =
           (exists_subterm (Termtab.defined ca_set) t andalso fail "Premise contains concrete argument")
           orelse exists_subterm (Termtab.defined aa_set) t
 
         val (preconds, prems) = split is_precond prems  
     
         val precond = 
           map atomize_prem preconds 
           |> mk_conjs
           |> fold lambda aargs
     
         val _ = add_dbg "precond" [precond]
         val _ = add_dbg "prems" prems
     
       in
         {
           thm = thm,
           precond = precond,
           prems = prems,
           ahead = (ahead,leading_RETURN),
           chead = (chead,leading_return),
           argrels = argrels,
           result_rel = R
         }
       end  
     
       fun pretty_hnr_analysis 
         ctxt 
         ({thm,precond,ahead,chead,argrels,result_rel,...}) 
         : Pretty.T =
       let  
         val _ = thm (* Suppress unused warning for thm *)
 
         fun pretty_argrel (R,k) = Pretty.block [
           Syntax.pretty_term ctxt R,
           if k then Pretty.str "\<^sup>k" else Pretty.str "\<^sup>d"
         ]
     
         val pretty_chead = case chead of 
           (t,false) => Syntax.pretty_term ctxt t 
         | (t,true) => Pretty.block [Pretty.str "return ", Syntax.pretty_term ctxt t]
 
         val pretty_ahead = case ahead of 
           (t,false) => Syntax.pretty_term ctxt t 
         | (t,true) => Pretty.block [Pretty.str "RETURN ", Syntax.pretty_term ctxt t]
 
       in
         Pretty.fbreaks [
           (*Display.pretty_thm ctxt thm,*)
           Pretty.block [ 
             Pretty.enclose "[" "]" [pretty_chead, pretty_ahead],
             Pretty.enclose "[" "]" [Syntax.pretty_term ctxt precond],
             Pretty.brk 1,
             Pretty.block (Pretty.separate " \<rightarrow>" (map pretty_argrel argrels @ [Syntax.pretty_term ctxt result_rel]))
           ]
         ] |> Pretty.block
     
       end
     
     
       fun mk_hfref_thm 
         ctxt 
         ({thm,precond,prems,ahead,chead,argrels,result_rel}) = 
       let
     
         fun mk_keep (R,true) = @{mk_term "?R\<^sup>k"}
           | mk_keep (R,false) = @{mk_term "?R\<^sup>d"}
     
         (* TODO: Move, this is of general use! *)  
         fun mk_uncurry f = @{mk_term "uncurry ?f"}  
       
         (* Uncurry function for the given number of arguments. 
           For zero arguments, add a unit-parameter.
         *)
         fun rpt_uncurry n t =
           if n=0 then @{mk_term "uncurry0 ?t"}
           else if n=1 then t 
           else funpow (n-1) mk_uncurry t
       
         (* Rewrite uncurried lambda's to \<lambda>(_,_). _ form. Use top-down rewriting
           to correctly handle nesting to the left. 
     
           TODO: Combine with abstraction and  uncurry-procedure,
             and mark the deviation about uncurry as redundant 
             intermediate step to be eliminated.
         *)  
         fun rew_uncurry_lambda t = let
           val rr = map (Logic.dest_equals o Thm.prop_of) @{thms uncurry_def uncurry0_def}
           val thy = Proof_Context.theory_of ctxt
         in 
           Pattern.rewrite_term_top thy rr [] t 
         end  
     
         (* Shortcuts for simplification tactics *)
         fun gsimp_only ctxt sec = let
           val ss = put_simpset HOL_basic_ss ctxt |> sec
         in asm_full_simp_tac ss end
     
         fun simp_only ctxt thms = gsimp_only ctxt (fn ctxt => ctxt addsimps thms)
     
     
         (********************************)
         (* Build theorem statement *)
         (* \<lbrakk>prems\<rbrakk> \<Longrightarrow> (chead,ahead) \<in> [precond] rels \<rightarrow> R *)
     
         (* Uncurry precondition *)
         val num_args = length argrels
         val precond = precond
           |> rpt_uncurry num_args
           |> rew_uncurry_lambda (* Convert to nicer \<lambda>((...,_),_) - form*)
 
         (* Re-attach leading RETURN/return *)
         fun mk_RETURN (t,r) = if r then 
             let
               val T = funpow num_args range_type (fastype_of (fst ahead))
               val tRETURN = Const (@{const_name RETURN}, T --> Type(@{type_name nres},[T]))
             in
               Refine_Util.mk_compN num_args tRETURN t
             end  
           else t
     
         fun mk_return (t,r) = if r then 
             let
               val T = funpow num_args range_type (fastype_of (fst chead))
               val tRETURN = Const (@{const_name return}, T --> Type(@{type_name Heap},[T]))
             in
               Refine_Util.mk_compN num_args tRETURN t
             end  
           else t
           
         (* Hrmpf!: Gone for good from 2015\<rightarrow>2016. Inserting ctxt-based substitute here. *)  
         fun certify_inst ctxt (instT, inst) =
-         (map (apsnd (Thm.ctyp_of ctxt)) instT,
-          map (apsnd (Thm.cterm_of ctxt)) inst);
+         (map (apsnd (Thm.ctyp_of ctxt)) (Term_Subst.TVars.dest instT),
+          map (apsnd (Thm.cterm_of ctxt)) (Term_Subst.Vars.dest inst));
 
         (*  
         fun mk_RETURN (t,r) = if r then @{mk_term "RETURN o ?t"} else t
         fun mk_return (t,r) = if r then @{mk_term "return o ?t"} else t
         *)
     
         (* Uncurry abstract and concrete function, append leading return *)
         val ahead = ahead |> mk_RETURN |> rpt_uncurry num_args  
         val chead = chead |> mk_return |> rpt_uncurry num_args 
     
         (* Add keep-flags and summarize argument relations to product *)
         val argrel = map mk_keep argrels |> rev (* TODO: Why this rev? *) |> mk_hfprods
     
         (* Produce final result statement *)
         val result = @{mk_term "Trueprop ((?chead,?ahead) \<in> [?precond]\<^sub>a ?argrel \<rightarrow> ?result_rel)"}
         val result = Logic.list_implies (prems,result)
     
         (********************************)
         (* Prove theorem *)
     
         (* Create context and import result statement and original theorem *)
         val orig_ctxt = ctxt
         (*val thy = Proof_Context.theory_of ctxt*)
         val (insts, ctxt) = Variable.import_inst true [result] ctxt
         val insts' = certify_inst ctxt insts
         val result = Term_Subst.instantiate insts result
         val thm = Thm.instantiate insts' thm
     
         (* Unfold APP tags. This is required as some APP-tags have also been unfolded by analysis *)
         val thm = Local_Defs.unfold0 ctxt @{thms APP_def} thm
     
         (* Tactic to prove the theorem. 
           A first step uses hfrefI to get a hnr-goal.
           This is then normalized in several consecutive steps, which 
             get rid of uncurrying. Finally, the original theorem is used for resolution,
             where the pre- and postcondition, and result relation are connected with 
             a consequence rule, to handle unfolded hn_ctxt-tags, re-ordered relations,
             and introduced unit-parameters (TODO: 
               Mark artificially introduced unit-parameter specially, it may get confused 
               with intentional unit-parameter, e.g., functional empty_set ()!)
     
           *)
         fun tac ctxt = 
                 resolve_tac ctxt @{thms hfrefI}
           THEN' gsimp_only ctxt (fn c => c 
             addsimps @{thms uncurry_def hn_ctxt_def uncurry0_def
                             keep_drop_sels uc_hfprod_sel o_apply
                             APP_def}
             |> Splitter.add_split @{thm prod.split}
           ) 
     
           THEN' TRY o (
             REPEAT_ALL_NEW (match_tac ctxt @{thms allI impI})
             THEN' simp_only ctxt @{thms Product_Type.split prod.inject})
     
           THEN' TRY o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE})
           THEN' TRY o hyp_subst_tac ctxt
           THEN' simp_only ctxt @{thms triv_forall_equality}
           THEN' (
             resolve_tac ctxt @{thms hn_refine_cons[rotated]} 
             THEN' (resolve_tac ctxt [thm] THEN_ALL_NEW assume_tac ctxt))
           THEN_ALL_NEW simp_only ctxt 
             @{thms hn_ctxt_def entt_refl pure_unit_rel_eq_empty
               mult_ac mult_1 mult_1_right keep_drop_sels}  
     
         (* Prove theorem *)  
         val result = Thm.cterm_of ctxt result
         val rthm = Goal.prove_internal ctxt [] result (fn _ => ALLGOALS (tac ctxt))
     
         (* Export statement to original context *)
         val rthm = singleton (Variable.export ctxt orig_ctxt) rthm
     
         (* Post-processing *)
         val rthm = Local_Defs.unfold0 ctxt (Named_Theorems.get ctxt @{named_theorems to_hfref_post}) rthm
 
       in
         rthm
       end
   
       fun to_hfref ctxt = analyze_hnr ctxt #> mk_hfref_thm ctxt
 
 
 
 
       (***********************************)
       (* Composition *)
 
       local
         fun norm_set_of ctxt = {
           trans_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_trans},
           cong_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_cong},
           norm_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_norm},
           refl_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_refl}
         }
     
         fun init_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_init}
         fun unfold_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_unfold}
         fun simp_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_simps}
 
       in  
         fun norm_fcomp_rule ctxt = let
           open PO_Normalizer Refine_Util
           val norm1 = gen_norm_rule (init_rules_of ctxt) (norm_set_of ctxt) ctxt
           val norm2 = Local_Defs.unfold0 ctxt (unfold_rules_of ctxt)
           val norm3 = Conv.fconv_rule (
             Simplifier.asm_full_rewrite 
               (put_simpset HOL_basic_ss ctxt addsimps simp_rules_of ctxt))
     
           val norm = changed_rule (try_rule norm1 o try_rule norm2 o try_rule norm3)
         in
           repeat_rule norm
         end
       end  
 
       fun add_pure_constraints_rule ctxt thm = let
         val orig_ctxt = ctxt
     
         val t = Thm.prop_of thm
     
         fun 
           cnv (@{mpat (typs) "pure (mpaq_STRUCT (mpaq_Var ?x _) :: (?'v_c\<times>?'v_a) set)"}) = 
           let
             val T = a --> c --> @{typ assn}
             val t = Var (x,T)
             val t = @{mk_term "(the_pure ?t)"}
           in
             [(x,T,t)]
           end
         | cnv (t$u) = union op= (cnv t) (cnv u)
         | cnv (Abs (_,_,t)) = cnv t  
         | cnv _ = []
     
         val pvars = cnv t
     
         val _ = (pvars |> map #1 |> has_duplicates op=) 
           andalso raise TERM ("Duplicate indexname with different type",[t]) (* This should not happen *)
     
         val substs = map (fn (x,_,t) => (x,t)) pvars
     
         val t' = subst_Vars substs t  
     
         fun mk_asm (x,T,_) = let
           val t = Var (x,T)
           val t = @{mk_term "Trueprop (CONSTRAINT is_pure ?t)"}
         in
           t
         end
     
         val assms = map mk_asm pvars
     
         fun add_prems prems t = let
           val prems' = Logic.strip_imp_prems t
           val concl = Logic.strip_imp_concl t
         in
           Logic.list_implies (prems@prems', concl)
         end
     
         val t' = add_prems assms t'
     
         val (t',ctxt) = yield_singleton (Variable.import_terms true) t' ctxt
     
         val thm' = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt t') (fn _ => 
           ALLGOALS (resolve_tac ctxt [thm] THEN_ALL_NEW assume_tac ctxt))
     
         val thm' = norm_fcomp_rule ctxt thm'
 
         val thm' = singleton (Variable.export ctxt orig_ctxt) thm'
       in
         thm'
       end  
 
 
       val cfg_simp_precond = 
         Attrib.setup_config_bool @{binding fcomp_simp_precond} (K true)
 
       local
         fun mk_simp_thm ctxt t = let
           val st = t
             |> HOLogic.mk_Trueprop
             |> Thm.cterm_of ctxt
             |> Goal.init
       
           val ctxt = Context_Position.set_visible false ctxt  
           val ctxt = ctxt addsimps (
               refine_pw_simps.get ctxt 
             @ Named_Theorems.get ctxt @{named_theorems fcomp_prenorm_simps}
             @ @{thms split_tupled_all cnv_conj_to_meta}  
             )
           
           val trace_incomplete_transfer_tac =
             COND (Thm.prems_of #> exists (strip_all_body #> Logic.strip_imp_concl #> Term.is_open))
               (print_tac ctxt "Failed transfer from intermediate level:") all_tac
     
           val tac = 
             ALLGOALS (resolve_tac ctxt @{thms auto_weaken_pre_comp_PRE_I} )
             THEN ALLGOALS (Simplifier.asm_full_simp_tac ctxt)
             THEN trace_incomplete_transfer_tac
             THEN ALLGOALS (TRY o filter_prems_tac ctxt (K false))
             THEN Local_Defs.unfold0_tac ctxt [Drule.triv_forall_equality]
       
           val st' = tac st |> Seq.take 1 |> Seq.list_of
           val thm = case st' of [st'] => Goal.conclude st' | _ => raise THM("Simp_Precond: Simp-Tactic failed",~1,[st])
     
           (* Check generated premises for leftover intermediate stuff *)
           val _ = exists (Logic.is_all) (Thm.prems_of thm) 
             andalso raise THM("Simp_Precond: Transfer from intermediate level failed",~1,[thm])
     
           val thm = 
              thm
           (*|> map (Simplifier.asm_full_simplify ctxt)*)
           |> Conv.fconv_rule (Object_Logic.atomize ctxt)
           |> Local_Defs.unfold0 ctxt @{thms auto_weaken_pre_to_imp_nf}
     
           val thm = case Thm.concl_of thm of
             @{mpat "Trueprop (_ \<longrightarrow> _)"} => thm
           | @{mpat "Trueprop _"} => thm RS @{thm auto_weaken_pre_add_dummy_imp}  
           | _ => raise THM("Simp_Precond: Generated odd theorem, expected form 'P\<longrightarrow>Q'",~1,[thm])
     
     
         in
           thm
         end
       in  
         fun simplify_precond ctxt thm = let
           val orig_ctxt = ctxt
           val thm = Refine_Util.OF_fst @{thms auto_weaken_pre_init} [asm_rl,thm]
           val thm = 
             Local_Defs.unfold0 ctxt @{thms split_tupled_all} thm
             OF @{thms auto_weaken_pre_uncurry_start}
       
           fun rec_uncurry thm =
             case try (fn () => thm OF @{thms auto_weaken_pre_uncurry_step}) () of
               NONE => thm OF @{thms auto_weaken_pre_uncurry_finish}
             | SOME thm => rec_uncurry thm  
       
           val thm = rec_uncurry thm  
             |> Conv.fconv_rule Thm.eta_conversion
       
           val t = case Thm.prems_of thm of
             t::_ => t | _ => raise THM("Simp-Precond: Expected at least one premise",~1,[thm])
       
           val (t,ctxt) = yield_singleton (Variable.import_terms false) t ctxt
           val ((_,t),ctxt) = Variable.focus NONE t ctxt
           val t = case t of
             @{mpat "Trueprop (_ \<longrightarrow> ?t)"} => t | _ => raise TERM("Simp_Precond: Expected implication",[t])
       
           val simpthm = mk_simp_thm ctxt t  
             |> singleton (Variable.export ctxt orig_ctxt)
             
           val thm = thm OF [simpthm]  
           val thm = Local_Defs.unfold0 ctxt @{thms prod_casesK} thm
         in
           thm
         end
 
         fun simplify_precond_if_cfg ctxt =
           if Config.get ctxt cfg_simp_precond then
             simplify_precond ctxt
           else I
 
       end  
 
       (* fref O fref *)
       fun compose_ff ctxt A B = 
           (@{thm fref_compI_PRE} OF [A,B])
         |> norm_fcomp_rule ctxt
         |> simplify_precond_if_cfg ctxt
         |> Conv.fconv_rule Thm.eta_conversion
 
       (* hfref O fref *)
       fun compose_hf ctxt A B =
           (@{thm hfref_compI_PRE} OF [A,B])
         |> norm_fcomp_rule ctxt
         |> simplify_precond_if_cfg ctxt
         |> Conv.fconv_rule Thm.eta_conversion
         |> add_pure_constraints_rule ctxt
         |> Conv.fconv_rule Thm.eta_conversion
 
       fun ensure_fref ctxt thm = case rthm_type thm of
         RT_HOPARAM => to_fref ctxt thm
       | RT_FREF => thm
       | _ => raise THM("Expected parametricity or fref theorem",~1,[thm])
 
       fun ensure_fref_nres ctxt thm = let
         val thm = ensure_fref ctxt thm
       in
         case Thm.concl_of thm of
           @{mpat (typs) "Trueprop (_\<in>fref _ _ (_::(_ nres\<times>_)set))"} => thm
         | @{mpat "Trueprop ((_,_)\<in>fref _ _ _)"} => 
             (thm RS @{thm ensure_fref_nresI}) |> Local_Defs.unfold0 ctxt @{thms ensure_fref_nres_unfold}
         | _ => raise THM("Expected fref-theorem",~1,[thm])
       end
 
       fun ensure_hfref ctxt thm = case rthm_type thm of
         RT_HNR => to_hfref ctxt thm
       | RT_HFREF => thm
       | _ => raise THM("Expected hnr or hfref theorem",~1,[thm])
 
       fun ensure_hnr ctxt thm = case rthm_type thm of
         RT_HNR => thm
       | RT_HFREF => to_hnr ctxt thm
       | _ => raise THM("Expected hnr or hfref theorem",~1,[thm])
 
       fun gen_compose ctxt A B = let
         val rtA = rthm_type A
       in
         if rtA = RT_HOPARAM orelse rtA = RT_FREF then
           compose_ff ctxt (ensure_fref ctxt A) (ensure_fref ctxt B)
         else  
           compose_hf ctxt (ensure_hfref ctxt A) ((ensure_fref_nres ctxt B))
         
       end
 
       val parse_fcomp_flags = Refine_Util.parse_paren_lists 
         (Refine_Util.parse_bool_config "prenorm" cfg_simp_precond)
 
       val fcomp_attrib = parse_fcomp_flags |-- Attrib.thm >> (fn B => Thm.rule_attribute [] (fn context => fn A => 
       let
         val ctxt = Context.proof_of context
       in  
         gen_compose ctxt A B
       end))
 
     end
   \<close>
 
   attribute_setup to_fref = \<open>
     Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_fref o Context.proof_of))
 \<close> "Convert parametricity theorem to uncurried fref-form" 
 
   attribute_setup to_foparam = \<open>
       Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_foparam o Context.proof_of))
 \<close> \<open>Convert param or fref rule to first order rule\<close>
   (* Overloading existing param_fo - attribute from Parametricity.thy *)
   attribute_setup param_fo = \<open>
       Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_foparam o Context.proof_of))
 \<close> \<open>Convert param or fref rule to first order rule\<close>
 
   attribute_setup to_hnr = \<open>
     Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_hnr o Context.proof_of))
 \<close> "Convert hfref-rule to hnr-rule"
   
   attribute_setup to_hfref = \<open>Scan.succeed (
       Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.to_hfref)
     )\<close> \<open>Convert hnr to hfref theorem\<close>
 
 
   attribute_setup ensure_fref_nres = \<open>Scan.succeed (
       Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.ensure_fref_nres)
     )\<close>
 
   attribute_setup sepref_dbg_norm_fcomp_rule = \<open>Scan.succeed (
       Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.norm_fcomp_rule)
     )\<close>
 
   attribute_setup sepref_simplify_precond = \<open>Scan.succeed (
       Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.simplify_precond)
     )\<close> \<open>Simplify precondition of fref/hfref-theorem\<close>
 
   attribute_setup FCOMP = Sepref_Rules.fcomp_attrib "Composition of refinement rules"
 
 end