src/ZF/Arith.thy
changeset 58860 fee7cfa69c50
parent 46821 ff6b0c1087f2
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/Arith.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/Arith.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -413,12 +413,12 @@
     1.4      "i \<in> nat ==> pred(i) \<in> nat"
     1.5  by (simp add: pred_def split: split_nat_case)
     1.6  
     1.7 -lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)";
     1.8 +lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)"
     1.9  apply (rule_tac m=i and n=j in diff_induct)
    1.10  apply (auto simp add: pred_def nat_imp_quasinat split: split_nat_case)
    1.11  done
    1.12  
    1.13 -lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)";
    1.14 +lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)"
    1.15  apply (insert nat_diff_pred [of "natify(i)" "natify(j)"])
    1.16  apply (simp add: natify_succ [symmetric])
    1.17  done
    1.18 @@ -435,7 +435,7 @@
    1.19  
    1.20  text{*We actually prove @{term "i #- j #- k = i #- (j #+ k)"}*}
    1.21  lemma diff_diff_left [simplified]:
    1.22 -     "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)";
    1.23 +     "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)"
    1.24  by (rule_tac m="natify(i)" and n="natify(j)" in diff_induct, auto)
    1.25  
    1.26