src/HOL/Integ/IntArith.thy
author nipkow
Wed Sep 25 07:42:24 2002 +0200 (2002-09-25)
changeset 13575 ecb6ecd9af13
parent 12023 d982f98e0f0d
child 13685 0b8fbcf65d73
permissions -rw-r--r--
added nat_split
wenzelm@12023
     1
wenzelm@12023
     2
header {* Integer arithmetic *}
wenzelm@12023
     3
wenzelm@9436
     4
theory IntArith = Bin
wenzelm@9436
     5
files ("int_arith1.ML") ("int_arith2.ML"):
wenzelm@9436
     6
wenzelm@12023
     7
use "int_arith1.ML"
wenzelm@12023
     8
setup int_arith_setup
wenzelm@12023
     9
use "int_arith2.ML"
wenzelm@12023
    10
declare zabs_split [arith_split]
wenzelm@12023
    11
nipkow@13575
    12
lemma split_nat[arith_split]:
nipkow@13575
    13
  "P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
nipkow@13575
    14
  (is "?P = (?L & ?R)")
nipkow@13575
    15
proof (cases "i < 0")
nipkow@13575
    16
  case True thus ?thesis by simp
nipkow@13575
    17
next
nipkow@13575
    18
  case False
nipkow@13575
    19
  have "?P = ?L"
nipkow@13575
    20
  proof
nipkow@13575
    21
    assume ?P thus ?L using False by clarsimp
nipkow@13575
    22
  next
nipkow@13575
    23
    assume ?L thus ?P using False by simp
nipkow@13575
    24
  qed
nipkow@13575
    25
  with False show ?thesis by simp
nipkow@13575
    26
qed
nipkow@13575
    27
wenzelm@7707
    28
end