equal
deleted
inserted
replaced
1 |
1 |
2 open LatInsts; |
2 open LatInsts; |
3 |
3 |
4 |
4 |
5 goal thy "Inf {x, y} = x && y"; |
5 Goal "Inf {x, y} = x && y"; |
6 by (rtac (Inf_uniq RS mp) 1); |
6 by (rtac (Inf_uniq RS mp) 1); |
7 by (stac bin_is_Inf_eq 1); |
7 by (stac bin_is_Inf_eq 1); |
8 by (rtac inf_is_inf 1); |
8 by (rtac inf_is_inf 1); |
9 qed "bin_Inf_eq"; |
9 qed "bin_Inf_eq"; |
10 |
10 |
11 goal thy "Sup {x, y} = x || y"; |
11 Goal "Sup {x, y} = x || y"; |
12 by (rtac (Sup_uniq RS mp) 1); |
12 by (rtac (Sup_uniq RS mp) 1); |
13 by (stac bin_is_Sup_eq 1); |
13 by (stac bin_is_Sup_eq 1); |
14 by (rtac sup_is_sup 1); |
14 by (rtac sup_is_sup 1); |
15 qed "bin_Sup_eq"; |
15 qed "bin_Sup_eq"; |
16 |
16 |
17 |
17 |
18 |
18 |
19 (* Unions and limits *) |
19 (* Unions and limits *) |
20 |
20 |
21 goal thy "Inf (A Un B) = Inf A && Inf B"; |
21 Goal "Inf (A Un B) = Inf A && Inf B"; |
22 by (rtac (Inf_uniq RS mp) 1); |
22 by (rtac (Inf_uniq RS mp) 1); |
23 by (rewtac is_Inf_def); |
23 by (rewtac is_Inf_def); |
24 by Safe_tac; |
24 by Safe_tac; |
25 |
25 |
26 by (rtac (conjI RS (le_trans RS mp)) 1); |
26 by (rtac (conjI RS (le_trans RS mp)) 1); |
37 by (Fast_tac 1); |
37 by (Fast_tac 1); |
38 by (rtac Inf_ub_lbs 1); |
38 by (rtac Inf_ub_lbs 1); |
39 by (Fast_tac 1); |
39 by (Fast_tac 1); |
40 qed "Inf_Un_eq"; |
40 qed "Inf_Un_eq"; |
41 |
41 |
42 goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}"; |
42 Goal "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}"; |
43 by (rtac (Inf_uniq RS mp) 1); |
43 by (rtac (Inf_uniq RS mp) 1); |
44 by (rewtac is_Inf_def); |
44 by (rewtac is_Inf_def); |
45 by Safe_tac; |
45 by Safe_tac; |
46 (*level 3*) |
46 (*level 3*) |
47 by (rtac (conjI RS (le_trans RS mp)) 1); |
47 by (rtac (conjI RS (le_trans RS mp)) 1); |
56 by (Fast_tac 1); |
56 by (Fast_tac 1); |
57 qed "Inf_UN_eq"; |
57 qed "Inf_UN_eq"; |
58 |
58 |
59 |
59 |
60 |
60 |
61 goal thy "Sup (A Un B) = Sup A || Sup B"; |
61 Goal "Sup (A Un B) = Sup A || Sup B"; |
62 by (rtac (Sup_uniq RS mp) 1); |
62 by (rtac (Sup_uniq RS mp) 1); |
63 by (rewtac is_Sup_def); |
63 by (rewtac is_Sup_def); |
64 by Safe_tac; |
64 by Safe_tac; |
65 |
65 |
66 by (rtac (conjI RS (le_trans RS mp)) 1); |
66 by (rtac (conjI RS (le_trans RS mp)) 1); |
77 by (Fast_tac 1); |
77 by (Fast_tac 1); |
78 by (rtac Sup_lb_ubs 1); |
78 by (rtac Sup_lb_ubs 1); |
79 by (Fast_tac 1); |
79 by (Fast_tac 1); |
80 qed "Sup_Un_eq"; |
80 qed "Sup_Un_eq"; |
81 |
81 |
82 goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}"; |
82 Goal "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}"; |
83 by (rtac (Sup_uniq RS mp) 1); |
83 by (rtac (Sup_uniq RS mp) 1); |
84 by (rewtac is_Sup_def); |
84 by (rewtac is_Sup_def); |
85 by Safe_tac; |
85 by Safe_tac; |
86 (*level 3*) |
86 (*level 3*) |
87 by (rtac (conjI RS (le_trans RS mp)) 1); |
87 by (rtac (conjI RS (le_trans RS mp)) 1); |