# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274110278 -7200
# Node ID e83493622e6ff81db31010bf05dfaf2476cac8e4
# Parent  f89773ab06853e3a233a184d15a72f96e0f786d2
alpha_alphabn for bindings in a type under bn.

diff -r f89773ab0685 -r e83493622e6f Nominal/Ex/Term8.thy
--- a/Nominal/Ex/Term8.thy	Mon May 17 16:29:33 2010 +0200
+++ b/Nominal/Ex/Term8.thy	Mon May 17 17:31:18 2010 +0200
@@ -6,9 +6,7 @@
 
 atom_decl name
 
-(* this should work but gives an error at the moment:
-   in alpha_bn_rsp proof.
-*)
+ML {* val _ = cheat_alpha_bn_rsp := true *}
 
 nominal_datatype foo =
   Foo0 "name"
@@ -22,6 +20,7 @@
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
+thm foo_bar.supp
 
 end
 
diff -r f89773ab0685 -r e83493622e6f Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Mon May 17 16:29:33 2010 +0200
+++ b/Nominal/Rsp.thy	Mon May 17 17:31:18 2010 +0200
@@ -145,10 +145,10 @@
 fun alpha_bn_rsp_tac simps res exhausts a ctxt =
   rtac allI THEN_ALL_NEW
   case_rules_tac ctxt a exhausts THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
   TRY o eresolve_tac res THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps simps);
+  asm_full_simp_tac (HOL_ss addsimps simps)
 *}
 
 
@@ -186,10 +186,15 @@
 end
 *}
 
+lemma exi_same: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q p) \<Longrightarrow> \<exists>pi. Q pi"
+  by auto
+
 ML {*
 fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt =
   prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind
-    (fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt
+    (fn _ => asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas})
+     THEN_ALL_NEW split_conj_tac THEN_ALL_NEW (TRY o etac @{thm exi_same})
+     THEN_ALL_NEW asm_full_simp_tac HOL_ss) alpha_bns ctxt
 *}
 
 ML {*