# HG changeset patch
# User urbanc
# Date 1174569965 -3600
# Node ID 8436bfd21bf338cf69c3e0439af9e6e93e696bf1
# Parent  68c8a8390e16f596708e1f399e66d34ebab13f58
corrected the lemmas min_nat_eqvt and min_int_eqvt

diff -r 68c8a8390e16 -r 8436bfd21bf3 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Mar 22 14:03:30 2007 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 22 14:26:05 2007 +0100
@@ -2388,12 +2388,12 @@
   assumes pta: "pt TYPE('a) TYPE('x)"
   and     at:  "at TYPE('x)" 
   and     f1:  "finite ((supp h)::'x set)"
-  and     a: "\<exists>a::'x. (a\<sharp>h \<and> a\<sharp>(h a))"
+  and     a: "\<exists>a::'x. a\<sharp>(h,h a)"
   shows  "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> (h a) = fr"
 proof -
   have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
   have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
-  from a obtain a0 where a1: "a0\<sharp>h" and a2: "a0\<sharp>(h a0)" by force
+  from a obtain a0 where a1: "a0\<sharp>h" and a2: "a0\<sharp>(h a0)" by (force simp add: fresh_prod)
   show ?thesis
   proof
     let ?fr = "h (a0::'x)"
@@ -2432,7 +2432,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)" 
   and     f1: "finite ((supp h)::'x set)"
-  and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+  and     a: "\<exists>(a::'x). a\<sharp>(h,h a)"
   shows  "\<exists>!(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr"
 proof (rule ex_ex1I)
   from pt at f1 a show "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr" by (simp add: freshness_lemma)
@@ -2440,7 +2440,7 @@
   fix fr1 fr2
   assume b1: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr1"
   assume b2: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr2"
-  from a obtain a where "(a::'x)\<sharp>h" by force 
+  from a obtain a where "(a::'x)\<sharp>h" by (force simp add: fresh_prod) 
   with b1 b2 have "h a = fr1 \<and> h a = fr2" by force
   thus "fr1 = fr2" by force
 qed
@@ -2456,7 +2456,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)" 
   and     f1: "finite ((supp h)::'x set)"
-  and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+  and     a: "\<exists>(a::'x). a\<sharp>(h,h a)"
   and     b: "a\<sharp>h"
   shows "(fresh_fun h) = (h a)"
 proof (unfold fresh_fun_def, rule the_equality)
@@ -2484,7 +2484,7 @@
   and     cpa: "cp TYPE('a) TYPE('x) TYPE('y)"
   and     cpb: "cp TYPE('y) TYPE('x) TYPE('y)"
   and     f1: "finite ((supp h)::'y set)"
-  and     a1: "\<exists>(a::'y). (a\<sharp>h \<and> a\<sharp>(h a))"
+  and     a1: "\<exists>(a::'y). a\<sharp>(h,h a)"
   shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
 proof -
   have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at']) 
@@ -2497,8 +2497,8 @@
     thus ?thesis
       by (simp add: pt_perm_supp_ineq[OF ptc, OF ptb, OF at, OF cpc])
   qed
-  from a1 obtain a' where c0: "a'\<sharp>h \<and> a'\<sharp>(h a')" by force
-  hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by simp_all
+  from a1 obtain a' where c0: "a'\<sharp>(h,h a')" by force
+  hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by (simp_all add: fresh_prod)
   have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1
   by (simp add: pt_fresh_bij_ineq[OF ptc, OF ptb, OF at, OF cpc])
   have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
@@ -2507,7 +2507,7 @@
       by (simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at,OF cpa])
     thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
   qed
-  have a2: "\<exists>(a::'y). (a\<sharp>(pi\<bullet>h) \<and> a\<sharp>((pi\<bullet>h) a))" using c3 c4 by force
+  have a2: "\<exists>(a::'y). a\<sharp>(pi\<bullet>h,(pi\<bullet>h) a)" using c3 c4 by (force simp add: fresh_prod)
   have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF ptb', OF at', OF f1])
   have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 
     by (simp add: fresh_fun_app[OF ptb', OF at', OF f2])
@@ -2520,7 +2520,7 @@
   assumes pta: "pt TYPE('a) TYPE('x)"
   and     at:  "at TYPE('x)" 
   and     f1:  "finite ((supp h)::'x set)"
-  and     a1: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+  and     a1: "\<exists>(a::'x). a\<sharp>(h,h a)"
   shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
 proof -
   have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
@@ -2530,15 +2530,15 @@
     from f1 have "finite (pi\<bullet>((supp h)::'x set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at])
     thus ?thesis by (simp add: pt_perm_supp[OF ptc, OF at])
   qed
-  from a1 obtain a' where c0: "a'\<sharp>h \<and> a'\<sharp>(h a')" by force
-  hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by simp_all
+  from a1 obtain a' where c0: "a'\<sharp>(h,h a')" by force
+  hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by (simp_all add: fresh_prod)
   have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1 by (simp add: pt_fresh_bij[OF ptc, OF at])
   have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
   proof -
     from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))" by (simp add: pt_fresh_bij[OF pta, OF at])
     thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
   qed
-  have a2: "\<exists>(a::'x). (a\<sharp>(pi\<bullet>h) \<and> a\<sharp>((pi\<bullet>h) a))" using c3 c4 by force
+  have a2: "\<exists>(a::'x). a\<sharp>(pi\<bullet>h,(pi\<bullet>h) a)" using c3 c4 by (force simp add: fresh_prod)
   have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF pta, OF at, OF f1])
   have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2])
   show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
@@ -2549,7 +2549,7 @@
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)" 
   and     f1: "finite ((supp h)::'x set)"
-  and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+  and     a: "\<exists>(a::'x). a\<sharp>(h,h a)"
   shows "((supp h)::'x set) supports (fresh_fun h)"
   apply(simp add: "op supports_def" fresh_def[symmetric])
   apply(auto)
@@ -3073,7 +3073,7 @@
 
 lemma min_nat_eqvt:
   fixes x::"nat"
-  shows "pi\<bullet>(max x y) = max (pi\<bullet>x) (pi\<bullet>y)" 
+  shows "pi\<bullet>(min x y) = min (pi\<bullet>x) (pi\<bullet>y)" 
 by (simp add:perm_nat_def) 
 
 lemma plus_nat_eqvt:
@@ -3115,7 +3115,7 @@
 
 lemma min_int_eqvt:
   fixes x::"int"
-  shows "pi\<bullet>(max x y) = max (pi\<bullet>x) (pi\<bullet>y)" 
+  shows "pi\<bullet>(min x y) = min (pi\<bullet>x) (pi\<bullet>y)" 
 by (simp add:perm_int_def) 
 
 lemma plus_int_eqvt: