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