src/HOL/Record_Benchmark/Record_Benchmark.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46079 65bde43e829c
child 51717 9e7d1c139569
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
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>"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   358
  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   359
  done
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   360
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   361
lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   362
  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
   363
  apply simp
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   364
  done
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   365
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   366
lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   367
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   368
  apply simp
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   369
  done
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   370
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   371
lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   372
  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
   373
  apply simp
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   374
  done
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   375
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   376
lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
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 simp
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
lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   382
  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
   383
  apply auto
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   384
  done
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   385
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   386
lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   387
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   388
  apply auto
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   389
  done
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   390
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   391
lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   392
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   393
  apply auto
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   394
  done
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   395
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   396
lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   397
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   398
  apply auto
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   399
  done
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   400
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   401
46079
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   402
notepad
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   403
begin
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   404
  fix P r
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   405
  assume "P (A155 r)"
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   406
  then have "\<exists>x. P x"
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   407
    apply -
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   408
    apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   409
    apply auto 
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   410
    done
65bde43e829c more benchmarks;
wenzelm
parents: 45860
diff changeset
   411
end
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   412
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   413
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   414
lemma "\<exists>r. A155 r = x"
44639
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
   415
  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
   416
  done
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
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
   419
end