# HG changeset patch # User Christian Urban # 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 \ T) \ infinite S \ infinite T" -apply(auto) -done + by simp lemma bi_eqvt: shows "(p \ (bi b)) = bi (p \ 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