isabelle: src/HOL/BCV/Types0.ML@f9679ddbc492 (annotated)

7626 5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	1	(* Title: HOL/BCV/Types0.ML
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	2	ID: $Id$
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	3	Author: Tobias Nipkow
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	4	Copyright 1999 TUM
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	5	*)
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	6
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	7	Goalw [le_typ] "(t::typ) <= t";
7961 422ac6888c7f expandshort paulson parents: 7626 diff changeset	8	by (Blast_tac 1);
7626 5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	9	qed "le_typ_refl";
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	10
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	11	Goalw [le_typ] "[\| (t1::typ) <= t2; t2<=t3 \|] ==> t1<=t3";
7961 422ac6888c7f expandshort paulson parents: 7626 diff changeset	12	by (Blast_tac 1);
7626 5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	13	qed "le_typ_trans";
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	14
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	15	Goalw [le_typ] "[\| (t1::typ) <= t2; t2<=t1 \|] ==> t1=t2";
7961 422ac6888c7f expandshort paulson parents: 7626 diff changeset	16	by (Blast_tac 1);
7626 5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	17	qed "le_typ_antisym";
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	18
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	19	Goalw [less_typ] "(t1::typ) < t2 = (t1<=t2 & t1 ~= t2)";
7961 422ac6888c7f expandshort paulson parents: 7626 diff changeset	20	by (rtac refl 1);
7626 5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	21	qed "less_le_typ";
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	22
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	23	Goal "(UNIV::typ set) = {Atyp,Btyp,Ctyp,Top}";
7961 422ac6888c7f expandshort paulson parents: 7626 diff changeset	24	by (Auto_tac);
422ac6888c7f expandshort paulson parents: 7626 diff changeset	25	by (rename_tac "t" 1);
8442 96023903c2df case_tac now subsumes both boolean and datatype cases; wenzelm parents: 8423 diff changeset	26	by (case_tac "t" 1);
7961 422ac6888c7f expandshort paulson parents: 7626 diff changeset	27	by (Auto_tac);
7626 5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	28	qed "UNIV_typ_enum";
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	29
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	30	Goal "finite(UNIV::typ set)";
7961 422ac6888c7f expandshort paulson parents: 7626 diff changeset	31	by (simp_tac (simpset() addsimps [UNIV_typ_enum]) 1);
7626 5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	32	qed "finite_UNIV_typ";
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	33	AddIffs [finite_UNIV_typ];

author	wenzelm
	Mon, 03 Apr 2000 14:02:40 +0200
changeset 8662	f9679ddbc492
parent 8442	96023903c2df
permissions	-rw-r--r--