1.1 --- a/src/HOL/Finite_Set.thy	Tue Sep 06 21:56:11 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Sep 06 22:37:32 2011 +0200
     1.3 @@ -486,22 +486,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instance unit :: finite proof
     1.8 -qed (simp add: UNIV_unit)
     1.9 -
    1.10 -instance bool :: finite proof
    1.11 -qed (simp add: UNIV_bool)
    1.12 -
    1.13  instance prod :: (finite, finite) finite proof
    1.14  qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    1.15  
    1.16 -lemma finite_option_UNIV [simp]:
    1.17 -  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    1.18 -  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    1.19 -
    1.20 -instance option :: (finite) finite proof
    1.21 -qed (simp add: UNIV_option_conv)
    1.22 -
    1.23  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
    1.24    by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
    1.25  
    1.26 @@ -519,9 +506,22 @@
    1.27    qed
    1.28  qed
    1.29  
    1.30 +instance bool :: finite proof
    1.31 +qed (simp add: UNIV_bool)
    1.32 +
    1.33 +instance unit :: finite proof
    1.34 +qed (simp add: UNIV_unit)
    1.35 +
    1.36  instance sum :: (finite, finite) finite proof
    1.37  qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    1.38  
    1.39 +lemma finite_option_UNIV [simp]:
    1.40 +  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    1.41 +  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    1.42 +
    1.43 +instance option :: (finite) finite proof
    1.44 +qed (simp add: UNIV_option_conv)
    1.45 +
    1.46  
    1.47  subsection {* A basic fold functional for finite sets *}
    1.48  

     2.1 --- a/src/HOL/Nominal/Nominal.thy	Tue Sep 06 21:56:11 2011 +0200
     2.2 +++ b/src/HOL/Nominal/Nominal.thy	Tue Sep 06 22:37:32 2011 +0200
     2.3 @@ -51,16 +51,16 @@
     2.4  begin
     2.5  
     2.6  definition
     2.7 -  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
     2.8 +  "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
     2.9  
    2.10  definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
    2.11 -  perm_bool_def: "perm_bool pi b = b"
    2.12 +  "perm_bool pi b = b"
    2.13  
    2.14  primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
    2.15    "perm_unit pi () = ()"
    2.16    
    2.17  primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
    2.18 -  "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
    2.19 +  "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
    2.20  
    2.21  primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.22    nil_eqvt:  "perm_list pi []     = []"
    2.23 @@ -71,13 +71,13 @@
    2.24  | none_eqvt:  "perm_option pi None     = None"
    2.25  
    2.26  definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
    2.27 -  perm_char_def: "perm_char pi c = c"
    2.28 +  "perm_char pi c = c"
    2.29  
    2.30  definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
    2.31 -  perm_nat_def: "perm_nat pi i = i"
    2.32 +  "perm_nat pi i = i"
    2.33  
    2.34  definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
    2.35 -  perm_int_def: "perm_int pi i = i"
    2.36 +  "perm_int pi i = i"
    2.37  
    2.38  primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
    2.39    nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
    2.40 @@ -962,7 +962,7 @@
    2.41    fixes pi::"'y prm"
    2.42    and   x ::"'x set"
    2.43    assumes dj: "disjoint TYPE('x) TYPE('y)"
    2.44 -  shows "(pi\<bullet>x)=x" 
    2.45 +  shows "pi\<bullet>x=x" 
    2.46    using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
    2.47  
    2.48  lemma dj_perm_perm_forget:
    2.49 @@ -1028,7 +1028,7 @@
    2.50  qed
    2.51  
    2.52  lemma pt_unit_inst:
    2.53 -  shows  "pt TYPE(unit) TYPE('x)"
    2.54 +  shows "pt TYPE(unit) TYPE('x)"
    2.55    by (simp add: pt_def)
    2.56  
    2.57  lemma pt_prod_inst:
    2.58 @@ -2262,7 +2262,7 @@
    2.59    and     at: "at TYPE('x)"
    2.60    shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
    2.61    apply(simp add: X_to_Un_supp_def)
    2.62 -  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'b="'x set"])
    2.63 +  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'd="'x set"])
    2.64    apply(simp add: pt_perm_supp[OF pt, OF at])
    2.65    apply(simp add: pt_pi_rev[OF pt, OF at])
    2.66    done

     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Tue Sep 06 21:56:11 2011 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Sep 06 22:37:32 2011 +0200
     3.3 @@ -130,7 +130,7 @@
     3.4       case redex of 
     3.5         (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
     3.6         (Const("Nominal.perm",_) $ pi $ f)  => 
     3.7 -          (if (applicable_fun f) then SOME perm_fun_def else NONE)
     3.8 +          (if applicable_fun f then SOME perm_fun_def else NONE)
     3.9        | _ => NONE
    3.10     end
    3.11