--- a/Nominal-General/Nominal2_Base.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal-General/Nominal2_Base.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -848,6 +848,18 @@
   qed
 qed
 
+section {* Support w.r.t. relations *}
+
+text {* 
+  This definition is used for unquotient types, where
+  alpha-equivalence does not coincide with equality.
+*}
+
+definition 
+  "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
+
+
+
 section {* Finitely-supported types *}
 
 class fs = pt +

--- a/Nominal-General/nominal_library.ML	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Fri Sep 10 09:17:40 2010 +0800
@@ -33,6 +33,11 @@
   val mk_supp_ty: typ -> term -> term
   val mk_supp: term -> term
 
+  val supp_rel_ty: typ -> typ
+  val supp_rel_const: typ -> term
+  val mk_supp_rel_ty: typ -> term -> term -> term
+  val mk_supp_rel: term -> term -> term		       
+
   val supports_const: typ -> term
   val mk_supports_ty: typ -> term -> term -> term
   val mk_supports: term -> term -> term
@@ -124,8 +129,13 @@
 
 fun supp_ty ty = ty --> @{typ "atom set"};
 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
-fun mk_supp_ty ty t = supp_const ty $ t;
-fun mk_supp t = mk_supp_ty (fastype_of t) t;
+fun mk_supp_ty ty t = supp_const ty $ t
+fun mk_supp t = mk_supp_ty (fastype_of t) t
+
+fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"};
+fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty)
+fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t
+fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r 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;

--- a/Nominal/Abs.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Abs.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -6,11 +6,6 @@
         "Quotient_Product" 
 begin
 
-section {* Support w.r.t. relations *}
-
-definition 
-  "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
-
 
 section {* Abstractions *}
 

--- a/Nominal/Ex/Ex1.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Ex/Ex1.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -18,8 +18,19 @@
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
-
-thm foo_bar.fv_defs[no_vars] foo_bar.bn_defs[no_vars]
+thm foo_bar.distinct
+thm foo_bar.induct
+thm foo_bar.inducts
+thm foo_bar.exhaust
+thm foo_bar.fv_defs
+thm foo_bar.bn_defs
+thm foo_bar.perm_simps
+thm foo_bar.eq_iff
+thm foo_bar.fv_bn_eqvt
+thm foo_bar.size_eqvt
+thm foo_bar.supports
+thm foo_bar.fsupp
+thm foo_bar.supp
 
 lemma
   "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"

--- a/Nominal/Ex/ExPS8.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Ex/ExPS8.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -6,11 +6,11 @@
 
 atom_decl name
 
-declare [[STEPS = 100]]
+declare [[STEPS = 31]]
 
-nominal_datatype exp =
+nominal_datatype fun_pats: exp =
   EVar name
-| EUnit
+| EUnit 
 | EPair exp exp
 | ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
 and fnclause =
@@ -44,6 +44,57 @@
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp) = {atom x}"
 
+thm fun_pats.distinct
+thm fun_pats.induct
+thm fun_pats.inducts
+thm fun_pats.exhaust
+thm fun_pats.fv_defs
+thm fun_pats.bn_defs
+thm fun_pats.perm_simps
+thm fun_pats.eq_iff
+thm fun_pats.fv_bn_eqvt
+thm fun_pats.size_eqvt
+thm fun_pats.supports
+thm fun_pats.fsupp
+thm fun_pats.supp
+
+
+ML {*
+fun add_ss thms =
+  HOL_basic_ss addsimps thms
+
+fun symmetric thms = 
+  map (fn thm => thm RS @{thm sym}) thms
+*}
+
+lemma
+  "(fv_exp x = supp x) \<and>
+   (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and>
+   (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and>
+   (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and>
+   (fv_lrbs xd = supp xd \<and> fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \<and>
+   (fv_pat xe = supp xe \<and> fv_b_pat xe = supp_rel alpha_b_pat xe)"
+apply(rule fun_pats.induct)
+apply(tactic {* ALLGOALS (TRY o rtac @{thm conjI})*})
+thm fun_pats.inducts
+oops
+
+
+lemma
+  "fv_exp x = supp x" and
+  "fv_fnclause y = supp y" and
+  "fv_fnclauses xb = supp xb" and
+  "fv_lrb xc = supp xc" and
+  "fv_lrbs xd = supp xd" and
+  "fv_pat xe = supp xe" and
+  "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and
+  "fv_b_pat xe = supp_rel alpha_b_pat xe" and
+  "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and 
+  "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and
+  "fv_b_lrb y = supp_rel alpha_b_lrb y"
+apply(induct "x::exp" and "y::fnclause" and xb and xc and xd and xe rule: fun_pats.inducts)
+thm fun_pats.inducts
+oops
 
 end
 

--- a/Nominal/Ex/LetFun.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Ex/LetFun.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -4,8 +4,11 @@
 
 atom_decl name
 
-(* x is bound in both e1 and e2
-   names in p are bound only in e1 *)
+(* x is bound in both e1 and e2;
+   bp-names in p are bound only in e1 
+*)
+
+declare [[STEPS = 100]]
 
 nominal_datatype exp =
   Var name
@@ -22,4 +25,19 @@
 | "bp (PUnit) = []"
 | "bp (PPair p1 p2) = bp p1 @ bp p2"
 
+thm exp_pat.distinct
+thm exp_pat.induct
+thm exp_pat.inducts
+thm exp_pat.exhaust
+thm exp_pat.fv_defs
+thm exp_pat.bn_defs
+thm exp_pat.perm_simps
+thm exp_pat.eq_iff
+thm exp_pat.fv_bn_eqvt
+thm exp_pat.size_eqvt
+thm exp_pat.supports
+thm exp_pat.fsupp
+thm exp_pat.supp
+
+
 end
\ No newline at end of file

--- a/Nominal/Ex/SingleLet.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -6,14 +6,14 @@
 
 declare [[STEPS = 100]]
 
-nominal_datatype single_let: trm  =
+nominal_datatype single_let: trm =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind x in t
 | Let a::"assg" t::"trm"  bind "bn a" in t
 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
-| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 
+| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set) x in t2 
 and assg =
   As "name" x::"name" t::"trm" bind x in t
 binder
@@ -34,6 +34,7 @@
 thm single_let.size_eqvt
 thm single_let.supports
 thm single_let.fsupp
+thm single_let.supp
 
 lemma test2:
   assumes "fv_trm t = supp t" 
@@ -44,26 +45,25 @@
 apply(rule assms)
 done
 
-
 lemma supp_fv:
-  "fv_trm t = supp t" "fv_assg as = supp as" "fv_bn as = supp_rel alpha_bn as"
-apply(induct t and as rule: single_let.inducts)
+  "fv_trm x = supp x" 
+  "fv_assg xa = supp xa"
+  "fv_bn xa = supp_rel alpha_bn xa"
+apply(induct rule: single_let.inducts)
 -- " 0A "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])?
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
 -- " 0B"
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])?
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
 --" 1 "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *})
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -72,7 +72,7 @@
 apply(simp only:)
 -- " 2 "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(subst supp_abs(3)[symmetric])
 apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -82,7 +82,7 @@
 apply(simp only:)
 -- " 3 "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(1)[symmetric])
+apply(subst supp_abs(1)[symmetric])
 apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -91,7 +91,7 @@
 apply(simp only: supp_Pair Un_assoc conj_assoc)
 -- " Bar "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(subst supp_abs(3)[symmetric])
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -100,7 +100,8 @@
 apply(simp only: supp_Pair Un_assoc conj_assoc)
 -- " Baz "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(subst supp_abs(1)[symmetric])
+apply(subst supp_abs(1)[symmetric])
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -110,7 +111,7 @@
 apply(simp only: supp_Pair Un_assoc conj_assoc)
 -- "last"
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *})
 apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)

--- a/Nominal/Nominal2.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Nominal2.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -249,7 +249,6 @@
 end
 *}
 
-
 ML {*
 (* for testing porposes - to exit the procedure early *)
 exception TEST of Proof.context
@@ -259,6 +258,7 @@
 fun get_STEPS ctxt = Config.get ctxt STEPS
 *}
 
+
 setup STEPS_setup
 
 ML {*
@@ -333,9 +333,8 @@
     mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys
 
   (* definition of alpha_eq_iff  lemmas *)
-  (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*)
   val _ = warning "Eq-iff theorems";
-  val (alpha_eq_iff_simps, alpha_eq_iff) = 
+  val alpha_eq_iff = 
     if get_STEPS lthy > 5
     then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases
     else raise TEST lthy4
@@ -542,6 +541,7 @@
   val qinducts = Project_Rule.projections lthyA qinduct
 
   (* supports lemmas *) 
+  val _ = warning "Proving Supports Lemmas and fs-Instances"
   val qsupports_thms =
     if get_STEPS lthy > 28
     then prove_supports lthyB qperm_simps qtrms
@@ -559,6 +559,15 @@
     then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB
     else raise TEST lthyB
 
+  (* fv - supp equality *)
+  val _ = warning "Proving Equality between fv and supp"
+  val qfv_supp_thms = 
+    if get_STEPS lthy > 31
+    then prove_fv_supp qtys qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs 
+      qperm_simps qfv_qbn_eqvts qinducts (flat raw_bclauses) lthyC
+    else []
+
+ 
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -575,15 +584,17 @@
      ||>> 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 "inducts", []), qinducts) 
+     ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
+     ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)
 *}
 
+
 section {* Preparing and parsing of the specification *}
 
 ML {* 

--- a/Nominal/nominal_dt_alpha.ML	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Fri Sep 10 09:17:40 2010 +0800
@@ -14,7 +14,7 @@
     term list -> typ list -> thm list
 
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
-    thm list -> (thm list * thm list)
+    thm list -> thm list
 
   val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
@@ -315,11 +315,12 @@
 
 (** produces the alpha_eq_iff simplification rules **)
 
-(* in case a theorem is of the form (C.. = C..), it will be
-   rewritten to ((C.. = C..) = True) *)
+(* in case a theorem is of the form (Rel Const Const), it will be
+   rewritten to ((Rel Const = Const) = True) 
+*)
 fun mk_simp_rule thm =
   case (prop_of thm) of
-    @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm]
+    @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI}
   | _ => thm
 
 fun alpha_eq_iff_tac dist_inj intros elims =
@@ -347,7 +348,7 @@
   val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
 in
   Variable.export ctxt' ctxt thms
-  |> `(map mk_simp_rule)
+  |> map mk_simp_rule
 end
 
 

--- a/Nominal/nominal_dt_quot.ML	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/nominal_dt_quot.ML	Fri Sep 10 09:17:40 2010 +0800
@@ -20,11 +20,13 @@
     (string * term * mixfix) list -> local_theory -> local_theory
 
   val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context
+
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
 struct
 
+
 (* defines the quotient types *)
 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
 let
@@ -86,7 +88,7 @@
 end
 
 
-(* lifts a theorem and cleans all "_raw" instances 
+(* lifts a theorem and cleans all "_raw" parts
    from variable names *)
 
 local
@@ -126,6 +128,5 @@
         #> unraw_vars_thm
         #> Drule.zero_var_indexes) thms, ctxt)
 
-
 end (* structure *)
 

--- a/Nominal/nominal_dt_supp.ML	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/nominal_dt_supp.ML	Fri Sep 10 09:17:40 2010 +0800
@@ -12,44 +12,48 @@
 
   val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->  
     local_theory -> local_theory
+
+  val prove_fv_supp: typ list -> term list -> term list -> term list -> thm list -> thm list -> 
+    thm list -> thm list -> thm list -> thm list -> bclause list list -> Proof.context -> thm list 
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
 struct
 
+fun lookup xs x = the (AList.lookup (op=) xs x)
 
 (* 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
+  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
+  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
+  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
@@ -58,44 +62,182 @@
 (* 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
+  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
+    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}) 
+  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
+    fun tac _ =
+      Class.intro_classes_tac [] THEN
+        (ALLGOALS (resolve_tac qfsupp_thms))
+  in
+    lthy1
+    |> Class.prove_instantiation_exit tac 
+    |> Named_Target.theory_init
+  end
+
+
+(* proves that fv and fv_bn equals supp *)
+
+fun mk_fvs_goals ty_arg_map fv =
+  let
+    val arg = fastype_of fv
+      |> domain_type
+      |> lookup ty_arg_map
+  in
+    (fv $ arg, mk_supp arg)
+      |> HOLogic.mk_eq
+      |> HOLogic.mk_Trueprop 
+  end
+
+fun mk_fv_bns_goals ty_arg_map fv_bn alpha_bn =
+  let
+    val arg = fastype_of fv_bn
+      |> domain_type
+      |> lookup ty_arg_map
+  in
+    (fv_bn $ arg, mk_supp_rel alpha_bn arg)
+      |> HOLogic.mk_eq
+      |> HOLogic.mk_Trueprop 
+  end
+
+fun add_ss thms =
+  HOL_basic_ss addsimps thms
+
+fun symmetric thms = 
+  map (fn thm => thm RS @{thm sym}) thms
+
+val supp_abs_set = @{thms supp_abs(1)[symmetric]}
+val supp_abs_res = @{thms supp_abs(2)[symmetric]}
+val supp_abs_lst = @{thms supp_abs(3)[symmetric]}
+
+fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_set 
+  | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_res
+  | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_lst
+
+fun mk_supp_abs_tac ctxt [] = []
+  | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
+  | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs
+
+fun mk_bn_supp_abs_tac thm =
+  (prop_of thm)
+  |> HOLogic.dest_Trueprop
+  |> snd o HOLogic.dest_eq
+  |> fastype_of
+  |> (fn ty => case ty of
+        @{typ "atom set"}  => simp_tac (add_ss supp_abs_set)
+      | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst)
+      | _ => raise TERM ("mk_bn_supp_abs_tac", [prop_of thm]))
+
+
+val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
+val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def 
+  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI}
+
+fun ind_tac ctxt qinducts = 
+  let
+    fun CASES_TAC_TO_TAC cases_tac st = Seq.map snd (cases_tac st)
+  in
+    DETERM o (CASES_TAC_TO_TAC o (Induct.induct_tac ctxt false [] [] [] (SOME qinducts) []))
+  end
+
+fun p_tac msg i = 
+  if false then print_tac ("ptest: " ^ msg) else all_tac
+
+fun q_tac msg i = 
+  if true then print_tac ("qtest: " ^ msg) else all_tac
+
+fun prove_fv_supp qtys fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps 
+  fv_bn_eqvts qinducts bclausess ctxt =
+  let
+    val (arg_names, ctxt') = 
+      Variable.variant_fixes (replicate (length qtys) "x") ctxt 
+    val args = map2 (curry Free) arg_names qtys 
+    val ty_arg_map = qtys ~~ args
+    val ind_args = map SOME arg_names
+
+    val goals1 = map (mk_fvs_goals ty_arg_map) fvs
+    val goals2 = map2 (mk_fv_bns_goals ty_arg_map) fv_bns alpha_bns
+
+    fun fv_tac ctxt bclauses =
+      SOLVED' (EVERY' [
+        (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ "  with  " ^ (@{make_string} bclauses))),
+        TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), 
+        p_tac "A",
+        TRY o EVERY' (mk_supp_abs_tac ctxt bclauses),
+        p_tac "B",
+        TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
+        p_tac "C",
+        TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
+        p_tac "D",
+        TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
+        p_tac "E",
+        TRY o asm_full_simp_tac (add_ss thms3),
+        p_tac "F",
+        TRY o simp_tac (add_ss thms2),
+        p_tac "G",
+        TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))),
+        p_tac "H",
+        (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i))
+        ])
+    
+    fun bn_tac ctxt bn_simp =
+      SOLVED' (EVERY' [
+        (fn i => print_tac ("BN Goal: " ^ string_of_int i)),
+        TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
+        q_tac "A",
+        TRY o mk_bn_supp_abs_tac bn_simp,
+        q_tac "B",
+        TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
+        q_tac "C",
+        TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
+        q_tac "D",
+        TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
+        q_tac "E",
+        TRY o asm_full_simp_tac (add_ss thms3),
+        q_tac "F",
+        TRY o simp_tac (add_ss thms2),
+        q_tac "G",
+        TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))),
+        (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i))
+        ])
+
+    fun fv_tacs ctxt = map (fv_tac ctxt) bclausess
+    fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps
+    
+  in
+    Goal.prove_multi ctxt' [] [] (goals1 @ goals2)
+     (fn {context as ctxt, ...} => HEADGOAL 
+       (ind_tac ctxt qinducts THEN' RANGE  (fv_tacs ctxt @ bn_tacs ctxt)))
+    |> ProofContext.export ctxt' ctxt
+  end
+
 
 
 end (* structure *)