# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1253538143 -7200
# Node ID d9bd7e01a681579577235ffe0d605487fdc90bb7
# Parent  a45e8ec2b51ee24ae014da629839deb059a8ed9b
tuned some proofs

diff -r a45e8ec2b51e -r d9bd7e01a681 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Mon Sep 21 13:42:36 2009 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Mon Sep 21 15:02:23 2009 +0200
@@ -408,20 +408,7 @@
 
 declare trm.inject[simp del]
 
-lemma whn_eqvt[eqvt]:
-  fixes pi::"name prm"
-  assumes a: "t \<Down> t'"
-  shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')"
-using a
-apply(induct)
-apply(rule QAN_Reduce)
-apply(rule whr_def.eqvt)
-apply(assumption)+
-apply(rule QAN_Normal)
-apply(auto)
-apply(drule_tac pi="rev pi" in whr_def.eqvt)
-apply(perm_simp)
-done
+equivariance whn_def
 
 lemma red_unicity : 
   assumes a: "x \<leadsto> a" 
@@ -631,6 +618,7 @@
 apply (force)
 apply (rule ty_cases)
 done
+
 termination by lexicographic_order
 
 lemma logical_monotonicity:
@@ -968,7 +956,7 @@
   then show  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma(1) val by simp
 qed
 
-text {* We leave soundness as an exercise - like in the book :-) \\ 
+text {* We leave soundness as an exercise - just like Crary in the ATS book :-) \\ 
  @{prop[mode=IfThen] "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} \\
  @{prop "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} 
 *}
diff -r a45e8ec2b51e -r d9bd7e01a681 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Sep 21 13:42:36 2009 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Sep 21 15:02:23 2009 +0200
@@ -2623,74 +2623,77 @@
   avoiding a finitely supported c and there is a permutation
   which 'translates' between both sets.
 *}
+
 lemma at_set_avoiding_aux:
   fixes Xs::"'a set"
   and   As::"'a set"
   assumes at: "at TYPE('a)"
-  and     a: "finite Xs"
   and     b: "Xs \<subseteq> As"
   and     c: "finite As"
   and     d: "finite ((supp c)::'a set)"
-  shows "\<exists>(Ys::'a set) (pi::'a prm). Ys\<sharp>*c \<and> Ys \<inter> As = {} \<and> (pi\<bullet>Xs=Ys) \<and> 
-          set pi \<subseteq> Xs \<times> Ys \<and> finite Ys"
-using a b c
-proof (induct)
-  case empty
-  have "({}::'a set)\<sharp>*c" by (simp add: fresh_star_def)
-  moreover
-  have "({}::'a set) \<inter> As = {}" by simp
-  moreover
-  have "([]::'a prm)\<bullet>{} = ({}::'a set)" 
-    by (rule pt1[OF pt_fun_inst, OF at_pt_inst[OF at], OF pt_bool_inst, OF at])
-  moreover
-  have "set ([]::'a prm) \<subseteq> {} \<times> {}" by simp
-  moreover 
-  have "finite ({}::'a set)" by simp
-  ultimately show ?case by blast
-next
-  case (insert x Xs)
-  then have ih: "\<exists>Ys pi. Ys\<sharp>*c \<and> Ys \<inter> As = {} \<and> pi\<bullet>Xs = Ys \<and> set pi \<subseteq> Xs \<times> Ys \<and> finite Ys" by simp
-  then obtain Ys pi where a1: "Ys\<sharp>*c" and a2: "Ys \<inter> As = {}" and a3: "pi\<bullet>Xs = Ys" and 
-                          a4: "set pi \<subseteq> Xs \<times> Ys" and a5: "finite Ys" by blast
-  have b: "x\<notin>Xs" by fact
-  have d1: "finite As" by fact
-  have d2: "finite Xs" by fact
-  have d3: "insert x Xs \<subseteq> As" by fact
-  have "\<exists>y::'a. y\<sharp>(c,x,Ys,As)" using d d1 a5
-    by (rule_tac at_exists_fresh'[OF at])
-       (simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at])
-  then obtain y::"'a" where  e: "y\<sharp>(c,x,Ys,As)" by blast
-  have "({y}\<union>Ys)\<sharp>*c" using a1 e by (simp add: fresh_star_def)
-  moreover
-  have "({y}\<union>Ys)\<inter>As = {}" using a2 d1 e by (simp add: fresh_prod at_fin_set_fresh[OF at])
-  moreover
-  have "(((pi\<bullet>x,y)#pi)\<bullet>(insert x Xs)) = {y}\<union>Ys"
-  proof -
-    have eq: "[(pi\<bullet>x,y)]\<bullet>Ys = Ys" 
+  shows "\<exists>(pi::'a prm). (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)"
+proof -
+  from b c have "finite Xs" by (simp add: finite_subset)
+  then show ?thesis using b 
+  proof (induct)
+    case empty
+    have "({}::'a set)\<sharp>*c" by (simp add: fresh_star_def)
+    moreover
+    have "({}::'a set) \<inter> As = {}" by simp
+    moreover
+    have "set ([]::'a prm) \<subseteq> {} \<times> {}" by simp
+    moreover
+    have "([]::'a prm)\<bullet>{} = ({}::'a set)" 
+      by (rule pt1[OF pt_fun_inst, OF at_pt_inst[OF at] pt_bool_inst at])
+    ultimately show ?case by simp
+  next
+    case (insert x Xs)
+    then have ih: "\<exists>pi. (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by simp
+    then obtain pi where a1: "(pi\<bullet>Xs)\<sharp>*c" and a2: "(pi\<bullet>Xs) \<inter> As = {}" and 
+      a4: "set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by blast
+    have b: "x\<notin>Xs" by fact
+    have d1: "finite As" by fact
+    have d2: "finite Xs" by fact
+    have d3: "({x} \<union> Xs) \<subseteq> As" using insert(4) by simp
+    from d d1 d2
+    obtain y::"'a" where fr: "y\<sharp>(c,pi\<bullet>Xs,As)" 
+      apply(rule_tac at_exists_fresh[OF at, where x="(c,pi\<bullet>Xs,As)"])
+      apply(auto simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at]
+	pt_supp_finite_pi[OF pt_fun_inst[OF at_pt_inst[OF at] pt_bool_inst at] at])
+      done
+    have "({y}\<union>(pi\<bullet>Xs))\<sharp>*c" using a1 fr by (simp add: fresh_star_def)
+    moreover
+    have "({y}\<union>(pi\<bullet>Xs))\<inter>As = {}" using a2 d1 fr 
+      by (simp add: fresh_prod at_fin_set_fresh[OF at])
+    moreover
+    have "pi\<bullet>x=x" using a4 b a2 d3 
+      by (rule_tac at_prm_fresh2[OF at]) (auto)
+    then have "set ((pi\<bullet>x,y)#pi) \<subseteq> ({x} \<union> Xs) \<times> ({y}\<union>(pi\<bullet>Xs))" using a4 by auto
+    moreover
+    have "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)"
     proof -
-      have "(pi\<bullet>x)\<sharp>Ys" using a3[symmetric] b d2 
-	by(simp add: pt_fresh_bij[OF pt_fun_inst, OF at_pt_inst[OF at], OF pt_bool_inst, OF at, OF at]
-                     at_fin_set_fresh[OF at])
-      moreover
-      have "y\<sharp>Ys" using e by simp
-      ultimately show "[(pi\<bullet>x,y)]\<bullet>Ys = Ys" 
-	by (simp add: pt_fresh_fresh[OF pt_fun_inst, OF at_pt_inst[OF at], OF pt_bool_inst, OF at, OF at])
+      have eq: "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 
+      proof -
+	have "(pi\<bullet>x)\<sharp>(pi\<bullet>Xs)" using b d2 
+	  by(simp add: pt_fresh_bij[OF pt_fun_inst, OF at_pt_inst[OF at], 
+            OF pt_bool_inst, OF at, OF at]
+            at_fin_set_fresh[OF at])
+	moreover
+	have "y\<sharp>(pi\<bullet>Xs)" using fr by simp
+	ultimately show "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 
+	  by (simp add: pt_fresh_fresh[OF pt_fun_inst, 
+            OF at_pt_inst[OF at], OF pt_bool_inst, OF at, OF at])
+      qed
+      have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))"
+	by (simp add: pt2[symmetric, OF pt_fun_inst, OF at_pt_inst[OF at], 
+          OF pt_bool_inst, OF at])
+      also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))" 
+	by (simp only: union_eqvt perm_set_eq[OF at_pt_inst[OF at], OF at] at_calc[OF at])(auto)
+      finally show "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)" using eq by simp
     qed
-    have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))"
-      by (simp add: pt2[symmetric, OF pt_fun_inst, OF at_pt_inst[OF at], OF pt_bool_inst, OF at])
-    also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))" 
-      by (simp only: union_eqvt perm_set_eq[OF at_pt_inst[OF at], OF at] at_calc[OF at])(auto)
-    also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>Ys)" using a3 by simp
-    also have "\<dots> = {y}\<union>Ys" using eq by simp
-    finally show "(((pi\<bullet>x,y)#pi)\<bullet>(insert x Xs)) = {y}\<union>Ys" by auto
+    ultimately 
+    show ?case by (rule_tac x="(pi\<bullet>x,y)#pi" in exI) (auto)
   qed
-  moreover
-  have "pi\<bullet>x=x" using a4 b a2 a3 d3 by (rule_tac at_prm_fresh2[OF at]) (auto)
-  then have "set ((pi\<bullet>x,y)#pi) \<subseteq> (insert x Xs) \<times> ({y}\<union>Ys)" using a4 by auto
-  moreover 
-  have "finite ({y}\<union>Ys)" using a5 by simp
-  ultimately 
-  show ?case by blast
 qed
 
 lemma at_set_avoiding:
@@ -2698,10 +2701,10 @@
   assumes at: "at TYPE('a)"
   and     a: "finite Xs"
   and     b: "finite ((supp c)::'a set)"
-  obtains pi::"'a prm" where "(pi \<bullet> Xs) \<sharp>* c" and "set pi \<subseteq> Xs \<times> (pi \<bullet> Xs)"
-  using a b
-  by (frule_tac As="Xs" in at_set_avoiding_aux[OF at]) auto
- 
+  obtains pi::"'a prm" where "(pi\<bullet>Xs)\<sharp>*c" and "set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)"
+using a b at_set_avoiding_aux[OF at, where Xs="Xs" and As="Xs" and c="c"]
+by (blast)
+
 section {* composition instances *}
 (* ============================= *)