49 *} |
49 *} |
50 |
50 |
51 subsection "Constructors" |
51 subsection "Constructors" |
52 |
52 |
53 lemma Fin_0: "Fin 0 = 0" |
53 lemma Fin_0: "Fin 0 = 0" |
54 by (simp add: inat_defs split:inat_splits) |
54 by (simp add: inat_defs split:inat_splits) |
55 |
55 |
56 lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0" |
56 lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0" |
57 by (simp add: inat_defs split:inat_splits) |
57 by (simp add: inat_defs split:inat_splits) |
58 |
58 |
59 lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>" |
59 lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>" |
60 by (simp add: inat_defs split:inat_splits) |
60 by (simp add: inat_defs split:inat_splits) |
61 |
61 |
62 lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)" |
62 lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)" |
63 by (simp add: inat_defs split:inat_splits) |
63 by (simp add: inat_defs split:inat_splits) |
64 |
64 |
65 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>" |
65 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>" |
66 by (simp add: inat_defs split:inat_splits) |
66 by (simp add: inat_defs split:inat_splits) |
67 |
67 |
68 lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0" |
68 lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0" |
69 by (simp add: inat_defs split:inat_splits) |
69 by (simp add: inat_defs split:inat_splits) |
70 |
70 |
71 lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)" |
71 lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)" |
72 by (simp add: inat_defs split:inat_splits) |
72 by (simp add: inat_defs split:inat_splits) |
73 |
73 |
74 |
74 |
75 subsection "Ordering relations" |
75 subsection "Ordering relations" |
76 |
76 |
77 lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R" |
77 lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R" |
78 by (simp add: inat_defs split:inat_splits) |
78 by (simp add: inat_defs split:inat_splits) |
79 |
79 |
80 lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)" |
80 lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)" |
81 by (simp add: inat_defs split:inat_splits, arith) |
81 by (simp add: inat_defs split:inat_splits, arith) |
82 |
82 |
83 lemma iless_not_refl [simp]: "\<not> n < (n::inat)" |
83 lemma iless_not_refl [simp]: "\<not> n < (n::inat)" |
84 by (simp add: inat_defs split:inat_splits) |
84 by (simp add: inat_defs split:inat_splits) |
85 |
85 |
86 lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)" |
86 lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)" |
87 by (simp add: inat_defs split:inat_splits) |
87 by (simp add: inat_defs split:inat_splits) |
88 |
88 |
89 lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)" |
89 lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)" |
90 by (simp add: inat_defs split:inat_splits) |
90 by (simp add: inat_defs split:inat_splits) |
91 |
91 |
92 lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)" |
92 lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)" |
93 by (simp add: inat_defs split:inat_splits) |
93 by (simp add: inat_defs split:inat_splits) |
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) |
96 by (simp add: inat_defs split:inat_splits) |
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) |
99 by (simp add: inat_defs split:inat_splits) |
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: neq0_conv inat_defs split:inat_splits) |
102 by (fastsimp simp: inat_defs split:inat_splits) |
103 |
103 |
104 lemma i0_iless_iSuc [simp]: "0 < iSuc n" |
104 lemma i0_iless_iSuc [simp]: "0 < iSuc n" |
105 by (simp add: inat_defs split:inat_splits) |
105 by (simp add: inat_defs split:inat_splits) |
106 |
106 |
107 lemma not_ilessi0 [simp]: "\<not> n < (0::inat)" |
107 lemma not_ilessi0 [simp]: "\<not> n < (0::inat)" |
108 by (simp add: inat_defs split:inat_splits) |
108 by (simp add: inat_defs split:inat_splits) |
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) |
111 by (simp add: inat_defs split:inat_splits) |
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) |
114 by (simp add: inat_defs split:inat_splits) |
115 |
115 |
116 |
116 |
117 |
117 |
118 lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))" |
118 lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))" |
119 by (simp add: inat_defs split:inat_splits, arith) |
119 by (simp add: inat_defs split:inat_splits, arith) |
120 |
120 |
121 lemma ile_refl [simp]: "n \<le> (n::inat)" |
121 lemma ile_refl [simp]: "n \<le> (n::inat)" |
122 by (simp add: inat_defs split:inat_splits) |
122 by (simp add: inat_defs split:inat_splits) |
123 |
123 |
124 lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)" |
124 lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)" |
125 by (simp add: inat_defs split:inat_splits) |
125 by (simp add: inat_defs split:inat_splits) |
126 |
126 |
127 lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)" |
127 lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)" |
128 by (simp add: inat_defs split:inat_splits) |
128 by (simp add: inat_defs split:inat_splits) |
129 |
129 |
130 lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)" |
130 lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)" |
131 by (simp add: inat_defs split:inat_splits) |
131 by (simp add: inat_defs split:inat_splits) |
132 |
132 |
133 lemma Infty_ub [simp]: "n \<le> \<infinity>" |
133 lemma Infty_ub [simp]: "n \<le> \<infinity>" |
134 by (simp add: inat_defs split:inat_splits) |
134 by (simp add: inat_defs split:inat_splits) |
135 |
135 |
136 lemma i0_lb [simp]: "(0::inat) \<le> n" |
136 lemma i0_lb [simp]: "(0::inat) \<le> n" |
137 by (simp add: inat_defs split:inat_splits) |
137 by (simp add: inat_defs split:inat_splits) |
138 |
138 |
139 lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R" |
139 lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R" |
140 by (simp add: inat_defs split:inat_splits) |
140 by (simp add: inat_defs split:inat_splits) |
141 |
141 |
142 lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)" |
142 lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)" |
143 by (simp add: inat_defs split:inat_splits, arith) |
143 by (simp add: inat_defs split:inat_splits, arith) |
144 |
144 |
145 lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)" |
145 lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)" |
146 by (simp add: inat_defs split:inat_splits) |
146 by (simp add: inat_defs split:inat_splits) |
147 |
147 |
148 lemma ileI1: "m < n ==> iSuc m \<le> n" |
148 lemma ileI1: "m < n ==> iSuc m \<le> n" |
149 by (simp add: inat_defs split:inat_splits) |
149 by (simp add: inat_defs split:inat_splits) |
150 |
150 |
151 lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)" |
151 lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)" |
152 by (simp add: inat_defs split:inat_splits, arith) |
152 by (simp add: inat_defs split:inat_splits, arith) |
153 |
153 |
154 lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)" |
154 lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)" |
155 by (simp add: inat_defs split:inat_splits) |
155 by (simp add: inat_defs split:inat_splits) |
156 |
156 |
157 lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)" |
157 lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)" |
158 by (simp add: inat_defs split:inat_splits, arith) |
158 by (simp add: inat_defs split:inat_splits, arith) |
159 |
159 |
160 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" |
160 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" |
161 by (simp add: inat_defs split:inat_splits) |
161 by (simp add: inat_defs split:inat_splits) |
162 |
162 |
163 lemma ile_iSuc [simp]: "n \<le> iSuc n" |
163 lemma ile_iSuc [simp]: "n \<le> iSuc n" |
164 by (simp add: inat_defs split:inat_splits) |
164 by (simp add: inat_defs split:inat_splits) |
165 |
165 |
166 lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k" |
166 lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k" |
167 by (simp add: inat_defs split:inat_splits) |
167 by (simp add: inat_defs split:inat_splits) |
168 |
168 |
169 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j" |
169 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j" |
170 apply (induct_tac k) |
170 apply (induct_tac k) |
171 apply (simp (no_asm) only: Fin_0) |
171 apply (simp (no_asm) only: Fin_0) |
172 apply (fast intro: ile_iless_trans i0_lb) |
172 apply (fast intro: ile_iless_trans i0_lb) |
173 apply (erule exE) |
173 apply (erule exE) |
174 apply (drule spec) |
174 apply (drule spec) |
175 apply (erule exE) |
175 apply (erule exE) |
176 apply (drule ileI1) |
176 apply (drule ileI1) |
177 apply (rule iSuc_Fin [THEN subst]) |
177 apply (rule iSuc_Fin [THEN subst]) |
178 apply (rule exI) |
178 apply (rule exI) |
179 apply (erule (1) ile_iless_trans) |
179 apply (erule (1) ile_iless_trans) |
180 done |
180 done |
181 |
181 |
182 end |
182 end |