summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Finite_Set.thy

changeset 17022 | b257300c3a9c |

parent 16775 | c1b87ef4a1c3 |

child 17085 | 5b57f995a179 |

1.1 --- a/src/HOL/Finite_Set.thy Wed Aug 03 16:43:39 2005 +0200 1.2 +++ b/src/HOL/Finite_Set.thy Fri Aug 05 12:20:30 2005 +0200 1.3 @@ -305,6 +305,9 @@ 1.4 by (blast intro: finite_UN_I finite_subset) 1.5 1.6 1.7 +lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)" 1.8 +by (simp add: Plus_def) 1.9 + 1.10 text {* Sigma of finite sets *} 1.11 1.12 lemma finite_SigmaI [simp]: 1.13 @@ -353,23 +356,6 @@ 1.14 done 1.15 1.16 1.17 -instance unit :: finite 1.18 -proof 1.19 - have "finite {()}" by simp 1.20 - also have "{()} = UNIV" by auto 1.21 - finally show "finite (UNIV :: unit set)" . 1.22 -qed 1.23 - 1.24 -instance * :: (finite, finite) finite 1.25 -proof 1.26 - show "finite (UNIV :: ('a \<times> 'b) set)" 1.27 - proof (rule finite_Prod_UNIV) 1.28 - show "finite (UNIV :: 'a set)" by (rule finite) 1.29 - show "finite (UNIV :: 'b set)" by (rule finite) 1.30 - qed 1.31 -qed 1.32 - 1.33 - 1.34 text {* The powerset of a finite set *} 1.35 1.36 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A" 1.37 @@ -2313,4 +2299,67 @@ 1.38 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)" 1.39 by(simp add: Max_def max.fold1_below_iff) 1.40 1.41 +subsection {* Properties of axclass @{text finite} *} 1.42 + 1.43 +text{* Many of these are by Brian Huffman. *} 1.44 + 1.45 +lemma finite_set: "finite (A::'a::finite set)" 1.46 +by (rule finite_subset [OF subset_UNIV finite]) 1.47 + 1.48 + 1.49 +instance unit :: finite 1.50 +proof 1.51 + have "finite {()}" by simp 1.52 + also have "{()} = UNIV" by auto 1.53 + finally show "finite (UNIV :: unit set)" . 1.54 +qed 1.55 + 1.56 +instance bool :: finite 1.57 +proof 1.58 + have "finite {True, False}" by simp 1.59 + also have "{True, False} = UNIV" by auto 1.60 + finally show "finite (UNIV :: bool set)" . 1.61 +qed 1.62 + 1.63 + 1.64 +instance * :: (finite, finite) finite 1.65 +proof 1.66 + show "finite (UNIV :: ('a \<times> 'b) set)" 1.67 + proof (rule finite_Prod_UNIV) 1.68 + show "finite (UNIV :: 'a set)" by (rule finite) 1.69 + show "finite (UNIV :: 'b set)" by (rule finite) 1.70 + qed 1.71 +qed 1.72 + 1.73 +instance "+" :: (finite, finite) finite 1.74 +proof 1.75 + have a: "finite (UNIV :: 'a set)" by (rule finite) 1.76 + have b: "finite (UNIV :: 'b set)" by (rule finite) 1.77 + from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))" 1.78 + by (rule finite_Plus) 1.79 + thus "finite (UNIV :: ('a + 'b) set)" by simp 1.80 +qed 1.81 + 1.82 + 1.83 +instance set :: (finite) finite 1.84 +proof 1.85 + have "finite (UNIV :: 'a set)" by (rule finite) 1.86 + hence "finite (Pow (UNIV :: 'a set))" 1.87 + by (rule finite_Pow_iff [THEN iffD2]) 1.88 + thus "finite (UNIV :: 'a set set)" by simp 1.89 +qed 1.90 + 1.91 +lemma inj_graph: "inj (%f. {(x, y). y = f x})" 1.92 +by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq) 1.93 + 1.94 +instance fun :: (finite, finite) finite 1.95 +proof 1.96 + show "finite (UNIV :: ('a => 'b) set)" 1.97 + proof (rule finite_imageD) 1.98 + let ?graph = "%f::'a => 'b. {(x, y). y = f x}" 1.99 + show "finite (range ?graph)" by (rule finite_set) 1.100 + show "inj ?graph" by (rule inj_graph) 1.101 + qed 1.102 +qed 1.103 + 1.104 end