lemmas by Andreas Lochbihler
authornipkow
Sat May 09 07:25:22 2009 +0200 (2009-05-09)
changeset 3108021ffc770ebc0
parent 31079 35b437f7ad51
child 31081 aee96acd5e79
lemmas by Andreas Lochbihler
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Nat_Numeral.thy
src/HOL/Option.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri May 08 19:20:00 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sat May 09 07:25:22 2009 +0200
     1.3 @@ -365,6 +365,29 @@
     1.4  lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
     1.5  by (simp add: Plus_def)
     1.6  
     1.7 +lemma finite_PlusD: 
     1.8 +  fixes A :: "'a set" and B :: "'b set"
     1.9 +  assumes fin: "finite (A <+> B)"
    1.10 +  shows "finite A" "finite B"
    1.11 +proof -
    1.12 +  have "Inl ` A \<subseteq> A <+> B" by auto
    1.13 +  hence "finite (Inl ` A :: ('a + 'b) set)" using fin by(rule finite_subset)
    1.14 +  thus "finite A" by(rule finite_imageD)(auto intro: inj_onI)
    1.15 +next
    1.16 +  have "Inr ` B \<subseteq> A <+> B" by auto
    1.17 +  hence "finite (Inr ` B :: ('a + 'b) set)" using fin by(rule finite_subset)
    1.18 +  thus "finite B" by(rule finite_imageD)(auto intro: inj_onI)
    1.19 +qed
    1.20 +
    1.21 +lemma finite_Plus_iff[simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
    1.22 +by(auto intro: finite_PlusD finite_Plus)
    1.23 +
    1.24 +lemma finite_Plus_UNIV_iff[simp]:
    1.25 +  "finite (UNIV :: ('a + 'b) set) =
    1.26 +  (finite (UNIV :: 'a set) & finite (UNIV :: 'b set))"
    1.27 +by(subst UNIV_Plus_UNIV[symmetric])(rule finite_Plus_iff)
    1.28 +
    1.29 +
    1.30  text {* Sigma of finite sets *}
    1.31  
    1.32  lemma finite_SigmaI [simp]:
    1.33 @@ -1563,6 +1586,20 @@
    1.34  qed
    1.35  
    1.36  
    1.37 +lemma setsum_Plus:
    1.38 +  fixes A :: "'a set" and B :: "'b set"
    1.39 +  assumes fin: "finite A" "finite B"
    1.40 +  shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
    1.41 +proof -
    1.42 +  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
    1.43 +  moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
    1.44 +    by(auto intro: finite_imageI)
    1.45 +  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
    1.46 +  moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
    1.47 +  ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
    1.48 +qed
    1.49 +
    1.50 +
    1.51  text {* Commuting outer and inner summation *}
    1.52  
    1.53  lemma swap_inj_on:
    1.54 @@ -2091,6 +2128,10 @@
    1.55  qed
    1.56  
    1.57  
    1.58 +lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
    1.59 +  unfolding UNIV_unit by simp
    1.60 +
    1.61 +
    1.62  subsubsection {* Cardinality of unions *}
    1.63  
    1.64  lemma card_UN_disjoint:
    1.65 @@ -2201,6 +2242,10 @@
    1.66      by (simp add: card_Un_disjoint card_image)
    1.67  qed
    1.68  
    1.69 +lemma card_Plus_conv_if:
    1.70 +  "card (A <+> B) = (if finite A \<and> finite B then card(A) + card(B) else 0)"
    1.71 +by(auto simp: card_def setsum_Plus simp del: setsum_constant)
    1.72 +
    1.73  
    1.74  subsubsection {* Cardinality of the Powerset *}
    1.75  
     2.1 --- a/src/HOL/Fun.thy	Fri May 08 19:20:00 2009 +0200
     2.2 +++ b/src/HOL/Fun.thy	Sat May 09 07:25:22 2009 +0200
     2.3 @@ -412,6 +412,9 @@
     2.4       "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
     2.5  by auto
     2.6  
     2.7 +lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
     2.8 +by(auto intro: ext)
     2.9 +
    2.10  
    2.11  subsection {* @{text override_on} *}
    2.12  
     3.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri May 08 19:20:00 2009 +0200
     3.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat May 09 07:25:22 2009 +0200
     3.3 @@ -55,7 +55,7 @@
     3.4    unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
     3.5  
     3.6  lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
     3.7 -  unfolding insert_None_conv_UNIV [symmetric]
     3.8 +  unfolding UNIV_option_conv
     3.9    apply (subgoal_tac "(None::'a option) \<notin> range Some")
    3.10    apply (simp add: card_image)
    3.11    apply fast
     4.1 --- a/src/HOL/List.thy	Fri May 08 19:20:00 2009 +0200
     4.2 +++ b/src/HOL/List.thy	Sat May 09 07:25:22 2009 +0200
     4.3 @@ -1347,8 +1347,7 @@
     4.4  by (induct xs, auto)
     4.5  
     4.6  lemma update_zip:
     4.7 -  "length xs = length ys ==>
     4.8 -  (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
     4.9 +  "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
    4.10  by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
    4.11  
    4.12  lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
    4.13 @@ -1829,6 +1828,10 @@
    4.14  apply simp_all
    4.15  done
    4.16  
    4.17 +text{* Courtesy of Andreas Lochbihler: *}
    4.18 +lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
    4.19 +by(induct xs) auto
    4.20 +
    4.21  lemma nth_zip [simp]:
    4.22  "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
    4.23  apply (induct ys arbitrary: i xs, simp)
    4.24 @@ -1838,11 +1841,11 @@
    4.25  
    4.26  lemma set_zip:
    4.27  "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
    4.28 -by (simp add: set_conv_nth cong: rev_conj_cong)
    4.29 +by(simp add: set_conv_nth cong: rev_conj_cong)
    4.30  
    4.31  lemma zip_update:
    4.32 -"length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
    4.33 -by (rule sym, simp add: update_zip)
    4.34 +  "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
    4.35 +by(rule sym, simp add: update_zip)
    4.36  
    4.37  lemma zip_replicate [simp]:
    4.38    "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
    4.39 @@ -2577,6 +2580,11 @@
    4.40  apply (simp add: add_commute)
    4.41  done
    4.42  
    4.43 +text{* Courtesy of Andreas Lochbihler: *}
    4.44 +lemma filter_replicate:
    4.45 +  "filter P (replicate n x) = (if P x then replicate n x else [])"
    4.46 +by(induct n) auto
    4.47 +
    4.48  lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
    4.49  by (induct n) auto
    4.50  
     5.1 --- a/src/HOL/Map.thy	Fri May 08 19:20:00 2009 +0200
     5.2 +++ b/src/HOL/Map.thy	Sat May 09 07:25:22 2009 +0200
     5.3 @@ -452,6 +452,9 @@
     5.4  
     5.5  subsection {* @{term [source] dom} *}
     5.6  
     5.7 +lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
     5.8 +by(auto intro!:ext simp: dom_def)
     5.9 +
    5.10  lemma domI: "m a = Some b ==> a : dom m"
    5.11  by(simp add:dom_def)
    5.12  (* declare domI [intro]? *)
    5.13 @@ -593,4 +596,19 @@
    5.14  lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
    5.15  by (clarsimp simp add: map_le_def map_add_def dom_def split: option.splits)
    5.16  
    5.17 +
    5.18 +lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
    5.19 +proof(rule iffI)
    5.20 +  assume "\<exists>v. f = [x \<mapsto> v]"
    5.21 +  thus "dom f = {x}" by(auto split: split_if_asm)
    5.22 +next
    5.23 +  assume "dom f = {x}"
    5.24 +  then obtain v where "f x = Some v" by auto
    5.25 +  hence "[x \<mapsto> v] \<subseteq>\<^sub>m f" by(auto simp add: map_le_def)
    5.26 +  moreover have "f \<subseteq>\<^sub>m [x \<mapsto> v]" using `dom f = {x}` `f x = Some v`
    5.27 +    by(auto simp add: map_le_def)
    5.28 +  ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym)
    5.29 +  thus "\<exists>v. f = [x \<mapsto> v]" by blast
    5.30 +qed
    5.31 +
    5.32  end
     6.1 --- a/src/HOL/Nat_Numeral.thy	Fri May 08 19:20:00 2009 +0200
     6.2 +++ b/src/HOL/Nat_Numeral.thy	Sat May 09 07:25:22 2009 +0200
     6.3 @@ -982,6 +982,9 @@
     6.4  
     6.5  subsubsection{*Various Other Lemmas*}
     6.6  
     6.7 +lemma card_UNIV_bool[simp]: "card (UNIV :: bool set) = 2"
     6.8 +by(simp add: UNIV_bool)
     6.9 +
    6.10  text {*Evens and Odds, for Mutilated Chess Board*}
    6.11  
    6.12  text{*Lemmas for specialist use, NOT as default simprules*}
     7.1 --- a/src/HOL/Option.thy	Fri May 08 19:20:00 2009 +0200
     7.2 +++ b/src/HOL/Option.thy	Sat May 09 07:25:22 2009 +0200
     7.3 @@ -20,6 +20,9 @@
     7.4  only when applied to assumptions, in practice it seems better to give
     7.5  them the uniform iff attribute. *}
     7.6  
     7.7 +lemma inj_Some [simp]: "inj_on Some A"
     7.8 +by (rule inj_onI) simp
     7.9 +
    7.10  lemma option_caseE:
    7.11    assumes c: "(case x of None => P | Some y => Q y)"
    7.12    obtains
    7.13 @@ -27,14 +30,15 @@
    7.14    | (Some) y where "x = Some y" and "Q y"
    7.15    using c by (cases x) simp_all
    7.16  
    7.17 -lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
    7.18 -  by (rule set_ext, case_tac x) auto
    7.19 +lemma UNIV_option_conv: "UNIV = insert None (range Some)"
    7.20 +by(auto intro: classical)
    7.21 +
    7.22 +lemma finite_option_UNIV[simp]:
    7.23 +  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    7.24 +by(auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    7.25  
    7.26  instance option :: (finite) finite proof
    7.27 -qed (simp add: insert_None_conv_UNIV [symmetric])
    7.28 -
    7.29 -lemma inj_Some [simp]: "inj_on Some A"
    7.30 -  by (rule inj_onI) simp
    7.31 +qed (simp add: UNIV_option_conv)
    7.32  
    7.33  
    7.34  subsubsection {* Operations *}
     8.1 --- a/src/HOL/Sum_Type.thy	Fri May 08 19:20:00 2009 +0200
     8.2 +++ b/src/HOL/Sum_Type.thy	Sat May 09 07:25:22 2009 +0200
     8.3 @@ -157,6 +157,8 @@
     8.4  apply auto
     8.5  done
     8.6  
     8.7 +lemma Plus_eq_empty_conv[simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
     8.8 +by(auto)
     8.9  
    8.10  subsection{*The @{term Part} Primitive*}
    8.11