equal
deleted
inserted
replaced
|
1 |
|
2 open LatMorph; |
|
3 |
|
4 |
|
5 (** monotone functions vs. "&&"- / "||"-semi-morphisms **) |
|
6 |
|
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); |
|
9 (*==> (level 1)*) |
|
10 by (stac le_inf_eq 1); |
|
11 br conjI 1; |
|
12 by (step_tac set_cs 1); |
|
13 by (step_tac set_cs 1); |
|
14 be mp 1; |
|
15 br inf_lb1 1; |
|
16 by (step_tac set_cs 1); |
|
17 by (step_tac set_cs 1); |
|
18 be mp 1; |
|
19 br inf_lb2 1; |
|
20 (*==> (level 11)*) |
|
21 br (conjI RS (le_trans RS mp)) 1; |
|
22 br inf_lb2 2; |
|
23 by (subgoal_tac "x && y = x" 1); |
|
24 be subst 1; |
|
25 by (fast_tac set_cs 1); |
|
26 by (stac inf_connect 1); |
|
27 ba 1; |
|
28 qed "mono_inf_eq"; |
|
29 |
|
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); |
|
32 (*==> (level 1)*) |
|
33 by (stac ge_sup_eq 1); |
|
34 br conjI 1; |
|
35 by (step_tac set_cs 1); |
|
36 by (step_tac set_cs 1); |
|
37 be mp 1; |
|
38 br sup_ub1 1; |
|
39 by (step_tac set_cs 1); |
|
40 by (step_tac set_cs 1); |
|
41 be mp 1; |
|
42 br sup_ub2 1; |
|
43 (*==> (level 11)*) |
|
44 br (conjI RS (le_trans RS mp)) 1; |
|
45 br sup_ub1 1; |
|
46 by (subgoal_tac "x || y = y" 1); |
|
47 be subst 1; |
|
48 by (fast_tac set_cs 1); |
|
49 by (stac sup_connect 1); |
|
50 ba 1; |
|
51 qed "mono_sup_eq"; |
|
52 |
|
53 |