src/HOL/NatArith.thy
changeset 10214 77349ed89f45
child 10599 2df753cf86e9
equal deleted inserted replaced
10213:01c2744a3786 10214:77349ed89f45
       
     1 (*  Title:      HOL/NatArith.thy
       
     2     ID:         $Id$
       
     3 
       
     4 Setup arithmetic proof procedures.
       
     5 *)
       
     6 
       
     7 theory NatArith = Nat
       
     8 files "arith_data.ML":
       
     9 
       
    10 setup arith_setup
       
    11 
       
    12 (*elimination of `-' on nat*)
       
    13 lemma nat_diff_split:
       
    14     "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
       
    15   by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
       
    16 
       
    17 ML {* val nat_diff_split = thm "nat_diff_split" *}
       
    18 
       
    19 lemmas [arith_split] = nat_diff_split split_min split_max
       
    20 
       
    21 end