equal
deleted
inserted
replaced
179 by (unfold OUnion_def oex_def lt_def, blast) |
179 by (unfold OUnion_def oex_def lt_def, blast) |
180 |
180 |
181 lemma OUN_cong [cong]: |
181 lemma OUN_cong [cong]: |
182 "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))" |
182 "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))" |
183 by (simp add: OUnion_def lt_def OUN_iff) |
183 by (simp add: OUnion_def lt_def OUN_iff) |
184 |
|
185 declare ltD [THEN beta, simp] |
|
186 |
184 |
187 lemma lt_induct: |
185 lemma lt_induct: |
188 "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) |] ==> P(i)" |
186 "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) |] ==> P(i)" |
189 apply (simp add: lt_def oall_def) |
187 apply (simp add: lt_def oall_def) |
190 apply (erule conjE) |
188 apply (erule conjE) |