# HG changeset patch
# User urbanc
# Date 1133775157 -3600
# Node ID 6bab9cef50cf78cb7e9423b4407f18388ef04e57
# Parent  66cda85ea3ab5a4bc47ebac3ee9addafac09f704
ISAR-fied two proofs

diff -r 66cda85ea3ab -r 6bab9cef50cf src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Dec 05 00:39:18 2005 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Mon Dec 05 10:32:37 2005 +0100
@@ -1683,26 +1683,35 @@
 proof -
   have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
   show ?thesis
-    apply(auto simp add: perm_set_def)
-    apply(rule_tac x="pi\<bullet>xa" in exI)
-    apply(rule conjI)
-    apply(rule_tac x="xa" in exI)
-    apply(simp)
-    apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xa) = pi\<bullet>(f xa)")(*A*)
-    apply(simp)
-    apply(rule pt_set_bij2[OF pt_x, OF at])
-    apply(assumption)
-    apply(rule sym)
-    apply(rule pt_fun_app_eq[OF pt, OF at])
-    apply(rule_tac x="(rev pi)\<bullet>x" in exI)
-    apply(rule conjI)
-    apply(rule sym)
-    apply(rule pt_pi_rev[OF pt_x, OF at])
-    apply(rule_tac x="a" in bexI)
-    apply(simp add: pt_set_bij1[OF pt_x, OF at])
-    apply(simp add: pt_fun_app_eq[OF pt, OF at])
-    apply(assumption)
-    done
+  proof (rule equalityI)
+    case goal1
+    show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
+      apply(auto simp add: perm_set_def)
+      apply(rule_tac x="pi\<bullet>xa" in exI)
+      apply(rule conjI)
+      apply(rule_tac x="xa" in exI)
+      apply(simp)
+      apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xa) = pi\<bullet>(f xa)")(*A*)
+      apply(simp)
+      apply(rule pt_set_bij2[OF pt_x, OF at])
+      apply(assumption)
+      (*A*)
+      apply(rule sym)
+      apply(rule pt_fun_app_eq[OF pt, OF at])
+      done
+  next
+    case goal2
+    show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
+      apply(auto simp add: perm_set_def)
+      apply(rule_tac x="(rev pi)\<bullet>x" in exI)
+      apply(rule conjI)
+      apply(simp add: pt_pi_rev[OF pt_x, OF at])
+      apply(rule_tac x="a" in bexI)
+      apply(simp add: pt_set_bij1[OF pt_x, OF at])
+      apply(simp add: pt_fun_app_eq[OF pt, OF at])
+      apply(assumption)
+      done
+  qed
 qed
 
 lemma X_to_Un_supp_eqvt:
@@ -1760,8 +1769,7 @@
     apply(force intro: pt_set_inst at_pt_inst pt at)+
     apply(rule pt_eqvt_fun2b)
     apply(force intro: pt_set_inst at_pt_inst pt at)+
-    apply(rule allI)
-    apply(rule allI)
+    apply(rule allI)+
     apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
     done
   hence "supp (\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> ((supp X)::'x set)" by (simp add: X_to_Un_supp_def)
@@ -1780,7 +1788,7 @@
   and     fs: "fs TYPE('a) TYPE('x)" 
   and     fi: "finite X"
   shows "(supp X) = (\<Union>x\<in>X. ((supp x)::'x set))"
-apply(rule subset_antisym)
+apply(rule equalityI)
 apply(rule supp_is_subset)
 apply(rule Union_supports_set[OF pt, OF at])
 apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
@@ -2242,38 +2250,6 @@
       and at: "at TYPE('x)"
       and a1: "a\<noteq>b" 
       and a2: "[a].x = [b].y" 
-  shows "x=[(a,b)]\<bullet>y\<and>a\<sharp>y"
-proof -
-  from a2 have a3: 
-         "\<forall>c::'x. (if c=a then nSome(x) else (if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone))
-                = (if c=b then nSome(y) else (if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone))"
-         (is "\<forall>c::'x. ?P c = ?Q c")
-    by (force simp add: abs_fun_def expand_fun_eq)
-  from a3 have "?P a = ?Q a" by (blast)
-  hence a4: "nSome(x) = ?Q a" by simp
-  show ?thesis using a4 (*a5*)
-  proof (cases "a\<sharp>y")
-    assume a6: "a\<sharp>y"
-    hence a7: "x = [(b,a)]\<bullet>y" using a4 a1 by simp
-    have "[(a,b)]\<bullet>y = [(b,a)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at])
-    thus ?thesis using a6 a7 by simp
-  next
-    assume "\<not>a\<sharp>y"
-    hence "nSome(x) = nNone" using a1 a4 by simp
-    hence False by force
-    thus ?thesis by force
-  qed
-qed
-
-lemma abs_fun_eq2:
-  fixes x  :: "'a"
-  and   y  :: "'a"
-  and   a  :: "'x"
-  and   b  :: "'x"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-      and at: "at TYPE('x)"
-      and a1: "a\<noteq>b" 
-      and a2: "[a].x = [b].y" 
   shows "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
 proof -
   from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: expand_fun_eq)