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

  Definitions of the alpha relations.
*)

signature NOMINAL_DT_ALPHA =
sig
  val define_raw_alpha: Datatype_Aux.descr -> (string * sort) 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 list -> 
    term list -> term list -> bn_info -> thm list * thm list

  val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
end

structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
struct

(** 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
  foldl1 combine_fn (map (bind_fn lthy args) bodies)
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 [the (AList.lookup (op=) 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 (the (AList.lookup (op=) 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 (the (AList.lookup (op=) 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) => [the (AList.lookup (op=) 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 = the (AList.lookup (op=) 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 descr sorts bn_info bclausesss fvs lthy =
let
  val alpha_names = prefix_dt_names descr sorts "alpha_"
  val alpha_arg_tys = all_dtyps descr sorts
  val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys
  val alpha_frees = map Free (alpha_names ~~ alpha_tys)
  val alpha_map = alpha_arg_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 (fn i => nth_dtyp descr sorts i) 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 constrs_info = all_dtyp_constrs_types descr sorts

  val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss 
  val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_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_alpha_distinct_goal alpha neq =
let
  val (lhs, rhs) = 
    neq
    |> HOLogic.dest_Trueprop
    |> HOLogic.dest_not
    |> HOLogic.dest_eq
in
  alpha $ lhs $ rhs
  |> HOLogic.mk_not
  |> HOLogic.mk_Trueprop
end

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

fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) =
let
  val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt
  val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms
  val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals
in
  Variable.export ctxt' ctxt nrels
end

fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos =
let
  val alpha_distincts = 
    map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms)
  val distinc_thms = map 
  val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos
  val alpha_bn_distincts =  
    map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms)
in
  (flat alpha_distincts, flat alpha_bn_distincts)
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

end (* structure *)