src/HOL/NatArith.thy
changeset 14607 099575a938e5
parent 14208 144f45277d5a
child 14981 e73f8140af78
equal deleted inserted replaced
14606:0be6c11e7128 14607:099575a938e5
    31  val nat_diff_split = thm "nat_diff_split";
    31  val nat_diff_split = thm "nat_diff_split";
    32  val nat_diff_split_asm = thm "nat_diff_split_asm";
    32  val nat_diff_split_asm = thm "nat_diff_split_asm";
    33 *}
    33 *}
    34 (* Careful: arith_tac produces counter examples!
    34 (* Careful: arith_tac produces counter examples!
    35 fun add_arith cs = cs addafter ("arith_tac", arith_tac);
    35 fun add_arith cs = cs addafter ("arith_tac", arith_tac);
    36 TODO: use arith_tac for force_tac in Provers/clasip.ML *)
    36 TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
    37 
    37 
    38 lemmas [arith_split] = nat_diff_split split_min split_max
    38 lemmas [arith_split] = nat_diff_split split_min split_max
    39 
    39 
    40 
    40 
    41 subsubsection {* Generic summation indexed over natural numbers *}
    41 subsection {* Generic summation indexed over natural numbers *}
    42 
    42 
    43 consts
    43 consts
    44   Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
    44   Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
    45 primrec
    45 primrec
    46   "Summation f 0 = 0"
    46   "Summation f 0 = 0"