|
7626
|
1 |
(* Title: HOL/BCV/Types0.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
Goalw [le_typ] "(t::typ) <= t";
|
|
|
8 |
by(Blast_tac 1);
|
|
|
9 |
qed "le_typ_refl";
|
|
|
10 |
|
|
|
11 |
Goalw [le_typ] "[| (t1::typ) <= t2; t2<=t3 |] ==> t1<=t3";
|
|
|
12 |
by(Blast_tac 1);
|
|
|
13 |
qed "le_typ_trans";
|
|
|
14 |
|
|
|
15 |
Goalw [le_typ] "[| (t1::typ) <= t2; t2<=t1 |] ==> t1=t2";
|
|
|
16 |
by(Blast_tac 1);
|
|
|
17 |
qed "le_typ_antisym";
|
|
|
18 |
|
|
|
19 |
Goalw [less_typ] "(t1::typ) < t2 = (t1<=t2 & t1 ~= t2)";
|
|
|
20 |
br refl 1;
|
|
|
21 |
qed "less_le_typ";
|
|
|
22 |
|
|
|
23 |
Goal "(UNIV::typ set) = {Atyp,Btyp,Ctyp,Top}";
|
|
|
24 |
by(Auto_tac);
|
|
|
25 |
by(rename_tac "t" 1);
|
|
|
26 |
by(exhaust_tac "t" 1);
|
|
|
27 |
by(Auto_tac);
|
|
|
28 |
qed "UNIV_typ_enum";
|
|
|
29 |
|
|
|
30 |
Goal "finite(UNIV::typ set)";
|
|
|
31 |
by(simp_tac (simpset() addsimps [UNIV_typ_enum]) 1);
|
|
|
32 |
qed "finite_UNIV_typ";
|
|
|
33 |
AddIffs [finite_UNIV_typ];
|