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

end

structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
struct


(* supports lemmas *)

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




end (* structure *)