src/FOL/ex/Natural_Numbers.thy
changeset 11726 2b2a45abe876
parent 11696 233362cfecc7
child 11789 da81334357ba
equal deleted inserted replaced
11725:d0c37d04906b 11726:2b2a45abe876
    60 lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
    60 lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
    61   by (induct m) simp_all
    61   by (induct m) simp_all
    62 
    62 
    63 lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)"
    63 lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)"
    64 proof -
    64 proof -
    65   assume a: "!!n. f(Suc(n)) = Suc(f(n))"
    65   assume "!!n. f(Suc(n)) = Suc(f(n))"
    66   show ?thesis by (induct i) (simp, simp add: a)  (* FIXME tune *)
    66   thus ?thesis by (induct i) simp_all
    67 qed
    67 qed
    68 
    68 
    69 end
    69 end