1 |
|
2 |
|
3 (** complete lattices **) |
|
4 |
|
5 Goal "is_inf x y (Inf {x, y})"; |
|
6 by (rtac (bin_is_Inf_eq RS subst) 1); |
|
7 by (rtac Inf_is_Inf 1); |
|
8 qed "Inf_is_inf"; |
|
9 |
|
10 Goal "is_sup x y (Sup {x, y})"; |
|
11 by (rtac (bin_is_Sup_eq RS subst) 1); |
|
12 by (rtac Sup_is_Sup 1); |
|
13 qed "Sup_is_sup"; |
|
14 |
|
15 |
|
16 |
|
17 (** product lattices **) |
|
18 |
|
19 (* pairs *) |
|
20 |
|
21 Goalw [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)"; |
|
22 by (Simp_tac 1); |
|
23 by Safe_tac; |
|
24 by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i)); |
|
25 qed "prod_is_inf"; |
|
26 |
|
27 Goalw [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)"; |
|
28 by (Simp_tac 1); |
|
29 by Safe_tac; |
|
30 by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i)); |
|
31 qed "prod_is_sup"; |
|
32 |
|
33 |
|
34 (* functions *) |
|
35 |
|
36 Goalw [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)"; |
|
37 by Safe_tac; |
|
38 by (rtac inf_lb1 1); |
|
39 by (rtac inf_lb2 1); |
|
40 by (rtac inf_ub_lbs 1); |
|
41 by (REPEAT_FIRST (Fast_tac)); |
|
42 qed "fun_is_inf"; |
|
43 |
|
44 Goalw [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)"; |
|
45 by Safe_tac; |
|
46 by (rtac sup_ub1 1); |
|
47 by (rtac sup_ub2 1); |
|
48 by (rtac sup_lb_ubs 1); |
|
49 by (REPEAT_FIRST (Fast_tac)); |
|
50 qed "fun_is_sup"; |
|
51 |
|
52 |
|
53 |
|
54 (** dual lattices **) |
|
55 |
|
56 Goalw [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))"; |
|
57 by (stac Abs_dual_inverse' 1); |
|
58 by Safe_tac; |
|
59 by (rtac sup_ub1 1); |
|
60 by (rtac sup_ub2 1); |
|
61 by (rtac sup_lb_ubs 1); |
|
62 by (assume_tac 1); |
|
63 by (assume_tac 1); |
|
64 qed "dual_is_inf"; |
|
65 |
|
66 Goalw [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))"; |
|
67 by (stac Abs_dual_inverse' 1); |
|
68 by Safe_tac; |
|
69 by (rtac inf_lb1 1); |
|
70 by (rtac inf_lb2 1); |
|
71 by (rtac inf_ub_lbs 1); |
|
72 by (assume_tac 1); |
|
73 by (assume_tac 1); |
|
74 qed "dual_is_sup"; |
|