isabelle: src/HOL/BCV/SemiLattice.thy@edaca60a54cd (annotated)

7626 5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	1	(* Title: HOL/BCV/SemiLattice.thy
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	Semilattices
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	7	*)
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	8
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	9	SemiLattice = Plus +
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	constdefs
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	12	semilat :: "('a::{order,plus} set) => bool"
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	13	"semilat A == (!x:A. !y:A. x <= x+y) &
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	14	(!x:A. !y:A. y <= x+y) &
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	15	(!x:A. !y:A. !z:A. x <= z & y <= z --> x+y <= z) &
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	16	(!x:A. !y:A. x+y : A)"
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	17
5997f35954d7 A new theory: a model of bytecode verification. nipkow parents: diff changeset	18	end

author	wenzelm
	Wed, 27 Oct 1999 18:12:40 +0200
changeset 7956	edaca60a54cd
parent 7626	5997f35954d7
permissions	-rw-r--r--