548 case (Suc m) |
548 case (Suc m) |
549 have nSuc: "n = Suc m" . |
549 have nSuc: "n = Suc m" . |
550 have mlessn: "m<n" by (simp add: nSuc) |
550 have mlessn: "m<n" by (simp add: nSuc) |
551 have "a \<in> h ` {i. i < n}" using aA by blast |
551 have "a \<in> h ` {i. i < n}" using aA by blast |
552 then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast |
552 then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast |
|
553 let ?hm = "swap k m h" |
|
554 have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn |
|
555 by (simp add: inj_on_swap_iff inj_on) |
553 show ?thesis |
556 show ?thesis |
554 proof cases |
557 proof (intro exI conjI) |
555 assume eq: "k=m" |
558 show "inj_on ?hm {i. i < m}" using inj_hm |
556 show ?thesis |
|
557 proof (intro exI conjI) |
|
558 show "inj_on h {i::nat. i<m}" using inj_on |
|
559 by (simp add: nSuc inj_on_def) |
|
560 show "m<n" by (rule mlessn) |
|
561 show "A = h ` {i. i < m}" using aA anot nSuc hkeq eq inj_on |
|
562 by (rules intro: insert_image_inj_on_eq) |
|
563 qed |
|
564 next |
|
565 assume diff: "k~=m" |
|
566 hence klessm: "k<m" using nSuc klessn by arith |
|
567 have hdiff: "h k ~= h m" using diff inj_on klessn mlessn |
|
568 by (auto simp add: inj_on_def) |
|
569 let ?hm = "swap k m h" |
|
570 have inj_onhm_n: "inj_on ?hm {i. i < n}" using klessn mlessn |
|
571 by (simp add: inj_on_swap_iff inj_on) |
|
572 hence inj_onhm_m: "inj_on ?hm {i. i < m}" |
|
573 by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on) |
559 by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on) |
574 show ?thesis |
560 show "m<n" by (rule mlessn) |
575 proof (intro exI conjI) |
561 show "A = ?hm ` {i. i < m}" |
576 show "inj_on ?hm {i. i < m}" by (rule inj_onhm_m) |
562 proof (rule insert_image_inj_on_eq) |
577 show "m<n" by (simp add: nSuc) |
563 show "inj_on (swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp |
578 show "A = ?hm ` {i. i < m}" |
564 show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) |
579 proof (rule insert_image_inj_on_eq) |
565 show "insert (?hm m) A = ?hm ` {i. i < Suc m}" |
580 show "inj_on (swap k m h) {i. i < Suc m}" using inj_onhm_n |
566 using aA hkeq nSuc klessn |
581 by (simp add: nSuc) |
567 by (auto simp add: swap_def image_less_Suc fun_upd_image |
582 show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) |
568 less_Suc_eq inj_on_image_set_diff [OF inj_on]) |
583 show "insert (?hm m) A = ?hm ` {i. i < Suc m}" |
|
584 using aA hkeq diff hdiff nSuc |
|
585 by (auto simp add: swap_def image_less_Suc fun_upd_image klessm |
|
586 inj_on_image_set_diff [OF inj_on]) |
|
587 qed |
|
588 qed |
569 qed |
589 qed |
570 qed |
590 qed |
571 qed |
591 |
572 |
592 lemma (in ACf) foldSet_determ_aux: |
573 lemma (in ACf) foldSet_determ_aux: |