src/HOL/Finite_Set.thy
changeset 22388 14098da702e0
parent 22316 f662831459de
child 22398 dfe146d65b14
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Mar 02 15:43:18 2007 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Mar 02 15:43:19 2007 +0100
     1.3 @@ -17,9 +17,6 @@
     1.4      emptyI [simp, intro!]: "finite {}"
     1.5    | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
     1.6  
     1.7 -axclass finite \<subseteq> type
     1.8 -  finite: "finite UNIV"
     1.9 -
    1.10  lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    1.11    assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
    1.12    shows "\<exists>a::'a. a \<notin> A"
    1.13 @@ -2233,7 +2230,7 @@
    1.14  apply(subgoal_tac "EX a. a:A")
    1.15  prefer 2 apply blast
    1.16  apply(erule exE)
    1.17 -apply(rule trans)
    1.18 +apply(rule order_trans)
    1.19  apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_inf])
    1.20  apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
    1.21  done
    1.22 @@ -2520,7 +2517,7 @@
    1.23  using hom_Min_commute[of "op + k" N]
    1.24  apply simp apply(rule arg_cong[where f = Min]) apply blast
    1.25  apply(simp add:min_def linorder_not_le)
    1.26 -apply(blast intro:order_class.antisym order_less_imp_le add_left_mono)
    1.27 +apply(blast intro: antisym order_less_imp_le add_left_mono)
    1.28  done
    1.29  
    1.30  lemma add_Max_commute: fixes k::"'a::{pordered_ab_semigroup_add,linorder}"
    1.31 @@ -2529,33 +2526,41 @@
    1.32  using hom_Max_commute[of "op + k" N]
    1.33  apply simp apply(rule arg_cong[where f = Max]) apply blast
    1.34  apply(simp add:max_def linorder_not_le)
    1.35 -apply(blast intro:order_class.antisym order_less_imp_le add_left_mono)
    1.36 +apply(blast intro: antisym order_less_imp_le add_left_mono)
    1.37  done
    1.38  
    1.39  
    1.40 -
    1.41 -subsection {* Properties of axclass @{text finite} *}
    1.42 -
    1.43 -text{* Many of these are by Brian Huffman. *}
    1.44 +subsection {* Class @{text finite} *}
    1.45 +
    1.46 +class finite (attach UNIV) =
    1.47 +  assumes finite: "finite UNIV"
    1.48  
    1.49  lemma finite_set: "finite (A::'a::finite set)"
    1.50 -by (rule finite_subset [OF subset_UNIV finite])
    1.51 -
    1.52 +  by (rule finite_subset [OF subset_UNIV finite])
    1.53 +
    1.54 +lemma univ_unit:
    1.55 +  "UNIV = {()}" by auto
    1.56  
    1.57  instance unit :: finite
    1.58  proof
    1.59    have "finite {()}" by simp
    1.60 -  also have "{()} = UNIV" by auto
    1.61 +  also note univ_unit [symmetric]
    1.62    finally show "finite (UNIV :: unit set)" .
    1.63  qed
    1.64  
    1.65 +lemmas [code func] = univ_unit
    1.66 +
    1.67 +lemma univ_bool:
    1.68 +  "UNIV = {False, True}" by auto
    1.69 +
    1.70  instance bool :: finite
    1.71  proof
    1.72 -  have "finite {True, False}" by simp
    1.73 -  also have "{True, False} = UNIV" by auto
    1.74 +  have "finite {False, True}" by simp
    1.75 +  also note univ_bool [symmetric]
    1.76    finally show "finite (UNIV :: bool set)" .
    1.77  qed
    1.78  
    1.79 +lemmas [code func] = univ_bool
    1.80  
    1.81  instance * :: (finite, finite) finite
    1.82  proof
    1.83 @@ -2566,6 +2571,10 @@
    1.84    qed
    1.85  qed
    1.86  
    1.87 +lemma univ_prod [code func]:
    1.88 +  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
    1.89 +  unfolding UNIV_Times_UNIV ..
    1.90 +
    1.91  instance "+" :: (finite, finite) finite
    1.92  proof
    1.93    have a: "finite (UNIV :: 'a set)" by (rule finite)
    1.94 @@ -2575,6 +2584,9 @@
    1.95    thus "finite (UNIV :: ('a + 'b) set)" by simp
    1.96  qed
    1.97  
    1.98 +lemma univ_sum [code func]:
    1.99 +  "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
   1.100 +  unfolding UNIV_Plus_UNIV ..
   1.101  
   1.102  instance set :: (finite) finite
   1.103  proof
   1.104 @@ -2584,8 +2596,11 @@
   1.105    thus "finite (UNIV :: 'a set set)" by simp
   1.106  qed
   1.107  
   1.108 +lemma univ_set [code func]:
   1.109 +  "UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
   1.110 +
   1.111  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   1.112 -by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
   1.113 +  by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
   1.114  
   1.115  instance "fun" :: (finite, finite) finite
   1.116  proof
   1.117 @@ -2597,4 +2612,13 @@
   1.118    qed
   1.119  qed
   1.120  
   1.121 +
   1.122 +subsection {* Equality on functions *}
   1.123 +
   1.124 +instance "fun" :: (finite, eq) eq ..
   1.125 +
   1.126 +lemma eq_fun [code func]:
   1.127 +  "f = g \<longleftrightarrow> (\<forall>x\<Colon>'a\<Colon>finite \<in> UNIV. (f x \<Colon> 'b\<Colon>eq) = g x)"
   1.128 +  unfolding expand_fun_eq by auto
   1.129 +
   1.130  end