src/HOL/Nat.thy
changeset 66936 cf8d8fc23891
parent 66816 212a3334e7da
child 66953 826a5fd4d36c
     1.1 --- a/src/HOL/Nat.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -166,9 +166,36 @@
     1.4  
     1.5  text \<open>Injectiveness and distinctness lemmas\<close>
     1.6  
     1.7 -lemma (in semidom_divide) inj_times:
     1.8 -  "inj (times a)" if "a \<noteq> 0"
     1.9 -proof (rule injI)
    1.10 +context cancel_ab_semigroup_add
    1.11 +begin
    1.12 +
    1.13 +lemma inj_on_add [simp]:
    1.14 +  "inj_on (plus a) A"
    1.15 +proof (rule inj_onI)
    1.16 +  fix b c
    1.17 +  assume "a + b = a + c"
    1.18 +  then have "a + b - a = a + c - a"
    1.19 +    by (simp only:)
    1.20 +  then show "b = c"
    1.21 +    by simp
    1.22 +qed
    1.23 +
    1.24 +lemma inj_on_add' [simp]:
    1.25 +  "inj_on (\<lambda>b. b + a) A"
    1.26 +  using inj_on_add [of a A] by (simp add: add.commute [of _ a])
    1.27 +
    1.28 +lemma bij_betw_add [simp]:
    1.29 +  "bij_betw (plus a) A B \<longleftrightarrow> plus a ` A = B"
    1.30 +  by (simp add: bij_betw_def)
    1.31 +
    1.32 +end
    1.33 +
    1.34 +context semidom_divide
    1.35 +begin
    1.36 +
    1.37 +lemma inj_on_mult:
    1.38 +  "inj_on (times a) A" if "a \<noteq> 0"
    1.39 +proof (rule inj_onI)
    1.40    fix b c
    1.41    assume "a * b = a * c"
    1.42    then have "a * b div a = a * c div a"
    1.43 @@ -177,20 +204,16 @@
    1.44      by simp
    1.45  qed
    1.46  
    1.47 -lemma (in cancel_ab_semigroup_add) inj_plus:
    1.48 -  "inj (plus a)"
    1.49 -proof (rule injI)
    1.50 -  fix b c
    1.51 -  assume "a + b = a + c"
    1.52 -  then have "a + b - a = a + c - a"
    1.53 -    by (simp only:)
    1.54 -  then show "b = c"
    1.55 -    by simp
    1.56 -qed
    1.57 -
    1.58 -lemma inj_Suc[simp]: "inj_on Suc N"
    1.59 +end
    1.60 +
    1.61 +lemma inj_Suc [simp]:
    1.62 +  "inj_on Suc N"
    1.63    by (simp add: inj_on_def)
    1.64  
    1.65 +lemma bij_betw_Suc [simp]:
    1.66 +  "bij_betw Suc M N \<longleftrightarrow> Suc ` M = N"
    1.67 +  by (simp add: bij_betw_def)
    1.68 +
    1.69  lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
    1.70    by (rule notE) (rule Suc_not_Zero)
    1.71  
    1.72 @@ -338,16 +361,9 @@
    1.73    for m n :: nat
    1.74    by (induct m) simp_all
    1.75  
    1.76 -lemma inj_on_add_nat [simp]: "inj_on (\<lambda>n. n + k) N"
    1.77 -  for k :: nat
    1.78 -proof (induct k)
    1.79 -  case 0
    1.80 -  then show ?case by simp
    1.81 -next
    1.82 -  case (Suc k)
    1.83 -  show ?case
    1.84 -    using comp_inj_on [OF Suc inj_Suc] by (simp add: o_def)
    1.85 -qed
    1.86 +lemma plus_1_eq_Suc:
    1.87 +  "plus 1 = Suc"
    1.88 +  by (simp add: fun_eq_iff)
    1.89  
    1.90  lemma Suc_eq_plus1: "Suc n = n + 1"
    1.91    by simp