# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269511282 -3600
# Node ID 06f44d498cef9d3d1c4b20435a1b376fc09dd2df
# Parent  0b47b699afe01d0f9bc5d581c316a0450d831fa5
Only let substitution is left.

diff -r 0b47b699afe0 -r 06f44d498cef Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Thu Mar 25 10:44:14 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 11:01:22 2010 +0100
@@ -38,6 +38,13 @@
   "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)"
   sorry
 
+lemma permute_bn_zero:
+  "permute_bn 0 a = a"
+  apply(induct a rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:test eqvts)
+  done
+
 lemma permute_bn_add:
   "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
   oops
@@ -46,6 +53,19 @@
   "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
   sorry
 
+lemma perm_bn:
+  "p \<bullet> bn l = bn(permute_bn p l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:test eqvts)
+  done
+
+lemma fin_bn:
+  "finite (bn l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(simp_all add:test eqvts)
+  done
+
 lemma 
   fixes t::trm
   and   l::lts
@@ -59,7 +79,7 @@
   shows "P1 c t" and "P2 c l"
 proof -
   have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
-       "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
+       b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
     apply(induct rule: trm_lts.inducts)
     apply(simp)
     apply(rule a1)
@@ -85,32 +105,37 @@
     apply(simp add: fresh_def)
     apply(simp add: trm_lts.fv[simplified trm_lts.supp])
     apply(simp)
-    apply(subgoal_tac "\<exists>q. (bn (permute_bn q (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
+    apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
     apply(erule exE)
     apply(erule conjE)
     apply(subst Lt_subst)
     apply assumption
     apply(rule a4)
+    apply(simp add:perm_bn)
     apply assumption
     apply (simp add: fresh_star_def fresh_def)
     apply(rotate_tac 1)
     apply(drule_tac x="q + p" in meta_spec)
     apply(simp)
-    (*apply(rule at_set_avoiding2)
+    apply(rule at_set_avoiding2)
+    apply(rule fin_bn)
     apply(simp add: finite_supp)
     apply(simp add: supp_Abs)
     apply(rule finite_Diff)
     apply(simp add: finite_supp)
-    apply(simp add: fresh_star_def fresh_def supp_Abs)*)
-    defer
+    apply(simp add: fresh_star_def fresh_def supp_Abs)
     apply(simp add: eqvts test)
     apply(rule a5)
     apply(simp add: test)
     apply(rule a6)
     apply simp
     apply simp
-    oops
-    
+    done
+  then have a: "P1 c (0 \<bullet> t)" by blast
+  have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+  then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+qed
+
 
 
 lemma lets_bla: