Records:
authorschirmer
Thu Nov 06 20:45:02 2003 +0100 (2003-11-06)
changeset 14255e6e3e3f0deed
parent 14254 342634f38451
child 14256 33e5ef9a4c98
Records:
- Record types are now by default printed with their type abbreviation
instead of the list of all field types. This can be configured via
the reference "print_record_type_abbr".
- Simproc "record_upd_simproc" for simplification of multiple updates
added (not enabled by default).
- Tactic "record_split_simp_tac" to split and simplify records added.
- Bug-fix and optimisation of "record_simproc".
- "record_simproc" and "record_upd_simproc" are now sensitive to
quick_and_dirty flag.
NEWS
src/HOL/Tools/record_package.ML
src/Pure/Syntax/type_ext.ML
     1.1 --- a/NEWS	Thu Nov 06 14:18:05 2003 +0100
     1.2 +++ b/NEWS	Thu Nov 06 20:45:02 2003 +0100
     1.3 @@ -56,6 +56,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Records:
     1.8 +  - Record types are now by default printed with their type abbreviation
     1.9 +    instead of the list of all field types. This can be configured via
    1.10 +    the reference "print_record_type_abbr".
    1.11 +  - Simproc "record_upd_simproc" for simplification of multiple updates added 
    1.12 +    (not enabled by default).
    1.13 +  - Tactic "record_split_simp_tac" to split and simplify records added.
    1.14 + 
    1.15  * 'specification' command added, allowing for definition by
    1.16    specification.  There is also an 'ax_specification' command that
    1.17    introduces the new constants axiomatically.
     2.1 --- a/src/HOL/Tools/record_package.ML	Thu Nov 06 14:18:05 2003 +0100
     2.2 +++ b/src/HOL/Tools/record_package.ML	Thu Nov 06 20:45:02 2003 +0100
     2.3 @@ -13,6 +13,7 @@
     2.4    val record_split_tac: int -> tactic
     2.5    val record_split_name: string
     2.6    val record_split_wrapper: string * wrapper
     2.7 +  val print_record_type_abbr: bool ref 
     2.8  end;
     2.9  
    2.10  signature RECORD_PACKAGE =
    2.11 @@ -22,6 +23,8 @@
    2.12    val updateN: string
    2.13    val mk_fieldT: (string * typ) * typ -> typ
    2.14    val dest_fieldT: typ -> (string * typ) * typ
    2.15 +  val dest_fieldTs: typ -> (string * typ) list
    2.16 +  val last_fieldT: typ -> (string * typ) option
    2.17    val mk_field: (string * term) * term -> term
    2.18    val mk_fst: term -> term
    2.19    val mk_snd: term -> term
    2.20 @@ -36,9 +39,12 @@
    2.21    val add_record_i: (string list * bstring) -> (typ list * string) option
    2.22      -> (bstring * typ * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
    2.23    val setup: (theory -> theory) list
    2.24 +  val record_upd_simproc: simproc
    2.25 +  val record_split_simproc: (term -> bool) -> simproc
    2.26 +  val record_split_simp_tac: (term -> bool) -> int -> tactic
    2.27  end;
    2.28  
    2.29 -structure RecordPackage: RECORD_PACKAGE =
    2.30 +structure RecordPackage :RECORD_PACKAGE =
    2.31  struct
    2.32  
    2.33  
    2.34 @@ -170,6 +176,12 @@
    2.35    in (c, T) :: dest_fieldTs U
    2.36    end handle TYPE _ => [];
    2.37  
    2.38 +fun last_fieldT T =
    2.39 +  let val ((c, T), U) = dest_fieldT T
    2.40 +  in (case last_fieldT U of
    2.41 +        None => Some (c,T)
    2.42 +      | Some l => Some l)
    2.43 +  end handle TYPE _ => None
    2.44  
    2.45  (* morphisms *)
    2.46  
    2.47 @@ -313,6 +325,9 @@
    2.48  
    2.49  (* print translations *)
    2.50  
    2.51 +
    2.52 +val print_record_type_abbr = ref true;
    2.53 +
    2.54  fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
    2.55        (case try (unsuffix sfx) name_field of
    2.56          Some name =>
    2.57 @@ -334,6 +349,49 @@
    2.58    gen_record_tr' "_field_types" "_field_type" field_typeN
    2.59      (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme";
    2.60  
    2.61 +
    2.62 +(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
    2.63 +(* the (nested) field types.                                                        *)
    2.64 +fun record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT tm =
    2.65 +  let
    2.66 +      (* tm is term representation of a (nested) field type. We first reconstruct the      *)
    2.67 +      (* type from tm so that we can continue on the type level rather then the term level.*)
    2.68 + 
    2.69 +      fun get_sort xs n = (case assoc (xs,n) of 
    2.70 +                             Some s => s 
    2.71 +                           | None => Sign.defaultS sg);
    2.72 +
    2.73 +      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) 
    2.74 +      val {tsig,...} = Sign.rep_sg sg
    2.75 +
    2.76 +      fun mk_type_abbr subst name alphas = 
    2.77 +          let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
    2.78 +          in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
    2.79 +
    2.80 +      fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
    2.81 +
    2.82 +   in if !print_record_type_abbr
    2.83 +      then (case last_fieldT T of
    2.84 +             Some (name,_) 
    2.85 +              => if name = lastF 
    2.86 +                 then
    2.87 +		   let val subst = unify rec_schemeT T 
    2.88 +                   in 
    2.89 +                    if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
    2.90 +                    then mk_type_abbr subst abbr alphas
    2.91 +                    else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
    2.92 +		   end handle TUNIFY => record_type_tr' tm
    2.93 +                 else raise Match (* give print translation of specialised record a chance *)
    2.94 +            | _ => record_type_tr' tm)
    2.95 +       else record_type_tr' tm
    2.96 +  end
    2.97 +
    2.98 +     
    2.99 +fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT name =
   2.100 +  let val name_sfx = suffix field_typeN name
   2.101 +      val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT 
   2.102 +  in (name_sfx, fn [t,u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   2.103 +      
   2.104  val record_tr' =
   2.105    gen_record_tr' "_fields" "_field" fieldN
   2.106      (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme";
   2.107 @@ -344,23 +402,24 @@
   2.108        foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   2.109    end;
   2.110  
   2.111 -
   2.112  fun gen_field_tr' sfx tr' name =
   2.113    let val name_sfx = suffix sfx name
   2.114    in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   2.115  
   2.116  fun print_translation names =
   2.117 -  map (gen_field_tr' field_typeN record_type_tr') names @
   2.118    map (gen_field_tr' fieldN record_tr') names @
   2.119    map (gen_field_tr' updateN record_update_tr') names;
   2.120  
   2.121 +fun print_translation_field_types names =
   2.122 +  map (gen_field_tr' field_typeN record_type_tr') names
   2.123 +
   2.124  
   2.125  
   2.126  (*** extend theory by record definition ***)
   2.127  
   2.128  (** record info **)
   2.129  
   2.130 -(* type record_info and parent_info *)
   2.131 +(* type record_info and parent_info  *)
   2.132  
   2.133  type record_info =
   2.134   {args: (string * sort) list,
   2.135 @@ -368,22 +427,24 @@
   2.136    fields: (string * typ) list,
   2.137    field_inducts: thm list,
   2.138    field_cases: thm list,
   2.139 +  field_splits: thm list,
   2.140    simps: thm list};
   2.141  
   2.142 -fun make_record_info args parent fields field_inducts field_cases simps =
   2.143 +fun make_record_info args parent fields field_inducts field_cases field_splits simps =
   2.144   {args = args, parent = parent, fields = fields, field_inducts = field_inducts,
   2.145 -  field_cases = field_cases, simps = simps}: record_info;
   2.146 +  field_cases = field_cases, field_splits = field_splits, simps = simps}: record_info;
   2.147  
   2.148  type parent_info =
   2.149   {name: string,
   2.150    fields: (string * typ) list,
   2.151    field_inducts: thm list,
   2.152    field_cases: thm list,
   2.153 +  field_splits: thm list,
   2.154    simps: thm list};
   2.155  
   2.156 -fun make_parent_info name fields field_inducts field_cases simps =
   2.157 +fun make_parent_info name fields field_inducts field_cases field_splits simps =
   2.158   {name = name, fields = fields, field_inducts = field_inducts,
   2.159 -  field_cases = field_cases, simps = simps}: parent_info;
   2.160 +  field_cases = field_cases, field_splits = field_splits, simps = simps}: parent_info;
   2.161  
   2.162  
   2.163  (* data kind 'HOL/records' *)
   2.164 @@ -397,11 +458,13 @@
   2.165    field_splits:
   2.166     {fields: unit Symtab.table,
   2.167      simpset: Simplifier.simpset},
   2.168 -  equalities: thm Symtab.table};
   2.169 +  equalities: thm Symtab.table,
   2.170 +  splits: (thm*thm*thm*thm) Symtab.table (* !!,!,EX - split-equalities,induct rule *) 
   2.171 +};
   2.172  
   2.173 -fun make_record_data records sel_upd field_splits equalities=
   2.174 +fun make_record_data records sel_upd field_splits equalities splits =
   2.175   {records = records, sel_upd = sel_upd, field_splits = field_splits,
   2.176 -  equalities = equalities}: record_data;
   2.177 +  equalities = equalities, splits = splits}: record_data;
   2.178  
   2.179  structure RecordsArgs =
   2.180  struct
   2.181 @@ -411,7 +474,7 @@
   2.182    val empty =
   2.183      make_record_data Symtab.empty
   2.184        {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
   2.185 -      {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty;
   2.186 +      {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty Symtab.empty;
   2.187  
   2.188    val copy = I;
   2.189    val prep_ext = I;
   2.190 @@ -419,19 +482,25 @@
   2.191     ({records = recs1,
   2.192       sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
   2.193       field_splits = {fields = flds1, simpset = fld_ss1},
   2.194 -     equalities = equalities1},
   2.195 +     equalities = equalities1,
   2.196 +     splits = splits1},
   2.197      {records = recs2,
   2.198       sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
   2.199       field_splits = {fields = flds2, simpset = fld_ss2},
   2.200 -     equalities = equalities2}) =
   2.201 -    make_record_data
   2.202 +     equalities = equalities2, 
   2.203 +     splits = splits2}) =
   2.204 +    make_record_data  
   2.205        (Symtab.merge (K true) (recs1, recs2))
   2.206        {selectors = Symtab.merge (K true) (sels1, sels2),
   2.207          updates = Symtab.merge (K true) (upds1, upds2),
   2.208          simpset = Simplifier.merge_ss (ss1, ss2)}
   2.209        {fields = Symtab.merge (K true) (flds1, flds2),
   2.210          simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)}
   2.211 -      (Symtab.merge Thm.eq_thm (equalities1, equalities2));
   2.212 +      (Symtab.merge Thm.eq_thm (equalities1, equalities2))
   2.213 +      (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
   2.214 +                     => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
   2.215 +                        Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) 
   2.216 +                    (splits1, splits2));
   2.217  
   2.218    fun print sg ({records = recs, ...}: record_data) =
   2.219      let
   2.220 @@ -462,9 +531,9 @@
   2.221  
   2.222  fun put_record name info thy =
   2.223    let
   2.224 -    val {records, sel_upd, field_splits, equalities} = RecordsData.get thy;
   2.225 +    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   2.226      val data = make_record_data (Symtab.update ((name, info), records))
   2.227 -      sel_upd field_splits equalities;
   2.228 +      sel_upd field_splits equalities splits;
   2.229    in RecordsData.put data thy end;
   2.230  
   2.231  
   2.232 @@ -476,32 +545,31 @@
   2.233  fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name);
   2.234  fun get_simpset sg = #simpset (get_sel_upd sg);
   2.235  
   2.236 -
   2.237  fun put_sel_upd names simps thy =
   2.238    let
   2.239      val sels = map (rpair ()) names;
   2.240      val upds = map (suffix updateN) names ~~ names;
   2.241  
   2.242      val {records, sel_upd = {selectors, updates, simpset}, field_splits,
   2.243 -      equalities} = RecordsData.get thy;
   2.244 +      equalities, splits} = RecordsData.get thy;
   2.245      val data = make_record_data records
   2.246        {selectors = Symtab.extend (selectors, sels),
   2.247          updates = Symtab.extend (updates, upds),
   2.248          simpset = Simplifier.addsimps (simpset, simps)}
   2.249 -      field_splits equalities;
   2.250 +      field_splits equalities splits;
   2.251    in RecordsData.put data thy end;
   2.252  
   2.253  
   2.254  (* access 'field_splits' *)
   2.255  
   2.256 -fun add_record_splits names simps thy =
   2.257 +fun add_field_splits names simps thy =
   2.258    let
   2.259      val {records, sel_upd, field_splits = {fields, simpset},
   2.260 -      equalities} = RecordsData.get thy;
   2.261 +      equalities, splits} = RecordsData.get thy;
   2.262      val flds = map (rpair ()) names;
   2.263      val data = make_record_data records sel_upd
   2.264        {fields = Symtab.extend (fields, flds),
   2.265 -       simpset = Simplifier.addsimps (simpset, simps)} equalities;
   2.266 +       simpset = Simplifier.addsimps (simpset, simps)} equalities splits;
   2.267    in RecordsData.put data thy end;
   2.268  
   2.269  
   2.270 @@ -509,14 +577,26 @@
   2.271  
   2.272  fun add_record_equalities name thm thy =
   2.273    let
   2.274 -    val {records, sel_upd, field_splits, equalities} = RecordsData.get thy;
   2.275 +    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   2.276      val data = make_record_data records sel_upd field_splits
   2.277 -      (Symtab.update_new ((name, thm), equalities));
   2.278 +      (Symtab.update_new ((name, thm), equalities)) splits;
   2.279    in RecordsData.put data thy end;
   2.280  
   2.281  fun get_equalities sg name =
   2.282    Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
   2.283  
   2.284 +(* access 'splits' *)
   2.285 +
   2.286 +fun add_record_splits name thmP thy =
   2.287 +  let
   2.288 +    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   2.289 +    val data = make_record_data records sel_upd field_splits
   2.290 +      equalities (Symtab.update_new ((name, thmP), splits));
   2.291 +  in RecordsData.put data thy end;
   2.292 +
   2.293 +fun get_splits sg name =
   2.294 +  Symtab.lookup (#splits (RecordsData.get_sg sg), name);
   2.295 +
   2.296  
   2.297  (* parent records *)
   2.298  
   2.299 @@ -526,7 +606,7 @@
   2.300          val sign = Theory.sign_of thy;
   2.301          fun err msg = error (msg ^ " parent record " ^ quote name);
   2.302  
   2.303 -        val {args, parent, fields, field_inducts, field_cases, simps} =
   2.304 +        val {args, parent, fields, field_inducts, field_cases, field_splits, simps} =
   2.305            (case get_record thy name of Some info => info | None => err "Unknown");
   2.306          val _ = if length types <> length args then err "Bad number of arguments for" else ();
   2.307  
   2.308 @@ -542,60 +622,201 @@
   2.309          conditional (not (null bads)) (fn () =>
   2.310            err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
   2.311          add_parents thy parent'
   2.312 -          (make_parent_info name fields' field_inducts field_cases simps :: parents)
   2.313 +          (make_parent_info name fields' field_inducts field_cases field_splits simps::parents)
   2.314        end;
   2.315  
   2.316  
   2.317 +(** record simprocs **)
   2.318 + 
   2.319 +fun quick_and_dirty_prove sg xs asms prop tac =
   2.320 +Tactic.prove sg xs asms prop
   2.321 +    (if ! quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
   2.322  
   2.323 -(** record simproc **)
   2.324 +
   2.325 +fun prove_split_simp sg T prop =
   2.326 +    (case last_fieldT T of
   2.327 +      Some (name,_) => (case get_splits sg name of
   2.328 +                         Some (all_thm,_,_,_) 
   2.329 +                          => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
   2.330 +                             in (quick_and_dirty_prove sg [] [] prop 
   2.331 +                                  (K (simp_tac (simpset addsimps [all_thm]) 1)))
   2.332 +                             end
   2.333 +                      | _ => error "RecordPackage.prove_split_simp: code should never been reached")
   2.334 +     | _ => error "RecordPackage.prove_split_simp: code should never been reached")
   2.335 +
   2.336  
   2.337 +(* record_simproc *)
   2.338 +(* Simplifies selections of an record update:
   2.339 + *  (1)  S (r(|S:=k|)) = k respectively
   2.340 + *  (2)  S (r(|X:=k|)) = S r
   2.341 + * The simproc skips multiple updates at once, eg:
   2.342 + *  S (r (|S:=k,X:=2,Y:=3|)) = k
   2.343 + * But be careful in (2) because of the extendibility of records.
   2.344 + * - If S is a more-selector we have to make sure that the update on component
   2.345 + *   X does not affect the selected subrecord.
   2.346 + * - If X is a more-selector we have to make sure that S is not in the updated
   2.347 + *   subrecord. 
   2.348 + *)
   2.349  val record_simproc =
   2.350    Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
   2.351      (fn sg => fn _ => fn t =>
   2.352 -      (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
   2.353 +      (case t of (sel as Const (s, Type (_,[domS,rangeS]))) $ ((upd as Const (u, _)) $ k $ r) =>
   2.354          (case get_selectors sg s of Some () =>
   2.355            (case get_updates sg u of Some u_name =>
   2.356              let
   2.357 -              fun mk_free x t = Free (x, fastype_of t);
   2.358 -              val k' = mk_free "k" k;
   2.359 -              val r' = mk_free "r" r;
   2.360 -              val t' = sel $ (upd $ k' $ r');
   2.361 -              fun prove prop =
   2.362 -                Tactic.prove sg ["k", "r"] [] prop (K (simp_all_tac (get_simpset sg) []));
   2.363 +              fun mk_abs_var x t = (x, fastype_of t);
   2.364 +              val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
   2.365 +
   2.366 +              fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
   2.367 +		  (case (Symtab.lookup (updates,u)) of
   2.368 +                     None => None
   2.369 +                   | Some u_name 
   2.370 +                     => if u_name = s
   2.371 +                        then let 
   2.372 +                               val rv = mk_abs_var "r" r
   2.373 +                               val rb = Bound 0
   2.374 +                               val kv = mk_abs_var "k" k
   2.375 +                               val kb = Bound 1 
   2.376 +                             in Some (upd$kb$rb,kb,[kv,rv],true) end
   2.377 +                        else if u_name mem (map fst (dest_fieldTs rangeS))
   2.378 +                             orelse s mem (map fst (dest_fieldTs updT))
   2.379 +                             then None
   2.380 +			     else (case mk_eq_terms r of 
   2.381 +                                     Some (trm,trm',vars,update_s) 
   2.382 +                                     => let   
   2.383 +					  val kv = mk_abs_var "k" k
   2.384 +                                          val kb = Bound (length vars)
   2.385 +		                        in Some (upd$kb$trm,trm',kv::vars,update_s) end
   2.386 +                                   | None
   2.387 +                                     => let 
   2.388 +					  val rv = mk_abs_var "r" r
   2.389 +                                          val rb = Bound 0
   2.390 +                                          val kv = mk_abs_var "k" k
   2.391 +                                          val kb = Bound 1 
   2.392 +                                        in Some (upd$kb$rb,rb,[kv,rv],false) end))
   2.393 +                | mk_eq_terms r = None     
   2.394              in
   2.395 -              if u_name = s then Some (prove (Logic.mk_equals (t', k')))
   2.396 -              else Some (prove (Logic.mk_equals (t', sel $ r')))
   2.397 +	      (case mk_eq_terms (upd$k$r) of
   2.398 +                 Some (trm,trm',vars,update_s) 
   2.399 +                 => if update_s 
   2.400 +		    then Some (prove_split_simp sg domS 
   2.401 +                                 (list_all(vars,(Logic.mk_equals (sel$trm,trm')))))
   2.402 +                    else Some (prove_split_simp sg domS 
   2.403 +                                 (list_all(vars,(Logic.mk_equals (sel$trm,sel$trm')))))
   2.404 +               | None => None)
   2.405              end
   2.406            | None => None)
   2.407          | None => None)
   2.408        | _ => None));
   2.409  
   2.410 +(* record_eq_simproc *)
   2.411 +(* looks up the most specific record-equality.
   2.412 + * Note on efficiency:
   2.413 + * Testing equality of records boils down to the test of equality of all components.
   2.414 + * Therefore the complexity is: #components * complexity for single component.
   2.415 + * Especially if a record has a lot of components it may be better to split up
   2.416 + * the record first and do simplification on that (record_split_simp_tac).
   2.417 + * e.g. r(|lots of updates|) = x
   2.418 + *
   2.419 + *               record_eq_simproc           record_split_simp_tac
   2.420 + * Complexity: #components * #updates     #updates   
   2.421 + *           
   2.422 + *)
   2.423  val record_eq_simproc =
   2.424    Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
   2.425      (fn sg => fn _ => fn t =>
   2.426        (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
   2.427 -        (case rev (dest_fieldTs T) of
   2.428 -           [] => None
   2.429 -         | (name, _) :: _ => (case get_equalities sg name of
   2.430 -             None => None
   2.431 -           | Some thm => Some (thm RS Eq_TrueI)))
   2.432 +        (case last_fieldT T of
   2.433 +           None => None
   2.434 +         | Some (name, _) => (case get_equalities sg name of
   2.435 +                                None => None
   2.436 +                              | Some thm => Some (thm RS Eq_TrueI)))
   2.437         | _ => None));
   2.438  
   2.439  
   2.440 +(* record_upd_simproc *)
   2.441 +(* simplify multiple updates; for example: "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" *)
   2.442 +val record_upd_simproc =
   2.443 +  Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u1 k1 (u2 k2 r))"]
   2.444 +    (fn sg => fn _ => fn t =>
   2.445 +      (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
   2.446 + 	 let val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
   2.447 +	     fun mk_abs_var x t = (x, fastype_of t);
   2.448 +
   2.449 +             fun mk_updterm upds already ((upd as Const (u,_)) $ k $ r) =
   2.450 +		 if is_some (Symtab.lookup (upds,u))
   2.451 +		 then let 
   2.452 +			 fun rest already = mk_updterm upds already
   2.453 +		      in if is_some (Symtab.lookup (already,u)) 
   2.454 +			 then (case (rest already r) of
   2.455 +				 None => let 
   2.456 +				           val rv = mk_abs_var "r" r
   2.457 +                                           val rb = Bound 0
   2.458 +					   val kv = mk_abs_var "k" k
   2.459 +                                           val kb = Bound 1	      
   2.460 +                                         in Some (upd$kb$rb,rb,[kv,rv]) end
   2.461 +                               | Some (trm,trm',vars) 
   2.462 +				 => let 
   2.463 +				     val kv = mk_abs_var "k" k
   2.464 +                                     val kb = Bound (length vars)
   2.465 +                                    in Some (upd$kb$trm,trm',kv::vars) end)
   2.466 +	                 else (case rest (Symtab.update ((u,()),already)) r of 
   2.467 +				 None => None
   2.468 +		               | Some (trm,trm',vars) 
   2.469 +                                  => let
   2.470 +				      val kv = mk_abs_var "k" k
   2.471 +                                      val kb = Bound (length vars)
   2.472 +                                     in Some (upd$kb$trm,upd$kb$trm',kv::vars) end)
   2.473 +		     end
   2.474 +		 else None
   2.475 +	       | mk_updterm _ _ _ = None;
   2.476 +
   2.477 +	 in (case mk_updterm updates Symtab.empty t of
   2.478 +	       Some (trm,trm',vars)
   2.479 +                => Some (prove_split_simp sg T (list_all(vars,(Logic.mk_equals (trm,trm')))))
   2.480 +             | None => None)
   2.481 +	 end
   2.482 +       | _ => None));
   2.483 +
   2.484 +(* record_split_simproc *)
   2.485 +(* splits quantified occurrences of records, for which P holds. P can peek on the 
   2.486 + * subterm starting at the quantified occurrence of the record (including the quantifier)
   2.487 + *)
   2.488 +fun record_split_simproc P =
   2.489 +  Simplifier.simproc (Theory.sign_of HOL.thy) "record_split_simp" ["(a t)"]
   2.490 +    (fn sg => fn _ => fn t =>
   2.491 +      (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
   2.492 +         if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
   2.493 +         then (case last_fieldT T of
   2.494 +                 None => None
   2.495 +               | Some (name, _)
   2.496 +                  => if P t 
   2.497 +                     then (case get_splits sg name of
   2.498 +                             None => None
   2.499 +                           | Some (all_thm, All_thm, Ex_thm,_) 
   2.500 +                              => Some (case quantifier of
   2.501 +                                         "all" => all_thm
   2.502 +                                       | "All" => All_thm RS HOL.eq_reflection
   2.503 +                                       | "Ex"  => Ex_thm RS HOL.eq_reflection
   2.504 +                                       | _     => error "record_split_simproc"))
   2.505 +                     else None)
   2.506 +         else None
   2.507 +       | _ => None))
   2.508  
   2.509  (** record field splitting **)
   2.510  
   2.511  (* tactic *)
   2.512  
   2.513 +fun is_fieldT fields (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
   2.514 +  | is_fieldT _ _ = false;
   2.515 +
   2.516  fun record_split_tac i st =
   2.517    let
   2.518      val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st);
   2.519  
   2.520 -    fun is_fieldT (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
   2.521 -      | is_fieldT _ = false;
   2.522      val has_field = exists_Const
   2.523        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   2.524 -          (s = "all" orelse s = "All") andalso is_fieldT T
   2.525 +          (s = "all" orelse s = "All") andalso is_fieldT fields T
   2.526          | _ => false);
   2.527  
   2.528      val goal = Library.nth_elem (i - 1, Thm.prems_of st);
   2.529 @@ -605,6 +826,60 @@
   2.530    end handle Library.LIST _ => Seq.empty;
   2.531  
   2.532  
   2.533 +local
   2.534 +val inductive_atomize = thms "induct_atomize";
   2.535 +val inductive_rulify1 = thms "induct_rulify1";
   2.536 +in
   2.537 +(* record_split_simp_tac *)
   2.538 +(* splits (and simplifies) all records in the goal for which P holds. 
   2.539 + * For quantified occurrences of a record
   2.540 + * P can peek on the whole subterm (including the quantifier); for free variables P
   2.541 + * can only peek on the variable itself. 
   2.542 + *)
   2.543 +fun record_split_simp_tac P i st =
   2.544 +  let
   2.545 +    val sg = Thm.sign_of_thm st;
   2.546 +    val {sel_upd={simpset,...},field_splits={fields,...},...} 
   2.547 +            = RecordsData.get_sg sg;
   2.548 +
   2.549 +    val has_field = exists_Const
   2.550 +      (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   2.551 +          (s = "all" orelse s = "All" orelse s = "Ex") andalso is_fieldT fields T
   2.552 +        | _ => false);
   2.553 +
   2.554 +    val goal = Library.nth_elem (i - 1, Thm.prems_of st);
   2.555 +    val frees = filter (is_fieldT fields o type_of) (term_frees goal);
   2.556 +
   2.557 +    fun mk_split_free_tac free induct_thm i = 
   2.558 +	let val cfree = cterm_of sg free;
   2.559 +            val (_$(_$r)) = concl_of induct_thm;
   2.560 +            val crec = cterm_of sg r;
   2.561 +            val thm  = cterm_instantiate [(crec,cfree)] induct_thm;
   2.562 +        in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
   2.563 +                  rtac thm i,
   2.564 +                  simp_tac (HOL_basic_ss addsimps inductive_rulify1) i]
   2.565 +	end;
   2.566 +
   2.567 +    fun split_free_tac P i (free as Free (n,T)) = 
   2.568 +	(case last_fieldT T of
   2.569 +           None => None
   2.570 +         | Some(name,_)=> if P free 
   2.571 +                          then (case get_splits sg name of
   2.572 +                                  None => None
   2.573 +                                | Some (_,_,_,induct_thm)
   2.574 +                                   => Some (mk_split_free_tac free induct_thm i))
   2.575 +                          else None)
   2.576 +     | split_free_tac _ _ _ = None;
   2.577 +
   2.578 +    val split_frees_tacs = mapfilter (split_free_tac P i) frees;
   2.579 +   
   2.580 +    val simprocs = if has_field goal then [record_split_simproc P] else [];
   2.581 +   
   2.582 +  in st |> (EVERY split_frees_tacs) 
   2.583 +           THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i)
   2.584 +  end handle Library.LIST _ => Seq.empty;
   2.585 +end;
   2.586 +
   2.587  (* wrapper *)
   2.588  
   2.589  val record_split_name = "record_split_tac";
   2.590 @@ -778,12 +1053,22 @@
   2.591      fun r_scheme n = Free (rN, rec_schemeT n);
   2.592      fun r n = Free (rN, recT n);
   2.593  
   2.594 +    
   2.595  
   2.596      (* prepare print translation functions *)
   2.597 -
   2.598      val field_tr's =
   2.599        print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
   2.600  
   2.601 +    val field_type_tr's = 
   2.602 +	let val fldnames = if parent_len = 0 then (tl names) else names;
   2.603 +        in print_translation_field_types (distinct (flat (map NameSpace.accesses' fldnames))) 
   2.604 +        end;
   2.605 +                          
   2.606 +    fun record_type_abbr_tr's thy =
   2.607 +	let val trnames = (distinct (flat (map NameSpace.accesses' [hd all_names])))
   2.608 +            val sg = Theory.sign_of thy
   2.609 +	in map (gen_record_type_abbr_tr' 
   2.610 +                 sg bname alphas zeta (hd (rev names)) (recT 0) (rec_schemeT 0)) trnames end;   
   2.611  
   2.612      (* prepare declarations *)
   2.613  
   2.614 @@ -879,7 +1164,33 @@
   2.615          ((r_scheme n === rec_scheme n) ==> C) ==> C;
   2.616      fun cases_prop n = All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C;
   2.617  
   2.618 +    (*split*)
   2.619 +    fun split_scheme_meta_prop n =
   2.620 +      let val P = Free ("P", rec_schemeT n --> Term.propT) in
   2.621 +       equals (Term.propT) $
   2.622 +        (Term.list_all_free ([(rN,rec_schemeT n)],(P $ r_scheme n)))$
   2.623 +        (All (prune n all_xs_more ~~ prune n all_types_more) (P $ rec_scheme n))
   2.624 +      end;
   2.625  
   2.626 +    fun split_scheme_object_prop n =
   2.627 +      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
   2.628 +          val ALL = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) 
   2.629 +      in
   2.630 +	Trueprop (
   2.631 +           HOLogic.eq_const (HOLogic.boolT) $
   2.632 +            (HOLogic.mk_all ((rN,rec_schemeT n,P $ r_scheme n)))$
   2.633 +            (ALL (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
   2.634 +      end;
   2.635 +
   2.636 +      fun split_scheme_object_ex_prop n =
   2.637 +      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
   2.638 +          val EX = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) 
   2.639 +      in
   2.640 +	Trueprop (
   2.641 +           HOLogic.eq_const (HOLogic.boolT) $
   2.642 +            (HOLogic.mk_exists ((rN,rec_schemeT n,P $ r_scheme n)))$
   2.643 +            (EX (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
   2.644 +      end;
   2.645      (* 1st stage: fields_thy *)
   2.646  
   2.647      val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) =
   2.648 @@ -889,17 +1200,22 @@
   2.649  
   2.650      val all_field_inducts = flat (map #field_inducts parents) @ field_inducts;
   2.651      val all_field_cases = flat (map #field_cases parents) @ field_cases;
   2.652 -
   2.653 +    val all_field_splits = flat (map #field_splits parents) @ field_splits
   2.654  
   2.655 +    
   2.656      (* 2nd stage: defs_thy *)
   2.657  
   2.658 +        
   2.659 +   
   2.660 +
   2.661      val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
   2.662        fields_thy
   2.663 -      |> add_record_splits (map (suffix field_typeN) names) field_splits
   2.664 +      |> Theory.add_trfuns 
   2.665 +           ([],[],record_type_abbr_tr's fields_thy @ field_type_tr's @ field_tr's, [])
   2.666 +      |> add_field_splits (map (suffix field_typeN) names) field_splits
   2.667        |> Theory.parent_path
   2.668        |> Theory.add_tyabbrs_i recordT_specs
   2.669        |> Theory.add_path bname
   2.670 -      |> Theory.add_trfuns ([], [], field_tr's, [])
   2.671        |> Theory.add_consts_i
   2.672          (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
   2.673        |> (Theory.add_consts_i o map Syntax.no_syn)
   2.674 @@ -935,12 +1251,32 @@
   2.675          EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_cases))
   2.676          THEN simp_all_tac HOL_basic_ss []);
   2.677  
   2.678 +    fun split_scheme_meta n =
   2.679 +      prove_standard [] [] (split_scheme_meta_prop n) (fn _ =>
   2.680 +        Simplifier.full_simp_tac (HOL_basic_ss addsimps all_field_splits) 1);
   2.681 +
   2.682 +    fun split_scheme_object induct_scheme n =
   2.683 +      prove_standard [] [] (split_scheme_object_prop n) (fn _ =>
   2.684 +         EVERY [rtac iffI 1, 
   2.685 +                REPEAT (rtac allI 1), etac allE 1, atac 1,
   2.686 +                rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
   2.687 +
   2.688 +    fun split_scheme_object_ex split_scheme_meta n =
   2.689 +      prove_standard [] [] (split_scheme_object_ex_prop n) (fn _ =>
   2.690 +        fast_simp_tac (claset_of HOL.thy,
   2.691 +                       HOL_basic_ss addsimps [split_scheme_meta]) 1);
   2.692 +       
   2.693      val induct_scheme0 = induct_scheme 0;
   2.694      val cases_scheme0 = cases_scheme 0;
   2.695 +    val split_scheme_meta0 = split_scheme_meta 0;
   2.696 +    val split_scheme_object0 = split_scheme_object induct_scheme0 0;
   2.697 +    val split_scheme_object_ex0 = split_scheme_object_ex split_scheme_meta0 0;
   2.698      val more_induct_scheme = map induct_scheme ancestry;
   2.699      val more_cases_scheme = map cases_scheme ancestry;
   2.700  
   2.701 -    val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _],
   2.702 +    val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _, 
   2.703 +                      [split_scheme_meta',split_scheme_object',
   2.704 +                       split_scheme_object_ex',split_scheme_free']],
   2.705          [induct_scheme', cases_scheme']), [more_induct_scheme', more_cases_scheme'])) =
   2.706        defs_thy
   2.707        |> (PureThy.add_thmss o map Thm.no_attributes)
   2.708 @@ -948,7 +1284,9 @@
   2.709          ("update_convs", update_convs),
   2.710          ("select_defs", sel_defs),
   2.711          ("update_defs", update_defs),
   2.712 -        ("defs", derived_defs)]
   2.713 +        ("defs", derived_defs),
   2.714 +        ("splits",[split_scheme_meta0,split_scheme_object0,
   2.715 +                   split_scheme_object_ex0,induct_scheme0])]
   2.716        |>>> PureThy.add_thms
   2.717         [(("induct_scheme", induct_scheme0), induct_type_global (suffix schemeN name)),
   2.718          (("cases_scheme", cases_scheme0), cases_type_global (suffix schemeN name))]
   2.719 @@ -1009,9 +1347,12 @@
   2.720      val final_thy =
   2.721        more_thms_thy'
   2.722        |> put_record name (make_record_info args parent fields field_inducts field_cases
   2.723 -        (field_simps @ simps))
   2.724 -      |> put_sel_upd (names @ [full_moreN]) (field_simps @ sel_defs' @ update_defs')
   2.725 +          field_splits (field_simps @ simps))
   2.726 +      |> put_sel_upd (names @ [full_moreN]) simps
   2.727        |> add_record_equalities (snd (split_last names)) equality'
   2.728 +      |> add_record_splits (snd (split_last names)) 
   2.729 +                           (split_scheme_meta',split_scheme_object',
   2.730 +                            split_scheme_object_ex',split_scheme_free')
   2.731        |> Theory.parent_path;
   2.732  
   2.733    in (final_thy, {simps = simps, iffs = iffs}) end;
   2.734 @@ -1129,7 +1470,6 @@
   2.735  val add_record_i = gen_add_record cert_typ (K I);
   2.736  
   2.737  
   2.738 -
   2.739  (** package setup **)
   2.740  
   2.741  (* setup theory *)
     3.1 --- a/src/Pure/Syntax/type_ext.ML	Thu Nov 06 14:18:05 2003 +0100
     3.2 +++ b/src/Pure/Syntax/type_ext.ML	Thu Nov 06 20:45:02 2003 +0100
     3.3 @@ -44,6 +44,7 @@
     3.4      fun sort (Const ("_topsort", _)) = []
     3.5        | sort (Const (c, _)) = [c]
     3.6        | sort (Free (c, _)) = [c]
     3.7 +      | sort (Const ("_class",_) $ Free (c, _)) = [c]
     3.8        | sort (Const ("_sort", _) $ cs) = classes cs
     3.9        | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
    3.10    in sort tm end;
    3.11 @@ -54,7 +55,11 @@
    3.12  fun raw_term_sorts tm =
    3.13    let
    3.14      fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort_of_term cs) ins env
    3.15 +      | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env 
    3.16 +                = ((x, ~1), sort_of_term cs) ins env
    3.17        | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort_of_term cs) ins env
    3.18 +      | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env 
    3.19 +                = (xi, sort_of_term cs) ins env
    3.20        | add_env (Abs (_, _, t)) env = add_env t env
    3.21        | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
    3.22        | add_env t env = env;
    3.23 @@ -69,9 +74,16 @@
    3.24            if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
    3.25            else Type (x, [])
    3.26        | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    3.27 +      | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
    3.28 +      | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
    3.29        | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
    3.30 +      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) 
    3.31 +               = TFree (x, get_sort (x, ~1))
    3.32        | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
    3.33 +      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) 
    3.34 +               = TVar (xi, get_sort xi)
    3.35        | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", map_sort (sort_of_term t))
    3.36 +     
    3.37        | typ_of tm =
    3.38            let
    3.39              val (t, ts) = strip_comb tm;