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

  val prove_fv_supp: typ list -> term list -> term list -> term list -> thm list -> thm list -> 
    thm list -> thm list -> thm list -> thm list -> 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 mk_fvs_goals ty_arg_map fv =
  let
    val arg = fastype_of fv
      |> domain_type
      |> lookup ty_arg_map
  in
    (fv $ arg, mk_supp arg)
      |> HOLogic.mk_eq
      |> HOLogic.mk_Trueprop 
  end

fun mk_fv_bns_goals ty_arg_map fv_bn alpha_bn =
  let
    val arg = fastype_of fv_bn
      |> domain_type
      |> lookup ty_arg_map
  in
    (fv_bn $ arg, mk_supp_rel alpha_bn arg)
      |> HOLogic.mk_eq
      |> HOLogic.mk_Trueprop 
  end

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 thm =
  (prop_of thm)
  |> HOLogic.dest_Trueprop
  |> snd o HOLogic.dest_eq
  |> fastype_of
  |> (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", [prop_of thm]))


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 ind_tac ctxt qinducts = 
  let
    fun CASES_TAC_TO_TAC cases_tac st = Seq.map snd (cases_tac st)
  in
    DETERM o (CASES_TAC_TO_TAC o (Induct.induct_tac ctxt false [] [] [] (SOME qinducts) []))
  end

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

fun prove_fv_supp qtys fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps 
  fv_bn_eqvts qinducts bclausess ctxt =
  let
    val (arg_names, ctxt') = 
      Variable.variant_fixes (replicate (length qtys) "x") ctxt 
    val args = map2 (curry Free) arg_names qtys 
    val ty_arg_map = qtys ~~ args
    val ind_args = map SOME arg_names

    val goals1 = map (mk_fvs_goals ty_arg_map) fvs
    val goals2 = map2 (mk_fv_bns_goals ty_arg_map) fv_bns alpha_bns

    fun fv_tac ctxt bclauses =
      SOLVED' (EVERY' [
        (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ "  with  " ^ (@{make_string} bclauses))),
        TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), 
        p_tac "A",
        TRY o EVERY' (mk_supp_abs_tac ctxt bclauses),
        p_tac "B",
        TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
        p_tac "C",
        TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
        p_tac "D",
        TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
        p_tac "E",
        TRY o asm_full_simp_tac (add_ss thms3),
        p_tac "F",
        TRY o simp_tac (add_ss thms2),
        p_tac "G",
        TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))),
        p_tac "H",
        (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i))
        ])
    
    fun bn_tac ctxt bn_simp =
      SOLVED' (EVERY' [
        (fn i => print_tac ("BN Goal: " ^ string_of_int i)),
        TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
        q_tac "A",
        TRY o mk_bn_supp_abs_tac bn_simp,
        q_tac "B",
        TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
        q_tac "C",
        TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
        q_tac "D",
        TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
        q_tac "E",
        TRY o asm_full_simp_tac (add_ss thms3),
        q_tac "F",
        TRY o simp_tac (add_ss thms2),
        q_tac "G",
        TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))),
        (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i))
        ])

    fun fv_tacs ctxt = map (fv_tac ctxt) bclausess
    fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps
    
  in
    Goal.prove_multi ctxt' [] [] (goals1 @ goals2)
     (fn {context as ctxt, ...} => HEADGOAL 
       (ind_tac ctxt qinducts THEN' RANGE  (fv_tacs ctxt @ bn_tacs ctxt)))
    |> ProofContext.export ctxt' ctxt
  end



end (* structure *)