1 (*  Title:      nominal_dt_alpha.ML

     2     Author:     Christian Urban

     3     Author:     Cezary Kaliszyk

     4 

     5   Deriving support propoerties for the quotient types.

     6 *)

     7 

     8 signature NOMINAL_DT_SUPP =

     9 sig

    10   val prove_supports: Proof.context -> thm list -> term list -> thm list  

    11 

    12 end

    13 

    14 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =

    15 struct

    16 

    17 

    18 (* supports lemmas *)

    19 

    20 fun mk_supports_goal ctxt qtrm =

    21 let  

    22   val vs = fresh_args ctxt qtrm

    23   val rhs = list_comb (qtrm, vs)

    24   val lhs = mk_supp (foldl1 HOLogic.mk_prod vs)

    25 in

    26   mk_supports lhs rhs

    27   |> HOLogic.mk_Trueprop

    28 end

    29 

    30 fun supports_tac ctxt perm_simps =

    31 let

    32   val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}

    33   val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}

    34 in

    35   EVERY' [ simp_tac ss1,

    36            Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [],

    37            simp_tac ss2 ]

    38 end

    39 

    40 fun prove_supports_single ctxt perm_simps qtrm =

    41 let

    42   val goal = mk_supports_goal ctxt qtrm 

    43   val ctxt' = Variable.auto_fixes goal ctxt

    44 in

    45   Goal.prove ctxt' [] [] goal

    46    (K (HEADGOAL (supports_tac ctxt perm_simps)))

    47   |> singleton (ProofContext.export ctxt' ctxt)

    48 end

    49 

    50 fun prove_supports ctxt perm_simps qtrms =

    51   map (prove_supports_single ctxt perm_simps) qtrms

    52 

    53 

    54 

    55 

    56 end (* structure *)

    57