--- a/Nominal/Test.thy	Fri Mar 12 17:42:31 2010 +0100
+++ b/Nominal/Test.thy	Sat Mar 13 13:49:15 2010 +0100
@@ -26,11 +26,61 @@
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
 
 term "supp (x :: lam)"
+lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]
 
-(* compat should be
-compat (BP x t) pi (BP x' t')
-  \<equiv> alpha_trm t t' \<and> pi o x = x'
-*)
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+apply(auto)
+done
+
+lemma bi_eqvt:
+  shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
+sorry
+
+lemma supp_fv:
+  "supp t = fv_lam t" and 
+  "supp b = fv_bp b"
+apply(induct t and b rule: lam_bp_inducts)
+apply(simp_all add: lam_bp_fv)
+(* VAR case *)
+apply(simp only: supp_def)
+apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+(* APP case *)
+apply(simp only: supp_def)
+apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+(* LET case *)
+defer
+(* BP case *)
+apply(simp only: supp_def)
+apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+apply(simp)
+(* LET case *)
+apply(simp only: supp_def)
+apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp_inject)
+apply(simp only: alpha_gen)
+
+thm alpha_gen
+thm lam_bp_fv
+thm lam_bp_inject
+oops
+
+
 
 text {* example 2 *}