# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1309268047 -3600
# Node ID b55098314f8326d6eeeb856bca17e41ac8beb96a
# Parent  b4bf3ff4bc91c159967ef3aa2544783be04827ed
fcb with explicit bn function

diff -r b4bf3ff4bc91 -r b55098314f83 Nominal/Ex/LetRecB.thy
--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:01:52 2011 +0100
+++ b/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:34:07 2011 +0100
@@ -32,12 +32,13 @@
   fixes as bs :: "atom list"
     and x y :: "'b :: fs"
     and c::"'c::fs"
-  assumes eq: "[as]lst. x = [bs]lst. y"
-  and fcb1: "(set as) \<sharp>* f as x c"
-  and fresh1: "set as \<sharp>* c"
-  and fresh2: "set bs \<sharp>* c"
+  assumes eq: "[bf as]lst. x = [bf bs]lst. y"
+  and fcb1: "(set (bf as)) \<sharp>* f as x c"
+  and fresh1: "set (bf as) \<sharp>* c"
+  and fresh2: "set (bf bs) \<sharp>* c"
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
+  and props: "eqvt bf" "inj bf"
   shows "f as x c = f bs y c"
 proof -
   have "supp (as, x, c) supports (f as x c)"
@@ -51,20 +52,20 @@
   then have fin2: "finite (supp (f bs y c))"
     by (auto intro: supports_finite simp add: finite_supp)
   obtain q::"perm" where 
-    fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and 
-    fr2: "supp q \<sharp>* Abs_lst as x" and 
-    inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)"
-    using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"]  
+    fr1: "(q \<bullet> (set (bf as))) \<sharp>* (x, c, f as x c, f bs y c)" and 
+    fr2: "supp q \<sharp>* ([bf as]lst. x)" and 
+    inc: "supp q \<subseteq> (set (bf as)) \<union> q \<bullet> (set (bf as))"
+    using at_set_avoiding3[where xs="set (bf as)" and c="(x, c, f as x c, f bs y c)" and x="[bf as]lst. x"]  
       fin1 fin2
     by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)
-  have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp
-  also have "\<dots> = Abs_lst as x"
+  have "[q \<bullet> (bf as)]lst. (q \<bullet> x) = q \<bullet> ([bf as]lst. x)" by simp
+  also have "\<dots> = [bf as]lst. x"
     by (simp only: fr2 perm_supp_eq)
-  finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp
+  finally have "[q \<bullet> (bf as)]lst. (q \<bullet> x) = [bf bs]lst. y" using eq by simp
   then obtain r::perm where 
     qq1: "q \<bullet> x = r \<bullet> y" and 
-    qq2: "q \<bullet> as = r \<bullet> bs" and 
-    qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs"
+    qq2: "q \<bullet> (bf as) = r \<bullet> (bf bs)" and 
+    qq3: "supp r \<subseteq> (q \<bullet> (set (bf as))) \<union> set (bf bs)"
     apply(drule_tac sym)
     apply(simp only: Abs_eq_iff2 alphas)
     apply(erule exE)
@@ -73,30 +74,35 @@
     apply(simp add: set_eqvt)
     apply(blast)
     done
-  have "(set as) \<sharp>* f as x c" by (rule fcb1)
-  then have "q \<bullet> ((set as) \<sharp>* f as x c)"
+  have qq4: "q \<bullet> as = r \<bullet> bs" using qq2 props unfolding eqvt_def inj_on_def
+    apply(perm_simp)
+    apply(simp)
+    done
+  have "(set (bf as)) \<sharp>* f as x c" by (rule fcb1)
+  then have "q \<bullet> ((set (bf as)) \<sharp>* f as x c)"
     by (simp add: permute_bool_def)
-  then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
+  then have "set (q \<bullet> (bf as)) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
     apply(simp add: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm1)
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
     done
-  then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
-  then have "r \<bullet> ((set bs) \<sharp>* f bs y c)"
+  then have "set (r \<bullet> (bf bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 qq4
+    by simp
+  then have "r \<bullet> ((set (bf bs)) \<sharp>* f bs y c)"
     apply(simp add: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
     done
-  then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def)
+  then have fcb2: "(set (bf bs)) \<sharp>* f bs y c" by (simp add: permute_bool_def)
   have "f as x c = q \<bullet> (f as x c)"
     apply(rule perm_supp_eq[symmetric])
     using inc fcb1 fr1 by (auto simp add: fresh_star_def)
   also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" 
     apply(rule perm1)
     using inc fresh1 fr1 by (auto simp add: fresh_star_def)
-  also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
+  also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq4 by simp
   also have "\<dots> = r \<bullet> (f bs y c)"
     apply(rule perm2[symmetric])
     using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)
@@ -133,13 +139,13 @@
   apply (simp_all add: fresh_star_def pure_fresh)[3]
   apply (simp add: eqvt_at_def)
   apply (simp add: eqvt_at_def)
+  apply(simp add: eqvt_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: inj_on_def)
   --"HERE"
-  thm  Abs_lst_fcb2
-  apply(rule Abs_lst_fcb2)
-     --" does not fit the assumption "
-
   apply (drule_tac c="()" in Abs_lst_fcb2)
-  prefer 6
+  prefer 8
   apply(assumption)
   apply (drule_tac c="()" in Abs_lst_fcb2)
   apply (simp add: Abs_eq_iff2)