--- a/Nominal-General/nominal_library.ML	Sat Aug 28 18:15:23 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sun Aug 29 00:09:45 2010 +0800
@@ -33,6 +33,10 @@
   val mk_supp_ty: typ -> term -> term
   val mk_supp: term -> term
 
+  val supports_const: typ -> term
+  val mk_supports_ty: typ -> term -> term -> term
+  val mk_supports: term -> term -> term
+
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 
@@ -43,6 +47,9 @@
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
 
+  (* fresh arguments for a term *)
+  val fresh_args: Proof.context -> term -> term list
+
   (* datatype operations *)
   type cns_info = (term * typ * typ list * bool list) list
 
@@ -114,6 +121,9 @@
 fun mk_supp_ty ty t = supp_const ty $ t;
 fun mk_supp t = mk_supp_ty (fastype_of t) t;
 
+fun supports_const ty = Const (@{const_name "supports"}, [@{typ "atom set"}, ty] ---> @{typ bool});
+fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2;
+fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2;
 
 fun mk_equiv r = r RS @{thm eq_reflection};
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
@@ -142,6 +152,18 @@
 
 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
 
+
+(* produces fresh arguments for a term *)
+
+fun fresh_args ctxt f =
+    f |> fastype_of
+      |> binder_types
+      |> map (pair "z")
+      |> Variable.variant_frees ctxt [f]
+      |> map Free
+
+
+
 (** datatypes **)
 
 (* constructor infos *)

--- a/Nominal/Ex/SingleLet.thy	Sat Aug 28 18:15:23 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 29 00:09:45 2010 +0800
@@ -21,6 +21,8 @@
 where
   "bn (As x y t) = {atom x}"
 
+thm Ball_def Bex_def mem_def
+
 thm single_let.distinct
 thm single_let.induct
 thm single_let.exhaust
@@ -30,19 +32,88 @@
 thm single_let.eq_iff
 thm single_let.fv_bn_eqvt
 thm single_let.size_eqvt
-
+thm single_let.supports
 
-(*
+lemma test:
+  "finite (supp (t::trm)) \<and> finite (supp (a::assg))"
+apply(rule single_let.induct)
+apply(rule supports_finite)
+apply(rule single_let.supports)
+apply(simp only: finite_supp supp_Pair finite_Un)
+apply(rule supports_finite)
+apply(rule single_let.supports)
+apply(simp only: finite_supp supp_Pair finite_Un, simp)
+apply(rule supports_finite)
+apply(rule single_let.supports)
+apply(simp only: finite_supp supp_Pair finite_Un, simp)
+apply(rule supports_finite)
+apply(rule single_let.supports)
+apply(simp only: finite_supp supp_Pair finite_Un, simp)
+apply(rule supports_finite)
+apply(rule single_let.supports)
+apply(simp only: finite_supp supp_Pair finite_Un, simp)
+apply(rule supports_finite)
+apply(rule single_let.supports)
+apply(simp only: finite_supp supp_Pair finite_Un, simp)
+apply(rule supports_finite)
+apply(rule single_let.supports)
+apply(simp only: finite_supp supp_Pair finite_Un, simp)
+apply(rule supports_finite)
+apply(rule single_let.supports)
+apply(simp only: finite_supp supp_Pair finite_Un, simp)
+done
+
+instantiation trm and assg :: fs
+begin
+
+instance
+apply(default)
+apply(simp_all add: test)
+done
+
+end
 
 
+
+
+lemma test: 
+  "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
+oops
+
+lemma Abs_eq_iff:
+  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
+  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+  by (lifting alphas_abs)
+
+(*
 lemma supp_fv:
-  "supp t = fv_trm t"
-  "supp b = fv_bn b"
-apply(induct t and b rule: i1)
-apply(simp_all add: f1)
-apply(simp_all add: supp_def)
-apply(simp_all add: b1)
+  "supp t = fv_trm t \<and> supp b = fv_bn b"
+apply(rule single_let.induct)
+apply(simp_all only: single_let.fv_defs)[2]
+apply(simp_all only: supp_def)[2]
+apply(simp_all only: single_let.perm_simps)[2]
+apply(simp_all only: single_let.eq_iff)[2]
+apply(simp_all only: de_Morgan_conj)[2]
+apply(simp_all only: Collect_disj_eq)[2]
+apply(simp_all only: finite_Un)[2]
+apply(simp_all only: de_Morgan_conj)[2]
+apply(simp_all only: Collect_disj_eq)[2]
+apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)")
+apply(simp only: single_let.fv_defs)
+apply(simp only: supp_abs)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: single_let.perm_simps)
+apply(simp only: single_let.eq_iff)
+apply(subst test)
+apply(simp only: Abs_eq_iff[symmetric])
+apply(simp only: alphas_abs[symmetric])
+apply(simp only: eqvts)
+thm Abs_eq_iff
+apply(simp only: alphas)
 sorry
+*)
+(*
 
 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"

--- a/Nominal/NewParser.thy	Sat Aug 28 18:15:23 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 29 00:09:45 2010 +0800
@@ -9,6 +9,7 @@
      ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
+     ("nominal_dt_supp.ML")
 begin
 
 use "nominal_dt_rawperm.ML"
@@ -23,13 +24,16 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
+use "nominal_dt_supp.ML"
+ML {* open Nominal_Dt_Supp *}
 
 section{* Interface for nominal_datatype *}
 
 ML {*
 (* attributes *)
-val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add)
+val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
+val simp_attr = Attrib.internal (K Simplifier.simp_add)
 
 *}
 
@@ -300,7 +304,7 @@
     else raise TEST lthy0
  
   (* noting the raw permutations as eqvt theorems *)
-  val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
+  val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
 
   (* definition of raw fv_functions *)
   val _ = warning "Definition of raw fv-functions";
@@ -345,7 +349,7 @@
     else raise TEST lthy4
 
   (* noting the raw_bn_eqvt lemmas in a temprorary theory *)
-  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_bn_eqvt) lthy4)
+  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4)
 
   val raw_fv_eqvt = 
     if get_STEPS lthy > 7
@@ -361,7 +365,7 @@
       |> map (fn thm => thm RS @{thm sym})
     else raise TEST lthy4
  
-  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_fv_eqvt) lthy_tmp)
+  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
     if get_STEPS lthy > 9
@@ -440,7 +444,7 @@
   (* noting the quot_respects lemmas *)
   val (_, lthy6a) = 
     if get_STEPS lthy > 21
-    then Local_Theory.note ((Binding.empty, [rsp_attrib]),
+    then Local_Theory.note ((Binding.empty, [rsp_attr]),
       raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6
     else raise TEST lthy6
 
@@ -503,7 +507,7 @@
     then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
-  val qconstrs = map #qconst qconstrs_info
+  val qtrms = map #qconst qconstrs_info
   val qbns = map #qconst qbns_info
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
@@ -536,6 +540,14 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
     else raise TEST lthyA
 
+  (* Supports lemmas *) 
+
+  val qsupports_thms =
+    if get_STEPS lthy > 28
+    then prove_supports lthyB qperm_simps qtrms
+    else raise TEST lthyB
+
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -548,11 +560,12 @@
      ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
-     ||>> Local_Theory.note ((thms_suffix "perm_simps", []), qperm_simps) 
+     ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
+     ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      
 in
   (0, lthy9')

--- /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 *)
+