merged
authorhaftmann
Thu Sep 08 11:31:53 2011 +0200 (2011-09-08)
changeset 4484038975527c757
parent 44829 5a2cd5db0a11
parent 44839 d19c677eb812
child 44841 e55503200061
merged
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Sep 08 09:25:55 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Sep 08 11:31:53 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	Thu Sep 08 09:25:55 2011 +0200
     2.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 08 11:31:53 2011 +0200
     2.3 @@ -50,17 +50,17 @@
     2.4    perm_nprod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked)
     2.5  begin
     2.6  
     2.7 -definition
     2.8 -  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
     2.9 +definition perm_fun :: "'x prm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    2.10 +  "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
    2.11  
    2.12  definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
    2.13 -  perm_bool_def: "perm_bool pi b = b"
    2.14 +  "perm_bool pi b = b"
    2.15  
    2.16  primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
    2.17    "perm_unit pi () = ()"
    2.18    
    2.19  primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
    2.20 -  "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
    2.21 +  "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
    2.22  
    2.23  primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.24    nil_eqvt:  "perm_list pi []     = []"
    2.25 @@ -71,13 +71,13 @@
    2.26  | none_eqvt:  "perm_option pi None     = None"
    2.27  
    2.28  definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
    2.29 -  perm_char_def: "perm_char pi c = c"
    2.30 +  "perm_char pi c = c"
    2.31  
    2.32  definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
    2.33 -  perm_nat_def: "perm_nat pi i = i"
    2.34 +  "perm_nat pi i = i"
    2.35  
    2.36  definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
    2.37 -  perm_int_def: "perm_int pi i = i"
    2.38 +  "perm_int pi i = i"
    2.39  
    2.40  primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
    2.41    nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
    2.42 @@ -962,7 +962,7 @@
    2.43    fixes pi::"'y prm"
    2.44    and   x ::"'x set"
    2.45    assumes dj: "disjoint TYPE('x) TYPE('y)"
    2.46 -  shows "(pi\<bullet>x)=x" 
    2.47 +  shows "pi\<bullet>x=x" 
    2.48    using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
    2.49  
    2.50  lemma dj_perm_perm_forget:
    2.51 @@ -1028,7 +1028,7 @@
    2.52  qed
    2.53  
    2.54  lemma pt_unit_inst:
    2.55 -  shows  "pt TYPE(unit) TYPE('x)"
    2.56 +  shows "pt TYPE(unit) TYPE('x)"
    2.57    by (simp add: pt_def)
    2.58  
    2.59  lemma pt_prod_inst:
     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Thu Sep 08 09:25:55 2011 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Sep 08 11:31:53 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