src/HOL/Tools/record_package.ML
changeset 14255 e6e3e3f0deed
parent 14079 1c22e5499eeb
child 14358 233c5bd5b539
--- a/src/HOL/Tools/record_package.ML	Thu Nov 06 14:18:05 2003 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Nov 06 20:45:02 2003 +0100
@@ -13,6 +13,7 @@
   val record_split_tac: int -> tactic
   val record_split_name: string
   val record_split_wrapper: string * wrapper
+  val print_record_type_abbr: bool ref 
 end;
 
 signature RECORD_PACKAGE =
@@ -22,6 +23,8 @@
   val updateN: string
   val mk_fieldT: (string * typ) * typ -> typ
   val dest_fieldT: typ -> (string * typ) * typ
+  val dest_fieldTs: typ -> (string * typ) list
+  val last_fieldT: typ -> (string * typ) option
   val mk_field: (string * term) * term -> term
   val mk_fst: term -> term
   val mk_snd: term -> term
@@ -36,9 +39,12 @@
   val add_record_i: (string list * bstring) -> (typ list * string) option
     -> (bstring * typ * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
   val setup: (theory -> theory) list
+  val record_upd_simproc: simproc
+  val record_split_simproc: (term -> bool) -> simproc
+  val record_split_simp_tac: (term -> bool) -> int -> tactic
 end;
 
-structure RecordPackage: RECORD_PACKAGE =
+structure RecordPackage :RECORD_PACKAGE =
 struct
 
 
@@ -170,6 +176,12 @@
   in (c, T) :: dest_fieldTs U
   end handle TYPE _ => [];
 
+fun last_fieldT T =
+  let val ((c, T), U) = dest_fieldT T
+  in (case last_fieldT U of
+        None => Some (c,T)
+      | Some l => Some l)
+  end handle TYPE _ => None
 
 (* morphisms *)
 
@@ -313,6 +325,9 @@
 
 (* print translations *)
 
+
+val print_record_type_abbr = ref true;
+
 fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
       (case try (unsuffix sfx) name_field of
         Some name =>
@@ -334,6 +349,49 @@
   gen_record_tr' "_field_types" "_field_type" field_typeN
     (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme";
 
+
+(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
+(* the (nested) field types.                                                        *)
+fun record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT tm =
+  let
+      (* tm is term representation of a (nested) field type. We first reconstruct the      *)
+      (* type from tm so that we can continue on the type level rather then the term level.*)
+ 
+      fun get_sort xs n = (case assoc (xs,n) of 
+                             Some s => s 
+                           | None => Sign.defaultS sg);
+
+      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) 
+      val {tsig,...} = Sign.rep_sg sg
+
+      fun mk_type_abbr subst name alphas = 
+          let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
+          in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
+
+      fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
+
+   in if !print_record_type_abbr
+      then (case last_fieldT T of
+             Some (name,_) 
+              => if name = lastF 
+                 then
+		   let val subst = unify rec_schemeT T 
+                   in 
+                    if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
+                    then mk_type_abbr subst abbr alphas
+                    else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
+		   end handle TUNIFY => record_type_tr' tm
+                 else raise Match (* give print translation of specialised record a chance *)
+            | _ => record_type_tr' tm)
+       else record_type_tr' tm
+  end
+
+     
+fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT name =
+  let val name_sfx = suffix field_typeN name
+      val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT 
+  in (name_sfx, fn [t,u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
+      
 val record_tr' =
   gen_record_tr' "_fields" "_field" fieldN
     (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme";
@@ -344,23 +402,24 @@
       foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   end;
 
-
 fun gen_field_tr' sfx tr' name =
   let val name_sfx = suffix sfx name
   in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
 
 fun print_translation names =
-  map (gen_field_tr' field_typeN record_type_tr') names @
   map (gen_field_tr' fieldN record_tr') names @
   map (gen_field_tr' updateN record_update_tr') names;
 
+fun print_translation_field_types names =
+  map (gen_field_tr' field_typeN record_type_tr') names
+
 
 
 (*** extend theory by record definition ***)
 
 (** record info **)
 
-(* type record_info and parent_info *)
+(* type record_info and parent_info  *)
 
 type record_info =
  {args: (string * sort) list,
@@ -368,22 +427,24 @@
   fields: (string * typ) list,
   field_inducts: thm list,
   field_cases: thm list,
+  field_splits: thm list,
   simps: thm list};
 
-fun make_record_info args parent fields field_inducts field_cases simps =
+fun make_record_info args parent fields field_inducts field_cases field_splits simps =
  {args = args, parent = parent, fields = fields, field_inducts = field_inducts,
-  field_cases = field_cases, simps = simps}: record_info;
+  field_cases = field_cases, field_splits = field_splits, simps = simps}: record_info;
 
 type parent_info =
  {name: string,
   fields: (string * typ) list,
   field_inducts: thm list,
   field_cases: thm list,
+  field_splits: thm list,
   simps: thm list};
 
-fun make_parent_info name fields field_inducts field_cases simps =
+fun make_parent_info name fields field_inducts field_cases field_splits simps =
  {name = name, fields = fields, field_inducts = field_inducts,
-  field_cases = field_cases, simps = simps}: parent_info;
+  field_cases = field_cases, field_splits = field_splits, simps = simps}: parent_info;
 
 
 (* data kind 'HOL/records' *)
@@ -397,11 +458,13 @@
   field_splits:
    {fields: unit Symtab.table,
     simpset: Simplifier.simpset},
-  equalities: thm Symtab.table};
+  equalities: thm Symtab.table,
+  splits: (thm*thm*thm*thm) Symtab.table (* !!,!,EX - split-equalities,induct rule *) 
+};
 
-fun make_record_data records sel_upd field_splits equalities=
+fun make_record_data records sel_upd field_splits equalities splits =
  {records = records, sel_upd = sel_upd, field_splits = field_splits,
-  equalities = equalities}: record_data;
+  equalities = equalities, splits = splits}: record_data;
 
 structure RecordsArgs =
 struct
@@ -411,7 +474,7 @@
   val empty =
     make_record_data Symtab.empty
       {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
-      {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty;
+      {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty Symtab.empty;
 
   val copy = I;
   val prep_ext = I;
@@ -419,19 +482,25 @@
    ({records = recs1,
      sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
      field_splits = {fields = flds1, simpset = fld_ss1},
-     equalities = equalities1},
+     equalities = equalities1,
+     splits = splits1},
     {records = recs2,
      sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
      field_splits = {fields = flds2, simpset = fld_ss2},
-     equalities = equalities2}) =
-    make_record_data
+     equalities = equalities2, 
+     splits = splits2}) =
+    make_record_data  
       (Symtab.merge (K true) (recs1, recs2))
       {selectors = Symtab.merge (K true) (sels1, sels2),
         updates = Symtab.merge (K true) (upds1, upds2),
         simpset = Simplifier.merge_ss (ss1, ss2)}
       {fields = Symtab.merge (K true) (flds1, flds2),
         simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)}
-      (Symtab.merge Thm.eq_thm (equalities1, equalities2));
+      (Symtab.merge Thm.eq_thm (equalities1, equalities2))
+      (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
+                     => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
+                        Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) 
+                    (splits1, splits2));
 
   fun print sg ({records = recs, ...}: record_data) =
     let
@@ -462,9 +531,9 @@
 
 fun put_record name info thy =
   let
-    val {records, sel_upd, field_splits, equalities} = RecordsData.get thy;
+    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
     val data = make_record_data (Symtab.update ((name, info), records))
-      sel_upd field_splits equalities;
+      sel_upd field_splits equalities splits;
   in RecordsData.put data thy end;
 
 
@@ -476,32 +545,31 @@
 fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name);
 fun get_simpset sg = #simpset (get_sel_upd sg);
 
-
 fun put_sel_upd names simps thy =
   let
     val sels = map (rpair ()) names;
     val upds = map (suffix updateN) names ~~ names;
 
     val {records, sel_upd = {selectors, updates, simpset}, field_splits,
-      equalities} = RecordsData.get thy;
+      equalities, splits} = RecordsData.get thy;
     val data = make_record_data records
       {selectors = Symtab.extend (selectors, sels),
         updates = Symtab.extend (updates, upds),
         simpset = Simplifier.addsimps (simpset, simps)}
-      field_splits equalities;
+      field_splits equalities splits;
   in RecordsData.put data thy end;
 
 
 (* access 'field_splits' *)
 
-fun add_record_splits names simps thy =
+fun add_field_splits names simps thy =
   let
     val {records, sel_upd, field_splits = {fields, simpset},
-      equalities} = RecordsData.get thy;
+      equalities, splits} = RecordsData.get thy;
     val flds = map (rpair ()) names;
     val data = make_record_data records sel_upd
       {fields = Symtab.extend (fields, flds),
-       simpset = Simplifier.addsimps (simpset, simps)} equalities;
+       simpset = Simplifier.addsimps (simpset, simps)} equalities splits;
   in RecordsData.put data thy end;
 
 
@@ -509,14 +577,26 @@
 
 fun add_record_equalities name thm thy =
   let
-    val {records, sel_upd, field_splits, equalities} = RecordsData.get thy;
+    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
     val data = make_record_data records sel_upd field_splits
-      (Symtab.update_new ((name, thm), equalities));
+      (Symtab.update_new ((name, thm), equalities)) splits;
   in RecordsData.put data thy end;
 
 fun get_equalities sg name =
   Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
 
+(* access 'splits' *)
+
+fun add_record_splits name thmP thy =
+  let
+    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
+    val data = make_record_data records sel_upd field_splits
+      equalities (Symtab.update_new ((name, thmP), splits));
+  in RecordsData.put data thy end;
+
+fun get_splits sg name =
+  Symtab.lookup (#splits (RecordsData.get_sg sg), name);
+
 
 (* parent records *)
 
@@ -526,7 +606,7 @@
         val sign = Theory.sign_of thy;
         fun err msg = error (msg ^ " parent record " ^ quote name);
 
-        val {args, parent, fields, field_inducts, field_cases, simps} =
+        val {args, parent, fields, field_inducts, field_cases, field_splits, simps} =
           (case get_record thy name of Some info => info | None => err "Unknown");
         val _ = if length types <> length args then err "Bad number of arguments for" else ();
 
@@ -542,60 +622,201 @@
         conditional (not (null bads)) (fn () =>
           err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
         add_parents thy parent'
-          (make_parent_info name fields' field_inducts field_cases simps :: parents)
+          (make_parent_info name fields' field_inducts field_cases field_splits simps::parents)
       end;
 
 
+(** record simprocs **)
+ 
+fun quick_and_dirty_prove sg xs asms prop tac =
+Tactic.prove sg xs asms prop
+    (if ! quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
 
-(** record simproc **)
+
+fun prove_split_simp sg T prop =
+    (case last_fieldT T of
+      Some (name,_) => (case get_splits sg name of
+                         Some (all_thm,_,_,_) 
+                          => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
+                             in (quick_and_dirty_prove sg [] [] prop 
+                                  (K (simp_tac (simpset addsimps [all_thm]) 1)))
+                             end
+                      | _ => error "RecordPackage.prove_split_simp: code should never been reached")
+     | _ => error "RecordPackage.prove_split_simp: code should never been reached")
+
 
+(* record_simproc *)
+(* Simplifies selections of an record update:
+ *  (1)  S (r(|S:=k|)) = k respectively
+ *  (2)  S (r(|X:=k|)) = S r
+ * The simproc skips multiple updates at once, eg:
+ *  S (r (|S:=k,X:=2,Y:=3|)) = k
+ * But be careful in (2) because of the extendibility of records.
+ * - If S is a more-selector we have to make sure that the update on component
+ *   X does not affect the selected subrecord.
+ * - If X is a more-selector we have to make sure that S is not in the updated
+ *   subrecord. 
+ *)
 val record_simproc =
   Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
     (fn sg => fn _ => fn t =>
-      (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
+      (case t of (sel as Const (s, Type (_,[domS,rangeS]))) $ ((upd as Const (u, _)) $ k $ r) =>
         (case get_selectors sg s of Some () =>
           (case get_updates sg u of Some u_name =>
             let
-              fun mk_free x t = Free (x, fastype_of t);
-              val k' = mk_free "k" k;
-              val r' = mk_free "r" r;
-              val t' = sel $ (upd $ k' $ r');
-              fun prove prop =
-                Tactic.prove sg ["k", "r"] [] prop (K (simp_all_tac (get_simpset sg) []));
+              fun mk_abs_var x t = (x, fastype_of t);
+              val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
+
+              fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
+		  (case (Symtab.lookup (updates,u)) of
+                     None => None
+                   | Some u_name 
+                     => if u_name = s
+                        then let 
+                               val rv = mk_abs_var "r" r
+                               val rb = Bound 0
+                               val kv = mk_abs_var "k" k
+                               val kb = Bound 1 
+                             in Some (upd$kb$rb,kb,[kv,rv],true) end
+                        else if u_name mem (map fst (dest_fieldTs rangeS))
+                             orelse s mem (map fst (dest_fieldTs updT))
+                             then None
+			     else (case mk_eq_terms r of 
+                                     Some (trm,trm',vars,update_s) 
+                                     => let   
+					  val kv = mk_abs_var "k" k
+                                          val kb = Bound (length vars)
+		                        in Some (upd$kb$trm,trm',kv::vars,update_s) end
+                                   | None
+                                     => let 
+					  val rv = mk_abs_var "r" r
+                                          val rb = Bound 0
+                                          val kv = mk_abs_var "k" k
+                                          val kb = Bound 1 
+                                        in Some (upd$kb$rb,rb,[kv,rv],false) end))
+                | mk_eq_terms r = None     
             in
-              if u_name = s then Some (prove (Logic.mk_equals (t', k')))
-              else Some (prove (Logic.mk_equals (t', sel $ r')))
+	      (case mk_eq_terms (upd$k$r) of
+                 Some (trm,trm',vars,update_s) 
+                 => if update_s 
+		    then Some (prove_split_simp sg domS 
+                                 (list_all(vars,(Logic.mk_equals (sel$trm,trm')))))
+                    else Some (prove_split_simp sg domS 
+                                 (list_all(vars,(Logic.mk_equals (sel$trm,sel$trm')))))
+               | None => None)
             end
           | None => None)
         | None => None)
       | _ => None));
 
+(* record_eq_simproc *)
+(* looks up the most specific record-equality.
+ * Note on efficiency:
+ * Testing equality of records boils down to the test of equality of all components.
+ * Therefore the complexity is: #components * complexity for single component.
+ * Especially if a record has a lot of components it may be better to split up
+ * the record first and do simplification on that (record_split_simp_tac).
+ * e.g. r(|lots of updates|) = x
+ *
+ *               record_eq_simproc           record_split_simp_tac
+ * Complexity: #components * #updates     #updates   
+ *           
+ *)
 val record_eq_simproc =
   Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
     (fn sg => fn _ => fn t =>
       (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
-        (case rev (dest_fieldTs T) of
-           [] => None
-         | (name, _) :: _ => (case get_equalities sg name of
-             None => None
-           | Some thm => Some (thm RS Eq_TrueI)))
+        (case last_fieldT T of
+           None => None
+         | Some (name, _) => (case get_equalities sg name of
+                                None => None
+                              | Some thm => Some (thm RS Eq_TrueI)))
        | _ => None));
 
 
+(* record_upd_simproc *)
+(* simplify multiple updates; for example: "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" *)
+val record_upd_simproc =
+  Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u1 k1 (u2 k2 r))"]
+    (fn sg => fn _ => fn t =>
+      (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
+ 	 let val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
+	     fun mk_abs_var x t = (x, fastype_of t);
+
+             fun mk_updterm upds already ((upd as Const (u,_)) $ k $ r) =
+		 if is_some (Symtab.lookup (upds,u))
+		 then let 
+			 fun rest already = mk_updterm upds already
+		      in if is_some (Symtab.lookup (already,u)) 
+			 then (case (rest already r) of
+				 None => let 
+				           val rv = mk_abs_var "r" r
+                                           val rb = Bound 0
+					   val kv = mk_abs_var "k" k
+                                           val kb = Bound 1	      
+                                         in Some (upd$kb$rb,rb,[kv,rv]) end
+                               | Some (trm,trm',vars) 
+				 => let 
+				     val kv = mk_abs_var "k" k
+                                     val kb = Bound (length vars)
+                                    in Some (upd$kb$trm,trm',kv::vars) end)
+	                 else (case rest (Symtab.update ((u,()),already)) r of 
+				 None => None
+		               | Some (trm,trm',vars) 
+                                  => let
+				      val kv = mk_abs_var "k" k
+                                      val kb = Bound (length vars)
+                                     in Some (upd$kb$trm,upd$kb$trm',kv::vars) end)
+		     end
+		 else None
+	       | mk_updterm _ _ _ = None;
+
+	 in (case mk_updterm updates Symtab.empty t of
+	       Some (trm,trm',vars)
+                => Some (prove_split_simp sg T (list_all(vars,(Logic.mk_equals (trm,trm')))))
+             | None => None)
+	 end
+       | _ => None));
+
+(* record_split_simproc *)
+(* splits quantified occurrences of records, for which P holds. P can peek on the 
+ * subterm starting at the quantified occurrence of the record (including the quantifier)
+ *)
+fun record_split_simproc P =
+  Simplifier.simproc (Theory.sign_of HOL.thy) "record_split_simp" ["(a t)"]
+    (fn sg => fn _ => fn t =>
+      (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
+         if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
+         then (case last_fieldT T of
+                 None => None
+               | Some (name, _)
+                  => if P t 
+                     then (case get_splits sg name of
+                             None => None
+                           | Some (all_thm, All_thm, Ex_thm,_) 
+                              => Some (case quantifier of
+                                         "all" => all_thm
+                                       | "All" => All_thm RS HOL.eq_reflection
+                                       | "Ex"  => Ex_thm RS HOL.eq_reflection
+                                       | _     => error "record_split_simproc"))
+                     else None)
+         else None
+       | _ => None))
 
 (** record field splitting **)
 
 (* tactic *)
 
+fun is_fieldT fields (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
+  | is_fieldT _ _ = false;
+
 fun record_split_tac i st =
   let
     val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st);
 
-    fun is_fieldT (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
-      | is_fieldT _ = false;
     val has_field = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
-          (s = "all" orelse s = "All") andalso is_fieldT T
+          (s = "all" orelse s = "All") andalso is_fieldT fields T
         | _ => false);
 
     val goal = Library.nth_elem (i - 1, Thm.prems_of st);
@@ -605,6 +826,60 @@
   end handle Library.LIST _ => Seq.empty;
 
 
+local
+val inductive_atomize = thms "induct_atomize";
+val inductive_rulify1 = thms "induct_rulify1";
+in
+(* record_split_simp_tac *)
+(* splits (and simplifies) all records in the goal for which P holds. 
+ * For quantified occurrences of a record
+ * P can peek on the whole subterm (including the quantifier); for free variables P
+ * can only peek on the variable itself. 
+ *)
+fun record_split_simp_tac P i st =
+  let
+    val sg = Thm.sign_of_thm st;
+    val {sel_upd={simpset,...},field_splits={fields,...},...} 
+            = RecordsData.get_sg sg;
+
+    val has_field = exists_Const
+      (fn (s, Type (_, [Type (_, [T, _]), _])) =>
+          (s = "all" orelse s = "All" orelse s = "Ex") andalso is_fieldT fields T
+        | _ => false);
+
+    val goal = Library.nth_elem (i - 1, Thm.prems_of st);
+    val frees = filter (is_fieldT fields o type_of) (term_frees goal);
+
+    fun mk_split_free_tac free induct_thm i = 
+	let val cfree = cterm_of sg free;
+            val (_$(_$r)) = concl_of induct_thm;
+            val crec = cterm_of sg r;
+            val thm  = cterm_instantiate [(crec,cfree)] induct_thm;
+        in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
+                  rtac thm i,
+                  simp_tac (HOL_basic_ss addsimps inductive_rulify1) i]
+	end;
+
+    fun split_free_tac P i (free as Free (n,T)) = 
+	(case last_fieldT T of
+           None => None
+         | Some(name,_)=> if P free 
+                          then (case get_splits sg name of
+                                  None => None
+                                | Some (_,_,_,induct_thm)
+                                   => Some (mk_split_free_tac free induct_thm i))
+                          else None)
+     | split_free_tac _ _ _ = None;
+
+    val split_frees_tacs = mapfilter (split_free_tac P i) frees;
+   
+    val simprocs = if has_field goal then [record_split_simproc P] else [];
+   
+  in st |> (EVERY split_frees_tacs) 
+           THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i)
+  end handle Library.LIST _ => Seq.empty;
+end;
+
 (* wrapper *)
 
 val record_split_name = "record_split_tac";
@@ -778,12 +1053,22 @@
     fun r_scheme n = Free (rN, rec_schemeT n);
     fun r n = Free (rN, recT n);
 
+    
 
     (* prepare print translation functions *)
-
     val field_tr's =
       print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
 
+    val field_type_tr's = 
+	let val fldnames = if parent_len = 0 then (tl names) else names;
+        in print_translation_field_types (distinct (flat (map NameSpace.accesses' fldnames))) 
+        end;
+                          
+    fun record_type_abbr_tr's thy =
+	let val trnames = (distinct (flat (map NameSpace.accesses' [hd all_names])))
+            val sg = Theory.sign_of thy
+	in map (gen_record_type_abbr_tr' 
+                 sg bname alphas zeta (hd (rev names)) (recT 0) (rec_schemeT 0)) trnames end;   
 
     (* prepare declarations *)
 
@@ -879,7 +1164,33 @@
         ((r_scheme n === rec_scheme n) ==> C) ==> C;
     fun cases_prop n = All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C;
 
+    (*split*)
+    fun split_scheme_meta_prop n =
+      let val P = Free ("P", rec_schemeT n --> Term.propT) in
+       equals (Term.propT) $
+        (Term.list_all_free ([(rN,rec_schemeT n)],(P $ r_scheme n)))$
+        (All (prune n all_xs_more ~~ prune n all_types_more) (P $ rec_scheme n))
+      end;
 
+    fun split_scheme_object_prop n =
+      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
+          val ALL = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) 
+      in
+	Trueprop (
+           HOLogic.eq_const (HOLogic.boolT) $
+            (HOLogic.mk_all ((rN,rec_schemeT n,P $ r_scheme n)))$
+            (ALL (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
+      end;
+
+      fun split_scheme_object_ex_prop n =
+      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
+          val EX = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) 
+      in
+	Trueprop (
+           HOLogic.eq_const (HOLogic.boolT) $
+            (HOLogic.mk_exists ((rN,rec_schemeT n,P $ r_scheme n)))$
+            (EX (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
+      end;
     (* 1st stage: fields_thy *)
 
     val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) =
@@ -889,17 +1200,22 @@
 
     val all_field_inducts = flat (map #field_inducts parents) @ field_inducts;
     val all_field_cases = flat (map #field_cases parents) @ field_cases;
-
+    val all_field_splits = flat (map #field_splits parents) @ field_splits
 
+    
     (* 2nd stage: defs_thy *)
 
+        
+   
+
     val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
       fields_thy
-      |> add_record_splits (map (suffix field_typeN) names) field_splits
+      |> Theory.add_trfuns 
+           ([],[],record_type_abbr_tr's fields_thy @ field_type_tr's @ field_tr's, [])
+      |> add_field_splits (map (suffix field_typeN) names) field_splits
       |> Theory.parent_path
       |> Theory.add_tyabbrs_i recordT_specs
       |> Theory.add_path bname
-      |> Theory.add_trfuns ([], [], field_tr's, [])
       |> Theory.add_consts_i
         (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
       |> (Theory.add_consts_i o map Syntax.no_syn)
@@ -935,12 +1251,32 @@
         EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_cases))
         THEN simp_all_tac HOL_basic_ss []);
 
+    fun split_scheme_meta n =
+      prove_standard [] [] (split_scheme_meta_prop n) (fn _ =>
+        Simplifier.full_simp_tac (HOL_basic_ss addsimps all_field_splits) 1);
+
+    fun split_scheme_object induct_scheme n =
+      prove_standard [] [] (split_scheme_object_prop n) (fn _ =>
+         EVERY [rtac iffI 1, 
+                REPEAT (rtac allI 1), etac allE 1, atac 1,
+                rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
+
+    fun split_scheme_object_ex split_scheme_meta n =
+      prove_standard [] [] (split_scheme_object_ex_prop n) (fn _ =>
+        fast_simp_tac (claset_of HOL.thy,
+                       HOL_basic_ss addsimps [split_scheme_meta]) 1);
+       
     val induct_scheme0 = induct_scheme 0;
     val cases_scheme0 = cases_scheme 0;
+    val split_scheme_meta0 = split_scheme_meta 0;
+    val split_scheme_object0 = split_scheme_object induct_scheme0 0;
+    val split_scheme_object_ex0 = split_scheme_object_ex split_scheme_meta0 0;
     val more_induct_scheme = map induct_scheme ancestry;
     val more_cases_scheme = map cases_scheme ancestry;
 
-    val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _],
+    val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _, 
+                      [split_scheme_meta',split_scheme_object',
+                       split_scheme_object_ex',split_scheme_free']],
         [induct_scheme', cases_scheme']), [more_induct_scheme', more_cases_scheme'])) =
       defs_thy
       |> (PureThy.add_thmss o map Thm.no_attributes)
@@ -948,7 +1284,9 @@
         ("update_convs", update_convs),
         ("select_defs", sel_defs),
         ("update_defs", update_defs),
-        ("defs", derived_defs)]
+        ("defs", derived_defs),
+        ("splits",[split_scheme_meta0,split_scheme_object0,
+                   split_scheme_object_ex0,induct_scheme0])]
       |>>> PureThy.add_thms
        [(("induct_scheme", induct_scheme0), induct_type_global (suffix schemeN name)),
         (("cases_scheme", cases_scheme0), cases_type_global (suffix schemeN name))]
@@ -1009,9 +1347,12 @@
     val final_thy =
       more_thms_thy'
       |> put_record name (make_record_info args parent fields field_inducts field_cases
-        (field_simps @ simps))
-      |> put_sel_upd (names @ [full_moreN]) (field_simps @ sel_defs' @ update_defs')
+          field_splits (field_simps @ simps))
+      |> put_sel_upd (names @ [full_moreN]) simps
       |> add_record_equalities (snd (split_last names)) equality'
+      |> add_record_splits (snd (split_last names)) 
+                           (split_scheme_meta',split_scheme_object',
+                            split_scheme_object_ex',split_scheme_free')
       |> Theory.parent_path;
 
   in (final_thy, {simps = simps, iffs = iffs}) end;
@@ -1129,7 +1470,6 @@
 val add_record_i = gen_add_record cert_typ (K I);
 
 
-
 (** package setup **)
 
 (* setup theory *)