merged
authorhaftmann
Mon Sep 05 19:18:38 2011 +0200 (2011-09-05)
changeset 4483227fb2285bdee
parent 44707 487ae6317f7b
parent 44831 4ea848959340
child 44834 242348d1b6d3
merged
     1.1 --- a/src/HOL/Finite_Set.thy	Sun Sep 04 06:27:59 2011 -0700
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Sep 05 19:18:38 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_permeq.ML	Sun Sep 04 06:27:59 2011 -0700
     2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Sep 05 19:18:38 2011 +0200
     2.3 @@ -130,7 +130,7 @@
     2.4       case redex of 
     2.5         (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
     2.6         (Const("Nominal.perm",_) $ pi $ f)  => 
     2.7 -          (if (applicable_fun f) then SOME perm_fun_def else NONE)
     2.8 +          (if applicable_fun f then SOME perm_fun_def else NONE)
     2.9        | _ => NONE
    2.10     end
    2.11