# HG changeset patch
# User schirmer
# Date 1088597098 -7200
# Node ID 28fa57b57209a64176422acd672f8e9fe6f2cd04
# Parent  35be762f58f95aeaf0027c2ca5663ec38f456eed
Added reference record_definition_quick_and_dirty_sensitive, to
skip proofs triggered by a record definition, if quick_and_dirty
is enabled.

diff -r 35be762f58f9 -r 28fa57b57209 NEWS
--- a/NEWS	Wed Jun 30 00:42:59 2004 +0200
+++ b/NEWS	Wed Jun 30 14:04:58 2004 +0200
@@ -96,6 +96,11 @@
   the old record representation. The type generated for a record is
   called <record_name>_ext_type.
 
+* HOL/record: Reference record_definition_quick_and_dirty_sensitive
+  can be enabled to skip the proofs triggered by a record definition
+  (if quick_and_dirty is enabled). Definitions of large records can
+  take quite long.
+
 * HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
 
   syntax (epsilon)
diff -r 35be762f58f9 -r 28fa57b57209 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jun 30 00:42:59 2004 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Jun 30 14:04:58 2004 +0200
@@ -24,6 +24,7 @@
 sig
   include BASIC_RECORD_PACKAGE
   val quiet_mode: bool ref
+  val record_definition_quick_and_dirty_sensitive: bool ref
   val updateN: string
   val ext_typeN: string
   val last_extT: typ -> (string * typ list) option
@@ -80,6 +81,10 @@
 val quiet_mode = ref false;
 fun message s = if ! quiet_mode then () else writeln s;
 
+(* timing *)
+
+fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
+ 
 (* syntax *)
 
 fun prune n xs = Library.drop (n, xs);
@@ -1063,6 +1068,16 @@
         (x, list_abs (params, Bound 0))])) rule'
   in compose_tac (false, rule'', nprems_of rule) i st end;
 
+
+val record_definition_quick_and_dirty_sensitive = ref false;
+
+(* fun is crucial here; val would evaluate only once! *)
+fun definition_prove_standard sg = 
+  if !record_definition_quick_and_dirty_sensitive
+  then quick_and_dirty_prove sg 
+  else Tactic.prove_standard sg;
+
+
 fun extension_typedef name repT alphas thy =
   let
     val UNIV = HOLogic.mk_UNIV repT;
@@ -1145,10 +1160,11 @@
            ===
            foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more')))
       end;
-
+    
     val induct_prop =
-      All (map dest_Free vars_more) (Trueprop (P $ ext)) ==> Trueprop (P $ s);
-     
+      (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
+
+
     val cases_prop =
       (All (map dest_Free vars_more) 
         (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) 
@@ -1158,21 +1174,26 @@
     val dest_conv_props =
        map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
 
-    val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
+    val prove_standard = definition_prove_standard (Theory.sign_of defs_thy);
     fun prove_simp simps =
       let val tac = simp_all_tac HOL_ss simps
       in fn prop => prove_standard [] [] prop (K tac) end;
     
     (* prove propositions *)
 
-    val inject = (prove_simp [ext_def,abs_inject,Pair_eq] inject_prop);
+    fun inject_prf () = (prove_simp [ext_def,abs_inject,Pair_eq] inject_prop);
+    val inject = timeit_msg "record extension inject proof:" inject_prf;
 
-    val induct =
-        prove_standard [] [] induct_prop (fn prems =>
-         EVERY [try_param_tac rN abs_induct 1, 
-                asm_full_simp_tac (HOL_ss addsimps [ext_def,split_paired_all]) 1]);
+    fun induct_prf () =
+      let val (assm, concl) = induct_prop
+      in prove_standard [] [assm] concl (fn prems =>
+           EVERY [try_param_tac rN abs_induct 1, 
+                  simp_tac (HOL_ss addsimps [split_paired_all]) 1,
+                  resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
+      end;
+    val induct = timeit_msg "record extension induct proof:" induct_prf;
 
-    val cases =
+    fun cases_prf () =
         prove_standard [] [] cases_prop (fn prems =>
          EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
                 try_param_tac rN induct 1,
@@ -1180,10 +1201,12 @@
                 REPEAT (etac allE 1),
                 etac mp 1,
                 rtac refl 1])
+    val cases = timeit_msg "record extension cases proof:" cases_prf;
 	
-    val dest_convs = map (prove_simp 
+    fun dest_convs_prf () = map (prove_simp 
                            ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
-    
+    val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf;
+
     val (thm_thy,([inject',induct',cases'],[dest_convs'])) =
       defs_thy 
       |> (PureThy.add_thms o map Thm.no_attributes) 
@@ -1478,27 +1501,31 @@
 
     (* 3rd stage: thms_thy *)
 
-    val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
+    val prove_standard = definition_prove_standard (Theory.sign_of defs_thy);
     fun prove_simp ss simps =
       let val tac = simp_all_tac ss simps
       in fn prop => prove_standard [] [] prop (K tac) end;
 
     val ss = get_simpset (sign_of defs_thy);
-    val sel_convs = map (prove_simp ss 
+
+    fun sel_convs_prf () = map (prove_simp ss 
                            (sel_defs@ext_dest_convs)) sel_conv_props;
+    val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
 
-    val upd_convs = map (prove_simp ss (sel_convs@upd_defs)) 
-                         upd_conv_props;
-      
+    fun upd_convs_prf () = map (prove_simp ss (sel_convs@upd_defs)) 
+                             upd_conv_props;
+    val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
+
     val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
 
-    val induct_scheme = prove_standard [] [] induct_scheme_prop (fn prems =>
+    fun induct_scheme_prf () = prove_standard [] [] induct_scheme_prop (fn prems =>
           (EVERY [if null parent_induct 
                   then all_tac else try_param_tac rN (hd parent_induct) 1,
                   try_param_tac rN ext_induct 1,
                   asm_simp_tac HOL_basic_ss 1]));
+    val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
 
-    val induct =
+    fun induct_prf () =
       let val (assm, concl) = induct_prop;
       in
         prove_standard [] [assm] concl (fn prems =>
@@ -1506,13 +1533,15 @@
           THEN try_param_tac "more" unit_induct 1
           THEN resolve_tac prems 1)
       end;
+    val induct = timeit_msg "record induct proof:" induct_prf;
 
-    val surjective = 
+    fun surjective_prf () = 
       prove_standard [] [] surjective_prop (fn prems =>
           (EVERY [try_param_tac rN induct_scheme 1,
                   simp_tac (ss addsimps sel_convs) 1]))
-    
-    val cases_scheme =
+    val surjective = timeit_msg "record surjective proof:" surjective_prf;
+
+    fun cases_scheme_prf () =
         prove_standard [] [] cases_scheme_prop (fn prems =>
          EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
                try_param_tac rN induct_scheme 1,
@@ -1520,37 +1549,57 @@
                REPEAT (etac allE 1),
                etac mp 1,
                rtac refl 1])
+    val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
 
-    val cases =
+    fun cases_prf () =
       prove_standard [] [] cases_prop  (fn _ =>
         try_param_tac rN cases_scheme 1
         THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
+    val cases = timeit_msg "record cases proof:" cases_prf;
 
-    val split_meta =
+    fun split_meta_prf () =
         prove_standard [] [] split_meta_prop (fn prems =>
          EVERY [rtac equal_intr_rule 1,
                   rtac meta_allE 1, etac triv_goal 1, atac 1,
                 rtac (prop_subst OF [surjective]) 1,
                 REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]),
                 atac 1]);
+    val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
 
-    val split_object =
+    fun split_object_prf () =
         prove_standard [] [] split_object_prop (fn prems =>
          EVERY [rtac iffI 1, 
                 REPEAT (rtac allI 1), etac allE 1, atac 1,
                 rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
+    val split_object = timeit_msg "record split_object proof:" split_object_prf;
 
-    val split_ex = 
+
+    fun split_ex_prf () = 
         prove_standard [] [] split_ex_prop (fn prems =>
-         fast_simp_tac (claset_of HOL.thy,
-                       HOL_basic_ss addsimps [split_meta]) 1);
+          EVERY [rtac iffI 1,
+                   etac exE 1,
+                   simp_tac (HOL_basic_ss addsimps [split_meta]) 1,
+                   REPEAT (rtac exI 1),
+                   atac 1,
+                 REPEAT (etac exE 1),
+                 rtac exI 1,
+                 atac 1]);
+    val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
 
-    val equality = prove_standard [] [] equality_prop (fn _ =>
+    fun equality_tac thms = 
+      let val (s'::s::eqs) = rev thms;
+          val ss' = ss addsimps (s'::s::sel_convs);
+          val eqs' = map (simplify ss') eqs;
+      in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end;
+ 
+   fun equality_prf () = prove_standard [] [] equality_prop (fn _ =>
       fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
         st |> (res_inst_tac [(rN, s)] cases_scheme 1
         THEN res_inst_tac [(rN, s')] cases_scheme 1
-        THEN simp_all_tac ss (sel_convs))
-      end);
+        THEN (METAHYPS equality_tac 1)) 
+             (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
+      end);                              
+     val equality = timeit_msg "record equality proof':" equality_prf;
 
     val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
                     derived_defs'],