(*  Title:      nominal_dt_alpha.ML

    Author:     Christian Urban

    Author:     Cezary Kaliszyk

  Deriving support propoerties for the quotient types.

*)

signature NOMINAL_DT_SUPP =

sig

  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

    thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 

end

structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =

struct

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

(* supports lemmas for constructors *)

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.simps permute_prod_def 

  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI}

fun p_tac msg i = 

  if false then print_tac ("ptest: " ^ msg) else all_tac

fun q_tac msg i = 

  if true then print_tac ("qtest: " ^ msg) else all_tac

  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

  end

end (* structure *)