--- a/Nominal/Test.thy	Tue Mar 16 20:07:13 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 06:49:33 2010 +0100
@@ -109,8 +109,95 @@
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
+ML {* val _ = recursive := true *}
+
+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'"
+binder
+  bi'::"bp' \<Rightarrow> atom set"
+where
+  "bi' (BP' x t) = {atom x}"
+
+thm lam'_bp'_fv
+thm lam'_bp'_inject[no_vars]
+thm lam'_bp'_bn
+thm lam'_bp'_perm
+thm lam'_bp'_induct
+thm lam'_bp'_inducts
+thm lam'_bp'_distinct
+ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
+
+lemma supp_fv:
+  shows "supp t = fv_lam' t" 
+  and "supp bp = fv_bp' bp"
+apply(induct t and bp 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)
+(* 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 *)
+apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and 
+               s="supp (Abs (bi' bp'_raw) (bp'_raw, 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: eqvts)
+apply(simp only: Abs_eq_iff)
+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(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(rule ext)
+apply(rule sym)
+apply(subgoal_tac "fv_bp' = supp")
+apply(subgoal_tac "fv_lam' = supp")
+apply(simp)
+apply(rule trans)
+apply(rule alpha_abs_Pair[symmetric])
+apply(simp add: alpha_gen supp_Pair)
+oops
+
+thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+
+
 text {* example 2 *}
 
+ML {* val _ = recursive := false  *}
 nominal_datatype trm' =
   Var "name"
 | App "trm'" "trm'"
@@ -134,11 +221,82 @@
 thm trm'_pat'_induct
 thm trm'_pat'_distinct
 
-(* compat should be
-compat (PN) pi (PN) == True
-compat (PS x) pi (PS x') == pi o x = x'
-compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'
-*)
+lemma supp_fv_trm'_pat':
+  shows "supp t = fv_trm' t" 
+  and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
+apply(induct t and bp rule: trm'_pat'_inducts)
+apply(simp_all add: trm'_pat'_fv)
+(* VAR case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+(* APP case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: de_Morgan_conj)
+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 trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: trm'_pat'_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 *)
+apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" 
+           and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: eqvts)
+apply(simp only: Abs_eq_iff)
+apply(simp only: ex_simps)
+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: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(blast)
+apply(simp add: supp_Abs)
+apply(blast)
+(* PN case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp)
+(* PS case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+apply(simp)
+(* PD case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_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 add: supp_at_base)
+done
+
+thm trm'_pat'_fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
 
 nominal_datatype trm0 =
   Var0 "name"