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.20  by(simp add:fold1_insert2)
    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.33 +by(simp add: below_def idem)
    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.152 +by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
   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