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

structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
struct


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


end (* structure *)