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

  Performing quotient constructions, lifting theorems and
  deriving support propoerties for the quotient types.
*)

signature NOMINAL_DT_QUOT =
sig
  val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> 
    thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory

  val define_qconsts: typ list -> (string  * term * mixfix) list -> local_theory -> 
    Quotient_Info.qconsts_info list * local_theory

  val define_qperms: typ list -> string list -> (string * sort) list -> 
    (string * term * mixfix) list -> thm list -> local_theory -> local_theory

  val define_qsizes: typ list -> string list -> (string * sort) list -> 
    (string * term * mixfix) list -> local_theory -> local_theory

  val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context

  val prove_supports: Proof.context -> thm list -> term list -> thm list  
  val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list

  val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->  
    local_theory -> local_theory

  val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> 
    thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 

  val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
 
  val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
    thm list -> Proof.context -> thm list

  val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
    thm list -> Proof.context -> thm list  
end

structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
struct


(* defines the quotient types *)
fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
  let
    val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
    val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms
  in
    fold_map Quotient_Type.add_quotient_type qty_args2 lthy
  end 


(* defines quotient constants *)
fun define_qconsts qtys consts_specs lthy =
  let
    val (qconst_infos, lthy') = 
      fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy
    val phi = ProofContext.export_morphism lthy' lthy
  in
    (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy')
  end


(* defines the quotient permutations and proves pt-class *)
fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy =
  let
    val lthy1 = 
      lthy
      |> Local_Theory.exit_global
      |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) 
  
    val (qs, lthy2) = define_qconsts qtys perm_specs lthy1

    val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2

    val lifted_perm_laws = 
      map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws'
      |> Variable.exportT lthy3 lthy2

    fun tac _ =
      Class.intro_classes_tac [] THEN
        (ALLGOALS (resolve_tac lifted_perm_laws))
  in
    lthy2
    |> Class.prove_instantiation_exit tac 
    |> Named_Target.theory_init
  end


(* defines the size functions and proves size-class *)
fun define_qsizes qtys qfull_ty_names tvs size_specs lthy =
  let
    val tac = K (Class.intro_classes_tac [])
  in
    lthy
    |> Local_Theory.exit_global
    |> Class.instantiation (qfull_ty_names, tvs, @{sort size})
    |> snd o (define_qconsts qtys size_specs)
    |> Class.prove_instantiation_exit tac
    |> Named_Target.theory_init
  end


(* lifts a theorem and cleans all "_raw" parts
   from variable names *)

local
  val any = Scan.one (Symbol.not_eof)
  val raw = Scan.this_string "_raw"
  val exclude =
    Scan.repeat (Scan.unless raw any) --| raw >> implode
  val parser = Scan.repeat (exclude || any)
in
  fun unraw_str s =
    s |> raw_explode
      |> Scan.finite Symbol.stopper parser >> implode 
      |> fst
end

fun unraw_vars_thm thm =
  let
    fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)

    val vars = Term.add_vars (prop_of thm) []
    val vars' = map (Var o unraw_var_str) vars
  in
    Thm.certify_instantiate ([], (vars ~~ vars')) thm
  end

fun unraw_bounds_thm th =
  let
    val trm = Thm.prop_of th
    val trm' = Term.map_abs_vars unraw_str trm
  in
    Thm.rename_boundvars trm trm' th
  end

fun lift_thms qtys simps thms ctxt =
  (map (Quotient_Tacs.lifted ctxt qtys simps
        #> unraw_bounds_thm
        #> unraw_vars_thm
        #> Drule.zero_var_indexes) thms, ctxt)



fun mk_supports_goal ctxt qtrm =
  let  
    val vs = fresh_args ctxt qtrm
    val rhs = list_comb (qtrm, vs)
    val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"}
      |> mk_supp
  in
    mk_supports lhs rhs
    |> HOLogic.mk_Trueprop
  end

fun supports_tac ctxt perm_simps =
  let
    val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}
    val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
  in
    EVERY' [ simp_tac ss1,
             Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [],
             simp_tac ss2 ]
  end

fun prove_supports_single ctxt perm_simps qtrm =
  let
    val goal = mk_supports_goal ctxt qtrm 
    val ctxt' = Variable.auto_fixes goal ctxt
  in
    Goal.prove ctxt' [] [] goal
      (K (HEADGOAL (supports_tac ctxt perm_simps)))
    |> singleton (ProofContext.export ctxt' ctxt)
  end

fun prove_supports ctxt perm_simps qtrms =
  map (prove_supports_single ctxt perm_simps) qtrms


(* finite supp lemmas for qtypes *)

fun prove_fsupp ctxt qtys qinduct qsupports_thms =
  let
    val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt
    val goals = vs ~~ qtys
      |> map Free
      |> map (mk_finite o mk_supp)
      |> foldr1 (HOLogic.mk_conj)
      |> HOLogic.mk_Trueprop

    val tac = 
      EVERY' [ rtac @{thm supports_finite},
               resolve_tac qsupports_thms,
               asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ]
  in
    Goal.prove ctxt' [] [] goals
      (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
    |> singleton (ProofContext.export ctxt' ctxt)
    |> Datatype_Aux.split_conj_thm
    |> map zero_var_indexes
  end


(* finite supp instances *)

fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy =
  let
    val lthy1 = 
      lthy
      |> Local_Theory.exit_global
      |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) 
  
    fun tac _ =
      Class.intro_classes_tac [] THEN
        (ALLGOALS (resolve_tac qfsupp_thms))
  in
    lthy1
    |> Class.prove_instantiation_exit tac 
    |> Named_Target.theory_init
  end


(* proves that fv and fv_bn equals supp *)

fun gen_mk_goals fv supp =
  let
    val arg_ty = 
      fastype_of fv
      |> domain_type
  in
    (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x))
  end

fun mk_fvs_goals fv = gen_mk_goals fv mk_supp
fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn)

fun add_ss thms =
  HOL_basic_ss addsimps thms

fun symmetric thms = 
  map (fn thm => thm RS @{thm sym}) thms

val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
val supp_Abs_res = @{thms supp_Abs(2)[symmetric]}
val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]}

fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set 
  | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res
  | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst

fun mk_supp_abs_tac ctxt [] = []
  | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
  | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs

fun mk_bn_supp_abs_tac trm =
  trm
  |> fastype_of
  |> body_type
  |> (fn ty => case ty of
        @{typ "atom set"}  => simp_tac (add_ss supp_Abs_set)
      | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst)
      | _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))


val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}

fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps 
  fv_bn_eqvts qinduct bclausess ctxt =
  let
    val goals1 = map mk_fvs_goals fvs
    val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns   

    fun tac ctxt =
      SUBGOAL (fn (goal, i) =>
        let
          val (fv_fun, arg) = 
            goal |> Envir.eta_contract
                 |> Logic.strip_assums_concl
                 |> HOLogic.dest_Trueprop
                 |> fst o HOLogic.dest_eq
                 |> dest_comb
          val supp_abs_tac = 
            case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of
              SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses)
            | NONE => mk_bn_supp_abs_tac fv_fun
        in
          EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
                   TRY o supp_abs_tac,
                   TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
                   TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
                   TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
                   TRY o asm_full_simp_tac (add_ss thms3),
                   TRY o simp_tac (add_ss thms2),
                   TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i
        end)
  in
    induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
    |> map atomize
    |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
  end


fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt =
  let
    fun mk_goal qbn = 
      let
        val arg_ty = domain_type (fastype_of qbn)
        val finite = @{term "finite :: atom set => bool"}
      in
        (arg_ty, fn x => finite $ (to_set (qbn $ x)))
      end

    val props = map mk_goal qbns
    val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ 
      @{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
  in
    induct_prove qtys props qinduct (K ss_tac) ctxt
  end


fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
  let 
    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
    val p = Free (p, @{typ perm})

    fun mk_goal qperm_bn alpha_bn =
      let
        val arg_ty = domain_type (fastype_of alpha_bn)
      in
        (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x)
      end

    val props = map2 mk_goal qperm_bns alpha_bns
    val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls
    val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss)
  in
    induct_prove qtys props qinduct (K ss_tac) ctxt'
    |> ProofContext.export ctxt' ctxt
    |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
  end

fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt =
  let 
    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
    val p = Free (p, @{typ perm})

    fun mk_goal qbn qperm_bn =
      let
        val arg_ty = domain_type (fastype_of qbn)
      in
        (arg_ty, fn x => 
          (mk_id (Abs ("", arg_ty, 
             HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x))
      end

    val props = map2 mk_goal qbns qperm_bns
    val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
    val ss_tac = 
      EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss),
              TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [],
              TRY o asm_full_simp_tac HOL_basic_ss]
  in
    induct_prove qtys props qinduct (K ss_tac) ctxt'
    |> ProofContext.export ctxt' ctxt 
    |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
  end

end (* structure *)