renamed a few vars, added a lemma
authornipkow
Sun Jan 30 20:48:50 2005 +0100 (2005-01-30)
changeset 15480cb3612cc41a3
parent 15479 fbc473ea9d3c
child 15481 fc075ae929e4
renamed a few vars, added a lemma
src/HOL/Finite_Set.thy
     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.6                  Additions by Jeremy Avigad in Feb 2004
     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.160  apply(simp add:finite_conv_nat_seg_image)
   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.189    apply (simp add: fold_insert_aux)
   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.219  subsubsection{*Lemmas about @{text fold}*}
   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.225    apply (simp add: left_commute)
   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.240    by (simp add: fold_nest_Un_Int)
   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 @@
   1.261      cong add: conj_cong simp add: fold1_def [symmetric] foldSet1_equality)
   1.262  done
   1.263  
   1.264 -locale ACIf = ACf +
   1.265 -  assumes idem: "x \<cdot> x = x"
   1.266 -
   1.267  lemma (in ACIf) fold1_insert2:
   1.268  assumes finA: "finite A" and nonA: "A \<noteq> {}"
   1.269  shows "fold1 f (insert a A) = f a (fold1 f A)"