equal
deleted
inserted
replaced
6 Lemmas for theory porder.thy |
6 Lemmas for theory porder.thy |
7 *) |
7 *) |
8 |
8 |
9 open Porder0; |
9 open Porder0; |
10 open Porder; |
10 open Porder; |
|
11 |
|
12 |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 (* the reverse law of anti--symmetrie of << *) |
|
15 (* ------------------------------------------------------------------------ *) |
|
16 |
|
17 val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x" |
|
18 (fn prems => |
|
19 [ |
|
20 (cut_facts_tac prems 1), |
|
21 (rtac conjI 1), |
|
22 ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)), |
|
23 ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1)) |
|
24 ]); |
|
25 |
11 |
26 |
12 val box_less = prove_goal Porder.thy |
27 val box_less = prove_goal Porder.thy |
13 "[| a << b; c << a; b << d|] ==> c << d" |
28 "[| a << b; c << a; b << d|] ==> c << d" |
14 (fn prems => |
29 (fn prems => |
15 [ |
30 [ |
70 (atac 1), |
85 (atac 1), |
71 (hyp_subst_tac 1), |
86 (hyp_subst_tac 1), |
72 (rtac refl_less 1) |
87 (rtac refl_less 1) |
73 ]); |
88 ]); |
74 |
89 |
75 (* ------------------------------------------------------------------------ *) |
|
76 (* Lemma for reasoning by cases on the natural numbers *) |
|
77 (* ------------------------------------------------------------------------ *) |
|
78 |
|
79 val nat_less_cases = prove_goal Porder.thy |
|
80 "[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)" |
|
81 ( fn prems => |
|
82 [ |
|
83 (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1), |
|
84 (etac disjE 2), |
|
85 (etac (hd (tl (tl prems))) 1), |
|
86 (etac (sym RS hd (tl prems)) 1), |
|
87 (etac (hd prems) 1) |
|
88 ]); |
|
89 |
90 |
90 (* ------------------------------------------------------------------------ *) |
91 (* ------------------------------------------------------------------------ *) |
91 (* The range of a chain is a totaly ordered << *) |
92 (* The range of a chain is a totaly ordered << *) |
92 (* ------------------------------------------------------------------------ *) |
93 (* ------------------------------------------------------------------------ *) |
93 |
94 |
121 (atac 1) |
122 (atac 1) |
122 ]); |
123 ]); |
123 |
124 |
124 |
125 |
125 (* ------------------------------------------------------------------------ *) |
126 (* ------------------------------------------------------------------------ *) |
126 (* technical lemmas about lub and is_lub, use above results about @ *) |
127 (* technical lemmas about lub and is_lub *) |
127 (* ------------------------------------------------------------------------ *) |
128 (* ------------------------------------------------------------------------ *) |
128 |
129 |
129 val lubI = prove_goal Porder.thy "(? x. M <<| x) ==> M <<| lub(M)" |
130 val lubI = prove_goal Porder.thy "(? x. M <<| x) ==> M <<| lub(M)" |
130 (fn prems => |
131 (fn prems => |
131 [ |
132 [ |
299 |
300 |
300 (* ------------------------------------------------------------------------ *) |
301 (* ------------------------------------------------------------------------ *) |
301 (* end of prototype lemmas for class pcpo *) |
302 (* end of prototype lemmas for class pcpo *) |
302 (* ------------------------------------------------------------------------ *) |
303 (* ------------------------------------------------------------------------ *) |
303 |
304 |
304 |
|
305 (* ------------------------------------------------------------------------ *) |
|
306 (* the reverse law of anti--symmetrie of << *) |
|
307 (* ------------------------------------------------------------------------ *) |
|
308 |
|
309 val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x" |
|
310 (fn prems => |
|
311 [ |
|
312 (cut_facts_tac prems 1), |
|
313 (rtac conjI 1), |
|
314 ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)), |
|
315 ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1)) |
|
316 ]); |
|
317 |
305 |
318 (* ------------------------------------------------------------------------ *) |
306 (* ------------------------------------------------------------------------ *) |
319 (* results about finite chains *) |
307 (* results about finite chains *) |
320 (* ------------------------------------------------------------------------ *) |
308 (* ------------------------------------------------------------------------ *) |
321 |
309 |