*** empty log message ***
authornipkow
Fri Dec 19 04:28:45 2003 +0100 (2003-12-19)
changeset 143026c24235e8d5d
parent 14301 48dc606749bd
child 14303 995212a00a50
*** empty log message ***
src/HOL/Finite_Set.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Dec 18 15:06:24 2003 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Dec 19 04:28:45 2003 +0100
     1.3 @@ -431,7 +431,9 @@
     1.4    by (simp add: insert_absorb)
     1.5  
     1.6  lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
     1.7 -by (rule_tac t = A in insert_Diff [THEN subst], assumption, simp)
     1.8 +apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
     1.9 +apply(simp del:insert_Diff_single)
    1.10 +done
    1.11  
    1.12  lemma card_Diff_singleton:
    1.13      "finite A ==> x: A ==> card (A - {x}) = card A - 1"
    1.14 @@ -860,7 +862,7 @@
    1.15    apply (erule ssubst)
    1.16    apply (drule spec)
    1.17    apply (erule (1) notE impE)
    1.18 -  apply (simp add: Ball_def)
    1.19 +  apply (simp add: Ball_def del:insert_Diff_single)
    1.20    done
    1.21  
    1.22  subsubsection{* Min and Max of finite linearly ordered sets *}
     2.1 --- a/src/HOL/List.thy	Thu Dec 18 15:06:24 2003 +0100
     2.2 +++ b/src/HOL/List.thy	Fri Dec 19 04:28:45 2003 +0100
     2.3 @@ -758,6 +758,23 @@
     2.4  lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
     2.5  by (induct xs) auto
     2.6  
     2.7 +lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
     2.8 +by(simp add:last.simps)
     2.9 +
    2.10 +lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
    2.11 +by(simp add:last.simps)
    2.12 +
    2.13 +lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
    2.14 +by (induct xs) (auto)
    2.15 +
    2.16 +lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
    2.17 +by(simp add:last_append)
    2.18 +
    2.19 +lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
    2.20 +by(simp add:last_append)
    2.21 +
    2.22 +
    2.23 +
    2.24  lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
    2.25  by (induct xs rule: rev_induct) auto
    2.26  
    2.27 @@ -1111,6 +1128,10 @@
    2.28    "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
    2.29    by (simp add: list_all2_conv_all_nth)
    2.30  
    2.31 +lemma list_all2_nthD2:
    2.32 +  "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
    2.33 +  by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
    2.34 +
    2.35  lemma list_all2_map1: 
    2.36    "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
    2.37    by (simp add: list_all2_conv_all_nth)
    2.38 @@ -1131,7 +1152,16 @@
    2.39    "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
    2.40    by (simp add: list_all2_lengthD list_all2_update_cong)
    2.41  
    2.42 -lemma list_all2_dropI [intro?]:
    2.43 +lemma list_all2_takeI [simp,intro?]:
    2.44 +  "\<And>n ys. list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
    2.45 +  apply (induct xs)
    2.46 +   apply simp
    2.47 +  apply (clarsimp simp add: list_all2_Cons1)
    2.48 +  apply (case_tac n)
    2.49 +  apply auto
    2.50 +  done
    2.51 +
    2.52 +lemma list_all2_dropI [simp,intro?]:
    2.53    "\<And>n bs. list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
    2.54    apply (induct as, simp)
    2.55    apply (clarsimp simp add: list_all2_Cons1)
     3.1 --- a/src/HOL/Nat.thy	Thu Dec 18 15:06:24 2003 +0100
     3.2 +++ b/src/HOL/Nat.thy	Fri Dec 19 04:28:45 2003 +0100
     3.3 @@ -268,6 +268,12 @@
     3.4    apply (blast intro: Suc_mono less_SucI elim: lessE)
     3.5    done
     3.6  
     3.7 +text {* "Less than" is antisymmetric, sort of *}
     3.8 +lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
     3.9 +apply(simp only:less_Suc_eq)
    3.10 +apply blast
    3.11 +done
    3.12 +
    3.13  lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
    3.14    using less_linear by blast
    3.15  
     4.1 --- a/src/HOL/Set.thy	Thu Dec 18 15:06:24 2003 +0100
     4.2 +++ b/src/HOL/Set.thy	Fri Dec 19 04:28:45 2003 +0100
     4.3 @@ -895,6 +895,9 @@
     4.4    apply (erule insertI2)
     4.5    done
     4.6  
     4.7 +lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
     4.8 +by blast
     4.9 +
    4.10  lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
    4.11    by blast
    4.12  
    4.13 @@ -961,6 +964,9 @@
    4.14  lemma Diff_subset: "A - B \<subseteq> A"
    4.15    by blast
    4.16  
    4.17 +lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
    4.18 +by blast
    4.19 +
    4.20  
    4.21  text {* \medskip Monotonicity. *}
    4.22  
    4.23 @@ -1052,6 +1058,9 @@
    4.24  lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
    4.25    by blast
    4.26  
    4.27 +lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
    4.28 +by blast
    4.29 +
    4.30  lemma insert_disjoint[simp]:
    4.31   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
    4.32  by blast
    4.33 @@ -1495,6 +1504,9 @@
    4.34  lemma Diff_cancel [simp]: "A - A = {}"
    4.35    by blast
    4.36  
    4.37 +lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"
    4.38 +by blast
    4.39 +
    4.40  lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
    4.41    by (blast elim: equalityE)
    4.42  
    4.43 @@ -1524,6 +1536,9 @@
    4.44  lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
    4.45    by blast
    4.46  
    4.47 +lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
    4.48 +by blast
    4.49 +
    4.50  lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
    4.51    by blast
    4.52