src/HOL/Finite_Set.thy
 changeset 15480 cb3612cc41a3 parent 15479 fbc473ea9d3c child 15483 704b3ce6d0f7
```     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 28 15:44:03 2005 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Sun Jan 30 20:48:50 2005 +0100
1.3 @@ -2,10 +2,6 @@
1.4      ID:         \$Id\$
1.5      Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
1.7 -
1.8 -Get rid of a couple of superfluous finiteness assumptions in lemmas
1.9 -about setsum and card - see FIXME.
1.10 -NB: the analogous lemmas for setprod should also be simplified!
1.11  *)
1.12
1.13  header {* Finite sets *}
1.14 @@ -412,7 +408,7 @@
1.15  subsection {* A fold functional for finite sets *}
1.16
1.17  text {* The intended behaviour is
1.18 -@{text "fold f g e {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) e)\<dots>)"}
1.19 +@{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"}
1.20  if @{text f} is associative-commutative. For an application of @{text fold}
1.21  se the definitions of sums and products over finite sets.
1.22  *}
1.23 @@ -420,30 +416,31 @@
1.24  consts
1.25    foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
1.26
1.27 -inductive "foldSet f g e"
1.28 +inductive "foldSet f g z"
1.29  intros
1.30 -emptyI [intro]: "({}, e) : foldSet f g e"
1.31 -insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g e \<rbrakk>
1.32 - \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g e"
1.33 +emptyI [intro]: "({}, z) : foldSet f g z"
1.34 +insertI [intro]: "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk>
1.35 + \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g z"
1.36
1.37 -inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g e"
1.38 +inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
1.39
1.40  constdefs
1.41    fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
1.42 -  "fold f g e A == THE x. (A, x) : foldSet f g e"
1.43 +  "fold f g z A == THE x. (A, x) : foldSet f g z"
1.44
1.45  lemma Diff1_foldSet:
1.46 -  "(A - {x}, y) : foldSet f g e ==> x: A ==> (A, f (g x) y) : foldSet f g e"
1.47 +  "(A - {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z"
1.48  by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
1.49
1.50 -lemma foldSet_imp_finite: "(A, x) : foldSet f g e ==> finite A"
1.51 +lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A"
1.52    by (induct set: foldSet) auto
1.53
1.54 -lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g e"
1.55 +lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g z"
1.56    by (induct set: Finites) auto
1.57
1.58
1.59  subsubsection {* Commutative monoids *}
1.60 +
1.61  locale ACf =
1.62    fixes f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
1.63    assumes commute: "x \<cdot> y = y \<cdot> x"
1.64 @@ -453,6 +450,9 @@
1.65    fixes e :: 'a
1.66    assumes ident [simp]: "x \<cdot> e = x"
1.67
1.68 +locale ACIf = ACf +
1.69 +  assumes idem: "x \<cdot> x = x"
1.70 +
1.71  lemma (in ACf) left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
1.72  proof -
1.73    have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp only: commute)
1.74 @@ -542,15 +542,15 @@
1.75  qed
1.76
1.77  lemma (in ACf) foldSet_determ_aux:
1.78 -  "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
1.79 +  "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
1.80     \<Longrightarrow> x' = x"
1.81  proof (induct n)
1.82    case 0 thus ?case by auto
1.83  next
1.84    case (Suc n)
1.85 -  have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
1.86 +  have IH: "!!A x x' h. \<lbrakk>A = h`{i::nat. i<n}; (A,x) \<in> foldSet f g z; (A,x') \<in> foldSet f g z\<rbrakk>
1.87             \<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}"
1.88 -  and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
1.89 +  and Afoldx: "(A, x) \<in> foldSet f g z" and Afoldy: "(A,x') \<in> foldSet f g z" .
1.90    show ?case
1.91    proof cases
1.92      assume "EX k<n. h n = h k"
1.93 @@ -561,22 +561,22 @@
1.94      assume new: "\<not>(EX k<n. h n = h k)"
1.95      show ?thesis
1.96      proof (rule foldSet.cases[OF Afoldx])
1.97 -      assume "(A, x) = ({}, e)"
1.98 +      assume "(A, x) = ({}, z)"
1.99        thus "x' = x" using Afoldy by (auto)
1.100      next
1.101        fix B b y
1.102        assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
1.103 -	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
1.104 +	and y: "(B,y) \<in> foldSet f g z" and notinB: "b \<notin> B"
1.105        hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
1.106        show ?thesis
1.107        proof (rule foldSet.cases[OF Afoldy])
1.108 -	assume "(A,x') = ({}, e)"
1.109 +	assume "(A,x') = ({}, z)"
1.110  	thus ?thesis using A1 by auto
1.111        next
1.112 -	fix C c z
1.113 -	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
1.114 -	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
1.115 -	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
1.116 +	fix C c r
1.117 +	assume eq2: "(A,x') = (insert c C, g c \<cdot> r)"
1.118 +	  and r: "(C,r) \<in> foldSet f g z" and notinC: "c \<notin> C"
1.119 +	hence A2: "A = insert c C" and x': "x' = g c \<cdot> r" by auto
1.120  	obtain hB where lessB: "B = hB ` {i. i<n}"
1.121  	  using card_lemma[OF A1 notinB card new] by auto
1.122  	obtain hC where lessC: "C = hC ` {i. i<n}"
1.123 @@ -585,7 +585,7 @@
1.124  	proof cases
1.125  	  assume "b = c"
1.126  	  then moreover have "B = C" using A1 A2 notinB notinC by auto
1.127 -	  ultimately show ?thesis using IH[OF lessB] y z x x' by auto
1.128 +	  ultimately show ?thesis using IH[OF lessB] y r x x' by auto
1.129  	next
1.130  	  assume diff: "b \<noteq> c"
1.131  	  let ?D = "B - {c}"
1.132 @@ -593,15 +593,15 @@
1.133  	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
1.134  	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
1.135  	  with A1 have "finite ?D" by simp
1.136 -	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
1.137 +	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
1.138  	    using finite_imp_foldSet by rules
1.139  	  moreover have cinB: "c \<in> B" using B by(auto)
1.140 -	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
1.141 +	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
1.142  	    by(rule Diff1_foldSet)
1.143  	  hence "g c \<cdot> d = y" by(rule IH[OF lessB y])
1.144 -          moreover have "g b \<cdot> d = z"
1.145 -	  proof (rule IH[OF lessC z])
1.146 -	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
1.147 +          moreover have "g b \<cdot> d = r"
1.148 +	  proof (rule IH[OF lessC r])
1.149 +	    show "(C,g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
1.150  	      by fastsimp
1.151  	  qed
1.152  	  ultimately show ?thesis using x x' by(auto simp:AC)
1.153 @@ -683,23 +683,23 @@
1.154  *)
1.155
1.156  lemma (in ACf) foldSet_determ:
1.157 -  "(A, x) : foldSet f g e ==> (A, y) : foldSet f g e ==> y = x"
1.158 +  "(A, x) : foldSet f g z ==> (A, y) : foldSet f g z ==> y = x"
1.159  apply(frule foldSet_imp_finite)
1.161  apply(blast intro: foldSet_determ_aux [rule_format])
1.162  done
1.163
1.164 -lemma (in ACf) fold_equality: "(A, y) : foldSet f g e ==> fold f g e A = y"
1.165 +lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"
1.166    by (unfold fold_def) (blast intro: foldSet_determ)
1.167
1.168  text{* The base case for @{text fold}: *}
1.169
1.170 -lemma fold_empty [simp]: "fold f g e {} = e"
1.171 +lemma fold_empty [simp]: "fold f g z {} = z"
1.172    by (unfold fold_def) blast
1.173
1.174  lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
1.175 -    ((insert x A, v) : foldSet f g e) =
1.176 -    (EX y. (A, y) : foldSet f g e & v = f (g x) y)"
1.177 +    ((insert x A, v) : foldSet f g z) =
1.178 +    (EX y. (A, y) : foldSet f g z & v = f (g x) y)"
1.179    apply auto
1.180    apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
1.181     apply (fastsimp dest: foldSet_imp_finite)
1.182 @@ -709,7 +709,7 @@
1.183  text{* The recursion equation for @{text fold}: *}
1.184
1.185  lemma (in ACf) fold_insert[simp]:
1.186 -    "finite A ==> x \<notin> A ==> fold f g e (insert x A) = f (g x) (fold f g e A)"
1.187 +    "finite A ==> x \<notin> A ==> fold f g z (insert x A) = f (g x) (fold f g z A)"
1.188    apply (unfold fold_def)
1.190    apply (rule the_equality)
1.191 @@ -721,29 +721,53 @@
1.192    empty_foldSetE [rule del]  foldSet.intros [rule del]
1.193    -- {* Delete rules to do with @{text foldSet} relation. *}
1.194
1.195 +text{* A simplified version for idempotent functions: *}
1.196 +
1.197 +lemma (in ACIf) fold_insert2:
1.198 +assumes finA: "finite A"
1.199 +shows "fold (op \<cdot>) g z (insert a A) = g a \<cdot> fold f g z A"
1.200 +proof cases
1.201 +  assume "a \<in> A"
1.202 +  then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
1.203 +    by(blast dest: mk_disjoint_insert)
1.204 +  show ?thesis
1.205 +  proof -
1.206 +    from finA A have finB: "finite B" by(blast intro: finite_subset)
1.207 +    have "fold f g z (insert a A) = fold f g z (insert a B)" using A by simp
1.208 +    also have "\<dots> = (g a) \<cdot> (fold f g z B)"
1.209 +      using finB disj by(simp)
1.210 +    also have "\<dots> = g a \<cdot> fold f g z A"
1.211 +      using A finB disj by(simp add:idem assoc[symmetric])
1.212 +    finally show ?thesis .
1.213 +  qed
1.214 +next
1.215 +  assume "a \<notin> A"
1.216 +  with finA show ?thesis by simp
1.217 +qed
1.218 +
1.220
1.221  lemma (in ACf) fold_commute:
1.222 -  "finite A ==> (!!e. f (g x) (fold f g e A) = fold f g (f (g x) e) A)"
1.223 +  "finite A ==> (!!z. f (g x) (fold f g z A) = fold f g (f (g x) z) A)"
1.224    apply (induct set: Finites, simp)
1.226    done
1.227
1.228  lemma (in ACf) fold_nest_Un_Int:
1.229    "finite A ==> finite B
1.230 -    ==> fold f g (fold f g e B) A = fold f g (fold f g e (A Int B)) (A Un B)"
1.231 +    ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
1.232    apply (induct set: Finites, simp)
1.233    apply (simp add: fold_commute Int_insert_left insert_absorb)
1.234    done
1.235
1.236  lemma (in ACf) fold_nest_Un_disjoint:
1.237    "finite A ==> finite B ==> A Int B = {}
1.238 -    ==> fold f g e (A Un B) = fold f g (fold f g e B) A"
1.239 +    ==> fold f g z (A Un B) = fold f g (fold f g z B) A"
1.241
1.242  lemma (in ACf) fold_reindex:
1.243  assumes fin: "finite B"
1.244 -shows "inj_on h B \<Longrightarrow> fold f g e (h ` B) = fold f (g \<circ> h) e B"
1.245 +shows "inj_on h B \<Longrightarrow> fold f g z (h ` B) = fold f (g \<circ> h) z B"
1.246  using fin apply (induct)
1.247   apply simp
1.248  apply simp
1.249 @@ -776,8 +800,8 @@
1.250    done
1.251
1.252  lemma (in ACf) fold_cong:
1.253 -  "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g a A = fold f h a A"
1.254 -  apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g a C = fold f h a C")
1.255 +  "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
1.256 +  apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold f g z C = fold f h z C")
1.257     apply simp
1.258    apply (erule finite_induct, simp)
1.259    apply (simp add: subset_insert_iff, clarify)
1.260 @@ -1826,9 +1850,6 @@