src/HOL/Tools/record_package.ML
changeset 14255 e6e3e3f0deed
parent 14079 1c22e5499eeb
child 14358 233c5bd5b539
     1.1 --- a/src/HOL/Tools/record_package.ML	Thu Nov 06 14:18:05 2003 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Thu Nov 06 20:45:02 2003 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4    val record_split_tac: int -> tactic
     1.5    val record_split_name: string
     1.6    val record_split_wrapper: string * wrapper
     1.7 +  val print_record_type_abbr: bool ref 
     1.8  end;
     1.9  
    1.10  signature RECORD_PACKAGE =
    1.11 @@ -22,6 +23,8 @@
    1.12    val updateN: string
    1.13    val mk_fieldT: (string * typ) * typ -> typ
    1.14    val dest_fieldT: typ -> (string * typ) * typ
    1.15 +  val dest_fieldTs: typ -> (string * typ) list
    1.16 +  val last_fieldT: typ -> (string * typ) option
    1.17    val mk_field: (string * term) * term -> term
    1.18    val mk_fst: term -> term
    1.19    val mk_snd: term -> term
    1.20 @@ -36,9 +39,12 @@
    1.21    val add_record_i: (string list * bstring) -> (typ list * string) option
    1.22      -> (bstring * typ * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
    1.23    val setup: (theory -> theory) list
    1.24 +  val record_upd_simproc: simproc
    1.25 +  val record_split_simproc: (term -> bool) -> simproc
    1.26 +  val record_split_simp_tac: (term -> bool) -> int -> tactic
    1.27  end;
    1.28  
    1.29 -structure RecordPackage: RECORD_PACKAGE =
    1.30 +structure RecordPackage :RECORD_PACKAGE =
    1.31  struct
    1.32  
    1.33  
    1.34 @@ -170,6 +176,12 @@
    1.35    in (c, T) :: dest_fieldTs U
    1.36    end handle TYPE _ => [];
    1.37  
    1.38 +fun last_fieldT T =
    1.39 +  let val ((c, T), U) = dest_fieldT T
    1.40 +  in (case last_fieldT U of
    1.41 +        None => Some (c,T)
    1.42 +      | Some l => Some l)
    1.43 +  end handle TYPE _ => None
    1.44  
    1.45  (* morphisms *)
    1.46  
    1.47 @@ -313,6 +325,9 @@
    1.48  
    1.49  (* print translations *)
    1.50  
    1.51 +
    1.52 +val print_record_type_abbr = ref true;
    1.53 +
    1.54  fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
    1.55        (case try (unsuffix sfx) name_field of
    1.56          Some name =>
    1.57 @@ -334,6 +349,49 @@
    1.58    gen_record_tr' "_field_types" "_field_type" field_typeN
    1.59      (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme";
    1.60  
    1.61 +
    1.62 +(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
    1.63 +(* the (nested) field types.                                                        *)
    1.64 +fun record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT tm =
    1.65 +  let
    1.66 +      (* tm is term representation of a (nested) field type. We first reconstruct the      *)
    1.67 +      (* type from tm so that we can continue on the type level rather then the term level.*)
    1.68 + 
    1.69 +      fun get_sort xs n = (case assoc (xs,n) of 
    1.70 +                             Some s => s 
    1.71 +                           | None => Sign.defaultS sg);
    1.72 +
    1.73 +      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) 
    1.74 +      val {tsig,...} = Sign.rep_sg sg
    1.75 +
    1.76 +      fun mk_type_abbr subst name alphas = 
    1.77 +          let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
    1.78 +          in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
    1.79 +
    1.80 +      fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
    1.81 +
    1.82 +   in if !print_record_type_abbr
    1.83 +      then (case last_fieldT T of
    1.84 +             Some (name,_) 
    1.85 +              => if name = lastF 
    1.86 +                 then
    1.87 +		   let val subst = unify rec_schemeT T 
    1.88 +                   in 
    1.89 +                    if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
    1.90 +                    then mk_type_abbr subst abbr alphas
    1.91 +                    else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
    1.92 +		   end handle TUNIFY => record_type_tr' tm
    1.93 +                 else raise Match (* give print translation of specialised record a chance *)
    1.94 +            | _ => record_type_tr' tm)
    1.95 +       else record_type_tr' tm
    1.96 +  end
    1.97 +
    1.98 +     
    1.99 +fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT name =
   1.100 +  let val name_sfx = suffix field_typeN name
   1.101 +      val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT 
   1.102 +  in (name_sfx, fn [t,u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   1.103 +      
   1.104  val record_tr' =
   1.105    gen_record_tr' "_fields" "_field" fieldN
   1.106      (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme";
   1.107 @@ -344,23 +402,24 @@
   1.108        foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   1.109    end;
   1.110  
   1.111 -
   1.112  fun gen_field_tr' sfx tr' name =
   1.113    let val name_sfx = suffix sfx name
   1.114    in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   1.115  
   1.116  fun print_translation names =
   1.117 -  map (gen_field_tr' field_typeN record_type_tr') names @
   1.118    map (gen_field_tr' fieldN record_tr') names @
   1.119    map (gen_field_tr' updateN record_update_tr') names;
   1.120  
   1.121 +fun print_translation_field_types names =
   1.122 +  map (gen_field_tr' field_typeN record_type_tr') names
   1.123 +
   1.124  
   1.125  
   1.126  (*** extend theory by record definition ***)
   1.127  
   1.128  (** record info **)
   1.129  
   1.130 -(* type record_info and parent_info *)
   1.131 +(* type record_info and parent_info  *)
   1.132  
   1.133  type record_info =
   1.134   {args: (string * sort) list,
   1.135 @@ -368,22 +427,24 @@
   1.136    fields: (string * typ) list,
   1.137    field_inducts: thm list,
   1.138    field_cases: thm list,
   1.139 +  field_splits: thm list,
   1.140    simps: thm list};
   1.141  
   1.142 -fun make_record_info args parent fields field_inducts field_cases simps =
   1.143 +fun make_record_info args parent fields field_inducts field_cases field_splits simps =
   1.144   {args = args, parent = parent, fields = fields, field_inducts = field_inducts,
   1.145 -  field_cases = field_cases, simps = simps}: record_info;
   1.146 +  field_cases = field_cases, field_splits = field_splits, simps = simps}: record_info;
   1.147  
   1.148  type parent_info =
   1.149   {name: string,
   1.150    fields: (string * typ) list,
   1.151    field_inducts: thm list,
   1.152    field_cases: thm list,
   1.153 +  field_splits: thm list,
   1.154    simps: thm list};
   1.155  
   1.156 -fun make_parent_info name fields field_inducts field_cases simps =
   1.157 +fun make_parent_info name fields field_inducts field_cases field_splits simps =
   1.158   {name = name, fields = fields, field_inducts = field_inducts,
   1.159 -  field_cases = field_cases, simps = simps}: parent_info;
   1.160 +  field_cases = field_cases, field_splits = field_splits, simps = simps}: parent_info;
   1.161  
   1.162  
   1.163  (* data kind 'HOL/records' *)
   1.164 @@ -397,11 +458,13 @@
   1.165    field_splits:
   1.166     {fields: unit Symtab.table,
   1.167      simpset: Simplifier.simpset},
   1.168 -  equalities: thm Symtab.table};
   1.169 +  equalities: thm Symtab.table,
   1.170 +  splits: (thm*thm*thm*thm) Symtab.table (* !!,!,EX - split-equalities,induct rule *) 
   1.171 +};
   1.172  
   1.173 -fun make_record_data records sel_upd field_splits equalities=
   1.174 +fun make_record_data records sel_upd field_splits equalities splits =
   1.175   {records = records, sel_upd = sel_upd, field_splits = field_splits,
   1.176 -  equalities = equalities}: record_data;
   1.177 +  equalities = equalities, splits = splits}: record_data;
   1.178  
   1.179  structure RecordsArgs =
   1.180  struct
   1.181 @@ -411,7 +474,7 @@
   1.182    val empty =
   1.183      make_record_data Symtab.empty
   1.184        {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
   1.185 -      {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty;
   1.186 +      {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty Symtab.empty;
   1.187  
   1.188    val copy = I;
   1.189    val prep_ext = I;
   1.190 @@ -419,19 +482,25 @@
   1.191     ({records = recs1,
   1.192       sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
   1.193       field_splits = {fields = flds1, simpset = fld_ss1},
   1.194 -     equalities = equalities1},
   1.195 +     equalities = equalities1,
   1.196 +     splits = splits1},
   1.197      {records = recs2,
   1.198       sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
   1.199       field_splits = {fields = flds2, simpset = fld_ss2},
   1.200 -     equalities = equalities2}) =
   1.201 -    make_record_data
   1.202 +     equalities = equalities2, 
   1.203 +     splits = splits2}) =
   1.204 +    make_record_data  
   1.205        (Symtab.merge (K true) (recs1, recs2))
   1.206        {selectors = Symtab.merge (K true) (sels1, sels2),
   1.207          updates = Symtab.merge (K true) (upds1, upds2),
   1.208          simpset = Simplifier.merge_ss (ss1, ss2)}
   1.209        {fields = Symtab.merge (K true) (flds1, flds2),
   1.210          simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)}
   1.211 -      (Symtab.merge Thm.eq_thm (equalities1, equalities2));
   1.212 +      (Symtab.merge Thm.eq_thm (equalities1, equalities2))
   1.213 +      (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
   1.214 +                     => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
   1.215 +                        Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) 
   1.216 +                    (splits1, splits2));
   1.217  
   1.218    fun print sg ({records = recs, ...}: record_data) =
   1.219      let
   1.220 @@ -462,9 +531,9 @@
   1.221  
   1.222  fun put_record name info thy =
   1.223    let
   1.224 -    val {records, sel_upd, field_splits, equalities} = RecordsData.get thy;
   1.225 +    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   1.226      val data = make_record_data (Symtab.update ((name, info), records))
   1.227 -      sel_upd field_splits equalities;
   1.228 +      sel_upd field_splits equalities splits;
   1.229    in RecordsData.put data thy end;
   1.230  
   1.231  
   1.232 @@ -476,32 +545,31 @@
   1.233  fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name);
   1.234  fun get_simpset sg = #simpset (get_sel_upd sg);
   1.235  
   1.236 -
   1.237  fun put_sel_upd names simps thy =
   1.238    let
   1.239      val sels = map (rpair ()) names;
   1.240      val upds = map (suffix updateN) names ~~ names;
   1.241  
   1.242      val {records, sel_upd = {selectors, updates, simpset}, field_splits,
   1.243 -      equalities} = RecordsData.get thy;
   1.244 +      equalities, splits} = RecordsData.get thy;
   1.245      val data = make_record_data records
   1.246        {selectors = Symtab.extend (selectors, sels),
   1.247          updates = Symtab.extend (updates, upds),
   1.248          simpset = Simplifier.addsimps (simpset, simps)}
   1.249 -      field_splits equalities;
   1.250 +      field_splits equalities splits;
   1.251    in RecordsData.put data thy end;
   1.252  
   1.253  
   1.254  (* access 'field_splits' *)
   1.255  
   1.256 -fun add_record_splits names simps thy =
   1.257 +fun add_field_splits names simps thy =
   1.258    let
   1.259      val {records, sel_upd, field_splits = {fields, simpset},
   1.260 -      equalities} = RecordsData.get thy;
   1.261 +      equalities, splits} = RecordsData.get thy;
   1.262      val flds = map (rpair ()) names;
   1.263      val data = make_record_data records sel_upd
   1.264        {fields = Symtab.extend (fields, flds),
   1.265 -       simpset = Simplifier.addsimps (simpset, simps)} equalities;
   1.266 +       simpset = Simplifier.addsimps (simpset, simps)} equalities splits;
   1.267    in RecordsData.put data thy end;
   1.268  
   1.269  
   1.270 @@ -509,14 +577,26 @@
   1.271  
   1.272  fun add_record_equalities name thm thy =
   1.273    let
   1.274 -    val {records, sel_upd, field_splits, equalities} = RecordsData.get thy;
   1.275 +    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   1.276      val data = make_record_data records sel_upd field_splits
   1.277 -      (Symtab.update_new ((name, thm), equalities));
   1.278 +      (Symtab.update_new ((name, thm), equalities)) splits;
   1.279    in RecordsData.put data thy end;
   1.280  
   1.281  fun get_equalities sg name =
   1.282    Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
   1.283  
   1.284 +(* access 'splits' *)
   1.285 +
   1.286 +fun add_record_splits name thmP thy =
   1.287 +  let
   1.288 +    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   1.289 +    val data = make_record_data records sel_upd field_splits
   1.290 +      equalities (Symtab.update_new ((name, thmP), splits));
   1.291 +  in RecordsData.put data thy end;
   1.292 +
   1.293 +fun get_splits sg name =
   1.294 +  Symtab.lookup (#splits (RecordsData.get_sg sg), name);
   1.295 +
   1.296  
   1.297  (* parent records *)
   1.298  
   1.299 @@ -526,7 +606,7 @@
   1.300          val sign = Theory.sign_of thy;
   1.301          fun err msg = error (msg ^ " parent record " ^ quote name);
   1.302  
   1.303 -        val {args, parent, fields, field_inducts, field_cases, simps} =
   1.304 +        val {args, parent, fields, field_inducts, field_cases, field_splits, simps} =
   1.305            (case get_record thy name of Some info => info | None => err "Unknown");
   1.306          val _ = if length types <> length args then err "Bad number of arguments for" else ();
   1.307  
   1.308 @@ -542,60 +622,201 @@
   1.309          conditional (not (null bads)) (fn () =>
   1.310            err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
   1.311          add_parents thy parent'
   1.312 -          (make_parent_info name fields' field_inducts field_cases simps :: parents)
   1.313 +          (make_parent_info name fields' field_inducts field_cases field_splits simps::parents)
   1.314        end;
   1.315  
   1.316  
   1.317 +(** record simprocs **)
   1.318 + 
   1.319 +fun quick_and_dirty_prove sg xs asms prop tac =
   1.320 +Tactic.prove sg xs asms prop
   1.321 +    (if ! quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
   1.322  
   1.323 -(** record simproc **)
   1.324 +
   1.325 +fun prove_split_simp sg T prop =
   1.326 +    (case last_fieldT T of
   1.327 +      Some (name,_) => (case get_splits sg name of
   1.328 +                         Some (all_thm,_,_,_) 
   1.329 +                          => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
   1.330 +                             in (quick_and_dirty_prove sg [] [] prop 
   1.331 +                                  (K (simp_tac (simpset addsimps [all_thm]) 1)))
   1.332 +                             end
   1.333 +                      | _ => error "RecordPackage.prove_split_simp: code should never been reached")
   1.334 +     | _ => error "RecordPackage.prove_split_simp: code should never been reached")
   1.335 +
   1.336  
   1.337 +(* record_simproc *)
   1.338 +(* Simplifies selections of an record update:
   1.339 + *  (1)  S (r(|S:=k|)) = k respectively
   1.340 + *  (2)  S (r(|X:=k|)) = S r
   1.341 + * The simproc skips multiple updates at once, eg:
   1.342 + *  S (r (|S:=k,X:=2,Y:=3|)) = k
   1.343 + * But be careful in (2) because of the extendibility of records.
   1.344 + * - If S is a more-selector we have to make sure that the update on component
   1.345 + *   X does not affect the selected subrecord.
   1.346 + * - If X is a more-selector we have to make sure that S is not in the updated
   1.347 + *   subrecord. 
   1.348 + *)
   1.349  val record_simproc =
   1.350    Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
   1.351      (fn sg => fn _ => fn t =>
   1.352 -      (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
   1.353 +      (case t of (sel as Const (s, Type (_,[domS,rangeS]))) $ ((upd as Const (u, _)) $ k $ r) =>
   1.354          (case get_selectors sg s of Some () =>
   1.355            (case get_updates sg u of Some u_name =>
   1.356              let
   1.357 -              fun mk_free x t = Free (x, fastype_of t);
   1.358 -              val k' = mk_free "k" k;
   1.359 -              val r' = mk_free "r" r;
   1.360 -              val t' = sel $ (upd $ k' $ r');
   1.361 -              fun prove prop =
   1.362 -                Tactic.prove sg ["k", "r"] [] prop (K (simp_all_tac (get_simpset sg) []));
   1.363 +              fun mk_abs_var x t = (x, fastype_of t);
   1.364 +              val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
   1.365 +
   1.366 +              fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
   1.367 +		  (case (Symtab.lookup (updates,u)) of
   1.368 +                     None => None
   1.369 +                   | Some u_name 
   1.370 +                     => if u_name = s
   1.371 +                        then let 
   1.372 +                               val rv = mk_abs_var "r" r
   1.373 +                               val rb = Bound 0
   1.374 +                               val kv = mk_abs_var "k" k
   1.375 +                               val kb = Bound 1 
   1.376 +                             in Some (upd$kb$rb,kb,[kv,rv],true) end
   1.377 +                        else if u_name mem (map fst (dest_fieldTs rangeS))
   1.378 +                             orelse s mem (map fst (dest_fieldTs updT))
   1.379 +                             then None
   1.380 +			     else (case mk_eq_terms r of 
   1.381 +                                     Some (trm,trm',vars,update_s) 
   1.382 +                                     => let   
   1.383 +					  val kv = mk_abs_var "k" k
   1.384 +                                          val kb = Bound (length vars)
   1.385 +		                        in Some (upd$kb$trm,trm',kv::vars,update_s) end
   1.386 +                                   | None
   1.387 +                                     => let 
   1.388 +					  val rv = mk_abs_var "r" r
   1.389 +                                          val rb = Bound 0
   1.390 +                                          val kv = mk_abs_var "k" k
   1.391 +                                          val kb = Bound 1 
   1.392 +                                        in Some (upd$kb$rb,rb,[kv,rv],false) end))
   1.393 +                | mk_eq_terms r = None     
   1.394              in
   1.395 -              if u_name = s then Some (prove (Logic.mk_equals (t', k')))
   1.396 -              else Some (prove (Logic.mk_equals (t', sel $ r')))
   1.397 +	      (case mk_eq_terms (upd$k$r) of
   1.398 +                 Some (trm,trm',vars,update_s) 
   1.399 +                 => if update_s 
   1.400 +		    then Some (prove_split_simp sg domS 
   1.401 +                                 (list_all(vars,(Logic.mk_equals (sel$trm,trm')))))
   1.402 +                    else Some (prove_split_simp sg domS 
   1.403 +                                 (list_all(vars,(Logic.mk_equals (sel$trm,sel$trm')))))
   1.404 +               | None => None)
   1.405              end
   1.406            | None => None)
   1.407          | None => None)
   1.408        | _ => None));
   1.409  
   1.410 +(* record_eq_simproc *)
   1.411 +(* looks up the most specific record-equality.
   1.412 + * Note on efficiency:
   1.413 + * Testing equality of records boils down to the test of equality of all components.
   1.414 + * Therefore the complexity is: #components * complexity for single component.
   1.415 + * Especially if a record has a lot of components it may be better to split up
   1.416 + * the record first and do simplification on that (record_split_simp_tac).
   1.417 + * e.g. r(|lots of updates|) = x
   1.418 + *
   1.419 + *               record_eq_simproc           record_split_simp_tac
   1.420 + * Complexity: #components * #updates     #updates   
   1.421 + *           
   1.422 + *)
   1.423  val record_eq_simproc =
   1.424    Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
   1.425      (fn sg => fn _ => fn t =>
   1.426        (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
   1.427 -        (case rev (dest_fieldTs T) of
   1.428 -           [] => None
   1.429 -         | (name, _) :: _ => (case get_equalities sg name of
   1.430 -             None => None
   1.431 -           | Some thm => Some (thm RS Eq_TrueI)))
   1.432 +        (case last_fieldT T of
   1.433 +           None => None
   1.434 +         | Some (name, _) => (case get_equalities sg name of
   1.435 +                                None => None
   1.436 +                              | Some thm => Some (thm RS Eq_TrueI)))
   1.437         | _ => None));
   1.438  
   1.439  
   1.440 +(* record_upd_simproc *)
   1.441 +(* simplify multiple updates; for example: "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" *)
   1.442 +val record_upd_simproc =
   1.443 +  Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u1 k1 (u2 k2 r))"]
   1.444 +    (fn sg => fn _ => fn t =>
   1.445 +      (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
   1.446 + 	 let val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
   1.447 +	     fun mk_abs_var x t = (x, fastype_of t);
   1.448 +
   1.449 +             fun mk_updterm upds already ((upd as Const (u,_)) $ k $ r) =
   1.450 +		 if is_some (Symtab.lookup (upds,u))
   1.451 +		 then let 
   1.452 +			 fun rest already = mk_updterm upds already
   1.453 +		      in if is_some (Symtab.lookup (already,u)) 
   1.454 +			 then (case (rest already r) of
   1.455 +				 None => let 
   1.456 +				           val rv = mk_abs_var "r" r
   1.457 +                                           val rb = Bound 0
   1.458 +					   val kv = mk_abs_var "k" k
   1.459 +                                           val kb = Bound 1	      
   1.460 +                                         in Some (upd$kb$rb,rb,[kv,rv]) end
   1.461 +                               | Some (trm,trm',vars) 
   1.462 +				 => let 
   1.463 +				     val kv = mk_abs_var "k" k
   1.464 +                                     val kb = Bound (length vars)
   1.465 +                                    in Some (upd$kb$trm,trm',kv::vars) end)
   1.466 +	                 else (case rest (Symtab.update ((u,()),already)) r of 
   1.467 +				 None => None
   1.468 +		               | Some (trm,trm',vars) 
   1.469 +                                  => let
   1.470 +				      val kv = mk_abs_var "k" k
   1.471 +                                      val kb = Bound (length vars)
   1.472 +                                     in Some (upd$kb$trm,upd$kb$trm',kv::vars) end)
   1.473 +		     end
   1.474 +		 else None
   1.475 +	       | mk_updterm _ _ _ = None;
   1.476 +
   1.477 +	 in (case mk_updterm updates Symtab.empty t of
   1.478 +	       Some (trm,trm',vars)
   1.479 +                => Some (prove_split_simp sg T (list_all(vars,(Logic.mk_equals (trm,trm')))))
   1.480 +             | None => None)
   1.481 +	 end
   1.482 +       | _ => None));
   1.483 +
   1.484 +(* record_split_simproc *)
   1.485 +(* splits quantified occurrences of records, for which P holds. P can peek on the 
   1.486 + * subterm starting at the quantified occurrence of the record (including the quantifier)
   1.487 + *)
   1.488 +fun record_split_simproc P =
   1.489 +  Simplifier.simproc (Theory.sign_of HOL.thy) "record_split_simp" ["(a t)"]
   1.490 +    (fn sg => fn _ => fn t =>
   1.491 +      (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
   1.492 +         if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
   1.493 +         then (case last_fieldT T of
   1.494 +                 None => None
   1.495 +               | Some (name, _)
   1.496 +                  => if P t 
   1.497 +                     then (case get_splits sg name of
   1.498 +                             None => None
   1.499 +                           | Some (all_thm, All_thm, Ex_thm,_) 
   1.500 +                              => Some (case quantifier of
   1.501 +                                         "all" => all_thm
   1.502 +                                       | "All" => All_thm RS HOL.eq_reflection
   1.503 +                                       | "Ex"  => Ex_thm RS HOL.eq_reflection
   1.504 +                                       | _     => error "record_split_simproc"))
   1.505 +                     else None)
   1.506 +         else None
   1.507 +       | _ => None))
   1.508  
   1.509  (** record field splitting **)
   1.510  
   1.511  (* tactic *)
   1.512  
   1.513 +fun is_fieldT fields (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
   1.514 +  | is_fieldT _ _ = false;
   1.515 +
   1.516  fun record_split_tac i st =
   1.517    let
   1.518      val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st);
   1.519  
   1.520 -    fun is_fieldT (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
   1.521 -      | is_fieldT _ = false;
   1.522      val has_field = exists_Const
   1.523        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.524 -          (s = "all" orelse s = "All") andalso is_fieldT T
   1.525 +          (s = "all" orelse s = "All") andalso is_fieldT fields T
   1.526          | _ => false);
   1.527  
   1.528      val goal = Library.nth_elem (i - 1, Thm.prems_of st);
   1.529 @@ -605,6 +826,60 @@
   1.530    end handle Library.LIST _ => Seq.empty;
   1.531  
   1.532  
   1.533 +local
   1.534 +val inductive_atomize = thms "induct_atomize";
   1.535 +val inductive_rulify1 = thms "induct_rulify1";
   1.536 +in
   1.537 +(* record_split_simp_tac *)
   1.538 +(* splits (and simplifies) all records in the goal for which P holds. 
   1.539 + * For quantified occurrences of a record
   1.540 + * P can peek on the whole subterm (including the quantifier); for free variables P
   1.541 + * can only peek on the variable itself. 
   1.542 + *)
   1.543 +fun record_split_simp_tac P i st =
   1.544 +  let
   1.545 +    val sg = Thm.sign_of_thm st;
   1.546 +    val {sel_upd={simpset,...},field_splits={fields,...},...} 
   1.547 +            = RecordsData.get_sg sg;
   1.548 +
   1.549 +    val has_field = exists_Const
   1.550 +      (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.551 +          (s = "all" orelse s = "All" orelse s = "Ex") andalso is_fieldT fields T
   1.552 +        | _ => false);
   1.553 +
   1.554 +    val goal = Library.nth_elem (i - 1, Thm.prems_of st);
   1.555 +    val frees = filter (is_fieldT fields o type_of) (term_frees goal);
   1.556 +
   1.557 +    fun mk_split_free_tac free induct_thm i = 
   1.558 +	let val cfree = cterm_of sg free;
   1.559 +            val (_$(_$r)) = concl_of induct_thm;
   1.560 +            val crec = cterm_of sg r;
   1.561 +            val thm  = cterm_instantiate [(crec,cfree)] induct_thm;
   1.562 +        in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
   1.563 +                  rtac thm i,
   1.564 +                  simp_tac (HOL_basic_ss addsimps inductive_rulify1) i]
   1.565 +	end;
   1.566 +
   1.567 +    fun split_free_tac P i (free as Free (n,T)) = 
   1.568 +	(case last_fieldT T of
   1.569 +           None => None
   1.570 +         | Some(name,_)=> if P free 
   1.571 +                          then (case get_splits sg name of
   1.572 +                                  None => None
   1.573 +                                | Some (_,_,_,induct_thm)
   1.574 +                                   => Some (mk_split_free_tac free induct_thm i))
   1.575 +                          else None)
   1.576 +     | split_free_tac _ _ _ = None;
   1.577 +
   1.578 +    val split_frees_tacs = mapfilter (split_free_tac P i) frees;
   1.579 +   
   1.580 +    val simprocs = if has_field goal then [record_split_simproc P] else [];
   1.581 +   
   1.582 +  in st |> (EVERY split_frees_tacs) 
   1.583 +           THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i)
   1.584 +  end handle Library.LIST _ => Seq.empty;
   1.585 +end;
   1.586 +
   1.587  (* wrapper *)
   1.588  
   1.589  val record_split_name = "record_split_tac";
   1.590 @@ -778,12 +1053,22 @@
   1.591      fun r_scheme n = Free (rN, rec_schemeT n);
   1.592      fun r n = Free (rN, recT n);
   1.593  
   1.594 +    
   1.595  
   1.596      (* prepare print translation functions *)
   1.597 -
   1.598      val field_tr's =
   1.599        print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
   1.600  
   1.601 +    val field_type_tr's = 
   1.602 +	let val fldnames = if parent_len = 0 then (tl names) else names;
   1.603 +        in print_translation_field_types (distinct (flat (map NameSpace.accesses' fldnames))) 
   1.604 +        end;
   1.605 +                          
   1.606 +    fun record_type_abbr_tr's thy =
   1.607 +	let val trnames = (distinct (flat (map NameSpace.accesses' [hd all_names])))
   1.608 +            val sg = Theory.sign_of thy
   1.609 +	in map (gen_record_type_abbr_tr' 
   1.610 +                 sg bname alphas zeta (hd (rev names)) (recT 0) (rec_schemeT 0)) trnames end;   
   1.611  
   1.612      (* prepare declarations *)
   1.613  
   1.614 @@ -879,7 +1164,33 @@
   1.615          ((r_scheme n === rec_scheme n) ==> C) ==> C;
   1.616      fun cases_prop n = All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C;
   1.617  
   1.618 +    (*split*)
   1.619 +    fun split_scheme_meta_prop n =
   1.620 +      let val P = Free ("P", rec_schemeT n --> Term.propT) in
   1.621 +       equals (Term.propT) $
   1.622 +        (Term.list_all_free ([(rN,rec_schemeT n)],(P $ r_scheme n)))$
   1.623 +        (All (prune n all_xs_more ~~ prune n all_types_more) (P $ rec_scheme n))
   1.624 +      end;
   1.625  
   1.626 +    fun split_scheme_object_prop n =
   1.627 +      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
   1.628 +          val ALL = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) 
   1.629 +      in
   1.630 +	Trueprop (
   1.631 +           HOLogic.eq_const (HOLogic.boolT) $
   1.632 +            (HOLogic.mk_all ((rN,rec_schemeT n,P $ r_scheme n)))$
   1.633 +            (ALL (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
   1.634 +      end;
   1.635 +
   1.636 +      fun split_scheme_object_ex_prop n =
   1.637 +      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
   1.638 +          val EX = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) 
   1.639 +      in
   1.640 +	Trueprop (
   1.641 +           HOLogic.eq_const (HOLogic.boolT) $
   1.642 +            (HOLogic.mk_exists ((rN,rec_schemeT n,P $ r_scheme n)))$
   1.643 +            (EX (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
   1.644 +      end;
   1.645      (* 1st stage: fields_thy *)
   1.646  
   1.647      val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) =
   1.648 @@ -889,17 +1200,22 @@
   1.649  
   1.650      val all_field_inducts = flat (map #field_inducts parents) @ field_inducts;
   1.651      val all_field_cases = flat (map #field_cases parents) @ field_cases;
   1.652 -
   1.653 +    val all_field_splits = flat (map #field_splits parents) @ field_splits
   1.654  
   1.655 +    
   1.656      (* 2nd stage: defs_thy *)
   1.657  
   1.658 +        
   1.659 +   
   1.660 +
   1.661      val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
   1.662        fields_thy
   1.663 -      |> add_record_splits (map (suffix field_typeN) names) field_splits
   1.664 +      |> Theory.add_trfuns 
   1.665 +           ([],[],record_type_abbr_tr's fields_thy @ field_type_tr's @ field_tr's, [])
   1.666 +      |> add_field_splits (map (suffix field_typeN) names) field_splits
   1.667        |> Theory.parent_path
   1.668        |> Theory.add_tyabbrs_i recordT_specs
   1.669        |> Theory.add_path bname
   1.670 -      |> Theory.add_trfuns ([], [], field_tr's, [])
   1.671        |> Theory.add_consts_i
   1.672          (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
   1.673        |> (Theory.add_consts_i o map Syntax.no_syn)
   1.674 @@ -935,12 +1251,32 @@
   1.675          EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_cases))
   1.676          THEN simp_all_tac HOL_basic_ss []);
   1.677  
   1.678 +    fun split_scheme_meta n =
   1.679 +      prove_standard [] [] (split_scheme_meta_prop n) (fn _ =>
   1.680 +        Simplifier.full_simp_tac (HOL_basic_ss addsimps all_field_splits) 1);
   1.681 +
   1.682 +    fun split_scheme_object induct_scheme n =
   1.683 +      prove_standard [] [] (split_scheme_object_prop n) (fn _ =>
   1.684 +         EVERY [rtac iffI 1, 
   1.685 +                REPEAT (rtac allI 1), etac allE 1, atac 1,
   1.686 +                rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
   1.687 +
   1.688 +    fun split_scheme_object_ex split_scheme_meta n =
   1.689 +      prove_standard [] [] (split_scheme_object_ex_prop n) (fn _ =>
   1.690 +        fast_simp_tac (claset_of HOL.thy,
   1.691 +                       HOL_basic_ss addsimps [split_scheme_meta]) 1);
   1.692 +       
   1.693      val induct_scheme0 = induct_scheme 0;
   1.694      val cases_scheme0 = cases_scheme 0;
   1.695 +    val split_scheme_meta0 = split_scheme_meta 0;
   1.696 +    val split_scheme_object0 = split_scheme_object induct_scheme0 0;
   1.697 +    val split_scheme_object_ex0 = split_scheme_object_ex split_scheme_meta0 0;
   1.698      val more_induct_scheme = map induct_scheme ancestry;
   1.699      val more_cases_scheme = map cases_scheme ancestry;
   1.700  
   1.701 -    val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _],
   1.702 +    val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _, 
   1.703 +                      [split_scheme_meta',split_scheme_object',
   1.704 +                       split_scheme_object_ex',split_scheme_free']],
   1.705          [induct_scheme', cases_scheme']), [more_induct_scheme', more_cases_scheme'])) =
   1.706        defs_thy
   1.707        |> (PureThy.add_thmss o map Thm.no_attributes)
   1.708 @@ -948,7 +1284,9 @@
   1.709          ("update_convs", update_convs),
   1.710          ("select_defs", sel_defs),
   1.711          ("update_defs", update_defs),
   1.712 -        ("defs", derived_defs)]
   1.713 +        ("defs", derived_defs),
   1.714 +        ("splits",[split_scheme_meta0,split_scheme_object0,
   1.715 +                   split_scheme_object_ex0,induct_scheme0])]
   1.716        |>>> PureThy.add_thms
   1.717         [(("induct_scheme", induct_scheme0), induct_type_global (suffix schemeN name)),
   1.718          (("cases_scheme", cases_scheme0), cases_type_global (suffix schemeN name))]
   1.719 @@ -1009,9 +1347,12 @@
   1.720      val final_thy =
   1.721        more_thms_thy'
   1.722        |> put_record name (make_record_info args parent fields field_inducts field_cases
   1.723 -        (field_simps @ simps))
   1.724 -      |> put_sel_upd (names @ [full_moreN]) (field_simps @ sel_defs' @ update_defs')
   1.725 +          field_splits (field_simps @ simps))
   1.726 +      |> put_sel_upd (names @ [full_moreN]) simps
   1.727        |> add_record_equalities (snd (split_last names)) equality'
   1.728 +      |> add_record_splits (snd (split_last names)) 
   1.729 +                           (split_scheme_meta',split_scheme_object',
   1.730 +                            split_scheme_object_ex',split_scheme_free')
   1.731        |> Theory.parent_path;
   1.732  
   1.733    in (final_thy, {simps = simps, iffs = iffs}) end;
   1.734 @@ -1129,7 +1470,6 @@
   1.735  val add_record_i = gen_add_record cert_typ (K I);
   1.736  
   1.737  
   1.738 -
   1.739  (** package setup **)
   1.740  
   1.741  (* setup theory *)