|
7626
|
1 |
(* Title: HOL/BCV/Types.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
Goalw [semilat_def,le_typ,plus_typ] "semilat (UNIV::typ set)";
|
|
|
8 |
by(Auto_tac);
|
|
|
9 |
qed "semilat_typ";
|
|
|
10 |
AddIffs [semilat_typ];
|
|
|
11 |
|
|
|
12 |
Goal "{(x,y::'a::order). y<x}^+ = {(x,y::'a::order). y<x}";
|
|
|
13 |
by(Auto_tac);
|
|
|
14 |
be trancl_induct 1;
|
|
|
15 |
by(Blast_tac 1);
|
|
|
16 |
by(blast_tac (claset() addIs [order_less_trans]) 1);
|
|
|
17 |
by(blast_tac (claset() addIs [r_into_trancl]) 1);
|
|
|
18 |
qed "trancl_order1_conv";
|
|
|
19 |
Addsimps [trancl_order1_conv];
|
|
|
20 |
|
|
|
21 |
Goalw [acyclic_def] "acyclic{(x,y::'a::order). y<x}";
|
|
|
22 |
by(Simp_tac 1);
|
|
|
23 |
qed "acyclic_order1";
|
|
|
24 |
AddIffs [acyclic_order1];
|
|
|
25 |
|
|
|
26 |
Goalw [acc_def] "acc(UNIV::typ set)";
|
|
|
27 |
br finite_acyclic_wf 1;
|
|
|
28 |
by(fast_tac (claset() addIs [finite_SigmaI RSN (2,finite_subset)]) 1);
|
|
|
29 |
by(blast_tac (claset() addIs [acyclic_subset]) 1);
|
|
|
30 |
qed "acc_UNIV_typ";
|
|
|
31 |
AddIffs [acc_UNIV_typ];
|