# HG changeset patch # User haftmann # Date 1204054690 -3600 # Node ID 61cb176d0385fc031d9039f0238086b46e169551 # Parent 95670b6e1fa381861cd9aa887deb8e25756fb7b0 tuned proofs diff -r 95670b6e1fa3 -r 61cb176d0385 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Tue Feb 26 16:10:54 2008 +0100 +++ b/src/HOL/Datatype.thy Tue Feb 26 20:38:10 2008 +0100 @@ -615,25 +615,8 @@ lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" by (rule set_ext, case_tac x) auto -instantiation option :: (finite) finite -begin - -definition - "Finite_Set.itself = TYPE('a option)" - -instance proof - have "finite (UNIV :: 'a set)" by (rule finite) - hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp - also have "insert None (Some ` (UNIV :: 'a set)) = UNIV" - by (rule insert_None_conv_UNIV) - finally show "finite (UNIV :: 'a option set)" . -qed - -end - -lemma univ_option [noatp, code func]: - "UNIV = insert (None \ 'a\finite option) (image Some UNIV)" - unfolding insert_None_conv_UNIV .. +instance option :: (finite) finite + by default (simp add: insert_None_conv_UNIV [symmetric]) subsubsection {* Operations *} diff -r 95670b6e1fa3 -r 61cb176d0385 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Feb 26 16:10:54 2008 +0100 +++ b/src/HOL/Finite_Set.thy Tue Feb 26 20:38:10 2008 +0100 @@ -428,8 +428,7 @@ by auto setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*} -class finite (attach UNIV) = type + - fixes itself :: "'a itself" +class finite (attach UNIV) = itself + assumes finite_UNIV: "finite (UNIV \ 'a set)" setup {* Sign.parent_path *} hide const finite @@ -437,112 +436,42 @@ lemma finite [simp]: "finite (A \ 'a\finite set)" by (rule finite_subset [OF subset_UNIV finite_UNIV]) -lemma univ_unit [noatp]: +lemma UNIV_unit [noatp]: "UNIV = {()}" by auto -instantiation unit :: finite -begin - -definition - "itself = TYPE(unit)" - -instance proof - have "finite {()}" by simp - also note univ_unit [symmetric] - finally show "finite (UNIV :: unit set)" . -qed - -end - -lemmas [code func] = univ_unit - -lemma univ_bool [noatp]: +instance unit :: finite + by default (simp add: UNIV_unit) + +lemmas [code func] = UNIV_unit + +lemma UNIV_bool [noatp]: "UNIV = {False, True}" by auto -instantiation bool :: finite -begin - -definition - "itself = TYPE(bool)" - -instance proof - have "finite {False, True}" by simp - also note univ_bool [symmetric] - finally show "finite (UNIV :: bool set)" . -qed - -end - -lemmas [code func] = univ_bool - -instantiation * :: (finite, finite) finite -begin - -definition - "itself = TYPE('a \ 'b)" - -instance proof - show "finite (UNIV :: ('a \ 'b) set)" - proof (rule finite_Prod_UNIV) - show "finite (UNIV :: 'a set)" by (rule finite) - show "finite (UNIV :: 'b set)" by (rule finite) - qed -qed - -end - -lemma univ_prod [noatp, code func]: - "UNIV = (UNIV \ 'a\finite set) \ (UNIV \ 'b\finite set)" - unfolding UNIV_Times_UNIV .. - -instantiation "+" :: (finite, finite) finite -begin - -definition - "itself = TYPE('a + 'b)" - -instance proof - have a: "finite (UNIV :: 'a set)" by (rule finite) - have b: "finite (UNIV :: 'b set)" by (rule finite) - from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))" - by (rule finite_Plus) - thus "finite (UNIV :: ('a + 'b) set)" by simp -qed - -end - -lemma univ_sum [noatp, code func]: - "UNIV = (UNIV \ 'a\finite set) <+> (UNIV \ 'b\finite set)" - unfolding UNIV_Plus_UNIV .. - -instantiation set :: (finite) finite -begin - -definition - "itself = TYPE('a set)" - -instance proof - have "finite (UNIV :: 'a set)" by (rule finite) - hence "finite (Pow (UNIV :: 'a set))" - by (rule finite_Pow_iff [THEN iffD2]) - thus "finite (UNIV :: 'a set set)" by simp -qed - -end - -lemma univ_set [noatp, code func]: - "UNIV = Pow (UNIV \ 'a\finite set)" unfolding Pow_UNIV .. +instance bool :: finite + by default (simp add: UNIV_bool) + +lemmas [code func] = UNIV_bool + +instance * :: (finite, finite) finite + by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) + +declare UNIV_Times_UNIV [symmetric, code func] + +instance "+" :: (finite, finite) finite + by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) + +declare UNIV_Plus_UNIV [symmetric, code func] + +instance set :: (finite) finite + by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite) + +declare Pow_UNIV [symmetric, code func] lemma inj_graph: "inj (%f. {(x, y). y = f x})" by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq) -instantiation "fun" :: (finite, finite) finite -begin - -definition - "itself \ TYPE('a \ 'b)" - -instance proof +instance "fun" :: (finite, finite) finite +proof show "finite (UNIV :: ('a => 'b) set)" proof (rule finite_imageD) let ?graph = "%f::'a => 'b. {(x, y). y = f x}" @@ -551,9 +480,6 @@ qed qed -end - -hide (open) const itself subsection {* Equality and order on functions *}