425 @{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"} |
421 @{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"} |
426 if @{text f} is associative-commutative. For an application of @{text fold} |
422 if @{text f} is associative-commutative. For an application of @{text fold} |
427 se the definitions of sums and products over finite sets. |
423 se the definitions of sums and products over finite sets. |
428 *} |
424 *} |
429 |
425 |
430 consts |
426 inductive2 |
431 foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set" |
427 foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool" |
432 |
428 for f :: "'a => 'a => 'a" |
433 inductive "foldSet f g z" |
429 and g :: "'b => 'a" |
434 intros |
430 and z :: 'a |
435 emptyI [intro]: "({}, z) : foldSet f g z" |
431 where |
436 insertI [intro]: |
432 emptyI [intro]: "foldSet f g z {} z" |
437 "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk> |
433 | insertI [intro]: |
438 \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g z" |
434 "\<lbrakk> x \<notin> A; foldSet f g z A y \<rbrakk> |
439 |
435 \<Longrightarrow> foldSet f g z (insert x A) (f (g x) y)" |
440 inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z" |
436 |
|
437 inductive_cases2 empty_foldSetE [elim!]: "foldSet f g z {} x" |
441 |
438 |
442 constdefs |
439 constdefs |
443 fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" |
440 fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" |
444 "fold f g z A == THE x. (A, x) : foldSet f g z" |
441 "fold f g z A == THE x. foldSet f g z A x" |
445 |
442 |
446 text{*A tempting alternative for the definiens is |
443 text{*A tempting alternative for the definiens is |
447 @{term "if finite A then THE x. (A, x) : foldSet f g e else e"}. |
444 @{term "if finite A then THE x. foldSet f g e A x else e"}. |
448 It allows the removal of finiteness assumptions from the theorems |
445 It allows the removal of finiteness assumptions from the theorems |
449 @{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}. |
446 @{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}. |
450 The proofs become ugly, with @{text rule_format}. It is not worth the effort.*} |
447 The proofs become ugly, with @{text rule_format}. It is not worth the effort.*} |
451 |
448 |
452 |
449 |
453 lemma Diff1_foldSet: |
450 lemma Diff1_foldSet: |
454 "(A - {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z" |
451 "foldSet f g z (A - {x}) y ==> x: A ==> foldSet f g z A (f (g x) y)" |
455 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) |
452 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) |
456 |
453 |
457 lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A" |
454 lemma foldSet_imp_finite: "foldSet f g z A x==> finite A" |
458 by (induct set: foldSet) auto |
455 by (induct set: foldSet) auto |
459 |
456 |
460 lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g z" |
457 lemma finite_imp_foldSet: "finite A ==> EX x. foldSet f g z A x" |
461 by (induct set: Finites) auto |
458 by (induct set: finite) auto |
462 |
459 |
463 |
460 |
464 subsubsection {* Commutative monoids *} |
461 subsubsection {* Commutative monoids *} |
465 |
462 |
466 locale ACf = |
463 locale ACf = |
552 qed |
549 qed |
553 qed |
550 qed |
554 |
551 |
555 lemma (in ACf) foldSet_determ_aux: |
552 lemma (in ACf) foldSet_determ_aux: |
556 "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; |
553 "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; |
557 (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk> |
554 foldSet f g z A x; foldSet f g z A x' \<rbrakk> |
558 \<Longrightarrow> x' = x" |
555 \<Longrightarrow> x' = x" |
559 proof (induct n rule: less_induct) |
556 proof (induct n rule: less_induct) |
560 case (less n) |
557 case (less n) |
561 have IH: "!!m h A x x'. |
558 have IH: "!!m h A x x'. |
562 \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; |
559 \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; |
563 (A,x) \<in> foldSet f g z; (A, x') \<in> foldSet f g z\<rbrakk> \<Longrightarrow> x' = x" . |
560 foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" . |
564 have Afoldx: "(A,x) \<in> foldSet f g z" and Afoldx': "(A,x') \<in> foldSet f g z" |
561 have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'" |
565 and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" . |
562 and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" . |
566 show ?case |
563 show ?case |
567 proof (rule foldSet.cases [OF Afoldx]) |
564 proof (rule foldSet.cases [OF Afoldx]) |
568 assume "(A, x) = ({}, z)" |
565 assume "A = {}" and "x = z" |
569 with Afoldx' show "x' = x" by blast |
566 with Afoldx' show "x' = x" by blast |
570 next |
567 next |
571 fix B b u |
568 fix B b u |
572 assume "(A,x) = (insert b B, g b \<cdot> u)" and notinB: "b \<notin> B" |
569 assume AbB: "A = insert b B" and x: "x = g b \<cdot> u" |
573 and Bu: "(B,u) \<in> foldSet f g z" |
570 and notinB: "b \<notin> B" and Bu: "foldSet f g z B u" |
574 hence AbB: "A = insert b B" and x: "x = g b \<cdot> u" by auto |
|
575 show "x'=x" |
571 show "x'=x" |
576 proof (rule foldSet.cases [OF Afoldx']) |
572 proof (rule foldSet.cases [OF Afoldx']) |
577 assume "(A, x') = ({}, z)" |
573 assume "A = {}" and "x' = z" |
578 with AbB show "x' = x" by blast |
574 with AbB show "x' = x" by blast |
579 next |
575 next |
580 fix C c v |
576 fix C c v |
581 assume "(A,x') = (insert c C, g c \<cdot> v)" and notinC: "c \<notin> C" |
577 assume AcC: "A = insert c C" and x': "x' = g c \<cdot> v" |
582 and Cv: "(C,v) \<in> foldSet f g z" |
578 and notinC: "c \<notin> C" and Cv: "foldSet f g z C v" |
583 hence AcC: "A = insert c C" and x': "x' = g c \<cdot> v" by auto |
|
584 from A AbB have Beq: "insert b B = h`{i. i<n}" by simp |
579 from A AbB have Beq: "insert b B = h`{i. i<n}" by simp |
585 from insert_inj_onE [OF Beq notinB injh] |
580 from insert_inj_onE [OF Beq notinB injh] |
586 obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" |
581 obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" |
587 and Beq: "B = hB ` {i. i < mB}" |
582 and Beq: "B = hB ` {i. i < mB}" |
588 and lessB: "mB < n" by auto |
583 and lessB: "mB < n" by auto |
602 let ?D = "B - {c}" |
597 let ?D = "B - {c}" |
603 have B: "B = insert c ?D" and C: "C = insert b ?D" |
598 have B: "B = insert c ?D" and C: "C = insert b ?D" |
604 using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ |
599 using AbB AcC notinB notinC diff by(blast elim!:equalityE)+ |
605 have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) |
600 have "finite A" by(rule foldSet_imp_finite[OF Afoldx]) |
606 with AbB have "finite ?D" by simp |
601 with AbB have "finite ?D" by simp |
607 then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z" |
602 then obtain d where Dfoldd: "foldSet f g z ?D d" |
608 using finite_imp_foldSet by iprover |
603 using finite_imp_foldSet by iprover |
609 moreover have cinB: "c \<in> B" using B by auto |
604 moreover have cinB: "c \<in> B" using B by auto |
610 ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z" |
605 ultimately have "foldSet f g z B (g c \<cdot> d)" |
611 by(rule Diff1_foldSet) |
606 by(rule Diff1_foldSet) |
612 hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) |
607 hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) |
613 moreover have "g b \<cdot> d = v" |
608 moreover have "g b \<cdot> d = v" |
614 proof (rule IH[OF lessC Ceq inj_onC Cv]) |
609 proof (rule IH[OF lessC Ceq inj_onC Cv]) |
615 show "(C, g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd |
610 show "foldSet f g z C (g b \<cdot> d)" using C notinB Dfoldd |
616 by fastsimp |
611 by fastsimp |
617 qed |
612 qed |
618 ultimately show ?thesis using x x' by (auto simp: AC) |
613 ultimately show ?thesis using x x' by (auto simp: AC) |
619 qed |
614 qed |
620 qed |
615 qed |
621 qed |
616 qed |
622 qed |
617 qed |
623 |
618 |
624 |
619 |
625 lemma (in ACf) foldSet_determ: |
620 lemma (in ACf) foldSet_determ: |
626 "(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x" |
621 "foldSet f g z A x ==> foldSet f g z A y ==> y = x" |
627 apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) |
622 apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) |
628 apply (blast intro: foldSet_determ_aux [rule_format]) |
623 apply (blast intro: foldSet_determ_aux [rule_format]) |
629 done |
624 done |
630 |
625 |
631 lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y" |
626 lemma (in ACf) fold_equality: "foldSet f g z A y ==> fold f g z A = y" |
632 by (unfold fold_def) (blast intro: foldSet_determ) |
627 by (unfold fold_def) (blast intro: foldSet_determ) |
633 |
628 |
634 text{* The base case for @{text fold}: *} |
629 text{* The base case for @{text fold}: *} |
635 |
630 |
636 lemma fold_empty [simp]: "fold f g z {} = z" |
631 lemma fold_empty [simp]: "fold f g z {} = z" |
637 by (unfold fold_def) blast |
632 by (unfold fold_def) blast |
638 |
633 |
639 lemma (in ACf) fold_insert_aux: "x \<notin> A ==> |
634 lemma (in ACf) fold_insert_aux: "x \<notin> A ==> |
640 ((insert x A, v) : foldSet f g z) = |
635 (foldSet f g z (insert x A) v) = |
641 (EX y. (A, y) : foldSet f g z & v = f (g x) y)" |
636 (EX y. foldSet f g z A y & v = f (g x) y)" |
642 apply auto |
637 apply auto |
643 apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) |
638 apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) |
644 apply (fastsimp dest: foldSet_imp_finite) |
639 apply (fastsimp dest: foldSet_imp_finite) |
645 apply (blast intro: foldSet_determ) |
640 apply (blast intro: foldSet_determ) |
646 done |
641 done |
1396 |
1391 |
1397 subsubsection {* Properties in more restricted classes of structures *} |
1392 subsubsection {* Properties in more restricted classes of structures *} |
1398 |
1393 |
1399 lemma setprod_eq_1_iff [simp]: |
1394 lemma setprod_eq_1_iff [simp]: |
1400 "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" |
1395 "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" |
1401 by (induct set: Finites) auto |
1396 by (induct set: finite) auto |
1402 |
1397 |
1403 lemma setprod_zero: |
1398 lemma setprod_zero: |
1404 "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" |
1399 "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" |
1405 apply (induct set: Finites, force, clarsimp) |
1400 apply (induct set: finite, force, clarsimp) |
1406 apply (erule disjE, auto) |
1401 apply (erule disjE, auto) |
1407 done |
1402 done |
1408 |
1403 |
1409 lemma setprod_nonneg [rule_format]: |
1404 lemma setprod_nonneg [rule_format]: |
1410 "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A" |
1405 "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A" |
1411 apply (case_tac "finite A") |
1406 apply (case_tac "finite A") |
1412 apply (induct set: Finites, force, clarsimp) |
1407 apply (induct set: finite, force, clarsimp) |
1413 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) |
1408 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) |
1414 apply (rule mult_mono, assumption+) |
1409 apply (rule mult_mono, assumption+) |
1415 apply (auto simp add: setprod_def) |
1410 apply (auto simp add: setprod_def) |
1416 done |
1411 done |
1417 |
1412 |
1418 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) |
1413 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) |
1419 --> 0 < setprod f A" |
1414 --> 0 < setprod f A" |
1420 apply (case_tac "finite A") |
1415 apply (case_tac "finite A") |
1421 apply (induct set: Finites, force, clarsimp) |
1416 apply (induct set: finite, force, clarsimp) |
1422 apply (subgoal_tac "0 * 0 < f x * setprod f F", force) |
1417 apply (subgoal_tac "0 * 0 < f x * setprod f F", force) |
1423 apply (rule mult_strict_mono, assumption+) |
1418 apply (rule mult_strict_mono, assumption+) |
1424 apply (auto simp add: setprod_def) |
1419 apply (auto simp add: setprod_def) |
1425 done |
1420 done |
1426 |
1421 |
1781 ALL c : C. k dvd card c ==> |
1776 ALL c : C. k dvd card c ==> |
1782 (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==> |
1777 (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==> |
1783 k dvd card (Union C)" |
1778 k dvd card (Union C)" |
1784 apply(frule finite_UnionD) |
1779 apply(frule finite_UnionD) |
1785 apply(rotate_tac -1) |
1780 apply(rotate_tac -1) |
1786 apply (induct set: Finites, simp_all, clarify) |
1781 apply (induct set: finite, simp_all, clarify) |
1787 apply (subst card_Un_disjoint) |
1782 apply (subst card_Un_disjoint) |
1788 apply (auto simp add: dvd_add disjoint_eq_subset_Compl) |
1783 apply (auto simp add: dvd_add disjoint_eq_subset_Compl) |
1789 done |
1784 done |
1790 |
1785 |
1791 |
1786 |
1792 subsection{* A fold functional for non-empty sets *} |
1787 subsection{* A fold functional for non-empty sets *} |
1793 |
1788 |
1794 text{* Does not require start value. *} |
1789 text{* Does not require start value. *} |
1795 |
1790 |
1796 consts |
1791 inductive2 |
1797 fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set" |
1792 fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool" |
1798 |
1793 for f :: "'a => 'a => 'a" |
1799 inductive "fold1Set f" |
1794 where |
1800 intros |
|
1801 fold1Set_insertI [intro]: |
1795 fold1Set_insertI [intro]: |
1802 "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f" |
1796 "\<lbrakk> foldSet f id a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x" |
1803 |
1797 |
1804 constdefs |
1798 constdefs |
1805 fold1 :: "('a => 'a => 'a) => 'a set => 'a" |
1799 fold1 :: "('a => 'a => 'a) => 'a set => 'a" |
1806 "fold1 f A == THE x. (A, x) : fold1Set f" |
1800 "fold1 f A == THE x. fold1Set f A x" |
1807 |
1801 |
1808 lemma fold1Set_nonempty: |
1802 lemma fold1Set_nonempty: |
1809 "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}" |
1803 "fold1Set f A x \<Longrightarrow> A \<noteq> {}" |
1810 by(erule fold1Set.cases, simp_all) |
1804 by(erule fold1Set.cases, simp_all) |
1811 |
1805 |
1812 |
1806 |
1813 inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f" |
1807 inductive_cases2 empty_fold1SetE [elim!]: "fold1Set f {} x" |
1814 |
1808 |
1815 inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f" |
1809 inductive_cases2 insert_fold1SetE [elim!]: "fold1Set f (insert a X) x" |
1816 |
1810 |
1817 |
1811 |
1818 lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)" |
1812 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)" |
1819 by (blast intro: foldSet.intros elim: foldSet.cases) |
1813 by (blast intro: foldSet.intros elim: foldSet.cases) |
1820 |
1814 |
1821 lemma fold1_singleton[simp]: "fold1 f {a} = a" |
1815 lemma fold1_singleton[simp]: "fold1 f {a} = a" |
1822 by (unfold fold1_def) blast |
1816 by (unfold fold1_def) blast |
1823 |
1817 |
1824 lemma finite_nonempty_imp_fold1Set: |
1818 lemma finite_nonempty_imp_fold1Set: |
1825 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f" |
1819 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x" |
1826 apply (induct A rule: finite_induct) |
1820 apply (induct A rule: finite_induct) |
1827 apply (auto dest: finite_imp_foldSet [of _ f id]) |
1821 apply (auto dest: finite_imp_foldSet [of _ f id]) |
1828 done |
1822 done |
1829 |
1823 |
1830 text{*First, some lemmas about @{term foldSet}.*} |
1824 text{*First, some lemmas about @{term foldSet}.*} |
1831 |
1825 |
1832 lemma (in ACf) foldSet_insert_swap: |
1826 lemma (in ACf) foldSet_insert_swap: |
1833 assumes fold: "(A,y) \<in> foldSet f id b" |
1827 assumes fold: "foldSet f id b A y" |
1834 shows "b \<notin> A \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z" |
1828 shows "b \<notin> A \<Longrightarrow> foldSet f id z (insert b A) (z \<cdot> y)" |
1835 using fold |
1829 using fold |
1836 proof (induct rule: foldSet.induct) |
1830 proof (induct rule: foldSet.induct) |
1837 case emptyI thus ?case by (force simp add: fold_insert_aux commute) |
1831 case emptyI thus ?case by (force simp add: fold_insert_aux commute) |
1838 next |
1832 next |
1839 case (insertI A x y) |
1833 case (insertI x A y) |
1840 have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z" |
1834 have "foldSet f (\<lambda>u. u) z (insert x (insert b A)) (x \<cdot> (z \<cdot> y))" |
1841 using insertI by force --{*how does @{term id} get unfolded?*} |
1835 using insertI by force --{*how does @{term id} get unfolded?*} |
1842 thus ?case by (simp add: insert_commute AC) |
1836 thus ?case by (simp add: insert_commute AC) |
1843 qed |
1837 qed |
1844 |
1838 |
1845 lemma (in ACf) foldSet_permute_diff: |
1839 lemma (in ACf) foldSet_permute_diff: |
1846 assumes fold: "(A,x) \<in> foldSet f id b" |
1840 assumes fold: "foldSet f id b A x" |
1847 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a" |
1841 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> foldSet f id a (insert b (A-{a})) x" |
1848 using fold |
1842 using fold |
1849 proof (induct rule: foldSet.induct) |
1843 proof (induct rule: foldSet.induct) |
1850 case emptyI thus ?case by simp |
1844 case emptyI thus ?case by simp |
1851 next |
1845 next |
1852 case (insertI A x y) |
1846 case (insertI x A y) |
1853 have "a = x \<or> a \<in> A" using insertI by simp |
1847 have "a = x \<or> a \<in> A" using insertI by simp |
1854 thus ?case |
1848 thus ?case |
1855 proof |
1849 proof |
1856 assume "a = x" |
1850 assume "a = x" |
1857 with insertI show ?thesis |
1851 with insertI show ?thesis |
1858 by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) |
1852 by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) |
1859 next |
1853 next |
1860 assume ainA: "a \<in> A" |
1854 assume ainA: "a \<in> A" |
1861 hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a" |
1855 hence "foldSet f id a (insert x (insert b (A - {a}))) (x \<cdot> y)" |
1862 using insertI by (force simp: id_def) |
1856 using insertI by (force simp: id_def) |
1863 moreover |
1857 moreover |
1864 have "insert x (insert b (A - {a})) = insert b (insert x A - {a})" |
1858 have "insert x (insert b (A - {a})) = insert b (insert x A - {a})" |
1865 using ainA insertI by blast |
1859 using ainA insertI by blast |
1866 ultimately show ?thesis by (simp add: id_def) |
1860 ultimately show ?thesis by (simp add: id_def) |
1941 subsubsection{* Determinacy for @{term fold1Set} *} |
1935 subsubsection{* Determinacy for @{term fold1Set} *} |
1942 |
1936 |
1943 text{*Not actually used!!*} |
1937 text{*Not actually used!!*} |
1944 |
1938 |
1945 lemma (in ACf) foldSet_permute: |
1939 lemma (in ACf) foldSet_permute: |
1946 "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|] |
1940 "[|foldSet f id b (insert a A) x; a \<notin> A; b \<notin> A|] |
1947 ==> (insert b A, x) \<in> foldSet f id a" |
1941 ==> foldSet f id a (insert b A) x" |
1948 apply (case_tac "a=b") |
1942 apply (case_tac "a=b") |
1949 apply (auto dest: foldSet_permute_diff) |
1943 apply (auto dest: foldSet_permute_diff) |
1950 done |
1944 done |
1951 |
1945 |
1952 lemma (in ACf) fold1Set_determ: |
1946 lemma (in ACf) fold1Set_determ: |
1953 "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x" |
1947 "fold1Set f A x ==> fold1Set f A y ==> y = x" |
1954 proof (clarify elim!: fold1Set.cases) |
1948 proof (clarify elim!: fold1Set.cases) |
1955 fix A x B y a b |
1949 fix A x B y a b |
1956 assume Ax: "(A, x) \<in> foldSet f id a" |
1950 assume Ax: "foldSet f id a A x" |
1957 assume By: "(B, y) \<in> foldSet f id b" |
1951 assume By: "foldSet f id b B y" |
1958 assume anotA: "a \<notin> A" |
1952 assume anotA: "a \<notin> A" |
1959 assume bnotB: "b \<notin> B" |
1953 assume bnotB: "b \<notin> B" |
1960 assume eq: "insert a A = insert b B" |
1954 assume eq: "insert a A = insert b B" |
1961 show "y=x" |
1955 show "y=x" |
1962 proof cases |
1956 proof cases |
1968 let ?D = "B - {a}" |
1962 let ?D = "B - {a}" |
1969 have B: "B = insert a ?D" and A: "A = insert b ?D" |
1963 have B: "B = insert a ?D" and A: "A = insert b ?D" |
1970 and aB: "a \<in> B" and bA: "b \<in> A" |
1964 and aB: "a \<in> B" and bA: "b \<in> A" |
1971 using eq anotA bnotB diff by (blast elim!:equalityE)+ |
1965 using eq anotA bnotB diff by (blast elim!:equalityE)+ |
1972 with aB bnotB By |
1966 with aB bnotB By |
1973 have "(insert b ?D, y) \<in> foldSet f id a" |
1967 have "foldSet f id a (insert b ?D) y" |
1974 by (auto intro: foldSet_permute simp add: insert_absorb) |
1968 by (auto intro: foldSet_permute simp add: insert_absorb) |
1975 moreover |
1969 moreover |
1976 have "(insert b ?D, x) \<in> foldSet f id a" |
1970 have "foldSet f id a (insert b ?D) x" |
1977 by (simp add: A [symmetric] Ax) |
1971 by (simp add: A [symmetric] Ax) |
1978 ultimately show ?thesis by (blast intro: foldSet_determ) |
1972 ultimately show ?thesis by (blast intro: foldSet_determ) |
1979 qed |
1973 qed |
1980 qed |
1974 qed |
1981 |
1975 |
1982 lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y" |
1976 lemma (in ACf) fold1Set_equality: "fold1Set f A y ==> fold1 f A = y" |
1983 by (unfold fold1_def) (blast intro: fold1Set_determ) |
1977 by (unfold fold1_def) (blast intro: fold1Set_determ) |
1984 |
1978 |
1985 declare |
1979 declare |
1986 empty_foldSetE [rule del] foldSet.intros [rule del] |
1980 empty_foldSetE [rule del] foldSet.intros [rule del] |
1987 empty_fold1SetE [rule del] insert_fold1SetE [rule del] |
1981 empty_fold1SetE [rule del] insert_fold1SetE [rule del] |