clarified quick-and-dirty usage in record package;
authorschirmer <schirmer@in.tum.de>
Sat Nov 14 09:31:54 2009 +0100 (2009-11-14)
changeset 336913db22a5707f3
parent 33653 feaf3627a844
child 33692 ac68c3ee4c2e
clarified quick-and-dirty usage in record package;
removed non-optimized versions of proofs;
introduced future proofs
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Fri Nov 13 06:24:31 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Nov 14 09:31:54 2009 +0100
     1.3 @@ -1008,19 +1008,19 @@
     1.4  
     1.5  (** record simprocs **)
     1.6  
     1.7 -fun quick_and_dirty_prove stndrd thy asms prop tac =
     1.8 -  if ! quick_and_dirty then
     1.9 -    Goal.prove (ProofContext.init thy) [] []
    1.10 -      (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
    1.11 -      (K (Skip_Proof.cheat_tac @{theory HOL}))
    1.12 -      (*Drule.standard can take quite a while for large records, thats why
    1.13 -        we varify the proposition manually here.*)
    1.14 -  else
    1.15 -    let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac
    1.16 -    in if stndrd then Drule.standard prf else prf end;
    1.17 -
    1.18 -fun quick_and_dirty_prf noopt opt () =
    1.19 -  if ! quick_and_dirty then noopt () else opt ();
    1.20 +fun future_forward_prf_standard thy prf prop () =
    1.21 +   let val thm = if !quick_and_dirty then Skip_Proof.make_thm thy prop 
    1.22 +                 else Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop;
    1.23 +   in Drule.standard thm end;
    1.24 +
    1.25 +fun prove_common immediate stndrd thy asms prop tac =
    1.26 +  let val prv = if !quick_and_dirty then Skip_Proof.prove 
    1.27 +                else if immediate then Goal.prove else Goal.prove_future;
    1.28 +      val prf = prv (ProofContext.init thy) [] asms prop tac
    1.29 +  in if stndrd then Drule.standard prf else prf end;
    1.30 +
    1.31 +val prove_future_global = prove_common false;
    1.32 +val prove_global = prove_common true;
    1.33  
    1.34  fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
    1.35    (case get_updates thy u of
    1.36 @@ -1400,7 +1400,7 @@
    1.37      (fn thy => fn ss => fn t =>
    1.38        let
    1.39          fun prove prop =
    1.40 -          quick_and_dirty_prove true thy [] prop
    1.41 +          prove_global true thy [] prop
    1.42              (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
    1.43                  addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
    1.44  
    1.45 @@ -1665,6 +1665,7 @@
    1.46        typ_thy
    1.47        |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)]
    1.48        |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name ext_spec)]
    1.49 +      ||> Theory.checkpoint
    1.50      val ([ext_def], defs_thy) =
    1.51        timeit_msg "record extension constructor def:" mk_defs;
    1.52  
    1.53 @@ -1696,7 +1697,7 @@
    1.54           (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
    1.55        end;
    1.56  
    1.57 -    val prove_standard = quick_and_dirty_prove true defs_thy;
    1.58 +    val prove_standard = prove_future_global true defs_thy;
    1.59  
    1.60      fun inject_prf () =
    1.61        simplify HOL_ss
    1.62 @@ -2045,6 +2046,7 @@
    1.63            #> fold Code.add_default_eqn upd_defs
    1.64            #> fold Code.add_default_eqn derived_defs
    1.65            #> pair defs)
    1.66 +      ||> Theory.checkpoint
    1.67      val (((sel_defs, upd_defs), derived_defs), defs_thy) =
    1.68        timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
    1.69          mk_defs;
    1.70 @@ -2115,8 +2117,9 @@
    1.71  
    1.72      (* 3rd stage: thms_thy *)
    1.73  
    1.74 -    fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
    1.75 -    val prove_standard = quick_and_dirty_prove true defs_thy;
    1.76 +    fun prove stndrd = prove_future_global stndrd defs_thy;
    1.77 +    val prove_standard = prove_future_global true defs_thy;
    1.78 +    val future_forward_prf = future_forward_prf_standard defs_thy;
    1.79  
    1.80      fun prove_simp stndrd ss simps =
    1.81        let val tac = simp_all_tac ss simps
    1.82 @@ -2167,7 +2170,7 @@
    1.83        end;
    1.84      val induct = timeit_msg "record induct proof:" induct_prf;
    1.85  
    1.86 -    fun cases_scheme_prf_opt () =
    1.87 +    fun cases_scheme_prf () =
    1.88        let
    1.89          val _ $ (Pvar $ _) = concl_of induct_scheme;
    1.90          val ind =
    1.91 @@ -2175,19 +2178,9 @@
    1.92              [(cterm_of defs_thy Pvar, cterm_of defs_thy
    1.93                (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
    1.94              induct_scheme;
    1.95 -        in Drule.standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
    1.96 -
    1.97 -    fun cases_scheme_prf_noopt () =
    1.98 -      prove_standard [] cases_scheme_prop
    1.99 -        (fn _ =>
   1.100 -          EVERY1
   1.101 -           [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]),
   1.102 -            try_param_tac rN induct_scheme,
   1.103 -            rtac impI,
   1.104 -            REPEAT o etac allE,
   1.105 -            etac mp,
   1.106 -            rtac refl]);
   1.107 -    val cases_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt;
   1.108 +        in ObjectLogic.rulify (mp OF [ind, refl]) end;
   1.109 +
   1.110 +    val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
   1.111      val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
   1.112  
   1.113      fun cases_prf () =
   1.114 @@ -2226,7 +2219,7 @@
   1.115      val split_meta_standard =
   1.116        timeit_msg "record split_meta standard:" split_meta_standardise;
   1.117  
   1.118 -    fun split_object_prf_opt () =
   1.119 +    fun split_object_prf () =
   1.120        let
   1.121          val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
   1.122          val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard));
   1.123 @@ -2247,17 +2240,10 @@
   1.124            |> equal_elim (symmetric split_meta') (*!!r. P r*)
   1.125            |> meta_to_obj_all                    (*All r. P r*)
   1.126            |> implies_intr cr                    (* 2 ==> 1 *)
   1.127 -     in Drule.standard (thr COMP (thl COMP iffI)) end;
   1.128 -
   1.129 -    fun split_object_prf_noopt () =
   1.130 -      prove_standard [] split_object_prop
   1.131 -        (fn _ =>
   1.132 -          EVERY1
   1.133 -           [rtac iffI,
   1.134 -            REPEAT o rtac allI, etac allE, atac,
   1.135 -            rtac allI, rtac induct_scheme, REPEAT o etac allE, atac]);
   1.136 -
   1.137 -    val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt;
   1.138 +     in thr COMP (thl COMP iffI) end;
   1.139 +
   1.140 +
   1.141 +    val split_object_prf = future_forward_prf split_object_prf split_object_prop;
   1.142      val split_object = timeit_msg "record split_object proof:" split_object_prf;
   1.143  
   1.144