# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1309114915 -32400
# Node ID eb322a3924618b9e7052ad7e3db97c1333ee77c1
# Parent  e26c6c728b9eaee55398a2aae9246d93a44d0f4a
equality of lst_binder and a few helper lemmas
[l]lst. T = [l]lst. S  <->  T = S

diff -r e26c6c728b9e -r eb322a392461 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Sun Jun 26 21:42:07 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Mon Jun 27 04:01:55 2011 +0900
@@ -160,6 +160,24 @@
   shows "f as x c = f bs y c"
 *)
 
+lemma supp_zero_perm_zero:
+  shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0"
+  by (metis supp_perm_singleton supp_zero_perm)
+
+lemma permute_atom_list_id:
+  shows "p \<bullet> l = l \<longleftrightarrow> supp p \<inter> set l = {}"
+  by (induct l) (auto simp add: supp_Nil supp_perm)
+
+lemma Abs_lst_binder_length:
+  shows "[xs]lst. T = [ys]lst. S \<Longrightarrow> length xs = length ys"
+  by (auto simp add: Abs_eq_iff alphas length_eqvt[symmetric] permute_pure)
+
+lemma Abs_lst_binder_eq:
+  shows "Abs_lst l T = Abs_lst l S \<longleftrightarrow> T = S"
+  by (rule, simp_all add: Abs_eq_iff2 alphas)
+     (metis fresh_star_zero inf_absorb1 permute_atom_list_id supp_perm_eq
+       supp_zero_perm_zero)
+
 nominal_primrec 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
 where