# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271244098 -7200
# Node ID 4650d428b1b5799f5c3708cdde697f702ebe95a8
# Parent  16653e702d89bbe306c247f897981568520ccf84# Parent  8db45a1065699b20ee243762eecf88662b65518a
merged

diff -r 16653e702d89 -r 4650d428b1b5 Nominal/Equivp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Equivp.thy	Wed Apr 14 13:21:38 2010 +0200
@@ -0,0 +1,367 @@
+theory Equivp
+imports "Fv"
+begin
+
+ML {*
+fun build_alpha_sym_trans_gl alphas (x, y, z) =
+let
+  fun build_alpha alpha =
+    let
+      val ty = domain_type (fastype_of alpha);
+      val var = Free(x, ty);
+      val var2 = Free(y, ty);
+      val var3 = Free(z, ty);
+      val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
+      val transp = HOLogic.mk_imp (alpha $ var $ var2,
+        HOLogic.mk_all (z, ty,
+          HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
+    in
+      (symp, transp)
+    end;
+  val eqs = map build_alpha alphas
+  val (sym_eqs, trans_eqs) = split_list eqs
+  fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
+in
+  (conj sym_eqs, conj trans_eqs)
+end
+*}
+
+ML {*
+fun build_alpha_refl_gl fv_alphas_lst alphas =
+let
+  val (fvs_alphas, _) = split_list fv_alphas_lst;
+  val (_, alpha_ts) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) alpha_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val args = map Free (names ~~ tys);
+  fun find_alphas ty x =
+    domain_type (fastype_of x) = ty;
+  fun refl_eq_arg (ty, arg) =
+    let
+      val rel_alphas = filter (find_alphas ty) alphas;
+    in
+      map (fn x => x $ arg $ arg) rel_alphas
+    end;
+  (* Flattening loses the induction structure *)
+  val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))
+in
+  (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
+end
+*}
+
+ML {*
+fun reflp_tac induct eq_iff =
+  rtac induct THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
+  split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
+  THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
+     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
+       add_0_left supp_zero_perm Int_empty_left split_conv})
+*}
+
+ML {*
+fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
+let
+  val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
+  val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
+in
+  HOLogic.conj_elims refl_conj
+end
+*}
+
+lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="-pi" in exI)
+by auto
+
+ML {*
+fun symp_tac induct inj eqvt ctxt =
+  rel_indtac induct THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
+  THEN_ALL_NEW
+  REPEAT o etac @{thm exi_neg}
+  THEN_ALL_NEW
+  split_conj_tac THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
+  TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW
+  (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
+*}
+
+
+lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
+apply (erule exE)+
+apply (rule_tac x="pia + pi" in exI)
+by auto
+
+
+ML {*
+fun eetac rule = 
+  Subgoal.FOCUS_PARAMS (fn focus =>
+    let
+      val concl = #concl focus
+      val prems = Logic.strip_imp_prems (term_of concl)
+      val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
+      val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
+      val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
+    in
+      (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
+    end
+  )
+*}
+
+ML {*
+fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
+  rel_indtac induct THEN_ALL_NEW
+  (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
+  split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
+  THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
+  THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
+  TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW
+  (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
+*}
+
+lemma transpI:
+  "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
+  unfolding transp_def
+  by blast
+
+ML {*
+fun equivp_tac reflps symps transps =
+  (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
+  simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+  THEN' rtac conjI THEN' rtac allI THEN'
+  resolve_tac reflps THEN'
+  rtac conjI THEN' rtac allI THEN' rtac allI THEN'
+  resolve_tac symps THEN'
+  rtac @{thm transpI} THEN' resolve_tac transps
+*}
+
+ML {*
+fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
+let
+  val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
+  val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
+  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
+  fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
+  val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
+  val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
+  val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
+  val symps = HOLogic.conj_elims symp
+  val transps = HOLogic.conj_elims transp
+  fun equivp alpha =
+    let
+      val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
+      val goal = @{term Trueprop} $ (equivp $ alpha)
+      fun tac _ = equivp_tac reflps symps transps 1
+    in
+      Goal.prove ctxt [] [] goal tac
+    end
+in
+  map equivp alphas
+end
+*}
+
+lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
+by auto
+
+ML {*
+fun supports_tac perm =
+  simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
+    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
+    asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
+      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
+      supp_fset_to_set supp_fmap_atom}))
+*}
+
+ML {*
+fun mk_supp ty x =
+  Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
+*}
+
+ML {*
+fun mk_supports_eq thy cnstr =
+let
+  val (tys, ty) = (strip_type o fastype_of) cnstr
+  val names = Datatype_Prop.make_tnames tys
+  val frees = map Free (names ~~ tys)
+  val rhs = list_comb (cnstr, frees)
+
+  fun mk_supp_arg (x, ty) =
+    if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
+    if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else
+    if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)
+    else mk_supp ty x
+  val lhss = map mk_supp_arg (frees ~~ tys)
+  val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
+  val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
+in
+  (names, eq)
+end
+*}
+
+ML {*
+fun prove_supports ctxt perms cnst =
+let
+  val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
+in
+  Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
+end
+*}
+
+ML {*
+fun mk_fs tys =
+let
+  val names = Datatype_Prop.make_tnames tys
+  val frees = map Free (names ~~ tys)
+  val supps = map2 mk_supp tys frees
+  val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps
+in
+  (names, HOLogic.mk_Trueprop (mk_conjl fin_supps))
+end
+*}
+
+ML {*
+fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
+  rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
+    supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
+*}
+
+ML {*
+fun prove_fs ctxt induct supports tys =
+let
+  val (names, eq) = mk_fs tys
+in
+  Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)
+end
+*}
+
+ML {*
+fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;
+
+fun mk_supp_neq arg (fv, alpha) =
+let
+  val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
+  val ty = fastype_of arg;
+  val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
+  val finite = @{term "finite :: atom set \<Rightarrow> bool"}
+  val rhs = collect $ Abs ("a", @{typ atom},
+    HOLogic.mk_not (finite $
+      (collect $ Abs ("b", @{typ atom},
+        HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))
+in
+  HOLogic.mk_eq (fv $ arg, rhs)
+end;
+
+fun supp_eq fv_alphas_lst =
+let
+  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (fv_ts, _) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) fv_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val args = map Free (names ~~ tys);
+  fun supp_eq_arg ((fv, arg), l) =
+    mk_conjl
+      ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::
+       (map (mk_supp_neq arg) l))
+  val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))
+in
+  (names, HOLogic.mk_Trueprop eqs)
+end
+*}
+
+ML {*
+fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =
+if length fv_ts_bn < length alpha_ts_bn then
+  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])
+else let
+  val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);
+  fun filter_fn i (x, j) = if j = i then SOME x else NONE;
+  val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;
+  val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;
+in
+  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all
+end
+*}
+
+(* TODO: this is a hack, it assumes that only one type of Abs's is present
+   in the type and chooses this supp_abs. Additionally single atoms are
+   treated properly. *)
+ML {*
+fun choose_alpha_abs eqiff =
+let
+  fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
+  val terms = map prop_of eqiff;
+  fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
+  val no =
+    if check @{const_name alpha_lst} then 2 else
+    if check @{const_name alpha_res} then 1 else
+    if check @{const_name alpha_gen} then 0 else
+    error "Failure choosing supp_abs"
+in
+  nth @{thms supp_abs[symmetric]} no
+end
+*}
+lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
+by (rule supp_abs(1))
+
+lemma supp_abs_sum:
+  "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+  "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
+  "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
+  apply (simp_all add: supp_abs supp_Pair)
+  apply blast+
+  done
+
+
+ML {*
+fun supp_eq_tac ind fv perm eqiff ctxt =
+  rel_indtac ind THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
+*}
+
+
+
+ML {*
+fun build_eqvt_gl pi frees fnctn ctxt =
+let
+  val typ = domain_type (fastype_of fnctn);
+  val arg = the (AList.lookup (op=) frees typ);
+in
+  ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
+end
+*}
+
+ML {*
+fun prove_eqvt tys ind simps funs ctxt =
+let
+  val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
+  val pi = Free (pi, @{typ perm});
+  val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))
+  val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
+  val ths = Variable.export ctxt' ctxt ths_loc
+  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
+in
+  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
+end
+*}
+
+end
diff -r 16653e702d89 -r 4650d428b1b5 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Apr 14 13:21:11 2010 +0200
+++ b/Nominal/Fv.thy	Wed Apr 14 13:21:38 2010 +0200
@@ -287,7 +287,6 @@
 *}
 
 (* We assume no bindings in the type on which bn is defined *)
-(* TODO: currently works only with current fv_bn function *)
 ML {*
 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) =
 let
@@ -416,7 +415,6 @@
   Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x
 *}
 
-(* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
 let
@@ -470,7 +468,7 @@
             if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
             if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else
             if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else
-            (* TODO we do not know what to do with non-atomizable things *)
+            (* TODO goes the code for preiously defined nominal datatypes *)
             @{term "{} :: atom set"}
         | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i)
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
@@ -490,7 +488,7 @@
                 if ((is_atom thy) o fastype_of) x then mk_single_atom x else
                 if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else
                 if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else
-                (* TODO we do not know what to do with non-atomizable things *)
+                (* TODO goes the code for preiously defined nominal datatypes *)
                 @{term "{} :: atom set"};
               (* If i = j then we generate it only once *)
               val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs;
@@ -607,368 +605,4 @@
 end
 *}
 
-
-
-ML {*
-fun build_alpha_sym_trans_gl alphas (x, y, z) =
-let
-  fun build_alpha alpha =
-    let
-      val ty = domain_type (fastype_of alpha);
-      val var = Free(x, ty);
-      val var2 = Free(y, ty);
-      val var3 = Free(z, ty);
-      val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
-      val transp = HOLogic.mk_imp (alpha $ var $ var2,
-        HOLogic.mk_all (z, ty,
-          HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
-    in
-      (symp, transp)
-    end;
-  val eqs = map build_alpha alphas
-  val (sym_eqs, trans_eqs) = split_list eqs
-  fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
-in
-  (conj sym_eqs, conj trans_eqs)
 end
-*}
-
-ML {*
-fun build_alpha_refl_gl fv_alphas_lst alphas =
-let
-  val (fvs_alphas, _) = split_list fv_alphas_lst;
-  val (_, alpha_ts) = split_list fvs_alphas;
-  val tys = map (domain_type o fastype_of) alpha_ts;
-  val names = Datatype_Prop.make_tnames tys;
-  val args = map Free (names ~~ tys);
-  fun find_alphas ty x =
-    domain_type (fastype_of x) = ty;
-  fun refl_eq_arg (ty, arg) =
-    let
-      val rel_alphas = filter (find_alphas ty) alphas;
-    in
-      map (fn x => x $ arg $ arg) rel_alphas
-    end;
-  (* Flattening loses the induction structure *)
-  val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))
-in
-  (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
-end
-*}
-
-ML {*
-fun reflp_tac induct eq_iff =
-  rtac induct THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
-  split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
-  THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
-     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
-       add_0_left supp_zero_perm Int_empty_left split_conv})
-*}
-
-ML {*
-fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
-let
-  val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
-  val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
-in
-  HOLogic.conj_elims refl_conj
-end
-*}
-
-lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="-pi" in exI)
-by auto
-
-ML {*
-fun symp_tac induct inj eqvt ctxt =
-  rel_indtac induct THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
-  THEN_ALL_NEW
-  REPEAT o etac @{thm exi_neg}
-  THEN_ALL_NEW
-  split_conj_tac THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
-  TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW
-  (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
-*}
-
-
-lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
-apply (erule exE)+
-apply (rule_tac x="pia + pi" in exI)
-by auto
-
-
-ML {*
-fun eetac rule = 
-  Subgoal.FOCUS_PARAMS (fn focus =>
-    let
-      val concl = #concl focus
-      val prems = Logic.strip_imp_prems (term_of concl)
-      val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
-      val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
-      val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
-    in
-      (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
-    end
-  )
-*}
-
-ML {*
-fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
-  rel_indtac induct THEN_ALL_NEW
-  (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
-  split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
-  THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
-  THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
-  TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW
-  (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
-*}
-
-lemma transpI:
-  "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
-  unfolding transp_def
-  by blast
-
-ML {*
-fun equivp_tac reflps symps transps =
-  (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
-  simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
-  THEN' rtac conjI THEN' rtac allI THEN'
-  resolve_tac reflps THEN'
-  rtac conjI THEN' rtac allI THEN' rtac allI THEN'
-  resolve_tac symps THEN'
-  rtac @{thm transpI} THEN' resolve_tac transps
-*}
-
-ML {*
-fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
-let
-  val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
-  val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
-  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
-  fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
-  val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
-  val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
-  val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
-  val symps = HOLogic.conj_elims symp
-  val transps = HOLogic.conj_elims transp
-  fun equivp alpha =
-    let
-      val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
-      val goal = @{term Trueprop} $ (equivp $ alpha)
-      fun tac _ = equivp_tac reflps symps transps 1
-    in
-      Goal.prove ctxt [] [] goal tac
-    end
-in
-  map equivp alphas
-end
-*}
-
-lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
-by auto
-
-ML {*
-fun supports_tac perm =
-  simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
-    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
-    asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
-      swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
-      supp_fset_to_set supp_fmap_atom}))
-*}
-
-ML {*
-fun mk_supp ty x =
-  Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
-*}
-
-ML {*
-fun mk_supports_eq thy cnstr =
-let
-  val (tys, ty) = (strip_type o fastype_of) cnstr
-  val names = Datatype_Prop.make_tnames tys
-  val frees = map Free (names ~~ tys)
-  val rhs = list_comb (cnstr, frees)
-
-  fun mk_supp_arg (x, ty) =
-    if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
-    if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else
-    if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)
-    else mk_supp ty x
-  val lhss = map mk_supp_arg (frees ~~ tys)
-  val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
-  val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
-in
-  (names, eq)
-end
-*}
-
-ML {*
-fun prove_supports ctxt perms cnst =
-let
-  val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
-in
-  Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
-end
-*}
-
-ML {*
-fun mk_fs tys =
-let
-  val names = Datatype_Prop.make_tnames tys
-  val frees = map Free (names ~~ tys)
-  val supps = map2 mk_supp tys frees
-  val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps
-in
-  (names, HOLogic.mk_Trueprop (mk_conjl fin_supps))
-end
-*}
-
-ML {*
-fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
-  rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
-    supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
-*}
-
-ML {*
-fun prove_fs ctxt induct supports tys =
-let
-  val (names, eq) = mk_fs tys
-in
-  Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)
-end
-*}
-
-ML {*
-fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;
-
-fun mk_supp_neq arg (fv, alpha) =
-let
-  val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
-  val ty = fastype_of arg;
-  val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
-  val finite = @{term "finite :: atom set \<Rightarrow> bool"}
-  val rhs = collect $ Abs ("a", @{typ atom},
-    HOLogic.mk_not (finite $
-      (collect $ Abs ("b", @{typ atom},
-        HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))
-in
-  HOLogic.mk_eq (fv $ arg, rhs)
-end;
-
-fun supp_eq fv_alphas_lst =
-let
-  val (fvs_alphas, ls) = split_list fv_alphas_lst;
-  val (fv_ts, _) = split_list fvs_alphas;
-  val tys = map (domain_type o fastype_of) fv_ts;
-  val names = Datatype_Prop.make_tnames tys;
-  val args = map Free (names ~~ tys);
-  fun supp_eq_arg ((fv, arg), l) =
-    mk_conjl
-      ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::
-       (map (mk_supp_neq arg) l))
-  val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))
-in
-  (names, HOLogic.mk_Trueprop eqs)
-end
-*}
-
-ML {*
-fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =
-if length fv_ts_bn < length alpha_ts_bn then
-  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])
-else let
-  val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);
-  fun filter_fn i (x, j) = if j = i then SOME x else NONE;
-  val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;
-  val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;
-in
-  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all
-end
-*}
-
-(* TODO: this is a hack, it assumes that only one type of Abs's is present
-   in the type and chooses this supp_abs. Additionally single atoms are
-   treated properly. *)
-ML {*
-fun choose_alpha_abs eqiff =
-let
-  fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
-  val terms = map prop_of eqiff;
-  fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
-  val no =
-    if check @{const_name alpha_lst} then 2 else
-    if check @{const_name alpha_res} then 1 else
-    if check @{const_name alpha_gen} then 0 else
-    error "Failure choosing supp_abs"
-in
-  nth @{thms supp_abs[symmetric]} no
-end
-*}
-lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
-by (rule supp_abs(1))
-
-lemma supp_abs_sum:
-  "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
-  "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
-  "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
-  apply (simp_all add: supp_abs supp_Pair)
-  apply blast+
-  done
-
-
-ML {*
-fun supp_eq_tac ind fv perm eqiff ctxt =
-  rel_indtac ind THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW
-  simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
-*}
-
-
-
-ML {*
-fun build_eqvt_gl pi frees fnctn ctxt =
-let
-  val typ = domain_type (fastype_of fnctn);
-  val arg = the (AList.lookup (op=) frees typ);
-in
-  ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
-end
-*}
-
-ML {*
-fun prove_eqvt tys ind simps funs ctxt =
-let
-  val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
-  val pi = Free (pi, @{typ perm});
-  val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))
-  val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
-  val ths = Variable.export ctxt' ctxt ths_loc
-  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
-in
-  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
-end
-*}
-
-end
diff -r 16653e702d89 -r 4650d428b1b5 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Wed Apr 14 13:21:11 2010 +0200
+++ b/Nominal/Lift.thy	Wed Apr 14 13:21:38 2010 +0200
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal_General/Nominal2_Supp" 
-        "Abs" "Perm" "Fv" "Rsp"
+        "Abs" "Perm" "Equivp" "Rsp"
 begin
 
 
diff -r 16653e702d89 -r 4650d428b1b5 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Apr 14 13:21:11 2010 +0200
+++ b/Nominal/Parser.thy	Wed Apr 14 13:21:38 2010 +0200
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "Fv" "Rsp" "Lift"
+        "Perm" "Equivp" "Rsp" "Lift"
 begin
 
 section{* Interface for nominal_datatype *}