--- a/Nominal/Ex/Foo2.thy	Sun Dec 19 07:50:37 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Tue Dec 21 10:28:08 2010 +0000
@@ -27,6 +27,7 @@
 
 
 
+
 thm foo.bn_defs
 thm foo.permute_bn
 thm foo.perm_bn_alpha
@@ -49,28 +50,167 @@
 thm foo.supp
 thm foo.fresh
 
-(*
-lemma ex_prop:
-  shows "\<exists>n::nat. Suc n = n"
-sorry
+lemma at_set_avoiding5:
+  assumes "finite xs"
+  and     "finite (supp c)"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> xs"
+using assms
+apply(erule_tac c="c" in at_set_avoiding)
+apply(auto)
+done
+
 
-lemma test:
-  shows "True"
-apply -
-ML_prf {*
-  val (x, ctxt') = Obtain.result (K (
-  EVERY [print_tac "test", 
-         etac exE 1,
-         print_tac "end"])) 
-  @{thms ex_prop} @{context};
-  ProofContext.verbose := true;
-  ProofContext.pretty_context ctxt'
-  |> Pretty.block
-  |> Pretty.writeln
-*}
-*)
+lemma Abs_rename_lst3:
+  fixes x::"'a::fs"
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
+  shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs"
+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 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 **
+    unfolding fresh_star_Pair
+    unfolding Abs_fresh_star_iff
+    unfolding fresh_star_def
+    by auto
+  also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp
+  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .
+  then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs" 
+    using * ** by metis
+qed
 
 
+lemma
+  fixes c::"'a::fs"
+  assumes a:  "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
+  shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
+apply -
+apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
+  supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
+defer
+apply(rule at_set_avoiding5)
+apply(simp add: foo.bn_finite)
+apply(simp add: supp_Pair finite_supp)
+apply(erule exE)
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair)
+apply(erule conjE)+
+thm Abs_rename_lst
+apply(insert Abs_rename_lst)[1]
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="bn assg1" in meta_spec)
+apply(drule_tac x="trm1" in meta_spec)
+apply(insert Abs_rename_lst)[1]
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="bn assg2" in meta_spec)
+apply(drule_tac x="trm2" in meta_spec)
+apply(drule meta_mp)
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair fresh_star_Un)
+apply(drule meta_mp)
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair fresh_star_Un)
+apply(erule exE)+
+apply(rule a)
+apply(assumption)
+apply(simp only: foo.eq_iff)
+apply(perm_simp add: foo.permute_bn)
+apply(rule conjI)
+apply(rule refl)
+apply(rule conjI)
+apply(rule foo.perm_bn_alpha)
+apply(rule conjI)
+apply(perm_simp add: foo.permute_bn)
+apply(rule refl)
+apply(rule foo.perm_bn_alpha)
+done
+
+lemma
+  fixes c::"'a::fs"
+  assumes a:  "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
+  shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
+apply -
+apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
+  supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
+defer
+apply(rule at_set_avoiding5)
+apply(simp add: foo.bn_finite)
+apply(simp add: supp_Pair finite_supp)
+apply(erule exE)
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair)
+apply(erule conjE)+
+apply(insert Abs_rename_lst3)[1]
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="bn assg1" in meta_spec)
+apply(drule_tac x="trm1" in meta_spec)
+apply(insert Abs_rename_lst3)[1]
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="bn assg2" in meta_spec)
+apply(drule_tac x="trm2" in meta_spec)
+apply(drule meta_mp)
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair fresh_star_Un)
+apply(drule meta_mp)
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair fresh_star_Un)
+apply(erule exE)+
+apply(erule conjE)+
+apply(simp add: foo.permute_bn)
+apply(rule a)
+apply(assumption)
+apply(clarify)
+apply(simp (no_asm) only: foo.eq_iff)
+apply(rule conjI)
+apply(assumption)
+apply(rule conjI)
+apply(rule foo.perm_bn_alpha)
+apply(rule conjI)
+apply(assumption)
+apply(rule foo.perm_bn_alpha)
+done
+
+
+lemma
+  fixes c::"'a::fs"
+  assumes a:  "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
+  shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
+apply -
+apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
+  supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2))))")
+defer
+apply(rule at_set_avoiding5)
+apply(simp add: foo.bn_finite)
+apply(simp add: supp_Pair finite_supp)
+apply(erule exE)
+apply(simp add: fresh_star_Pair)
+apply(erule conjE)+
+apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt)
+apply(rule a)
+apply(assumption)
+apply(clarify)
+apply(simp (no_asm) only: foo.eq_iff)
+apply(rule conjI)
+apply(rule trans)
+apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(rule fresh_star_supp_conv)
+apply(simp (no_asm_use) add: fresh_star_def)
+apply(simp (no_asm_use) add: Abs_fresh_iff)[1]
+apply(rule ballI)
+apply(auto simp add: fresh_Pair)[1]
+apply(simp (no_asm_use) only: permute_Abs)
+apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt)
+apply(simp)
+apply(rule at_set_avoiding5)
+apply(simp add: multi_recs.bn_finite)
+apply(simp add: supp_Pair finite_supp)
+apply(rule finite_sets_supp)
+apply(simp add: multi_recs.bn_finite)
+done
 
 
 
@@ -112,14 +252,9 @@
 (* 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(perm_simp add: foo.permute_bn)
 apply(simp add: fresh_star_Pair)
 apply(erule conjE)+
-apply(assumption)
-apply(simp only:)
-apply(simp only: foo.eq_iff)
-(* *)
 apply(insert Abs_rename_lst)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg1" in meta_spec)
@@ -129,21 +264,22 @@
 apply(drule_tac x="bn assg2" in meta_spec)
 apply(drule_tac x="trm2" in meta_spec)
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair fresh_star_Un)
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair fresh_star_Un)
 apply(erule exE)+
-apply(perm_simp add: foo.permute_bn)
-apply(simp add: fresh_star_Pair)
-apply(erule conjE)+
 apply(rule assms(4))
 apply(assumption)
 apply(simp add: foo.eq_iff refl)
 apply(rule conjI)
+apply(perm_simp add: foo.permute_bn)
 apply(rule refl)
 apply(rule conjI)
 apply(rule foo.perm_bn_alpha)
 apply(rule conjI)
+apply(perm_simp add: foo.permute_bn)
 apply(rule refl)
 apply(rule foo.perm_bn_alpha)
 apply(rule at_set_avoiding1)