# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1290898529 0
# Node ID 3ebc7ecfb0dd47bc89db80e42ecb7f24e71e850a
# Parent  385add25dedffed47d63dafd88fd97c32059dfd1
disabled the Foo examples, because of heavy work

diff -r 385add25dedf -r 3ebc7ecfb0dd Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Fri Nov 26 22:43:26 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sat Nov 27 22:55:29 2010 +0000
@@ -148,9 +148,58 @@
 using assms
 apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric])
 apply(simp del: permute_Abs)
-apply(rule at_set_avoiding3)
-apply(simp_all only: finite_supp Abs_fresh_star finite_set)
-done
+sorry
+
+lemma strong_exhaust1:
+  fixes c::"'a::fs"
+  assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
+  and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  and     "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" 
+  and     "\<exists>assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P"
+  and     "\<exists>assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P"
+  and     "\<exists>assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P"
+  and     "\<exists>assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P"
+  shows "P"
+apply(rule_tac y="y" in foo.exhaust(1))
+apply(rule assms(1))
+apply(rule exI)
+apply(assumption)
+apply(rule assms(2))
+apply(rule exI)+
+apply(assumption)
+apply(rule assms(3))
+apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(3))
+apply(perm_simp)
+apply(assumption)
+apply(simp)
+apply(drule supp_perm_eq[symmetric])
+apply(perm_simp)
+apply(simp)
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: foo.fresh fresh_star_def)
+apply(drule Let1_rename_a)
+apply(erule exE)
+apply(erule conjE)
+apply(rule assms(4))
+apply(simp only: set_eqvt tt1)
+apply(assumption)
+(*
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
+apply(erule exE)
+apply(erule conjE)
+*)
+thm assms(5)
+apply(rule assms(5))
+prefer 2
+apply(clarify)
+unfolding foo.eq_iff
+apply
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
@@ -188,10 +237,24 @@
 apply(rule assms(4))
 apply(simp only: set_eqvt tt1)
 apply(assumption)
+(*
 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
+*)
+thm assms(5)
 apply(rule assms(5))
+prefer 2
+apply(clarify)
+unfolding foo.eq_iff
+apply(rule conjI)
+prefer 2
+apply(rule uu2)
+apply(simp only: tt2[symmetric])
+prefer 2
+apply(simp only: tt2[symmetric])
+
+apply(simp_all only:)[2]
 apply(simp add: set_eqvt)
 apply(simp add: tt2)
 apply(simp add: foo.eq_iff)
diff -r 385add25dedf -r 3ebc7ecfb0dd Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Fri Nov 26 22:43:26 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Sat Nov 27 22:55:29 2010 +0000
@@ -314,6 +314,82 @@
 apply(simp)
 done
 
+lemma abs_rename_set1:
+  fixes x::"'a::fs"
+  assumes "(p \<bullet> b) \<sharp> x" 
+  shows "\<exists>y. [{b}]set. x = [{p \<bullet> b}]set. y"
+apply(rule_tac x="(b \<rightleftharpoons> (p \<bullet> b)) \<bullet> x" in exI)
+apply(subst Abs_swap1[where a="b" and b="p \<bullet> b"])
+apply(simp)
+using assms
+apply(simp add: fresh_def)
+apply(perm_simp)
+apply(simp)
+done
+
+lemma yy:
+  assumes "finite bs"
+  and "bs \<inter> p \<bullet> bs = {}"
+  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
+using assms
+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)[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)
+defer
+apply(auto)[1]
+apply(erule conjE)+
+apply(drule sym)
+apply(auto)[1]
+apply(simp add: mem_permute_iff)
+apply(simp add: mem_permute_iff)
+apply(auto)[1]
+apply(simp add: supp_perm)
+apply(auto)[1]
+done
+
+lemma zz:
+  fixes bs::"atom list"
+  assumes "set bs \<inter> (set (p \<bullet> bs)) = {}"
+  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (set (p \<bullet> bs))"
+sorry
+
+lemma abs_rename_set2:
+  fixes x::"'a::fs"
+  assumes "(p \<bullet> bs) \<sharp>* x" "bs \<inter> p \<bullet> bs ={}" "finite bs"
+  shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
+using yy assms
+apply -
+apply(drule_tac x="bs" in meta_spec)
+apply(drule_tac x="p" in meta_spec)
+apply(auto)
+apply(rule_tac x="q \<bullet> x" in exI)
+apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x")
+apply(simp add: permute_Abs)
+apply(rule supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(simp add: fresh_star_def)
+apply(simp add: Abs_fresh_iff)
+apply(auto)
+done
+
 lemma abs_rename_list:
   fixes x::"'a::fs"
   assumes "b' \<sharp> x" "sort_of b = sort_of b'"
@@ -328,6 +404,26 @@
 apply(simp)
 done
 
+lemma abs_rename_list2:
+  fixes x::"'a::fs"
+  assumes "(set (p \<bullet> bs)) \<sharp>* x" "(set bs) \<inter> (set (p \<bullet> bs)) ={}" 
+  shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"
+using zz assms
+apply -
+apply(drule_tac x="bs" in meta_spec)
+apply(drule_tac x="p" in meta_spec)
+apply(auto simp add: set_eqvt)
+apply(rule_tac x="q \<bullet> x" in exI)
+apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x")
+apply(simp)
+apply(rule supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(simp add: fresh_star_def)
+apply(simp add: Abs_fresh_iff)
+apply(auto)
+done
+
+
 lemma test3:
   fixes c::"'a::fs"
   assumes a: "y = Let2 x1 x2 trm1 trm2"
@@ -338,62 +434,30 @@
 apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)")
 apply(erule exE)
 apply(perm_simp)
+apply(simp only: foo.eq_iff)
 apply(drule_tac x="q \<bullet> x1" in spec)
 apply(drule_tac x="q \<bullet> x2" in spec)
-apply(simp only: foo.eq_iff)
 apply(simp)
 apply(erule mp)
 apply(rule conjI)
 apply(simp add: fresh_star_prod)
 apply(rule conjI)
-prefer 2
-apply(rule abs_rename_list)
-apply(simp add: fresh_star_prod)
-apply(simp add: fresh_star_def)
-apply(simp)
-apply(case_tac "x1=x2")
-apply(simp)
-apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])
-apply(simp)
-apply(simp add: fresh_star_def)
-apply(simp add: fresh_def supp_Pair)
-apply(simp)
-apply(rule exI)
-apply(rule refl)
-apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])
-apply(simp)
-apply(simp add: fresh_star_def)
-apply(simp add: fresh_def supp_Pair)
-apply(simp)
-apply(simp add: flip_def[symmetric] atom_eqvt)
-apply(subgoal_tac "q \<bullet> x2 \<noteq> x1")
-apply(simp)
-apply(subst Abs_swap2[where a="atom x1" and b="atom (q \<bullet> x1)"])
-apply(simp)
-apply(subgoal_tac " atom (q \<bullet> x1) \<notin> supp ((x2 \<leftrightarrow> q \<bullet> x2) \<bullet> trm1)")
-apply(simp add: fresh_star_def)
-apply(simp add: fresh_star_def)
-apply(simp add: fresh_def supp_Pair)
-apply(erule conjE)+
-apply(rule_tac p="(x2 \<leftrightarrow> q \<bullet> x2)" in permute_boolE)
-apply(simp add: mem_eqvt Not_eqvt atom_eqvt supp_eqvt)
-apply(subgoal_tac "q \<bullet> x2 \<noteq> q \<bullet> x1")
-apply(subgoal_tac "x2 \<noteq> q \<bullet> x1")
-apply(simp)
-apply(simp add: supp_at_base)
-apply(simp)
-apply(simp)
-apply(rule exI)
-apply(rule refl)
-apply(simp add: fresh_star_def)
-apply(simp add: fresh_def supp_Pair)
-apply(simp add: supp_at_base)
-apply(rule at_set_avoiding3[where x="()", simplified])
-apply(simp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: fresh_star_def fresh_Unit)
-done
+apply(simp add: atom_eqvt[symmetric])
+apply(subst (2) permute_list.simps(1)[where p="q", symmetric])
+apply(subst permute_list.simps(2)[symmetric])
+apply(subst permute_list.simps(2)[symmetric])
+apply(rule abs_rename_list2)
+apply(simp add: atom_eqvt fresh_star_prod)
+apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
+apply(simp add: atom_eqvt[symmetric])
+apply(subst (2) permute_list.simps(1)[where p="q", symmetric])
+apply(subst permute_list.simps(2)[symmetric])
+apply(rule abs_rename_list2)
+apply(simp add: atom_eqvt fresh_star_prod)
+apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
+apply(simp add: atom_eqvt[symmetric])
+apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base)
+sorry
 
 lemma test4:
   fixes c::"'a::fs"
diff -r 385add25dedf -r 3ebc7ecfb0dd Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri Nov 26 22:43:26 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Sat Nov 27 22:55:29 2010 +0000
@@ -1583,9 +1583,15 @@
   assumes "finite xs"
   and     "finite (supp c)" "finite (supp x)"
   and     "xs \<sharp>* x"
-  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> x = p \<bullet> x"
-using at_set_avoiding2[OF assms]
-by (auto simp add: supp_perm_eq)
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p \<subseteq> xs \<union> (p \<bullet> xs)"
+using assms
+apply(erule_tac c="(c, x)" in at_set_avoiding)
+apply(simp add: supp_Pair)
+apply(rule_tac x="p" in exI)
+apply(simp add: fresh_star_prod)
+apply(rule fresh_star_supp_conv)
+apply(auto simp add: fresh_star_def)
+done
 
 
 lemma at_set_avoiding2_atom:
diff -r 385add25dedf -r 3ebc7ecfb0dd Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Fri Nov 26 22:43:26 2010 +0000
+++ b/Nominal/ROOT.ML	Sat Nov 27 22:55:29 2010 +0000
@@ -22,7 +22,7 @@
     "Ex/SystemFOmega",
     "Ex/TypeSchemes",
     "Ex/TypeVarsTest",
-    "Ex/Foo1",
-    "Ex/Foo2",
+    (*"Ex/Foo1",
+    "Ex/Foo2",*)
     "Ex/CoreHaskell"
     ];