--- a/Nominal/Equivp.thy	Wed Oct 13 22:55:58 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,185 +0,0 @@
-theory Equivp
-imports "Abs" "Perm" "Tacs" "Rsp"
-begin
-
-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 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 $ fold_union lhss $ rhs)
-in
-  (names, eq)
-end
-*}
-
-ML {*
-fun prove_supports ctxt perms cnst =
-let
-  val (names, eq) = mk_supports_eq 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 = rtac 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 = member (op =) (map (exists_subterm f) ts) true;
-  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 =
-  rtac 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})
-*}
-
-
-
-
-
-end