equal
deleted
inserted
replaced
7 imports "HOL-Computational_Algebra.Primes" QuotRing Lattice |
7 imports "HOL-Computational_Algebra.Primes" QuotRing Lattice |
8 begin |
8 begin |
9 |
9 |
10 section \<open>The Ring of Integers\<close> |
10 section \<open>The Ring of Integers\<close> |
11 |
11 |
12 subsection \<open>Some properties of @{typ int}\<close> |
12 subsection \<open>Some properties of \<^typ>\<open>int\<close>\<close> |
13 |
13 |
14 lemma dvds_eq_abseq: |
14 lemma dvds_eq_abseq: |
15 fixes k :: int |
15 fixes k :: int |
16 shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>" |
16 shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>" |
17 by (metis dvd_if_abs_eq lcm.commute lcm_proj1_iff_int) |
17 by (metis dvd_if_abs_eq lcm.commute lcm_proj1_iff_int) |
144 show "domain \<Z>" |
144 show "domain \<Z>" |
145 by unfold_locales (auto simp: distrib_right distrib_left) |
145 by unfold_locales (auto simp: distrib_right distrib_left) |
146 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+ |
146 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+ |
147 |
147 |
148 |
148 |
149 text \<open>Removal of occurrences of @{term UNIV} in interpretation result |
149 text \<open>Removal of occurrences of \<^term>\<open>UNIV\<close> in interpretation result |
150 --- experimental.\<close> |
150 --- experimental.\<close> |
151 |
151 |
152 lemma UNIV: |
152 lemma UNIV: |
153 "x \<in> UNIV \<longleftrightarrow> True" |
153 "x \<in> UNIV \<longleftrightarrow> True" |
154 "A \<subseteq> UNIV \<longleftrightarrow> True" |
154 "A \<subseteq> UNIV \<longleftrightarrow> True" |