20 |
20 |
21 (* pairs *) |
21 (* pairs *) |
22 |
22 |
23 goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)"; |
23 goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)"; |
24 by (Simp_tac 1); |
24 by (Simp_tac 1); |
25 by (safe_tac HOL_cs); |
25 by (safe_tac (!claset)); |
26 by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i)); |
26 by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i)); |
27 qed "prod_is_inf"; |
27 qed "prod_is_inf"; |
28 |
28 |
29 goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)"; |
29 goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)"; |
30 by (Simp_tac 1); |
30 by (Simp_tac 1); |
31 by (safe_tac HOL_cs); |
31 by (safe_tac (!claset)); |
32 by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i)); |
32 by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i)); |
33 qed "prod_is_sup"; |
33 qed "prod_is_sup"; |
34 |
34 |
35 |
35 |
36 (* functions *) |
36 (* functions *) |
37 |
37 |
38 goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)"; |
38 goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)"; |
39 by (safe_tac HOL_cs); |
39 by (safe_tac (!claset)); |
40 br inf_lb1 1; |
40 br inf_lb1 1; |
41 br inf_lb2 1; |
41 br inf_lb2 1; |
42 br inf_ub_lbs 1; |
42 br inf_ub_lbs 1; |
43 by (REPEAT_FIRST (fast_tac HOL_cs)); |
43 by (REPEAT_FIRST (Fast_tac)); |
44 qed "fun_is_inf"; |
44 qed "fun_is_inf"; |
45 |
45 |
46 goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)"; |
46 goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)"; |
47 by (safe_tac HOL_cs); |
47 by (safe_tac (!claset)); |
48 br sup_ub1 1; |
48 br sup_ub1 1; |
49 br sup_ub2 1; |
49 br sup_ub2 1; |
50 br sup_lb_ubs 1; |
50 br sup_lb_ubs 1; |
51 by (REPEAT_FIRST (fast_tac HOL_cs)); |
51 by (REPEAT_FIRST (Fast_tac)); |
52 qed "fun_is_sup"; |
52 qed "fun_is_sup"; |
53 |
53 |
54 |
54 |
55 |
55 |
56 (** dual lattices **) |
56 (** dual lattices **) |
57 |
57 |
58 goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))"; |
58 goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))"; |
59 by (stac Abs_dual_inverse' 1); |
59 by (stac Abs_dual_inverse' 1); |
60 by (safe_tac HOL_cs); |
60 by (safe_tac (!claset)); |
61 br sup_ub1 1; |
61 br sup_ub1 1; |
62 br sup_ub2 1; |
62 br sup_ub2 1; |
63 br sup_lb_ubs 1; |
63 br sup_lb_ubs 1; |
64 ba 1; |
64 ba 1; |
65 ba 1; |
65 ba 1; |
66 qed "dual_is_inf"; |
66 qed "dual_is_inf"; |
67 |
67 |
68 goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))"; |
68 goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))"; |
69 by (stac Abs_dual_inverse' 1); |
69 by (stac Abs_dual_inverse' 1); |
70 by (safe_tac HOL_cs); |
70 by (safe_tac (!claset)); |
71 br inf_lb1 1; |
71 br inf_lb1 1; |
72 br inf_lb2 1; |
72 br inf_lb2 1; |
73 br inf_ub_lbs 1; |
73 br inf_ub_lbs 1; |
74 ba 1; |
74 ba 1; |
75 ba 1; |
75 ba 1; |