diff -r 0f289a52edbe -r b136721eedb2 Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Tue Dec 07 14:27:39 2010 +0000
@@ -24,6 +24,8 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
+thm foo.bn_defs
+thm foo.permute_bn
 thm foo.perm_bn_alpha
 thm foo.perm_bn_simps
 thm foo.bn_finite
@@ -43,57 +45,61 @@
 thm foo.supp
 thm foo.fresh
 
-lemma tt1:
-  shows "(p \<bullet> bn as) = bn (permute_bn p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[5]
-apply(simp only: foo.perm_bn_simps foo.bn_defs)
-apply(perm_simp)
-apply(simp only:)
-apply(simp only: foo.perm_bn_simps foo.bn_defs)
-apply(perm_simp add: foo.fv_bn_eqvt)
-apply(simp only:)
-done
-
 text {*
   tests by cu
 *}
 
-lemma yy:
+lemma set_renaming_perm:
   assumes a: "p \<bullet> bs \<inter> bs = {}" 
   and     b: "finite bs"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
 using b a
-apply(induct)
-apply(simp add: permute_set_eq)
-apply(rule_tac x="0" in exI)
-apply(simp add: supp_perm)
-apply(perm_simp)
-apply(drule meta_mp)
-apply(auto simp add: fresh_star_def fresh_finite_insert)[1]
-apply(erule exE)
-apply(simp)
-apply(case_tac "q \<bullet> x = p \<bullet> x")
-apply(rule_tac x="q" in exI)
-apply(auto)[1]
-apply(rule_tac x="((q \<bullet> x) \<rightleftharpoons> (p \<bullet> x)) + q" in exI)
-apply(subgoal_tac "p \<bullet> x \<notin> p \<bullet> F")
-apply(subgoal_tac "q \<bullet> x \<notin> p \<bullet> F")
-apply(simp add: swap_set_not_in)
-apply(rule subset_trans)
-apply(rule supp_plus_perm)
-apply(simp)
-apply(rule conjI)
-apply(simp add: supp_swap)
-apply(simp add: supp_perm)
-apply(auto)[1]
-apply(auto)[1]
-apply(erule conjE)+
-apply(drule sym)
-apply(simp add: mem_permute_iff)
-apply(simp add: mem_permute_iff)
-done
-
+proof (induct)
+  case empty
+  have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
+    by (simp add: permute_set_eq supp_perm)
+  then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
+next
+  case (insert a bs)
+  then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" 
+    by (perm_simp) (auto)
+  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast 
+  { assume 1: "q \<bullet> a = p \<bullet> a"
+    have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)
+    moreover 
+    have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
+      using ** by (auto simp add: insert_eqvt)
+    ultimately 
+    have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+  }
+  moreover
+  { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"
+    def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
+    { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)
+      moreover 
+      have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)
+      ultimately 
+      have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def 
+        by (simp add: insert_eqvt  swap_set_not_in) 
+    }
+    moreover 
+    { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+	using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}`
+	by (auto simp add: supp_perm insert_eqvt)
+      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)
+      moreover
+      have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
+	using ** by (auto simp add: insert_eqvt)
+      ultimately 
+      have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
+        unfolding q'_def using supp_plus_perm by blast
+    }
+    ultimately 
+    have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+  }
+  ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+    by blast
+qed
 
 
 lemma Abs_rename_set:
@@ -103,7 +109,8 @@
   shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
 proof -
   from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   
-  with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  with set_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
   have "[bs]set. x =  q \<bullet> ([bs]set. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
@@ -124,7 +131,8 @@
   shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"
 proof -
   from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) 
-  with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  with set_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
   have "[bs]res. x =  q \<bullet> ([bs]res. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
@@ -138,54 +146,60 @@
   then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast
 qed
 
-lemma zz0:
-  assumes "p \<bullet> bs = q \<bullet> bs"
-  and a: "a \<in> set bs"
-  shows "p \<bullet> a = q \<bullet> a"
-using assms
-by (induct bs) (auto)
-
-lemma zz:
+lemma list_renaming_perm:
   fixes bs::"atom list"
-  assumes "(p \<bullet> (set bs)) \<inter> (set bs) = {}"
+  assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
-using assms
-apply(induct bs)
-apply(simp add: permute_set_eq)
-apply(rule_tac x="0" in exI)
-apply(simp add: supp_perm)
-apply(drule meta_mp)
-apply(perm_simp)
-apply(auto)[1]
-apply(erule exE)
-apply(simp)
-apply(case_tac "a \<in> set bs")
-apply(rule_tac x="q" in exI)
-apply(perm_simp)
-apply(auto dest: zz0)[1]
-apply(subgoal_tac "q \<bullet> a \<sharp> p \<bullet> bs")
-apply(subgoal_tac "p \<bullet> a \<sharp> p \<bullet> bs")
-apply(rule_tac x="((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" in exI)
-apply(simp add: swap_fresh_fresh)
-apply(rule subset_trans)
-apply(rule supp_plus_perm)
-apply(simp)
-apply(rule conjI)
-apply(simp add: supp_swap)
-apply(simp add: supp_perm)
-apply(perm_simp)
-apply(auto simp add: fresh_def supp_of_atom_list)[1]
-apply(perm_simp)
-apply(auto)[1]
-apply(simp add: fresh_permute_iff)
-apply(simp add: fresh_def supp_of_atom_list)
-apply(erule conjE)+
-apply(drule sym)
-apply(drule sym)
-apply(simp)
-apply(simp add: fresh_permute_iff)
-apply(auto simp add: fresh_def supp_of_atom_list)[1]
-done
+using a
+proof (induct bs)
+  case Nil
+  have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
+    by (simp add: permute_set_eq supp_perm)
+  then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
+next
+  case (Cons a bs)
+  then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" 
+    by (perm_simp) (auto)
+  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast 
+  { assume 1: "a \<in> set bs"
+    have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)
+    then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp 
+    moreover 
+    have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)
+    ultimately 
+    have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+  }
+  moreover
+  { assume 2: "a \<notin> set bs"
+    def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
+    { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] 
+	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
+      moreover 
+      have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` 
+	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
+      ultimately 
+      have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def 
+        by (simp add: swap_fresh_fresh) 
+    }
+    moreover 
+    { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+	using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}`
+	by (auto simp add: supp_perm insert_eqvt)
+      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)
+      moreover
+      have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
+	using ** by (auto simp add: insert_eqvt)
+      ultimately 
+      have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
+        unfolding q'_def using supp_plus_perm by blast
+    }
+    ultimately 
+    have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+  }
+  ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+    by blast
+qed
+
 
 lemma Abs_rename_list:
   fixes x::"'a::fs"
@@ -194,7 +208,8 @@
 proof -
   from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 
     by (simp add: fresh_star_Pair fresh_star_set)
-  with zz obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 
+  with list_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 
   have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
@@ -208,6 +223,23 @@
   then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast
 qed
 
+(*
+thm at_set_avoiding1[THEN exE]
+
+
+lemma Let1_rename:
+  fixes c::"'a::fs"
+  shows "\<exists>name' trm'. {atom name'} \<sharp>* c \<and>  Lam name trm = Lam name' trm'"
+apply(simp only: foo.eq_iff)
+apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE])
+apply(simp)
+apply(simp add: finite_supp)
+apply(perm_simp)
+apply(rule Abs_rename_list[THEN exE])
+apply(simp only: set_eqvt)
+apply
+sorry 
+*)
 
 lemma test6:
   fixes c::"'a::fs"
@@ -224,6 +256,14 @@
 apply(rule assms(2))
 apply(rule exI)+
 apply(assumption)
+(* lam case *)
+(*
+apply(rule Let1_rename)
+apply(rule assms(3))
+apply(assumption)
+apply(simp)
+*)
+
 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
 apply(erule exE)
 apply(insert Abs_rename_list)[1]
@@ -245,10 +285,10 @@
 apply(rule at_set_avoiding1)
 apply(simp)
 apply(simp add: finite_supp)
+(* let1 case *)
 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")
 apply(erule exE)
 apply(rule assms(4))
-apply(simp only:)
 apply(simp only: foo.eq_iff)
 apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
@@ -264,7 +304,7 @@
 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
 apply(erule exE)+
 apply(rule exI)+
-apply(perm_simp add: tt1)
+apply(perm_simp add: foo.permute_bn)
 apply(rule conjI)
 apply(simp add: fresh_star_Pair fresh_star_Un)
 apply(erule conjE)+
@@ -282,6 +322,7 @@
 apply(rule at_set_avoiding1)
 apply(simp)
 apply(simp add: finite_supp)
+(* let2 case *)
 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")
 apply(erule exE)
 apply(rule assms(5))
@@ -309,7 +350,7 @@
 apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1]
 apply(erule exE)+
 apply(rule exI)+
-apply(perm_simp add: tt1)
+apply(perm_simp add: foo.permute_bn)
 apply(rule conjI)
 prefer 2
 apply(rule conjI)