fold and fol1 changes
authornipkow
Wed Feb 02 09:15:40 2005 +0100 (2005-02-02)
changeset 154842636ec211ec8
parent 15483 704b3ce6d0f7
child 15485 e93a3badc2bc
fold and fol1 changes
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 02 08:53:03 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Feb 02 09:15:40 2005 +0100
     1.3 @@ -58,6 +58,24 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma finite_ne_induct[case_names singleton insert, consumes 2]:
     1.8 +assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
     1.9 + \<lbrakk> \<And>x. P{x};
    1.10 +   \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
    1.11 + \<Longrightarrow> P F"
    1.12 +using fin
    1.13 +proof induct
    1.14 +  case empty thus ?case by simp
    1.15 +next
    1.16 +  case (insert x F)
    1.17 +  show ?case
    1.18 +  proof cases
    1.19 +    assume "F = {}" thus ?thesis using insert(4) by simp
    1.20 +  next
    1.21 +    assume "F \<noteq> {}" thus ?thesis using insert by blast
    1.22 +  qed
    1.23 +qed
    1.24 +
    1.25  lemma finite_subset_induct [consumes 2, case_names empty insert]:
    1.26    "finite F ==> F \<subseteq> A ==>
    1.27      P {} ==> (!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)) ==>
    1.28 @@ -745,6 +763,10 @@
    1.29    with finA show ?thesis by simp
    1.30  qed
    1.31  
    1.32 +lemma (in ACIf) foldI_conv_id:
    1.33 +  "finite A \<Longrightarrow> fold f g z A = fold f id z (g ` A)"
    1.34 +by(erule finite_induct)(simp_all add: fold_insert2 del: fold_insert)
    1.35 +
    1.36  subsubsection{*Lemmas about @{text fold}*}
    1.37  
    1.38  lemma (in ACf) fold_commute:
    1.39 @@ -1850,7 +1872,7 @@
    1.40      cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality)
    1.41  done
    1.42  
    1.43 -lemma (in ACIf) fold1_insert2:
    1.44 +lemma (in ACIf) fold1_insert2[simp]:
    1.45  assumes finA: "finite A" and nonA: "A \<noteq> {}"
    1.46  shows "fold1 f (insert a A) = f a (fold1 f A)"
    1.47  proof cases
    1.48 @@ -1876,7 +1898,6 @@
    1.49    with finA nonA show ?thesis by(simp add:fold1_insert)
    1.50  qed
    1.51  
    1.52 -
    1.53  text{* Now the recursion rules for definitions: *}
    1.54  
    1.55  lemma fold1_singleton_def: "g \<equiv> fold1 f \<Longrightarrow> g {a} = a"
    1.56 @@ -1891,6 +1912,67 @@
    1.57  by(simp add:fold1_insert2)
    1.58  
    1.59  
    1.60 +subsubsection{* Lemmas about {@text fold1} *}
    1.61 +
    1.62 +lemma (in ACf) fold1_Un:
    1.63 +assumes A: "finite A" "A \<noteq> {}"
    1.64 +shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
    1.65 +       fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
    1.66 +using A
    1.67 +proof(induct rule:finite_ne_induct)
    1.68 +  case singleton thus ?case by(simp add:fold1_insert)
    1.69 +next
    1.70 +  case insert thus ?case by (simp add:fold1_insert assoc)
    1.71 +qed
    1.72 +
    1.73 +lemma (in ACIf) fold1_Un2:
    1.74 +assumes A: "finite A" "A \<noteq> {}"
    1.75 +shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
    1.76 +       fold1 f (A Un B) = f (fold1 f A) (fold1 f B)"
    1.77 +using A
    1.78 +proof(induct rule:finite_ne_induct)
    1.79 +  case singleton thus ?case by(simp add:fold1_insert2)
    1.80 +next
    1.81 +  case insert thus ?case by (simp add:fold1_insert2 assoc)
    1.82 +qed
    1.83 +
    1.84 +lemma (in ACf) fold1_in:
    1.85 +  assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x\<cdot>y \<in> {x,y}"
    1.86 +  shows "fold1 f A \<in> A"
    1.87 +using A
    1.88 +proof (induct rule:finite_ne_induct)
    1.89 +  case singleton thus ?case by(simp)
    1.90 +next
    1.91 +  case insert thus ?case using elem by (force simp add:fold1_insert)
    1.92 +qed
    1.93 +
    1.94 +lemma fold1_le:
    1.95 +  assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.96 +  and A: "finite (A)" "A \<noteq> {}" and le: "\<And>x y. f x y \<le> x"
    1.97 +  shows "a \<in> A \<Longrightarrow> fold1 f A \<le> a"
    1.98 +using A
    1.99 +proof (induct rule:finite_ne_induct)
   1.100 +  case singleton thus ?case by(simp)
   1.101 +next
   1.102 +  from le have le2: "\<And>x y. f x y \<le> y" by (fastsimp simp:ACf.commute[OF ACf])
   1.103 +  case (insert x F) thus ?case using le le2
   1.104 +    by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: le order_trans)
   1.105 +qed
   1.106 +
   1.107 +lemma fold1_ge:
   1.108 +  assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
   1.109 +  and A: "finite (A)" "A \<noteq> {}" and ge: "\<And>x y. x \<le> f x y"
   1.110 +  shows "a \<in> A \<Longrightarrow> a \<le> fold1 f A"
   1.111 +using A
   1.112 +proof (induct rule:finite_ne_induct)
   1.113 +  case singleton thus ?case by(simp)
   1.114 +next
   1.115 +  from ge have ge2: "\<And>x y. y \<le> f x y" by (fastsimp simp:ACf.commute[OF ACf])
   1.116 +  case (insert x F) thus ?case using ge ge2
   1.117 +    by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: ge order_trans)
   1.118 +qed
   1.119 +
   1.120 +
   1.121  subsection{*Min and Max*}
   1.122  
   1.123  text{* As an application of @{text fold1} we define the minimal and
   1.124 @@ -1937,71 +2019,22 @@
   1.125    fold1_singleton_def[OF Max_def, simp]
   1.126    ACIf.fold1_insert2_def[OF ACIf_max Max_def, simp]
   1.127  
   1.128 -text{* Now we prove some properties by induction: *}
   1.129 +text{* Now we instantiate some @{text fold1} properties: *}
   1.130  
   1.131  lemma Min_in [simp]:
   1.132 -  assumes a: "finite S"
   1.133 -  shows "S \<noteq> {} \<Longrightarrow> Min S \<in> S"
   1.134 -using a
   1.135 -proof induct
   1.136 -  case empty thus ?case by simp
   1.137 -next
   1.138 -  case (insert x S)
   1.139 -  show ?case
   1.140 -  proof cases
   1.141 -    assume "S = {}" thus ?thesis by simp
   1.142 -  next
   1.143 -    assume "S \<noteq> {}" thus ?thesis using insert by (simp add:min_def)
   1.144 -  qed
   1.145 -qed
   1.146 -
   1.147 -lemma Min_le [simp]:
   1.148 -  assumes a: "finite S"
   1.149 -  shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> Min S \<le> x"
   1.150 -using a
   1.151 -proof induct
   1.152 -  case empty thus ?case by simp
   1.153 -next
   1.154 -  case (insert y S)
   1.155 -  show ?case
   1.156 -  proof cases
   1.157 -    assume "S = {}" thus ?thesis using insert by simp
   1.158 -  next
   1.159 -    assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:min_def)
   1.160 -  qed
   1.161 -qed
   1.162 +  shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
   1.163 +using ACf.fold1_in[OF ACf_min]
   1.164 +by(fastsimp simp: Min_def min_def)
   1.165  
   1.166  lemma Max_in [simp]:
   1.167 -  assumes a: "finite S"
   1.168 -  shows "S \<noteq> {} \<Longrightarrow> Max S \<in> S"
   1.169 -using a
   1.170 -proof induct
   1.171 -  case empty thus ?case by simp
   1.172 -next
   1.173 -  case (insert x S)
   1.174 -  show ?case
   1.175 -  proof cases
   1.176 -    assume "S = {}" thus ?thesis by simp
   1.177 -  next
   1.178 -    assume "S \<noteq> {}" thus ?thesis using insert by (simp add:max_def)
   1.179 -  qed
   1.180 -qed
   1.181 +  shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
   1.182 +using ACf.fold1_in[OF ACf_max]
   1.183 +by(fastsimp simp: Max_def max_def)
   1.184  
   1.185 -lemma Max_le [simp]:
   1.186 -  assumes a: "finite S"
   1.187 -  shows "\<lbrakk> S \<noteq> {}; x \<in> S \<rbrakk> \<Longrightarrow> x \<le> Max S"
   1.188 -using a
   1.189 -proof induct
   1.190 -  case empty thus ?case by simp
   1.191 -next
   1.192 -  case (insert y S)
   1.193 -  show ?case
   1.194 -  proof cases
   1.195 -    assume "S = {}" thus ?thesis using insert by simp
   1.196 -  next
   1.197 -    assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:max_def)
   1.198 -  qed
   1.199 -qed
   1.200 +lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
   1.201 +by(simp add: Min_def fold1_le[OF ACf_min] min_le_iff_disj)
   1.202  
   1.203 +lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
   1.204 +by(simp add: Max_def fold1_ge[OF ACf_max] le_max_iff_disj)
   1.205  
   1.206  end