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