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--
 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 \ P n) & (i < 0 \ 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 ```