equal
deleted
inserted
replaced
17 br inf_is_inf 1; |
17 br inf_is_inf 1; |
18 ba 1; |
18 ba 1; |
19 qed "inf_uniq"; |
19 qed "inf_uniq"; |
20 |
20 |
21 goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf"; |
21 goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf"; |
22 by (safe_tac HOL_cs); |
22 by (safe_tac (!claset)); |
23 by (step_tac HOL_cs 1); |
23 by (Step_tac 1); |
24 by (step_tac HOL_cs 1); |
24 by (Step_tac 1); |
25 br inf_is_inf 1; |
25 br inf_is_inf 1; |
26 br (inf_uniq RS mp RS sym) 1; |
26 br (inf_uniq RS mp RS sym) 1; |
27 ba 1; |
27 ba 1; |
28 qed "ex1_inf"; |
28 qed "ex1_inf"; |
29 |
29 |
39 br sup_is_sup 1; |
39 br sup_is_sup 1; |
40 ba 1; |
40 ba 1; |
41 qed "sup_uniq"; |
41 qed "sup_uniq"; |
42 |
42 |
43 goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup"; |
43 goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup"; |
44 by (safe_tac HOL_cs); |
44 by (safe_tac (!claset)); |
45 by (step_tac HOL_cs 1); |
45 by (Step_tac 1); |
46 by (step_tac HOL_cs 1); |
46 by (Step_tac 1); |
47 br sup_is_sup 1; |
47 br sup_is_sup 1; |
48 br (sup_uniq RS mp RS sym) 1; |
48 br (sup_uniq RS mp RS sym) 1; |
49 ba 1; |
49 ba 1; |
50 qed "ex1_sup"; |
50 qed "ex1_sup"; |
51 |
51 |
53 (* "&&" yields g.l.bs, "||" yields l.u.bs. --- in pieces *) |
53 (* "&&" yields g.l.bs, "||" yields l.u.bs. --- in pieces *) |
54 |
54 |
55 val tac = |
55 val tac = |
56 cut_facts_tac [inf_is_inf] 1 THEN |
56 cut_facts_tac [inf_is_inf] 1 THEN |
57 rewrite_goals_tac [inf_def, is_inf_def] THEN |
57 rewrite_goals_tac [inf_def, is_inf_def] THEN |
58 fast_tac HOL_cs 1; |
58 Fast_tac 1; |
59 |
59 |
60 goal thy "x && y [= x"; |
60 goal thy "x && y [= x"; |
61 by tac; |
61 by tac; |
62 qed "inf_lb1"; |
62 qed "inf_lb1"; |
63 |
63 |
72 |
72 |
73 |
73 |
74 val tac = |
74 val tac = |
75 cut_facts_tac [sup_is_sup] 1 THEN |
75 cut_facts_tac [sup_is_sup] 1 THEN |
76 rewrite_goals_tac [sup_def, is_sup_def] THEN |
76 rewrite_goals_tac [sup_def, is_sup_def] THEN |
77 fast_tac HOL_cs 1; |
77 Fast_tac 1; |
78 |
78 |
79 goal thy "x [= x || y"; |
79 goal thy "x [= x || y"; |
80 by tac; |
80 by tac; |
81 qed "sup_ub1"; |
81 qed "sup_ub1"; |
82 |
82 |
104 br (inf_uniq RS mp) 1; |
104 br (inf_uniq RS mp) 1; |
105 by (rewtac is_inf_def); |
105 by (rewtac is_inf_def); |
106 by (REPEAT_FIRST (rtac conjI)); |
106 by (REPEAT_FIRST (rtac conjI)); |
107 br le_refl 1; |
107 br le_refl 1; |
108 ba 1; |
108 ba 1; |
109 by (fast_tac HOL_cs 1); |
109 by (Fast_tac 1); |
110 qed "inf_connect"; |
110 qed "inf_connect"; |
111 |
111 |
112 goal thy "(x || y = y) = (x [= y)"; |
112 goal thy "(x || y = y) = (x [= y)"; |
113 br iffI 1; |
113 br iffI 1; |
114 (*==>*) |
114 (*==>*) |
118 br (sup_uniq RS mp) 1; |
118 br (sup_uniq RS mp) 1; |
119 by (rewtac is_sup_def); |
119 by (rewtac is_sup_def); |
120 by (REPEAT_FIRST (rtac conjI)); |
120 by (REPEAT_FIRST (rtac conjI)); |
121 ba 1; |
121 ba 1; |
122 br le_refl 1; |
122 br le_refl 1; |
123 by (fast_tac HOL_cs 1); |
123 by (Fast_tac 1); |
124 qed "sup_connect"; |
124 qed "sup_connect"; |
125 |
125 |
126 |
126 |
127 (* minorized infs / majorized sups *) |
127 (* minorized infs / majorized sups *) |
128 |
128 |