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 nipkow
Tue, 28 Sep 1999 16:36:12 +0200
changeset 7626 5997f35954d7
child 7961 422ac6888c7f
permissions -rw-r--r--
A new theory: a model of bytecode verification.

(*  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)";
br 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