more visible benchmarks;
authorwenzelm
Wed Dec 14 12:02:02 2011 +0100 (2011-12-14)
changeset 4586093eda35a8377
parent 45859 36ff12b5663b
child 45861 4bb0fc92247b
more visible benchmarks;
uniform IsaMakefile target "full" to cover such extra sessions;
Admin/Benchmarks/HOL-datatype/Brackin.thy
Admin/Benchmarks/HOL-datatype/Instructions.thy
Admin/Benchmarks/HOL-datatype/ROOT.ML
Admin/Benchmarks/HOL-datatype/SML.thy
Admin/Benchmarks/HOL-datatype/Verilog.thy
Admin/Benchmarks/HOL-record/ROOT.ML
Admin/Benchmarks/HOL-record/Record_Benchmark.thy
Admin/Benchmarks/IsaMakefile
src/CCL/IsaMakefile
src/CTT/IsaMakefile
src/Cube/IsaMakefile
src/FOL/IsaMakefile
src/FOLP/IsaMakefile
src/HOL/Datatype_Benchmark/Brackin.thy
src/HOL/Datatype_Benchmark/Instructions.thy
src/HOL/Datatype_Benchmark/ROOT.ML
src/HOL/Datatype_Benchmark/SML.thy
src/HOL/Datatype_Benchmark/Verilog.thy
src/HOL/HOLCF/IsaMakefile
src/HOL/IsaMakefile
src/HOL/Record_Benchmark/ROOT.ML
src/HOL/Record_Benchmark/Record_Benchmark.thy
src/LCF/IsaMakefile
src/Pure/IsaMakefile
src/Sequents/IsaMakefile
src/Tools/WWW_Find/IsaMakefile
src/ZF/IsaMakefile
     1.1 --- a/Admin/Benchmarks/HOL-datatype/Brackin.thy	Wed Dec 14 10:18:28 2011 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,43 +0,0 @@
     1.4 -(*  Title:      Admin/Benchmarks/HOL-datatype/Brackin.thy
     1.5 -
     1.6 -A couple from Steve Brackin's work.
     1.7 -*)
     1.8 -
     1.9 -theory Brackin imports Main begin
    1.10 -
    1.11 -datatype   T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
    1.12 -                X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
    1.13 -                X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
    1.14 -                X32 | X33 | X34
    1.15 -
    1.16 -datatype  
    1.17 -  ('a, 'b, 'c) TY1 =
    1.18 -      NoF__
    1.19 -    | Fk__ 'a "('a, 'b, 'c) TY2"
    1.20 -and
    1.21 -  ('a, 'b, 'c) TY2 =
    1.22 -      Ta__ bool
    1.23 -    | Td__ bool
    1.24 -    | Tf__ "('a, 'b, 'c) TY1"
    1.25 -    | Tk__ bool
    1.26 -    | Tp__ bool
    1.27 -    | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
    1.28 -    | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
    1.29 -and
    1.30 -  ('a, 'b, 'c) TY3 =
    1.31 -      NoS__
    1.32 -    | Fresh__ "('a, 'b, 'c) TY2"
    1.33 -    | Trustworthy__ 'a
    1.34 -    | PrivateKey__ 'a 'b 'c
    1.35 -    | PublicKey__ 'a 'b 'c
    1.36 -    | Conveyed__ 'a "('a, 'b, 'c) TY2"
    1.37 -    | Possesses__ 'a "('a, 'b, 'c) TY2"
    1.38 -    | Received__ 'a "('a, 'b, 'c) TY2"
    1.39 -    | Recognizes__ 'a "('a, 'b, 'c) TY2"
    1.40 -    | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
    1.41 -    | Sends__ 'a "('a, 'b, 'c) TY2" 'b
    1.42 -    | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
    1.43 -    | Believes__ 'a "('a, 'b, 'c) TY3"
    1.44 -    | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
    1.45 -
    1.46 -end
     2.1 --- a/Admin/Benchmarks/HOL-datatype/Instructions.thy	Wed Dec 14 10:18:28 2011 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,162 +0,0 @@
     2.4 -(*  Title:      Admin/Benchmarks/HOL-datatype/Instructions.thy
     2.5 -
     2.6 -Example from Konrad: 68000 instruction set.
     2.7 -*)
     2.8 -
     2.9 -theory Instructions imports Main begin
    2.10 -
    2.11 -datatype Size = Byte | Word | Long
    2.12 -
    2.13 -datatype DataRegister
    2.14 -              = RegD0
    2.15 -              | RegD1
    2.16 -              | RegD2
    2.17 -              | RegD3
    2.18 -              | RegD4
    2.19 -              | RegD5
    2.20 -              | RegD6
    2.21 -              | RegD7
    2.22 -
    2.23 -datatype AddressRegister
    2.24 -              = RegA0
    2.25 -              | RegA1
    2.26 -              | RegA2
    2.27 -              | RegA3
    2.28 -              | RegA4
    2.29 -              | RegA5
    2.30 -              | RegA6
    2.31 -              | RegA7
    2.32 -
    2.33 -datatype DataOrAddressRegister
    2.34 -              = data DataRegister
    2.35 -              | address AddressRegister
    2.36 -
    2.37 -datatype Condition
    2.38 -              = Hi
    2.39 -              | Ls
    2.40 -              | Cc
    2.41 -              | Cs
    2.42 -              | Ne
    2.43 -              | Eq
    2.44 -              | Vc
    2.45 -              | Vs
    2.46 -              | Pl
    2.47 -              | Mi
    2.48 -              | Ge
    2.49 -              | Lt
    2.50 -              | Gt
    2.51 -              | Le
    2.52 -
    2.53 -datatype AddressingMode
    2.54 -        = immediate nat
    2.55 -        | direct DataOrAddressRegister
    2.56 -        | indirect AddressRegister
    2.57 -        | postinc AddressRegister
    2.58 -        | predec AddressRegister
    2.59 -        | indirectdisp nat AddressRegister
    2.60 -        | indirectindex nat AddressRegister DataOrAddressRegister Size
    2.61 -        | absolute nat
    2.62 -        | pcdisp nat
    2.63 -        | pcindex nat DataOrAddressRegister Size
    2.64 -
    2.65 -datatype M68kInstruction
    2.66 -    = ABCD AddressingMode AddressingMode
    2.67 -    | ADD Size AddressingMode AddressingMode
    2.68 -    | ADDA Size AddressingMode AddressRegister
    2.69 -    | ADDI Size nat AddressingMode
    2.70 -    | ADDQ Size nat AddressingMode
    2.71 -    | ADDX Size AddressingMode AddressingMode
    2.72 -    | AND Size AddressingMode AddressingMode
    2.73 -    | ANDI Size nat AddressingMode
    2.74 -    | ANDItoCCR nat
    2.75 -    | ANDItoSR nat
    2.76 -    | ASL Size AddressingMode DataRegister
    2.77 -    | ASLW AddressingMode
    2.78 -    | ASR Size AddressingMode DataRegister
    2.79 -    | ASRW AddressingMode
    2.80 -    | Bcc Condition Size nat
    2.81 -    | BTST Size AddressingMode AddressingMode
    2.82 -    | BCHG Size AddressingMode AddressingMode
    2.83 -    | BCLR Size AddressingMode AddressingMode
    2.84 -    | BSET Size AddressingMode AddressingMode
    2.85 -    | BRA Size nat
    2.86 -    | BSR Size nat
    2.87 -    | CHK AddressingMode DataRegister
    2.88 -    | CLR Size AddressingMode
    2.89 -    | CMP Size AddressingMode DataRegister
    2.90 -    | CMPA Size AddressingMode AddressRegister
    2.91 -    | CMPI Size nat AddressingMode
    2.92 -    | CMPM Size AddressRegister AddressRegister
    2.93 -    | DBT DataRegister nat
    2.94 -    | DBF DataRegister nat
    2.95 -    | DBcc Condition DataRegister nat
    2.96 -    | DIVS AddressingMode DataRegister
    2.97 -    | DIVU AddressingMode DataRegister
    2.98 -    | EOR Size DataRegister AddressingMode
    2.99 -    | EORI Size nat AddressingMode
   2.100 -    | EORItoCCR nat
   2.101 -    | EORItoSR nat
   2.102 -    | EXG DataOrAddressRegister DataOrAddressRegister
   2.103 -    | EXT Size DataRegister
   2.104 -    | ILLEGAL
   2.105 -    | JMP AddressingMode
   2.106 -    | JSR AddressingMode
   2.107 -    | LEA AddressingMode AddressRegister
   2.108 -    | LINK AddressRegister nat
   2.109 -    | LSL Size AddressingMode DataRegister
   2.110 -    | LSLW AddressingMode
   2.111 -    | LSR Size AddressingMode DataRegister
   2.112 -    | LSRW AddressingMode
   2.113 -    | MOVE Size AddressingMode AddressingMode
   2.114 -    | MOVEtoCCR AddressingMode
   2.115 -    | MOVEtoSR AddressingMode
   2.116 -    | MOVEfromSR AddressingMode
   2.117 -    | MOVEtoUSP AddressingMode
   2.118 -    | MOVEfromUSP AddressingMode
   2.119 -    | MOVEA Size AddressingMode AddressRegister
   2.120 -    | MOVEMto Size AddressingMode "DataOrAddressRegister list"
   2.121 -    | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
   2.122 -    | MOVEP Size AddressingMode AddressingMode
   2.123 -    | MOVEQ nat DataRegister
   2.124 -    | MULS AddressingMode DataRegister
   2.125 -    | MULU AddressingMode DataRegister
   2.126 -    | NBCD AddressingMode
   2.127 -    | NEG Size AddressingMode
   2.128 -    | NEGX Size AddressingMode
   2.129 -    | NOP
   2.130 -    | NOT Size AddressingMode
   2.131 -    | OR Size AddressingMode AddressingMode
   2.132 -    | ORI Size nat AddressingMode
   2.133 -    | ORItoCCR nat
   2.134 -    | ORItoSR nat
   2.135 -    | PEA AddressingMode
   2.136 -    | RESET
   2.137 -    | ROL Size AddressingMode DataRegister
   2.138 -    | ROLW AddressingMode
   2.139 -    | ROR Size AddressingMode DataRegister
   2.140 -    | RORW AddressingMode
   2.141 -    | ROXL Size AddressingMode DataRegister
   2.142 -    | ROXLW AddressingMode
   2.143 -    | ROXR Size AddressingMode DataRegister
   2.144 -    | ROXRW AddressingMode
   2.145 -    | RTE
   2.146 -    | RTR
   2.147 -    | RTS
   2.148 -    | SBCD AddressingMode AddressingMode
   2.149 -    | ST AddressingMode
   2.150 -    | SF AddressingMode
   2.151 -    | Scc Condition AddressingMode
   2.152 -    | STOP nat
   2.153 -    | SUB Size AddressingMode AddressingMode
   2.154 -    | SUBA Size AddressingMode AddressingMode
   2.155 -    | SUBI Size nat AddressingMode
   2.156 -    | SUBQ Size nat AddressingMode
   2.157 -    | SUBX Size AddressingMode AddressingMode
   2.158 -    | SWAP DataRegister
   2.159 -    | TAS AddressingMode
   2.160 -    | TRAP nat
   2.161 -    | TRAPV
   2.162 -    | TST Size AddressingMode
   2.163 -    | UNLK AddressRegister
   2.164 -
   2.165 -end
     3.1 --- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Wed Dec 14 10:18:28 2011 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,15 +0,0 @@
     3.4 -(*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
     3.5 -
     3.6 -Some rather large datatype examples (from John Harrison).
     3.7 -*)
     3.8 -
     3.9 -val tests = ["Brackin", "Instructions", "SML", "Verilog"];
    3.10 -
    3.11 -Toplevel.timing := true;
    3.12 -
    3.13 -warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
    3.14 -use_thys tests;
    3.15 -
    3.16 -warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
    3.17 -List.app Thy_Info.remove_thy tests;
    3.18 -use_thys tests;
     4.1 --- a/Admin/Benchmarks/HOL-datatype/SML.thy	Wed Dec 14 10:18:28 2011 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,91 +0,0 @@
     4.4 -(*  Title:      Admin/Benchmarks/HOL-datatype/SML.thy
     4.5 -
     4.6 -Example from Myra: part of the syntax of SML.
     4.7 -*)
     4.8 -
     4.9 -theory SML imports Main begin
    4.10 -
    4.11 -datatype
    4.12 -  string = EMPTY_STRING | CONS_STRING nat string
    4.13 -
    4.14 -datatype
    4.15 -   strid = STRID string
    4.16 -
    4.17 -datatype
    4.18 -   var = VAR string
    4.19 -
    4.20 -datatype
    4.21 -   con = CON string
    4.22 -
    4.23 -datatype
    4.24 -   scon = SCINT nat | SCSTR string
    4.25 -
    4.26 -datatype
    4.27 -   excon = EXCON string
    4.28 -
    4.29 -datatype
    4.30 -   label = LABEL string
    4.31 -
    4.32 -datatype
    4.33 -  'a nonemptylist = Head_and_tail 'a "'a list"
    4.34 -
    4.35 -datatype
    4.36 -  'a long = BASE 'a | QUALIFIED strid "'a long"
    4.37 -
    4.38 -datatype
    4.39 -   atpat_e = WILDCARDatpat_e
    4.40 -           | SCONatpat_e scon
    4.41 -           | VARatpat_e var
    4.42 -           | CONatpat_e "con long"
    4.43 -           | EXCONatpat_e "excon long"
    4.44 -           | RECORDatpat_e "patrow_e option"
    4.45 -           | PARatpat_e pat_e
    4.46 -and
    4.47 -   patrow_e = DOTDOTDOT_e
    4.48 -            | PATROW_e label pat_e "patrow_e option"
    4.49 -and
    4.50 -   pat_e = ATPATpat_e atpat_e
    4.51 -         | CONpat_e "con long" atpat_e
    4.52 -         | EXCONpat_e "excon long" atpat_e
    4.53 -         | LAYEREDpat_e var pat_e
    4.54 -and
    4.55 -   conbind_e = CONBIND_e con "conbind_e option"
    4.56 -and
    4.57 -   datbind_e = DATBIND_e conbind_e "datbind_e option"
    4.58 -and
    4.59 -   exbind_e = EXBIND1_e excon "exbind_e option"
    4.60 -            | EXBIND2_e excon "excon long" "exbind_e option"
    4.61 -and
    4.62 -   atexp_e = SCONatexp_e scon
    4.63 -           | VARatexp_e "var long"
    4.64 -           | CONatexp_e "con long"
    4.65 -           | EXCONatexp_e "excon long"
    4.66 -           | RECORDatexp_e "exprow_e option"
    4.67 -           | LETatexp_e dec_e exp_e
    4.68 -           | PARatexp_e exp_e
    4.69 -and
    4.70 -   exprow_e = EXPROW_e label exp_e "exprow_e option"
    4.71 -and
    4.72 -   exp_e = ATEXPexp_e atexp_e
    4.73 -         | APPexp_e exp_e atexp_e
    4.74 -         | HANDLEexp_e exp_e match_e
    4.75 -         | RAISEexp_e exp_e
    4.76 -         | FNexp_e match_e
    4.77 -and
    4.78 -   match_e = MATCH_e mrule_e "match_e option"
    4.79 -and
    4.80 -   mrule_e = MRULE_e pat_e exp_e
    4.81 -and
    4.82 -   dec_e = VALdec_e valbind_e
    4.83 -         | DATATYPEdec_e datbind_e
    4.84 -         | ABSTYPEdec_e datbind_e dec_e
    4.85 -         | EXCEPTdec_e exbind_e
    4.86 -         | LOCALdec_e dec_e dec_e
    4.87 -         | OPENdec_e "strid long nonemptylist"
    4.88 -         | EMPTYdec_e
    4.89 -         | SEQdec_e dec_e dec_e
    4.90 -and
    4.91 -   valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
    4.92 -             | RECvalbind_e valbind_e
    4.93 -
    4.94 -end
     5.1 --- a/Admin/Benchmarks/HOL-datatype/Verilog.thy	Wed Dec 14 10:18:28 2011 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,138 +0,0 @@
     5.4 -(*  Title:      Admin/Benchmarks/HOL-datatype/Verilog.thy
     5.5 -
     5.6 -Example from Daryl: a Verilog grammar.
     5.7 -*)
     5.8 -
     5.9 -theory Verilog imports Main begin
    5.10 -
    5.11 -datatype
    5.12 -  Source_text
    5.13 -     = module string "string list" "Module_item list"
    5.14 -     | Source_textMeta string
    5.15 -and
    5.16 -  Module_item
    5.17 -     = "declaration" Declaration
    5.18 -     | initial Statement
    5.19 -     | always Statement
    5.20 -     | assign Lvalue Expression
    5.21 -     | Module_itemMeta string
    5.22 -and
    5.23 -  Declaration
    5.24 -     = reg_declaration "Range option" "string list"
    5.25 -     | net_declaration "Range option" "string list"
    5.26 -     | input_declaration "Range option" "string list"
    5.27 -     | output_declaration "Range option" "string list"
    5.28 -     | DeclarationMeta string
    5.29 -and
    5.30 -  Range = range Expression Expression | RangeMeta string
    5.31 -and
    5.32 -  Statement
    5.33 -     = clock_statement Clock Statement_or_null
    5.34 -     | blocking_assignment Lvalue Expression
    5.35 -     | non_blocking_assignment Lvalue Expression
    5.36 -     | conditional_statement
    5.37 -          Expression Statement_or_null "Statement_or_null option"
    5.38 -     | case_statement Expression "Case_item list"
    5.39 -     | while_loop Expression Statement
    5.40 -     | repeat_loop Expression Statement
    5.41 -     | for_loop
    5.42 -          Lvalue Expression Expression Lvalue Expression Statement
    5.43 -     | forever_loop Statement
    5.44 -     | disable string
    5.45 -     | seq_block "string option" "Statement list"
    5.46 -     | StatementMeta string
    5.47 -and
    5.48 -  Statement_or_null
    5.49 -     = statement Statement | null_statement | Statement_or_nullMeta string
    5.50 -and
    5.51 -  Clock
    5.52 -     = posedge string
    5.53 -     | negedge string
    5.54 -     | clock string
    5.55 -     | ClockMeta string
    5.56 -and
    5.57 -  Case_item
    5.58 -     = case_item "Expression list" Statement_or_null
    5.59 -     | default_case_item Statement_or_null
    5.60 -     | Case_itemMeta string
    5.61 -and
    5.62 -  Expression
    5.63 -     = plus Expression Expression
    5.64 -     | minus Expression Expression
    5.65 -     | lshift Expression Expression
    5.66 -     | rshift Expression Expression
    5.67 -     | lt Expression Expression
    5.68 -     | leq Expression Expression
    5.69 -     | gt Expression Expression
    5.70 -     | geq Expression Expression
    5.71 -     | logeq Expression Expression
    5.72 -     | logneq Expression Expression
    5.73 -     | caseeq Expression Expression
    5.74 -     | caseneq Expression Expression
    5.75 -     | bitand Expression Expression
    5.76 -     | bitxor Expression Expression
    5.77 -     | bitor Expression Expression
    5.78 -     | logand Expression Expression
    5.79 -     | logor Expression Expression
    5.80 -     | conditional Expression Expression Expression
    5.81 -     | positive Primary
    5.82 -     | negative Primary
    5.83 -     | lognot Primary
    5.84 -     | bitnot Primary
    5.85 -     | reducand Primary
    5.86 -     | reducxor Primary
    5.87 -     | reducor Primary
    5.88 -     | reducnand Primary
    5.89 -     | reducxnor Primary
    5.90 -     | reducnor Primary
    5.91 -     | primary Primary
    5.92 -     | ExpressionMeta string
    5.93 -and
    5.94 -  Primary
    5.95 -     = primary_number Number
    5.96 -     | primary_IDENTIFIER string
    5.97 -     | primary_bit_select string Expression
    5.98 -     | primary_part_select string Expression Expression
    5.99 -     | primary_gen_bit_select Expression Expression
   5.100 -     | primary_gen_part_select Expression Expression Expression
   5.101 -     | primary_concatenation Concatenation
   5.102 -     | primary_multiple_concatenation Multiple_concatenation
   5.103 -     | brackets Expression
   5.104 -     | PrimaryMeta string
   5.105 -and
   5.106 -  Lvalue
   5.107 -     = lvalue string
   5.108 -     | lvalue_bit_select string Expression
   5.109 -     | lvalue_part_select string Expression Expression
   5.110 -     | lvalue_concatenation Concatenation
   5.111 -     | LvalueMeta string
   5.112 -and
   5.113 -  Number
   5.114 -     = decimal string
   5.115 -     | based "string option" string
   5.116 -     | NumberMeta string
   5.117 -and
   5.118 -  Concatenation
   5.119 -     = concatenation "Expression list" | ConcatenationMeta string
   5.120 -and
   5.121 -  Multiple_concatenation
   5.122 -     = multiple_concatenation Expression "Expression list"
   5.123 -     | Multiple_concatenationMeta string
   5.124 -and
   5.125 -  meta
   5.126 -     = Meta_Source_text Source_text
   5.127 -     | Meta_Module_item Module_item
   5.128 -     | Meta_Declaration Declaration
   5.129 -     | Meta_Range Range
   5.130 -     | Meta_Statement Statement
   5.131 -     | Meta_Statement_or_null Statement_or_null
   5.132 -     | Meta_Clock Clock
   5.133 -     | Meta_Case_item Case_item
   5.134 -     | Meta_Expression Expression
   5.135 -     | Meta_Primary Primary
   5.136 -     | Meta_Lvalue Lvalue
   5.137 -     | Meta_Number Number
   5.138 -     | Meta_Concatenation Concatenation
   5.139 -     | Meta_Multiple_concatenation Multiple_concatenation
   5.140 -
   5.141 -end
     6.1 --- a/Admin/Benchmarks/HOL-record/ROOT.ML	Wed Dec 14 10:18:28 2011 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,14 +0,0 @@
     6.4 -(*  Title:      Admin/Benchmarks/HOL-record/ROOT.ML
     6.5 -
     6.6 -Some benchmark on large record.
     6.7 -*)
     6.8 -
     6.9 -val tests = ["Record_Benchmark"];
    6.10 -
    6.11 -Toplevel.timing := true;
    6.12 -
    6.13 -warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
    6.14 -use_thys tests;
    6.15 -
    6.16 -warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
    6.17 -use_thys tests;
     7.1 --- a/Admin/Benchmarks/HOL-record/Record_Benchmark.thy	Wed Dec 14 10:18:28 2011 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,390 +0,0 @@
     7.4 -(*  Title:      Admin/Benchmarks/HOL-record/Record_Benchmark.thy
     7.5 -    Author:     Norbert Schirmer, DFKI
     7.6 -*)
     7.7 -
     7.8 -header {* Benchmark for large record *}
     7.9 -
    7.10 -theory Record_Benchmark
    7.11 -imports Main
    7.12 -begin
    7.13 -
    7.14 -declare [[record_timing]]
    7.15 -
    7.16 -record many_A =
    7.17 -A000::nat
    7.18 -A001::nat
    7.19 -A002::nat
    7.20 -A003::nat
    7.21 -A004::nat
    7.22 -A005::nat
    7.23 -A006::nat
    7.24 -A007::nat
    7.25 -A008::nat
    7.26 -A009::nat
    7.27 -A010::nat
    7.28 -A011::nat
    7.29 -A012::nat
    7.30 -A013::nat
    7.31 -A014::nat
    7.32 -A015::nat
    7.33 -A016::nat
    7.34 -A017::nat
    7.35 -A018::nat
    7.36 -A019::nat
    7.37 -A020::nat
    7.38 -A021::nat
    7.39 -A022::nat
    7.40 -A023::nat
    7.41 -A024::nat
    7.42 -A025::nat
    7.43 -A026::nat
    7.44 -A027::nat
    7.45 -A028::nat
    7.46 -A029::nat
    7.47 -A030::nat
    7.48 -A031::nat
    7.49 -A032::nat
    7.50 -A033::nat
    7.51 -A034::nat
    7.52 -A035::nat
    7.53 -A036::nat
    7.54 -A037::nat
    7.55 -A038::nat
    7.56 -A039::nat
    7.57 -A040::nat
    7.58 -A041::nat
    7.59 -A042::nat
    7.60 -A043::nat
    7.61 -A044::nat
    7.62 -A045::nat
    7.63 -A046::nat
    7.64 -A047::nat
    7.65 -A048::nat
    7.66 -A049::nat
    7.67 -A050::nat
    7.68 -A051::nat
    7.69 -A052::nat
    7.70 -A053::nat
    7.71 -A054::nat
    7.72 -A055::nat
    7.73 -A056::nat
    7.74 -A057::nat
    7.75 -A058::nat
    7.76 -A059::nat
    7.77 -A060::nat
    7.78 -A061::nat
    7.79 -A062::nat
    7.80 -A063::nat
    7.81 -A064::nat
    7.82 -A065::nat
    7.83 -A066::nat
    7.84 -A067::nat
    7.85 -A068::nat
    7.86 -A069::nat
    7.87 -A070::nat
    7.88 -A071::nat
    7.89 -A072::nat
    7.90 -A073::nat
    7.91 -A074::nat
    7.92 -A075::nat
    7.93 -A076::nat
    7.94 -A077::nat
    7.95 -A078::nat
    7.96 -A079::nat
    7.97 -A080::nat
    7.98 -A081::nat
    7.99 -A082::nat
   7.100 -A083::nat
   7.101 -A084::nat
   7.102 -A085::nat
   7.103 -A086::nat
   7.104 -A087::nat
   7.105 -A088::nat
   7.106 -A089::nat
   7.107 -A090::nat
   7.108 -A091::nat
   7.109 -A092::nat
   7.110 -A093::nat
   7.111 -A094::nat
   7.112 -A095::nat
   7.113 -A096::nat
   7.114 -A097::nat
   7.115 -A098::nat
   7.116 -A099::nat
   7.117 -A100::nat
   7.118 -A101::nat
   7.119 -A102::nat
   7.120 -A103::nat
   7.121 -A104::nat
   7.122 -A105::nat
   7.123 -A106::nat
   7.124 -A107::nat
   7.125 -A108::nat
   7.126 -A109::nat
   7.127 -A110::nat
   7.128 -A111::nat
   7.129 -A112::nat
   7.130 -A113::nat
   7.131 -A114::nat
   7.132 -A115::nat
   7.133 -A116::nat
   7.134 -A117::nat
   7.135 -A118::nat
   7.136 -A119::nat
   7.137 -A120::nat
   7.138 -A121::nat
   7.139 -A122::nat
   7.140 -A123::nat
   7.141 -A124::nat
   7.142 -A125::nat
   7.143 -A126::nat
   7.144 -A127::nat
   7.145 -A128::nat
   7.146 -A129::nat
   7.147 -A130::nat
   7.148 -A131::nat
   7.149 -A132::nat
   7.150 -A133::nat
   7.151 -A134::nat
   7.152 -A135::nat
   7.153 -A136::nat
   7.154 -A137::nat
   7.155 -A138::nat
   7.156 -A139::nat
   7.157 -A140::nat
   7.158 -A141::nat
   7.159 -A142::nat
   7.160 -A143::nat
   7.161 -A144::nat
   7.162 -A145::nat
   7.163 -A146::nat
   7.164 -A147::nat
   7.165 -A148::nat
   7.166 -A149::nat
   7.167 -A150::nat
   7.168 -A151::nat
   7.169 -A152::nat
   7.170 -A153::nat
   7.171 -A154::nat
   7.172 -A155::nat
   7.173 -A156::nat
   7.174 -A157::nat
   7.175 -A158::nat
   7.176 -A159::nat
   7.177 -A160::nat
   7.178 -A161::nat
   7.179 -A162::nat
   7.180 -A163::nat
   7.181 -A164::nat
   7.182 -A165::nat
   7.183 -A166::nat
   7.184 -A167::nat
   7.185 -A168::nat
   7.186 -A169::nat
   7.187 -A170::nat
   7.188 -A171::nat
   7.189 -A172::nat
   7.190 -A173::nat
   7.191 -A174::nat
   7.192 -A175::nat
   7.193 -A176::nat
   7.194 -A177::nat
   7.195 -A178::nat
   7.196 -A179::nat
   7.197 -A180::nat
   7.198 -A181::nat
   7.199 -A182::nat
   7.200 -A183::nat
   7.201 -A184::nat
   7.202 -A185::nat
   7.203 -A186::nat
   7.204 -A187::nat
   7.205 -A188::nat
   7.206 -A189::nat
   7.207 -A190::nat
   7.208 -A191::nat
   7.209 -A192::nat
   7.210 -A193::nat
   7.211 -A194::nat
   7.212 -A195::nat
   7.213 -A196::nat
   7.214 -A197::nat
   7.215 -A198::nat
   7.216 -A199::nat
   7.217 -A200::nat
   7.218 -A201::nat
   7.219 -A202::nat
   7.220 -A203::nat
   7.221 -A204::nat
   7.222 -A205::nat
   7.223 -A206::nat
   7.224 -A207::nat
   7.225 -A208::nat
   7.226 -A209::nat
   7.227 -A210::nat
   7.228 -A211::nat
   7.229 -A212::nat
   7.230 -A213::nat
   7.231 -A214::nat
   7.232 -A215::nat
   7.233 -A216::nat
   7.234 -A217::nat
   7.235 -A218::nat
   7.236 -A219::nat
   7.237 -A220::nat
   7.238 -A221::nat
   7.239 -A222::nat
   7.240 -A223::nat
   7.241 -A224::nat
   7.242 -A225::nat
   7.243 -A226::nat
   7.244 -A227::nat
   7.245 -A228::nat
   7.246 -A229::nat
   7.247 -A230::nat
   7.248 -A231::nat
   7.249 -A232::nat
   7.250 -A233::nat
   7.251 -A234::nat
   7.252 -A235::nat
   7.253 -A236::nat
   7.254 -A237::nat
   7.255 -A238::nat
   7.256 -A239::nat
   7.257 -A240::nat
   7.258 -A241::nat
   7.259 -A242::nat
   7.260 -A243::nat
   7.261 -A244::nat
   7.262 -A245::nat
   7.263 -A246::nat
   7.264 -A247::nat
   7.265 -A248::nat
   7.266 -A249::nat
   7.267 -A250::nat
   7.268 -A251::nat
   7.269 -A252::nat
   7.270 -A253::nat
   7.271 -A254::nat
   7.272 -A255::nat
   7.273 -A256::nat
   7.274 -A257::nat
   7.275 -A258::nat
   7.276 -A259::nat
   7.277 -A260::nat
   7.278 -A261::nat
   7.279 -A262::nat
   7.280 -A263::nat
   7.281 -A264::nat
   7.282 -A265::nat
   7.283 -A266::nat
   7.284 -A267::nat
   7.285 -A268::nat
   7.286 -A269::nat
   7.287 -A270::nat
   7.288 -A271::nat
   7.289 -A272::nat
   7.290 -A273::nat
   7.291 -A274::nat
   7.292 -A275::nat
   7.293 -A276::nat
   7.294 -A277::nat
   7.295 -A278::nat
   7.296 -A279::nat
   7.297 -A280::nat
   7.298 -A281::nat
   7.299 -A282::nat
   7.300 -A283::nat
   7.301 -A284::nat
   7.302 -A285::nat
   7.303 -A286::nat
   7.304 -A287::nat
   7.305 -A288::nat
   7.306 -A289::nat
   7.307 -A290::nat
   7.308 -A291::nat
   7.309 -A292::nat
   7.310 -A293::nat
   7.311 -A294::nat
   7.312 -A295::nat
   7.313 -A296::nat
   7.314 -A297::nat
   7.315 -A298::nat
   7.316 -A299::nat
   7.317 -
   7.318 -lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
   7.319 -  by simp
   7.320 -
   7.321 -lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
   7.322 -  by simp
   7.323 -
   7.324 -lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   7.325 -  by simp
   7.326 -
   7.327 -lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   7.328 -  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
   7.329 -  done
   7.330 -
   7.331 -lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   7.332 -  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   7.333 -  apply simp
   7.334 -  done
   7.335 -
   7.336 -lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   7.337 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   7.338 -  apply simp
   7.339 -  done
   7.340 -
   7.341 -lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   7.342 -  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   7.343 -  apply simp
   7.344 -  done
   7.345 -
   7.346 -lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   7.347 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   7.348 -  apply simp
   7.349 -  done
   7.350 -
   7.351 -lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   7.352 -  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   7.353 -  apply auto
   7.354 -  done
   7.355 -
   7.356 -lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   7.357 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   7.358 -  apply auto
   7.359 -  done
   7.360 -
   7.361 -lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   7.362 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   7.363 -  apply auto
   7.364 -  done
   7.365 -
   7.366 -lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   7.367 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   7.368 -  apply auto
   7.369 -  done
   7.370 -
   7.371 -
   7.372 -lemma True
   7.373 -proof -
   7.374 -  {
   7.375 -    fix P r
   7.376 -    assume pre: "P (A155 r)"
   7.377 -    have "\<exists>x. P x"
   7.378 -      using pre
   7.379 -      apply -
   7.380 -      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   7.381 -      apply auto 
   7.382 -      done
   7.383 -  }
   7.384 -  show ?thesis ..
   7.385 -qed
   7.386 -
   7.387 -
   7.388 -lemma "\<exists>r. A155 r = x"
   7.389 -  apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
   7.390 -  done
   7.391 -
   7.392 -
   7.393 -end
   7.394 \ No newline at end of file
     8.1 --- a/Admin/Benchmarks/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,43 +0,0 @@
     8.4 -
     8.5 -## targets
     8.6 -
     8.7 -default: all
     8.8 -images:
     8.9 -test: HOL-datatype HOL-record
    8.10 -all: images test
    8.11 -
    8.12 -
    8.13 -## global settings
    8.14 -
    8.15 -SRC = $(ISABELLE_HOME)/src
    8.16 -OUT = $(ISABELLE_OUTPUT)
    8.17 -LOG = $(OUT)/log
    8.18 -
    8.19 -
    8.20 -## HOL-datatype
    8.21 -
    8.22 -HOL:
    8.23 -	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
    8.24 -
    8.25 -
    8.26 -HOL-datatype: HOL $(LOG)/HOL-datatype.gz
    8.27 -
    8.28 -$(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/ROOT.ML		\
    8.29 -  HOL-datatype/Brackin.thy HOL-datatype/Instructions.thy	\
    8.30 -  HOL-datatype/SML.thy HOL-datatype/Verilog.thy
    8.31 -	@$(ISABELLE_TOOL) usedir -s datatype $(OUT)/HOL HOL-datatype
    8.32 -
    8.33 -
    8.34 -## HOL-record
    8.35 -
    8.36 -HOL-record: HOL $(LOG)/HOL-record.gz
    8.37 -
    8.38 -$(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML	\
    8.39 -   HOL-record/Record_Benchmark.thy
    8.40 -	@$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record
    8.41 -
    8.42 -
    8.43 -## clean
    8.44 -
    8.45 -clean:
    8.46 -	@rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz
     9.1 --- a/src/CCL/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
     9.2 +++ b/src/CCL/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
     9.3 @@ -8,6 +8,7 @@
     9.4  images: CCL
     9.5  test: CCL-ex
     9.6  all: images test
     9.7 +full: all
     9.8  smlnj: all
     9.9  
    9.10  
    10.1 --- a/src/CTT/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    10.2 +++ b/src/CTT/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    10.3 @@ -8,6 +8,7 @@
    10.4  images: CTT
    10.5  test: CTT-ex
    10.6  all: images test
    10.7 +full: all
    10.8  smlnj: all
    10.9  
   10.10  
    11.1 --- a/src/Cube/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    11.2 +++ b/src/Cube/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    11.3 @@ -8,6 +8,7 @@
    11.4  images:
    11.5  test: Pure-Cube
    11.6  all: images test
    11.7 +full: all
    11.8  smlnj: all
    11.9  
   11.10  
    12.1 --- a/src/FOL/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    12.2 +++ b/src/FOL/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    12.3 @@ -8,6 +8,7 @@
    12.4  images: FOL
    12.5  test: FOL-ex
    12.6  all: images test
    12.7 +full: all
    12.8  smlnj: all
    12.9  
   12.10  
    13.1 --- a/src/FOLP/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    13.2 +++ b/src/FOLP/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    13.3 @@ -8,6 +8,7 @@
    13.4  images: FOLP
    13.5  test: FOLP-ex
    13.6  all: images test
    13.7 +full: all
    13.8  smlnj: all
    13.9  
   13.10  
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Datatype_Benchmark/Brackin.thy	Wed Dec 14 12:02:02 2011 +0100
    14.3 @@ -0,0 +1,43 @@
    14.4 +(*  Title:      HOL/Datatype_Benchmark/Brackin.thy
    14.5 +
    14.6 +A couple from Steve Brackin's work.
    14.7 +*)
    14.8 +
    14.9 +theory Brackin imports Main begin
   14.10 +
   14.11 +datatype   T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
   14.12 +                X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
   14.13 +                X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
   14.14 +                X32 | X33 | X34
   14.15 +
   14.16 +datatype  
   14.17 +  ('a, 'b, 'c) TY1 =
   14.18 +      NoF__
   14.19 +    | Fk__ 'a "('a, 'b, 'c) TY2"
   14.20 +and
   14.21 +  ('a, 'b, 'c) TY2 =
   14.22 +      Ta__ bool
   14.23 +    | Td__ bool
   14.24 +    | Tf__ "('a, 'b, 'c) TY1"
   14.25 +    | Tk__ bool
   14.26 +    | Tp__ bool
   14.27 +    | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
   14.28 +    | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
   14.29 +and
   14.30 +  ('a, 'b, 'c) TY3 =
   14.31 +      NoS__
   14.32 +    | Fresh__ "('a, 'b, 'c) TY2"
   14.33 +    | Trustworthy__ 'a
   14.34 +    | PrivateKey__ 'a 'b 'c
   14.35 +    | PublicKey__ 'a 'b 'c
   14.36 +    | Conveyed__ 'a "('a, 'b, 'c) TY2"
   14.37 +    | Possesses__ 'a "('a, 'b, 'c) TY2"
   14.38 +    | Received__ 'a "('a, 'b, 'c) TY2"
   14.39 +    | Recognizes__ 'a "('a, 'b, 'c) TY2"
   14.40 +    | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
   14.41 +    | Sends__ 'a "('a, 'b, 'c) TY2" 'b
   14.42 +    | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
   14.43 +    | Believes__ 'a "('a, 'b, 'c) TY3"
   14.44 +    | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
   14.45 +
   14.46 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Datatype_Benchmark/Instructions.thy	Wed Dec 14 12:02:02 2011 +0100
    15.3 @@ -0,0 +1,162 @@
    15.4 +(*  Title:      HOL/Datatype_Benchmark/Instructions.thy
    15.5 +
    15.6 +Example from Konrad: 68000 instruction set.
    15.7 +*)
    15.8 +
    15.9 +theory Instructions imports Main begin
   15.10 +
   15.11 +datatype Size = Byte | Word | Long
   15.12 +
   15.13 +datatype DataRegister
   15.14 +              = RegD0
   15.15 +              | RegD1
   15.16 +              | RegD2
   15.17 +              | RegD3
   15.18 +              | RegD4
   15.19 +              | RegD5
   15.20 +              | RegD6
   15.21 +              | RegD7
   15.22 +
   15.23 +datatype AddressRegister
   15.24 +              = RegA0
   15.25 +              | RegA1
   15.26 +              | RegA2
   15.27 +              | RegA3
   15.28 +              | RegA4
   15.29 +              | RegA5
   15.30 +              | RegA6
   15.31 +              | RegA7
   15.32 +
   15.33 +datatype DataOrAddressRegister
   15.34 +              = data DataRegister
   15.35 +              | address AddressRegister
   15.36 +
   15.37 +datatype Condition
   15.38 +              = Hi
   15.39 +              | Ls
   15.40 +              | Cc
   15.41 +              | Cs
   15.42 +              | Ne
   15.43 +              | Eq
   15.44 +              | Vc
   15.45 +              | Vs
   15.46 +              | Pl
   15.47 +              | Mi
   15.48 +              | Ge
   15.49 +              | Lt
   15.50 +              | Gt
   15.51 +              | Le
   15.52 +
   15.53 +datatype AddressingMode
   15.54 +        = immediate nat
   15.55 +        | direct DataOrAddressRegister
   15.56 +        | indirect AddressRegister
   15.57 +        | postinc AddressRegister
   15.58 +        | predec AddressRegister
   15.59 +        | indirectdisp nat AddressRegister
   15.60 +        | indirectindex nat AddressRegister DataOrAddressRegister Size
   15.61 +        | absolute nat
   15.62 +        | pcdisp nat
   15.63 +        | pcindex nat DataOrAddressRegister Size
   15.64 +
   15.65 +datatype M68kInstruction
   15.66 +    = ABCD AddressingMode AddressingMode
   15.67 +    | ADD Size AddressingMode AddressingMode
   15.68 +    | ADDA Size AddressingMode AddressRegister
   15.69 +    | ADDI Size nat AddressingMode
   15.70 +    | ADDQ Size nat AddressingMode
   15.71 +    | ADDX Size AddressingMode AddressingMode
   15.72 +    | AND Size AddressingMode AddressingMode
   15.73 +    | ANDI Size nat AddressingMode
   15.74 +    | ANDItoCCR nat
   15.75 +    | ANDItoSR nat
   15.76 +    | ASL Size AddressingMode DataRegister
   15.77 +    | ASLW AddressingMode
   15.78 +    | ASR Size AddressingMode DataRegister
   15.79 +    | ASRW AddressingMode
   15.80 +    | Bcc Condition Size nat
   15.81 +    | BTST Size AddressingMode AddressingMode
   15.82 +    | BCHG Size AddressingMode AddressingMode
   15.83 +    | BCLR Size AddressingMode AddressingMode
   15.84 +    | BSET Size AddressingMode AddressingMode
   15.85 +    | BRA Size nat
   15.86 +    | BSR Size nat
   15.87 +    | CHK AddressingMode DataRegister
   15.88 +    | CLR Size AddressingMode
   15.89 +    | CMP Size AddressingMode DataRegister
   15.90 +    | CMPA Size AddressingMode AddressRegister
   15.91 +    | CMPI Size nat AddressingMode
   15.92 +    | CMPM Size AddressRegister AddressRegister
   15.93 +    | DBT DataRegister nat
   15.94 +    | DBF DataRegister nat
   15.95 +    | DBcc Condition DataRegister nat
   15.96 +    | DIVS AddressingMode DataRegister
   15.97 +    | DIVU AddressingMode DataRegister
   15.98 +    | EOR Size DataRegister AddressingMode
   15.99 +    | EORI Size nat AddressingMode
  15.100 +    | EORItoCCR nat
  15.101 +    | EORItoSR nat
  15.102 +    | EXG DataOrAddressRegister DataOrAddressRegister
  15.103 +    | EXT Size DataRegister
  15.104 +    | ILLEGAL
  15.105 +    | JMP AddressingMode
  15.106 +    | JSR AddressingMode
  15.107 +    | LEA AddressingMode AddressRegister
  15.108 +    | LINK AddressRegister nat
  15.109 +    | LSL Size AddressingMode DataRegister
  15.110 +    | LSLW AddressingMode
  15.111 +    | LSR Size AddressingMode DataRegister
  15.112 +    | LSRW AddressingMode
  15.113 +    | MOVE Size AddressingMode AddressingMode
  15.114 +    | MOVEtoCCR AddressingMode
  15.115 +    | MOVEtoSR AddressingMode
  15.116 +    | MOVEfromSR AddressingMode
  15.117 +    | MOVEtoUSP AddressingMode
  15.118 +    | MOVEfromUSP AddressingMode
  15.119 +    | MOVEA Size AddressingMode AddressRegister
  15.120 +    | MOVEMto Size AddressingMode "DataOrAddressRegister list"
  15.121 +    | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
  15.122 +    | MOVEP Size AddressingMode AddressingMode
  15.123 +    | MOVEQ nat DataRegister
  15.124 +    | MULS AddressingMode DataRegister
  15.125 +    | MULU AddressingMode DataRegister
  15.126 +    | NBCD AddressingMode
  15.127 +    | NEG Size AddressingMode
  15.128 +    | NEGX Size AddressingMode
  15.129 +    | NOP
  15.130 +    | NOT Size AddressingMode
  15.131 +    | OR Size AddressingMode AddressingMode
  15.132 +    | ORI Size nat AddressingMode
  15.133 +    | ORItoCCR nat
  15.134 +    | ORItoSR nat
  15.135 +    | PEA AddressingMode
  15.136 +    | RESET
  15.137 +    | ROL Size AddressingMode DataRegister
  15.138 +    | ROLW AddressingMode
  15.139 +    | ROR Size AddressingMode DataRegister
  15.140 +    | RORW AddressingMode
  15.141 +    | ROXL Size AddressingMode DataRegister
  15.142 +    | ROXLW AddressingMode
  15.143 +    | ROXR Size AddressingMode DataRegister
  15.144 +    | ROXRW AddressingMode
  15.145 +    | RTE
  15.146 +    | RTR
  15.147 +    | RTS
  15.148 +    | SBCD AddressingMode AddressingMode
  15.149 +    | ST AddressingMode
  15.150 +    | SF AddressingMode
  15.151 +    | Scc Condition AddressingMode
  15.152 +    | STOP nat
  15.153 +    | SUB Size AddressingMode AddressingMode
  15.154 +    | SUBA Size AddressingMode AddressingMode
  15.155 +    | SUBI Size nat AddressingMode
  15.156 +    | SUBQ Size nat AddressingMode
  15.157 +    | SUBX Size AddressingMode AddressingMode
  15.158 +    | SWAP DataRegister
  15.159 +    | TAS AddressingMode
  15.160 +    | TRAP nat
  15.161 +    | TRAPV
  15.162 +    | TST Size AddressingMode
  15.163 +    | UNLK AddressRegister
  15.164 +
  15.165 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Datatype_Benchmark/ROOT.ML	Wed Dec 14 12:02:02 2011 +0100
    16.3 @@ -0,0 +1,8 @@
    16.4 +(*  Title:      HOL/Datatype_Benchmark/ROOT.ML
    16.5 +
    16.6 +Some rather large datatype examples (from John Harrison).
    16.7 +*)
    16.8 +
    16.9 +Toplevel.timing := true;
   16.10 +
   16.11 +use_thys ["Brackin", "Instructions", "SML", "Verilog"];
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Datatype_Benchmark/SML.thy	Wed Dec 14 12:02:02 2011 +0100
    17.3 @@ -0,0 +1,91 @@
    17.4 +(*  Title:      HOL/Datatype_Benchmark/SML.thy
    17.5 +
    17.6 +Example from Myra: part of the syntax of SML.
    17.7 +*)
    17.8 +
    17.9 +theory SML imports Main begin
   17.10 +
   17.11 +datatype
   17.12 +  string = EMPTY_STRING | CONS_STRING nat string
   17.13 +
   17.14 +datatype
   17.15 +   strid = STRID string
   17.16 +
   17.17 +datatype
   17.18 +   var = VAR string
   17.19 +
   17.20 +datatype
   17.21 +   con = CON string
   17.22 +
   17.23 +datatype
   17.24 +   scon = SCINT nat | SCSTR string
   17.25 +
   17.26 +datatype
   17.27 +   excon = EXCON string
   17.28 +
   17.29 +datatype
   17.30 +   label = LABEL string
   17.31 +
   17.32 +datatype
   17.33 +  'a nonemptylist = Head_and_tail 'a "'a list"
   17.34 +
   17.35 +datatype
   17.36 +  'a long = BASE 'a | QUALIFIED strid "'a long"
   17.37 +
   17.38 +datatype
   17.39 +   atpat_e = WILDCARDatpat_e
   17.40 +           | SCONatpat_e scon
   17.41 +           | VARatpat_e var
   17.42 +           | CONatpat_e "con long"
   17.43 +           | EXCONatpat_e "excon long"
   17.44 +           | RECORDatpat_e "patrow_e option"
   17.45 +           | PARatpat_e pat_e
   17.46 +and
   17.47 +   patrow_e = DOTDOTDOT_e
   17.48 +            | PATROW_e label pat_e "patrow_e option"
   17.49 +and
   17.50 +   pat_e = ATPATpat_e atpat_e
   17.51 +         | CONpat_e "con long" atpat_e
   17.52 +         | EXCONpat_e "excon long" atpat_e
   17.53 +         | LAYEREDpat_e var pat_e
   17.54 +and
   17.55 +   conbind_e = CONBIND_e con "conbind_e option"
   17.56 +and
   17.57 +   datbind_e = DATBIND_e conbind_e "datbind_e option"
   17.58 +and
   17.59 +   exbind_e = EXBIND1_e excon "exbind_e option"
   17.60 +            | EXBIND2_e excon "excon long" "exbind_e option"
   17.61 +and
   17.62 +   atexp_e = SCONatexp_e scon
   17.63 +           | VARatexp_e "var long"
   17.64 +           | CONatexp_e "con long"
   17.65 +           | EXCONatexp_e "excon long"
   17.66 +           | RECORDatexp_e "exprow_e option"
   17.67 +           | LETatexp_e dec_e exp_e
   17.68 +           | PARatexp_e exp_e
   17.69 +and
   17.70 +   exprow_e = EXPROW_e label exp_e "exprow_e option"
   17.71 +and
   17.72 +   exp_e = ATEXPexp_e atexp_e
   17.73 +         | APPexp_e exp_e atexp_e
   17.74 +         | HANDLEexp_e exp_e match_e
   17.75 +         | RAISEexp_e exp_e
   17.76 +         | FNexp_e match_e
   17.77 +and
   17.78 +   match_e = MATCH_e mrule_e "match_e option"
   17.79 +and
   17.80 +   mrule_e = MRULE_e pat_e exp_e
   17.81 +and
   17.82 +   dec_e = VALdec_e valbind_e
   17.83 +         | DATATYPEdec_e datbind_e
   17.84 +         | ABSTYPEdec_e datbind_e dec_e
   17.85 +         | EXCEPTdec_e exbind_e
   17.86 +         | LOCALdec_e dec_e dec_e
   17.87 +         | OPENdec_e "strid long nonemptylist"
   17.88 +         | EMPTYdec_e
   17.89 +         | SEQdec_e dec_e dec_e
   17.90 +and
   17.91 +   valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
   17.92 +             | RECvalbind_e valbind_e
   17.93 +
   17.94 +end
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/Datatype_Benchmark/Verilog.thy	Wed Dec 14 12:02:02 2011 +0100
    18.3 @@ -0,0 +1,138 @@
    18.4 +(*  Title:      HOL/Datatype_Benchmark/Verilog.thy
    18.5 +
    18.6 +Example from Daryl: a Verilog grammar.
    18.7 +*)
    18.8 +
    18.9 +theory Verilog imports Main begin
   18.10 +
   18.11 +datatype
   18.12 +  Source_text
   18.13 +     = module string "string list" "Module_item list"
   18.14 +     | Source_textMeta string
   18.15 +and
   18.16 +  Module_item
   18.17 +     = "declaration" Declaration
   18.18 +     | initial Statement
   18.19 +     | always Statement
   18.20 +     | assign Lvalue Expression
   18.21 +     | Module_itemMeta string
   18.22 +and
   18.23 +  Declaration
   18.24 +     = reg_declaration "Range option" "string list"
   18.25 +     | net_declaration "Range option" "string list"
   18.26 +     | input_declaration "Range option" "string list"
   18.27 +     | output_declaration "Range option" "string list"
   18.28 +     | DeclarationMeta string
   18.29 +and
   18.30 +  Range = range Expression Expression | RangeMeta string
   18.31 +and
   18.32 +  Statement
   18.33 +     = clock_statement Clock Statement_or_null
   18.34 +     | blocking_assignment Lvalue Expression
   18.35 +     | non_blocking_assignment Lvalue Expression
   18.36 +     | conditional_statement
   18.37 +          Expression Statement_or_null "Statement_or_null option"
   18.38 +     | case_statement Expression "Case_item list"
   18.39 +     | while_loop Expression Statement
   18.40 +     | repeat_loop Expression Statement
   18.41 +     | for_loop
   18.42 +          Lvalue Expression Expression Lvalue Expression Statement
   18.43 +     | forever_loop Statement
   18.44 +     | disable string
   18.45 +     | seq_block "string option" "Statement list"
   18.46 +     | StatementMeta string
   18.47 +and
   18.48 +  Statement_or_null
   18.49 +     = statement Statement | null_statement | Statement_or_nullMeta string
   18.50 +and
   18.51 +  Clock
   18.52 +     = posedge string
   18.53 +     | negedge string
   18.54 +     | clock string
   18.55 +     | ClockMeta string
   18.56 +and
   18.57 +  Case_item
   18.58 +     = case_item "Expression list" Statement_or_null
   18.59 +     | default_case_item Statement_or_null
   18.60 +     | Case_itemMeta string
   18.61 +and
   18.62 +  Expression
   18.63 +     = plus Expression Expression
   18.64 +     | minus Expression Expression
   18.65 +     | lshift Expression Expression
   18.66 +     | rshift Expression Expression
   18.67 +     | lt Expression Expression
   18.68 +     | leq Expression Expression
   18.69 +     | gt Expression Expression
   18.70 +     | geq Expression Expression
   18.71 +     | logeq Expression Expression
   18.72 +     | logneq Expression Expression
   18.73 +     | caseeq Expression Expression
   18.74 +     | caseneq Expression Expression
   18.75 +     | bitand Expression Expression
   18.76 +     | bitxor Expression Expression
   18.77 +     | bitor Expression Expression
   18.78 +     | logand Expression Expression
   18.79 +     | logor Expression Expression
   18.80 +     | conditional Expression Expression Expression
   18.81 +     | positive Primary
   18.82 +     | negative Primary
   18.83 +     | lognot Primary
   18.84 +     | bitnot Primary
   18.85 +     | reducand Primary
   18.86 +     | reducxor Primary
   18.87 +     | reducor Primary
   18.88 +     | reducnand Primary
   18.89 +     | reducxnor Primary
   18.90 +     | reducnor Primary
   18.91 +     | primary Primary
   18.92 +     | ExpressionMeta string
   18.93 +and
   18.94 +  Primary
   18.95 +     = primary_number Number
   18.96 +     | primary_IDENTIFIER string
   18.97 +     | primary_bit_select string Expression
   18.98 +     | primary_part_select string Expression Expression
   18.99 +     | primary_gen_bit_select Expression Expression
  18.100 +     | primary_gen_part_select Expression Expression Expression
  18.101 +     | primary_concatenation Concatenation
  18.102 +     | primary_multiple_concatenation Multiple_concatenation
  18.103 +     | brackets Expression
  18.104 +     | PrimaryMeta string
  18.105 +and
  18.106 +  Lvalue
  18.107 +     = lvalue string
  18.108 +     | lvalue_bit_select string Expression
  18.109 +     | lvalue_part_select string Expression Expression
  18.110 +     | lvalue_concatenation Concatenation
  18.111 +     | LvalueMeta string
  18.112 +and
  18.113 +  Number
  18.114 +     = decimal string
  18.115 +     | based "string option" string
  18.116 +     | NumberMeta string
  18.117 +and
  18.118 +  Concatenation
  18.119 +     = concatenation "Expression list" | ConcatenationMeta string
  18.120 +and
  18.121 +  Multiple_concatenation
  18.122 +     = multiple_concatenation Expression "Expression list"
  18.123 +     | Multiple_concatenationMeta string
  18.124 +and
  18.125 +  meta
  18.126 +     = Meta_Source_text Source_text
  18.127 +     | Meta_Module_item Module_item
  18.128 +     | Meta_Declaration Declaration
  18.129 +     | Meta_Range Range
  18.130 +     | Meta_Statement Statement
  18.131 +     | Meta_Statement_or_null Statement_or_null
  18.132 +     | Meta_Clock Clock
  18.133 +     | Meta_Case_item Case_item
  18.134 +     | Meta_Expression Expression
  18.135 +     | Meta_Primary Primary
  18.136 +     | Meta_Lvalue Lvalue
  18.137 +     | Meta_Number Number
  18.138 +     | Meta_Concatenation Concatenation
  18.139 +     | Meta_Multiple_concatenation Multiple_concatenation
  18.140 +
  18.141 +end
    19.1 --- a/src/HOL/HOLCF/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    19.2 +++ b/src/HOL/HOLCF/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    19.3 @@ -17,6 +17,7 @@
    19.4    IOA-Storage \
    19.5    IOA-ex
    19.6  all: images test
    19.7 +full: all
    19.8  
    19.9  
   19.10  ## global settings
    20.1 --- a/src/HOL/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    20.2 +++ b/src/HOL/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    20.3 @@ -81,6 +81,10 @@
    20.4    HOL-ZF
    20.5      # ^ this is the sort position
    20.6  
    20.7 +benchmark: \
    20.8 +  HOL-Datatype_Benchmark \
    20.9 +  HOL-Record_Benchmark
   20.10 +
   20.11  images-no-smlnj: \
   20.12    HOL-Probability
   20.13  
   20.14 @@ -91,8 +95,10 @@
   20.15    HOL-Nominal-Examples
   20.16  
   20.17  all: test-no-smlnj test images-no-smlnj images
   20.18 +full: all benchmark
   20.19  smlnj: test images
   20.20  
   20.21 +
   20.22  ## global settings
   20.23  
   20.24  SRC = $(ISABELLE_HOME)/src
   20.25 @@ -1772,6 +1778,28 @@
   20.26  	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
   20.27  
   20.28  
   20.29 +
   20.30 +## HOL-Datatype_Benchmark
   20.31 +
   20.32 +HOL-Datatype_Benchmark: HOL $(LOG)/HOL-Datatype_Benchmark.gz
   20.33 +
   20.34 +$(LOG)/HOL-Datatype_Benchmark.gz: $(OUT)/HOL				\
   20.35 +  Datatype_Benchmark/ROOT.ML Datatype_Benchmark/Brackin.thy		\
   20.36 +  Datatype_Benchmark/Instructions.thy Datatype_Benchmark/SML.thy	\
   20.37 +  Datatype_Benchmark/Verilog.thy
   20.38 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Datatype_Benchmark
   20.39 +
   20.40 +
   20.41 +## HOL-Record_Benchmark
   20.42 +
   20.43 +HOL-Record_Benchmark: HOL $(LOG)/HOL-Record_Benchmark.gz
   20.44 +
   20.45 +$(LOG)/HOL-Record_Benchmark.gz: $(OUT)/HOL Record_Benchmark/ROOT.ML	\
   20.46 +   Record_Benchmark/Record_Benchmark.thy
   20.47 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Record_Benchmark
   20.48 +
   20.49 +
   20.50 +
   20.51  ## clean
   20.52  
   20.53  clean:
   20.54 @@ -1799,23 +1827,25 @@
   20.55  		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz		\
   20.56  		$(LOG)/HOL-Proofs-Extraction.gz				\
   20.57  		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
   20.58 -		$(LOG)/HOL-Word-SMT_Examples.gz				\
   20.59 -		$(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz	\
   20.60 -		$(LOG)/HOL-SPARK-Manual.gz				\
   20.61 -		$(LOG)/HOL-Statespace.gz				\
   20.62 +		$(LOG)/HOL-Word-SMT_Examples.gz $(LOG)/HOL-SPARK.gz	\
   20.63 +		$(LOG)/HOL-SPARK-Examples.gz				\
   20.64 +		$(LOG)/HOL-SPARK-Manual.gz $(LOG)/HOL-Statespace.gz	\
   20.65  		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
   20.66  		$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz		\
   20.67  		$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz		\
   20.68  		$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz	\
   20.69  		$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL		\
   20.70  		$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie	\
   20.71 -		$(OUT)/HOL-IMP $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis	\
   20.72 -		$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain	\
   20.73 +		$(OUT)/HOL-IMP $(OUT)/HOL-Main				\
   20.74 +		$(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA		\
   20.75 +		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain			\
   20.76  		$(OUT)/HOL-Probability $(OUT)/HOL-Proofs		\
   20.77 -		$(OUT)/HOL-SPARK					\
   20.78 -		$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA			\
   20.79 -		$(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz	\
   20.80 -		$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\
   20.81 -		$(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\
   20.82 +		$(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/HOL4		\
   20.83 +		$(OUT)/TLA $(OUT)/HOLCF $(LOG)/HOLCF.gz			\
   20.84 +		$(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz			\
   20.85 +		$(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA $(LOG)/IOA.gz		\
   20.86 +		$(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz			\
   20.87  		$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz		\
   20.88 -		$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz
   20.89 +		$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz		\
   20.90 +		$(LOG)/HOL-Datatype_Benchmark.gz			\
   20.91 +		$(LOG)/HOL-Record_Benchmark.gz
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/Record_Benchmark/ROOT.ML	Wed Dec 14 12:02:02 2011 +0100
    21.3 @@ -0,0 +1,8 @@
    21.4 +(*  Title:      HOL/Record_Benchmark/ROOT.ML
    21.5 +
    21.6 +Some benchmark on large record.
    21.7 +*)
    21.8 +
    21.9 +Toplevel.timing := true;
   21.10 +
   21.11 +use_thys ["Record_Benchmark"];
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/Record_Benchmark/Record_Benchmark.thy	Wed Dec 14 12:02:02 2011 +0100
    22.3 @@ -0,0 +1,390 @@
    22.4 +(*  Title:      HOL/Record_Benchmark/Record_Benchmark.thy
    22.5 +    Author:     Norbert Schirmer, DFKI
    22.6 +*)
    22.7 +
    22.8 +header {* Benchmark for large record *}
    22.9 +
   22.10 +theory Record_Benchmark
   22.11 +imports Main
   22.12 +begin
   22.13 +
   22.14 +declare [[record_timing]]
   22.15 +
   22.16 +record many_A =
   22.17 +A000::nat
   22.18 +A001::nat
   22.19 +A002::nat
   22.20 +A003::nat
   22.21 +A004::nat
   22.22 +A005::nat
   22.23 +A006::nat
   22.24 +A007::nat
   22.25 +A008::nat
   22.26 +A009::nat
   22.27 +A010::nat
   22.28 +A011::nat
   22.29 +A012::nat
   22.30 +A013::nat
   22.31 +A014::nat
   22.32 +A015::nat
   22.33 +A016::nat
   22.34 +A017::nat
   22.35 +A018::nat
   22.36 +A019::nat
   22.37 +A020::nat
   22.38 +A021::nat
   22.39 +A022::nat
   22.40 +A023::nat
   22.41 +A024::nat
   22.42 +A025::nat
   22.43 +A026::nat
   22.44 +A027::nat
   22.45 +A028::nat
   22.46 +A029::nat
   22.47 +A030::nat
   22.48 +A031::nat
   22.49 +A032::nat
   22.50 +A033::nat
   22.51 +A034::nat
   22.52 +A035::nat
   22.53 +A036::nat
   22.54 +A037::nat
   22.55 +A038::nat
   22.56 +A039::nat
   22.57 +A040::nat
   22.58 +A041::nat
   22.59 +A042::nat
   22.60 +A043::nat
   22.61 +A044::nat
   22.62 +A045::nat
   22.63 +A046::nat
   22.64 +A047::nat
   22.65 +A048::nat
   22.66 +A049::nat
   22.67 +A050::nat
   22.68 +A051::nat
   22.69 +A052::nat
   22.70 +A053::nat
   22.71 +A054::nat
   22.72 +A055::nat
   22.73 +A056::nat
   22.74 +A057::nat
   22.75 +A058::nat
   22.76 +A059::nat
   22.77 +A060::nat
   22.78 +A061::nat
   22.79 +A062::nat
   22.80 +A063::nat
   22.81 +A064::nat
   22.82 +A065::nat
   22.83 +A066::nat
   22.84 +A067::nat
   22.85 +A068::nat
   22.86 +A069::nat
   22.87 +A070::nat
   22.88 +A071::nat
   22.89 +A072::nat
   22.90 +A073::nat
   22.91 +A074::nat
   22.92 +A075::nat
   22.93 +A076::nat
   22.94 +A077::nat
   22.95 +A078::nat
   22.96 +A079::nat
   22.97 +A080::nat
   22.98 +A081::nat
   22.99 +A082::nat
  22.100 +A083::nat
  22.101 +A084::nat
  22.102 +A085::nat
  22.103 +A086::nat
  22.104 +A087::nat
  22.105 +A088::nat
  22.106 +A089::nat
  22.107 +A090::nat
  22.108 +A091::nat
  22.109 +A092::nat
  22.110 +A093::nat
  22.111 +A094::nat
  22.112 +A095::nat
  22.113 +A096::nat
  22.114 +A097::nat
  22.115 +A098::nat
  22.116 +A099::nat
  22.117 +A100::nat
  22.118 +A101::nat
  22.119 +A102::nat
  22.120 +A103::nat
  22.121 +A104::nat
  22.122 +A105::nat
  22.123 +A106::nat
  22.124 +A107::nat
  22.125 +A108::nat
  22.126 +A109::nat
  22.127 +A110::nat
  22.128 +A111::nat
  22.129 +A112::nat
  22.130 +A113::nat
  22.131 +A114::nat
  22.132 +A115::nat
  22.133 +A116::nat
  22.134 +A117::nat
  22.135 +A118::nat
  22.136 +A119::nat
  22.137 +A120::nat
  22.138 +A121::nat
  22.139 +A122::nat
  22.140 +A123::nat
  22.141 +A124::nat
  22.142 +A125::nat
  22.143 +A126::nat
  22.144 +A127::nat
  22.145 +A128::nat
  22.146 +A129::nat
  22.147 +A130::nat
  22.148 +A131::nat
  22.149 +A132::nat
  22.150 +A133::nat
  22.151 +A134::nat
  22.152 +A135::nat
  22.153 +A136::nat
  22.154 +A137::nat
  22.155 +A138::nat
  22.156 +A139::nat
  22.157 +A140::nat
  22.158 +A141::nat
  22.159 +A142::nat
  22.160 +A143::nat
  22.161 +A144::nat
  22.162 +A145::nat
  22.163 +A146::nat
  22.164 +A147::nat
  22.165 +A148::nat
  22.166 +A149::nat
  22.167 +A150::nat
  22.168 +A151::nat
  22.169 +A152::nat
  22.170 +A153::nat
  22.171 +A154::nat
  22.172 +A155::nat
  22.173 +A156::nat
  22.174 +A157::nat
  22.175 +A158::nat
  22.176 +A159::nat
  22.177 +A160::nat
  22.178 +A161::nat
  22.179 +A162::nat
  22.180 +A163::nat
  22.181 +A164::nat
  22.182 +A165::nat
  22.183 +A166::nat
  22.184 +A167::nat
  22.185 +A168::nat
  22.186 +A169::nat
  22.187 +A170::nat
  22.188 +A171::nat
  22.189 +A172::nat
  22.190 +A173::nat
  22.191 +A174::nat
  22.192 +A175::nat
  22.193 +A176::nat
  22.194 +A177::nat
  22.195 +A178::nat
  22.196 +A179::nat
  22.197 +A180::nat
  22.198 +A181::nat
  22.199 +A182::nat
  22.200 +A183::nat
  22.201 +A184::nat
  22.202 +A185::nat
  22.203 +A186::nat
  22.204 +A187::nat
  22.205 +A188::nat
  22.206 +A189::nat
  22.207 +A190::nat
  22.208 +A191::nat
  22.209 +A192::nat
  22.210 +A193::nat
  22.211 +A194::nat
  22.212 +A195::nat
  22.213 +A196::nat
  22.214 +A197::nat
  22.215 +A198::nat
  22.216 +A199::nat
  22.217 +A200::nat
  22.218 +A201::nat
  22.219 +A202::nat
  22.220 +A203::nat
  22.221 +A204::nat
  22.222 +A205::nat
  22.223 +A206::nat
  22.224 +A207::nat
  22.225 +A208::nat
  22.226 +A209::nat
  22.227 +A210::nat
  22.228 +A211::nat
  22.229 +A212::nat
  22.230 +A213::nat
  22.231 +A214::nat
  22.232 +A215::nat
  22.233 +A216::nat
  22.234 +A217::nat
  22.235 +A218::nat
  22.236 +A219::nat
  22.237 +A220::nat
  22.238 +A221::nat
  22.239 +A222::nat
  22.240 +A223::nat
  22.241 +A224::nat
  22.242 +A225::nat
  22.243 +A226::nat
  22.244 +A227::nat
  22.245 +A228::nat
  22.246 +A229::nat
  22.247 +A230::nat
  22.248 +A231::nat
  22.249 +A232::nat
  22.250 +A233::nat
  22.251 +A234::nat
  22.252 +A235::nat
  22.253 +A236::nat
  22.254 +A237::nat
  22.255 +A238::nat
  22.256 +A239::nat
  22.257 +A240::nat
  22.258 +A241::nat
  22.259 +A242::nat
  22.260 +A243::nat
  22.261 +A244::nat
  22.262 +A245::nat
  22.263 +A246::nat
  22.264 +A247::nat
  22.265 +A248::nat
  22.266 +A249::nat
  22.267 +A250::nat
  22.268 +A251::nat
  22.269 +A252::nat
  22.270 +A253::nat
  22.271 +A254::nat
  22.272 +A255::nat
  22.273 +A256::nat
  22.274 +A257::nat
  22.275 +A258::nat
  22.276 +A259::nat
  22.277 +A260::nat
  22.278 +A261::nat
  22.279 +A262::nat
  22.280 +A263::nat
  22.281 +A264::nat
  22.282 +A265::nat
  22.283 +A266::nat
  22.284 +A267::nat
  22.285 +A268::nat
  22.286 +A269::nat
  22.287 +A270::nat
  22.288 +A271::nat
  22.289 +A272::nat
  22.290 +A273::nat
  22.291 +A274::nat
  22.292 +A275::nat
  22.293 +A276::nat
  22.294 +A277::nat
  22.295 +A278::nat
  22.296 +A279::nat
  22.297 +A280::nat
  22.298 +A281::nat
  22.299 +A282::nat
  22.300 +A283::nat
  22.301 +A284::nat
  22.302 +A285::nat
  22.303 +A286::nat
  22.304 +A287::nat
  22.305 +A288::nat
  22.306 +A289::nat
  22.307 +A290::nat
  22.308 +A291::nat
  22.309 +A292::nat
  22.310 +A293::nat
  22.311 +A294::nat
  22.312 +A295::nat
  22.313 +A296::nat
  22.314 +A297::nat
  22.315 +A298::nat
  22.316 +A299::nat
  22.317 +
  22.318 +lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
  22.319 +  by simp
  22.320 +
  22.321 +lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
  22.322 +  by simp
  22.323 +
  22.324 +lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
  22.325 +  by simp
  22.326 +
  22.327 +lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
  22.328 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
  22.329 +  done
  22.330 +
  22.331 +lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
  22.332 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
  22.333 +  apply simp
  22.334 +  done
  22.335 +
  22.336 +lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
  22.337 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
  22.338 +  apply simp
  22.339 +  done
  22.340 +
  22.341 +lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
  22.342 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
  22.343 +  apply simp
  22.344 +  done
  22.345 +
  22.346 +lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
  22.347 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
  22.348 +  apply simp
  22.349 +  done
  22.350 +
  22.351 +lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
  22.352 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
  22.353 +  apply auto
  22.354 +  done
  22.355 +
  22.356 +lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
  22.357 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
  22.358 +  apply auto
  22.359 +  done
  22.360 +
  22.361 +lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
  22.362 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
  22.363 +  apply auto
  22.364 +  done
  22.365 +
  22.366 +lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
  22.367 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
  22.368 +  apply auto
  22.369 +  done
  22.370 +
  22.371 +
  22.372 +lemma True
  22.373 +proof -
  22.374 +  {
  22.375 +    fix P r
  22.376 +    assume pre: "P (A155 r)"
  22.377 +    have "\<exists>x. P x"
  22.378 +      using pre
  22.379 +      apply -
  22.380 +      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
  22.381 +      apply auto 
  22.382 +      done
  22.383 +  }
  22.384 +  show ?thesis ..
  22.385 +qed
  22.386 +
  22.387 +
  22.388 +lemma "\<exists>r. A155 r = x"
  22.389 +  apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
  22.390 +  done
  22.391 +
  22.392 +
  22.393 +end
  22.394 \ No newline at end of file
    23.1 --- a/src/LCF/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    23.2 +++ b/src/LCF/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    23.3 @@ -8,6 +8,7 @@
    23.4  images: LCF
    23.5  test: LCF-ex
    23.6  all: images test
    23.7 +full: all
    23.8  smlnj: all
    23.9  
   23.10  
    24.1 --- a/src/Pure/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    24.2 +++ b/src/Pure/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    24.3 @@ -8,6 +8,7 @@
    24.4  images: Pure
    24.5  test: RAW
    24.6  all: images test
    24.7 +full: all
    24.8  smlnj: all
    24.9  
   24.10  
    25.1 --- a/src/Sequents/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    25.2 +++ b/src/Sequents/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    25.3 @@ -8,6 +8,7 @@
    25.4  images: Sequents
    25.5  test: Sequents-LK
    25.6  all: images test
    25.7 +full: all
    25.8  smlnj: all
    25.9  
   25.10  
    26.1 --- a/src/Tools/WWW_Find/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    26.2 +++ b/src/Tools/WWW_Find/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    26.3 @@ -9,6 +9,7 @@
    26.4  images:
    26.5  test: Pure-WWW_Find
    26.6  all: images test
    26.7 +full: all
    26.8  smlnj: all
    26.9  
   26.10  
    27.1 --- a/src/ZF/IsaMakefile	Wed Dec 14 10:18:28 2011 +0100
    27.2 +++ b/src/ZF/IsaMakefile	Wed Dec 14 12:02:02 2011 +0100
    27.3 @@ -10,6 +10,7 @@
    27.4  #Note: keep targets sorted
    27.5  test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
    27.6  all: images test
    27.7 +full: all
    27.8  smlnj: all
    27.9  
   27.10