src/HOL/Library/Nat_Bijection.thy
 changeset 58834 773b378d9313 parent 58770 ae5e9b4f8daf child 58881 b9556a055632
```     1.1 --- a/src/HOL/Library/Nat_Bijection.thy	Thu Oct 30 16:36:44 2014 +0000
1.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Thu Oct 30 21:02:01 2014 +0100
1.3 @@ -122,7 +122,7 @@
1.4  by (induct x) simp_all
1.5
1.6  lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
1.7 -  by (simp add: even_two_times_div_two odd_two_times_div_two_Suc sum_decode_def sum_encode_def)
1.8 +  by (simp add: even_two_times_div_two sum_decode_def sum_encode_def)
1.9
1.10  lemma inj_sum_encode: "inj_on sum_encode A"
1.11  by (rule inj_on_inverseI, rule sum_encode_inverse)
1.12 @@ -269,12 +269,18 @@
1.13  by auto
1.14
1.15  lemma div2_even_ext_nat:
1.16 -  "x div 2 = y div 2 \<Longrightarrow> even x \<longleftrightarrow> even y \<Longrightarrow> (x::nat) = y"
1.17 -apply (rule mod_div_equality [of x 2, THEN subst])
1.18 -apply (rule mod_div_equality [of y 2, THEN subst])
1.19 -apply (cases "even x")
1.21 -done
1.22 +  fixes x y :: nat
1.23 +  assumes "x div 2 = y div 2"
1.24 +  and "even x \<longleftrightarrow> even y"
1.25 +  shows "x = y"
1.26 +proof -
1.27 +  from `even x \<longleftrightarrow> even y` have "x mod 2 = y mod 2"
1.28 +    by (simp only: even_iff_mod_2_eq_zero) auto
1.29 +  with assms have "x div 2 * 2 + x mod 2 = y div 2 * 2 + y mod 2"
1.30 +    by simp
1.31 +  then show ?thesis
1.32 +    by simp
1.33 +qed
1.34
1.35
1.36  subsubsection {* From sets to naturals *}
```