summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 05 Aug 2005 12:20:30 +0200 | |

changeset 17022 | b257300c3a9c |

parent 17021 | 1c361a3de73d |

child 17023 | 7425bf9f0f4b |

added Brian Hufmann's finite instances

--- a/src/HOL/Finite_Set.thy Wed Aug 03 16:43:39 2005 +0200 +++ b/src/HOL/Finite_Set.thy Fri Aug 05 12:20:30 2005 +0200 @@ -305,6 +305,9 @@ by (blast intro: finite_UN_I finite_subset) +lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)" +by (simp add: Plus_def) + text {* Sigma of finite sets *} lemma finite_SigmaI [simp]: @@ -353,23 +356,6 @@ done -instance unit :: finite -proof - have "finite {()}" by simp - also have "{()} = UNIV" by auto - finally show "finite (UNIV :: unit set)" . -qed - -instance * :: (finite, finite) finite -proof - show "finite (UNIV :: ('a \<times> '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 - - text {* The powerset of a finite set *} lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A" @@ -2313,4 +2299,67 @@ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)" by(simp add: Max_def max.fold1_below_iff) +subsection {* Properties of axclass @{text finite} *} + +text{* Many of these are by Brian Huffman. *} + +lemma finite_set: "finite (A::'a::finite set)" +by (rule finite_subset [OF subset_UNIV finite]) + + +instance unit :: finite +proof + have "finite {()}" by simp + also have "{()} = UNIV" by auto + finally show "finite (UNIV :: unit set)" . +qed + +instance bool :: finite +proof + have "finite {True, False}" by simp + also have "{True, False} = UNIV" by auto + finally show "finite (UNIV :: bool set)" . +qed + + +instance * :: (finite, finite) finite +proof + show "finite (UNIV :: ('a \<times> '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 + +instance "+" :: (finite, finite) finite +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 + + +instance set :: (finite) finite +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 + +lemma inj_graph: "inj (%f. {(x, y). y = f x})" +by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq) + +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}" + show "finite (range ?graph)" by (rule finite_set) + show "inj ?graph" by (rule inj_graph) + qed +qed + end