--- a/Nominal/Unused.thy	Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="pi \<bullet> pia" in exI)
-by auto
-
-ML {*
-fun alpha_eqvt_tac induct simps ctxt =
-  rtac induct THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
-  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps
-    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
-  (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
-    @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
-  THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
-*}
-
-ML {*
-fun build_alpha_eqvt alpha names =
-let
-  val pi = Free ("p", @{typ perm});
-  val (tys, _) = strip_type (fastype_of alpha)
-  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
-  val args = map Free (indnames ~~ tys);
-  val perm_args = map (fn x => mk_perm pi x) args
-in
-  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
-end
-*}
-
-ML {*
-fun build_alpha_eqvts funs tac ctxt =
-let
-  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
-  val thm = Goal.prove ctxt names [] gl tac
-in
-  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
-end
-*}
-
-(* Given [fv1, fv2, fv3]
-   produces %(x, y, z). fv1 x u fv2 y u fv3 z *)
-ML {*
-fun mk_compound_fv fvs =
-let
-  val nos = (length fvs - 1) downto 0;
-  val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);
-  val fvs_union = mk_union fvs_applied;
-  val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);
-  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
-in
-  fold fold_fun tys (Abs ("", tyh, fvs_union))
-end;
-*}
-
-(* Given [R1, R2, R3]
-   produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
-ML {*
-fun mk_compound_alpha Rs =
-let
-  val nos = (length Rs - 1) downto 0;
-  val nos2 = (2 * length Rs - 1) downto length Rs;
-  val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)
-    (Rs ~~ (nos2 ~~ nos));
-  val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;
-  val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);
-  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
-  val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
-in
-  fold fold_fun tys (Abs ("", tyh, abs_rhs))
-end;
-*}