equal
deleted
inserted
replaced
91 int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)" |
91 int (card {s \<in> simplices. \<not> compo s \<and> card {f \<in> faces. face f s \<and> compo' f} = 2} * 2)" |
92 using lem1[unfolded lem3 lem2 lem5] by auto |
92 using lem1[unfolded lem3 lem2 lem5] by auto |
93 have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto |
93 have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto |
94 have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto |
94 have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto |
95 show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum] |
95 show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum] |
96 unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even) |
96 unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even) |
97 apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed |
97 apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed |
98 |
98 |
99 subsection {* The odd/even result for faces of complete vertices, generalized. *} |
99 subsection {* The odd/even result for faces of complete vertices, generalized. *} |
100 |
100 |
101 lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def |
101 lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def |