# HG changeset patch
# User paulson
# Date 1024048624 -7200
# Node ID ba84715f6785f0bf527fe2192f3b8050f5b1be13
# Parent  aabdb4b336253081066feadec7291a0ab7d4001a
better proof of ord_iso_restrict_pred

diff -r aabdb4b33625 -r ba84715f6785 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Thu Jun 13 17:22:10 2002 +0200
+++ b/src/ZF/Order.thy	Fri Jun 14 11:57:04 2002 +0200
@@ -394,16 +394,20 @@
 apply (auto simp add: right_inverse_bij  bij_is_fun [THEN apply_funtype])
 done
 
+lemma ord_iso_restrict_image:
+     "[| f : ord_iso(A,r,B,s);  C<=A |] 
+      ==> restrict(f,C) : ord_iso(C, r, f``C, s)"
+apply (simp add: ord_iso_def) 
+apply (blast intro: bij_is_inj restrict_bij) 
+done
+
 (*But in use, A and B may themselves be initial segments.  Then use
   trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
-lemma ord_iso_restrict_pred: "[| f : ord_iso(A,r,B,s);   a:A |] ==>
-       restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
-apply (simp add: ord_iso_image_pred [symmetric])
-apply (simp add: ord_iso_def, clarify)
-apply (rule conjI)
-apply (erule restrict_bij [OF bij_is_inj pred_subset])
-apply (frule bij_is_fun)
-apply (auto simp add: pred_def)
+lemma ord_iso_restrict_pred:
+   "[| f : ord_iso(A,r,B,s);   a:A |]
+    ==> restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
+apply (simp add: ord_iso_image_pred [symmetric]) 
+apply (blast intro: ord_iso_restrict_image elim: predE) 
 done
 
 (*Tricky; a lot of forward proof!*)