242 by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1); |
242 by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1); |
243 by (safe_tac (ZF_cs addSEs [bij_is_fun RS apply_type])); |
243 by (safe_tac (ZF_cs addSEs [bij_is_fun RS apply_type])); |
244 by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
244 by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
245 by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
245 by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
246 qed "linear_ord_iso"; |
246 qed "linear_ord_iso"; |
247 |
|
248 (*FOR FOL/IFOL.ML*) |
|
249 fun iff_tac prems i = |
|
250 resolve_tac (prems RL [iffE]) i THEN |
|
251 REPEAT1 (eresolve_tac [asm_rl,mp] i); |
|
252 |
|
253 (*Reversed congruence rule!*) |
|
254 val conj_cong2 = prove_goal IFOL.thy |
|
255 "[| P <-> P'; P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')" |
|
256 (fn prems => |
|
257 [ (cut_facts_tac prems 1), |
|
258 (REPEAT (ares_tac [iffI,conjI] 1 |
|
259 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
|
260 ORELSE iff_tac prems 1)) ]); |
|
261 |
247 |
262 goalw Order.thy [wf_on_def, wf_def, ord_iso_def] |
248 goalw Order.thy [wf_on_def, wf_def, ord_iso_def] |
263 "!!A B r. [| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"; |
249 "!!A B r. [| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"; |
264 (*reversed &-congruence rule handles context of membership in A*) |
250 (*reversed &-congruence rule handles context of membership in A*) |
265 by (asm_full_simp_tac (ZF_ss addcongs [conj_cong2]) 1); |
251 by (asm_full_simp_tac (ZF_ss addcongs [conj_cong2]) 1); |