--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_dt_supp.ML	Sun Aug 29 00:09:45 2010 +0800
@@ -0,0 +1,57 @@
+(*  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 = mk_supp (foldl1 HOLogic.mk_prod vs)
+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 *)
+