isabelle: src/HOLCF/Void.thy@51993fea433f (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	1	(* Title: HOLCF/void.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Definition of type void with partial order. Void is the prototype for
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	all types in class 'po'
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9	Type void is defined as a set Void over type bool.
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11
2445 51993fea433f removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2 oheimb parents: 1479 diff changeset	12	Void = Nat +
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14	types void 0
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16	arities void :: term
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18	consts
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	19	Void :: "bool set"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	20	UU_void_Rep :: "bool"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	21	Rep_Void :: "void => bool"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	22	Abs_Void :: "bool => void"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	23	UU_void :: "void"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	24	less_void :: "[void,void] => bool"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	26	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	28	(* The unique element in Void is False:bool *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	30	UU_void_Rep_def "UU_void_Rep == False"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	31	Void_def "Void == {x. x = UU_void_Rep}"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	33	(defining the abstract constants)
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	34
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	35	UU_void_def "UU_void == Abs_Void(UU_void_Rep)"
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	36	less_void_def "less_void x y == (Rep_Void x = Rep_Void y)"
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	37
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	38	rules
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 243 diff changeset	39
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	40	(faking a type definition... )
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41	(* void is isomorphic to Void *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	42
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	43	Rep_Void "Rep_Void(x):Void"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	44	Rep_Void_inverse "Abs_Void(Rep_Void(x)) = x"
21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	45	Abs_Void_inverse "y:Void ==> Rep_Void(Abs_Void(y)) = y"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	46
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	47	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	48
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	49
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	50
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	51

author	oheimb
	Wed, 18 Dec 1996 15:16:13 +0100
changeset 2445	51993fea433f
parent 1479	21eb5e156d91
permissions	-rw-r--r--