--- a/Nominal/Ex/LetPat.thy	Sat Dec 17 17:03:01 2011 +0000
+++ b/Nominal/Ex/LetPat.thy	Sat Dec 17 17:08:47 2011 +0000
@@ -7,96 +7,28 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"       binds x in t
-| Let p::"pat" "trm" t::"trm"  binds "bn p" in t
+| Lam x::"name" t::"trm"       binds (set) x in t
+| Let p::"pat" "trm" t::"trm"  binds (set) "f p" in t
 and pat =
-  PNil
-| PVar "name"
-| PTup "pat" "pat"
+  PN
+| PS "name"
+| PD "name" "name"
 binder
-  bn::"pat \<Rightarrow> atom list"
+  f::"pat \<Rightarrow> atom set"
 where
-  "bn PNil = []"
-| "bn (PVar x) = [atom x]"
-| "bn (PTup p1 p2) = bn p1 @ bn p2"
+  "f PN = {}"
+| "f (PD x y) = {atom x, atom y}"
+| "f (PS x) = {atom x}"
 
-thm trm_pat.eq_iff
 thm trm_pat.distinct
 thm trm_pat.induct
-thm trm_pat.strong_induct[no_vars]
 thm trm_pat.exhaust
-thm trm_pat.strong_exhaust[no_vars]
 thm trm_pat.fv_defs
 thm trm_pat.bn_defs
 thm trm_pat.perm_simps
 thm trm_pat.eq_iff
 thm trm_pat.fv_bn_eqvt
-thm trm_pat.size
-
-(* Nominal_Abs test *)
-
-lemma alpha_res_alpha_set:
-  "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> 
-  (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
-  using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
-
-
-lemma
-  fixes x::"'a::fs"
-  assumes "(supp x - as) \<sharp>* p"
-      and "p \<bullet> x = y"
-      and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y"
-  shows "(as, x) \<approx>res (op =) supp p (bs, y)"
-  using assms
-  unfolding alpha_res_alpha_set
-  unfolding alphas
-  apply simp
-  apply rule
-  apply (rule trans)
-  apply (rule supp_perm_eq[symmetric, of _ p])
-  apply(subst supp_finite_atom_set)
-  apply (metis finite_Diff finite_supp)
-  apply (simp add: fresh_star_def)
-  apply blast
-  apply(perm_simp)
-  apply(simp)
-  done
-
-lemma
-  fixes x::"'a::fs"
-  assumes "(supp x - as) \<sharp>* p"
-      and "p \<bullet> x = y"
-      and "p \<bullet> as = bs"
-  shows "(as, x) \<approx>set (op =) supp p (bs, y)"
-  using assms
-  unfolding alphas
-  apply simp
-  apply (rule trans)
-  apply (rule supp_perm_eq[symmetric, of _ p])
-  apply(subst supp_finite_atom_set)
-  apply (metis finite_Diff finite_supp)
-  apply(simp)
-  apply(perm_simp)
-  apply(simp)
-  done
-
-lemma
-  fixes x::"'a::fs"
-  assumes "(supp x - set as) \<sharp>* p"
-      and "p \<bullet> x = y"
-      and "p \<bullet> as = bs"
-  shows "(as, x) \<approx>lst (op =) supp p (bs, y)"
-  using assms
-  unfolding alphas
-  apply simp
-  apply (rule trans)
-  apply (rule supp_perm_eq[symmetric, of _ p])
-  apply(subst supp_finite_atom_set)
-  apply (metis finite_Diff finite_supp)
-  apply(simp)
-  apply(perm_simp)
-  apply(simp)
-  done
+thm trm_pat.size_eqvt
 
 
 end