93 by (simp add: inat_defs split:inat_splits, arith?) |
93 by (simp add: inat_defs split:inat_splits, arith?) |
94 |
94 |
95 lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>" |
95 lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>" |
96 by (simp add: inat_defs split:inat_splits, arith?) |
96 by (simp add: inat_defs split:inat_splits, arith?) |
97 |
97 |
98 lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)" |
98 lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)" |
99 by (simp add: inat_defs split:inat_splits, arith?) |
99 by (simp add: inat_defs split:inat_splits, arith?) |
100 |
100 |
101 lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)" |
101 lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)" |
102 by (simp add: inat_defs split:inat_splits, arith?) |
102 by (simp add: inat_defs split:inat_splits, arith?) |
103 |
103 |
108 by (simp add: inat_defs split:inat_splits, arith?) |
108 by (simp add: inat_defs split:inat_splits, arith?) |
109 |
109 |
110 lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k" |
110 lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k" |
111 by (simp add: inat_defs split:inat_splits, arith?) |
111 by (simp add: inat_defs split:inat_splits, arith?) |
112 |
112 |
113 lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)" |
113 lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)" |
114 by (simp add: inat_defs split:inat_splits, arith?) |
114 by (simp add: inat_defs split:inat_splits, arith?) |
115 |
115 |
116 |
116 |
117 (* ----------------------------------------------------------------------- *) |
117 (* ----------------------------------------------------------------------- *) |
118 |
118 |
119 lemma ile_def2: "m \<le> n = (m < n \<or> m = (n::inat))" |
119 lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))" |
120 by (simp add: inat_defs split:inat_splits, arith?) |
120 by (simp add: inat_defs split:inat_splits, arith?) |
121 |
121 |
122 lemma ile_refl [simp]: "n \<le> (n::inat)" |
122 lemma ile_refl [simp]: "n \<le> (n::inat)" |
123 by (simp add: inat_defs split:inat_splits, arith?) |
123 by (simp add: inat_defs split:inat_splits, arith?) |
124 |
124 |
147 by (simp add: inat_defs split:inat_splits, arith?) |
147 by (simp add: inat_defs split:inat_splits, arith?) |
148 |
148 |
149 lemma ileI1: "m < n ==> iSuc m \<le> n" |
149 lemma ileI1: "m < n ==> iSuc m \<le> n" |
150 by (simp add: inat_defs split:inat_splits, arith?) |
150 by (simp add: inat_defs split:inat_splits, arith?) |
151 |
151 |
152 lemma Suc_ile_eq: "Fin (Suc m) \<le> n = (Fin m < n)" |
152 lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)" |
153 by (simp add: inat_defs split:inat_splits, arith?) |
153 by (simp add: inat_defs split:inat_splits, arith?) |
154 |
154 |
155 lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m = (n \<le> m)" |
155 lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)" |
156 by (simp add: inat_defs split:inat_splits, arith?) |
156 by (simp add: inat_defs split:inat_splits, arith?) |
157 |
157 |
158 lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m \<le> n)" |
158 lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)" |
159 by (simp add: inat_defs split:inat_splits, arith?) |
159 by (simp add: inat_defs split:inat_splits, arith?) |
160 |
160 |
161 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" |
161 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" |
162 by (simp add: inat_defs split:inat_splits, arith?) |
162 by (simp add: inat_defs split:inat_splits, arith?) |
163 |
163 |