src/HOL/Finite_Set.thy
changeset 15510 9de204d7b699
parent 15509 c54970704285
child 15512 ed1fa4617f52
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 09 12:08:46 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Feb 09 18:32:28 2005 +0100
     1.3 @@ -100,18 +100,23 @@
     1.4  
     1.5  text{* Finite sets are the images of initial segments of natural numbers: *}
     1.6  
     1.7 -lemma finite_imp_nat_seg_image:
     1.8 -assumes fin: "finite A" shows "\<exists> (n::nat) f. A = f ` {i::nat. i<n}"
     1.9 +lemma finite_imp_nat_seg_image_inj_on:
    1.10 +  assumes fin: "finite A" 
    1.11 +  shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
    1.12  using fin
    1.13  proof induct
    1.14    case empty
    1.15 -  show ?case
    1.16 -  proof show "\<exists>f. {} = f ` {i::nat. i < 0}" by(simp add:image_def) qed
    1.17 +  show ?case  
    1.18 +  proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp 
    1.19 +  qed
    1.20  next
    1.21    case (insert a A)
    1.22 -  from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" by blast
    1.23 -  hence "insert a A = (%i. if i<n then f i else a) ` {i. i < n+1}"
    1.24 -    by (auto simp add:image_def Ball_def)
    1.25 +  have notinA: "a \<notin> A" .
    1.26 +  from insert.hyps obtain n f
    1.27 +    where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
    1.28 +  hence "insert a A = f(n:=a) ` {i. i < Suc n}"
    1.29 +        "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
    1.30 +    by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
    1.31    thus ?case by blast
    1.32  qed
    1.33  
    1.34 @@ -137,7 +142,7 @@
    1.35  
    1.36  lemma finite_conv_nat_seg_image:
    1.37    "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
    1.38 -by(blast intro: finite_imp_nat_seg_image nat_seg_image_imp_finite)
    1.39 +by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
    1.40  
    1.41  subsubsection{* Finiteness and set theoretic constructions *}
    1.42  
    1.43 @@ -522,207 +527,142 @@
    1.44  
    1.45  subsubsection{*From @{term foldSet} to @{term fold}*}
    1.46  
    1.47 -(* only used in the next lemma, but in there twice *)
    1.48 -lemma card_lemma: assumes A1: "A = insert b B" and notinB: "b \<notin> B" and
    1.49 -  card: "A = h`{i. i<Suc n}" and new: "\<not>(EX k<n. h n = h k)"
    1.50 -shows "EX h. B = h`{i. i<n}" (is "EX h. ?P h")
    1.51 -proof
    1.52 -  let ?h = "%i. if h i = b then h n else h i"
    1.53 -  show "B = ?h`{i. i<n}" (is "_ = ?r")
    1.54 -  proof
    1.55 -    show "B \<subseteq> ?r"
    1.56 -    proof
    1.57 -      fix u assume "u \<in> B"
    1.58 -      hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+
    1.59 -      then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
    1.60 -	using card by(auto simp:image_def)
    1.61 -      show "u \<in> ?r"
    1.62 -      proof cases
    1.63 -	assume "i\<^isub>u < n"
    1.64 -	thus ?thesis using unotb by fastsimp
    1.65 -      next
    1.66 -	assume "\<not> i\<^isub>u < n"
    1.67 -	with below have [simp]: "i\<^isub>u = n" by arith
    1.68 -	obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k"
    1.69 -	  using A1 card by blast
    1.70 -	have "i\<^isub>k < n"
    1.71 -	proof (rule ccontr)
    1.72 -	  assume "\<not> i\<^isub>k < n"
    1.73 -	  hence "i\<^isub>k = n" using i\<^isub>k by arith
    1.74 -	  thus False using unotb by simp
    1.75 -	qed
    1.76 -	thus ?thesis by(auto simp add:image_def)
    1.77 -      qed
    1.78 +lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
    1.79 +by (auto simp add: less_Suc_eq) 
    1.80 +
    1.81 +lemma insert_image_inj_on_eq:
    1.82 +     "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 
    1.83 +        inj_on h {i. i < Suc m}|] 
    1.84 +      ==> A = h ` {i. i < m}"
    1.85 +apply (auto simp add: image_less_Suc inj_on_def)
    1.86 +apply (blast intro: less_trans) 
    1.87 +done
    1.88 +
    1.89 +lemma insert_inj_onE:
    1.90 +  assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A" 
    1.91 +      and inj_on: "inj_on h {i::nat. i<n}"
    1.92 +  shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
    1.93 +proof (cases n)
    1.94 +  case 0 thus ?thesis using aA by auto
    1.95 +next
    1.96 +  case (Suc m)
    1.97 +  have nSuc: "n = Suc m" . 
    1.98 +  have mlessn: "m<n" by (simp add: nSuc)
    1.99 +  have "a \<in> h ` {i. i < n}" using aA by blast
   1.100 +  then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast
   1.101 +  show ?thesis
   1.102 +  proof cases
   1.103 +    assume eq: "k=m"
   1.104 +    show ?thesis
   1.105 +    proof (intro exI conjI)
   1.106 +      show "inj_on h {i::nat. i<m}" using inj_on
   1.107 +	by (simp add: nSuc inj_on_def) 
   1.108 +      show "m<n" by (rule mlessn)
   1.109 +      show "A = h ` {i. i < m}" using aA anot nSuc hkeq eq inj_on
   1.110 +	by (rules intro: insert_image_inj_on_eq) 
   1.111      qed
   1.112    next
   1.113 -    show "?r \<subseteq> B"
   1.114 -    proof
   1.115 -      fix u assume "u \<in> ?r"
   1.116 -      then obtain i\<^isub>u where below: "i\<^isub>u < n" and
   1.117 -        or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
   1.118 -	by(auto simp:image_def)
   1.119 -      from or show "u \<in> B"
   1.120 -      proof
   1.121 -	assume [simp]: "b = h i\<^isub>u \<and> u = h n"
   1.122 -	have "u \<in> A" using card by auto
   1.123 -        moreover have "u \<noteq> b" using new below by auto
   1.124 -	ultimately show "u \<in> B" using A1 by blast
   1.125 -      next
   1.126 -	assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
   1.127 -	moreover hence "u \<in> A" using card below by auto
   1.128 -	ultimately show "u \<in> B" using A1 by blast
   1.129 +    assume diff: "k~=m"
   1.130 +    hence klessm: "k<m" using nSuc klessn by arith
   1.131 +    have hdiff: "h k ~= h m" using diff inj_on klessn mlessn
   1.132 +	by (auto simp add: inj_on_def) 
   1.133 +    let ?hm = "swap k m h"
   1.134 +    have inj_onhm_n: "inj_on ?hm {i. i < n}" using klessn mlessn 
   1.135 +      by (simp add: inj_on_swap_iff inj_on)
   1.136 +    hence inj_onhm_m: "inj_on ?hm {i. i < m}"
   1.137 +      by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
   1.138 +    show ?thesis
   1.139 +    proof (intro exI conjI)
   1.140 +      show "inj_on ?hm {i. i < m}" by (rule inj_onhm_m)
   1.141 +      show "m<n" by (simp add: nSuc)
   1.142 +      show "A = ?hm ` {i. i < m}" 
   1.143 +      proof (rule insert_image_inj_on_eq)
   1.144 +	show "inj_on (swap k m h) {i. i < Suc m}" using inj_onhm_n
   1.145 +	  by (simp add: nSuc)
   1.146 +        show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
   1.147 +        show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
   1.148 +          using aA hkeq diff hdiff nSuc
   1.149 +	  by (auto simp add: swap_def image_less_Suc fun_upd_image klessm 
   1.150 +                             inj_on_image_set_diff [OF inj_on])
   1.151        qed
   1.152      qed
   1.153    qed
   1.154  qed
   1.155  
   1.156  lemma (in ACf) foldSet_determ_aux:
   1.157 -  "!!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.158 +  "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
   1.159 +                (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
   1.160     \<Longrightarrow> x' = x"
   1.161 -proof (induct n)
   1.162 -  case 0 thus ?case by auto
   1.163 -next
   1.164 -  case (Suc n)
   1.165 -  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.166 -           \<Longrightarrow> x' = x" and card: "A = h`{i. i<Suc n}"
   1.167 -  and Afoldx: "(A, x) \<in> foldSet f g z" and Afoldy: "(A,x') \<in> foldSet f g z" .
   1.168 -  show ?case
   1.169 -  proof cases
   1.170 -    assume "EX k<n. h n = h k" 
   1.171 -      --{*@{term h} is not injective, so the cardinality has not increased*}
   1.172 -    hence card': "A = h ` {i. i < n}"
   1.173 -      using card by (auto simp:image_def less_Suc_eq)
   1.174 -    show ?thesis by(rule IH[OF card' Afoldx Afoldy])
   1.175 -  next
   1.176 -    assume new: "\<not>(EX k<n. h n = h k)"
   1.177 -    show ?thesis
   1.178 -    proof (rule foldSet.cases[OF Afoldx])
   1.179 -      assume "(A, x) = ({}, z)"  --{*fold of a singleton set*}
   1.180 -      thus "x' = x" using Afoldy by auto
   1.181 +proof (induct n rule: less_induct)
   1.182 +  case (less n)
   1.183 +    have IH: "!!m h A x x'. 
   1.184 +               \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
   1.185 +                (A,x) \<in> foldSet f g z; (A, x') \<in> foldSet f g z\<rbrakk> \<Longrightarrow> x' = x" .
   1.186 +    have Afoldx: "(A,x) \<in> foldSet f g z" and Afoldx': "(A,x') \<in> foldSet f g z"
   1.187 +     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" .
   1.188 +    show ?case
   1.189 +    proof (rule foldSet.cases [OF Afoldx])
   1.190 +      assume "(A, x) = ({}, z)"
   1.191 +      with Afoldx' show "x' = x" by blast
   1.192      next
   1.193 -      fix B b y
   1.194 -      assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
   1.195 -	and y: "(B,y) \<in> foldSet f g z" and notinB: "b \<notin> B"
   1.196 -      hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
   1.197 -      show ?thesis
   1.198 -      proof (rule foldSet.cases[OF Afoldy])
   1.199 -	assume "(A,x') = ({}, z)"
   1.200 -	thus ?thesis using A1 by auto
   1.201 +      fix B b u
   1.202 +      assume "(A,x) = (insert b B, g b \<cdot> u)" and notinB: "b \<notin> B"
   1.203 +         and Bu: "(B,u) \<in> foldSet f g z"
   1.204 +      hence AbB: "A = insert b B" and x: "x = g b \<cdot> u" by auto
   1.205 +      show "x'=x" 
   1.206 +      proof (rule foldSet.cases [OF Afoldx'])
   1.207 +        assume "(A, x') = ({}, z)"
   1.208 +        with AbB show "x' = x" by blast
   1.209        next
   1.210 -	fix C c r
   1.211 -	assume eq2: "(A,x') = (insert c C, g c \<cdot> r)"
   1.212 -	  and r: "(C,r) \<in> foldSet f g z" and notinC: "c \<notin> C"
   1.213 -	hence A2: "A = insert c C" and x': "x' = g c \<cdot> r" by auto
   1.214 -	obtain hB where lessB: "B = hB ` {i. i<n}"
   1.215 -	  using card_lemma[OF A1 notinB card new] by auto
   1.216 -	obtain hC where lessC: "C = hC ` {i. i<n}"
   1.217 -	  using card_lemma[OF A2 notinC card new] by auto
   1.218 -	show ?thesis
   1.219 +	fix C c v
   1.220 +	assume "(A,x') = (insert c C, g c \<cdot> v)" and notinC: "c \<notin> C"
   1.221 +	   and Cv: "(C,v) \<in> foldSet f g z"
   1.222 +	hence AcC: "A = insert c C" and x': "x' = g c \<cdot> v" by auto
   1.223 +	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   1.224 +        from insert_inj_onE [OF Beq notinB injh]
   1.225 +        obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   1.226 +                     and Beq: "B = hB ` {i. i < mB}"
   1.227 +                     and lessB: "mB < n" by auto 
   1.228 +	from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
   1.229 +        from insert_inj_onE [OF Ceq notinC injh]
   1.230 +        obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
   1.231 +                       and Ceq: "C = hC ` {i. i < mC}"
   1.232 +                       and lessC: "mC < n" by auto 
   1.233 +	show "x'=x"
   1.234  	proof cases
   1.235 -	  assume "b = c"
   1.236 -	  then moreover have "B = C" using A1 A2 notinB notinC by auto
   1.237 -	  ultimately show ?thesis using IH[OF lessB] y r x x' by auto
   1.238 +          assume "b=c"
   1.239 +	  then moreover have "B = C" using AbB AcC notinB notinC by auto
   1.240 +	  ultimately show ?thesis  using Bu Cv x x' IH[OF lessC Ceq inj_onC]
   1.241 +            by auto
   1.242  	next
   1.243  	  assume diff: "b \<noteq> c"
   1.244  	  let ?D = "B - {c}"
   1.245  	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   1.246 -	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
   1.247 +	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   1.248  	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   1.249 -	  with A1 have "finite ?D" by simp
   1.250 +	  with AbB have "finite ?D" by simp
   1.251  	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
   1.252  	    using finite_imp_foldSet by rules
   1.253  	  moreover have cinB: "c \<in> B" using B by auto
   1.254  	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
   1.255  	    by(rule Diff1_foldSet)
   1.256 -	  hence "g c \<cdot> d = y" by(rule IH[OF lessB y])
   1.257 -          moreover have "g b \<cdot> d = r"
   1.258 -	  proof (rule IH[OF lessC r])
   1.259 -	    show "(C,g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
   1.260 +	  hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   1.261 +          moreover have "g b \<cdot> d = v"
   1.262 +	  proof (rule IH[OF lessC Ceq inj_onC Cv])
   1.263 +	    show "(C, g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
   1.264  	      by fastsimp
   1.265  	  qed
   1.266 -	  ultimately show ?thesis using x x' by(auto simp:AC)
   1.267 +	  ultimately show ?thesis using x x' by (auto simp: AC)
   1.268  	qed
   1.269        qed
   1.270      qed
   1.271    qed
   1.272 -qed
   1.273  
   1.274 -(* The same proof, but using card 
   1.275 -lemma (in ACf) foldSet_determ_aux:
   1.276 -  "!!A x x'. \<lbrakk> card A < n; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
   1.277 -   \<Longrightarrow> x' = x"
   1.278 -proof (induct n)
   1.279 -  case 0 thus ?case by simp
   1.280 -next
   1.281 -  case (Suc n)
   1.282 -  have IH: "!!A x x'. \<lbrakk>card A < n; (A,x) \<in> foldSet f g e; (A,x') \<in> foldSet f g e\<rbrakk>
   1.283 -           \<Longrightarrow> x' = x" and card: "card A < Suc n"
   1.284 -  and Afoldx: "(A, x) \<in> foldSet f g e" and Afoldy: "(A,x') \<in> foldSet f g e" .
   1.285 -  from card have "card A < n \<or> card A = n" by arith
   1.286 -  thus ?case
   1.287 -  proof
   1.288 -    assume less: "card A < n"
   1.289 -    show ?thesis by(rule IH[OF less Afoldx Afoldy])
   1.290 -  next
   1.291 -    assume cardA: "card A = n"
   1.292 -    show ?thesis
   1.293 -    proof (rule foldSet.cases[OF Afoldx])
   1.294 -      assume "(A, x) = ({}, e)"
   1.295 -      thus "x' = x" using Afoldy by auto
   1.296 -    next
   1.297 -      fix B b y
   1.298 -      assume eq1: "(A, x) = (insert b B, g b \<cdot> y)"
   1.299 -	and y: "(B,y) \<in> foldSet f g e" and notinB: "b \<notin> B"
   1.300 -      hence A1: "A = insert b B" and x: "x = g b \<cdot> y" by auto
   1.301 -      show ?thesis
   1.302 -      proof (rule foldSet.cases[OF Afoldy])
   1.303 -	assume "(A,x') = ({}, e)"
   1.304 -	thus ?thesis using A1 by auto
   1.305 -      next
   1.306 -	fix C c z
   1.307 -	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
   1.308 -	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
   1.309 -	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
   1.310 -	have finA: "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   1.311 -	with cardA A1 notinB have less: "card B < n" by simp
   1.312 -	show ?thesis
   1.313 -	proof cases
   1.314 -	  assume "b = c"
   1.315 -	  then moreover have "B = C" using A1 A2 notinB notinC by auto
   1.316 -	  ultimately show ?thesis using IH[OF less] y z x x' by auto
   1.317 -	next
   1.318 -	  assume diff: "b \<noteq> c"
   1.319 -	  let ?D = "B - {c}"
   1.320 -	  have B: "B = insert c ?D" and C: "C = insert b ?D"
   1.321 -	    using A1 A2 notinB notinC diff by(blast elim!:equalityE)+
   1.322 -	  have "finite ?D" using finA A1 by simp
   1.323 -	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g e"
   1.324 -	    using finite_imp_foldSet by rules
   1.325 -	  moreover have cinB: "c \<in> B" using B by auto
   1.326 -	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
   1.327 -	    by(rule Diff1_foldSet)
   1.328 -	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
   1.329 -          moreover have "g b \<cdot> d = z"
   1.330 -	  proof (rule IH[OF _ z])
   1.331 -	    show "card C < n" using C cardA A1 notinB finA cinB
   1.332 -	      by(auto simp:card_Diff1_less)
   1.333 -	  next
   1.334 -	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
   1.335 -	      by fastsimp
   1.336 -	  qed
   1.337 -	  ultimately show ?thesis using x x' by(auto simp:AC)
   1.338 -	qed
   1.339 -      qed
   1.340 -    qed
   1.341 -  qed
   1.342 -qed
   1.343 -*)
   1.344  
   1.345  lemma (in ACf) foldSet_determ:
   1.346 -  "(A, x) : foldSet f g z ==> (A, y) : foldSet f g z ==> y = x"
   1.347 -apply(frule foldSet_imp_finite)
   1.348 -apply(simp add:finite_conv_nat_seg_image)
   1.349 -apply(blast intro: foldSet_determ_aux [rule_format])
   1.350 +  "(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x"
   1.351 +apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   1.352 +apply (blast intro: foldSet_determ_aux [rule_format])
   1.353  done
   1.354  
   1.355  lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"