author | berghofe |
Fri, 02 May 1997 16:41:35 +0200 | |
changeset 3098 | a31170b67367 |
parent 3026 | 7a5611f66b72 |
child 3323 | 194ae2e0c193 |
permissions | -rw-r--r-- |
2644 | 1 |
(* Title: HOLCF/Porder0.ML |
2 |
ID: $Id$ |
|
3 |
Author: Oscar Slotosch |
|
4 |
Copyright 1997 Technische Universitaet Muenchen |
|
5 |
||
6 |
derive the characteristic axioms for the characteristic constants *) |
|
7 |
||
8 |
open Porder0; |
|
9 |
||
10 |
qed_goalw "refl_less" thy [ po_def ] "x << x" |
|
11 |
(fn prems => |
|
12 |
[ |
|
13 |
(fast_tac (HOL_cs addSIs [ax_refl_less]) 1) |
|
14 |
]); |
|
15 |
||
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2644
diff
changeset
|
16 |
AddIffs [refl_less]; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2644
diff
changeset
|
17 |
|
2644 | 18 |
qed_goalw "antisym_less" thy [ po_def ] "[| x << y; y << x |] ==> x = y" |
19 |
(fn prems => |
|
20 |
[ |
|
21 |
(fast_tac (HOL_cs addSIs prems@[ax_antisym_less]) 1) |
|
22 |
]); |
|
23 |
||
24 |
qed_goalw "trans_less" thy [ po_def ] "[| x << y; y << z |] ==> x << z" |
|
25 |
(fn prems => |
|
26 |
[ |
|
27 |
(fast_tac (HOL_cs addIs prems@[ax_trans_less]) 1) |
|
28 |
]); |
|
29 |
||
30 |
(* ------------------------------------------------------------------------ *) |
|
31 |
(* minimal fixes least element *) |
|
32 |
(* ------------------------------------------------------------------------ *) |
|
33 |
bind_thm("minimal2UU",allI RS (prove_goal thy "!x.uu<<x==>uu=(@u.!y.u<<y)" |
|
34 |
(fn prems => |
|
35 |
[ |
|
36 |
(cut_facts_tac prems 1), |
|
37 |
(rtac antisym_less 1), |
|
38 |
(etac spec 1), |
|
39 |
(res_inst_tac [("a","uu")] selectI2 1), |
|
40 |
(atac 1), |
|
41 |
(etac spec 1) |
|
42 |
]))); |
|
3026
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
43 |
|
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
44 |
(* ------------------------------------------------------------------------ *) |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
45 |
(* the reverse law of anti--symmetrie of << *) |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
46 |
(* ------------------------------------------------------------------------ *) |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
47 |
|
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
48 |
qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x" |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
49 |
(fn prems => |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
50 |
[ |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
51 |
(cut_facts_tac prems 1), |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
52 |
(rtac conjI 1), |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
53 |
((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)), |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
54 |
((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1)) |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
55 |
]); |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
56 |
|
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
57 |
|
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
58 |
qed_goal "box_less" thy |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
59 |
"[| a << b; c << a; b << d|] ==> c << d" |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
60 |
(fn prems => |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
61 |
[ |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
62 |
(cut_facts_tac prems 1), |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
63 |
(etac trans_less 1), |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
64 |
(etac trans_less 1), |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
65 |
(atac 1) |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
66 |
]); |
7a5611f66b72
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
slotosch
parents:
2841
diff
changeset
|
67 |