# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269071767 -3600
# Node ID 604c4cffc5b9b1d7b45c269db56ec2b9ff89c4e5
# Parent  d375804ce6bada279282777390837ff25b13a6e1
Build alpha-->alphabn implications

diff -r d375804ce6ba -r 604c4cffc5b9 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 20 08:04:59 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 20 08:56:07 2010 +0100
@@ -717,6 +717,36 @@
 end
 *}
 
+ML {*
+fun build_alpha_alphabn fv_alphas_lst inducts eq_iff ctxt  =
+let
+  val (fvs_alphas, ls) = 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 names2 = Name.variant_list names names;
+  val args = map Free (names ~~ tys);
+  val args2 = map Free (names2 ~~ tys);
+  fun alpha_alphabn ((alpha, (arg, arg2)), (no, l)) =
+    if l = [] then [] else
+    let
+      val alpha_bns = map snd l;
+      val lhs = alpha $ arg $ arg2;
+      val rhs = foldr1 HOLogic.mk_conj (map (fn x => x $ arg $ arg2) alpha_bns);
+      val gl = Logic.mk_implies (HOLogic.mk_Trueprop lhs, HOLogic.mk_Trueprop rhs);
+      fun tac _ = (etac (nth inducts no) THEN_ALL_NEW TRY o rtac @{thm TrueI}
+        THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps eq_iff)) 1
+      val th = Goal.prove ctxt (names @ names2) [] gl tac;
+    in
+      Project_Rule.projects ctxt (1 upto length l) th
+    end;
+  val eqs = map alpha_alphabn ((alpha_ts ~~ (args ~~ args2)) ~~ ((0 upto (length ls - 1)) ~~ ls));
+in
+  flat eqs
+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)