--- a/Nominal/Ex/LetPat.thy	Wed Sep 21 17:16:11 2011 +0900
+++ b/Nominal/Ex/LetPat.thy	Wed Sep 21 10:23:06 2011 +0200
@@ -7,28 +7,96 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"       binds (set) x in t
-| Let p::"pat" "trm" t::"trm"  binds (set) "f p" in t
+| Lam x::"name" t::"trm"       binds x in t
+| Let p::"pat" "trm" t::"trm"  binds "bn p" in t
 and pat =
-  PN
-| PS "name"
-| PD "name" "name"
+  PNil
+| PVar "name"
+| PTup "pat" "pat"
 binder
-  f::"pat \<Rightarrow> atom set"
+  bn::"pat \<Rightarrow> atom list"
 where
-  "f PN = {}"
-| "f (PD x y) = {atom x, atom y}"
-| "f (PS x) = {atom x}"
+  "bn PNil = []"
+| "bn (PVar x) = [atom x]"
+| "bn (PTup p1 p2) = bn p1 @ bn p2"
 
+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_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
 
 
 end