Added reference record_definition_quick_and_dirty_sensitive, to
authorschirmer
Wed Jun 30 14:04:58 2004 +0200 (2004-06-30)
changeset 1501228fa57b57209
parent 15011 35be762f58f9
child 15013 34264f5e4691
Added reference record_definition_quick_and_dirty_sensitive, to
skip proofs triggered by a record definition, if quick_and_dirty
is enabled.
NEWS
src/HOL/Tools/record_package.ML
     1.1 --- a/NEWS	Wed Jun 30 00:42:59 2004 +0200
     1.2 +++ b/NEWS	Wed Jun 30 14:04:58 2004 +0200
     1.3 @@ -96,6 +96,11 @@
     1.4    the old record representation. The type generated for a record is
     1.5    called <record_name>_ext_type.
     1.6  
     1.7 +* HOL/record: Reference record_definition_quick_and_dirty_sensitive
     1.8 +  can be enabled to skip the proofs triggered by a record definition
     1.9 +  (if quick_and_dirty is enabled). Definitions of large records can
    1.10 +  take quite long.
    1.11 +
    1.12  * HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
    1.13  
    1.14    syntax (epsilon)
     2.1 --- a/src/HOL/Tools/record_package.ML	Wed Jun 30 00:42:59 2004 +0200
     2.2 +++ b/src/HOL/Tools/record_package.ML	Wed Jun 30 14:04:58 2004 +0200
     2.3 @@ -24,6 +24,7 @@
     2.4  sig
     2.5    include BASIC_RECORD_PACKAGE
     2.6    val quiet_mode: bool ref
     2.7 +  val record_definition_quick_and_dirty_sensitive: bool ref
     2.8    val updateN: string
     2.9    val ext_typeN: string
    2.10    val last_extT: typ -> (string * typ list) option
    2.11 @@ -80,6 +81,10 @@
    2.12  val quiet_mode = ref false;
    2.13  fun message s = if ! quiet_mode then () else writeln s;
    2.14  
    2.15 +(* timing *)
    2.16 +
    2.17 +fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
    2.18 + 
    2.19  (* syntax *)
    2.20  
    2.21  fun prune n xs = Library.drop (n, xs);
    2.22 @@ -1063,6 +1068,16 @@
    2.23          (x, list_abs (params, Bound 0))])) rule'
    2.24    in compose_tac (false, rule'', nprems_of rule) i st end;
    2.25  
    2.26 +
    2.27 +val record_definition_quick_and_dirty_sensitive = ref false;
    2.28 +
    2.29 +(* fun is crucial here; val would evaluate only once! *)
    2.30 +fun definition_prove_standard sg = 
    2.31 +  if !record_definition_quick_and_dirty_sensitive
    2.32 +  then quick_and_dirty_prove sg 
    2.33 +  else Tactic.prove_standard sg;
    2.34 +
    2.35 +
    2.36  fun extension_typedef name repT alphas thy =
    2.37    let
    2.38      val UNIV = HOLogic.mk_UNIV repT;
    2.39 @@ -1145,10 +1160,11 @@
    2.40             ===
    2.41             foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more')))
    2.42        end;
    2.43 -
    2.44 +    
    2.45      val induct_prop =
    2.46 -      All (map dest_Free vars_more) (Trueprop (P $ ext)) ==> Trueprop (P $ s);
    2.47 -     
    2.48 +      (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
    2.49 +
    2.50 +
    2.51      val cases_prop =
    2.52        (All (map dest_Free vars_more) 
    2.53          (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) 
    2.54 @@ -1158,21 +1174,26 @@
    2.55      val dest_conv_props =
    2.56         map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
    2.57  
    2.58 -    val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
    2.59 +    val prove_standard = definition_prove_standard (Theory.sign_of defs_thy);
    2.60      fun prove_simp simps =
    2.61        let val tac = simp_all_tac HOL_ss simps
    2.62        in fn prop => prove_standard [] [] prop (K tac) end;
    2.63      
    2.64      (* prove propositions *)
    2.65  
    2.66 -    val inject = (prove_simp [ext_def,abs_inject,Pair_eq] inject_prop);
    2.67 +    fun inject_prf () = (prove_simp [ext_def,abs_inject,Pair_eq] inject_prop);
    2.68 +    val inject = timeit_msg "record extension inject proof:" inject_prf;
    2.69  
    2.70 -    val induct =
    2.71 -        prove_standard [] [] induct_prop (fn prems =>
    2.72 -         EVERY [try_param_tac rN abs_induct 1, 
    2.73 -                asm_full_simp_tac (HOL_ss addsimps [ext_def,split_paired_all]) 1]);
    2.74 +    fun induct_prf () =
    2.75 +      let val (assm, concl) = induct_prop
    2.76 +      in prove_standard [] [assm] concl (fn prems =>
    2.77 +           EVERY [try_param_tac rN abs_induct 1, 
    2.78 +                  simp_tac (HOL_ss addsimps [split_paired_all]) 1,
    2.79 +                  resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
    2.80 +      end;
    2.81 +    val induct = timeit_msg "record extension induct proof:" induct_prf;
    2.82  
    2.83 -    val cases =
    2.84 +    fun cases_prf () =
    2.85          prove_standard [] [] cases_prop (fn prems =>
    2.86           EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
    2.87                  try_param_tac rN induct 1,
    2.88 @@ -1180,10 +1201,12 @@
    2.89                  REPEAT (etac allE 1),
    2.90                  etac mp 1,
    2.91                  rtac refl 1])
    2.92 +    val cases = timeit_msg "record extension cases proof:" cases_prf;
    2.93  	
    2.94 -    val dest_convs = map (prove_simp 
    2.95 +    fun dest_convs_prf () = map (prove_simp 
    2.96                             ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
    2.97 -    
    2.98 +    val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf;
    2.99 +
   2.100      val (thm_thy,([inject',induct',cases'],[dest_convs'])) =
   2.101        defs_thy 
   2.102        |> (PureThy.add_thms o map Thm.no_attributes) 
   2.103 @@ -1478,27 +1501,31 @@
   2.104  
   2.105      (* 3rd stage: thms_thy *)
   2.106  
   2.107 -    val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
   2.108 +    val prove_standard = definition_prove_standard (Theory.sign_of defs_thy);
   2.109      fun prove_simp ss simps =
   2.110        let val tac = simp_all_tac ss simps
   2.111        in fn prop => prove_standard [] [] prop (K tac) end;
   2.112  
   2.113      val ss = get_simpset (sign_of defs_thy);
   2.114 -    val sel_convs = map (prove_simp ss 
   2.115 +
   2.116 +    fun sel_convs_prf () = map (prove_simp ss 
   2.117                             (sel_defs@ext_dest_convs)) sel_conv_props;
   2.118 +    val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
   2.119  
   2.120 -    val upd_convs = map (prove_simp ss (sel_convs@upd_defs)) 
   2.121 -                         upd_conv_props;
   2.122 -      
   2.123 +    fun upd_convs_prf () = map (prove_simp ss (sel_convs@upd_defs)) 
   2.124 +                             upd_conv_props;
   2.125 +    val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
   2.126 +
   2.127      val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
   2.128  
   2.129 -    val induct_scheme = prove_standard [] [] induct_scheme_prop (fn prems =>
   2.130 +    fun induct_scheme_prf () = prove_standard [] [] induct_scheme_prop (fn prems =>
   2.131            (EVERY [if null parent_induct 
   2.132                    then all_tac else try_param_tac rN (hd parent_induct) 1,
   2.133                    try_param_tac rN ext_induct 1,
   2.134                    asm_simp_tac HOL_basic_ss 1]));
   2.135 +    val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
   2.136  
   2.137 -    val induct =
   2.138 +    fun induct_prf () =
   2.139        let val (assm, concl) = induct_prop;
   2.140        in
   2.141          prove_standard [] [assm] concl (fn prems =>
   2.142 @@ -1506,13 +1533,15 @@
   2.143            THEN try_param_tac "more" unit_induct 1
   2.144            THEN resolve_tac prems 1)
   2.145        end;
   2.146 +    val induct = timeit_msg "record induct proof:" induct_prf;
   2.147  
   2.148 -    val surjective = 
   2.149 +    fun surjective_prf () = 
   2.150        prove_standard [] [] surjective_prop (fn prems =>
   2.151            (EVERY [try_param_tac rN induct_scheme 1,
   2.152                    simp_tac (ss addsimps sel_convs) 1]))
   2.153 -    
   2.154 -    val cases_scheme =
   2.155 +    val surjective = timeit_msg "record surjective proof:" surjective_prf;
   2.156 +
   2.157 +    fun cases_scheme_prf () =
   2.158          prove_standard [] [] cases_scheme_prop (fn prems =>
   2.159           EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
   2.160                 try_param_tac rN induct_scheme 1,
   2.161 @@ -1520,37 +1549,57 @@
   2.162                 REPEAT (etac allE 1),
   2.163                 etac mp 1,
   2.164                 rtac refl 1])
   2.165 +    val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
   2.166  
   2.167 -    val cases =
   2.168 +    fun cases_prf () =
   2.169        prove_standard [] [] cases_prop  (fn _ =>
   2.170          try_param_tac rN cases_scheme 1
   2.171          THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
   2.172 +    val cases = timeit_msg "record cases proof:" cases_prf;
   2.173  
   2.174 -    val split_meta =
   2.175 +    fun split_meta_prf () =
   2.176          prove_standard [] [] split_meta_prop (fn prems =>
   2.177           EVERY [rtac equal_intr_rule 1,
   2.178                    rtac meta_allE 1, etac triv_goal 1, atac 1,
   2.179                  rtac (prop_subst OF [surjective]) 1,
   2.180                  REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]),
   2.181                  atac 1]);
   2.182 +    val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
   2.183  
   2.184 -    val split_object =
   2.185 +    fun split_object_prf () =
   2.186          prove_standard [] [] split_object_prop (fn prems =>
   2.187           EVERY [rtac iffI 1, 
   2.188                  REPEAT (rtac allI 1), etac allE 1, atac 1,
   2.189                  rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
   2.190 +    val split_object = timeit_msg "record split_object proof:" split_object_prf;
   2.191  
   2.192 -    val split_ex = 
   2.193 +
   2.194 +    fun split_ex_prf () = 
   2.195          prove_standard [] [] split_ex_prop (fn prems =>
   2.196 -         fast_simp_tac (claset_of HOL.thy,
   2.197 -                       HOL_basic_ss addsimps [split_meta]) 1);
   2.198 +          EVERY [rtac iffI 1,
   2.199 +                   etac exE 1,
   2.200 +                   simp_tac (HOL_basic_ss addsimps [split_meta]) 1,
   2.201 +                   REPEAT (rtac exI 1),
   2.202 +                   atac 1,
   2.203 +                 REPEAT (etac exE 1),
   2.204 +                 rtac exI 1,
   2.205 +                 atac 1]);
   2.206 +    val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
   2.207  
   2.208 -    val equality = prove_standard [] [] equality_prop (fn _ =>
   2.209 +    fun equality_tac thms = 
   2.210 +      let val (s'::s::eqs) = rev thms;
   2.211 +          val ss' = ss addsimps (s'::s::sel_convs);
   2.212 +          val eqs' = map (simplify ss') eqs;
   2.213 +      in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end;
   2.214 + 
   2.215 +   fun equality_prf () = prove_standard [] [] equality_prop (fn _ =>
   2.216        fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
   2.217          st |> (res_inst_tac [(rN, s)] cases_scheme 1
   2.218          THEN res_inst_tac [(rN, s')] cases_scheme 1
   2.219 -        THEN simp_all_tac ss (sel_convs))
   2.220 -      end);
   2.221 +        THEN (METAHYPS equality_tac 1)) 
   2.222 +             (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
   2.223 +      end);                              
   2.224 +     val equality = timeit_msg "record equality proof':" equality_prf;
   2.225  
   2.226      val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
   2.227                      derived_defs'],