# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274776999 -7200
# Node ID 9b566c5dc1f54f7a69bc487384a30edb0a0a0c1a
# Parent  5054f170024e4842a9e9b98b5178c0e92fe6ed67
overlapping deep binders proof

diff -r 5054f170024e -r 9b566c5dc1f5 Nominal/Ex/Ex2.thy
--- a/Nominal/Ex/Ex2.thy	Tue May 25 07:59:16 2010 +0200
+++ b/Nominal/Ex/Ex2.thy	Tue May 25 10:43:19 2010 +0200
@@ -10,23 +10,42 @@
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"          bind_set x in t
-| Let p::"pat" "trm" t::"trm"   bind_set "f p" in t
+| Let p::"pat" "trm" t::"trm"     bind "f p" in t
 and pat =
   PN
 | PS "name"
 | PD "name" "name"
 binder
-  f::"pat \<Rightarrow> atom set"
+  f::"pat \<Rightarrow> atom list"
 where
-  "f PN = {}"
-| "f (PD x y) = {atom x, atom y}"
-| "f (PS x) = {atom x}"
+  "f PN = []"
+| "f (PS x) = [atom x]"
+| "f (PD x y) = [atom x, atom y]"
+
 thm trm_pat.bn
 thm trm_pat.perm
 thm trm_pat.induct
 thm trm_pat.distinct
 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
+lemma lets_overlap1:
+  "atom a \<noteq> atom b \<Longrightarrow> Let (PD a a) x y \<noteq> Let (PD a b) x y"
+  by (simp add: trm_pat.eq_iff alphas)
+
+lemma lets_overlap2:
+  "atom a \<notin> supp y \<Longrightarrow> atom b \<notin> supp y \<Longrightarrow> Let (PD a a) x y = Let (PD b b) x y"
+  apply (simp add: trm_pat.eq_iff alphas trm_pat.supp)
+  apply (rule_tac x="(a\<leftrightarrow>b)" in exI)
+  apply (simp add: eqvts)
+  apply (rule conjI)
+  prefer 2
+  apply (rule Nominal2_Supp.supp_perm_eq)
+  apply (unfold fresh_star_def)
+  apply (unfold fresh_def)
+  apply (unfold flip_def)
+  apply (simp_all add: supp_swap)
+  apply auto
+  done
 
 end