96 |
96 |
97 lemma "i < j ==> nat (i - j) = 0" |
97 lemma "i < j ==> nat (i - j) = 0" |
98 by linarith |
98 by linarith |
99 |
99 |
100 lemma "(i::nat) mod 0 = i" |
100 lemma "(i::nat) mod 0 = i" |
101 using split_mod [of _ _ 0, arith_split] |
101 using split_mod [of _ _ 0, linarith_split] |
102 \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close> |
102 \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close> |
103 by linarith |
103 by linarith |
104 |
104 |
105 lemma "(i::nat) mod 1 = 0" |
105 lemma "(i::nat) mod 1 = 0" |
106 (* rule split_mod is only declared by default for numerals *) |
106 (* rule split_mod is only declared by default for numerals *) |
107 using split_mod [of _ _ 1, arith_split] |
107 using split_mod [of _ _ 1, linarith_split] |
108 \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close> |
108 \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close> |
109 by linarith |
109 by linarith |
110 |
110 |
111 lemma "(i::nat) mod 42 <= 41" |
111 lemma "(i::nat) mod 42 <= 41" |
112 by linarith |
112 by linarith |
113 |
113 |
114 lemma "(i::int) mod 0 = i" |
114 lemma "(i::int) mod 0 = i" |
115 using split_zmod [of _ _ 0, arith_split] |
115 using split_zmod [of _ _ 0, linarith_split] |
116 \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close> |
116 \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close> |
117 by linarith |
117 by linarith |
118 |
118 |
119 lemma "(i::int) mod 1 = 0" |
119 lemma "(i::int) mod 1 = 0" |
120 using split_zmod [of _ _ "1", arith_split] |
120 using split_zmod [of _ _ "1", linarith_split] |
121 \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close> |
121 \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close> |
122 by linarith |
122 by linarith |
123 |
123 |
124 lemma "(i::int) mod 42 <= 41" |
124 lemma "(i::int) mod 42 <= 41" |
125 by linarith |
125 by linarith |