more visible benchmarks;
uniform IsaMakefile target "full" to cover such extra sessions;
--- a/Admin/Benchmarks/HOL-datatype/Brackin.thy Wed Dec 14 10:18:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy
-
-A couple from Steve Brackin's work.
-*)
-
-theory Brackin imports Main begin
-
-datatype T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
- X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
- X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
- X32 | X33 | X34
-
-datatype
- ('a, 'b, 'c) TY1 =
- NoF__
- | Fk__ 'a "('a, 'b, 'c) TY2"
-and
- ('a, 'b, 'c) TY2 =
- Ta__ bool
- | Td__ bool
- | Tf__ "('a, 'b, 'c) TY1"
- | Tk__ bool
- | Tp__ bool
- | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
- | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
-and
- ('a, 'b, 'c) TY3 =
- NoS__
- | Fresh__ "('a, 'b, 'c) TY2"
- | Trustworthy__ 'a
- | PrivateKey__ 'a 'b 'c
- | PublicKey__ 'a 'b 'c
- | Conveyed__ 'a "('a, 'b, 'c) TY2"
- | Possesses__ 'a "('a, 'b, 'c) TY2"
- | Received__ 'a "('a, 'b, 'c) TY2"
- | Recognizes__ 'a "('a, 'b, 'c) TY2"
- | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
- | Sends__ 'a "('a, 'b, 'c) TY2" 'b
- | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
- | Believes__ 'a "('a, 'b, 'c) TY3"
- | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
-
-end
--- a/Admin/Benchmarks/HOL-datatype/Instructions.thy Wed Dec 14 10:18:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(* Title: Admin/Benchmarks/HOL-datatype/Instructions.thy
-
-Example from Konrad: 68000 instruction set.
-*)
-
-theory Instructions imports Main begin
-
-datatype Size = Byte | Word | Long
-
-datatype DataRegister
- = RegD0
- | RegD1
- | RegD2
- | RegD3
- | RegD4
- | RegD5
- | RegD6
- | RegD7
-
-datatype AddressRegister
- = RegA0
- | RegA1
- | RegA2
- | RegA3
- | RegA4
- | RegA5
- | RegA6
- | RegA7
-
-datatype DataOrAddressRegister
- = data DataRegister
- | address AddressRegister
-
-datatype Condition
- = Hi
- | Ls
- | Cc
- | Cs
- | Ne
- | Eq
- | Vc
- | Vs
- | Pl
- | Mi
- | Ge
- | Lt
- | Gt
- | Le
-
-datatype AddressingMode
- = immediate nat
- | direct DataOrAddressRegister
- | indirect AddressRegister
- | postinc AddressRegister
- | predec AddressRegister
- | indirectdisp nat AddressRegister
- | indirectindex nat AddressRegister DataOrAddressRegister Size
- | absolute nat
- | pcdisp nat
- | pcindex nat DataOrAddressRegister Size
-
-datatype M68kInstruction
- = ABCD AddressingMode AddressingMode
- | ADD Size AddressingMode AddressingMode
- | ADDA Size AddressingMode AddressRegister
- | ADDI Size nat AddressingMode
- | ADDQ Size nat AddressingMode
- | ADDX Size AddressingMode AddressingMode
- | AND Size AddressingMode AddressingMode
- | ANDI Size nat AddressingMode
- | ANDItoCCR nat
- | ANDItoSR nat
- | ASL Size AddressingMode DataRegister
- | ASLW AddressingMode
- | ASR Size AddressingMode DataRegister
- | ASRW AddressingMode
- | Bcc Condition Size nat
- | BTST Size AddressingMode AddressingMode
- | BCHG Size AddressingMode AddressingMode
- | BCLR Size AddressingMode AddressingMode
- | BSET Size AddressingMode AddressingMode
- | BRA Size nat
- | BSR Size nat
- | CHK AddressingMode DataRegister
- | CLR Size AddressingMode
- | CMP Size AddressingMode DataRegister
- | CMPA Size AddressingMode AddressRegister
- | CMPI Size nat AddressingMode
- | CMPM Size AddressRegister AddressRegister
- | DBT DataRegister nat
- | DBF DataRegister nat
- | DBcc Condition DataRegister nat
- | DIVS AddressingMode DataRegister
- | DIVU AddressingMode DataRegister
- | EOR Size DataRegister AddressingMode
- | EORI Size nat AddressingMode
- | EORItoCCR nat
- | EORItoSR nat
- | EXG DataOrAddressRegister DataOrAddressRegister
- | EXT Size DataRegister
- | ILLEGAL
- | JMP AddressingMode
- | JSR AddressingMode
- | LEA AddressingMode AddressRegister
- | LINK AddressRegister nat
- | LSL Size AddressingMode DataRegister
- | LSLW AddressingMode
- | LSR Size AddressingMode DataRegister
- | LSRW AddressingMode
- | MOVE Size AddressingMode AddressingMode
- | MOVEtoCCR AddressingMode
- | MOVEtoSR AddressingMode
- | MOVEfromSR AddressingMode
- | MOVEtoUSP AddressingMode
- | MOVEfromUSP AddressingMode
- | MOVEA Size AddressingMode AddressRegister
- | MOVEMto Size AddressingMode "DataOrAddressRegister list"
- | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
- | MOVEP Size AddressingMode AddressingMode
- | MOVEQ nat DataRegister
- | MULS AddressingMode DataRegister
- | MULU AddressingMode DataRegister
- | NBCD AddressingMode
- | NEG Size AddressingMode
- | NEGX Size AddressingMode
- | NOP
- | NOT Size AddressingMode
- | OR Size AddressingMode AddressingMode
- | ORI Size nat AddressingMode
- | ORItoCCR nat
- | ORItoSR nat
- | PEA AddressingMode
- | RESET
- | ROL Size AddressingMode DataRegister
- | ROLW AddressingMode
- | ROR Size AddressingMode DataRegister
- | RORW AddressingMode
- | ROXL Size AddressingMode DataRegister
- | ROXLW AddressingMode
- | ROXR Size AddressingMode DataRegister
- | ROXRW AddressingMode
- | RTE
- | RTR
- | RTS
- | SBCD AddressingMode AddressingMode
- | ST AddressingMode
- | SF AddressingMode
- | Scc Condition AddressingMode
- | STOP nat
- | SUB Size AddressingMode AddressingMode
- | SUBA Size AddressingMode AddressingMode
- | SUBI Size nat AddressingMode
- | SUBQ Size nat AddressingMode
- | SUBX Size AddressingMode AddressingMode
- | SWAP DataRegister
- | TAS AddressingMode
- | TRAP nat
- | TRAPV
- | TST Size AddressingMode
- | UNLK AddressRegister
-
-end
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Wed Dec 14 10:18:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Admin/Benchmarks/HOL-datatype/ROOT.ML
-
-Some rather large datatype examples (from John Harrison).
-*)
-
-val tests = ["Brackin", "Instructions", "SML", "Verilog"];
-
-Toplevel.timing := true;
-
-warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
-use_thys tests;
-
-warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
-List.app Thy_Info.remove_thy tests;
-use_thys tests;
--- a/Admin/Benchmarks/HOL-datatype/SML.thy Wed Dec 14 10:18:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(* Title: Admin/Benchmarks/HOL-datatype/SML.thy
-
-Example from Myra: part of the syntax of SML.
-*)
-
-theory SML imports Main begin
-
-datatype
- string = EMPTY_STRING | CONS_STRING nat string
-
-datatype
- strid = STRID string
-
-datatype
- var = VAR string
-
-datatype
- con = CON string
-
-datatype
- scon = SCINT nat | SCSTR string
-
-datatype
- excon = EXCON string
-
-datatype
- label = LABEL string
-
-datatype
- 'a nonemptylist = Head_and_tail 'a "'a list"
-
-datatype
- 'a long = BASE 'a | QUALIFIED strid "'a long"
-
-datatype
- atpat_e = WILDCARDatpat_e
- | SCONatpat_e scon
- | VARatpat_e var
- | CONatpat_e "con long"
- | EXCONatpat_e "excon long"
- | RECORDatpat_e "patrow_e option"
- | PARatpat_e pat_e
-and
- patrow_e = DOTDOTDOT_e
- | PATROW_e label pat_e "patrow_e option"
-and
- pat_e = ATPATpat_e atpat_e
- | CONpat_e "con long" atpat_e
- | EXCONpat_e "excon long" atpat_e
- | LAYEREDpat_e var pat_e
-and
- conbind_e = CONBIND_e con "conbind_e option"
-and
- datbind_e = DATBIND_e conbind_e "datbind_e option"
-and
- exbind_e = EXBIND1_e excon "exbind_e option"
- | EXBIND2_e excon "excon long" "exbind_e option"
-and
- atexp_e = SCONatexp_e scon
- | VARatexp_e "var long"
- | CONatexp_e "con long"
- | EXCONatexp_e "excon long"
- | RECORDatexp_e "exprow_e option"
- | LETatexp_e dec_e exp_e
- | PARatexp_e exp_e
-and
- exprow_e = EXPROW_e label exp_e "exprow_e option"
-and
- exp_e = ATEXPexp_e atexp_e
- | APPexp_e exp_e atexp_e
- | HANDLEexp_e exp_e match_e
- | RAISEexp_e exp_e
- | FNexp_e match_e
-and
- match_e = MATCH_e mrule_e "match_e option"
-and
- mrule_e = MRULE_e pat_e exp_e
-and
- dec_e = VALdec_e valbind_e
- | DATATYPEdec_e datbind_e
- | ABSTYPEdec_e datbind_e dec_e
- | EXCEPTdec_e exbind_e
- | LOCALdec_e dec_e dec_e
- | OPENdec_e "strid long nonemptylist"
- | EMPTYdec_e
- | SEQdec_e dec_e dec_e
-and
- valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
- | RECvalbind_e valbind_e
-
-end
--- a/Admin/Benchmarks/HOL-datatype/Verilog.thy Wed Dec 14 10:18:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(* Title: Admin/Benchmarks/HOL-datatype/Verilog.thy
-
-Example from Daryl: a Verilog grammar.
-*)
-
-theory Verilog imports Main begin
-
-datatype
- Source_text
- = module string "string list" "Module_item list"
- | Source_textMeta string
-and
- Module_item
- = "declaration" Declaration
- | initial Statement
- | always Statement
- | assign Lvalue Expression
- | Module_itemMeta string
-and
- Declaration
- = reg_declaration "Range option" "string list"
- | net_declaration "Range option" "string list"
- | input_declaration "Range option" "string list"
- | output_declaration "Range option" "string list"
- | DeclarationMeta string
-and
- Range = range Expression Expression | RangeMeta string
-and
- Statement
- = clock_statement Clock Statement_or_null
- | blocking_assignment Lvalue Expression
- | non_blocking_assignment Lvalue Expression
- | conditional_statement
- Expression Statement_or_null "Statement_or_null option"
- | case_statement Expression "Case_item list"
- | while_loop Expression Statement
- | repeat_loop Expression Statement
- | for_loop
- Lvalue Expression Expression Lvalue Expression Statement
- | forever_loop Statement
- | disable string
- | seq_block "string option" "Statement list"
- | StatementMeta string
-and
- Statement_or_null
- = statement Statement | null_statement | Statement_or_nullMeta string
-and
- Clock
- = posedge string
- | negedge string
- | clock string
- | ClockMeta string
-and
- Case_item
- = case_item "Expression list" Statement_or_null
- | default_case_item Statement_or_null
- | Case_itemMeta string
-and
- Expression
- = plus Expression Expression
- | minus Expression Expression
- | lshift Expression Expression
- | rshift Expression Expression
- | lt Expression Expression
- | leq Expression Expression
- | gt Expression Expression
- | geq Expression Expression
- | logeq Expression Expression
- | logneq Expression Expression
- | caseeq Expression Expression
- | caseneq Expression Expression
- | bitand Expression Expression
- | bitxor Expression Expression
- | bitor Expression Expression
- | logand Expression Expression
- | logor Expression Expression
- | conditional Expression Expression Expression
- | positive Primary
- | negative Primary
- | lognot Primary
- | bitnot Primary
- | reducand Primary
- | reducxor Primary
- | reducor Primary
- | reducnand Primary
- | reducxnor Primary
- | reducnor Primary
- | primary Primary
- | ExpressionMeta string
-and
- Primary
- = primary_number Number
- | primary_IDENTIFIER string
- | primary_bit_select string Expression
- | primary_part_select string Expression Expression
- | primary_gen_bit_select Expression Expression
- | primary_gen_part_select Expression Expression Expression
- | primary_concatenation Concatenation
- | primary_multiple_concatenation Multiple_concatenation
- | brackets Expression
- | PrimaryMeta string
-and
- Lvalue
- = lvalue string
- | lvalue_bit_select string Expression
- | lvalue_part_select string Expression Expression
- | lvalue_concatenation Concatenation
- | LvalueMeta string
-and
- Number
- = decimal string
- | based "string option" string
- | NumberMeta string
-and
- Concatenation
- = concatenation "Expression list" | ConcatenationMeta string
-and
- Multiple_concatenation
- = multiple_concatenation Expression "Expression list"
- | Multiple_concatenationMeta string
-and
- meta
- = Meta_Source_text Source_text
- | Meta_Module_item Module_item
- | Meta_Declaration Declaration
- | Meta_Range Range
- | Meta_Statement Statement
- | Meta_Statement_or_null Statement_or_null
- | Meta_Clock Clock
- | Meta_Case_item Case_item
- | Meta_Expression Expression
- | Meta_Primary Primary
- | Meta_Lvalue Lvalue
- | Meta_Number Number
- | Meta_Concatenation Concatenation
- | Meta_Multiple_concatenation Multiple_concatenation
-
-end
--- a/Admin/Benchmarks/HOL-record/ROOT.ML Wed Dec 14 10:18:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Title: Admin/Benchmarks/HOL-record/ROOT.ML
-
-Some benchmark on large record.
-*)
-
-val tests = ["Record_Benchmark"];
-
-Toplevel.timing := true;
-
-warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
-use_thys tests;
-
-warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
-use_thys tests;
--- a/Admin/Benchmarks/HOL-record/Record_Benchmark.thy Wed Dec 14 10:18:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,390 +0,0 @@
-(* Title: Admin/Benchmarks/HOL-record/Record_Benchmark.thy
- Author: Norbert Schirmer, DFKI
-*)
-
-header {* Benchmark for large record *}
-
-theory Record_Benchmark
-imports Main
-begin
-
-declare [[record_timing]]
-
-record many_A =
-A000::nat
-A001::nat
-A002::nat
-A003::nat
-A004::nat
-A005::nat
-A006::nat
-A007::nat
-A008::nat
-A009::nat
-A010::nat
-A011::nat
-A012::nat
-A013::nat
-A014::nat
-A015::nat
-A016::nat
-A017::nat
-A018::nat
-A019::nat
-A020::nat
-A021::nat
-A022::nat
-A023::nat
-A024::nat
-A025::nat
-A026::nat
-A027::nat
-A028::nat
-A029::nat
-A030::nat
-A031::nat
-A032::nat
-A033::nat
-A034::nat
-A035::nat
-A036::nat
-A037::nat
-A038::nat
-A039::nat
-A040::nat
-A041::nat
-A042::nat
-A043::nat
-A044::nat
-A045::nat
-A046::nat
-A047::nat
-A048::nat
-A049::nat
-A050::nat
-A051::nat
-A052::nat
-A053::nat
-A054::nat
-A055::nat
-A056::nat
-A057::nat
-A058::nat
-A059::nat
-A060::nat
-A061::nat
-A062::nat
-A063::nat
-A064::nat
-A065::nat
-A066::nat
-A067::nat
-A068::nat
-A069::nat
-A070::nat
-A071::nat
-A072::nat
-A073::nat
-A074::nat
-A075::nat
-A076::nat
-A077::nat
-A078::nat
-A079::nat
-A080::nat
-A081::nat
-A082::nat
-A083::nat
-A084::nat
-A085::nat
-A086::nat
-A087::nat
-A088::nat
-A089::nat
-A090::nat
-A091::nat
-A092::nat
-A093::nat
-A094::nat
-A095::nat
-A096::nat
-A097::nat
-A098::nat
-A099::nat
-A100::nat
-A101::nat
-A102::nat
-A103::nat
-A104::nat
-A105::nat
-A106::nat
-A107::nat
-A108::nat
-A109::nat
-A110::nat
-A111::nat
-A112::nat
-A113::nat
-A114::nat
-A115::nat
-A116::nat
-A117::nat
-A118::nat
-A119::nat
-A120::nat
-A121::nat
-A122::nat
-A123::nat
-A124::nat
-A125::nat
-A126::nat
-A127::nat
-A128::nat
-A129::nat
-A130::nat
-A131::nat
-A132::nat
-A133::nat
-A134::nat
-A135::nat
-A136::nat
-A137::nat
-A138::nat
-A139::nat
-A140::nat
-A141::nat
-A142::nat
-A143::nat
-A144::nat
-A145::nat
-A146::nat
-A147::nat
-A148::nat
-A149::nat
-A150::nat
-A151::nat
-A152::nat
-A153::nat
-A154::nat
-A155::nat
-A156::nat
-A157::nat
-A158::nat
-A159::nat
-A160::nat
-A161::nat
-A162::nat
-A163::nat
-A164::nat
-A165::nat
-A166::nat
-A167::nat
-A168::nat
-A169::nat
-A170::nat
-A171::nat
-A172::nat
-A173::nat
-A174::nat
-A175::nat
-A176::nat
-A177::nat
-A178::nat
-A179::nat
-A180::nat
-A181::nat
-A182::nat
-A183::nat
-A184::nat
-A185::nat
-A186::nat
-A187::nat
-A188::nat
-A189::nat
-A190::nat
-A191::nat
-A192::nat
-A193::nat
-A194::nat
-A195::nat
-A196::nat
-A197::nat
-A198::nat
-A199::nat
-A200::nat
-A201::nat
-A202::nat
-A203::nat
-A204::nat
-A205::nat
-A206::nat
-A207::nat
-A208::nat
-A209::nat
-A210::nat
-A211::nat
-A212::nat
-A213::nat
-A214::nat
-A215::nat
-A216::nat
-A217::nat
-A218::nat
-A219::nat
-A220::nat
-A221::nat
-A222::nat
-A223::nat
-A224::nat
-A225::nat
-A226::nat
-A227::nat
-A228::nat
-A229::nat
-A230::nat
-A231::nat
-A232::nat
-A233::nat
-A234::nat
-A235::nat
-A236::nat
-A237::nat
-A238::nat
-A239::nat
-A240::nat
-A241::nat
-A242::nat
-A243::nat
-A244::nat
-A245::nat
-A246::nat
-A247::nat
-A248::nat
-A249::nat
-A250::nat
-A251::nat
-A252::nat
-A253::nat
-A254::nat
-A255::nat
-A256::nat
-A257::nat
-A258::nat
-A259::nat
-A260::nat
-A261::nat
-A262::nat
-A263::nat
-A264::nat
-A265::nat
-A266::nat
-A267::nat
-A268::nat
-A269::nat
-A270::nat
-A271::nat
-A272::nat
-A273::nat
-A274::nat
-A275::nat
-A276::nat
-A277::nat
-A278::nat
-A279::nat
-A280::nat
-A281::nat
-A282::nat
-A283::nat
-A284::nat
-A285::nat
-A286::nat
-A287::nat
-A288::nat
-A289::nat
-A290::nat
-A291::nat
-A292::nat
-A293::nat
-A294::nat
-A295::nat
-A296::nat
-A297::nat
-A298::nat
-A299::nat
-
-lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
- by simp
-
-lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
- by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
- by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
- apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
- done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
- apply simp
- done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
- apply simp
- done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
- apply simp
- done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
- apply simp
- done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
- apply auto
- done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
- apply auto
- done
-
-lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
- apply auto
- done
-
-lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
- apply auto
- done
-
-
-lemma True
-proof -
- {
- fix P r
- assume pre: "P (A155 r)"
- have "\<exists>x. P x"
- using pre
- apply -
- apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
- apply auto
- done
- }
- show ?thesis ..
-qed
-
-
-lemma "\<exists>r. A155 r = x"
- apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
- done
-
-
-end
\ No newline at end of file
--- a/Admin/Benchmarks/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-
-## targets
-
-default: all
-images:
-test: HOL-datatype HOL-record
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-
-
-## HOL-datatype
-
-HOL:
- @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
-
-
-HOL-datatype: HOL $(LOG)/HOL-datatype.gz
-
-$(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/ROOT.ML \
- HOL-datatype/Brackin.thy HOL-datatype/Instructions.thy \
- HOL-datatype/SML.thy HOL-datatype/Verilog.thy
- @$(ISABELLE_TOOL) usedir -s datatype $(OUT)/HOL HOL-datatype
-
-
-## HOL-record
-
-HOL-record: HOL $(LOG)/HOL-record.gz
-
-$(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML \
- HOL-record/Record_Benchmark.thy
- @$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record
-
-
-## clean
-
-clean:
- @rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz
--- a/src/CCL/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/CCL/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -8,6 +8,7 @@
images: CCL
test: CCL-ex
all: images test
+full: all
smlnj: all
--- a/src/CTT/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/CTT/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -8,6 +8,7 @@
images: CTT
test: CTT-ex
all: images test
+full: all
smlnj: all
--- a/src/Cube/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/Cube/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -8,6 +8,7 @@
images:
test: Pure-Cube
all: images test
+full: all
smlnj: all
--- a/src/FOL/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/FOL/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -8,6 +8,7 @@
images: FOL
test: FOL-ex
all: images test
+full: all
smlnj: all
--- a/src/FOLP/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/FOLP/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -8,6 +8,7 @@
images: FOLP
test: FOLP-ex
all: images test
+full: all
smlnj: all
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/Brackin.thy Wed Dec 14 12:02:02 2011 +0100
@@ -0,0 +1,43 @@
+(* Title: HOL/Datatype_Benchmark/Brackin.thy
+
+A couple from Steve Brackin's work.
+*)
+
+theory Brackin imports Main begin
+
+datatype T = X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
+ X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
+ X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
+ X32 | X33 | X34
+
+datatype
+ ('a, 'b, 'c) TY1 =
+ NoF__
+ | Fk__ 'a "('a, 'b, 'c) TY2"
+and
+ ('a, 'b, 'c) TY2 =
+ Ta__ bool
+ | Td__ bool
+ | Tf__ "('a, 'b, 'c) TY1"
+ | Tk__ bool
+ | Tp__ bool
+ | App__ 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
+ | Pair__ "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
+and
+ ('a, 'b, 'c) TY3 =
+ NoS__
+ | Fresh__ "('a, 'b, 'c) TY2"
+ | Trustworthy__ 'a
+ | PrivateKey__ 'a 'b 'c
+ | PublicKey__ 'a 'b 'c
+ | Conveyed__ 'a "('a, 'b, 'c) TY2"
+ | Possesses__ 'a "('a, 'b, 'c) TY2"
+ | Received__ 'a "('a, 'b, 'c) TY2"
+ | Recognizes__ 'a "('a, 'b, 'c) TY2"
+ | NeverMalFromSelf__ 'a 'b "('a, 'b, 'c) TY2"
+ | Sends__ 'a "('a, 'b, 'c) TY2" 'b
+ | SharedSecret__ 'a "('a, 'b, 'c) TY2" 'b
+ | Believes__ 'a "('a, 'b, 'c) TY3"
+ | And__ "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/Instructions.thy Wed Dec 14 12:02:02 2011 +0100
@@ -0,0 +1,162 @@
+(* Title: HOL/Datatype_Benchmark/Instructions.thy
+
+Example from Konrad: 68000 instruction set.
+*)
+
+theory Instructions imports Main begin
+
+datatype Size = Byte | Word | Long
+
+datatype DataRegister
+ = RegD0
+ | RegD1
+ | RegD2
+ | RegD3
+ | RegD4
+ | RegD5
+ | RegD6
+ | RegD7
+
+datatype AddressRegister
+ = RegA0
+ | RegA1
+ | RegA2
+ | RegA3
+ | RegA4
+ | RegA5
+ | RegA6
+ | RegA7
+
+datatype DataOrAddressRegister
+ = data DataRegister
+ | address AddressRegister
+
+datatype Condition
+ = Hi
+ | Ls
+ | Cc
+ | Cs
+ | Ne
+ | Eq
+ | Vc
+ | Vs
+ | Pl
+ | Mi
+ | Ge
+ | Lt
+ | Gt
+ | Le
+
+datatype AddressingMode
+ = immediate nat
+ | direct DataOrAddressRegister
+ | indirect AddressRegister
+ | postinc AddressRegister
+ | predec AddressRegister
+ | indirectdisp nat AddressRegister
+ | indirectindex nat AddressRegister DataOrAddressRegister Size
+ | absolute nat
+ | pcdisp nat
+ | pcindex nat DataOrAddressRegister Size
+
+datatype M68kInstruction
+ = ABCD AddressingMode AddressingMode
+ | ADD Size AddressingMode AddressingMode
+ | ADDA Size AddressingMode AddressRegister
+ | ADDI Size nat AddressingMode
+ | ADDQ Size nat AddressingMode
+ | ADDX Size AddressingMode AddressingMode
+ | AND Size AddressingMode AddressingMode
+ | ANDI Size nat AddressingMode
+ | ANDItoCCR nat
+ | ANDItoSR nat
+ | ASL Size AddressingMode DataRegister
+ | ASLW AddressingMode
+ | ASR Size AddressingMode DataRegister
+ | ASRW AddressingMode
+ | Bcc Condition Size nat
+ | BTST Size AddressingMode AddressingMode
+ | BCHG Size AddressingMode AddressingMode
+ | BCLR Size AddressingMode AddressingMode
+ | BSET Size AddressingMode AddressingMode
+ | BRA Size nat
+ | BSR Size nat
+ | CHK AddressingMode DataRegister
+ | CLR Size AddressingMode
+ | CMP Size AddressingMode DataRegister
+ | CMPA Size AddressingMode AddressRegister
+ | CMPI Size nat AddressingMode
+ | CMPM Size AddressRegister AddressRegister
+ | DBT DataRegister nat
+ | DBF DataRegister nat
+ | DBcc Condition DataRegister nat
+ | DIVS AddressingMode DataRegister
+ | DIVU AddressingMode DataRegister
+ | EOR Size DataRegister AddressingMode
+ | EORI Size nat AddressingMode
+ | EORItoCCR nat
+ | EORItoSR nat
+ | EXG DataOrAddressRegister DataOrAddressRegister
+ | EXT Size DataRegister
+ | ILLEGAL
+ | JMP AddressingMode
+ | JSR AddressingMode
+ | LEA AddressingMode AddressRegister
+ | LINK AddressRegister nat
+ | LSL Size AddressingMode DataRegister
+ | LSLW AddressingMode
+ | LSR Size AddressingMode DataRegister
+ | LSRW AddressingMode
+ | MOVE Size AddressingMode AddressingMode
+ | MOVEtoCCR AddressingMode
+ | MOVEtoSR AddressingMode
+ | MOVEfromSR AddressingMode
+ | MOVEtoUSP AddressingMode
+ | MOVEfromUSP AddressingMode
+ | MOVEA Size AddressingMode AddressRegister
+ | MOVEMto Size AddressingMode "DataOrAddressRegister list"
+ | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
+ | MOVEP Size AddressingMode AddressingMode
+ | MOVEQ nat DataRegister
+ | MULS AddressingMode DataRegister
+ | MULU AddressingMode DataRegister
+ | NBCD AddressingMode
+ | NEG Size AddressingMode
+ | NEGX Size AddressingMode
+ | NOP
+ | NOT Size AddressingMode
+ | OR Size AddressingMode AddressingMode
+ | ORI Size nat AddressingMode
+ | ORItoCCR nat
+ | ORItoSR nat
+ | PEA AddressingMode
+ | RESET
+ | ROL Size AddressingMode DataRegister
+ | ROLW AddressingMode
+ | ROR Size AddressingMode DataRegister
+ | RORW AddressingMode
+ | ROXL Size AddressingMode DataRegister
+ | ROXLW AddressingMode
+ | ROXR Size AddressingMode DataRegister
+ | ROXRW AddressingMode
+ | RTE
+ | RTR
+ | RTS
+ | SBCD AddressingMode AddressingMode
+ | ST AddressingMode
+ | SF AddressingMode
+ | Scc Condition AddressingMode
+ | STOP nat
+ | SUB Size AddressingMode AddressingMode
+ | SUBA Size AddressingMode AddressingMode
+ | SUBI Size nat AddressingMode
+ | SUBQ Size nat AddressingMode
+ | SUBX Size AddressingMode AddressingMode
+ | SWAP DataRegister
+ | TAS AddressingMode
+ | TRAP nat
+ | TRAPV
+ | TST Size AddressingMode
+ | UNLK AddressRegister
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/ROOT.ML Wed Dec 14 12:02:02 2011 +0100
@@ -0,0 +1,8 @@
+(* Title: HOL/Datatype_Benchmark/ROOT.ML
+
+Some rather large datatype examples (from John Harrison).
+*)
+
+Toplevel.timing := true;
+
+use_thys ["Brackin", "Instructions", "SML", "Verilog"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/SML.thy Wed Dec 14 12:02:02 2011 +0100
@@ -0,0 +1,91 @@
+(* Title: HOL/Datatype_Benchmark/SML.thy
+
+Example from Myra: part of the syntax of SML.
+*)
+
+theory SML imports Main begin
+
+datatype
+ string = EMPTY_STRING | CONS_STRING nat string
+
+datatype
+ strid = STRID string
+
+datatype
+ var = VAR string
+
+datatype
+ con = CON string
+
+datatype
+ scon = SCINT nat | SCSTR string
+
+datatype
+ excon = EXCON string
+
+datatype
+ label = LABEL string
+
+datatype
+ 'a nonemptylist = Head_and_tail 'a "'a list"
+
+datatype
+ 'a long = BASE 'a | QUALIFIED strid "'a long"
+
+datatype
+ atpat_e = WILDCARDatpat_e
+ | SCONatpat_e scon
+ | VARatpat_e var
+ | CONatpat_e "con long"
+ | EXCONatpat_e "excon long"
+ | RECORDatpat_e "patrow_e option"
+ | PARatpat_e pat_e
+and
+ patrow_e = DOTDOTDOT_e
+ | PATROW_e label pat_e "patrow_e option"
+and
+ pat_e = ATPATpat_e atpat_e
+ | CONpat_e "con long" atpat_e
+ | EXCONpat_e "excon long" atpat_e
+ | LAYEREDpat_e var pat_e
+and
+ conbind_e = CONBIND_e con "conbind_e option"
+and
+ datbind_e = DATBIND_e conbind_e "datbind_e option"
+and
+ exbind_e = EXBIND1_e excon "exbind_e option"
+ | EXBIND2_e excon "excon long" "exbind_e option"
+and
+ atexp_e = SCONatexp_e scon
+ | VARatexp_e "var long"
+ | CONatexp_e "con long"
+ | EXCONatexp_e "excon long"
+ | RECORDatexp_e "exprow_e option"
+ | LETatexp_e dec_e exp_e
+ | PARatexp_e exp_e
+and
+ exprow_e = EXPROW_e label exp_e "exprow_e option"
+and
+ exp_e = ATEXPexp_e atexp_e
+ | APPexp_e exp_e atexp_e
+ | HANDLEexp_e exp_e match_e
+ | RAISEexp_e exp_e
+ | FNexp_e match_e
+and
+ match_e = MATCH_e mrule_e "match_e option"
+and
+ mrule_e = MRULE_e pat_e exp_e
+and
+ dec_e = VALdec_e valbind_e
+ | DATATYPEdec_e datbind_e
+ | ABSTYPEdec_e datbind_e dec_e
+ | EXCEPTdec_e exbind_e
+ | LOCALdec_e dec_e dec_e
+ | OPENdec_e "strid long nonemptylist"
+ | EMPTYdec_e
+ | SEQdec_e dec_e dec_e
+and
+ valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
+ | RECvalbind_e valbind_e
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Benchmark/Verilog.thy Wed Dec 14 12:02:02 2011 +0100
@@ -0,0 +1,138 @@
+(* Title: HOL/Datatype_Benchmark/Verilog.thy
+
+Example from Daryl: a Verilog grammar.
+*)
+
+theory Verilog imports Main begin
+
+datatype
+ Source_text
+ = module string "string list" "Module_item list"
+ | Source_textMeta string
+and
+ Module_item
+ = "declaration" Declaration
+ | initial Statement
+ | always Statement
+ | assign Lvalue Expression
+ | Module_itemMeta string
+and
+ Declaration
+ = reg_declaration "Range option" "string list"
+ | net_declaration "Range option" "string list"
+ | input_declaration "Range option" "string list"
+ | output_declaration "Range option" "string list"
+ | DeclarationMeta string
+and
+ Range = range Expression Expression | RangeMeta string
+and
+ Statement
+ = clock_statement Clock Statement_or_null
+ | blocking_assignment Lvalue Expression
+ | non_blocking_assignment Lvalue Expression
+ | conditional_statement
+ Expression Statement_or_null "Statement_or_null option"
+ | case_statement Expression "Case_item list"
+ | while_loop Expression Statement
+ | repeat_loop Expression Statement
+ | for_loop
+ Lvalue Expression Expression Lvalue Expression Statement
+ | forever_loop Statement
+ | disable string
+ | seq_block "string option" "Statement list"
+ | StatementMeta string
+and
+ Statement_or_null
+ = statement Statement | null_statement | Statement_or_nullMeta string
+and
+ Clock
+ = posedge string
+ | negedge string
+ | clock string
+ | ClockMeta string
+and
+ Case_item
+ = case_item "Expression list" Statement_or_null
+ | default_case_item Statement_or_null
+ | Case_itemMeta string
+and
+ Expression
+ = plus Expression Expression
+ | minus Expression Expression
+ | lshift Expression Expression
+ | rshift Expression Expression
+ | lt Expression Expression
+ | leq Expression Expression
+ | gt Expression Expression
+ | geq Expression Expression
+ | logeq Expression Expression
+ | logneq Expression Expression
+ | caseeq Expression Expression
+ | caseneq Expression Expression
+ | bitand Expression Expression
+ | bitxor Expression Expression
+ | bitor Expression Expression
+ | logand Expression Expression
+ | logor Expression Expression
+ | conditional Expression Expression Expression
+ | positive Primary
+ | negative Primary
+ | lognot Primary
+ | bitnot Primary
+ | reducand Primary
+ | reducxor Primary
+ | reducor Primary
+ | reducnand Primary
+ | reducxnor Primary
+ | reducnor Primary
+ | primary Primary
+ | ExpressionMeta string
+and
+ Primary
+ = primary_number Number
+ | primary_IDENTIFIER string
+ | primary_bit_select string Expression
+ | primary_part_select string Expression Expression
+ | primary_gen_bit_select Expression Expression
+ | primary_gen_part_select Expression Expression Expression
+ | primary_concatenation Concatenation
+ | primary_multiple_concatenation Multiple_concatenation
+ | brackets Expression
+ | PrimaryMeta string
+and
+ Lvalue
+ = lvalue string
+ | lvalue_bit_select string Expression
+ | lvalue_part_select string Expression Expression
+ | lvalue_concatenation Concatenation
+ | LvalueMeta string
+and
+ Number
+ = decimal string
+ | based "string option" string
+ | NumberMeta string
+and
+ Concatenation
+ = concatenation "Expression list" | ConcatenationMeta string
+and
+ Multiple_concatenation
+ = multiple_concatenation Expression "Expression list"
+ | Multiple_concatenationMeta string
+and
+ meta
+ = Meta_Source_text Source_text
+ | Meta_Module_item Module_item
+ | Meta_Declaration Declaration
+ | Meta_Range Range
+ | Meta_Statement Statement
+ | Meta_Statement_or_null Statement_or_null
+ | Meta_Clock Clock
+ | Meta_Case_item Case_item
+ | Meta_Expression Expression
+ | Meta_Primary Primary
+ | Meta_Lvalue Lvalue
+ | Meta_Number Number
+ | Meta_Concatenation Concatenation
+ | Meta_Multiple_concatenation Multiple_concatenation
+
+end
--- a/src/HOL/HOLCF/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/HOL/HOLCF/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -17,6 +17,7 @@
IOA-Storage \
IOA-ex
all: images test
+full: all
## global settings
--- a/src/HOL/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/HOL/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -81,6 +81,10 @@
HOL-ZF
# ^ this is the sort position
+benchmark: \
+ HOL-Datatype_Benchmark \
+ HOL-Record_Benchmark
+
images-no-smlnj: \
HOL-Probability
@@ -91,8 +95,10 @@
HOL-Nominal-Examples
all: test-no-smlnj test images-no-smlnj images
+full: all benchmark
smlnj: test images
+
## global settings
SRC = $(ISABELLE_HOME)/src
@@ -1772,6 +1778,28 @@
@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
+
+## HOL-Datatype_Benchmark
+
+HOL-Datatype_Benchmark: HOL $(LOG)/HOL-Datatype_Benchmark.gz
+
+$(LOG)/HOL-Datatype_Benchmark.gz: $(OUT)/HOL \
+ Datatype_Benchmark/ROOT.ML Datatype_Benchmark/Brackin.thy \
+ Datatype_Benchmark/Instructions.thy Datatype_Benchmark/SML.thy \
+ Datatype_Benchmark/Verilog.thy
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Datatype_Benchmark
+
+
+## HOL-Record_Benchmark
+
+HOL-Record_Benchmark: HOL $(LOG)/HOL-Record_Benchmark.gz
+
+$(LOG)/HOL-Record_Benchmark.gz: $(OUT)/HOL Record_Benchmark/ROOT.ML \
+ Record_Benchmark/Record_Benchmark.thy
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Record_Benchmark
+
+
+
## clean
clean:
@@ -1799,23 +1827,25 @@
$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz \
$(LOG)/HOL-Proofs-Extraction.gz \
$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
- $(LOG)/HOL-Word-SMT_Examples.gz \
- $(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz \
- $(LOG)/HOL-SPARK-Manual.gz \
- $(LOG)/HOL-Statespace.gz \
+ $(LOG)/HOL-Word-SMT_Examples.gz $(LOG)/HOL-SPARK.gz \
+ $(LOG)/HOL-SPARK-Examples.gz \
+ $(LOG)/HOL-SPARK-Manual.gz $(LOG)/HOL-Statespace.gz \
$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \
$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \
$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \
$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \
$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \
- $(OUT)/HOL-IMP $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \
- $(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \
+ $(OUT)/HOL-IMP $(OUT)/HOL-Main \
+ $(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA \
+ $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \
$(OUT)/HOL-Probability $(OUT)/HOL-Proofs \
- $(OUT)/HOL-SPARK \
- $(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA \
- $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
- $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \
- $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
+ $(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/HOL4 \
+ $(OUT)/TLA $(OUT)/HOLCF $(LOG)/HOLCF.gz \
+ $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz \
+ $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA $(LOG)/IOA.gz \
+ $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \
- $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz
+ $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz \
+ $(LOG)/HOL-Datatype_Benchmark.gz \
+ $(LOG)/HOL-Record_Benchmark.gz
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Record_Benchmark/ROOT.ML Wed Dec 14 12:02:02 2011 +0100
@@ -0,0 +1,8 @@
+(* Title: HOL/Record_Benchmark/ROOT.ML
+
+Some benchmark on large record.
+*)
+
+Toplevel.timing := true;
+
+use_thys ["Record_Benchmark"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Record_Benchmark/Record_Benchmark.thy Wed Dec 14 12:02:02 2011 +0100
@@ -0,0 +1,390 @@
+(* Title: HOL/Record_Benchmark/Record_Benchmark.thy
+ Author: Norbert Schirmer, DFKI
+*)
+
+header {* Benchmark for large record *}
+
+theory Record_Benchmark
+imports Main
+begin
+
+declare [[record_timing]]
+
+record many_A =
+A000::nat
+A001::nat
+A002::nat
+A003::nat
+A004::nat
+A005::nat
+A006::nat
+A007::nat
+A008::nat
+A009::nat
+A010::nat
+A011::nat
+A012::nat
+A013::nat
+A014::nat
+A015::nat
+A016::nat
+A017::nat
+A018::nat
+A019::nat
+A020::nat
+A021::nat
+A022::nat
+A023::nat
+A024::nat
+A025::nat
+A026::nat
+A027::nat
+A028::nat
+A029::nat
+A030::nat
+A031::nat
+A032::nat
+A033::nat
+A034::nat
+A035::nat
+A036::nat
+A037::nat
+A038::nat
+A039::nat
+A040::nat
+A041::nat
+A042::nat
+A043::nat
+A044::nat
+A045::nat
+A046::nat
+A047::nat
+A048::nat
+A049::nat
+A050::nat
+A051::nat
+A052::nat
+A053::nat
+A054::nat
+A055::nat
+A056::nat
+A057::nat
+A058::nat
+A059::nat
+A060::nat
+A061::nat
+A062::nat
+A063::nat
+A064::nat
+A065::nat
+A066::nat
+A067::nat
+A068::nat
+A069::nat
+A070::nat
+A071::nat
+A072::nat
+A073::nat
+A074::nat
+A075::nat
+A076::nat
+A077::nat
+A078::nat
+A079::nat
+A080::nat
+A081::nat
+A082::nat
+A083::nat
+A084::nat
+A085::nat
+A086::nat
+A087::nat
+A088::nat
+A089::nat
+A090::nat
+A091::nat
+A092::nat
+A093::nat
+A094::nat
+A095::nat
+A096::nat
+A097::nat
+A098::nat
+A099::nat
+A100::nat
+A101::nat
+A102::nat
+A103::nat
+A104::nat
+A105::nat
+A106::nat
+A107::nat
+A108::nat
+A109::nat
+A110::nat
+A111::nat
+A112::nat
+A113::nat
+A114::nat
+A115::nat
+A116::nat
+A117::nat
+A118::nat
+A119::nat
+A120::nat
+A121::nat
+A122::nat
+A123::nat
+A124::nat
+A125::nat
+A126::nat
+A127::nat
+A128::nat
+A129::nat
+A130::nat
+A131::nat
+A132::nat
+A133::nat
+A134::nat
+A135::nat
+A136::nat
+A137::nat
+A138::nat
+A139::nat
+A140::nat
+A141::nat
+A142::nat
+A143::nat
+A144::nat
+A145::nat
+A146::nat
+A147::nat
+A148::nat
+A149::nat
+A150::nat
+A151::nat
+A152::nat
+A153::nat
+A154::nat
+A155::nat
+A156::nat
+A157::nat
+A158::nat
+A159::nat
+A160::nat
+A161::nat
+A162::nat
+A163::nat
+A164::nat
+A165::nat
+A166::nat
+A167::nat
+A168::nat
+A169::nat
+A170::nat
+A171::nat
+A172::nat
+A173::nat
+A174::nat
+A175::nat
+A176::nat
+A177::nat
+A178::nat
+A179::nat
+A180::nat
+A181::nat
+A182::nat
+A183::nat
+A184::nat
+A185::nat
+A186::nat
+A187::nat
+A188::nat
+A189::nat
+A190::nat
+A191::nat
+A192::nat
+A193::nat
+A194::nat
+A195::nat
+A196::nat
+A197::nat
+A198::nat
+A199::nat
+A200::nat
+A201::nat
+A202::nat
+A203::nat
+A204::nat
+A205::nat
+A206::nat
+A207::nat
+A208::nat
+A209::nat
+A210::nat
+A211::nat
+A212::nat
+A213::nat
+A214::nat
+A215::nat
+A216::nat
+A217::nat
+A218::nat
+A219::nat
+A220::nat
+A221::nat
+A222::nat
+A223::nat
+A224::nat
+A225::nat
+A226::nat
+A227::nat
+A228::nat
+A229::nat
+A230::nat
+A231::nat
+A232::nat
+A233::nat
+A234::nat
+A235::nat
+A236::nat
+A237::nat
+A238::nat
+A239::nat
+A240::nat
+A241::nat
+A242::nat
+A243::nat
+A244::nat
+A245::nat
+A246::nat
+A247::nat
+A248::nat
+A249::nat
+A250::nat
+A251::nat
+A252::nat
+A253::nat
+A254::nat
+A255::nat
+A256::nat
+A257::nat
+A258::nat
+A259::nat
+A260::nat
+A261::nat
+A262::nat
+A263::nat
+A264::nat
+A265::nat
+A266::nat
+A267::nat
+A268::nat
+A269::nat
+A270::nat
+A271::nat
+A272::nat
+A273::nat
+A274::nat
+A275::nat
+A276::nat
+A277::nat
+A278::nat
+A279::nat
+A280::nat
+A281::nat
+A282::nat
+A283::nat
+A284::nat
+A285::nat
+A286::nat
+A287::nat
+A288::nat
+A289::nat
+A290::nat
+A291::nat
+A292::nat
+A293::nat
+A294::nat
+A295::nat
+A296::nat
+A297::nat
+A298::nat
+A299::nat
+
+lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
+ by simp
+
+lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
+ by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+ by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
+ done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply simp
+ done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply simp
+ done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply simp
+ done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply simp
+ done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply auto
+ done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+
+lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+
+lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+
+
+lemma True
+proof -
+ {
+ fix P r
+ assume pre: "P (A155 r)"
+ have "\<exists>x. P x"
+ using pre
+ apply -
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+ }
+ show ?thesis ..
+qed
+
+
+lemma "\<exists>r. A155 r = x"
+ apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
+ done
+
+
+end
\ No newline at end of file
--- a/src/LCF/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/LCF/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -8,6 +8,7 @@
images: LCF
test: LCF-ex
all: images test
+full: all
smlnj: all
--- a/src/Pure/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/Pure/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -8,6 +8,7 @@
images: Pure
test: RAW
all: images test
+full: all
smlnj: all
--- a/src/Sequents/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/Sequents/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -8,6 +8,7 @@
images: Sequents
test: Sequents-LK
all: images test
+full: all
smlnj: all
--- a/src/Tools/WWW_Find/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/Tools/WWW_Find/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -9,6 +9,7 @@
images:
test: Pure-WWW_Find
all: images test
+full: all
smlnj: all
--- a/src/ZF/IsaMakefile Wed Dec 14 10:18:28 2011 +0100
+++ b/src/ZF/IsaMakefile Wed Dec 14 12:02:02 2011 +0100
@@ -10,6 +10,7 @@
#Note: keep targets sorted
test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
all: images test
+full: all
smlnj: all