equal
deleted
inserted
replaced
178 (*** ordermap preserves the orderings in both directions ***) |
178 (*** ordermap preserves the orderings in both directions ***) |
179 |
179 |
180 lemma ordermap_mono: |
180 lemma ordermap_mono: |
181 "[| <w,x>: r; wf[A](r); w: A; x: A |] |
181 "[| <w,x>: r; wf[A](r); w: A; x: A |] |
182 ==> ordermap(A,r)`w : ordermap(A,r)`x" |
182 ==> ordermap(A,r)`w : ordermap(A,r)`x" |
183 apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption) |
183 apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption, blast) |
184 apply blast |
|
185 done |
184 done |
186 |
185 |
187 (*linearity of r is crucial here*) |
186 (*linearity of r is crucial here*) |
188 lemma converse_ordermap_mono: |
187 lemma converse_ordermap_mono: |
189 "[| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); w: A; x: A |] |
188 "[| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); w: A; x: A |] |