added/moved lemmas by Andreas Lochbihler
authorhaftmann
Tue Jun 02 16:23:43 2009 +0200 (2009-06-02)
changeset 31380f25536c0bb80
parent 31379 213299656575
child 31381 b3a785a69538
added/moved lemmas by Andreas Lochbihler
src/HOL/Finite_Set.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Fin_Fun.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jun 02 15:53:34 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jun 02 16:23:43 2009 +0200
     1.3 @@ -1926,34 +1926,40 @@
     1.4  But now that we have @{text setsum} things are easy:
     1.5  *}
     1.6  
     1.7 -definition card :: "'a set \<Rightarrow> nat"
     1.8 -where "card A = setsum (\<lambda>x. 1) A"
     1.9 +definition card :: "'a set \<Rightarrow> nat" where
    1.10 +  "card A = setsum (\<lambda>x. 1) A"
    1.11 +
    1.12 +lemmas card_eq_setsum = card_def
    1.13  
    1.14  lemma card_empty [simp]: "card {} = 0"
    1.15 -by (simp add: card_def)
    1.16 -
    1.17 -lemma card_infinite [simp]: "~ finite A ==> card A = 0"
    1.18 -by (simp add: card_def)
    1.19 -
    1.20 -lemma card_eq_setsum: "card A = setsum (%x. 1) A"
    1.21 -by (simp add: card_def)
    1.22 +  by (simp add: card_def)
    1.23  
    1.24  lemma card_insert_disjoint [simp]:
    1.25    "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
    1.26 -by(simp add: card_def)
    1.27 +  by (simp add: card_def)
    1.28  
    1.29  lemma card_insert_if:
    1.30    "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
    1.31 -by (simp add: insert_absorb)
    1.32 +  by (simp add: insert_absorb)
    1.33 +
    1.34 +lemma card_infinite [simp]: "~ finite A ==> card A = 0"
    1.35 +  by (simp add: card_def)
    1.36 +
    1.37 +lemma card_ge_0_finite:
    1.38 +  "card A > 0 \<Longrightarrow> finite A"
    1.39 +  by (rule ccontr) simp
    1.40  
    1.41  lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
    1.42 -apply auto
    1.43 -apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
    1.44 -done
    1.45 +  apply auto
    1.46 +  apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
    1.47 +  done
    1.48 +
    1.49 +lemma finite_UNIV_card_ge_0:
    1.50 +  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
    1.51 +  by (rule ccontr) simp
    1.52  
    1.53  lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
    1.54 -by auto
    1.55 -
    1.56 +  by auto
    1.57  
    1.58  lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
    1.59  apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
    1.60 @@ -2049,6 +2055,24 @@
    1.61         finite_subset [of _ "\<Union> (insert x F)"])
    1.62  done
    1.63  
    1.64 +lemma card_eq_UNIV_imp_eq_UNIV:
    1.65 +  assumes fin: "finite (UNIV :: 'a set)"
    1.66 +  and card: "card A = card (UNIV :: 'a set)"
    1.67 +  shows "A = (UNIV :: 'a set)"
    1.68 +proof
    1.69 +  show "A \<subseteq> UNIV" by simp
    1.70 +  show "UNIV \<subseteq> A"
    1.71 +  proof
    1.72 +    fix x
    1.73 +    show "x \<in> A"
    1.74 +    proof (rule ccontr)
    1.75 +      assume "x \<notin> A"
    1.76 +      then have "A \<subset> UNIV" by auto
    1.77 +      with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
    1.78 +      with card show False by simp
    1.79 +    qed
    1.80 +  qed
    1.81 +qed
    1.82  
    1.83  text{*The form of a finite set of given cardinality*}
    1.84  
    1.85 @@ -2078,6 +2102,17 @@
    1.86   apply(auto intro:ccontr)
    1.87  done
    1.88  
    1.89 +lemma finite_fun_UNIVD2:
    1.90 +  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
    1.91 +  shows "finite (UNIV :: 'b set)"
    1.92 +proof -
    1.93 +  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
    1.94 +    by(rule finite_imageI)
    1.95 +  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
    1.96 +    by(rule UNIV_eq_I) auto
    1.97 +  ultimately show "finite (UNIV :: 'b set)" by simp
    1.98 +qed
    1.99 +
   1.100  lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
   1.101  apply (cases "finite A")
   1.102  apply (erule finite_induct)
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Jun 02 15:53:34 2009 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Jun 02 16:23:43 2009 +0200
     2.3 @@ -219,6 +219,25 @@
     2.4  apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
     2.5  done
     2.6  
     2.7 +lemma finite_fun_UNIVD1:
     2.8 +  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
     2.9 +  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
    2.10 +  shows "finite (UNIV :: 'a set)"
    2.11 +proof -
    2.12 +  from fin have finb: "finite (UNIV :: 'b set)" by (rule finite_fun_UNIVD2)
    2.13 +  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
    2.14 +    by (cases "card (UNIV :: 'b set)") (auto simp add: card_eq_0_iff)
    2.15 +  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)" by auto
    2.16 +  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by (auto simp add: card_Suc_eq)
    2.17 +  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by (rule finite_imageI)
    2.18 +  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
    2.19 +  proof (rule UNIV_eq_I)
    2.20 +    fix x :: 'a
    2.21 +    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_def)
    2.22 +    thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
    2.23 +  qed
    2.24 +  ultimately show "finite (UNIV :: 'a set)" by simp
    2.25 +qed
    2.26  
    2.27  subsection {*Inverse of a PI-function (restricted domain)*}
    2.28  
     3.1 --- a/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 15:53:34 2009 +0200
     3.2 +++ b/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 16:23:43 2009 +0200
     3.3 @@ -17,68 +17,12 @@
     3.4    For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
     3.5  *}
     3.6  
     3.7 -subsection {* Auxiliary definitions and lemmas *}
     3.8 -
     3.9 -(*FIXME move these to Finite_Set.thy*)
    3.10 -lemma card_ge_0_finite:
    3.11 -  "card A > 0 \<Longrightarrow> finite A"
    3.12 -by(rule ccontr, drule card_infinite, simp)
    3.13 -
    3.14 -lemma finite_UNIV_card_ge_0:
    3.15 -  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
    3.16 -by(rule ccontr) simp
    3.17 -
    3.18 -lemma card_eq_UNIV_imp_eq_UNIV:
    3.19 -  assumes fin: "finite (UNIV :: 'a set)"
    3.20 -  and card: "card A = card (UNIV :: 'a set)"
    3.21 -  shows "A = (UNIV :: 'a set)"
    3.22 -apply -
    3.23 -  proof
    3.24 -  show "A \<subseteq> UNIV" by simp
    3.25 -  show "UNIV \<subseteq> A"
    3.26 -  proof
    3.27 -    fix x
    3.28 -    show "x \<in> A"
    3.29 -    proof(rule ccontr)
    3.30 -      assume "x \<notin> A"
    3.31 -      hence "A \<subset> UNIV" by auto
    3.32 -      from psubset_card_mono[OF fin this] card show False by simp
    3.33 -    qed
    3.34 -  qed
    3.35 -qed
    3.36 -
    3.37 -lemma finite_fun_UNIVD2: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
    3.38 -  shows "finite (UNIV :: 'b set)"
    3.39 -proof -
    3.40 -  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
    3.41 -    by(rule finite_imageI)
    3.42 -  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
    3.43 -    by(rule UNIV_eq_I) auto
    3.44 -  ultimately show "finite (UNIV :: 'b set)" by simp
    3.45 -qed
    3.46 -
    3.47 -lemma finite_fun_UNIVD1: assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
    3.48 -  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
    3.49 -  shows "finite (UNIV :: 'a set)"
    3.50 -proof -
    3.51 -  from fin have finb: "finite (UNIV :: 'b set)" by(rule finite_fun_UNIVD2)
    3.52 -  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
    3.53 -    by(cases "card (UNIV :: 'b set)")(auto simp add: card_eq_0_iff)
    3.54 -  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - 2" by(auto)
    3.55 -  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by(auto simp add: card_Suc_eq)
    3.56 -  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by(rule finite_imageI)
    3.57 -  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
    3.58 -  proof(rule UNIV_eq_I)
    3.59 -    fix x :: 'a
    3.60 -    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by(simp add: inv_def)
    3.61 -    thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
    3.62 -  qed
    3.63 -  ultimately show "finite (UNIV :: 'a set)" by simp
    3.64 -qed
    3.65 -
    3.66  (*FIXME move to Map.thy*)
    3.67  lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
    3.68 -by(auto simp add: restrict_map_def intro: ext)
    3.69 +  by (auto simp add: restrict_map_def intro: ext)
    3.70 +
    3.71 +
    3.72 +subsection {* The @{text "map_default"} operation *}
    3.73  
    3.74  definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    3.75  where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
     4.1 --- a/src/HOL/Map.thy	Tue Jun 02 15:53:34 2009 +0200
     4.2 +++ b/src/HOL/Map.thy	Tue Jun 02 16:23:43 2009 +0200
     4.3 @@ -332,6 +332,9 @@
     4.4  lemma restrict_map_to_empty [simp]: "m|`{} = empty"
     4.5  by (simp add: restrict_map_def)
     4.6  
     4.7 +lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
     4.8 +by (auto simp add: restrict_map_def intro: ext)
     4.9 +
    4.10  lemma restrict_map_empty [simp]: "empty|`D = empty"
    4.11  by (simp add: restrict_map_def)
    4.12