Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BCV/Types0.ML
author paulson
Thu, 11 Nov 1999 10:25:17 +0100
changeset 8005 b64d86018785
parent 7961 422ac6888c7f
child 8423 3c19160b6432
permissions -rw-r--r--
new-style infix declaration for "image"

(*  Title:      HOL/BCV/Types0.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1999 TUM
*)

Goalw [le_typ] "(t::typ) <= t";
by (Blast_tac 1);
qed "le_typ_refl";

Goalw [le_typ] "[| (t1::typ) <= t2; t2<=t3 |] ==> t1<=t3";
by (Blast_tac 1);
qed "le_typ_trans";

Goalw [le_typ] "[| (t1::typ) <= t2; t2<=t1 |] ==> t1=t2";
by (Blast_tac 1);
qed "le_typ_antisym";

Goalw [less_typ] "(t1::typ) < t2 = (t1<=t2 & t1 ~= t2)";
by (rtac refl 1);
qed "less_le_typ";

Goal "(UNIV::typ set) = {Atyp,Btyp,Ctyp,Top}";
by (Auto_tac);
by (rename_tac "t" 1);
by (exhaust_tac "t" 1);
by (Auto_tac);
qed "UNIV_typ_enum";

Goal "finite(UNIV::typ set)";
by (simp_tac (simpset() addsimps [UNIV_typ_enum]) 1);
qed "finite_UNIV_typ";
AddIffs [finite_UNIV_typ];
isabelle