* record_upd_simproc also simplifies trivial updates:
authorschirmer
Tue Jul 06 20:31:06 2004 +0200 (2004-07-06)
changeset 15015c5768e8c4da4
parent 15014 97ab70c3d955
child 15016 bcbef8418da5
* record_upd_simproc also simplifies trivial updates:
r(|x := x r|) = r
* tuned quick and dirty mode
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Sat Jul 03 15:26:58 2004 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jul 06 20:31:06 2004 +0200
     1.3 @@ -24,12 +24,13 @@
     1.4  sig
     1.5    include BASIC_RECORD_PACKAGE
     1.6    val quiet_mode: bool ref
     1.7 -  val record_definition_quick_and_dirty_sensitive: bool ref
     1.8 +  val record_quick_and_dirty_sensitive: bool ref
     1.9    val updateN: string
    1.10    val ext_typeN: string
    1.11    val last_extT: typ -> (string * typ list) option
    1.12    val dest_recTs : typ -> (string * typ list) list
    1.13    val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option
    1.14 +  val get_extinjects: Sign.sg -> thm list
    1.15    val print_records: theory -> unit
    1.16    val add_record: string list * string -> string option -> (string * string * mixfix) list 
    1.17                    -> theory -> theory
    1.18 @@ -75,6 +76,8 @@
    1.19  (*** utilities ***)
    1.20  
    1.21  fun but_last xs = fst (split_last xs);
    1.22 +fun list None = []
    1.23 +  | list (Some x) = [x]
    1.24  
    1.25  (* messages *)
    1.26  
    1.27 @@ -201,14 +204,17 @@
    1.28      updates: string Symtab.table,
    1.29      simpset: Simplifier.simpset},
    1.30    equalities: thm Symtab.table,
    1.31 +  extinjects: thm list,
    1.32 +  extsplit: thm Symtab.table, (* maps extension name to split rule *)
    1.33    splits: (thm*thm*thm*thm) Symtab.table,    (* !!,!,EX - split-equalities,induct rule *) 
    1.34    extfields: (string*typ) list Symtab.table, (* maps extension to its fields *)
    1.35    fieldext: (string*typ list) Symtab.table   (* maps field to its extension *)
    1.36  };
    1.37  
    1.38 -fun make_record_data records sel_upd equalities splits extfields fieldext =
    1.39 +fun make_record_data 
    1.40 +      records sel_upd equalities extinjects extsplit splits extfields fieldext =
    1.41   {records = records, sel_upd = sel_upd, 
    1.42 -  equalities = equalities, splits = splits, 
    1.43 +  equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, 
    1.44    extfields = extfields, fieldext = fieldext }: record_data;
    1.45  
    1.46  structure RecordsArgs =
    1.47 @@ -219,7 +225,7 @@
    1.48    val empty =
    1.49      make_record_data Symtab.empty
    1.50        {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
    1.51 -      Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
    1.52 +       Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
    1.53  
    1.54    val copy = I;
    1.55    val prep_ext = I;
    1.56 @@ -227,12 +233,16 @@
    1.57     ({records = recs1,
    1.58       sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
    1.59       equalities = equalities1,
    1.60 +     extinjects = extinjects1, 
    1.61 +     extsplit = extsplit1,
    1.62       splits = splits1,
    1.63       extfields = extfields1,
    1.64       fieldext = fieldext1},
    1.65      {records = recs2,
    1.66       sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
    1.67 -     equalities = equalities2, 
    1.68 +     equalities = equalities2,
    1.69 +     extinjects = extinjects2, 
    1.70 +     extsplit = extsplit2, 
    1.71       splits = splits2,
    1.72       extfields = extfields2,
    1.73       fieldext = fieldext2}) =
    1.74 @@ -242,6 +252,8 @@
    1.75          updates = Symtab.merge (K true) (upds1, upds2),
    1.76          simpset = Simplifier.merge_ss (ss1, ss2)}
    1.77        (Symtab.merge Thm.eq_thm (equalities1, equalities2))
    1.78 +      (extinjects1 @ extinjects2)
    1.79 +      (Symtab.merge Thm.eq_thm (extsplit1,extsplit2))
    1.80        (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
    1.81                       => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
    1.82                          Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) 
    1.83 @@ -277,9 +289,10 @@
    1.84  
    1.85  fun put_record name info thy =
    1.86    let
    1.87 -    val {records, sel_upd, equalities, splits,extfields,fieldext} = RecordsData.get thy;
    1.88 +    val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} = 
    1.89 +          RecordsData.get thy;
    1.90      val data = make_record_data (Symtab.update ((name, info), records))
    1.91 -      sel_upd equalities splits extfields fieldext;
    1.92 +      sel_upd equalities extinjects extsplit splits extfields fieldext;
    1.93    in RecordsData.put data thy end;
    1.94  
    1.95  (* access 'sel_upd' *)
    1.96 @@ -302,38 +315,70 @@
    1.97      val upds = map (suffix updateN) names ~~ names;
    1.98  
    1.99      val {records, sel_upd = {selectors, updates, simpset}, 
   1.100 -      equalities, splits, extfields,fieldext} = RecordsData.get thy;
   1.101 +      equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
   1.102      val data = make_record_data records
   1.103        {selectors = Symtab.extend (selectors, sels),
   1.104          updates = Symtab.extend (updates, upds),
   1.105          simpset = Simplifier.addsimps (simpset, simps)}
   1.106 -       equalities splits extfields fieldext;
   1.107 +       equalities extinjects extsplit splits extfields fieldext;
   1.108    in RecordsData.put data thy end;
   1.109  
   1.110  (* access 'equalities' *)
   1.111  
   1.112  fun add_record_equalities name thm thy =
   1.113    let
   1.114 -    val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy;
   1.115 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = 
   1.116 +          RecordsData.get thy;
   1.117      val data = make_record_data records sel_upd 
   1.118 -      (Symtab.update_new ((name, thm), equalities)) splits extfields fieldext;
   1.119 +           (Symtab.update_new ((name, thm), equalities)) extinjects extsplit 
   1.120 +           splits extfields fieldext;
   1.121    in RecordsData.put data thy end;
   1.122  
   1.123  fun get_equalities sg name =
   1.124    Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
   1.125  
   1.126 +(* access 'extinjects' *)
   1.127 +
   1.128 +fun add_extinjects thm thy =
   1.129 +  let
   1.130 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = 
   1.131 +          RecordsData.get thy;
   1.132 +    val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit  
   1.133 +                 splits extfields fieldext;
   1.134 +  in RecordsData.put data thy end;
   1.135 +
   1.136 +fun get_extinjects sg = #extinjects (RecordsData.get_sg sg);
   1.137 +
   1.138 +(* access 'extsplit' *)
   1.139 +
   1.140 +fun add_extsplit name thm thy =
   1.141 +  let
   1.142 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = 
   1.143 +          RecordsData.get thy;
   1.144 +    val data = make_record_data records sel_upd 
   1.145 +      equalities extinjects (Symtab.update_new ((name, thm), extsplit)) splits 
   1.146 +      extfields fieldext;
   1.147 +  in RecordsData.put data thy end;
   1.148 +
   1.149 +fun get_extsplit sg name =
   1.150 +  Symtab.lookup (#extsplit (RecordsData.get_sg sg), name);
   1.151 +
   1.152  (* access 'splits' *)
   1.153  
   1.154  fun add_record_splits name thmP thy =
   1.155    let
   1.156 -    val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy;
   1.157 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = 
   1.158 +          RecordsData.get thy;
   1.159      val data = make_record_data records sel_upd 
   1.160 -      equalities (Symtab.update_new ((name, thmP), splits)) extfields fieldext;
   1.161 +      equalities extinjects extsplit (Symtab.update_new ((name, thmP), splits)) 
   1.162 +      extfields fieldext;
   1.163    in RecordsData.put data thy end;
   1.164  
   1.165  fun get_splits sg name =
   1.166    Symtab.lookup (#splits (RecordsData.get_sg sg), name);
   1.167  
   1.168 +
   1.169 +
   1.170  (* extension of a record name *)
   1.171  fun get_extension sg name =
   1.172   case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
   1.173 @@ -344,9 +389,11 @@
   1.174  
   1.175  fun add_extfields name fields thy =
   1.176    let
   1.177 -    val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy;
   1.178 +    val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} = 
   1.179 +          RecordsData.get thy;
   1.180      val data = make_record_data records sel_upd 
   1.181 -         equalities splits (Symtab.update_new ((name, fields), extfields)) fieldext;
   1.182 +         equalities extinjects extsplit splits 
   1.183 +         (Symtab.update_new ((name, fields), extfields)) fieldext;
   1.184    in RecordsData.put data thy end;
   1.185  
   1.186  fun get_extfields sg name =
   1.187 @@ -356,10 +403,12 @@
   1.188  
   1.189  fun add_fieldext extname_types fields thy =
   1.190    let
   1.191 -    val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy;
   1.192 +    val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = 
   1.193 +           RecordsData.get thy;
   1.194      val fieldext' = foldl (fn (table,field) => Symtab.update_new ((field,extname_types),table))  
   1.195                            (fieldext,fields);
   1.196 -    val data = make_record_data records sel_upd equalities splits extfields fieldext';
   1.197 +    val data=make_record_data records sel_upd equalities extinjects extsplit 
   1.198 +              splits extfields fieldext';
   1.199    in RecordsData.put data thy end;
   1.200  
   1.201  
   1.202 @@ -707,22 +756,41 @@
   1.203                           (list_comb (Syntax.const name_sfx,ts))
   1.204    in (name_sfx, tr') end;
   1.205  
   1.206 +(** record simprocs **)
   1.207  
   1.208 -(** record simprocs **)
   1.209 -fun quick_and_dirty_prove sg xs asms prop tac =
   1.210 -Tactic.prove_standard sg xs asms prop
   1.211 -    (if !quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
   1.212 +val record_quick_and_dirty_sensitive = ref false;
   1.213 +
   1.214 +fun quick_and_dirty_prove sg asms prop tac =
   1.215 +  if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
   1.216 +  then Tactic.prove sg [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
   1.217 +        (K (SkipProof.cheat_tac HOL.thy))
   1.218 +        (* standard can take quite a while for large records, thats why
   1.219 +         * we varify the proposition manually here.*) 
   1.220 +  else Tactic.prove_standard sg [] asms prop tac;
   1.221  
   1.222  
   1.223  fun prove_split_simp sg T prop =
   1.224    (case get_splits sg (rec_id T) of
   1.225       Some (all_thm,_,_,_) 
   1.226 -     => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
   1.227 -        in (quick_and_dirty_prove sg [] [] prop 
   1.228 -           (K (simp_tac (simpset addsimps [all_thm]) 1)))
   1.229 +     => let
   1.230 +	   val {sel_upd={simpset,...},extsplit,...} = RecordsData.get_sg sg;
   1.231 +           val extsplits = 
   1.232 +                 foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) 
   1.233 +                    ([],dest_recTs T);
   1.234 +           val thms = all_thm::(case extsplits of [thm] => [] | _ => extsplits);
   1.235 +                                     (* [thm] is the same as all_thm *)
   1.236 +        in (quick_and_dirty_prove sg [] prop 
   1.237 +            (fn _ => (simp_tac (simpset addsimps thms) 1)))
   1.238          end
   1.239     | _ => error "RecordPackage.prove_split_simp:code should never been reached")
   1.240  
   1.241 +
   1.242 +
   1.243 +local
   1.244 +fun get_fields extfields T = 
   1.245 +     foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN))))
   1.246 +             ([],(dest_recTs T));
   1.247 +in
   1.248  (* record_simproc *)
   1.249  (* Simplifies selections of an record update:
   1.250   *  (1)  S (r(|S:=k|)) = k respectively
   1.251 @@ -738,15 +806,13 @@
   1.252  val record_simproc =
   1.253    Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
   1.254      (fn sg => fn _ => fn t =>
   1.255 -      (case t of (sel as Const (s, Type (_,[domS,rangeS]))) $ ((upd as Const (u, _)) $ k $ r) =>
   1.256 +      (case t of (sel as Const (s, Type (_,[domS,rangeS])))$((upd as Const (u, _)) $ k $ r)=>
   1.257          (case get_selectors sg s of Some () =>
   1.258            (case get_updates sg u of Some u_name =>
   1.259              let
   1.260                fun mk_abs_var x t = (x, fastype_of t);
   1.261                val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg;
   1.262 -              fun flds T = 
   1.263 -                   foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN))))
   1.264 -                         ([],(dest_recTs T));
   1.265 +              
   1.266                fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
   1.267  		  (case (Symtab.lookup (updates,u)) of
   1.268                       None => None
   1.269 @@ -758,8 +824,8 @@
   1.270                                 val kv = mk_abs_var "k" k
   1.271                                 val kb = Bound 1 
   1.272                               in Some (upd$kb$rb,kb,[kv,rv],true) end
   1.273 -                        else if u_name mem (flds rangeS)
   1.274 -                             orelse s mem (flds updT)
   1.275 +                        else if u_name mem (get_fields extfields rangeS)
   1.276 +                             orelse s mem (get_fields extfields updT)
   1.277                               then None
   1.278  			     else (case mk_eq_terms r of 
   1.279                                       Some (trm,trm',vars,update_s) 
   1.280 @@ -789,6 +855,114 @@
   1.281          | None => None)
   1.282        | _ => None));
   1.283  
   1.284 +(* record_upd_simproc *) 
   1.285 +(* simplify multiple updates:
   1.286 + *  (1)  "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)"
   1.287 + *  (2)  "r(|M:= M r|) = r"
   1.288 + * For (2) special care of "more" updates has to be taken:
   1.289 + *    r(|more := m; A := A r|)
   1.290 + * If A is contained in the fields of m we cannot remove the update A := A r!
   1.291 + * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|) 
   1.292 +*)
   1.293 +val record_upd_simproc =
   1.294 +  Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"]
   1.295 +    (fn sg => fn _ => fn t =>
   1.296 +      (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
   1.297 + 	 let datatype ('a,'b) calc = Init of 'b | Inter of 'a  
   1.298 +             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get_sg sg;
   1.299 +             
   1.300 +	     fun mk_abs_var x t = (x, fastype_of t);
   1.301 +             fun sel_name u = NameSpace.base (unsuffix updateN u);
   1.302 +
   1.303 +             fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
   1.304 +                  if s mem (get_fields extfields mT) then upd else seed s r
   1.305 +               | seed _ r = r;
   1.306 +
   1.307 +             fun grow u uT k vars (sprout,skeleton) = 
   1.308 +		   if sel_name u = moreN
   1.309 +                   then let val kv = mk_abs_var "k" k;
   1.310 +                            val kb = Bound (length vars);
   1.311 +                        in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
   1.312 +                   else ((sprout,skeleton),vars);
   1.313 +
   1.314 +             fun is_upd_same (sprout,skeleton) u ((sel as Const (s,_))$r) =
   1.315 +                   if (unsuffix updateN u) = s andalso (seed s sprout) = r 
   1.316 +                   then Some (sel,seed s skeleton)
   1.317 +                   else None
   1.318 +               | is_upd_same _ _ _ = None
   1.319 + 
   1.320 +             fun init_seed r = ((r,Bound 0), [mk_abs_var "r" r]);
   1.321 +                       
   1.322 +             (* mk_updterm returns either
   1.323 +              *  - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
   1.324 +              *     where vars are the bound variables in the skeleton 
   1.325 +              *  - Inter (orig-term-skeleton,simplified-term-skeleton, 
   1.326 +              *           vars, term-sprout, skeleton-sprout)
   1.327 +              *     where "All vars. orig-term-skeleton = simplified-term-skeleton" is
   1.328 +              *     the desired simplification rule,
   1.329 +              *     the sprouts accumulate the "more-updates" on the way from the seed
   1.330 +              *     to the outermost update. It is only relevant to calculate the 
   1.331 +              *     possible simplification for (2) 
   1.332 +              * The algorithm first walks down the updates to the seed-record while
   1.333 +              * memorising the updates in the already-table. While walking up the
   1.334 +              * updates again, the optimised term is constructed.
   1.335 +              *)
   1.336 +             fun mk_updterm upds already (t as ((upd as Const (u,uT)) $ k $ r)) =
   1.337 +		 if is_some (Symtab.lookup (upds,u))
   1.338 +		 then let 
   1.339 +			 fun rest already = mk_updterm upds already
   1.340 +		      in if is_some (Symtab.lookup (already,u)) 
   1.341 +			 then (case (rest already r) of
   1.342 +				 Init ((sprout,skel),vars) => 
   1.343 +                                 let
   1.344 +	                           val kv = mk_abs_var (sel_name u) k;
   1.345 +                                   val kb = Bound (length vars);
   1.346 +                                   val (sprout',vars')= grow u uT k (kv::vars) (sprout,skel);
   1.347 +                                 in Inter (upd$kb$skel,skel,vars',sprout') end
   1.348 +                               | Inter (trm,trm',vars,sprout) => 
   1.349 +                                 let 
   1.350 +		                   val kv = mk_abs_var (sel_name u) k;
   1.351 +                                   val kb = Bound (length vars);
   1.352 +                                   val (sprout',vars') = grow u uT k (kv::vars) sprout;
   1.353 +                                 in Inter(upd$kb$trm,trm',kv::vars',sprout') end) 
   1.354 +	                 else 
   1.355 +                          (case rest (Symtab.update ((u,()),already)) r of 
   1.356 +			     Init ((sprout,skel),vars) => 
   1.357 +                              (case is_upd_same (sprout,skel) u k of
   1.358 +                                 Some (sel,skel') => 
   1.359 +                                 let
   1.360 +		                   val (sprout',vars') = grow u uT k vars (sprout,skel); 
   1.361 +                                  in Inter(upd$(sel$skel')$skel,skel,vars',sprout') end
   1.362 +                               | None =>  
   1.363 +                                 let
   1.364 +	                           val kv = mk_abs_var (sel_name u) k;
   1.365 +                                   val kb = Bound (length vars);
   1.366 +                                 in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end)
   1.367 +		           | Inter (trm,trm',vars,sprout) => 
   1.368 +                               (case is_upd_same sprout u k of
   1.369 +                                  Some (sel,skel) =>
   1.370 +                                  let
   1.371 +                                    val (sprout',vars') = grow u uT k vars sprout
   1.372 +                                  in Inter(upd$(sel$skel)$trm,trm',vars',sprout') end
   1.373 +                                | None =>
   1.374 +                                  let
   1.375 +				    val kv = mk_abs_var (sel_name u) k
   1.376 +                                    val kb = Bound (length vars)
   1.377 +                                    val (sprout',vars') = grow u uT k (kv::vars) sprout
   1.378 +                                  in Inter (upd$kb$trm,upd$kb$trm',vars',sprout') end))
   1.379 +		      end
   1.380 +		 else Init (init_seed t)
   1.381 +	       | mk_updterm _ _ t = Init (init_seed t);
   1.382 +
   1.383 +	 in (case mk_updterm updates Symtab.empty t of
   1.384 +	       Inter (trm,trm',vars,_)
   1.385 +                => Some (prove_split_simp sg T  
   1.386 +                          (list_all(vars,(Logic.mk_equals (trm,trm')))))
   1.387 +             | _ => None)
   1.388 +	 end
   1.389 +       | _ => None));
   1.390 +end
   1.391 +
   1.392  (* record_eq_simproc *)
   1.393  (* looks up the most specific record-equality.
   1.394   * Note on efficiency:
   1.395 @@ -813,52 +987,6 @@
   1.396                                | Some thm => Some (thm RS Eq_TrueI)))
   1.397         | _ => None));
   1.398  
   1.399 -
   1.400 -(* record_upd_simproc *)
   1.401 -(* simplify multiple updates; for example: "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" *)
   1.402 -val record_upd_simproc =
   1.403 -  Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u1 k1 (u2 k2 r))"]
   1.404 -    (fn sg => fn _ => fn t =>
   1.405 -      (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
   1.406 - 	 let val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
   1.407 -	     fun mk_abs_var x t = (x, fastype_of t);
   1.408 -
   1.409 -             fun mk_updterm upds already ((upd as Const (u,_)) $ k $ r) =
   1.410 -		 if is_some (Symtab.lookup (upds,u))
   1.411 -		 then let 
   1.412 -			 fun rest already = mk_updterm upds already
   1.413 -		      in if is_some (Symtab.lookup (already,u)) 
   1.414 -			 then (case (rest already r) of
   1.415 -				 None => let 
   1.416 -				           val rv = mk_abs_var "r" r
   1.417 -                                           val rb = Bound 0
   1.418 -					   val kv = mk_abs_var "k" k
   1.419 -                                           val kb = Bound 1	      
   1.420 -                                         in Some (upd$kb$rb,rb,[kv,rv]) end
   1.421 -                               | Some (trm,trm',vars) 
   1.422 -				 => let 
   1.423 -				     val kv = mk_abs_var "k" k
   1.424 -                                     val kb = Bound (length vars)
   1.425 -                                    in Some (upd$kb$trm,trm',kv::vars) end)
   1.426 -	                 else (case rest (Symtab.update ((u,()),already)) r of 
   1.427 -				 None => None
   1.428 -		               | Some (trm,trm',vars) 
   1.429 -                                  => let
   1.430 -				      val kv = mk_abs_var "k" k
   1.431 -                                      val kb = Bound (length vars)
   1.432 -                                     in Some (upd$kb$trm,upd$kb$trm',kv::vars) end)
   1.433 -		     end
   1.434 -		 else None
   1.435 -	       | mk_updterm _ _ _ = None;
   1.436 -
   1.437 -	 in (case mk_updterm updates Symtab.empty t of
   1.438 -	       Some (trm,trm',vars)
   1.439 -                => Some (prove_split_simp sg T  
   1.440 -                          (list_all(vars,(Logic.mk_equals (trm,trm')))))
   1.441 -             | None => None)
   1.442 -	 end
   1.443 -       | _ => None));
   1.444 -
   1.445  (* record_split_simproc *)
   1.446  (* splits quantified occurrences of records, for which P holds. P can peek on the 
   1.447   * subterm starting at the quantified occurrence of the record (including the quantifier)
   1.448 @@ -888,7 +1016,7 @@
   1.449    Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
   1.450      (fn sg => fn _ => fn t =>
   1.451         let 
   1.452 -         fun prove prop = (quick_and_dirty_prove sg [] [] prop 
   1.453 +         fun prove prop = (quick_and_dirty_prove sg [] prop 
   1.454                               (fn _ => (simp_tac ((get_simpset sg) addsimps simp_thms
   1.455                                          addsimprocs [record_split_simproc (K true)]) 1)));
   1.456  
   1.457 @@ -1068,16 +1196,6 @@
   1.458          (x, list_abs (params, Bound 0))])) rule'
   1.459    in compose_tac (false, rule'', nprems_of rule) i st end;
   1.460  
   1.461 -
   1.462 -val record_definition_quick_and_dirty_sensitive = ref false;
   1.463 -
   1.464 -(* fun is crucial here; val would evaluate only once! *)
   1.465 -fun definition_prove_standard sg = 
   1.466 -  if !record_definition_quick_and_dirty_sensitive
   1.467 -  then quick_and_dirty_prove sg 
   1.468 -  else Tactic.prove_standard sg;
   1.469 -
   1.470 -
   1.471  fun extension_typedef name repT alphas thy =
   1.472    let
   1.473      val UNIV = HOLogic.mk_UNIV repT;
   1.474 @@ -1147,10 +1265,11 @@
   1.475  
   1.476      val vars_more = vars@[more];
   1.477      val named_vars_more = (names@[full moreN])~~vars_more;
   1.478 +    val variants = map (fn (Free (x,_))=>x) vars_more;
   1.479      val ext = list_comb (Const ext_decl,vars_more);
   1.480      val s     = Free (rN, extT);
   1.481 -    val P = Free (variant (map (fn (Free (x,_))=>x) vars_more) "P", extT-->HOLogic.boolT);
   1.482 -    val C = Free (variant (map (fn (Free (x,_))=>x) vars_more) "C", HOLogic.boolT);
   1.483 +    val P = Free (variant variants "P", extT-->HOLogic.boolT);
   1.484 +    val C = Free (variant variants "C", HOLogic.boolT);
   1.485  
   1.486      val inject_prop =
   1.487        let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
   1.488 @@ -1174,10 +1293,21 @@
   1.489      val dest_conv_props =
   1.490         map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
   1.491  
   1.492 -    val prove_standard = definition_prove_standard (Theory.sign_of defs_thy);
   1.493 +    val surjective_prop =
   1.494 +      let val args = 
   1.495 +           map (fn (c, Free (_,T)) => mk_sel s (suffix ext_dest c,T)) named_vars_more;
   1.496 +      in s === list_comb (Const ext_decl, args) end;
   1.497 +
   1.498 +    val split_meta_prop =
   1.499 +      let val P = Free (variant variants "P", extT-->Term.propT) in
   1.500 +        Logic.mk_equals 
   1.501 +         (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
   1.502 +      end; 
   1.503 +
   1.504 +    val prove_standard = quick_and_dirty_prove (Theory.sign_of defs_thy);
   1.505      fun prove_simp simps =
   1.506        let val tac = simp_all_tac HOL_ss simps
   1.507 -      in fn prop => prove_standard [] [] prop (K tac) end;
   1.508 +      in fn prop => prove_standard [] prop (K tac) end;
   1.509      
   1.510      (* prove propositions *)
   1.511  
   1.512 @@ -1186,7 +1316,7 @@
   1.513  
   1.514      fun induct_prf () =
   1.515        let val (assm, concl) = induct_prop
   1.516 -      in prove_standard [] [assm] concl (fn prems =>
   1.517 +      in prove_standard [assm] concl (fn prems =>
   1.518             EVERY [try_param_tac rN abs_induct 1, 
   1.519                    simp_tac (HOL_ss addsimps [split_paired_all]) 1,
   1.520                    resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
   1.521 @@ -1194,7 +1324,7 @@
   1.522      val induct = timeit_msg "record extension induct proof:" induct_prf;
   1.523  
   1.524      fun cases_prf () =
   1.525 -        prove_standard [] [] cases_prop (fn prems =>
   1.526 +        prove_standard [] cases_prop (fn prems =>
   1.527           EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
   1.528                  try_param_tac rN induct 1,
   1.529                  rtac impI 1,
   1.530 @@ -1207,16 +1337,33 @@
   1.531                             ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
   1.532      val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf;
   1.533  
   1.534 -    val (thm_thy,([inject',induct',cases'],[dest_convs'])) =
   1.535 +    fun surjective_prf () = 
   1.536 +      prove_standard [] surjective_prop (fn prems =>
   1.537 +          (EVERY [try_param_tac rN induct 1,
   1.538 +                  simp_tac (HOL_basic_ss addsimps dest_convs) 1]));
   1.539 +    val surjective = timeit_msg "record extension surjective proof:" surjective_prf;
   1.540 +
   1.541 +    fun split_meta_prf () =
   1.542 +        prove_standard [] split_meta_prop (fn prems =>
   1.543 +         EVERY [rtac equal_intr_rule 1,
   1.544 +                  rtac meta_allE 1, etac triv_goal 1, atac 1,
   1.545 +                rtac (prop_subst OF [surjective]) 1,
   1.546 +                REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]),
   1.547 +                atac 1]);
   1.548 +    val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
   1.549 +
   1.550 +    val (thm_thy,([inject',induct',cases',surjective',split_meta'],[dest_convs'])) =
   1.551        defs_thy 
   1.552        |> (PureThy.add_thms o map Thm.no_attributes) 
   1.553             [("ext_inject", inject),
   1.554              ("ext_induct", induct),
   1.555 -            ("ext_cases", cases)]
   1.556 +            ("ext_cases", cases),
   1.557 +            ("ext_surjective", surjective),
   1.558 +            ("ext_split", split_meta)]
   1.559        |>>> (PureThy.add_thmss o map Thm.no_attributes)
   1.560                [("dest_convs",dest_convs)] 
   1.561  
   1.562 -  in (thm_thy,extT,induct',inject',dest_convs')
   1.563 +  in (thm_thy,extT,induct',inject',dest_convs',split_meta')
   1.564    end;
   1.565     
   1.566  fun chunks []      []   = []
   1.567 @@ -1295,7 +1442,7 @@
   1.568     
   1.569      (* 1st stage: extension_thy *)
   1.570  	
   1.571 -    val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs) =
   1.572 +    val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split) =
   1.573        thy
   1.574        |> Theory.add_path bname
   1.575        |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
   1.576 @@ -1501,10 +1648,10 @@
   1.577  
   1.578      (* 3rd stage: thms_thy *)
   1.579  
   1.580 -    val prove_standard = definition_prove_standard (Theory.sign_of defs_thy);
   1.581 +    val prove_standard = quick_and_dirty_prove (Theory.sign_of defs_thy);
   1.582      fun prove_simp ss simps =
   1.583        let val tac = simp_all_tac ss simps
   1.584 -      in fn prop => prove_standard [] [] prop (K tac) end;
   1.585 +      in fn prop => prove_standard [] prop (K tac) end;
   1.586  
   1.587      val ss = get_simpset (sign_of defs_thy);
   1.588  
   1.589 @@ -1518,7 +1665,7 @@
   1.590  
   1.591      val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
   1.592  
   1.593 -    fun induct_scheme_prf () = prove_standard [] [] induct_scheme_prop (fn prems =>
   1.594 +    fun induct_scheme_prf () = prove_standard [] induct_scheme_prop (fn prems =>
   1.595            (EVERY [if null parent_induct 
   1.596                    then all_tac else try_param_tac rN (hd parent_induct) 1,
   1.597                    try_param_tac rN ext_induct 1,
   1.598 @@ -1528,7 +1675,7 @@
   1.599      fun induct_prf () =
   1.600        let val (assm, concl) = induct_prop;
   1.601        in
   1.602 -        prove_standard [] [assm] concl (fn prems =>
   1.603 +        prove_standard [assm] concl (fn prems =>
   1.604            try_param_tac rN induct_scheme 1
   1.605            THEN try_param_tac "more" unit_induct 1
   1.606            THEN resolve_tac prems 1)
   1.607 @@ -1536,13 +1683,13 @@
   1.608      val induct = timeit_msg "record induct proof:" induct_prf;
   1.609  
   1.610      fun surjective_prf () = 
   1.611 -      prove_standard [] [] surjective_prop (fn prems =>
   1.612 +      prove_standard [] surjective_prop (fn prems =>
   1.613            (EVERY [try_param_tac rN induct_scheme 1,
   1.614                    simp_tac (ss addsimps sel_convs) 1]))
   1.615      val surjective = timeit_msg "record surjective proof:" surjective_prf;
   1.616  
   1.617      fun cases_scheme_prf () =
   1.618 -        prove_standard [] [] cases_scheme_prop (fn prems =>
   1.619 +        prove_standard [] cases_scheme_prop (fn prems =>
   1.620           EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
   1.621                 try_param_tac rN induct_scheme 1,
   1.622                 rtac impI 1,
   1.623 @@ -1552,13 +1699,13 @@
   1.624      val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
   1.625  
   1.626      fun cases_prf () =
   1.627 -      prove_standard [] [] cases_prop  (fn _ =>
   1.628 +      prove_standard [] cases_prop  (fn _ =>
   1.629          try_param_tac rN cases_scheme 1
   1.630          THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
   1.631      val cases = timeit_msg "record cases proof:" cases_prf;
   1.632  
   1.633      fun split_meta_prf () =
   1.634 -        prove_standard [] [] split_meta_prop (fn prems =>
   1.635 +        prove_standard [] split_meta_prop (fn prems =>
   1.636           EVERY [rtac equal_intr_rule 1,
   1.637                    rtac meta_allE 1, etac triv_goal 1, atac 1,
   1.638                  rtac (prop_subst OF [surjective]) 1,
   1.639 @@ -1567,7 +1714,7 @@
   1.640      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
   1.641  
   1.642      fun split_object_prf () =
   1.643 -        prove_standard [] [] split_object_prop (fn prems =>
   1.644 +        prove_standard [] split_object_prop (fn prems =>
   1.645           EVERY [rtac iffI 1, 
   1.646                  REPEAT (rtac allI 1), etac allE 1, atac 1,
   1.647                  rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
   1.648 @@ -1575,7 +1722,7 @@
   1.649  
   1.650  
   1.651      fun split_ex_prf () = 
   1.652 -        prove_standard [] [] split_ex_prop (fn prems =>
   1.653 +        prove_standard [] split_ex_prop (fn prems =>
   1.654            EVERY [rtac iffI 1,
   1.655                     etac exE 1,
   1.656                     simp_tac (HOL_basic_ss addsimps [split_meta]) 1,
   1.657 @@ -1592,14 +1739,14 @@
   1.658            val eqs' = map (simplify ss') eqs;
   1.659        in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end;
   1.660   
   1.661 -   fun equality_prf () = prove_standard [] [] equality_prop (fn _ =>
   1.662 +   fun equality_prf () = prove_standard [] equality_prop (fn _ =>
   1.663        fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
   1.664          st |> (res_inst_tac [(rN, s)] cases_scheme 1
   1.665          THEN res_inst_tac [(rN, s')] cases_scheme 1
   1.666          THEN (METAHYPS equality_tac 1)) 
   1.667               (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
   1.668        end);                              
   1.669 -     val equality = timeit_msg "record equality proof':" equality_prf;
   1.670 +     val equality = timeit_msg "record equality proof:" equality_prf;
   1.671  
   1.672      val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
   1.673                      derived_defs'],
   1.674 @@ -1632,6 +1779,8 @@
   1.675        |> put_record name (make_record_info args parent fields extension induct_scheme') 
   1.676        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
   1.677        |> add_record_equalities extension_id equality'
   1.678 +      |> add_extinjects ext_inject
   1.679 +      |> add_extsplit extension_name ext_split
   1.680        |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
   1.681        |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) 
   1.682        |> add_fieldext (extension_name,snd extension) (names @ [full_moreN])