(*  Title:      nominal_dt_alpha.ML

    Author:     Christian Urban

    Author:     Cezary Kaliszyk

  Performing quotient constructions, lifting theorems and

  deriving support properties 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  

  val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> 

    thm list -> thm list -> thm list -> thm list -> thm list

  val prove_strong_induct: Proof.context -> thm -> thm list -> bclause list list list -> thm

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

(* fixme: move into nominal_library *)

fun abs_const bmode ty =

  let

    val (const_name, binder_ty, abs_ty) = 

      case bmode of

        Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})

      | Set => (@{const_name "Abs_set"}, @{typ "atom set"},  @{type_name abs_set})

      | Res => (@{const_name "Abs_res"}, @{typ "atom set"},  @{type_name abs_res})

  in

    Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty]))

  end

fun mk_abs bmode trm1 trm2 =

  abs_const bmode (fastype_of trm2) $ trm1 $ trm2  

fun is_abs_eq thm =

  let

    fun is_abs trm =

      case (head_of trm) of

        Const (@{const_name "Abs_set"}, _) => true

      | Const (@{const_name "Abs_lst"}, _) => true

      | Const (@{const_name "Abs_res"}, _) => true

      | _ => false

  in 

    thm |> prop_of 

        |> HOLogic.dest_Trueprop

        |> HOLogic.dest_eq

        |> fst

        |> is_abs

  end

(* adds a freshness condition to the assumptions *)

fun mk_ecase_prems lthy c (params, prems, concl) bclauses =

  let

    val tys = map snd params

    val binders = get_all_binders bclauses

    fun prep_binder (opt, i) = 

      let

        val t = Bound (length tys - i - 1)

      in

        case opt of

          NONE => setify_ty lthy (nth tys i) t 

        | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)   

      end 

    val prems' = 

      case binders of

        [] => prems                        (* case: no binders *)

      | _ => binders                       (* case: binders *) 

          |> map prep_binder

          |> fold_union_env tys

          |> (fn t => mk_fresh_star t c)

          |> (fn t => HOLogic.mk_Trueprop t :: prems)

  in

    mk_full_horn params prems' concl

  end  

(* derives the freshness theorem that there exists a p, such that 

   (p o as) #* (c, t1,..., tn) *)

fun fresh_thm ctxt c parms binders bn_finite_thms =

  let

    fun prep_binder (opt, i) = 

      case opt of

        NONE => setify ctxt (nth parms i) 

      | SOME bn => to_set (bn $ (nth parms i))  

    fun prep_binder2 (opt, i) = 

      case opt of

        NONE => atomify ctxt (nth parms i)

      | SOME bn => bn $ (nth parms i) 

    val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))

    val lhs = binders

      |> map prep_binder

      |> fold_union

      |> mk_perm (Bound 0)

    val goal = mk_fresh_star lhs rhs

      |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))

      |> HOLogic.mk_Trueprop   

    val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} 

      @ @{thms finite.intros finite_Un finite_set finite_fset}  

  in

    Goal.prove ctxt [] [] goal

      (K (HEADGOAL (rtac @{thm at_set_avoiding1}

          THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))

  end

(* derives an abs_eq theorem of the form 

   Exists q. [as].x = [p o as].(q o x)  for non-recursive binders 

   Exists q. [as].x = [q o as].(q o x)  for recursive binders

*)

fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns

  (bclause as (BC (bmode, binders, bodies))) =

  case binders of

    [] => [] 

  | _ =>

      let

        val rec_flag = is_recursive_binder bclause

        val binder_trm = comb_binders ctxt bmode parms binders