src/HOL/Finite_Set.thy
 changeset 18423 d7859164447f parent 17782 b3846df9d643 child 18493 343da052b961
```     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