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