--- a/Nominal/Test.thy	Mon Mar 15 08:39:23 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 17:51:35 2010 +0100
@@ -6,9 +6,11 @@
 
 atom_decl name
 
+(*
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
+| LAM x::"name" t::"lam" bind x in t
 | LET bp::"bp" t::"lam"   bind "bi bp" in t
 and bp =
   BP "name" "lam"
@@ -16,6 +18,19 @@
   bi::"bp \<Rightarrow> atom set"
 where
   "bi (BP x t) = {atom x}"
+*)
+
+nominal_datatype lam =
+  VAR "name"
+| APP "lam" "lam"
+| LAM x::"name" t::"lam" bind x in t
+| LET bp::"bp" t::"lam"   bind "bi bp" in t
+and bp =
+  BP "name"
+binder
+  bi::"bp \<Rightarrow> atom set"
+where
+  "bi (BP x) = {atom x}"
 
 thm lam_bp_fv
 thm lam_bp_inject
@@ -43,6 +58,21 @@
 apply(simp add: eqvts)
 done
 
+term alpha_bi
+
+lemma alpha_bi:
+  shows "alpha_bi pi b b' = True"
+apply(induct b rule: lam_bp_inducts(2))
+sorry
+
+lemma fv_bi:
+  shows "fv_bi b = {}"
+apply(induct b rule: lam_bp_inducts(2))
+apply(auto)[1]
+apply(simp_all)
+apply(simp add: lam_bp_fv)
+done
+
 lemma supp_fv:
   "supp t = fv_lam t" and 
   "supp b = fv_bp b"
@@ -62,31 +92,57 @@
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
+(* LAM case *)
+apply(rule_tac t="supp (LAM name lam_raw)" and s="supp (Abs {atom name} lam_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lam_bp_perm)
+apply(simp only: permute_ABS)
+apply(simp only: lam_bp_inject)
+apply(simp only: Abs_eq_iff)
+apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(simp only: supp_Abs)
 (* 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)
+(*apply(simp)*)
 (* LET case *)
-apply(simp only: supp_def)
+apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs_tst bi bp_raw lam_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
+apply(simp only: permute_ABS_tst)
 apply(simp only: lam_bp_inject)
+apply(simp only: eqvts_raw)
+apply(simp only: Abs_tst_eq_iff)
+apply(simp only: alpha_bi)
 apply(simp only: alpha_gen)
-
-thm alpha_gen
-thm lam_bp_fv
-thm lam_bp_inject
-oops
-
-
+apply(simp only: alpha_tst) 
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+defer (* hacking *)
+apply(simp add: supp_Abs_tst)
+apply(simp add: fv_bi)
+apply(rule Collect_cong)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(rule Collect_cong)
+apply(blast)
+done
 
 text {* example 2 *}