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.20 -apply (simp_all add: even_iff_mod_2_eq_zero)
    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 *}