(*  Title:      nominal_dt_alpha.ML
    Author:     Cezary Kaliszyk
    Author:     Christian Urban

  Definitions and proofs for the alpha-relations.
*)

signature NOMINAL_DT_ALPHA =
sig
  val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
    term list -> Proof.context -> term list * term list * thm list * thm list * thm * local_theory

  val mk_alpha_distincts: Proof.context -> thm list -> thm list -> 
    term list -> typ list -> thm list

  val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
    thm list -> (thm list * thm list)

  val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> 
    (Proof.context -> int -> tactic) -> Proof.context -> thm list

  val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
  val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
  val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
  val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> 
    Proof.context -> thm list * thm list
  val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
  val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
    term list -> thm -> thm list -> Proof.context -> thm list
  val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
  val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
  val raw_alpha_bn_rsp: thm list -> thm list -> thm list

  val mk_funs_rsp: thm -> thm
  val mk_alpha_permute_rsp: thm -> thm 
end

structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
struct

fun lookup xs x = the (AList.lookup (op=) xs x)
fun group xs = AList.group (op=) xs

(** definition of the inductive rules for alpha and alpha_bn **)

(* construct the compound terms for prod_fv and prod_alpha *)
fun mk_prod_fv (t1, t2) =
let
  val ty1 = fastype_of t1
  val ty2 = fastype_of t2 
  val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
in
  Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
end

fun mk_prod_alpha (t1, t2) =
let
  val ty1 = fastype_of t1
  val ty2 = fastype_of t2 
  val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
  val resT = [prodT, prodT] ---> @{typ "bool"}
in
  Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
end

(* generates the compound binder terms *)
fun mk_binders lthy bmode args bodies = 
let  
  fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
    | bind_set _ args (SOME bn, i) = bn $ (nth args i)
  fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
    | bind_lst _ args (SOME bn, i) = bn $ (nth args i)

  val (combine_fn, bind_fn) =
    case bmode of
      Lst => (mk_append, bind_lst) 
    | Set => (mk_union,  bind_set)
    | Res => (mk_union,  bind_set)
in
  bodies
  |> map (bind_fn lthy args)
  |> foldl1 combine_fn 
end

(* produces the term for an alpha with abstraction *)
fun mk_alpha_term bmode fv alpha args args' binders binders' =
let
  val (alpha_name, binder_ty) = 
    case bmode of
      Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
    | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
    | Res => (@{const_name "alpha_res"}, @{typ "atom set"})
  val ty = fastype_of args
  val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
  val alpha_ty = [ty, ty] ---> @{typ "bool"}
  val fv_ty = ty --> @{typ "atom set"}
  val pair_lhs = HOLogic.mk_prod (binders, args)
  val pair_rhs = HOLogic.mk_prod (binders', args')
in
  HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
    Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) 
      $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs)
end

(* for non-recursive binders we have to produce alpha_bn premises *)
fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = 
  case binder of
    (NONE, _) => []
  | (SOME bn, i) =>
     if member (op=) bodies i then [] 
     else [lookup alpha_bn_map bn $ nth args i $ nth args' i]

(* generat the premises for an alpha rule; mk_frees is used
   if no binders are present *)
fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
let
  fun mk_frees i =
    let
      val arg = nth args i
      val arg' = nth args' i
      val ty = fastype_of arg
    in
      if nth is_rec i
      then fst (lookup alpha_map ty) $ arg $ arg'
      else HOLogic.mk_eq (arg, arg')
    end

  fun mk_alpha_fv i = 
    let
      val ty = fastype_of (nth args i)
    in
      case AList.lookup (op=) alpha_map ty of
        NONE => (HOLogic.eq_const ty, supp_const ty) 
      | SOME (alpha, fv) => (alpha, fv) 
    end  
in
  case bclause of
    BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies 
  | BC (bmode, binders, bodies) => 
    let
      val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
      val comp_fv = foldl1 mk_prod_fv fvs
      val comp_alpha = foldl1 mk_prod_alpha alphas
      val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
      val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
      val comp_binders = mk_binders lthy bmode args binders
      val comp_binders' = mk_binders lthy bmode args' binders
      val alpha_prem = 
        mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
      val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
    in
      map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
    end
end

(* produces the introduction rule for an alpha rule *)
fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = 
let
  val arg_names = Datatype_Prop.make_tnames arg_tys
  val arg_names' = Name.variant_list arg_names arg_names
  val args = map Free (arg_names ~~ arg_tys)
  val args' = map Free (arg_names' ~~ arg_tys)
  val alpha = fst (lookup alpha_map ty)
  val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
  val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
in
  Library.foldr Logic.mk_implies (flat prems, concl)
end

(* produces the premise of an alpha-bn rule; we only need to
   treat the case special where the binding clause is empty;
   
   - if the body is not included in the bn_info, then we either
     produce an equation or an alpha-premise

   - if the body is included in the bn_info, then we create
     either a recursive call to alpha-bn, or no premise  *)
fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
let
  fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i = 
  let
    val arg = nth args i
    val arg' = nth args' i
    val ty = fastype_of arg
  in
    case AList.lookup (op=) bn_args i of
      NONE => (case (AList.lookup (op=) alpha_map ty) of
                 NONE =>  [HOLogic.mk_eq (arg, arg')]
               | SOME (alpha, _) => [alpha $ arg $ arg'])
    | SOME (NONE) => []
    | SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg']
  end  
in
  case bclause of
    BC (_, [], bodies) => 
      map HOLogic.mk_Trueprop 
        (flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))
  | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
end

fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
let
  val arg_names = Datatype_Prop.make_tnames arg_tys
  val arg_names' = Name.variant_list arg_names arg_names
  val args = map Free (arg_names ~~ arg_tys)
  val args' = map Free (arg_names' ~~ arg_tys)
  val alpha_bn = lookup alpha_bn_map bn_trm
  val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
  val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
in
  Library.foldr Logic.mk_implies (flat prems, concl)
end

fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = 
let
  val nth_constrs_info = nth constrs_info bn_n
  val nth_bclausess = nth bclausesss bn_n
in
  map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
end

fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy =
let
  val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names
  val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys
  val alpha_frees = map Free (alpha_names ~~ alpha_tys)
  val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs)

  val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
  val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
  val alpha_bn_names = map (prefix "alpha_") bn_names
  val alpha_bn_arg_tys = map (nth raw_tys) bn_tys
  val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
  val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
  val alpha_bn_map = bns ~~ alpha_bn_frees

  val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) cns_info bclausesss 
  val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info

  val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
    (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
  val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
  
  val (alphas, lthy') = Inductive.add_inductive_i
     {quiet_mode = true, verbose = false, alt_name = Binding.empty,
      coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
     all_alpha_names [] all_alpha_intros [] lthy

  val all_alpha_trms_loc = #preds alphas;
  val alpha_induct_loc = #raw_induct alphas;
  val alpha_intros_loc = #intrs alphas;
  val alpha_cases_loc = #elims alphas;
  val phi = ProofContext.export_morphism lthy' lthy;

  val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc;
  val alpha_induct = Morphism.thm phi alpha_induct_loc;
  val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
  val alpha_cases = map (Morphism.thm phi) alpha_cases_loc

  val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
in
  (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
end



(** produces the distinctness theorems **)

(* transforms the distinctness theorems of the constructors 
   to "not-alphas" of the constructors *)
fun mk_distinct_goal ty_trm_assoc neq =
let
  val (lhs, rhs) = 
    neq
    |> HOLogic.dest_Trueprop
    |> HOLogic.dest_not
    |> HOLogic.dest_eq
  val ty = fastype_of lhs
in
  (lookup ty_trm_assoc ty) $ lhs $ rhs
  |> HOLogic.mk_not
  |> HOLogic.mk_Trueprop
end

fun distinct_tac cases_thms distinct_thms =
  rtac notI THEN' eresolve_tac cases_thms 
  THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)


fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
let
  val ty_trm_assoc = alpha_tys ~~ alpha_trms

  fun mk_alpha_distinct distinct_trm =
  let
    val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt
    val goal = mk_distinct_goal ty_trm_assoc trm'
  in
    Goal.prove ctxt' [] [] goal 
      (K (distinct_tac cases_thms distinct_thms 1))
    |> singleton (Variable.export ctxt' ctxt)
  end
    
in
  map (mk_alpha_distinct o prop_of) distinct_thms
end



(** produces the alpha_eq_iff simplification rules **)

(* in case a theorem is of the form (C.. = C..), it will be
   rewritten to ((C.. = C..) = True) *)
fun mk_simp_rule thm =
  case (prop_of thm) of
    @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm]
  | _ => thm

fun alpha_eq_iff_tac dist_inj intros elims =
  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE'
  (rtac @{thm iffI} THEN' 
    RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj),
           asm_full_simp_tac (HOL_ss addsimps intros)])

fun mk_alpha_eq_iff_goal thm =
  let
    val prop = prop_of thm;
    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
    fun list_conj l = foldr1 HOLogic.mk_conj l;
  in
    if hyps = [] then HOLogic.mk_Trueprop concl
    else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
  end;

fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
let
  val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
  val goals = map mk_alpha_eq_iff_goal thms_imp;
  val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1;
  val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
in
  Variable.export ctxt' ctxt thms
  |> `(map mk_simp_rule)
end


(** proof by induction over the alpha-definitions **)

fun is_true @{term "Trueprop True"} = true
  | is_true _ = false 

fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
let
  val arg_tys = map (domain_type o fastype_of) alphas

  val ((arg_names1, arg_names2), ctxt') =
    ctxt
    |> Variable.variant_fixes (replicate (length alphas) "x") 
    ||>> Variable.variant_fixes (replicate (length alphas) "y")

  val args1 = map2 (curry Free) arg_names1 arg_tys
  val args2 = map2 (curry Free) arg_names2 arg_tys

  val true_trms = replicate (length alphas) (K @{term True})
  
  fun apply_all x fs = map (fn f => f x) fs
  val goals_rhs = 
    group (props @ (alphas ~~ true_trms))
    |> map snd 
    |> map2 apply_all (args1 ~~ args2)
    |> map fold_conj

  fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
  val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)

  val goals =
    (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
    |> foldr1 HOLogic.mk_conj
    |> HOLogic.mk_Trueprop

  fun tac ctxt =
   HEADGOAL 
     (DETERM o (rtac alpha_induct_thm) 
      THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
in
  Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
  |> singleton (ProofContext.export ctxt' ctxt)
  |> Datatype_Aux.split_conj_thm
  |> map (fn th => th RS mp) 
  |> map Datatype_Aux.split_conj_thm
  |> flat
  |> map zero_var_indexes
  |> filter_out (is_true o concl_of)
end


(** reflexivity proof for the alphas **)

val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}

fun cases_tac intros =
let
  val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}

  val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac  

  val bound_tac = 
    EVERY' [ rtac exi_zero, 
             resolve_tac @{thms alpha_refl}, 
             asm_full_simp_tac (HOL_ss addsimps prod_simps) ]
in
  REPEAT o FIRST' [rtac @{thm conjI}, 
    resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]]
end

fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt =
let
  val arg_tys = 
    alpha_trms
    |> map fastype_of
    |> map domain_type
  val arg_bn_tys = 
    alpha_bns
    |> map fastype_of
    |> map domain_type
  val arg_names = Datatype_Prop.make_tnames arg_tys
  val arg_bn_names = map (lookup (arg_tys ~~ arg_names)) arg_bn_tys
  val args = map Free (arg_names ~~ arg_tys)
  val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys)
  val goal = 
    group ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms))
    |> map (fn (ar, cnsts) => map (fn c => c $ ar $ ar) cnsts) 
    |> map (foldr1 HOLogic.mk_conj)
    |> foldr1 HOLogic.mk_conj
    |> HOLogic.mk_Trueprop
in
  Goal.prove ctxt arg_names [] goal
    (fn {context, ...} => 
       HEADGOAL (DETERM o (rtac raw_dt_induct) THEN_ALL_NEW cases_tac alpha_intros)) 
  |> Datatype_Aux.split_conj_thm 
  |> map Datatype_Aux.split_conj_thm 
  |> flat
end



(** symmetry proof for the alphas **)

val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"
  by (erule exE, rule_tac x="-p" in exI, auto)}

(* for premises that contain binders *)
fun prem_bound_tac pred_names ctxt = 
let
  fun trans_prem_tac pred_names ctxt = 
    SUBPROOF (fn {prems, context, ...} => 
    let
      val prems' = map (transform_prem1 context pred_names) prems
    in
      resolve_tac prems' 1
    end) ctxt
  val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
in
  EVERY' 
    [ etac exi_neg,
      resolve_tac @{thms alpha_sym_eqvt},
      asm_full_simp_tac (HOL_ss addsimps prod_simps),
      Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
      trans_prem_tac pred_names ctxt ] 
end

fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =
let
  val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
  
  fun tac ctxt = 
    let
      val alpha_names =  map (fst o dest_Const) alpha_trms   
    in
      resolve_tac alpha_intros THEN_ALL_NEW 
      FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt]
  end
in
  alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt 
end


(** transitivity proof for alphas **)

(* applies cases rules and resolves them with the last premise *)
fun ecases_tac cases = 
  Subgoal.FOCUS (fn {prems, ...} =>
    HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))

fun aatac pred_names = 
  SUBPROOF (fn {prems, context, ...} =>
    HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
  
(* instantiates exI with the permutation p + q *)
val perm_inst_tac =
  Subgoal.FOCUS (fn {params, ...} => 
    let
      val (p, q) = pairself snd (last2 params)
      val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q]
      val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
    in
      HEADGOAL (rtac exi_inst)
    end)

fun non_trivial_cases_tac pred_names intros ctxt = 
let
  val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
in
  resolve_tac intros
  THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
    TRY o EVERY'   (* if binders are present *)
      [ etac @{thm exE},
        etac @{thm exE},
        perm_inst_tac ctxt, 
        resolve_tac @{thms alpha_trans_eqvt}, 
        atac,
        aatac pred_names ctxt, 
        Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
        asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
end
			  
fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt =
let
  fun all_cases ctxt = 
    asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) 
    THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
in
  EVERY' [ rtac @{thm allI}, rtac @{thm impI}, 
           ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]
end

fun prep_trans_goal alpha_trm (arg1, arg2) =
let
  val arg_ty = fastype_of arg1
  val mid = alpha_trm $ arg2 $ (Bound 0)
  val rhs = alpha_trm $ arg1 $ (Bound 0) 
in
  HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))
end

fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
let
  val alpha_names =  map (fst o dest_Const) alpha_trms 
  val props = map prep_trans_goal alpha_trms
  val norm = @{lemma "A ==> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}  
in
  alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
    (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
end


(** proves the equivp predicate for all alphas **)

val transp_def' =
  @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" 
    by (rule eq_reflection, auto simp add: transp_def)}

fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = 
let
  val refl' = map (fold_rule @{thms reflp_def} o atomize) refl
  val symm' = map (fold_rule @{thms symp_def} o atomize) symm
  val trans' = map (fold_rule [transp_def'] o atomize) trans

  fun prep_goal t = 
    HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) 
in    
  Goal.prove_multi ctxt [] [] (map prep_goal (alphas @ alpha_bns))
  (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' 
     RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
  |> chop (length alphas)
end


(* proves that alpha_raw implies alpha_bn *)

fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = 
  SUBPROOF (fn {prems, context, ...} => 
    let
      val prems' = flat (map Datatype_Aux.split_conj_thm prems)
      val prems'' = map (transform_prem1 context pred_names) prems'
    in
      HEADGOAL 
        (REPEAT_ALL_NEW 
           (FIRST' [ rtac @{thm TrueI}, 
                     rtac @{thm conjI}, 
                     resolve_tac prems', 
                     resolve_tac prems'',
                     resolve_tac alpha_intros ]))
    end) ctxt

fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt =
let
  val arg_ty = domain_type o fastype_of 
  val alpha_names =  map (fst o dest_Const) alpha_trms
  val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
  val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms
in
  alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct 
    (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt
end


(* respectfulness for fv_raw / bn_raw *)

fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
let
  val arg_ty = domain_type o fastype_of 
  val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
  fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)

  val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
  val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)
  val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
  
  val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} 
    @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) 
in
  alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct 
    (K (asm_full_simp_tac ss)) ctxt
end


(* respectfulness for size *)

fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
let
  val arg_tys = map (domain_type o fastype_of) all_alpha_trms

  fun mk_prop ty (x, y) = HOLogic.mk_eq 
    (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)

  val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys 
  
  val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps 
    permute_prod_def prod.cases prod.recs})

  val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
in
  alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
end


(* respectfulness for constructors *)

fun raw_constr_rsp_tac alpha_intros simps = 
let
  val pre_ss = HOL_ss addsimps @{thms fun_rel_def}
  val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps 
    prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
  (* funs_rsp alpha_bn_simps *)
in
  asm_full_simp_tac pre_ss
  THEN' REPEAT o (resolve_tac @{thms allI impI})
  THEN' resolve_tac alpha_intros
  THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
end


fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
let
  val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
  
  fun lookup ty = 
    case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of
      NONE => HOLogic.eq_const ty
    | SOME alpha => alpha 
  
  fun fun_rel_app t1 t2 = 
    Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2

  fun prep_goal trm =
    trm
    |> strip_type o fastype_of
    |>> map lookup
    ||> lookup
    |> uncurry (fold_rev fun_rel_app)
    |> (fn t => t $ trm $ trm)
    |> Syntax.check_term ctxt
    |> HOLogic.mk_Trueprop
in
  Goal.prove_multi ctxt [] [] (map prep_goal constrs)
    (K (HEADGOAL 
      (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))
end


(* rsp lemmas for alpha_bn relations *)

val rsp_equivp =
  @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q"
    by (simp only: fun_rel_def equivp_def, metis)}

fun raw_alpha_bn_rsp alpha_bn_equivp alpha_bn_imps =
let
  fun mk_thm thm1 thm2 = 
    (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp)
in
  map2 mk_thm alpha_bn_equivp alpha_bn_imps
end


(* transformation of the natural rsp-lemmas into standard form *)

val fun_rsp = @{lemma
  "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}

fun mk_funs_rsp thm = 
 thm
 |> atomize
 |> single
 |> curry (op OF) fun_rsp


val permute_rsp = @{lemma 
  "(!x y p. R x y --> R (permute p x) (permute p y)) 
     ==> ((op =) ===> R ===> R) permute permute"  by simp}

fun mk_alpha_permute_rsp thm = 
 thm
 |> atomize
 |> single
 |> curry (op OF) permute_rsp




end (* structure *)