5 (** lifting of quasi / partial orders **) |
5 (** lifting of quasi / partial orders **) |
6 |
6 |
7 (* pairs *) |
7 (* pairs *) |
8 |
8 |
9 goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)"; |
9 goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)"; |
10 br conjI 1; |
10 by (rtac conjI 1); |
11 br le_refl 1; |
11 by (rtac le_refl 1); |
12 br le_refl 1; |
12 by (rtac le_refl 1); |
13 qed "le_prod_refl"; |
13 qed "le_prod_refl"; |
14 |
14 |
15 goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)"; |
15 goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)"; |
16 by (safe_tac (claset())); |
16 by Safe_tac; |
17 be (conjI RS (le_trans RS mp)) 1; |
17 by (etac (conjI RS (le_trans RS mp)) 1); |
18 ba 1; |
18 by (assume_tac 1); |
19 be (conjI RS (le_trans RS mp)) 1; |
19 by (etac (conjI RS (le_trans RS mp)) 1); |
20 ba 1; |
20 by (assume_tac 1); |
21 qed "le_prod_trans"; |
21 qed "le_prod_trans"; |
22 |
22 |
23 goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)"; |
23 goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)"; |
24 by (safe_tac (claset())); |
24 by Safe_tac; |
25 by (stac Pair_fst_snd_eq 1); |
25 by (stac Pair_fst_snd_eq 1); |
26 br conjI 1; |
26 by (rtac conjI 1); |
27 be (conjI RS (le_antisym RS mp)) 1; |
27 by (etac (conjI RS (le_antisym RS mp)) 1); |
28 ba 1; |
28 by (assume_tac 1); |
29 be (conjI RS (le_antisym RS mp)) 1; |
29 by (etac (conjI RS (le_antisym RS mp)) 1); |
30 ba 1; |
30 by (assume_tac 1); |
31 qed "le_prod_antisym"; |
31 qed "le_prod_antisym"; |
32 |
32 |
33 |
33 |
34 (* functions *) |
34 (* functions *) |
35 |
35 |
36 goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)"; |
36 goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)"; |
37 br allI 1; |
37 by (rtac allI 1); |
38 br le_refl 1; |
38 by (rtac le_refl 1); |
39 qed "le_fun_refl"; |
39 qed "le_fun_refl"; |
40 |
40 |
41 goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)"; |
41 goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)"; |
42 by (safe_tac (claset())); |
42 by Safe_tac; |
43 br (le_trans RS mp) 1; |
43 by (rtac (le_trans RS mp) 1); |
44 by (Fast_tac 1); |
44 by (Fast_tac 1); |
45 qed "le_fun_trans"; |
45 qed "le_fun_trans"; |
46 |
46 |
47 goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)"; |
47 goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)"; |
48 by (safe_tac (claset())); |
48 by Safe_tac; |
49 br ext 1; |
49 by (rtac ext 1); |
50 br (le_antisym RS mp) 1; |
50 by (rtac (le_antisym RS mp) 1); |
51 by (Fast_tac 1); |
51 by (Fast_tac 1); |
52 qed "le_fun_antisym"; |
52 qed "le_fun_antisym"; |
53 |
53 |
54 |
54 |
55 |
55 |
56 (** duals **) |
56 (** duals **) |
57 |
57 |
58 (*"'a dual" is even an isotype*) |
58 (*"'a dual" is even an isotype*) |
59 goal thy "Rep_dual (Abs_dual y) = y"; |
59 goal thy "Rep_dual (Abs_dual y) = y"; |
60 br Abs_dual_inverse 1; |
60 by (rtac Abs_dual_inverse 1); |
61 by (rewtac dual_def); |
61 by (rewtac dual_def); |
62 by (Fast_tac 1); |
62 by (Fast_tac 1); |
63 qed "Abs_dual_inverse'"; |
63 qed "Abs_dual_inverse'"; |
64 |
64 |
65 |
65 |
66 goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)"; |
66 goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)"; |
67 br le_refl 1; |
67 by (rtac le_refl 1); |
68 qed "le_dual_refl"; |
68 qed "le_dual_refl"; |
69 |
69 |
70 goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)"; |
70 goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)"; |
71 by (stac conj_commut 1); |
71 by (stac conj_commut 1); |
72 br le_trans 1; |
72 by (rtac le_trans 1); |
73 qed "le_dual_trans"; |
73 qed "le_dual_trans"; |
74 |
74 |
75 goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)"; |
75 goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)"; |
76 by (safe_tac (claset())); |
76 by Safe_tac; |
77 br (Rep_dual_inverse RS subst) 1; |
77 by (rtac (Rep_dual_inverse RS subst) 1); |
78 br sym 1; |
78 by (rtac sym 1); |
79 br (Rep_dual_inverse RS subst) 1; |
79 by (rtac (Rep_dual_inverse RS subst) 1); |
80 br arg_cong 1; |
80 by (rtac arg_cong 1); |
81 back(); |
81 back(); |
82 be (conjI RS (le_antisym RS mp)) 1; |
82 by (etac (conjI RS (le_antisym RS mp)) 1); |
83 ba 1; |
83 by (assume_tac 1); |
84 qed "le_dual_antisym"; |
84 qed "le_dual_antisym"; |
85 |
85 |
86 goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)"; |
86 goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)"; |
87 br le_linear 1; |
87 by (rtac le_linear 1); |
88 qed "le_dual_linear"; |
88 qed "le_dual_linear"; |