equal
deleted
inserted
replaced
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Proves that 'a discr is a po |
6 Proves that 'a discr is a po |
7 *) |
7 *) |
8 |
8 |
9 Goalw [less_discr_def] "(x::('a::term)discr) << x"; |
9 Goalw [less_discr_def] "(x::('a::type)discr) << x"; |
10 by (rtac refl 1); |
10 by (rtac refl 1); |
11 qed "less_discr_refl"; |
11 qed "less_discr_refl"; |
12 |
12 |
13 Goalw [less_discr_def] |
13 Goalw [less_discr_def] |
14 "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x << z"; |
14 "!!x. [| (x::('a::type)discr) << y; y << z |] ==> x << z"; |
15 by (etac trans 1); |
15 by (etac trans 1); |
16 by (assume_tac 1); |
16 by (assume_tac 1); |
17 qed "less_discr_trans"; |
17 qed "less_discr_trans"; |
18 |
18 |
19 Goalw [less_discr_def] |
19 Goalw [less_discr_def] |
20 "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y"; |
20 "!!x. [| (x::('a::type)discr) << y; y << x |] ==> x=y"; |
21 by (assume_tac 1); |
21 by (assume_tac 1); |
22 qed "less_discr_antisym"; |
22 qed "less_discr_antisym"; |