# HG changeset patch # User schirmer # Date 1258286802 -3600 # Node ID f06fe9c2152ddd7256e2f185d82b9ed74bc2f0aa # Parent 9d76c8080aea772f2ccab6f952387d600431b5a0# Parent 889d06128608945fc225c5b48902c7d611f669c6 merged diff -r 889d06128608 -r f06fe9c2152d Admin/Benchmarks/HOL-record/IsaMakefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Benchmarks/HOL-record/IsaMakefile Sun Nov 15 13:06:42 2009 +0100 @@ -0,0 +1,34 @@ +# +# $Id$ +# + +## targets + +default: HOL-record +images: +test: HOL-record +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src +OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + + +## HOL-record + +HOL: + @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL + +HOL-record: HOL $(LOG)/HOL-record.gz + +$(LOG)/HOL-record.gz: RecordBenchmark.thy + @cd ..; $(ISABELLE_TOOL) usedir -s HOL-record $(OUT)/HOL HOL-record + + +## clean + +clean: + @rm -f $(LOG)/HOL-record.gz diff -r 889d06128608 -r f06fe9c2152d Admin/Benchmarks/HOL-record/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Benchmarks/HOL-record/ROOT.ML Sun Nov 15 13:06:42 2009 +0100 @@ -0,0 +1,14 @@ +(* Title: Admin/Benchmarks/HOL-record/ROOT.ML + +Some benchmark on large record +*) + +val tests = ["RecordBenchmark"]; + +Unsynchronized.set timing; + +warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty; +List.app time_use_thy tests; + +warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty; +List.app time_use_thy tests; diff -r 889d06128608 -r f06fe9c2152d Admin/Benchmarks/HOL-record/RecordBenchmark.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Benchmarks/HOL-record/RecordBenchmark.thy Sun Nov 15 13:06:42 2009 +0100 @@ -0,0 +1,397 @@ +(* Title: Admin/Benchmarks/HOL-record/RecordBenchmark.thy + Author: Norbert Schirmer + DFKI +*) + +header {* Benchmark for large record *} + +theory RecordBenchmark +imports Main +begin + +ML {* Unsynchronized.set 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\A255:=x\) = A155 r" +by simp + +lemma "A155 (r\A255:=x,A253:=y,A255:=z \) = A155 r" +by simp + +lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" +by simp + +lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" +apply (tactic {* simp_tac + (HOL_basic_ss addsimprocs [Record.record_upd_simproc]) 1*}) +done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* simp_tac + (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* simp_tac + (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply simp + done + +lemma "\r. P (A155 r) \ (\x. P x)" + apply (tactic {* simp_tac + (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) + apply auto + done + +lemma "\r. P (A155 r) \ (\x. P x)" + apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply auto + done + +lemma "P (A155 r) \ (\x. P x)" + apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply auto + done + +lemma fixes r shows "P (A155 r) \ (\x. P x)" + apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply auto + done + + +lemma True +proof - + { + fix P r + assume pre: "P (A155 r)" + have "\x. P x" + using pre + apply - + apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) + apply auto + done + } + show ?thesis .. +qed + + +lemma "\r. A155 r = x" + apply (tactic {*simp_tac + (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*}) + done + + + +end \ No newline at end of file diff -r 889d06128608 -r f06fe9c2152d Admin/Benchmarks/IsaMakefile --- a/Admin/Benchmarks/IsaMakefile Sun Nov 15 00:34:21 2009 +0100 +++ b/Admin/Benchmarks/IsaMakefile Sun Nov 15 13:06:42 2009 +0100 @@ -6,7 +6,7 @@ default: HOL-datatype images: -test: HOL-datatype +test: HOL-datatype HOL-record all: images test @@ -29,8 +29,12 @@ HOL-datatype/Verilog.thy @$(ISABELLE_TOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype +HOL-record: HOL $(LOG)/HOL-record.gz + +$(LOG)/HOL-record.gz: HOL-record/RecordBenchmark.thy + @$(ISABELLE_TOOL) usedir -s HOL-record $(OUT)/HOL HOL-record ## clean clean: - @rm -f $(LOG)/HOL-datatype.gz + @rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz diff -r 889d06128608 -r f06fe9c2152d src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sun Nov 15 00:34:21 2009 +0100 +++ b/src/HOL/Tools/record.ML Sun Nov 15 13:06:42 2009 +0100 @@ -1008,19 +1008,19 @@ (** record simprocs **) -fun quick_and_dirty_prove stndrd thy asms prop tac = - if ! quick_and_dirty then - Goal.prove (ProofContext.init thy) [] [] - (Logic.list_implies (map Logic.varify asms, Logic.varify prop)) - (K (Skip_Proof.cheat_tac @{theory HOL})) - (*Drule.standard can take quite a while for large records, thats why - we varify the proposition manually here.*) - else - let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac - in if stndrd then Drule.standard prf else prf end; - -fun quick_and_dirty_prf noopt opt () = - if ! quick_and_dirty then noopt () else opt (); +fun future_forward_prf_standard thy prf prop () = + let val thm = if !quick_and_dirty then Skip_Proof.make_thm thy prop + else Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop; + in Drule.standard thm end; + +fun prove_common immediate stndrd thy asms prop tac = + let val prv = if !quick_and_dirty then Skip_Proof.prove + else if immediate then Goal.prove else Goal.prove_future; + val prf = prv (ProofContext.init thy) [] asms prop tac + in if stndrd then Drule.standard prf else prf end; + +val prove_future_global = prove_common false; +val prove_global = prove_common true; fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) = (case get_updates thy u of @@ -1400,7 +1400,7 @@ (fn thy => fn ss => fn t => let fun prove prop = - quick_and_dirty_prove true thy [] prop + prove_global true thy [] prop (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1); @@ -1665,6 +1665,7 @@ typ_thy |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)] |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name ext_spec)] + ||> Theory.checkpoint val ([ext_def], defs_thy) = timeit_msg "record extension constructor def:" mk_defs; @@ -1696,7 +1697,7 @@ (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) end; - val prove_standard = quick_and_dirty_prove true defs_thy; + val prove_standard = prove_future_global true defs_thy; fun inject_prf () = simplify HOL_ss @@ -2045,6 +2046,7 @@ #> fold Code.add_default_eqn upd_defs #> fold Code.add_default_eqn derived_defs #> pair defs) + ||> Theory.checkpoint val (((sel_defs, upd_defs), derived_defs), defs_thy) = timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" mk_defs; @@ -2115,8 +2117,9 @@ (* 3rd stage: thms_thy *) - fun prove stndrd = quick_and_dirty_prove stndrd defs_thy; - val prove_standard = quick_and_dirty_prove true defs_thy; + fun prove stndrd = prove_future_global stndrd defs_thy; + val prove_standard = prove_future_global true defs_thy; + val future_forward_prf = future_forward_prf_standard defs_thy; fun prove_simp stndrd ss simps = let val tac = simp_all_tac ss simps @@ -2167,7 +2170,7 @@ end; val induct = timeit_msg "record induct proof:" induct_prf; - fun cases_scheme_prf_opt () = + fun cases_scheme_prf () = let val _ $ (Pvar $ _) = concl_of induct_scheme; val ind = @@ -2175,19 +2178,9 @@ [(cterm_of defs_thy Pvar, cterm_of defs_thy (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))] induct_scheme; - in Drule.standard (ObjectLogic.rulify (mp OF [ind, refl])) end; - - fun cases_scheme_prf_noopt () = - prove_standard [] cases_scheme_prop - (fn _ => - EVERY1 - [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]), - try_param_tac rN induct_scheme, - rtac impI, - REPEAT o etac allE, - etac mp, - rtac refl]); - val cases_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt; + in ObjectLogic.rulify (mp OF [ind, refl]) end; + + val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop; val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf; fun cases_prf () = @@ -2226,7 +2219,7 @@ val split_meta_standard = timeit_msg "record split_meta standard:" split_meta_standardise; - fun split_object_prf_opt () = + fun split_object_prf () = let val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0))); val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard)); @@ -2247,17 +2240,10 @@ |> equal_elim (symmetric split_meta') (*!!r. P r*) |> meta_to_obj_all (*All r. P r*) |> implies_intr cr (* 2 ==> 1 *) - in Drule.standard (thr COMP (thl COMP iffI)) end; - - fun split_object_prf_noopt () = - prove_standard [] split_object_prop - (fn _ => - EVERY1 - [rtac iffI, - REPEAT o rtac allI, etac allE, atac, - rtac allI, rtac induct_scheme, REPEAT o etac allE, atac]); - - val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt; + in thr COMP (thl COMP iffI) end; + + + val split_object_prf = future_forward_prf split_object_prf split_object_prop; val split_object = timeit_msg "record split_object proof:" split_object_prf;