src/HOL/Integ/IntArith.thy
 author nipkow Tue Oct 29 11:32:52 2002 +0100 (2002-10-29) changeset 13685 0b8fbcf65d73 parent 13575 ecb6ecd9af13 child 13837 8dd150d36c65 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` nipkow@13685 ` 28` ```subsubsection "Induction principles for int" ``` nipkow@13685 ` 29` nipkow@13685 ` 30` ``` (* `set:int': dummy construction *) ``` nipkow@13685 ` 31` ```theorem int_ge_induct[case_names base step,induct set:int]: ``` nipkow@13685 ` 32` ``` assumes ge: "k \ (i::int)" and ``` nipkow@13685 ` 33` ``` base: "P(k)" and ``` nipkow@13685 ` 34` ``` step: "\i. \k \ i; P i\ \ P(i+1)" ``` nipkow@13685 ` 35` ``` shows "P i" ``` nipkow@13685 ` 36` ```proof - ``` nipkow@13685 ` 37` ``` { fix n have "\i::int. n = nat(i-k) \ k <= i \ P i" ``` nipkow@13685 ` 38` ``` proof (induct n) ``` nipkow@13685 ` 39` ``` case 0 ``` nipkow@13685 ` 40` ``` hence "i = k" by arith ``` nipkow@13685 ` 41` ``` thus "P i" using base by simp ``` nipkow@13685 ` 42` ``` next ``` nipkow@13685 ` 43` ``` case (Suc n) ``` nipkow@13685 ` 44` ``` hence "n = nat((i - 1) - k)" by arith ``` nipkow@13685 ` 45` ``` moreover ``` nipkow@13685 ` 46` ``` have ki1: "k \ i - 1" using Suc.prems by arith ``` nipkow@13685 ` 47` ``` ultimately ``` nipkow@13685 ` 48` ``` have "P(i - 1)" by(rule Suc.hyps) ``` nipkow@13685 ` 49` ``` from step[OF ki1 this] show ?case by simp ``` nipkow@13685 ` 50` ``` qed ``` nipkow@13685 ` 51` ``` } ``` nipkow@13685 ` 52` ``` from this ge show ?thesis by fast ``` nipkow@13685 ` 53` ```qed ``` nipkow@13685 ` 54` nipkow@13685 ` 55` ``` (* `set:int': dummy construction *) ``` nipkow@13685 ` 56` ```theorem int_gr_induct[case_names base step,induct set:int]: ``` nipkow@13685 ` 57` ``` assumes gr: "k < (i::int)" and ``` nipkow@13685 ` 58` ``` base: "P(k+1)" and ``` nipkow@13685 ` 59` ``` step: "\i. \k < i; P i\ \ P(i+1)" ``` nipkow@13685 ` 60` ``` shows "P i" ``` nipkow@13685 ` 61` ```apply(rule int_ge_induct[of "k + 1"]) ``` nipkow@13685 ` 62` ``` using gr apply arith ``` nipkow@13685 ` 63` ``` apply(rule base) ``` nipkow@13685 ` 64` ```apply(rule step) ``` nipkow@13685 ` 65` ``` apply simp+ ``` nipkow@13685 ` 66` ```done ``` nipkow@13685 ` 67` nipkow@13685 ` 68` ```theorem int_le_induct[consumes 1,case_names base step]: ``` nipkow@13685 ` 69` ``` assumes le: "i \ (k::int)" and ``` nipkow@13685 ` 70` ``` base: "P(k)" and ``` nipkow@13685 ` 71` ``` step: "\i. \i \ k; P i\ \ P(i - 1)" ``` nipkow@13685 ` 72` ``` shows "P i" ``` nipkow@13685 ` 73` ```proof - ``` nipkow@13685 ` 74` ``` { fix n have "\i::int. n = nat(k-i) \ i <= k \ P i" ``` nipkow@13685 ` 75` ``` proof (induct n) ``` nipkow@13685 ` 76` ``` case 0 ``` nipkow@13685 ` 77` ``` hence "i = k" by arith ``` nipkow@13685 ` 78` ``` thus "P i" using base by simp ``` nipkow@13685 ` 79` ``` next ``` nipkow@13685 ` 80` ``` case (Suc n) ``` nipkow@13685 ` 81` ``` hence "n = nat(k - (i+1))" by arith ``` nipkow@13685 ` 82` ``` moreover ``` nipkow@13685 ` 83` ``` have ki1: "i + 1 \ k" using Suc.prems by arith ``` nipkow@13685 ` 84` ``` ultimately ``` nipkow@13685 ` 85` ``` have "P(i+1)" by(rule Suc.hyps) ``` nipkow@13685 ` 86` ``` from step[OF ki1 this] show ?case by simp ``` nipkow@13685 ` 87` ``` qed ``` nipkow@13685 ` 88` ``` } ``` nipkow@13685 ` 89` ``` from this le show ?thesis by fast ``` nipkow@13685 ` 90` ```qed ``` nipkow@13685 ` 91` nipkow@13685 ` 92` ```theorem int_less_induct[consumes 1,case_names base step]: ``` nipkow@13685 ` 93` ``` assumes less: "(i::int) < k" and ``` nipkow@13685 ` 94` ``` base: "P(k - 1)" and ``` nipkow@13685 ` 95` ``` step: "\i. \i < k; P i\ \ P(i - 1)" ``` nipkow@13685 ` 96` ``` shows "P i" ``` nipkow@13685 ` 97` ```apply(rule int_le_induct[of _ "k - 1"]) ``` nipkow@13685 ` 98` ``` using less apply arith ``` nipkow@13685 ` 99` ``` apply(rule base) ``` nipkow@13685 ` 100` ```apply(rule step) ``` nipkow@13685 ` 101` ``` apply simp+ ``` nipkow@13685 ` 102` ```done ``` nipkow@13685 ` 103` wenzelm@7707 ` 104` ```end ```