author nipkow Fri Dec 16 16:59:32 2005 +0100 (2005-12-16) changeset 18423 d7859164447f parent 18422 875451c9d253 child 18424 a37f06555c07
new lemmas
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Fri Dec 16 16:00:58 2005 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Fri Dec 16 16:59:32 2005 +0100
1.3 @@ -177,7 +177,7 @@
1.4    qed
1.5  qed
1.6
1.7 -lemma finite_Collect_subset: "finite A \<Longrightarrow> finite{x \<in> A. P x}"
1.8 +lemma finite_Collect_subset[simp]: "finite A \<Longrightarrow> finite{x \<in> A. P x}"
1.9  using finite_subset[of "{x \<in> A. P x}" "A"] by blast
1.10
1.11  lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
1.12 @@ -2108,6 +2108,28 @@
1.14
1.15
1.16 +lemma (in ACIfSLlin) fold1_antimono:
1.17 +assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
1.18 +shows "fold1 f B \<sqsubseteq> fold1 f A"
1.19 +proof(cases)
1.20 +  assume "A = B" thus ?thesis by simp
1.21 +next
1.22 +  assume "A \<noteq> B"
1.23 +  have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
1.24 +  have "fold1 f B = fold1 f (A \<union> (B-A))" by(subst B)(rule refl)
1.25 +  also have "\<dots> = f (fold1 f A) (fold1 f (B-A))"
1.26 +  proof -
1.27 +    have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
1.28 +    moreover have "finite(B-A)" by(blast intro:finite_Diff prems)
1.29 +    moreover have "(B-A) \<noteq> {}" using prems by blast
1.30 +    moreover have "A Int (B-A) = {}" using prems by blast
1.31 +    ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
1.32 +  qed
1.33 +  also have "\<dots> \<sqsubseteq> fold1 f A" by(simp add: above_f_conv)
1.34 +  finally show ?thesis .
1.35 +qed
1.36 +
1.37 +
1.38  subsubsection{* Lattices *}
1.39
1.40  locale Lattice = lattice +
1.41 @@ -2185,27 +2207,30 @@
1.42  by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
1.43
1.44
1.45 -lemma (in Distrib_Lattice) sup_Inf1_distrib:
1.46 -assumes A: "finite A" "A \<noteq> {}"
1.47 -shows "(x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
1.48 -using A
1.49 -proof (induct rule: finite_ne_induct)
1.50 -  case singleton thus ?case by(simp add:Inf_def)
1.51 +lemma (in ACIf) hom_fold1_commute:
1.52 +assumes hom: "!!x y. h(f x y) = f (h x) (h y)"
1.53 +and N: "finite N" "N \<noteq> {}" shows "h(fold1 f N) = fold1 f (h ` N)"
1.54 +using N proof (induct rule: finite_ne_induct)
1.55 +  case singleton thus ?case by simp
1.56  next
1.57 -  case (insert y A)
1.58 -  have fin: "finite {x \<squnion> a |a. a \<in> A}"
1.59 -    by(fast intro: finite_surj[where f = "%a. x \<squnion> a", OF insert(1)])
1.60 -  have "x \<squnion> \<Sqinter> (insert y A) = x \<squnion> (y \<sqinter> \<Sqinter> A)"
1.61 -    using insert by(simp add:ACf.fold1_insert_def[OF ACf_inf Inf_def])
1.62 -  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> \<Sqinter> A)" by(rule sup_inf_distrib1)
1.63 -  also have "x \<squnion> \<Sqinter> A = \<Sqinter>{x \<squnion> a|a. a \<in> A}" using insert by simp
1.64 -  also have "(x \<squnion> y) \<sqinter> \<dots> = \<Sqinter> (insert (x \<squnion> y) {x \<squnion> a |a. a \<in> A})"
1.65 -    using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def fin])
1.66 -  also have "insert (x\<squnion>y) {x\<squnion>a |a. a \<in> A} = {x\<squnion>a |a. a \<in> insert y A}"
1.67 -    by blast
1.68 +  case (insert n N)
1.69 +  have "h(fold1 f (insert n N)) = h(f n (fold1 f N))" using insert by(simp)
1.70 +  also have "\<dots> = f (h n) (h(fold1 f N))" by(rule hom)
1.71 +  also have "h(fold1 f N) = fold1 f (h ` N)" by(rule insert)
1.72 +  also have "f (h n) \<dots> = fold1 f (insert (h n) (h ` N))"
1.73 +    using insert by(simp)
1.74 +  also have "insert (h n) (h ` N) = h ` insert n N" by simp
1.75    finally show ?case .
1.76  qed
1.77
1.78 +lemma (in Distrib_Lattice) sup_Inf1_distrib:
1.79 + "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
1.81 +  ACIf.hom_fold1_commute[OF ACIf_inf, where h="sup x", OF sup_inf_distrib1])
1.82 +apply(rule arg_cong, blast)
1.83 +done
1.84 +
1.85 +
1.86  lemma (in Distrib_Lattice) sup_Inf2_distrib:
1.87  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
1.88  shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
1.89 @@ -2239,6 +2264,47 @@
1.90  qed
1.91
1.92
1.93 +lemma (in Distrib_Lattice) inf_Sup1_distrib:
1.94 + "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<sqinter> \<Squnion>A) = \<Squnion>{x \<sqinter> a|a. a \<in> A}"
1.96 +  ACIf.hom_fold1_commute[OF ACIf_sup, where h="inf x", OF inf_sup_distrib1])
1.97 +apply(rule arg_cong, blast)
1.98 +done
1.99 +
1.100 +
1.101 +lemma (in Distrib_Lattice) inf_Sup2_distrib:
1.102 +assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
1.103 +shows "(\<Squnion>A \<sqinter> \<Squnion>B) = \<Squnion>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
1.104 +using A
1.105 +proof (induct rule: finite_ne_induct)
1.106 +  case singleton thus ?case
1.107 +    by(simp add: inf_Sup1_distrib[OF B] fold1_singleton_def[OF Sup_def])
1.108 +next
1.109 +  case (insert x A)
1.110 +  have finB: "finite {x \<sqinter> b |b. b \<in> B}"
1.111 +    by(fast intro: finite_surj[where f = "%b. x \<sqinter> b", OF B(1)])
1.112 +  have finAB: "finite {a \<sqinter> b |a b. a \<in> A \<and> b \<in> B}"
1.113 +  proof -
1.114 +    have "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<sqinter> b})"
1.115 +      by blast
1.116 +    thus ?thesis by(simp add: insert(1) B(1))
1.117 +  qed
1.118 +  have ne: "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
1.119 +  have "\<Squnion>(insert x A) \<sqinter> \<Squnion>B = (x \<squnion> \<Squnion>A) \<sqinter> \<Squnion>B"
1.120 +    using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_sup Sup_def])
1.121 +  also have "\<dots> = (x \<sqinter> \<Squnion>B) \<squnion> (\<Squnion>A \<sqinter> \<Squnion>B)" by(rule inf_sup_distrib2)
1.122 +  also have "\<dots> = \<Squnion>{x \<sqinter> b|b. b \<in> B} \<squnion> \<Squnion>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
1.123 +    using insert by(simp add:inf_Sup1_distrib[OF B])
1.124 +  also have "\<dots> = \<Squnion>({x\<sqinter>b |b. b \<in> B} \<union> {a\<sqinter>b |a b. a \<in> A \<and> b \<in> B})"
1.125 +    (is "_ = \<Squnion>?M")
1.126 +    using B insert
1.127 +    by(simp add:Sup_def ACIf.fold1_Un2[OF ACIf_sup finB _ finAB ne])
1.128 +  also have "?M = {a \<sqinter> b |a b. a \<in> insert x A \<and> b \<in> B}"
1.129 +    by blast
1.130 +  finally show ?case .
1.131 +qed
1.132 +
1.133 +
1.134  subsection{*Min and Max*}
1.135
1.136  text{* As an application of @{text fold1} we define the minimal and
1.137 @@ -2338,6 +2404,12 @@
1.138  using max.fold1_in
1.139  by(fastsimp simp: Max_def max_def)
1.140
1.141 +lemma Min_antimono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<le> Min M"
1.143 +
1.144 +lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<le> Max N"
1.146 +
1.147  lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
1.149
1.150 @@ -2360,6 +2432,46 @@
1.151    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
1.153
1.154 +lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
1.155 +  \<Longrightarrow> Min (A \<union> B) = min (Min A) (Min B)"
1.157 +
1.158 +lemma Max_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
1.159 +  \<Longrightarrow> Max (A \<union> B) = max (Max A) (Max B)"
1.161 +
1.162 +
1.163 +lemma hom_Min_commute:
1.164 + "(!!x y::'a::linorder. h(min x y) = min (h x) (h y::'a))
1.165 +  \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h(Min N) = Min(h ` N)"
1.167 +
1.168 +lemma hom_Max_commute:
1.169 + "(!!x y::'a::linorder. h(max x y) = max (h x) (h y::'a))
1.170 +  \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h(Max N) = Max(h ` N)"
1.172 +
1.173 +
1.175 + shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k + Min N = Min {k+m|m. m \<in> N}"
1.176 +apply(subgoal_tac "!!x y. k + min x y = min (k + x) (k + y)")
1.177 +using hom_Min_commute[of "op + k" N]
1.178 +apply simp apply(rule arg_cong[where f = Min]) apply blast
1.181 +done
1.182 +
1.184 + shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k + Max N = Max {k+m|m. m \<in> N}"
1.185 +apply(subgoal_tac "!!x y. k + max x y = max (k + x) (k + y)")
1.186 +using hom_Max_commute[of "op + k" N]
1.187 +apply simp apply(rule arg_cong[where f = Max]) apply blast
1.190 +done
1.191 +
1.192 +
1.193 +
1.194  subsection {* Properties of axclass @{text finite} *}
1.195
1.196  text{* Many of these are by Brian Huffman. *}
```
```     2.1 --- a/src/HOL/List.thy	Fri Dec 16 16:00:58 2005 +0100
2.2 +++ b/src/HOL/List.thy	Fri Dec 16 16:59:32 2005 +0100
2.3 @@ -628,6 +628,9 @@
2.4
2.5  lemmas rev_cases = rev_exhaust
2.6
2.7 +lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
2.8 +by(rule rev_cases[of xs]) auto
2.9 +
2.10
2.11  subsubsection {* @{text set} *}
2.12
2.13 @@ -734,6 +737,10 @@
2.14  lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
2.15  by (induct xs) (auto simp add: le_SucI)
2.16
2.17 +lemma sum_length_filter_compl:
2.18 +  "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
2.19 +by(induct xs) simp_all
2.20 +
2.21  lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
2.22  by (induct xs) auto
2.23
2.24 @@ -906,6 +913,9 @@
2.25  apply (case_tac n, auto)
2.26  done
2.27
2.28 +lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
2.29 +by(cases xs) simp_all
2.30 +
2.31
2.32  lemma list_eq_iff_nth_eq:
2.33   "!!ys. (xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
2.34 @@ -1202,6 +1212,9 @@
2.35  apply (case_tac xs, auto)
2.36  done
2.37
2.38 +lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
2.40 +
2.41  lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs"
2.42  by(induct xs)(auto simp:take_Cons split:nat.split)
2.43
2.44 @@ -1322,6 +1335,14 @@
2.45  apply auto
2.46  done
2.47
2.48 +lemma takeWhile_not_last:
2.49 + "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
2.50 +apply(induct xs)
2.51 + apply simp
2.52 +apply(case_tac xs)
2.53 +apply(auto)
2.54 +done
2.55 +
2.56  lemma takeWhile_cong [recdef_cong]:
2.57    "[| l = k; !!x. x : set l ==> P x = Q x |]
2.58    ==> takeWhile P l = takeWhile Q k"
2.59 @@ -2044,6 +2065,12 @@
2.61  done
2.62
2.63 +lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
2.64 +apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
2.65 +apply(subgoal_tac "length xs \<noteq> 0")
2.66 + prefer 2 apply simp
2.67 +using mod_less_divisor[of "length xs" n] by arith
2.68 +
2.69
2.70  subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
2.71
2.72 @@ -2335,7 +2362,7 @@
2.73    "lexn r n =
2.74      {(xs,ys). length xs = n \<and> length ys = n \<and>
2.75      (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
2.76 -apply (induct n, simp, blast)
2.77 +apply (induct n, simp)
2.78  apply (simp add: image_Collect lex_prod_def, safe, blast)
2.79   apply (rule_tac x = "ab # xys" in exI, simp)
2.80  apply (case_tac xys, simp_all, blast)
```
```     3.1 --- a/src/HOL/Set.thy	Fri Dec 16 16:00:58 2005 +0100
3.2 +++ b/src/HOL/Set.thy	Fri Dec 16 16:59:32 2005 +0100
3.3 @@ -1120,7 +1120,10 @@
3.4    by (unfold psubset_def) blast
3.5
3.6  lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
3.7 -  by auto
3.8 +by blast
3.9 +
3.10 +lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)"
3.11 +by blast
3.12
3.13  lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
3.14    by blast
```