new lemmas
authornipkow
Fri Dec 16 16:59:32 2005 +0100 (2005-12-16)
changeset 18423d7859164447f
parent 18422 875451c9d253
child 18424 a37f06555c07
new lemmas
src/HOL/Finite_Set.thy
src/HOL/List.thy
src/HOL/Set.thy
     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.13  by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
    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.80 +apply(simp add:Inf_def image_def
    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.95 +apply(simp add:Sup_def image_def
    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.142 +by(simp add:Finite_Set.Min_def min.fold1_antimono)
   1.143 +
   1.144 +lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<le> Max N"
   1.145 +by(simp add:Max_def max.fold1_antimono)
   1.146 +
   1.147  lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
   1.148  by(simp add: Min_def min.fold1_belowI)
   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.152  by(simp add: Max_def max.fold1_below_iff)
   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.156 +by(simp add:Min_def min.f.fold1_Un2)
   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.160 +by(simp add:Max_def max.f.fold1_Un2)
   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.166 +by(simp add:Finite_Set.Min_def min.hom_fold1_commute)
   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.171 +by(simp add:Max_def max.hom_fold1_commute)
   1.172 +
   1.173 +
   1.174 +lemma add_Min_commute: fixes k::"'a::{pordered_ab_semigroup_add,linorder}"
   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.179 +apply(simp add:min_def linorder_not_le)
   1.180 +apply(blast intro:order.antisym order_less_imp_le add_left_mono)
   1.181 +done
   1.182 +
   1.183 +lemma add_Max_commute: fixes k::"'a::{pordered_ab_semigroup_add,linorder}"
   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.188 +apply(simp add:max_def linorder_not_le)
   1.189 +apply(blast intro:order.antisym order_less_imp_le add_left_mono)
   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.39 +by(simp add: hd_conv_nth)
    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.60  apply(simp add:rotate_drop_take rev_drop rev_take)
    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