(*  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

  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: term list -> 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 binders = 

  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

    binders

    |> 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_set"}, @{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]

(* generate 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 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 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 (all_alpha_trms', _) = Variable.importT_terms all_alpha_trms lthy  

    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

    (* proper import of type-variables does not work,

       since then they are replaced by new variables, messing

       up the ty_trm assoc list *)

    val distinct_thms' = map Thm.legacy_freezeT distinct_thms

    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 distinct_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'

    |> map Thm.varifyT_global

  end

(** produces the alpha_eq_iff simplification rules **)

(* in case a theorem is of the form (Rel Const Const), it will be

   rewritten to ((Rel Const = Const) = True) 

*)

fun mk_simp_rule thm =

  case (prop_of thm) of

    @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI}

  | _ => 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

        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