merged

--- /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

--- /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;

--- /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\<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.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.record_split_simproc (K ~1)]) 1*})
+  apply simp
+  done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+  apply (tactic {* Record.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.record_split_simproc (K ~1)]) 1*})
+  apply simp
+  done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* Record.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.record_split_simproc (K ~1)]) 1*})
+  apply auto
+  done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
+  apply auto
+  done
+
+lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+  apply (tactic {* Record.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.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.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.record_ex_sel_eq_simproc]) 1*})
+  done
+
+
+
+end
\ No newline at end of file

--- 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

--- 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;