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.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. *}