src/HOL/Tools/record.ML

 
 
 
 (** record simprocs **)
 
-fun future_forward_prf thy prf prop =
-  let val thm =
-    if ! quick_and_dirty then Skip_Proof.make_thm thy prop
-    else if Goal.future_enabled () then
-      Goal.future_result (Proof_Context.init_global thy) (Goal.fork prf) prop
-    else prf ()
-  in Drule.export_without_context thm end;
-
 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')]));
 

       let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
       in r0 === mk_rec args 0 end;
 
     (*cases*)
     val cases_scheme_prop =
-      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
-        ==> Trueprop C;
+      (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
 
     val cases_prop =
       (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
          ==> Trueprop C;
 

            [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
             try_param_tac rN ext_induct 1,
             asm_simp_tac HOL_basic_ss 1]));
 
     val induct = timeit_msg ctxt "record induct proof:" (fn () =>
-      let val (assm, concl) = induct_prop in
-        Skip_Proof.prove_global defs_thy [] [assm] concl (fn {prems, ...} =>
-          try_param_tac rN induct_scheme 1
-          THEN try_param_tac "more" @{thm unit.induct} 1
-          THEN resolve_tac prems 1)
-      end);
-
-    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 Object_Logic.rulify (mp OF [ind, refl]) end;
-
-    val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () =>
-      future_forward_prf defs_thy cases_scheme_prf cases_scheme_prop);
-
-    val cases = timeit_msg ctxt "record cases proof:" (fn () =>
-      Skip_Proof.prove_global defs_thy [] [] cases_prop
-        (fn _ =>
-          try_param_tac rN cases_scheme 1 THEN
-          ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps [@{thm unit_all_eq1}]))));
+      Skip_Proof.prove_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
+        try_param_tac rN induct_scheme 1
+        THEN try_param_tac "more" @{thm unit.induct} 1
+        THEN resolve_tac prems 1));
 
     val surjective = timeit_msg ctxt "record surjective proof:" (fn () =>
       let
         val leaf_ss =
           get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});

               simp_tac init_ss 1,
               REPEAT
                 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
                   (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
       end);
+
+    val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () =>
+      Skip_Proof.prove_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
+        (fn {prems, ...} =>
+          resolve_tac prems 1 THEN
+          rtac surjective 1));
+
+    val cases = timeit_msg ctxt "record cases proof:" (fn () =>
+      Skip_Proof.prove_global defs_thy [] [] cases_prop
+        (fn _ =>
+          try_param_tac rN cases_scheme 1 THEN
+          ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps @{thms unit_all_eq1}))));
 
     val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
       Skip_Proof.prove_global defs_thy [] [] split_meta_prop
         (fn _ =>
           EVERY1