isabelle: src/HOL/Record_Benchmark/Record_Benchmark.thy@93eda35a8377 (annotated)

45860 93eda35a8377 more visible benchmarks; wenzelm parents: 44640 diff changeset	1	(* Title: HOL/Record_Benchmark/Record_Benchmark.thy
33695 bec342db1bf4 eliminated obsolete CVS Ids; wenzelm parents: 33693 diff changeset	2	Author: Norbert Schirmer, DFKI
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	3	*)
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	4
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	5	header {* Benchmark for large record *}
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	6
44640 3e666dcdcd32 modernized theory name; wenzelm parents: 44639 diff changeset	7	theory Record_Benchmark
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	8	imports Main
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	9	begin
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	10
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	11	declare [[record_timing]]
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	12
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	13	record many_A =
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	14	A000::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	15	A001::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	16	A002::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	17	A003::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	18	A004::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	19	A005::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	20	A006::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	21	A007::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	22	A008::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	23	A009::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	24	A010::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	25	A011::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	26	A012::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	27	A013::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	28	A014::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	29	A015::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	30	A016::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	31	A017::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	32	A018::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	33	A019::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	34	A020::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	35	A021::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	36	A022::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	37	A023::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	38	A024::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	39	A025::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	40	A026::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	41	A027::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	42	A028::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	43	A029::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	44	A030::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	45	A031::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	46	A032::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	47	A033::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	48	A034::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	49	A035::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	50	A036::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	51	A037::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	52	A038::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	53	A039::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	54	A040::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	55	A041::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	56	A042::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	57	A043::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	58	A044::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	59	A045::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	60	A046::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	61	A047::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	62	A048::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	63	A049::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	64	A050::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	65	A051::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	66	A052::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	67	A053::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	68	A054::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	69	A055::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	70	A056::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	71	A057::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	72	A058::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	73	A059::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	74	A060::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	75	A061::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	76	A062::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	77	A063::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	78	A064::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	79	A065::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	80	A066::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	81	A067::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	82	A068::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	83	A069::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	84	A070::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	85	A071::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	86	A072::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	87	A073::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	88	A074::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	89	A075::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	90	A076::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	91	A077::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	92	A078::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	93	A079::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	94	A080::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	95	A081::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	96	A082::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	97	A083::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	98	A084::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	99	A085::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	100	A086::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	101	A087::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	102	A088::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	103	A089::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	104	A090::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	105	A091::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	106	A092::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	107	A093::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	108	A094::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	109	A095::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	110	A096::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	111	A097::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	112	A098::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	113	A099::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	114	A100::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	115	A101::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	116	A102::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	117	A103::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	118	A104::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	119	A105::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	120	A106::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	121	A107::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	122	A108::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	123	A109::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	124	A110::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	125	A111::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	126	A112::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	127	A113::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	128	A114::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	129	A115::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	130	A116::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	131	A117::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	132	A118::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	133	A119::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	134	A120::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	135	A121::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	136	A122::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	137	A123::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	138	A124::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	139	A125::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	140	A126::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	141	A127::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	142	A128::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	143	A129::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	144	A130::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	145	A131::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	146	A132::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	147	A133::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	148	A134::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	149	A135::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	150	A136::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	151	A137::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	152	A138::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	153	A139::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	154	A140::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	155	A141::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	156	A142::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	157	A143::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	158	A144::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	159	A145::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	160	A146::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	161	A147::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	162	A148::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	163	A149::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	164	A150::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	165	A151::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	166	A152::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	167	A153::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	168	A154::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	169	A155::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	170	A156::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	171	A157::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	172	A158::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	173	A159::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	174	A160::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	175	A161::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	176	A162::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	177	A163::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	178	A164::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	179	A165::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	180	A166::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	181	A167::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	182	A168::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	183	A169::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	184	A170::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	185	A171::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	186	A172::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	187	A173::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	188	A174::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	189	A175::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	190	A176::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	191	A177::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	192	A178::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	193	A179::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	194	A180::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	195	A181::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	196	A182::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	197	A183::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	198	A184::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	199	A185::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	200	A186::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	201	A187::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	202	A188::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	203	A189::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	204	A190::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	205	A191::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	206	A192::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	207	A193::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	208	A194::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	209	A195::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	210	A196::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	211	A197::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	212	A198::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	213	A199::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	214	A200::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	215	A201::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	216	A202::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	217	A203::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	218	A204::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	219	A205::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	220	A206::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	221	A207::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	222	A208::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	223	A209::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	224	A210::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	225	A211::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	226	A212::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	227	A213::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	228	A214::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	229	A215::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	230	A216::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	231	A217::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	232	A218::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	233	A219::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	234	A220::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	235	A221::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	236	A222::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	237	A223::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	238	A224::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	239	A225::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	240	A226::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	241	A227::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	242	A228::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	243	A229::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	244	A230::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	245	A231::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	246	A232::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	247	A233::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	248	A234::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	249	A235::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	250	A236::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	251	A237::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	252	A238::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	253	A239::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	254	A240::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	255	A241::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	256	A242::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	257	A243::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	258	A244::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	259	A245::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	260	A246::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	261	A247::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	262	A248::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	263	A249::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	264	A250::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	265	A251::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	266	A252::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	267	A253::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	268	A254::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	269	A255::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	270	A256::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	271	A257::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	272	A258::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	273	A259::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	274	A260::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	275	A261::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	276	A262::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	277	A263::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	278	A264::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	279	A265::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	280	A266::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	281	A267::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	282	A268::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	283	A269::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	284	A270::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	285	A271::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	286	A272::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	287	A273::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	288	A274::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	289	A275::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	290	A276::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	291	A277::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	292	A278::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	293	A279::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	294	A280::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	295	A281::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	296	A282::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	297	A283::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	298	A284::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	299	A285::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	300	A286::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	301	A287::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	302	A288::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	303	A289::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	304	A290::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	305	A291::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	306	A292::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	307	A293::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	308	A294::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	309	A295::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	310	A296::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	311	A297::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	312	A298::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	313	A299::nat
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	314
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	315	lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	316	by simp
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	317
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	318	lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	319	by simp
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	320
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	321	lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	322	by simp
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	323
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	324	lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	325	apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	326	done
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	327
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	328	lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	329	apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	330	apply simp
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	331	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	332
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	333	lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	334	apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	335	apply simp
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	336	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	337
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	338	lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	339	apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	340	apply simp
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	341	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	342
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	343	lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	344	apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	345	apply simp
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	346	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	347
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	348	lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	349	apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	350	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	351	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	352
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	353	lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	354	apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	355	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	356	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	357
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	358	lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	359	apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	360	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	361	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	362
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	363	lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	364	apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	365	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	366	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	367
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	368
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	369	lemma True
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	370	proof -
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	371	{
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	372	fix P r
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	373	assume pre: "P (A155 r)"
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	374	have "\<exists>x. P x"
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	375	using pre
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	376	apply -
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	377	apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	378	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	379	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	380	}
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	381	show ?thesis ..
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	382	qed
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	383
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	384
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	385	lemma "\<exists>r. A155 r = x"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	386	apply (tactic {simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1})
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	387	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	388
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	389
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	390	end

author	wenzelm
	Wed, 14 Dec 2011 12:02:02 +0100
changeset 45860	93eda35a8377
parent 44640	Admin/Benchmarks/HOL-record/Record_Benchmark.thy@3e666dcdcd32
child 46079	65bde43e829c
permissions	-rw-r--r--