# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268638090 -3600
# Node ID bdd73f8bb63ba8bc35e1ea63003c900e42c3a99e
# Parent  61671de8a5450cdcee405a06a96c004cb9d303e6
added an eqvt-proof for bi

diff -r 61671de8a545 -r bdd73f8bb63b Nominal/Test.thy
--- a/Nominal/Test.thy	Mon Mar 15 06:11:35 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 08:28:10 2010 +0100
@@ -28,14 +28,20 @@
 term "supp (x :: lam)"
 lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]
 
+(* maybe should be added to Infinite.thy *)
 lemma infinite_Un:
   shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-apply(auto)
-done
+  by simp
 
 lemma bi_eqvt:
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-sorry
+apply(induct b rule: lam_bp_inducts(2))
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp add: lam_bp_bn lam_bp_perm)
+apply(simp add: eqvts)
+done
 
 lemma supp_fv:
   "supp t = fv_lam t" and