Added Krzysztof's theorems irrefl_converse, trans_on_converse,
authorlcp
Fri Dec 23 16:35:42 1994 +0100 (1994-12-23 ago)
changeset 836627f4842b020
parent 835 313ac9b513f1
child 837 778f01546669
Added Krzysztof's theorems irrefl_converse, trans_on_converse,
part_ord_converse, linear_converse, tot_ord_converse,
Proved rvimage_converse, ord_iso_rvimage_eq
src/ZF/Order.ML
     1.1 --- a/src/ZF/Order.ML	Fri Dec 23 16:35:08 1994 +0100
     1.2 +++ b/src/ZF/Order.ML	Fri Dec 23 16:35:42 1994 +0100
     1.3 @@ -99,6 +99,7 @@
     1.4  by (fast_tac eq_cs 1);
     1.5  qed "trans_pred_pred_eq";
     1.6  
     1.7 +
     1.8  (** The ordering's properties hold over all subsets of its domain 
     1.9      [including initial segments of the form pred(A,x,r) **)
    1.10  
    1.11 @@ -124,6 +125,39 @@
    1.12  qed "well_ord_subset";
    1.13  
    1.14  
    1.15 +(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
    1.16 +
    1.17 +goalw Order.thy [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)";
    1.18 +by (fast_tac ZF_cs 1);
    1.19 +qed "irrefl_Int_iff";
    1.20 +
    1.21 +goalw Order.thy [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)";
    1.22 +by (fast_tac ZF_cs 1);
    1.23 +qed "trans_on_Int_iff";
    1.24 +
    1.25 +goalw Order.thy [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)";
    1.26 +by (simp_tac (ZF_ss addsimps [irrefl_Int_iff, trans_on_Int_iff]) 1);
    1.27 +qed "part_ord_Int_iff";
    1.28 +
    1.29 +goalw Order.thy [linear_def] "linear(A,r Int A*A) <-> linear(A,r)";
    1.30 +by (fast_tac ZF_cs 1);
    1.31 +qed "linear_Int_iff";
    1.32 +
    1.33 +goalw Order.thy [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)";
    1.34 +by (simp_tac (ZF_ss addsimps [part_ord_Int_iff, linear_Int_iff]) 1);
    1.35 +qed "tot_ord_Int_iff";
    1.36 +
    1.37 +goalw Order.thy [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)";
    1.38 +by (fast_tac ZF_cs 1);
    1.39 +qed "wf_on_Int_iff";
    1.40 +
    1.41 +goalw Order.thy [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)";
    1.42 +by (simp_tac (ZF_ss addsimps [tot_ord_Int_iff, wf_on_Int_iff]) 1);
    1.43 +qed "well_ord_Int_iff";
    1.44 +
    1.45 +
    1.46 +
    1.47 +
    1.48  (** Order-preserving (monotone) maps **)
    1.49  
    1.50  goalw Order.thy [mono_map_def] 
    1.51 @@ -527,3 +561,30 @@
    1.52  by (fast_tac ZF_cs 1);
    1.53  qed "well_ord_trichotomy";
    1.54  
    1.55 +
    1.56 +(*** Properties of converse(r), by Krzysztof Grabczewski ***)
    1.57 +
    1.58 +goalw Order.thy [irrefl_def] 
    1.59 +            "!!A. irrefl(A,r) ==> irrefl(A,converse(r))";
    1.60 +by (fast_tac (ZF_cs addSIs [converseI]) 1);
    1.61 +qed "irrefl_converse";
    1.62 +
    1.63 +goalw Order.thy [trans_on_def] 
    1.64 +    "!!A. trans[A](r) ==> trans[A](converse(r))";
    1.65 +by (fast_tac (ZF_cs addSIs [converseI]) 1);
    1.66 +qed "trans_on_converse";
    1.67 +
    1.68 +goalw Order.thy [part_ord_def] 
    1.69 +    "!!A. part_ord(A,r) ==> part_ord(A,converse(r))";
    1.70 +by (fast_tac (ZF_cs addSIs [irrefl_converse, trans_on_converse]) 1);
    1.71 +qed "part_ord_converse";
    1.72 +
    1.73 +goalw Order.thy [linear_def] 
    1.74 +    "!!A. linear(A,r) ==> linear(A,converse(r))";
    1.75 +by (fast_tac (ZF_cs addSIs [converseI]) 1);
    1.76 +qed "linear_converse";
    1.77 +
    1.78 +goalw Order.thy [tot_ord_def] 
    1.79 +    "!!A. tot_ord(A,r) ==> tot_ord(A,converse(r))";
    1.80 +by (fast_tac (ZF_cs addSIs [part_ord_converse, linear_converse]) 1);
    1.81 +qed "tot_ord_converse";