better proof of ord_iso_restrict_pred
authorpaulson
Fri Jun 14 11:57:04 2002 +0200 (2002-06-14)
changeset 13212ba84715f6785
parent 13211 aabdb4b33625
child 13213 833ffcb2e92d
better proof of ord_iso_restrict_pred
src/ZF/Order.thy
     1.1 --- a/src/ZF/Order.thy	Thu Jun 13 17:22:10 2002 +0200
     1.2 +++ b/src/ZF/Order.thy	Fri Jun 14 11:57:04 2002 +0200
     1.3 @@ -394,16 +394,20 @@
     1.4  apply (auto simp add: right_inverse_bij  bij_is_fun [THEN apply_funtype])
     1.5  done
     1.6  
     1.7 +lemma ord_iso_restrict_image:
     1.8 +     "[| f : ord_iso(A,r,B,s);  C<=A |] 
     1.9 +      ==> restrict(f,C) : ord_iso(C, r, f``C, s)"
    1.10 +apply (simp add: ord_iso_def) 
    1.11 +apply (blast intro: bij_is_inj restrict_bij) 
    1.12 +done
    1.13 +
    1.14  (*But in use, A and B may themselves be initial segments.  Then use
    1.15    trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
    1.16 -lemma ord_iso_restrict_pred: "[| f : ord_iso(A,r,B,s);   a:A |] ==>
    1.17 -       restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
    1.18 -apply (simp add: ord_iso_image_pred [symmetric])
    1.19 -apply (simp add: ord_iso_def, clarify)
    1.20 -apply (rule conjI)
    1.21 -apply (erule restrict_bij [OF bij_is_inj pred_subset])
    1.22 -apply (frule bij_is_fun)
    1.23 -apply (auto simp add: pred_def)
    1.24 +lemma ord_iso_restrict_pred:
    1.25 +   "[| f : ord_iso(A,r,B,s);   a:A |]
    1.26 +    ==> restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
    1.27 +apply (simp add: ord_iso_image_pred [symmetric]) 
    1.28 +apply (blast intro: ord_iso_restrict_image elim: predE) 
    1.29  done
    1.30  
    1.31  (*Tricky; a lot of forward proof!*)