added new lemmas
authornipkow
Tue Sep 06 14:25:16 2011 +0200 (2011-09-06)
changeset 44744bdf8eb8f126b
parent 44743 804dfa6d35b6
child 44747 ab7522fbe1a2
child 44751 f523923d8182
child 44850 a6095c96a89b
added new lemmas
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Sep 06 11:31:01 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Sep 06 14:25:16 2011 +0200
     1.3 @@ -2054,6 +2054,11 @@
     1.4   apply(auto intro:ccontr)
     1.5  done
     1.6  
     1.7 +lemma card_le_Suc_iff: "finite A \<Longrightarrow>
     1.8 +  Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
     1.9 +by (fastsimp simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
    1.10 +  dest: subset_singletonD split: nat.splits if_splits)
    1.11 +
    1.12  lemma finite_fun_UNIVD2:
    1.13    assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
    1.14    shows "finite (UNIV :: 'b set)"
     2.1 --- a/src/HOL/Fun.thy	Tue Sep 06 11:31:01 2011 +0200
     2.2 +++ b/src/HOL/Fun.thy	Tue Sep 06 14:25:16 2011 +0200
     2.3 @@ -612,6 +612,10 @@
     2.4  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
     2.5  by (auto intro: ext)
     2.6  
     2.7 +lemma UNION_fun_upd:
     2.8 +  "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
     2.9 +by (auto split: if_splits)
    2.10 +
    2.11  
    2.12  subsection {* @{text override_on} *}
    2.13  
     3.1 --- a/src/HOL/Set.thy	Tue Sep 06 11:31:01 2011 +0200
     3.2 +++ b/src/HOL/Set.thy	Tue Sep 06 14:25:16 2011 +0200
     3.3 @@ -785,6 +785,26 @@
     3.4  lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
     3.5  by auto
     3.6  
     3.7 +lemma insert_eq_iff: assumes "a \<notin> A" "b \<notin> B"
     3.8 +shows "insert a A = insert b B \<longleftrightarrow>
     3.9 +  (if a=b then A=B else \<exists>C. A = insert b C \<and> b \<notin> C \<and> B = insert a C \<and> a \<notin> C)"
    3.10 +  (is "?L \<longleftrightarrow> ?R")
    3.11 +proof
    3.12 +  assume ?L
    3.13 +  show ?R
    3.14 +  proof cases
    3.15 +    assume "a=b" with assms `?L` show ?R by (simp add: insert_ident)
    3.16 +  next
    3.17 +    assume "a\<noteq>b"
    3.18 +    let ?C = "A - {b}"
    3.19 +    have "A = insert b ?C \<and> b \<notin> ?C \<and> B = insert a ?C \<and> a \<notin> ?C"
    3.20 +      using assms `?L` `a\<noteq>b` by auto
    3.21 +    thus ?R using `a\<noteq>b` by auto
    3.22 +  qed
    3.23 +next
    3.24 +  assume ?R thus ?L by(auto split: if_splits)
    3.25 +qed
    3.26 +
    3.27  subsubsection {* Singletons, using insert *}
    3.28  
    3.29  lemma singletonI [intro!,no_atp]: "a : {a}"