isabelle: src/Benchmarks/Record_Benchmark/Record_Benchmark.thy@bfabccdad18e (annotated)

62286 705d4c4003ea clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default; wenzelm parents: 62117 diff changeset	1	(* Title: Benchmarks/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
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	5	section \<open>Benchmark for large record\<close>
33693 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
46079 65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	315	record many_B = many_A +
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	316	B000::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	317	B001::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	318	B002::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	319	B003::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	320	B004::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	321	B005::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	322	B006::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	323	B007::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	324	B008::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	325	B009::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	326	B010::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	327	B011::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	328	B012::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	329	B013::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	330	B014::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	331	B015::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	332	B016::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	333	B017::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	334	B018::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	335	B019::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	336	B020::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	337	B021::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	338	B022::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	339	B023::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	340	B024::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	341	B025::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	342	B026::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	343	B027::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	344	B028::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	345	B029::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	346	B030::nat
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	347
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	348	lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	349	by simp
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	350
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	351	lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	352	by simp
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	353
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	354	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	355	by simp
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	356
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	357	lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	358	apply (tactic \<open>simp_tac
658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	359	(put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1\<close>)
44639 83dc04ccabd5 repaired benchmarks; wenzelm parents: 38798 diff changeset	360	done
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	361
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	362	lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	363	apply (tactic \<open>simp_tac
658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	364	(put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	365	apply simp
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	lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	369	apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	370	apply simp
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	371	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	372
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	373	lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	374	apply (tactic \<open>simp_tac
658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	375	(put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	376	apply simp
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	377	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	378
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	379	lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	380	apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	381	apply simp
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	382	done
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	lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	385	apply (tactic \<open>simp_tac
658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	386	(put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	387	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	388	done
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	lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	391	apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	392	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	393	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	394
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	395	lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	396	apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	397	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	398	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	399
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	400	lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	401	apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	402	apply auto
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	403	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	404
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	405
46079 65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	406	notepad
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	407	begin
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	408	fix P r
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	409	assume "P (A155 r)"
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	410	then have "\<exists>x. P x"
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	411	apply -
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	412	apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
46079 65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	413	apply auto
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	414	done
65bde43e829c more benchmarks; wenzelm parents: 45860 diff changeset	415	end
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	416
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	417
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	418	lemma "\<exists>r. A155 r = x"
62290 658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	419	apply (tactic \<open>simp_tac
658276428cfc isabelle update_cartouches -c -t; wenzelm parents: 62286 diff changeset	420	(put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	421	done
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	422
62117 86a31308a8e1 print_record: diagnostic printing of record definitions kleing parents: 58889 diff changeset	423	print_record many_A
86a31308a8e1 print_record: diagnostic printing of record definitions kleing parents: 58889 diff changeset	424
86a31308a8e1 print_record: diagnostic printing of record definitions kleing parents: 58889 diff changeset	425	print_record many_B
33693 9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	426
9d76c8080aea added benchmark for large records schirmer <schirmer@in.tum.de> parents: diff changeset	427	end

author	wenzelm
	Fri, 01 Sep 2017 12:52:46 +0200
changeset 66587	bfabccdad18e
parent 62290	658276428cfc
child 67399	eab6ce8368fa
permissions	-rw-r--r--