3 |
3 |
4 |
4 |
5 (** monotone functions vs. "&&"- / "||"-semi-morphisms **) |
5 (** monotone functions vs. "&&"- / "||"-semi-morphisms **) |
6 |
6 |
7 goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)"; |
7 goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)"; |
8 by (safe_tac set_cs); |
8 by (safe_tac (!claset)); |
9 (*==> (level 1)*) |
9 (*==> (level 1)*) |
10 by (stac le_inf_eq 1); |
10 by (stac le_inf_eq 1); |
11 br conjI 1; |
11 br conjI 1; |
12 by (step_tac set_cs 1); |
12 by (Step_tac 1); |
13 by (step_tac set_cs 1); |
13 by (Step_tac 1); |
14 be mp 1; |
14 be mp 1; |
15 br inf_lb1 1; |
15 br inf_lb1 1; |
16 by (step_tac set_cs 1); |
16 by (Step_tac 1); |
17 by (step_tac set_cs 1); |
17 by (Step_tac 1); |
18 be mp 1; |
18 be mp 1; |
19 br inf_lb2 1; |
19 br inf_lb2 1; |
20 (*==> (level 11)*) |
20 (*==> (level 11)*) |
21 br (conjI RS (le_trans RS mp)) 1; |
21 br (conjI RS (le_trans RS mp)) 1; |
22 br inf_lb2 2; |
22 br inf_lb2 2; |
23 by (subgoal_tac "x && y = x" 1); |
23 by (subgoal_tac "x && y = x" 1); |
24 be subst 1; |
24 be subst 1; |
25 by (fast_tac set_cs 1); |
25 by (Fast_tac 1); |
26 by (stac inf_connect 1); |
26 by (stac inf_connect 1); |
27 ba 1; |
27 ba 1; |
28 qed "mono_inf_eq"; |
28 qed "mono_inf_eq"; |
29 |
29 |
30 goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))"; |
30 goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))"; |
31 by (safe_tac set_cs); |
31 by (safe_tac (!claset)); |
32 (*==> (level 1)*) |
32 (*==> (level 1)*) |
33 by (stac ge_sup_eq 1); |
33 by (stac ge_sup_eq 1); |
34 br conjI 1; |
34 br conjI 1; |
35 by (step_tac set_cs 1); |
35 by (Step_tac 1); |
36 by (step_tac set_cs 1); |
36 by (Step_tac 1); |
37 be mp 1; |
37 be mp 1; |
38 br sup_ub1 1; |
38 br sup_ub1 1; |
39 by (step_tac set_cs 1); |
39 by (Step_tac 1); |
40 by (step_tac set_cs 1); |
40 by (Step_tac 1); |
41 be mp 1; |
41 be mp 1; |
42 br sup_ub2 1; |
42 br sup_ub2 1; |
43 (*==> (level 11)*) |
43 (*==> (level 11)*) |
44 br (conjI RS (le_trans RS mp)) 1; |
44 br (conjI RS (le_trans RS mp)) 1; |
45 br sup_ub1 1; |
45 br sup_ub1 1; |
46 by (subgoal_tac "x || y = y" 1); |
46 by (subgoal_tac "x || y = y" 1); |
47 be subst 1; |
47 be subst 1; |
48 by (fast_tac set_cs 1); |
48 by (Fast_tac 1); |
49 by (stac sup_connect 1); |
49 by (stac sup_connect 1); |
50 ba 1; |
50 ba 1; |
51 qed "mono_sup_eq"; |
51 qed "mono_sup_eq"; |
52 |
52 |
53 |
53 |