539 |
539 |
540 instance option :: (finite) finite proof |
540 instance option :: (finite) finite proof |
541 qed (simp add: UNIV_option_conv) |
541 qed (simp add: UNIV_option_conv) |
542 |
542 |
543 lemma inj_graph: "inj (%f. {(x, y). y = f x})" |
543 lemma inj_graph: "inj (%f. {(x, y). y = f x})" |
544 by (rule inj_onI, auto simp add: set_ext_iff ext_iff) |
544 by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff) |
545 |
545 |
546 instance "fun" :: (finite, finite) finite |
546 instance "fun" :: (finite, finite) finite |
547 proof |
547 proof |
548 show "finite (UNIV :: ('a => 'b) set)" |
548 show "finite (UNIV :: ('a => 'b) set)" |
549 proof (rule finite_imageD) |
549 proof (rule finite_imageD) |
574 begin |
574 begin |
575 |
575 |
576 text{* On a functional level it looks much nicer: *} |
576 text{* On a functional level it looks much nicer: *} |
577 |
577 |
578 lemma fun_comp_comm: "f x \<circ> f y = f y \<circ> f x" |
578 lemma fun_comp_comm: "f x \<circ> f y = f y \<circ> f x" |
579 by (simp add: fun_left_comm ext_iff) |
579 by (simp add: fun_left_comm fun_eq_iff) |
580 |
580 |
581 end |
581 end |
582 |
582 |
583 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" |
583 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" |
584 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where |
584 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where |
718 assumes fun_left_idem: "f x (f x z) = f x z" |
718 assumes fun_left_idem: "f x (f x z) = f x z" |
719 begin |
719 begin |
720 |
720 |
721 text{* The nice version: *} |
721 text{* The nice version: *} |
722 lemma fun_comp_idem : "f x o f x = f x" |
722 lemma fun_comp_idem : "f x o f x = f x" |
723 by (simp add: fun_left_idem ext_iff) |
723 by (simp add: fun_left_idem fun_eq_iff) |
724 |
724 |
725 lemma fold_insert_idem: |
725 lemma fold_insert_idem: |
726 assumes fin: "finite A" |
726 assumes fin: "finite A" |
727 shows "fold f z (insert x A) = f x (fold f z A)" |
727 shows "fold f z (insert x A) = f x (fold f z A)" |
728 proof cases |
728 proof cases |
1361 assumes eq_fold: "finite A \<Longrightarrow> F A s = fold f s A" |
1361 assumes eq_fold: "finite A \<Longrightarrow> F A s = fold f s A" |
1362 begin |
1362 begin |
1363 |
1363 |
1364 lemma empty [simp]: |
1364 lemma empty [simp]: |
1365 "F {} = id" |
1365 "F {} = id" |
1366 by (simp add: eq_fold ext_iff) |
1366 by (simp add: eq_fold fun_eq_iff) |
1367 |
1367 |
1368 lemma insert [simp]: |
1368 lemma insert [simp]: |
1369 assumes "finite A" and "x \<notin> A" |
1369 assumes "finite A" and "x \<notin> A" |
1370 shows "F (insert x A) = F A \<circ> f x" |
1370 shows "F (insert x A) = F A \<circ> f x" |
1371 proof - |
1371 proof - |
1372 interpret fun_left_comm f proof |
1372 interpret fun_left_comm f proof |
1373 qed (insert commute_comp, simp add: ext_iff) |
1373 qed (insert commute_comp, simp add: fun_eq_iff) |
1374 from fold_insert2 assms |
1374 from fold_insert2 assms |
1375 have "\<And>s. fold f s (insert x A) = fold f (f x s) A" . |
1375 have "\<And>s. fold f s (insert x A) = fold f (f x s) A" . |
1376 with `finite A` show ?thesis by (simp add: eq_fold ext_iff) |
1376 with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff) |
1377 qed |
1377 qed |
1378 |
1378 |
1379 lemma remove: |
1379 lemma remove: |
1380 assumes "finite A" and "x \<in> A" |
1380 assumes "finite A" and "x \<in> A" |
1381 shows "F A = F (A - {x}) \<circ> f x" |
1381 shows "F A = F (A - {x}) \<circ> f x" |
1734 proof - |
1734 proof - |
1735 from `A \<noteq> {}` obtain b where "b \<in> A" by blast |
1735 from `A \<noteq> {}` obtain b where "b \<in> A" by blast |
1736 then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert) |
1736 then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert) |
1737 with `finite A` have "finite B" by simp |
1737 with `finite A` have "finite B" by simp |
1738 interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof |
1738 interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof |
1739 qed (simp_all add: ext_iff ac_simps) |
1739 qed (simp_all add: fun_eq_iff ac_simps) |
1740 thm fold.commute_comp' [of B b, simplified ext_iff, simplified] |
1740 thm fold.commute_comp' [of B b, simplified fun_eq_iff, simplified] |
1741 from `finite B` fold.commute_comp' [of B x] |
1741 from `finite B` fold.commute_comp' [of B x] |
1742 have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp |
1742 have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp |
1743 then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: ext_iff commute) |
1743 then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute) |
1744 from `finite B` * fold.insert [of B b] |
1744 from `finite B` * fold.insert [of B b] |
1745 have "(\<lambda>x. fold op * x (insert b B)) = (\<lambda>x. fold op * x B) \<circ> op * b" by simp |
1745 have "(\<lambda>x. fold op * x (insert b B)) = (\<lambda>x. fold op * x B) \<circ> op * b" by simp |
1746 then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: ext_iff) |
1746 then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: fun_eq_iff) |
1747 from A B assms * show ?thesis by (simp add: eq_fold' del: fold.insert) |
1747 from A B assms * show ?thesis by (simp add: eq_fold' del: fold.insert) |
1748 qed |
1748 qed |
1749 |
1749 |
1750 lemma remove: |
1750 lemma remove: |
1751 assumes "finite A" and "x \<in> A" |
1751 assumes "finite A" and "x \<in> A" |