src/HOL/Finite_Set.thy
 changeset 15497 53bca254719a parent 15487 55497029b255 child 15498 3988e90613d4
```     1.1 --- a/src/HOL/Finite_Set.thy	Thu Feb 03 16:45:59 2005 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Fri Feb 04 17:14:42 2005 +0100
1.3 @@ -487,6 +487,15 @@
1.4    thus ?thesis by (subst commute)
1.5  qed
1.6
1.7 +lemma (in ACIf) idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y"
1.8 +proof -
1.9 +  have "x \<cdot> (x \<cdot> y) = (x \<cdot> x) \<cdot> y" by(simp add:assoc)
1.10 +  also have "\<dots> = x \<cdot> y" by(simp add:idem)
1.11 +  finally show ?thesis .
1.12 +qed
1.13 +
1.14 +lemmas (in ACIf) ACI = AC idem idem2
1.15 +
1.16  text{* Instantiation of locales: *}
1.17
1.18  lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
1.19 @@ -1913,6 +1922,74 @@
1.21
1.22
1.23 +subsubsection{* Semi-Lattices *}
1.24 +
1.25 +locale ACIfSL = ACIf +
1.26 +  fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<preceq>" 50)
1.27 +  assumes below_def: "x \<preceq> y = (x\<cdot>y = x)"
1.28 +
1.29 +locale ACIfSLlin = ACIfSL +
1.30 +  assumes lin: "x\<cdot>y \<in> {x,y}"
1.31 +
1.32 +lemma (in ACIfSL) below_refl[simp]: "x \<preceq> x"
1.34 +
1.35 +lemma (in ACIfSL) below_f_conv[simp]: "x \<preceq> y \<cdot> z = (x \<preceq> y \<and> x \<preceq> z)"
1.36 +proof
1.37 +  assume "x \<preceq> y \<cdot> z"
1.38 +  hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
1.39 +  have "x \<cdot> y = x"
1.40 +  proof -
1.41 +    have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
1.42 +    also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
1.43 +    also have "\<dots> = x" by(rule xyzx)
1.44 +    finally show ?thesis .
1.45 +  qed
1.46 +  moreover have "x \<cdot> z = x"
1.47 +  proof -
1.48 +    have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
1.49 +    also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
1.50 +    also have "\<dots> = x" by(rule xyzx)
1.51 +    finally show ?thesis .
1.52 +  qed
1.53 +  ultimately show "x \<preceq> y \<and> x \<preceq> z" by(simp add: below_def)
1.54 +next
1.55 +  assume a: "x \<preceq> y \<and> x \<preceq> z"
1.56 +  hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
1.57 +  have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
1.58 +  also have "x \<cdot> y = x" using a by(simp_all add: below_def)
1.59 +  also have "x \<cdot> z = x" using a by(simp_all add: below_def)
1.60 +  finally show "x \<preceq> y \<cdot> z" by(simp_all add: below_def)
1.61 +qed
1.62 +
1.63 +lemma (in ACIfSLlin) above_f_conv:
1.64 + "x \<cdot> y \<preceq> z = (x \<preceq> z \<or> y \<preceq> z)"
1.65 +proof
1.66 +  assume a: "x \<cdot> y \<preceq> z"
1.67 +  have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
1.68 +  thus "x \<preceq> z \<or> y \<preceq> z"
1.69 +  proof
1.70 +    assume "x \<cdot> y = x" hence "x \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
1.71 +  next
1.72 +    assume "x \<cdot> y = y" hence "y \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
1.73 +  qed
1.74 +next
1.75 +  assume "x \<preceq> z \<or> y \<preceq> z"
1.76 +  thus "x \<cdot> y \<preceq> z"
1.77 +  proof
1.78 +    assume a: "x \<preceq> z"
1.79 +    have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
1.80 +    also have "x \<cdot> z = x" using a by(simp add:below_def)
1.81 +    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
1.82 +  next
1.83 +    assume a: "y \<preceq> z"
1.84 +    have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
1.85 +    also have "y \<cdot> z = y" using a by(simp add:below_def)
1.86 +    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
1.87 +  qed
1.88 +qed
1.89 +
1.90 +
1.91  subsubsection{* Lemmas about {@text fold1} *}
1.92
1.93  lemma (in ACf) fold1_Un:
1.94 @@ -1947,38 +2024,59 @@
1.95    case insert thus ?case using elem by (force simp add:fold1_insert)
1.96  qed
1.97
1.98 -lemma fold1_le:
1.99 -  assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1.100 -  and A: "finite (A)" "A \<noteq> {}" and le: "\<And>x y. f x y \<le> x"
1.101 -  shows "a \<in> A \<Longrightarrow> fold1 f A \<le> a"
1.102 +lemma (in ACIfSL) below_fold1_iff:
1.103 +assumes A: "finite A" "A \<noteq> {}"
1.104 +shows "x \<preceq> fold1 f A = (\<forall>a\<in>A. x \<preceq> a)"
1.105 +using A
1.106 +by(induct rule:finite_ne_induct) simp_all
1.107 +
1.108 +lemma (in ACIfSL) fold1_belowI:
1.109 +assumes A: "finite A" "A \<noteq> {}"
1.110 +shows "a \<in> A \<Longrightarrow> fold1 f A \<preceq> a"
1.111  using A
1.112  proof (induct rule:finite_ne_induct)
1.113 -  case singleton thus ?case by(simp)
1.114 +  case singleton thus ?case by simp
1.115  next
1.116 -  from le have le2: "\<And>x y. f x y \<le> y" by (fastsimp simp:ACf.commute[OF ACf])
1.117 -  case (insert x F) thus ?case using le le2
1.118 -    by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: le order_trans)
1.119 +  case (insert x F)
1.120 +  from insert(4) have "a = x \<or> a \<in> F" by simp
1.121 +  thus ?case
1.122 +  proof
1.123 +    assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
1.124 +  next
1.125 +    assume "a \<in> F"
1.126 +    hence bel: "fold1 op \<cdot> F \<preceq> a" by(rule insert)
1.127 +    have "fold1 op \<cdot> (insert x F) \<cdot> a = x \<cdot> (fold1 op \<cdot> F \<cdot> a)"
1.128 +      using insert by(simp add:below_def ACI)
1.129 +    also have "fold1 op \<cdot> F \<cdot> a = fold1 op \<cdot> F"
1.130 +      using bel  by(simp add:below_def ACI)
1.131 +    also have "x \<cdot> \<dots> = fold1 op \<cdot> (insert x F)"
1.132 +      using insert by(simp add:below_def ACI)
1.133 +    finally show ?thesis  by(simp add:below_def)
1.134 +  qed
1.135  qed
1.136
1.137 -lemma fold1_ge:
1.138 -  assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1.139 -  and A: "finite (A)" "A \<noteq> {}" and ge: "\<And>x y. x \<le> f x y"
1.140 -  shows "a \<in> A \<Longrightarrow> a \<le> fold1 f A"
1.141 +lemma (in ACIfSLlin) fold1_below_iff:
1.142 +assumes A: "finite A" "A \<noteq> {}"
1.143 +shows "fold1 f A \<preceq> x = (\<exists>a\<in>A. a \<preceq> x)"
1.144  using A
1.145 -proof (induct rule:finite_ne_induct)
1.146 -  case singleton thus ?case by(simp)
1.147 -next
1.148 -  from ge have ge2: "\<And>x y. y \<le> f x y" by (fastsimp simp:ACf.commute[OF ACf])
1.149 -  case (insert x F) thus ?case using ge ge2
1.150 -    by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: ge order_trans)
1.151 -qed
1.153
1.154
1.155  subsection{*Min and Max*}
1.156
1.157  text{* As an application of @{text fold1} we define the minimal and
1.158 -maximal element of a (non-empty) set over a linear order. First we
1.159 -show that @{text min} and @{text max} are ACI: *}
1.160 +maximal element of a (non-empty) set over a linear order. *}
1.161 +
1.162 +constdefs
1.163 +  Min :: "('a::linorder)set => 'a"
1.164 +  "Min  ==  fold1 min"
1.165 +
1.166 +  Max :: "('a::linorder)set => 'a"
1.167 +  "Max  ==  fold1 max"
1.168 +
1.169 +
1.170 +text{* Before we can do anything, we need to show that @{text min} and
1.171 +@{text max} are ACI and the ordering is linear: *}
1.172
1.173  lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1.174  apply(rule ACf.intro)
1.175 @@ -2002,14 +2100,39 @@
1.176  apply(auto simp:max_def)
1.177  done
1.178
1.179 -text{* Now we make the definitions: *}
1.180 +lemma ACIfSL_min: "ACIfSL(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
1.181 +apply(rule ACIfSL.intro)
1.182 +apply(rule ACf_min)
1.183 +apply(rule ACIf.axioms[OF ACIf_min])
1.184 +apply(rule ACIfSL_axioms.intro)
1.185 +apply(auto simp:min_def)
1.186 +done
1.187 +
1.188 +lemma ACIfSLlin_min: "ACIfSLlin(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
1.189 +apply(rule ACIfSLlin.intro)
1.190 +apply(rule ACf_min)
1.191 +apply(rule ACIf.axioms[OF ACIf_min])
1.192 +apply(rule ACIfSL.axioms[OF ACIfSL_min])
1.193 +apply(rule ACIfSLlin_axioms.intro)
1.194 +apply(auto simp:min_def)
1.195 +done
1.196
1.197 -constdefs
1.198 -  Min :: "('a::linorder)set => 'a"
1.199 -  "Min  ==  fold1 min"
1.200 +lemma ACIfSL_max: "ACIfSL(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
1.201 +apply(rule ACIfSL.intro)
1.202 +apply(rule ACf_max)
1.203 +apply(rule ACIf.axioms[OF ACIf_max])
1.204 +apply(rule ACIfSL_axioms.intro)
1.205 +apply(auto simp:max_def)
1.206 +done
1.207
1.208 -  Max :: "('a::linorder)set => 'a"
1.209 -  "Max  ==  fold1 max"
1.210 +lemma ACIfSLlin_max: "ACIfSLlin(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
1.211 +apply(rule ACIfSLlin.intro)
1.212 +apply(rule ACf_max)
1.213 +apply(rule ACIf.axioms[OF ACIf_max])
1.214 +apply(rule ACIfSL.axioms[OF ACIfSL_max])
1.215 +apply(rule ACIfSLlin_axioms.intro)
1.216 +apply(auto simp:max_def)
1.217 +done
1.218
1.219  text{* Now we instantiate the recursion equations and declare them
1.220  simplification rules: *}
1.221 @@ -2033,9 +2156,25 @@
1.222  by(fastsimp simp: Max_def max_def)
1.223
1.224  lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
1.225 -by(simp add: Min_def fold1_le[OF ACf_min] min_le_iff_disj)
1.226 +by(simp add: Min_def ACIfSL.fold1_belowI[OF ACIfSL_min])
1.227
1.228  lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
1.229 -by(simp add: Max_def fold1_ge[OF ACf_max] le_max_iff_disj)
1.230 +by(simp add: Max_def ACIfSL.fold1_belowI[OF ACIfSL_max])
1.231 +
1.232 +lemma Min_ge_iff[simp]:
1.233 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
1.234 +by(simp add: Min_def ACIfSL.below_fold1_iff[OF ACIfSL_min])
1.235 +
1.236 +lemma Max_le_iff[simp]:
1.237 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
1.238 +by(simp add: Max_def ACIfSL.below_fold1_iff[OF ACIfSL_max])
1.239 +
1.240 +lemma Min_le_iff:
1.241 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
1.242 +by(simp add: Min_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_min])
1.243 +
1.244 +lemma Max_ge_iff:
1.245 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
1.246 +by(simp add: Max_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_max])
1.247
1.248  end
```