# HG changeset patch
# User haftmann
# Date 1315339454 -7200
# Node ID ff6b9eb9c5ef66c760fa5f36f064100924c6b99a
# Parent  deb929f002b886545cbe144da0b4402a48eabc9e# Parent  242348d1b6d3dda3434aeff7137e6864e99854a5
merged

diff -r deb929f002b8 -r ff6b9eb9c5ef src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Sep 06 21:11:12 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Sep 06 22:04:14 2011 +0200
@@ -486,22 +486,9 @@
 
 end
 
-instance unit :: finite proof
-qed (simp add: UNIV_unit)
-
-instance bool :: finite proof
-qed (simp add: UNIV_bool)
-
 instance prod :: (finite, finite) finite proof
 qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
 
-lemma finite_option_UNIV [simp]:
-  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
-  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
-
-instance option :: (finite) finite proof
-qed (simp add: UNIV_option_conv)
-
 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
 
@@ -519,9 +506,22 @@
   qed
 qed
 
+instance bool :: finite proof
+qed (simp add: UNIV_bool)
+
+instance unit :: finite proof
+qed (simp add: UNIV_unit)
+
 instance sum :: (finite, finite) finite proof
 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
 
+lemma finite_option_UNIV [simp]:
+  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
+  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
+
+instance option :: (finite) finite proof
+qed (simp add: UNIV_option_conv)
+
 
 subsection {* A basic fold functional for finite sets *}
 
diff -r deb929f002b8 -r ff6b9eb9c5ef src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Sep 06 21:11:12 2011 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Sep 06 22:04:14 2011 +0200
@@ -51,16 +51,16 @@
 begin
 
 definition
-  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
+  "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
 
 definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
-  perm_bool_def: "perm_bool pi b = b"
+  "perm_bool pi b = b"
 
 primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
   "perm_unit pi () = ()"
   
 primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
-  "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
+  "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
 
 primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   nil_eqvt:  "perm_list pi []     = []"
@@ -71,13 +71,13 @@
 | none_eqvt:  "perm_option pi None     = None"
 
 definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
-  perm_char_def: "perm_char pi c = c"
+  "perm_char pi c = c"
 
 definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
-  perm_nat_def: "perm_nat pi i = i"
+  "perm_nat pi i = i"
 
 definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
-  perm_int_def: "perm_int pi i = i"
+  "perm_int pi i = i"
 
 primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
   nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
@@ -962,7 +962,7 @@
   fixes pi::"'y prm"
   and   x ::"'x set"
   assumes dj: "disjoint TYPE('x) TYPE('y)"
-  shows "(pi\<bullet>x)=x" 
+  shows "pi\<bullet>x=x" 
   using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
 
 lemma dj_perm_perm_forget:
@@ -1028,7 +1028,7 @@
 qed
 
 lemma pt_unit_inst:
-  shows  "pt TYPE(unit) TYPE('x)"
+  shows "pt TYPE(unit) TYPE('x)"
   by (simp add: pt_def)
 
 lemma pt_prod_inst:
@@ -2262,7 +2262,7 @@
   and     at: "at TYPE('x)"
   shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
   apply(simp add: X_to_Un_supp_def)
-  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'b="'x set"])
+  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'd="'x set"])
   apply(simp add: pt_perm_supp[OF pt, OF at])
   apply(simp add: pt_pi_rev[OF pt, OF at])
   done
diff -r deb929f002b8 -r ff6b9eb9c5ef src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Tue Sep 06 21:11:12 2011 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Sep 06 22:04:14 2011 +0200
@@ -130,7 +130,7 @@
      case redex of 
        (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
        (Const("Nominal.perm",_) $ pi $ f)  => 
-          (if (applicable_fun f) then SOME perm_fun_def else NONE)
+          (if applicable_fun f then SOME perm_fun_def else NONE)
       | _ => NONE
    end