src/HOL/NatArith.thy
changeset 10599 2df753cf86e9
parent 10214 77349ed89f45
child 11164 03f5dc539fd9
equal deleted inserted replaced
10598:f92037156f4d 10599:2df753cf86e9
     9 
     9 
    10 setup arith_setup
    10 setup arith_setup
    11 
    11 
    12 (*elimination of `-' on nat*)
    12 (*elimination of `-' on nat*)
    13 lemma nat_diff_split:
    13 lemma nat_diff_split:
    14     "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
    14     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
    15   by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
    15   by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
    16 
    16 
    17 ML {* val nat_diff_split = thm "nat_diff_split" *}
    17 ML {* val nat_diff_split = thm "nat_diff_split" *}
    18 
    18 
    19 lemmas [arith_split] = nat_diff_split split_min split_max
    19 lemmas [arith_split] = nat_diff_split split_min split_max