isabelle: Admin/Benchmarks/HOL-datatype/Brackin.thy@6f60110e317c (annotated)

7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	1	(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	2	ID: $Id$
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	3	*)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	4
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 7373 diff changeset	5	theory Brackin imports Main begin
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	6
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	7	(* ------------------------------------------------------------------------- *)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	8	(* A couple from Steve Brackin's work. *)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	9	(* ------------------------------------------------------------------------- *)
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	10
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	11	datatype T = X1 \| X2 \| X3 \| X4 \| X5 \| X6 \| X7 \| X8 \| X9 \| X10 \| X11 \|
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	12	X12 \| X13 \| X14 \| X15 \| X16 \| X17 \| X18 \| X19 \| X20 \| X21 \|
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	13	X22 \| X23 \| X24 \| X25 \| X26 \| X27 \| X28 \| X29 \| X30 \| X31 \|
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	14	X32 \| X33 \| X34
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	15
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	16	datatype
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	17	('a, 'b, 'c) TY1 =
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	18	NoF__
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	19	\| Fk__ 'a "('a, 'b, 'c) TY2"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	20	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	21	('a, 'b, 'c) TY2 =
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	22	Ta__ bool
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	23	\| Td__ bool
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	24	\| Tf__ "('a, 'b, 'c) TY1"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	25	\| Tk__ bool
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	26	\| Tp__ bool
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	27	\| App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	28	\| Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	29	and
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	30	('a, 'b, 'c) TY3 =
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	31	NoS__
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	32	\| Fresh__ "('a, 'b, 'c) TY2"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	33	\| Trustworthy__ 'a
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	34	\| PrivateKey__ 'a 'b 'c
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	35	\| PublicKey__ 'a 'b 'c
7373 776d888472aa better timing information; wenzelm parents: 7013 diff changeset	36	\| Conveyed__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	37	\| Possesses__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	38	\| Received__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	39	\| Recognizes__ 'a "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	40	\| NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	41	\| Sends__ 'a "('a, 'b, 'c) TY2" 'b
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	42	\| SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	43	\| Believes__ 'a "('a, 'b, 'c) TY3"
776d888472aa better timing information; wenzelm parents: 7013 diff changeset	44	\| And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
7013 8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	45
8a7fb425e04a Some rather large datatype examples (from John Harrison). berghofe parents: diff changeset	46	end

author	wenzelm
	Fri, 15 Aug 2008 23:10:36 +0200
changeset 27910	6f60110e317c
parent 16417	9bc16273c2d4
child 33695	bec342db1bf4
permissions	-rw-r--r--