src/HOL/Tools/record.ML

 
 
 
 (** 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
     SOME u_name => u_name = s
   | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));

 val record_ex_sel_eq_simproc =
   Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
     (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);
 
         fun mkeq (lr, Teq, (sel, Tsel), x) i =
           if is_selector thy sel then

 
     fun mk_defs () =
       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;
 
 
     (* prepare propositions *)

       let val P = Free (Name.variant variants "P", extT --> Term.propT) in
         Logic.mk_equals
          (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
         (prove_standard [] inject_prop
           (fn _ =>

         (fn defs as ((sel_defs, upd_defs), derived_defs) =>
           fold Code.add_default_eqn sel_defs
           #> 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;
 
     (* prepare propositions *)

       in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
 
 
     (* 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
       in fn prop => prove stndrd [] prop (K tac) end;
 

           THEN try_param_tac "more" @{thm unit.induct} 1
           THEN resolve_tac prems 1)
       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 =
           cterm_instantiate
             [(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 () =
       prove_standard [] cases_prop
         (fn _ =>

     val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
     fun split_meta_standardise () = Drule.standard split_meta;
     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));
         val cP = cterm_of defs_thy P;
         val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard;

           assume cr                             (*All n m more. P (ext n m more)*)
           |> obj_to_meta_all                    (*!!n m more. P (ext n m more)*)
           |> 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;
 
 
     fun split_ex_prf () =
       let