reimplementation of HOL records; only one type is created for
authorschirmer
Mon May 03 23:22:17 2004 +0200 (2004-05-03)
changeset 147002f885b7e5ba7
parent 14699 2c9b463044ec
child 14701 62a724ce51c7
reimplementation of HOL records; only one type is created for
each record extension, instead of one type for each field. See NEWS.
NEWS
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Record.thy
src/HOL/Tools/record_package.ML
src/HOL/ex/Records.thy
src/HOL/thy_syntax.ML
src/Pure/sign.ML
     1.1 --- a/NEWS	Sat May 01 22:28:51 2004 +0200
     1.2 +++ b/NEWS	Mon May 03 23:22:17 2004 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  depend on the signature of the theory context being presently used for
     1.5  parsing/printing, see also isar-ref manual.
     1.6  
     1.7 +
     1.8  * Pure: improved indexed syntax and implicit structures.  First of
     1.9  all, indexed syntax provides a notational device for subscripted
    1.10  application, using the new syntax \<^bsub>term\<^esub> for arbitrary
    1.11 @@ -30,6 +31,17 @@
    1.12  * Pure: tuned internal renaming of symbolic identifiers -- attach
    1.13  primes instead of base 26 numbers.
    1.14  
    1.15 +*** HOL ***
    1.16 +
    1.17 +* Records:
    1.18 +   Reimplementation of records to avoid performance problems for
    1.19 +   type inference. Records are no longer composed of nested field types,
    1.20 +   but of nested extension types. Therefore the record type only grows
    1.21 +   linear in the number of extensions and not in the number of fields.
    1.22 +   The top-level (users) view on records is preserved. 
    1.23 +   Potential INCOMPATIBILITY only in strange cases, where the theory
    1.24 +   depends on the old record representation. The type generated for
    1.25 +   a record is called <record_name>_ext_type.    
    1.26  
    1.27  *** HOLCF ***
    1.28  
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sat May 01 22:28:51 2004 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon May 03 23:22:17 2004 +0200
     2.3 @@ -92,7 +92,7 @@
     2.4  lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
     2.5  by (simp add: acc_modi_accmodi_def)
     2.6  
     2.7 -instance access_field_type:: ("type","type") has_accmodi ..
     2.8 +instance decl_ext_type:: ("type") has_accmodi ..
     2.9  
    2.10  defs (overloaded)
    2.11  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    2.12 @@ -130,7 +130,7 @@
    2.13  axclass has_declclass < "type"
    2.14  consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
    2.15  
    2.16 -instance pid_field_type::("type","type") has_declclass ..
    2.17 +instance qtname_ext_type::("type") has_declclass ..
    2.18  
    2.19  defs (overloaded)
    2.20  qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
    2.21 @@ -153,17 +153,17 @@
    2.22  axclass has_static < "type"
    2.23  consts is_static :: "'a::has_static \<Rightarrow> bool"
    2.24  
    2.25 -instance access_field_type :: ("type","has_static") has_static ..
    2.26 +instance decl_ext_type :: ("has_static") has_static ..
    2.27  
    2.28  defs (overloaded)
    2.29  decl_is_static_def: 
    2.30   "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" 
    2.31  
    2.32 -instance static_field_type :: ("type","type") has_static ..
    2.33 +instance member_ext_type :: ("type") has_static ..
    2.34  
    2.35  defs (overloaded)
    2.36  static_field_type_is_static_def: 
    2.37 - "is_static (m::(bool,'b::type) static_field_type) \<equiv> static_val m"
    2.38 + "is_static (m::('b::type) member_ext_type) \<equiv> static_val m"
    2.39  
    2.40  lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
    2.41  apply (cases m)
    2.42 @@ -401,37 +401,30 @@
    2.43  axclass has_resTy < "type"
    2.44  consts resTy:: "'a::has_resTy \<Rightarrow> ty"
    2.45  
    2.46 -instance access_field_type :: ("type","has_resTy") has_resTy ..
    2.47 +instance decl_ext_type :: ("has_resTy") has_resTy ..
    2.48  
    2.49  defs (overloaded)
    2.50  decl_resTy_def: 
    2.51   "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" 
    2.52  
    2.53 -instance static_field_type :: ("type","has_resTy") has_resTy ..
    2.54 -
    2.55 -defs (overloaded)
    2.56 -static_field_type_resTy_def: 
    2.57 - "resTy (m::(bool,'b::has_resTy) static_field_type) 
    2.58 -  \<equiv> resTy (static_more m)" 
    2.59 -
    2.60 -instance pars_field_type :: ("type","has_resTy") has_resTy ..
    2.61 +instance member_ext_type :: ("has_resTy") has_resTy ..
    2.62  
    2.63  defs (overloaded)
    2.64 -pars_field_type_resTy_def: 
    2.65 - "resTy (m::(vname list,'b::has_resTy) pars_field_type) 
    2.66 -  \<equiv> resTy (pars_more m)" 
    2.67 +member_ext_type_resTy_def: 
    2.68 + "resTy (m::('b::has_resTy) member_ext_type) 
    2.69 +  \<equiv> resTy (member.more_val m)" 
    2.70  
    2.71 -instance resT_field_type :: ("type","type") has_resTy ..
    2.72 +instance mhead_ext_type :: ("type") has_resTy ..
    2.73  
    2.74  defs (overloaded)
    2.75 -resT_field_type_resTy_def: 
    2.76 - "resTy (m::(ty,'b::type) resT_field_type) 
    2.77 +mhead_ext_type_resTy_def: 
    2.78 + "resTy (m::('b mhead_ext_type)) 
    2.79    \<equiv> resT_val m" 
    2.80  
    2.81  lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
    2.82  apply (cases m)
    2.83 -apply (simp add: decl_resTy_def static_field_type_resTy_def 
    2.84 -                 pars_field_type_resTy_def resT_field_type_resTy_def
    2.85 +apply (simp add: decl_resTy_def member_ext_type_resTy_def 
    2.86 +                 mhead_ext_type_resTy_def 
    2.87                   member.dest_convs mhead.dest_convs)
    2.88  done
    2.89  
     3.1 --- a/src/HOL/Bali/Name.thy	Sat May 01 22:28:51 2004 +0200
     3.2 +++ b/src/HOL/Bali/Name.thy	Mon May 03 23:22:17 2004 +0200
     3.3 @@ -80,7 +80,7 @@
     3.4  consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
     3.5  
     3.6  (* Declare qtname as instance of has_qtname *)
     3.7 -instance pid_field_type::(has_pname,"type") has_qtname ..
     3.8 +instance qtname_ext_type::("type") has_qtname ..
     3.9  
    3.10  defs (overloaded)
    3.11  qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
     4.1 --- a/src/HOL/Bali/TypeRel.thy	Sat May 01 22:28:51 2004 +0200
     4.2 +++ b/src/HOL/Bali/TypeRel.thy	Mon May 03 23:22:17 2004 +0200
     4.3 @@ -545,7 +545,7 @@
     4.4  lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
     4.5  apply (case_tac T)
     4.6  apply (auto)
     4.7 -apply (subgoal_tac "G\<turnstile>pid_field_type\<preceq>\<^sub>C Object")
     4.8 +apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object")
     4.9  apply (auto intro: subcls_ObjectI)
    4.10  done
    4.11  
     5.1 --- a/src/HOL/Bali/TypeSafe.thy	Sat May 01 22:28:51 2004 +0200
     5.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon May 03 23:22:17 2004 +0200
     5.3 @@ -776,12 +776,8 @@
     5.4  apply (force intro: var_tys_Some_eq [THEN iffD2])
     5.5  done
     5.6  
     5.7 -lemma obj_split: "\<And> obj. \<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
     5.8 -proof record_split
     5.9 -  fix tag values more
    5.10 -  show "\<exists>t vs. \<lparr>tag = tag, values = values, \<dots> = more\<rparr> = \<lparr>tag = t, values = vs\<rparr>"
    5.11 -    by auto
    5.12 -qed
    5.13 +lemma obj_split: "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
    5.14 +  by (cases obj) auto
    5.15   
    5.16  lemma AVar_lemma2: "error_free state 
    5.17         \<Longrightarrow> error_free
    5.18 @@ -3602,7 +3598,7 @@
    5.19  	show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
    5.20  	  by (auto dest!: accfield_fields dest: fields_declC)
    5.21  	from accfield
    5.22 -	show fld: "table_of (fields G statC) (fn, statDeclC) = Some f"
    5.23 +	show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f"
    5.24  	  by (auto dest!: accfield_fields)
    5.25  	from wf show "wf_prog G" .
    5.26  	from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
     6.1 --- a/src/HOL/Record.thy	Sat May 01 22:28:51 2004 +0200
     6.2 +++ b/src/HOL/Record.thy	Mon May 03 23:22:17 2004 +0200
     6.3 @@ -1,88 +1,32 @@
     6.4  (*  Title:      HOL/Record.thy
     6.5      ID:         $Id$
     6.6 -    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     6.7 +    Author:     Wolfgang Naraschewski, Norbert Schirmer  and Markus Wenzel, TU Muenchen
     6.8  *)
     6.9  
    6.10 -header {* Extensible records with structural subtyping *}
    6.11 -
    6.12  theory Record = Product_Type
    6.13  files ("Tools/record_package.ML"):
    6.14  
    6.15 -
    6.16 -subsection {* Abstract product types *}
    6.17 -
    6.18 -locale product_type =
    6.19 -  fixes Rep and Abs and pair and dest1 and dest2
    6.20 -  assumes "typedef": "type_definition Rep Abs UNIV"
    6.21 -    and pair: "pair == (\<lambda>a b. Abs (a, b))"
    6.22 -    and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
    6.23 -    and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
    6.24 -
    6.25 -lemma (in product_type)
    6.26 -    "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
    6.27 -  by (simp add: pair type_definition.Abs_inject [OF "typedef"])
    6.28 -
    6.29 -lemma (in product_type) conv1: "dest1 (pair x y) = x"
    6.30 -  by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
    6.31 -
    6.32 -lemma (in product_type) conv2: "dest2 (pair x y) = y"
    6.33 -  by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
    6.34 -
    6.35 -lemma (in product_type) induct [induct type]:
    6.36 -  assumes hyp: "!!x y. P (pair x y)"
    6.37 -  shows "P p"
    6.38 -proof (rule type_definition.Abs_induct [OF "typedef"])
    6.39 -  fix q show "P (Abs q)"
    6.40 -  proof (induct q)
    6.41 -    fix x y have "P (pair x y)" by (rule hyp)
    6.42 -    also have "pair x y = Abs (x, y)" by (simp only: pair)
    6.43 -    finally show "P (Abs (x, y))" .
    6.44 -  qed
    6.45 -qed
    6.46 +ML {*
    6.47 +val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
    6.48 +by (rtac h2 1);
    6.49 +by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
    6.50 +qed "meta_allE";
    6.51 +*}
    6.52  
    6.53 -lemma (in product_type) cases [cases type]:
    6.54 -    "(!!x y. p = pair x y ==> C) ==> C"
    6.55 -  by (induct p) (auto simp add: "inject")
    6.56 -
    6.57 -lemma (in product_type) surjective_pairing:
    6.58 -    "p = pair (dest1 p) (dest2 p)"
    6.59 -  by (induct p) (simp only: conv1 conv2)
    6.60 +lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
    6.61 +  by simp
    6.62  
    6.63 -lemma (in product_type) split_paired_all:
    6.64 -  "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
    6.65 -proof
    6.66 -  fix a b
    6.67 -  assume "!!x. PROP P x"
    6.68 -  thus "PROP P (pair a b)" .
    6.69 -next
    6.70 -  fix x
    6.71 -  assume "!!a b. PROP P (pair a b)"
    6.72 -  hence "PROP P (pair (dest1 x) (dest2 x))" .
    6.73 -  thus "PROP P x" by (simp only: surjective_pairing [symmetric])
    6.74 -qed
    6.75 +lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
    6.76 +  by simp
    6.77  
    6.78 -lemma (in product_type) split_paired_All:
    6.79 -  "(ALL x. P x) = (ALL a b. P (pair a b))"
    6.80 -proof
    6.81 -  fix a b
    6.82 -  assume "ALL x. P x"
    6.83 -  thus "ALL a b. P (pair a b)" by rules
    6.84 -next
    6.85 -  assume P: "ALL a b. P (pair a b)"
    6.86 -  show "ALL x. P x"
    6.87 -  proof
    6.88 -    fix x
    6.89 -    from P have "P (pair (dest1 x) (dest2 x))" by rules
    6.90 -    thus "P x" by (simp only: surjective_pairing [symmetric])
    6.91 -  qed
    6.92 -qed
    6.93 +lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    6.94 +  by simp
    6.95  
    6.96  
    6.97  subsection {* Concrete record syntax *}
    6.98  
    6.99  nonterminals
   6.100    ident field_type field_types field fields update updates
   6.101 -
   6.102  syntax
   6.103    "_constify"           :: "id => ident"                        ("_")
   6.104    "_constify"           :: "longid => ident"                    ("_")
   6.105 @@ -112,10 +56,27 @@
   6.106    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   6.107    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   6.108  
   6.109 +(* 
   6.110  
   6.111 -subsection {* Package setup *}
   6.112 +  "_structure"             :: "fields => 'a"          ("(3{| _ |})")
   6.113 +  "_structure_scheme"      :: "[fields, 'a] => 'a"    ("(3{| _,/ (2... =/ _) |})")
   6.114 +  
   6.115 +  "_structure_update_name":: idt
   6.116 +  "_structure_update"  :: "['a, updates] \<Rightarrow> 'b"    ("_/(3{| _ |})" [900,0] 900)
   6.117  
   6.118 -use "Tools/record_package.ML"
   6.119 -setup RecordPackage.setup
   6.120 +  "_structure_type"        :: "field_types => type"    ("(3{| _ |})")
   6.121 +  "_structure_type_scheme" :: "[field_types, type] => type" 
   6.122 +                                      ("(3{| _,/ (2... ::/ _) |})")
   6.123 +syntax (xsymbols)
   6.124 +
   6.125 + "_structure_scheme"   :: "[fields, 'a] => 'a"       ("(3{|_,/ (2\<dots> =/ _)|})")
   6.126 +
   6.127 +  "_structure_type_scheme" :: "[field_types, type] => type"        
   6.128 +                                      ("(3{|_,/ (2\<dots> ::/ _)|})")
   6.129 +
   6.130 +*)
   6.131 +use "Tools/record_package.ML";
   6.132 +setup RecordPackage.setup;
   6.133  
   6.134  end
   6.135 +
     7.1 --- a/src/HOL/Tools/record_package.ML	Sat May 01 22:28:51 2004 +0200
     7.2 +++ b/src/HOL/Tools/record_package.ML	Mon May 03 23:22:17 2004 +0200
     7.3 @@ -10,10 +10,15 @@
     7.4  sig
     7.5    val record_simproc: simproc
     7.6    val record_eq_simproc: simproc
     7.7 +  val record_upd_simproc: simproc
     7.8 +  val record_split_simproc: (term -> bool) -> simproc
     7.9 +  val record_ex_sel_eq_simproc: simproc
    7.10    val record_split_tac: int -> tactic
    7.11 +  val record_split_simp_tac: (term -> bool) -> int -> tactic
    7.12    val record_split_name: string
    7.13    val record_split_wrapper: string * wrapper
    7.14 -  val print_record_type_abbr: bool ref 
    7.15 +  val print_record_type_abbr: bool ref
    7.16 +  val print_record_type_as_fields: bool ref 
    7.17  end;
    7.18  
    7.19  signature RECORD_PACKAGE =
    7.20 @@ -21,59 +26,73 @@
    7.21    include BASIC_RECORD_PACKAGE
    7.22    val quiet_mode: bool ref
    7.23    val updateN: string
    7.24 -  val mk_fieldT: (string * typ) * typ -> typ
    7.25 -  val dest_fieldT: typ -> (string * typ) * typ
    7.26 -  val dest_fieldTs: typ -> (string * typ) list
    7.27 -  val last_fieldT: typ -> (string * typ) option
    7.28 -  val last_field: Sign.sg -> string -> (string * typ) option
    7.29 -  val get_parents: Sign.sg -> string -> string list
    7.30 -  val mk_field: (string * term) * term -> term
    7.31 -  val mk_fst: term -> term
    7.32 -  val mk_snd: term -> term
    7.33 -  val mk_recordT: (string * typ) list * typ -> typ
    7.34 -  val dest_recordT: typ -> (string * typ) list * typ
    7.35 -  val mk_record: (string * term) list * term -> term
    7.36 -  val mk_sel: term -> string -> term
    7.37 -  val mk_update: term -> string * term -> term
    7.38 +  val ext_typeN: string
    7.39 +  val last_extT: typ -> (string * typ list) option
    7.40 +  val dest_recTs : typ -> (string * typ list) list
    7.41 +  val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option
    7.42    val print_records: theory -> unit
    7.43 -  val add_record: (string list * bstring) -> string option
    7.44 -    -> (bstring * string * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
    7.45 -  val add_record_i: (string list * bstring) -> (typ list * string) option
    7.46 -    -> (bstring * typ * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
    7.47 +  val add_record: string list * string -> string option -> (string * string * mixfix) list 
    7.48 +                  -> theory -> theory
    7.49 +  val add_record_i: string list * string -> (typ list * string) option 
    7.50 +                    -> (string * typ * mixfix) list -> theory -> theory
    7.51    val setup: (theory -> theory) list
    7.52 -  val record_upd_simproc: simproc
    7.53 -  val record_split_simproc: (term -> bool) -> simproc
    7.54 -  val record_ex_sel_eq_simproc: simproc
    7.55 -  val record_split_simp_tac: (term -> bool) -> int -> tactic
    7.56  end;
    7.57  
    7.58 -structure RecordPackage: RECORD_PACKAGE =
    7.59 +
    7.60 +structure RecordPackage :RECORD_PACKAGE =    
    7.61  struct
    7.62  
    7.63 -
    7.64 -(*** theory context references ***)
    7.65 -
    7.66 -val product_typeN = "Record.product_type";
    7.67 -
    7.68 -val product_type_intro = thm "product_type.intro";
    7.69 -val product_type_inject = thm "product_type.inject";
    7.70 -val product_type_conv1 = thm "product_type.conv1";
    7.71 -val product_type_conv2 = thm "product_type.conv2";
    7.72 -val product_type_induct = thm "product_type.induct";
    7.73 -val product_type_cases = thm "product_type.cases";
    7.74 -val product_type_split_paired_all = thm "product_type.split_paired_all";
    7.75 -val product_type_split_paired_All = thm "product_type.split_paired_All";
    7.76 +val rec_UNIV_I = thm "rec_UNIV_I";
    7.77 +val rec_True_simp = thm "rec_True_simp";
    7.78 +val Pair_eq = thm "Product_Type.Pair_eq";
    7.79 +val atomize_all = thm "HOL.atomize_all";
    7.80 +val atomize_imp = thm "HOL.atomize_imp";
    7.81 +val triv_goal   = thm "triv_goal";
    7.82 +val prop_subst  = thm "prop_subst";
    7.83 +val Pair_sel_convs = [fst_conv,snd_conv];
    7.84  
    7.85  
    7.86  
    7.87 +(** name components **)
    7.88 +
    7.89 +val rN = "r";
    7.90 +val moreN = "more";
    7.91 +val schemeN = "_scheme";
    7.92 +val ext_typeN = "_ext_type"; 
    7.93 +val extN ="_ext";
    7.94 +val ext_dest = "_val";
    7.95 +val updateN = "_update";
    7.96 +val schemeN = "_scheme";
    7.97 +val makeN = "make";
    7.98 +val fields_selN = "fields";
    7.99 +val extendN = "extend";
   7.100 +val truncateN = "truncate";
   7.101 +
   7.102 +(*see typedef_package.ML*)
   7.103 +val RepN = "Rep_";
   7.104 +val AbsN = "Abs_";
   7.105 +
   7.106  (*** utilities ***)
   7.107  
   7.108 +
   7.109 +fun last [] = error "RecordPackage.last: empty list"
   7.110 +  | last [x] = x
   7.111 +  | last (x::xs) = last xs;
   7.112 +
   7.113 +fun but_last [] = error "RecordPackage.but_last: empty list"
   7.114 +  | but_last [x] = []
   7.115 +  | but_last (x::xs) = x::but_last xs;
   7.116 +
   7.117 +fun remdups [] = []
   7.118 +  | remdups (x::xs) = x::remdups (filter_out (fn y => y=x) xs);
   7.119 +
   7.120 +fun is_suffix sfx s = is_some (try (unsuffix sfx) s);
   7.121 +
   7.122  (* messages *)
   7.123  
   7.124  val quiet_mode = ref false;
   7.125  fun message s = if ! quiet_mode then () else writeln s;
   7.126  
   7.127 -
   7.128  (* syntax *)
   7.129  
   7.130  fun prune n xs = Library.drop (n, xs);
   7.131 @@ -91,332 +110,66 @@
   7.132  val (op ===) = Trueprop o HOLogic.mk_eq;
   7.133  val (op ==>) = Logic.mk_implies;
   7.134  
   7.135 -
   7.136 -(* attributes *)
   7.137 -
   7.138 -fun case_names_fields x = RuleCases.case_names ["fields"] x;
   7.139 -fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
   7.140 -fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
   7.141 -
   7.142 -
   7.143 -(* tactics *)
   7.144 -
   7.145 -fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
   7.146 -
   7.147 -(* do case analysis / induction on last parameter of ith subgoal (or s) *)
   7.148 -
   7.149 -fun try_param_tac s rule i st =
   7.150 -  let
   7.151 -    val cert = cterm_of (Thm.sign_of_thm st);
   7.152 -    val g = nth_elem (i - 1, prems_of st);
   7.153 -    val params = Logic.strip_params g;
   7.154 -    val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
   7.155 -    val rule' = Thm.lift_rule (st, i) rule;
   7.156 -    val (P, ys) = strip_comb (HOLogic.dest_Trueprop
   7.157 -      (Logic.strip_assums_concl (prop_of rule')));
   7.158 -    val (x, ca) = (case rev (drop (length params, ys)) of
   7.159 -        [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
   7.160 -          (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
   7.161 -      | [x] => (head_of x, false));
   7.162 -    val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
   7.163 -        [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of
   7.164 -          None => sys_error "try_param_tac: no such variable"
   7.165 -        | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl),
   7.166 -            (x, Free (s, T))])
   7.167 -      | (_, T) :: _ => [(P, list_abs (params, if ca then concl
   7.168 -          else incr_boundvars 1 (Abs (s, T, concl)))),
   7.169 -        (x, list_abs (params, Bound 0))])) rule'
   7.170 -  in compose_tac (false, rule'', nprems_of rule) i st end;
   7.171 -
   7.172 -
   7.173 -
   7.174 -(*** code generator data ***)
   7.175 -
   7.176 -val [prod_code, fst_code, snd_code] =
   7.177 -  map (Codegen.parse_mixfix (K (Bound 0))) ["(_,/ _)", "fst", "snd"];
   7.178 -val prodT_code = Codegen.parse_mixfix (K dummyT) "(_ */ _)";
   7.179 -
   7.180 -
   7.181 -
   7.182 -(*** syntax operations ***)
   7.183 -
   7.184 -(** name components **)
   7.185 -
   7.186 -val rN = "r";
   7.187 -val moreN = "more";
   7.188 -val schemeN = "_scheme";
   7.189 -val field_typeN = "_field_type";
   7.190 -val fieldN = "_field";
   7.191 -val fstN = "_val";
   7.192 -val sndN = "_more";
   7.193 -val updateN = "_update";
   7.194 -val makeN = "make";
   7.195 -val fieldsN = "fields";
   7.196 -val extendN = "extend";
   7.197 -val truncateN = "truncate";
   7.198 -
   7.199 -
   7.200 -(*see typedef_package.ML*)
   7.201 -val RepN = "Rep_";
   7.202 -val AbsN = "Abs_";
   7.203 -
   7.204 -
   7.205 -
   7.206 -(** tuple operations **)
   7.207 -
   7.208 -(* types *)
   7.209 -
   7.210 -fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]);
   7.211 -
   7.212 -fun dest_fieldT (typ as Type (c_field_type, [T, U])) =
   7.213 -      (case try (unsuffix field_typeN) c_field_type of
   7.214 -        None => raise TYPE ("dest_fieldT", [typ], [])
   7.215 -      | Some c => ((c, T), U))
   7.216 -  | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []);
   7.217 -
   7.218 -fun dest_fieldTs T =
   7.219 -  let val ((c, T), U) = dest_fieldT T
   7.220 -  in (c, T) :: dest_fieldTs U
   7.221 -  end handle TYPE _ => [];
   7.222 -
   7.223 -fun last_fieldT T =
   7.224 -  let val ((c, T), U) = dest_fieldT T
   7.225 -  in (case last_fieldT U of
   7.226 -        None => Some (c,T)
   7.227 -      | Some l => Some l)
   7.228 -  end handle TYPE _ => None
   7.229 -
   7.230  (* morphisms *)
   7.231  
   7.232 -fun mk_Rep U (c, T) =
   7.233 -  Const (suffix field_typeN (prefix_base RepN c),
   7.234 -    mk_fieldT ((c, T), U) --> HOLogic.mk_prodT (T, U));
   7.235 +fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
   7.236 +fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name);
   7.237  
   7.238 -fun mk_Abs U (c, T) =
   7.239 -  Const (suffix field_typeN (prefix_base AbsN c),
   7.240 -    HOLogic.mk_prodT (T, U) --> mk_fieldT ((c, T), U));
   7.241 -
   7.242 +fun mk_Rep name repT absT  =
   7.243 +  Const (suffix ext_typeN (prefix_base RepN name),absT --> repT);
   7.244  
   7.245 -(* constructors *)
   7.246 +fun mk_Abs name repT absT =
   7.247 +  Const (mk_AbsN name,repT --> absT);
   7.248  
   7.249 -fun mk_fieldC U (c, T) = (suffix fieldN c, T --> U --> mk_fieldT ((c, T), U));
   7.250 +(* constructor *)
   7.251  
   7.252 -fun mk_field ((c, t), u) =
   7.253 -  let val T = fastype_of t and U = fastype_of u
   7.254 -  in Const (suffix fieldN c, [T, U] ---> mk_fieldT ((c, T), U)) $ t $ u end;
   7.255 +fun mk_extC (name,T) Ts  = (suffix extN name, Ts ---> T);
   7.256  
   7.257 +fun mk_ext (name,T) ts =
   7.258 +  let val Ts = map fastype_of ts
   7.259 +  in list_comb (Const (mk_extC (name,T) Ts),ts) end;
   7.260  
   7.261 -(* destructors *)
   7.262 +(* selector *)
   7.263 +
   7.264 +fun mk_selC sT (c,T) = (c,sT --> T);
   7.265  
   7.266 -fun mk_fstC U (c, T) = (suffix fstN c, mk_fieldT ((c, T), U) --> T);
   7.267 -fun mk_sndC U (c, T) = (suffix sndN c, mk_fieldT ((c, T), U) --> U);
   7.268 +fun mk_sel s (c,T) =
   7.269 +  let val sT = fastype_of s
   7.270 +  in Const (mk_selC sT (c,T)) $ s end;
   7.271  
   7.272 -fun dest_field fst_or_snd p =
   7.273 -  let
   7.274 -    val pT = fastype_of p;
   7.275 -    val ((c, T), U) = dest_fieldT pT;
   7.276 -    val (destN, destT) = if fst_or_snd then (fstN, T) else (sndN, U);
   7.277 -  in Const (suffix destN c, pT --> destT) $ p end;
   7.278 +(* updates *)
   7.279 +
   7.280 +fun mk_updC sT (c,T) = (suffix updateN c, T --> sT --> sT);
   7.281  
   7.282 -val mk_fst = dest_field true;
   7.283 -val mk_snd = dest_field false;
   7.284 -
   7.285 -
   7.286 -
   7.287 -(** record operations **)
   7.288 +fun mk_upd c v s =
   7.289 +  let val sT = fastype_of s;
   7.290 +      val vT = fastype_of v;
   7.291 +  in Const (mk_updC sT (c, vT)) $ v $ s end;
   7.292  
   7.293  (* types *)
   7.294  
   7.295 -val mk_recordT = foldr mk_fieldT;
   7.296 -
   7.297 -fun dest_recordT T =
   7.298 -  (case try dest_fieldT T of
   7.299 -    None => ([], T)
   7.300 -  | Some (c_T, U) => apfst (cons c_T) (dest_recordT U));
   7.301 -
   7.302 -fun find_fieldT c rT =
   7.303 -  (case assoc (fst (dest_recordT rT), c) of
   7.304 -    None => raise TYPE ("find_field: " ^ c, [rT], [])
   7.305 -  | Some T => T);
   7.306 -
   7.307 -
   7.308 -(* constructors *)
   7.309 -
   7.310 -val mk_record = foldr mk_field;
   7.311 -
   7.312 -
   7.313 -(* selectors *)
   7.314 -
   7.315 -fun mk_selC rT (c, T) = (c, rT --> T);
   7.316 -
   7.317 -fun mk_sel r c =
   7.318 -  let val rT = fastype_of r
   7.319 -  in Const (mk_selC rT (c, find_fieldT c rT)) $ r end;
   7.320 -
   7.321 -fun mk_named_sels names r = names ~~ map (mk_sel r) names;
   7.322 -
   7.323 -val mk_moreC = mk_selC;
   7.324 -
   7.325 -fun mk_more r c =
   7.326 -  let val rT = fastype_of r
   7.327 -  in Const (mk_moreC rT (c, snd (dest_recordT rT))) $ r end;
   7.328 -
   7.329 -
   7.330 -(* updates *)
   7.331 -
   7.332 -fun mk_updateC rT (c, T) = (suffix updateN c, T --> rT --> rT);
   7.333 -
   7.334 -fun mk_update r (c, x) =
   7.335 -  let val rT = fastype_of r
   7.336 -  in Const (mk_updateC rT (c, find_fieldT c rT)) $ x $ r end;
   7.337 -
   7.338 -val mk_more_updateC = mk_updateC;
   7.339 +fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) =
   7.340 +      (case try (unsuffix ext_typeN) c_ext_type of
   7.341 +        None => raise TYPE ("RecordPackage.dest_recT", [typ], [])
   7.342 +      | Some c => ((c, Ts), last Ts))
   7.343 +  | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []);
   7.344  
   7.345 -fun mk_more_update r (c, x) =
   7.346 -  let val rT = fastype_of r
   7.347 -  in Const (mk_more_updateC rT (c, snd (dest_recordT rT))) $ x $ r end;
   7.348 -
   7.349 -
   7.350 -
   7.351 -(** concrete syntax for records **)
   7.352 -
   7.353 -(* parse translations *)
   7.354 -
   7.355 -fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
   7.356 -      if c = mark then Syntax.const (suffix sfx name) $ arg
   7.357 -      else raise TERM ("gen_field_tr: " ^ mark, [t])
   7.358 -  | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
   7.359 -
   7.360 -fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
   7.361 -      if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
   7.362 -      else [gen_field_tr mark sfx tm]
   7.363 -  | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
   7.364 -
   7.365 -fun gen_record_tr sep mark sfx unit [t] = foldr (op $) (gen_fields_tr sep mark sfx t, unit)
   7.366 -  | gen_record_tr _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   7.367 -
   7.368 -fun gen_record_scheme_tr sep mark sfx [t, more] = foldr (op $) (gen_fields_tr sep mark sfx t, more)
   7.369 -  | gen_record_scheme_tr _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   7.370 -
   7.371 -
   7.372 -val record_type_tr = gen_record_tr "_field_types" "_field_type" field_typeN (Syntax.const "unit");
   7.373 -val record_type_scheme_tr = gen_record_scheme_tr "_field_types" "_field_type" field_typeN;
   7.374 -
   7.375 -val record_tr = gen_record_tr "_fields" "_field" fieldN HOLogic.unit;
   7.376 -val record_scheme_tr = gen_record_scheme_tr "_fields" "_field" fieldN;
   7.377 -
   7.378 -fun record_update_tr [t, u] =
   7.379 -      foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
   7.380 -  | record_update_tr ts = raise TERM ("record_update_tr", ts);
   7.381 -
   7.382 -
   7.383 -fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
   7.384 -  | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
   7.385 -  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
   7.386 -      (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
   7.387 -  | update_name_tr ts = raise TERM ("update_name_tr", ts);
   7.388 -
   7.389 +fun is_recT T =
   7.390 +  (case try dest_recT T of None => false | Some _ => true); 
   7.391  
   7.392 -val parse_translation =
   7.393 - [("_record_type", record_type_tr),
   7.394 -  ("_record_type_scheme", record_type_scheme_tr),
   7.395 -  ("_record", record_tr),
   7.396 -  ("_record_scheme", record_scheme_tr),
   7.397 -  ("_record_update", record_update_tr),
   7.398 -  ("_update_name", update_name_tr)];
   7.399 -
   7.400 -
   7.401 -(* print translations *)
   7.402 -
   7.403 -
   7.404 -val print_record_type_abbr = ref true;
   7.405 -
   7.406 -fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
   7.407 -      (case try (unsuffix sfx) name_field of
   7.408 -        Some name =>
   7.409 -          apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_fields_tr' mark sfx u)
   7.410 -      | None => ([], tm))
   7.411 -  | gen_fields_tr' _ _ tm = ([], tm);
   7.412 -
   7.413 -fun gen_record_tr' sep mark sfx is_unit record record_scheme tm =
   7.414 -  let
   7.415 -    val (ts, u) = gen_fields_tr' mark sfx tm;
   7.416 -    val t' = foldr1 (fn (v, w) => Syntax.const sep $ v $ w) ts;
   7.417 -  in
   7.418 -    if is_unit u then Syntax.const record $ t'
   7.419 -    else Syntax.const record_scheme $ t' $ u
   7.420 -  end;
   7.421 -
   7.422 -
   7.423 -val record_type_tr' =
   7.424 -  gen_record_tr' "_field_types" "_field_type" field_typeN
   7.425 -    (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme";
   7.426 -
   7.427 -
   7.428 -(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
   7.429 -(* the (nested) field types.                                                        *)
   7.430 -fun record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT tm =
   7.431 -  let
   7.432 -      (* tm is term representation of a (nested) field type. We first reconstruct the      *)
   7.433 -      (* type from tm so that we can continue on the type level rather then the term level.*)
   7.434 - 
   7.435 -      fun get_sort xs n = (case assoc (xs,n) of 
   7.436 -                             Some s => s 
   7.437 -                           | None => Sign.defaultS sg);
   7.438 -
   7.439 -      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm);
   7.440 -      val tsig = Sign.tsig_of sg;
   7.441 +fun dest_recTs T =
   7.442 +  let val ((c, Ts), U) = dest_recT T
   7.443 +  in (c, Ts) :: dest_recTs U
   7.444 +  end handle TYPE _ => [];
   7.445  
   7.446 -      fun mk_type_abbr subst name alphas = 
   7.447 -          let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
   7.448 -          in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
   7.449 -
   7.450 -      fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
   7.451 -
   7.452 -   in if !print_record_type_abbr
   7.453 -      then (case last_fieldT T of
   7.454 -             Some (name,_) 
   7.455 -              => if name = lastF 
   7.456 -                 then
   7.457 -		   let val subst = unify rec_schemeT T 
   7.458 -                   in 
   7.459 -                    if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
   7.460 -                    then mk_type_abbr subst abbr alphas
   7.461 -                    else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
   7.462 -		   end handle TUNIFY => record_type_tr' tm
   7.463 -                 else raise Match (* give print translation of specialised record a chance *)
   7.464 -            | _ => record_type_tr' tm)
   7.465 -       else record_type_tr' tm
   7.466 -  end
   7.467 +fun last_extT T =
   7.468 +  let val ((c, Ts), U) = dest_recT T
   7.469 +  in (case last_extT U of
   7.470 +        None => Some (c,Ts)
   7.471 +      | Some l => Some l)
   7.472 +  end handle TYPE _ => None
   7.473  
   7.474 -     
   7.475 -fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT name =
   7.476 -  let val name_sfx = suffix field_typeN name
   7.477 -      val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT 
   7.478 -  in (name_sfx, fn [t,u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   7.479 -      
   7.480 -val record_tr' =
   7.481 -  gen_record_tr' "_fields" "_field" fieldN
   7.482 -    (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme";
   7.483 -
   7.484 -fun record_update_tr' tm =
   7.485 -  let val (ts, u) = gen_fields_tr' "_update" updateN tm in
   7.486 -    Syntax.const "_record_update" $ u $
   7.487 -      foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   7.488 -  end;
   7.489 -
   7.490 -fun gen_field_tr' sfx tr' name =
   7.491 -  let val name_sfx = suffix sfx name
   7.492 -  in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   7.493 -
   7.494 -fun print_translation names =
   7.495 -  map (gen_field_tr' fieldN record_tr') names @
   7.496 -  map (gen_field_tr' updateN record_update_tr') names;
   7.497 -
   7.498 -fun print_translation_field_types names =
   7.499 -  map (gen_field_tr' field_typeN record_type_tr') names
   7.500 -
   7.501 -
   7.502 +fun rec_id T = foldl (fn (s,(c,T)) => s ^ c) ("",dest_recTs T);
   7.503  
   7.504  (*** extend theory by record definition ***)
   7.505  
   7.506 @@ -428,29 +181,26 @@
   7.507   {args: (string * sort) list,
   7.508    parent: (typ list * string) option,
   7.509    fields: (string * typ) list,
   7.510 -  field_inducts: thm list,
   7.511 -  field_cases: thm list,
   7.512 -  field_splits: thm list,
   7.513 -  simps: thm list};
   7.514 +  extension: (string * typ list),
   7.515 +  induct: thm
   7.516 + };
   7.517  
   7.518 -fun make_record_info args parent fields field_inducts field_cases field_splits simps =
   7.519 - {args = args, parent = parent, fields = fields, field_inducts = field_inducts,
   7.520 -  field_cases = field_cases, field_splits = field_splits, simps = simps}: record_info;
   7.521 +fun make_record_info args parent fields extension induct =
   7.522 + {args = args, parent = parent, fields = fields, extension = extension, 
   7.523 +  induct = induct}: record_info;
   7.524 +
   7.525  
   7.526  type parent_info =
   7.527   {name: string,
   7.528    fields: (string * typ) list,
   7.529 -  field_inducts: thm list,
   7.530 -  field_cases: thm list,
   7.531 -  field_splits: thm list,
   7.532 -  simps: thm list};
   7.533 +  extension: (string * typ list),
   7.534 +  induct: thm
   7.535 +};
   7.536  
   7.537 -fun make_parent_info name fields field_inducts field_cases field_splits simps =
   7.538 - {name = name, fields = fields, field_inducts = field_inducts,
   7.539 -  field_cases = field_cases, field_splits = field_splits, simps = simps}: parent_info;
   7.540 +fun make_parent_info name fields extension induct =
   7.541 + {name = name, fields = fields, extension = extension, induct = induct}: parent_info;
   7.542  
   7.543 -
   7.544 -(* data kind 'HOL/records' *)
   7.545 +(* data kind 'HOL/record' *)
   7.546  
   7.547  type record_data =
   7.548   {records: record_info Symtab.table,
   7.549 @@ -458,52 +208,54 @@
   7.550     {selectors: unit Symtab.table,
   7.551      updates: string Symtab.table,
   7.552      simpset: Simplifier.simpset},
   7.553 -  field_splits:
   7.554 -   {fields: unit Symtab.table,
   7.555 -    simpset: Simplifier.simpset},
   7.556    equalities: thm Symtab.table,
   7.557 -  splits: (thm*thm*thm*thm) Symtab.table (* !!,!,EX - split-equalities,induct rule *) 
   7.558 +  splits: (thm*thm*thm*thm) Symtab.table,    (* !!,!,EX - split-equalities,induct rule *) 
   7.559 +  extfields: (string*typ) list Symtab.table, (* maps extension to its fields *)
   7.560 +  fieldext: (string*typ list) Symtab.table   (* maps field to its extension *)
   7.561  };
   7.562  
   7.563 -fun make_record_data records sel_upd field_splits equalities splits =
   7.564 - {records = records, sel_upd = sel_upd, field_splits = field_splits,
   7.565 -  equalities = equalities, splits = splits}: record_data;
   7.566 +fun make_record_data records sel_upd equalities splits extfields fieldext =
   7.567 + {records = records, sel_upd = sel_upd, 
   7.568 +  equalities = equalities, splits = splits, 
   7.569 +  extfields = extfields, fieldext = fieldext }: record_data;
   7.570  
   7.571  structure RecordsArgs =
   7.572  struct
   7.573 -  val name = "HOL/records";
   7.574 +  val name = "HOL/records";    
   7.575    type T = record_data;
   7.576  
   7.577    val empty =
   7.578      make_record_data Symtab.empty
   7.579        {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
   7.580 -      {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty Symtab.empty;
   7.581 +      Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
   7.582  
   7.583    val copy = I;
   7.584    val prep_ext = I;
   7.585    fun merge
   7.586     ({records = recs1,
   7.587       sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
   7.588 -     field_splits = {fields = flds1, simpset = fld_ss1},
   7.589       equalities = equalities1,
   7.590 -     splits = splits1},
   7.591 +     splits = splits1,
   7.592 +     extfields = extfields1,
   7.593 +     fieldext = fieldext1},
   7.594      {records = recs2,
   7.595       sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
   7.596 -     field_splits = {fields = flds2, simpset = fld_ss2},
   7.597       equalities = equalities2, 
   7.598 -     splits = splits2}) =
   7.599 +     splits = splits2,
   7.600 +     extfields = extfields2,
   7.601 +     fieldext = fieldext2}) =
   7.602      make_record_data  
   7.603        (Symtab.merge (K true) (recs1, recs2))
   7.604        {selectors = Symtab.merge (K true) (sels1, sels2),
   7.605          updates = Symtab.merge (K true) (upds1, upds2),
   7.606          simpset = Simplifier.merge_ss (ss1, ss2)}
   7.607 -      {fields = Symtab.merge (K true) (flds1, flds2),
   7.608 -        simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)}
   7.609        (Symtab.merge Thm.eq_thm (equalities1, equalities2))
   7.610        (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
   7.611                       => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
   7.612                          Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) 
   7.613 -                    (splits1, splits2));
   7.614 +                    (splits1, splits2))
   7.615 +      (Symtab.merge (K true) (extfields1,extfields2))
   7.616 +      (Symtab.merge (K true) (fieldext1,fieldext2));
   7.617  
   7.618    fun print sg ({records = recs, ...}: record_data) =
   7.619      let
   7.620 @@ -527,24 +279,28 @@
   7.621  structure RecordsData = TheoryDataFun(RecordsArgs);
   7.622  val print_records = RecordsData.print;
   7.623  
   7.624 -
   7.625  (* access 'records' *)
   7.626  
   7.627  fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
   7.628  
   7.629  fun put_record name info thy =
   7.630    let
   7.631 -    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   7.632 +    val {records, sel_upd, equalities, splits,extfields,fieldext} = RecordsData.get thy;
   7.633      val data = make_record_data (Symtab.update ((name, info), records))
   7.634 -      sel_upd field_splits equalities splits;
   7.635 +      sel_upd equalities splits extfields fieldext;
   7.636    in RecordsData.put data thy end;
   7.637  
   7.638 -
   7.639  (* access 'sel_upd' *)
   7.640  
   7.641  fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg);
   7.642  
   7.643  fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
   7.644 +fun is_selector sg name = 
   7.645 +  case get_selectors sg (Sign.intern_const sg name) of 
   7.646 +     None => false
   7.647 +   | Some _ => true
   7.648 +
   7.649 +                             
   7.650  fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name);
   7.651  fun get_simpset sg = #simpset (get_sel_upd sg);
   7.652  
   7.653 @@ -553,36 +309,22 @@
   7.654      val sels = map (rpair ()) names;
   7.655      val upds = map (suffix updateN) names ~~ names;
   7.656  
   7.657 -    val {records, sel_upd = {selectors, updates, simpset}, field_splits,
   7.658 -      equalities, splits} = RecordsData.get thy;
   7.659 +    val {records, sel_upd = {selectors, updates, simpset}, 
   7.660 +      equalities, splits, extfields,fieldext} = RecordsData.get thy;
   7.661      val data = make_record_data records
   7.662        {selectors = Symtab.extend (selectors, sels),
   7.663          updates = Symtab.extend (updates, upds),
   7.664          simpset = Simplifier.addsimps (simpset, simps)}
   7.665 -      field_splits equalities splits;
   7.666 +       equalities splits extfields fieldext;
   7.667    in RecordsData.put data thy end;
   7.668  
   7.669 -
   7.670 -(* access 'field_splits' *)
   7.671 -
   7.672 -fun add_field_splits names simps thy =
   7.673 -  let
   7.674 -    val {records, sel_upd, field_splits = {fields, simpset},
   7.675 -      equalities, splits} = RecordsData.get thy;
   7.676 -    val flds = map (rpair ()) names;
   7.677 -    val data = make_record_data records sel_upd
   7.678 -      {fields = Symtab.extend (fields, flds),
   7.679 -       simpset = Simplifier.addsimps (simpset, simps)} equalities splits;
   7.680 -  in RecordsData.put data thy end;
   7.681 -
   7.682 -
   7.683  (* access 'equalities' *)
   7.684  
   7.685  fun add_record_equalities name thm thy =
   7.686    let
   7.687 -    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   7.688 -    val data = make_record_data records sel_upd field_splits
   7.689 -      (Symtab.update_new ((name, thm), equalities)) splits;
   7.690 +    val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy;
   7.691 +    val data = make_record_data records sel_upd 
   7.692 +      (Symtab.update_new ((name, thm), equalities)) splits extfields fieldext;
   7.693    in RecordsData.put data thy end;
   7.694  
   7.695  fun get_equalities sg name =
   7.696 @@ -592,28 +334,46 @@
   7.697  
   7.698  fun add_record_splits name thmP thy =
   7.699    let
   7.700 -    val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   7.701 -    val data = make_record_data records sel_upd field_splits
   7.702 -      equalities (Symtab.update_new ((name, thmP), splits));
   7.703 +    val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy;
   7.704 +    val data = make_record_data records sel_upd 
   7.705 +      equalities (Symtab.update_new ((name, thmP), splits)) extfields fieldext;
   7.706    in RecordsData.put data thy end;
   7.707  
   7.708  fun get_splits sg name =
   7.709    Symtab.lookup (#splits (RecordsData.get_sg sg), name);
   7.710  
   7.711 -(* last field of a record *)
   7.712 -fun last_field sg name =
   7.713 -      case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
   7.714 -        Some r => Some (hd (rev (#fields r)))
   7.715 +(* extension of a record name *)
   7.716 +fun get_extension sg name =
   7.717 + case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
   7.718 +        Some s => Some (#extension s)
   7.719        | None => None;
   7.720  
   7.721 -(* get parent names *)
   7.722 -fun get_parents sg name =
   7.723 -     (case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
   7.724 -         Some r => (case #parent r of
   7.725 -                     Some (_,p) => p::get_parents sg p
   7.726 -                   | None => [])
   7.727 -      | None => [])
   7.728 -       
   7.729 +(* access 'extfields' *)
   7.730 +
   7.731 +fun add_extfields name fields thy =
   7.732 +  let
   7.733 +    val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy;
   7.734 +    val data = make_record_data records sel_upd 
   7.735 +         equalities splits (Symtab.update_new ((name, fields), extfields)) fieldext;
   7.736 +  in RecordsData.put data thy end;
   7.737 +
   7.738 +fun get_extfields sg name =
   7.739 +  Symtab.lookup (#extfields (RecordsData.get_sg sg), name);
   7.740 +
   7.741 +(* access 'fieldext' *)
   7.742 +
   7.743 +fun add_fieldext extname_types fields thy =
   7.744 +  let
   7.745 +    val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy;
   7.746 +    val fieldext' = foldl (fn (table,field) => Symtab.update_new ((field,extname_types),table))  
   7.747 +                          (fieldext,fields);
   7.748 +    val data = make_record_data records sel_upd equalities splits extfields fieldext';
   7.749 +  in RecordsData.put data thy end;
   7.750 +
   7.751 +
   7.752 +fun get_fieldext sg name =
   7.753 +  Symtab.lookup (#fieldext (RecordsData.get_sg sg), name);
   7.754 +
   7.755  (* parent records *)
   7.756  
   7.757  fun add_parents thy None parents = parents
   7.758 @@ -622,7 +382,7 @@
   7.759          val sign = Theory.sign_of thy;
   7.760          fun err msg = error (msg ^ " parent record " ^ quote name);
   7.761  
   7.762 -        val {args, parent, fields, field_inducts, field_cases, field_splits, simps} =
   7.763 +        val {args, parent, fields, extension, induct} =
   7.764            (case get_record thy name of Some info => info | None => err "Unknown");
   7.765          val _ = if length types <> length args then err "Bad number of arguments for" else ();
   7.766  
   7.767 @@ -634,33 +394,342 @@
   7.768          val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x)));
   7.769          val parent' = apsome (apfst (map subst)) parent;
   7.770          val fields' = map (apsnd subst) fields;
   7.771 +        val extension' = apsnd (map subst) extension;
   7.772        in
   7.773          conditional (not (null bads)) (fn () =>
   7.774            err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
   7.775          add_parents thy parent'
   7.776 -          (make_parent_info name fields' field_inducts field_cases field_splits simps::parents)
   7.777 +          (make_parent_info name fields' extension' induct::parents)
   7.778        end;
   7.779  
   7.780  
   7.781 +(** concrete syntax for records **)
   7.782 +
   7.783 +(* parse translations *)
   7.784 +
   7.785 +fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
   7.786 +      if c = mark then Syntax.const (suffix sfx name) $ arg
   7.787 +      else raise TERM ("gen_field_tr: " ^ mark, [t])
   7.788 +  | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
   7.789 +
   7.790 +fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
   7.791 +      if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
   7.792 +      else [gen_field_tr mark sfx tm]
   7.793 +  | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
   7.794 +
   7.795 +
   7.796 +fun record_update_tr [t, u] =
   7.797 +      foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
   7.798 +  | record_update_tr ts = raise TERM ("record_update_tr", ts);
   7.799 +
   7.800 +fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
   7.801 +  | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
   7.802 +  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
   7.803 +      (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
   7.804 +  | update_name_tr ts = raise TERM ("update_name_tr", ts);
   7.805 +
   7.806 +fun dest_ext_field mark (t as (Const (c,_) $ Const (name,_) $ arg)) =
   7.807 +     if c = mark then (name,arg) else raise TERM ("dest_ext_field: " ^ mark, [t])
   7.808 +  | dest_ext_field _ t = raise TERM ("dest_ext_field", [t])
   7.809 +
   7.810 +fun dest_ext_fields sep mark (trm as (Const (c,_) $ t $ u)) =
   7.811 +     if c = sep then dest_ext_field mark t::dest_ext_fields sep mark u
   7.812 +     else [dest_ext_field mark trm]
   7.813 +  | dest_ext_fields _ mark t = [dest_ext_field mark t]
   7.814 +
   7.815 +fun gen_ext_fields_tr sep mark sfx more sg t =
   7.816 +  let 
   7.817 +    val fieldargs = dest_ext_fields sep mark t; 
   7.818 +    fun splitargs (field::fields) ((name,arg)::fargs) =
   7.819 +          if is_suffix name field
   7.820 +          then let val (args,rest) = splitargs fields fargs
   7.821 +               in (arg::args,rest) end
   7.822 +          else raise TERM ("gen_ext_fields_tr: expecting field " ^ field ^ 
   7.823 +                           " but got " ^ name, [t])
   7.824 +      | splitargs [] (fargs as (_::_)) = ([],fargs)
   7.825 +      | splitargs (_::_) [] = raise TERM ("gen_ext_fields_tr: expecting more fields", [t])
   7.826 +      | splitargs _ _ = ([],[]);
   7.827 +
   7.828 +    fun mk_ext (fargs as (name,arg)::_) =
   7.829 +         (case get_fieldext sg (Sign.intern_const sg name) of
   7.830 +            Some (ext,_) => (case get_extfields sg ext of
   7.831 +                               Some flds 
   7.832 +                                 => let val (args,rest) = 
   7.833 +                                               splitargs (map fst (but_last flds)) fargs;
   7.834 +                                        val more' = mk_ext rest;  
   7.835 +                                    in list_comb (Syntax.const (suffix sfx ext),args@[more'])
   7.836 +                                    end
   7.837 +                             | None => raise TERM("gen_ext_fields_tr: no fields defined for "
   7.838 +                                                   ^ ext,[t]))
   7.839 +          | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t]))
   7.840 +      | mk_ext [] = more
   7.841 +
   7.842 +  in mk_ext fieldargs end;   
   7.843 +
   7.844 +fun gen_ext_type_tr sep mark sfx more sg t =
   7.845 +  let 
   7.846 +    val fieldargs = dest_ext_fields sep mark t; 
   7.847 +    fun splitargs (field::fields) ((name,arg)::fargs) =
   7.848 +          if is_suffix name field
   7.849 +          then let val (args,rest) = splitargs fields fargs
   7.850 +               in (arg::args,rest) end
   7.851 +          else raise TERM ("gen_ext_type_tr: expecting field " ^ field ^ 
   7.852 +                           " but got " ^ name, [t])
   7.853 +      | splitargs [] (fargs as (_::_)) = ([],fargs)
   7.854 +      | splitargs (_::_) [] = raise TERM ("gen_ext_type_tr: expecting more fields", [t])
   7.855 +      | splitargs _ _ = ([],[]);
   7.856 +
   7.857 +    fun get_sort xs n = (case assoc (xs,n) of 
   7.858 +                                Some s => s 
   7.859 +                              | None => Sign.defaultS sg);
   7.860 +    fun to_type t = Sign.intern_typ sg 
   7.861 +                      (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t);
   7.862 + 
   7.863 +    val tsig = Sign.tsig_of sg;
   7.864 +    fun unify (t,env) = Type.unify tsig env t; 
   7.865 +    
   7.866 +    fun mk_ext (fargs as (name,arg)::_) =
   7.867 +         (case get_fieldext sg (Sign.intern_const sg name) of
   7.868 +            Some (ext,alphas) => 
   7.869 +              (case get_extfields sg ext of
   7.870 +                 Some flds 
   7.871 +                  => (let
   7.872 +                       val flds' = but_last flds;
   7.873 +                       val types = map snd flds'; 
   7.874 +                       val (args,rest) = splitargs (map fst flds') fargs;
   7.875 +                       val vartypes = map Type.varifyT types;
   7.876 +                       val argtypes = map to_type args;
   7.877 +                       val (subst,_) = foldr unify (vartypes ~~ argtypes,(Vartab.empty,0));
   7.878 +                       val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o 
   7.879 +                                          (Envir.norm_type subst) o Type.varifyT) 
   7.880 +                                         (but_last alphas);
   7.881 + 
   7.882 +                       val more' = mk_ext rest;   
   7.883 +                     in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) 
   7.884 +                     end handle TUNIFY => raise 
   7.885 +                           TERM ("gen_ext_type_tr: type is no proper record (extension)", [t]))
   7.886 +               | None => raise TERM ("gen_ext_fields_tr: no fields defined for " ^ ext,[t]))
   7.887 +          | None => raise TERM ("gen_ext_fields_tr: "^ name ^" is no proper field",[t]))
   7.888 +      | mk_ext [] = more
   7.889 +
   7.890 +  in mk_ext fieldargs end;   
   7.891 +
   7.892 +fun gen_adv_record_tr sep mark sfx unit sg [t] = 
   7.893 +      gen_ext_fields_tr sep mark sfx unit sg t
   7.894 +  | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   7.895 +
   7.896 +fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] = 
   7.897 +      gen_ext_fields_tr sep mark sfx more sg t 
   7.898 +  | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   7.899 +
   7.900 +fun gen_adv_record_type_tr sep mark sfx unit sg [t] = 
   7.901 +      gen_ext_type_tr sep mark sfx unit sg t
   7.902 +  | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   7.903 +
   7.904 +fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] = 
   7.905 +      gen_ext_type_tr sep mark sfx more sg t 
   7.906 +  | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   7.907 +
   7.908 +val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
   7.909 +val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN;
   7.910 +
   7.911 +val adv_record_type_tr = 
   7.912 +      gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN 
   7.913 +        (Syntax.term_of_typ false (HOLogic.unitT));
   7.914 +val adv_record_type_scheme_tr = 
   7.915 +      gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
   7.916 +
   7.917 +val parse_translation =
   7.918 + [("_record_update", record_update_tr),
   7.919 +  ("_update_name", update_name_tr)];
   7.920 +
   7.921 +val adv_parse_translation = 
   7.922 + [("_record",adv_record_tr),
   7.923 +  ("_record_scheme",adv_record_scheme_tr),
   7.924 +  ("_record_type",adv_record_type_tr),
   7.925 +  ("_record_type_scheme",adv_record_type_scheme_tr)];
   7.926 +
   7.927 +
   7.928 +(* print translations *)
   7.929 +
   7.930 +val print_record_type_abbr = ref true;
   7.931 +val print_record_type_as_fields = ref true;
   7.932 +
   7.933 +fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
   7.934 +    (case try (unsuffix sfx) name_field of
   7.935 +      Some name =>
   7.936 +        apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
   7.937 +     | None => ([], tm))
   7.938 +  | gen_field_upds_tr' _ _ tm = ([], tm);
   7.939 +
   7.940 +fun record_update_tr' tm =
   7.941 +  let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in
   7.942 +    Syntax.const "_record_update" $ u $
   7.943 +      foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   7.944 +  end;
   7.945 +
   7.946 +fun gen_field_tr' sfx tr' name =
   7.947 +  let val name_sfx = suffix sfx name
   7.948 +  in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   7.949 +
   7.950 +fun record_tr' sep mark record record_scheme unit sg t =
   7.951 +  let 
   7.952 +    fun field_lst t =
   7.953 +      (case strip_comb t of
   7.954 +        (Const (ext,_),args) 
   7.955 +         => (case try (unsuffix extN) (Sign.intern_const sg ext) of
   7.956 +               Some ext' 
   7.957 +               => (case get_extfields sg ext' of
   7.958 +                     Some flds 
   7.959 +                     => (let
   7.960 +                          val (f::fs) = but_last (map fst flds);
   7.961 +                          val flds' = Sign.extern sg Sign.constK f::map NameSpace.base fs; 
   7.962 +                          val (args',more) = split_last args; 
   7.963 +                         in (flds'~~args')@field_lst more end
   7.964 +                         handle LIST _ => [("",t)]) 
   7.965 +                   | None => [("",t)])
   7.966 +             | None => [("",t)])
   7.967 +       | _ => [("",t)])
   7.968 +
   7.969 +    val (flds,(_,more)) = split_last (field_lst t);
   7.970 +    val flds' = map (fn (n,t)=>Syntax.const mark$Syntax.const n$t) flds;
   7.971 +    val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
   7.972 +
   7.973 +  in if null flds then raise Match
   7.974 +     else if unit more  
   7.975 +          then Syntax.const record$flds'' 
   7.976 +          else Syntax.const record_scheme$flds''$more
   7.977 +  end
   7.978 +
   7.979 +fun gen_record_tr' name = 
   7.980 +  let val name_sfx = suffix extN name;
   7.981 +      val unit = (fn Const ("Unity",_) => true | _ => false);
   7.982 +      fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg 
   7.983 +                       (list_comb (Syntax.const name_sfx,ts))
   7.984 +  in (name_sfx,tr')
   7.985 +  end
   7.986 +
   7.987 +fun print_translation names =
   7.988 +  map (gen_field_tr' updateN record_update_tr') names;
   7.989 +
   7.990 +(* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
   7.991 +(* the (nested) extension types.                                                    *)
   7.992 +fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg tm =
   7.993 +  let
   7.994 +      (* tm is term representation of a (nested) field type. We first reconstruct the      *)
   7.995 +      (* type from tm so that we can continue on the type level rather then the term level.*)
   7.996 +
   7.997 +      fun get_sort xs n = (case assoc (xs,n) of 
   7.998 +                             Some s => s 
   7.999 +                           | None => Sign.defaultS sg);
  7.1000 +
  7.1001 +      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) 
  7.1002 +      val tsig = Sign.tsig_of sg
  7.1003 +
  7.1004 +      fun mk_type_abbr subst name alphas = 
  7.1005 +          let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
  7.1006 +          in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
  7.1007 +
  7.1008 +      fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
  7.1009 +
  7.1010 +   in if !print_record_type_abbr
  7.1011 +      then (case last_extT T of
  7.1012 +             Some (name,_) 
  7.1013 +              => if name = lastExt 
  7.1014 +                 then
  7.1015 +		  (let val subst = unify schemeT T 
  7.1016 +                   in 
  7.1017 +                    if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
  7.1018 +                    then mk_type_abbr subst abbr alphas
  7.1019 +                    else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
  7.1020 +		   end handle TUNIFY => default_tr' sg tm)
  7.1021 +                 else raise Match (* give print translation of specialised record a chance *)
  7.1022 +            | _ => raise Match)
  7.1023 +       else default_tr' sg tm
  7.1024 +  end
  7.1025 +
  7.1026 +fun record_type_tr' sep mark record record_scheme sg t =
  7.1027 +  let
  7.1028 +    fun get_sort xs n = (case assoc (xs,n) of 
  7.1029 +                             Some s => s 
  7.1030 +                           | None => Sign.defaultS sg);
  7.1031 +
  7.1032 +    val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
  7.1033 +
  7.1034 +    val tsig = Sign.tsig_of sg
  7.1035 +    fun unify (t,v) = Type.unify tsig v t;
  7.1036 +
  7.1037 +    fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T);
  7.1038 + 
  7.1039 +    fun field_lst T =
  7.1040 +      (case T of
  7.1041 +        Type (ext,args) 
  7.1042 +         => (case try (unsuffix ext_typeN) ext of
  7.1043 +               Some ext' 
  7.1044 +               => (case get_extfields sg ext' of
  7.1045 +                     Some flds 
  7.1046 +                     => (case get_fieldext sg (fst (hd flds)) of
  7.1047 +                           Some (_,alphas) 
  7.1048 +                           => (let
  7.1049 +                                val (f::fs) = but_last flds;
  7.1050 +                                val flds' = apfst (Sign.extern sg Sign.constK) f
  7.1051 +                                            ::map (apfst NameSpace.base) fs; 
  7.1052 +                                val (args',more) = split_last args; 
  7.1053 +                                val alphavars = map Type.varifyT (but_last alphas); 
  7.1054 +                                val (subst,_)= foldr unify (alphavars~~args',(Vartab.empty,0));
  7.1055 +                                val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT)))
  7.1056 +                                                flds';
  7.1057 +                              in flds''@field_lst more end
  7.1058 +                              handle TUNIFY => [("",T)] 
  7.1059 +                                   | LIST _=> [("",T)])
  7.1060 +                         | None => [("",T)])
  7.1061 +                   | None => [("",T)])
  7.1062 +             | None => [("",T)]) 
  7.1063 +        | _ => [("",T)])
  7.1064 +
  7.1065 +    val (flds,(_,moreT)) = split_last (field_lst T);
  7.1066 +    val flds' = map (fn (n,T)=>Syntax.const mark$Syntax.const n$term_of_type T) flds;
  7.1067 +    val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
  7.1068 +
  7.1069 +  in if not (!print_record_type_as_fields) orelse null flds then raise Match
  7.1070 +     else if moreT = HOLogic.unitT 
  7.1071 +          then Syntax.const record$flds'' 
  7.1072 +          else Syntax.const record_scheme$flds''$term_of_type moreT
  7.1073 +  end
  7.1074 +    
  7.1075 +
  7.1076 +fun gen_record_type_tr' name = 
  7.1077 +  let val name_sfx = suffix ext_typeN name;
  7.1078 +      fun tr' sg ts = record_type_tr' "_field_types" "_field_type" 
  7.1079 +                       "_record_type" "_record_type_scheme" sg 
  7.1080 +                       (list_comb (Syntax.const name_sfx,ts))
  7.1081 +  in (name_sfx,tr')
  7.1082 +  end
  7.1083 +
  7.1084 +     
  7.1085 +fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name =
  7.1086 +  let val name_sfx = suffix ext_typeN name;
  7.1087 +      val default_tr' = record_type_tr' "_field_types" "_field_type" 
  7.1088 +                               "_record_type" "_record_type_scheme" 
  7.1089 +      fun tr' sg ts = record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg
  7.1090 +                         (list_comb (Syntax.const name_sfx,ts))
  7.1091 +  in (name_sfx, tr') end;
  7.1092 +
  7.1093  
  7.1094  (** record simprocs **)
  7.1095 - 
  7.1096  fun quick_and_dirty_prove sg xs asms prop tac =
  7.1097  Tactic.prove sg xs asms prop
  7.1098 -    (if ! quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
  7.1099 +    (if !quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
  7.1100  
  7.1101  
  7.1102  fun prove_split_simp sg T prop =
  7.1103 -    (case last_fieldT T of
  7.1104 -      Some (name,_) => (case get_splits sg name of
  7.1105 -                         Some (all_thm,_,_,_) 
  7.1106 -                          => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
  7.1107 -                             in (quick_and_dirty_prove sg [] [] prop 
  7.1108 -                                  (K (simp_tac (simpset addsimps [all_thm]) 1)))
  7.1109 -                             end
  7.1110 -                      | _ => error "RecordPackage.prove_split_simp: code should never been reached")
  7.1111 -     | _ => error "RecordPackage.prove_split_simp: code should never been reached")
  7.1112 -
  7.1113 +  (case get_splits sg (rec_id T) of
  7.1114 +     Some (all_thm,_,_,_) 
  7.1115 +     => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
  7.1116 +        in (quick_and_dirty_prove sg [] [] prop 
  7.1117 +           (K (simp_tac (simpset addsimps [all_thm]) 1)))
  7.1118 +        end
  7.1119 +   | _ => error "RecordPackage.prove_split_simp:code should never been reached")
  7.1120  
  7.1121  (* record_simproc *)
  7.1122  (* Simplifies selections of an record update:
  7.1123 @@ -682,8 +751,10 @@
  7.1124            (case get_updates sg u of Some u_name =>
  7.1125              let
  7.1126                fun mk_abs_var x t = (x, fastype_of t);
  7.1127 -              val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
  7.1128 -
  7.1129 +              val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg;
  7.1130 +              fun flds T = 
  7.1131 +                   foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN))))
  7.1132 +                         ([],(dest_recTs T));
  7.1133                fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
  7.1134  		  (case (Symtab.lookup (updates,u)) of
  7.1135                       None => None
  7.1136 @@ -695,8 +766,8 @@
  7.1137                                 val kv = mk_abs_var "k" k
  7.1138                                 val kb = Bound 1 
  7.1139                               in Some (upd$kb$rb,kb,[kv,rv],true) end
  7.1140 -                        else if u_name mem (map fst (dest_fieldTs rangeS))
  7.1141 -                             orelse s mem (map fst (dest_fieldTs updT))
  7.1142 +                        else if u_name mem (flds rangeS)
  7.1143 +                             orelse s mem (flds updT)
  7.1144                               then None
  7.1145  			     else (case mk_eq_terms r of 
  7.1146                                       Some (trm,trm',vars,update_s) 
  7.1147 @@ -735,7 +806,7 @@
  7.1148   * the record first and do simplification on that (record_split_simp_tac).
  7.1149   * e.g. r(|lots of updates|) = x
  7.1150   *
  7.1151 - *               record_eq_simproc           record_split_simp_tac
  7.1152 + *               record_eq_simproc       record_split_simp_tac
  7.1153   * Complexity: #components * #updates     #updates   
  7.1154   *           
  7.1155   *)
  7.1156 @@ -743,9 +814,9 @@
  7.1157    Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
  7.1158      (fn sg => fn _ => fn t =>
  7.1159        (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
  7.1160 -        (case last_fieldT T of
  7.1161 -           None => None
  7.1162 -         | Some (name, _) => (case get_equalities sg name of
  7.1163 +        (case rec_id T of
  7.1164 +           "" => None
  7.1165 +         | name => (case get_equalities sg name of
  7.1166                                  None => None
  7.1167                                | Some thm => Some (thm RS Eq_TrueI)))
  7.1168         | _ => None));
  7.1169 @@ -790,7 +861,8 @@
  7.1170  
  7.1171  	 in (case mk_updterm updates Symtab.empty t of
  7.1172  	       Some (trm,trm',vars)
  7.1173 -                => Some (prove_split_simp sg T (list_all(vars,(Logic.mk_equals (trm,trm')))))
  7.1174 +                => Some (prove_split_simp sg T  
  7.1175 +                          (list_all(vars,(Logic.mk_equals (trm,trm')))))
  7.1176               | None => None)
  7.1177  	 end
  7.1178         | _ => None));
  7.1179 @@ -804,9 +876,9 @@
  7.1180      (fn sg => fn _ => fn t =>
  7.1181        (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
  7.1182           if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
  7.1183 -         then (case last_fieldT T of
  7.1184 -                 None => None
  7.1185 -               | Some (name, _)
  7.1186 +         then (case rec_id T of
  7.1187 +                 "" => None
  7.1188 +               | name
  7.1189                    => if P t 
  7.1190                       then (case get_splits sg name of
  7.1191                               None => None
  7.1192 @@ -821,7 +893,7 @@
  7.1193         | _ => None))
  7.1194  
  7.1195  (* record_ex_sel_eq_simproc *)
  7.1196 -(* record: (EX r. x = sel r) resp. (EX r. sel r = x) to True *) 
  7.1197 +(* simplifies: (EX s. x = sel s) resp. (EX s. sel s = x) to True *) 
  7.1198  val record_ex_sel_eq_simproc =
  7.1199    Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
  7.1200      (fn sg => fn _ => fn t =>
  7.1201 @@ -830,24 +902,24 @@
  7.1202                                         addsimprocs [record_split_simproc (K true)]) 1)));
  7.1203         in     
  7.1204           (case t of 
  7.1205 -           (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X)) =>
  7.1206 +           (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X)) =>
  7.1207               (case get_selectors sg sel of Some () =>
  7.1208                  let 
  7.1209                    val X' = ("x",range_type Tsel);
  7.1210  		  val prop = list_all ([X'], 
  7.1211                                 Logic.mk_equals
  7.1212 -		                 (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$
  7.1213 +		                 (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$
  7.1214                                                        (Const (sel,Tsel)$Bound 0)$Bound 1),
  7.1215                                    Const ("True",HOLogic.boolT)));
  7.1216                  in Some (prove prop) end
  7.1217                | None => None)
  7.1218 -          |(Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0))) =>
  7.1219 +          |(Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0))) =>
  7.1220               (case get_selectors sg sel of Some () =>
  7.1221                  let 
  7.1222                    val X' = ("x",range_type Tsel);
  7.1223  		  val prop = list_all ([X'], 
  7.1224                                 Logic.mk_equals
  7.1225 -		                 (Const ("Ex",Tex)$Abs(r,T,Const ("op =",Teq)$
  7.1226 +		                 (Const ("Ex",Tex)$Abs(s,T,Const ("op =",Teq)$
  7.1227                                                       Bound 1$(Const (sel,Tsel)$Bound 0)),
  7.1228                                    Const ("True",HOLogic.boolT)));
  7.1229                  in Some (prove prop) end 
  7.1230 @@ -855,28 +927,8 @@
  7.1231            | _ => None)
  7.1232           end)
  7.1233  
  7.1234 -(** record field splitting **)
  7.1235  
  7.1236 -(* tactic *)
  7.1237 -
  7.1238 -fun is_fieldT fields (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
  7.1239 -  | is_fieldT _ _ = false;
  7.1240 -
  7.1241 -fun record_split_tac i st =
  7.1242 -  let
  7.1243 -    val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st);
  7.1244 -
  7.1245 -    val has_field = exists_Const
  7.1246 -      (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  7.1247 -          (s = "all" orelse s = "All") andalso is_fieldT fields T
  7.1248 -        | _ => false);
  7.1249 -
  7.1250 -    val goal = Library.nth_elem (i - 1, Thm.prems_of st);
  7.1251 -  in
  7.1252 -    if has_field goal then Simplifier.full_simp_tac simpset i st
  7.1253 -    else Seq.empty
  7.1254 -  end handle Library.LIST _ => Seq.empty;
  7.1255 -
  7.1256 +    
  7.1257  
  7.1258  local
  7.1259  val inductive_atomize = thms "induct_atomize";
  7.1260 @@ -891,16 +943,16 @@
  7.1261  fun record_split_simp_tac P i st =
  7.1262    let
  7.1263      val sg = Thm.sign_of_thm st;
  7.1264 -    val {sel_upd={simpset,...},field_splits={fields,...},...} 
  7.1265 +    val {sel_upd={simpset,...},...} 
  7.1266              = RecordsData.get_sg sg;
  7.1267  
  7.1268 -    val has_field = exists_Const
  7.1269 +    val has_rec = exists_Const
  7.1270        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  7.1271 -          (s = "all" orelse s = "All" orelse s = "Ex") andalso is_fieldT fields T
  7.1272 +          (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T 
  7.1273          | _ => false);
  7.1274  
  7.1275      val goal = Library.nth_elem (i - 1, Thm.prems_of st);
  7.1276 -    val frees = filter (is_fieldT fields o type_of) (term_frees goal);
  7.1277 +    val frees = filter (is_recT o type_of) (term_frees goal);
  7.1278  
  7.1279      fun mk_split_free_tac free induct_thm i = 
  7.1280  	let val cfree = cterm_of sg free;
  7.1281 @@ -913,504 +965,55 @@
  7.1282  	end;
  7.1283  
  7.1284      fun split_free_tac P i (free as Free (n,T)) = 
  7.1285 -	(case last_fieldT T of
  7.1286 -           None => None
  7.1287 -         | Some(name,_)=> if P free 
  7.1288 -                          then (case get_splits sg name of
  7.1289 -                                  None => None
  7.1290 -                                | Some (_,_,_,induct_thm)
  7.1291 -                                   => Some (mk_split_free_tac free induct_thm i))
  7.1292 -                          else None)
  7.1293 +	(case rec_id T of
  7.1294 +           "" => None
  7.1295 +         | name => if P free 
  7.1296 +                   then (case get_splits sg name of
  7.1297 +                           None => None
  7.1298 +                         | Some (_,_,_,induct_thm)
  7.1299 +                             => Some (mk_split_free_tac free induct_thm i))
  7.1300 +                   else None)
  7.1301       | split_free_tac _ _ _ = None;
  7.1302  
  7.1303      val split_frees_tacs = mapfilter (split_free_tac P i) frees;
  7.1304     
  7.1305 -    val simprocs = if has_field goal then [record_split_simproc P] else [];
  7.1306 +    val simprocs = if has_rec goal then [record_split_simproc P] else [];
  7.1307     
  7.1308    in st |> (EVERY split_frees_tacs) 
  7.1309             THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i)
  7.1310    end handle Library.LIST _ => Seq.empty;
  7.1311  end;
  7.1312  
  7.1313 +
  7.1314 +(* record_split_tac *)
  7.1315 +(* splits all records in the goal, which are quantified by ! or !!. *)
  7.1316 +fun record_split_tac i st =
  7.1317 +  let
  7.1318 +    val sg = Thm.sign_of_thm st;
  7.1319 +
  7.1320 +    val has_rec = exists_Const
  7.1321 +      (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  7.1322 +          (s = "all" orelse s = "All") andalso is_recT T 
  7.1323 +        | _ => false);
  7.1324 + 
  7.1325 +    val goal = Library.nth_elem (i - 1, Thm.prems_of st);   
  7.1326 +
  7.1327 +    fun is_all t =
  7.1328 +      (case t of (Const (quantifier, _)$_) =>
  7.1329 +         quantifier = "All" orelse quantifier = "all"
  7.1330 +       | _ => false);
  7.1331 + 
  7.1332 +  in if has_rec goal 
  7.1333 +     then Simplifier.full_simp_tac 
  7.1334 +           (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st 
  7.1335 +     else Seq.empty
  7.1336 +  end handle Library.LIST _ => Seq.empty;
  7.1337 +
  7.1338  (* wrapper *)
  7.1339  
  7.1340  val record_split_name = "record_split_tac";
  7.1341  val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
  7.1342  
  7.1343 -
  7.1344 -(* method *)
  7.1345 -
  7.1346 -val record_split_method =
  7.1347 -  ("record_split", Method.no_args (Method.SIMPLE_METHOD' HEADGOAL record_split_tac),
  7.1348 -    "split record fields");
  7.1349 -
  7.1350 -
  7.1351 -
  7.1352 -(** internal theory extenders **)
  7.1353 -
  7.1354 -(* field_typedefs *)
  7.1355 -
  7.1356 -fun field_typedefs zeta moreT names theory =
  7.1357 -  let
  7.1358 -    val alpha = "'a";
  7.1359 -    val aT = TFree (alpha, HOLogic.typeS);
  7.1360 -    val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT));
  7.1361 -
  7.1362 -    fun type_def (thy, name) =
  7.1363 -      let val (thy', {type_definition, set_def = Some def, ...}) =
  7.1364 -        thy |> setmp TypedefPackage.quiet_mode true
  7.1365 -          (TypedefPackage.add_typedef_i true None
  7.1366 -            (suffix field_typeN (Sign.base_name name), [alpha, zeta], Syntax.NoSyn) UNIV None
  7.1367 -          (Tactic.rtac UNIV_witness 1))
  7.1368 -      in (thy', Tactic.rewrite_rule [def] type_definition) end
  7.1369 -  in foldl_map type_def (theory, names) end;
  7.1370 -
  7.1371 -
  7.1372 -(* field_definitions *)
  7.1373 -
  7.1374 -fun field_definitions fields names alphas zeta moreT more vars thy =
  7.1375 -  let
  7.1376 -    val sign = Theory.sign_of thy;
  7.1377 -    val base = Sign.base_name;
  7.1378 -
  7.1379 -    val xT = TFree (variant alphas "'x", HOLogic.typeS);
  7.1380 -
  7.1381 -
  7.1382 -    (* prepare declarations and definitions *)
  7.1383 -
  7.1384 -    (*field constructors*)
  7.1385 -    val field_decls = map (mk_fieldC moreT) fields;
  7.1386 -
  7.1387 -    fun mk_field_spec ((c, T), v) =
  7.1388 -      Term.head_of (mk_field ((c, v), more)) :==
  7.1389 -        lambda v (lambda more (mk_Abs moreT (c, T) $ (HOLogic.mk_prod (v, more))));
  7.1390 -    val field_specs = map mk_field_spec (fields ~~ vars);
  7.1391 -
  7.1392 -    (*field destructors*)
  7.1393 -    val dest_decls = map (mk_fstC moreT) fields @ map (mk_sndC moreT) fields;
  7.1394 -
  7.1395 -    fun mk_dest_spec dest sel (c, T) =
  7.1396 -      let val p = Free ("p", mk_fieldT ((c, T), moreT));
  7.1397 -      in Term.head_of (dest p) :== lambda p (sel (mk_Rep moreT (c, T) $ p)) end;
  7.1398 -    val dest_specs1 = map (mk_dest_spec mk_fst HOLogic.mk_fst) fields;
  7.1399 -    val dest_specs2 = map (mk_dest_spec mk_snd HOLogic.mk_snd) fields;
  7.1400 -
  7.1401 -
  7.1402 -    (* 1st stage: defs_thy *)
  7.1403 -
  7.1404 -    val (defs_thy, (((typedefs, field_defs), dest_defs1), dest_defs2)) =
  7.1405 -      thy
  7.1406 -      |> field_typedefs zeta moreT names
  7.1407 -      |>> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
  7.1408 -      |>>> (PureThy.add_defs_i false o map Thm.no_attributes) field_specs
  7.1409 -      |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs1
  7.1410 -      |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs2;
  7.1411 -
  7.1412 -    val prod_types = map (fn (((a, b), c), d) => product_type_intro OF [a, b, c, d])
  7.1413 -      (typedefs ~~ field_defs ~~ dest_defs1 ~~ dest_defs2);
  7.1414 -
  7.1415 -
  7.1416 -    (* 2nd stage: thms_thy *)
  7.1417 -
  7.1418 -    fun make ren th = map (fn (prod_type, field) => Drule.standard
  7.1419 -      (Drule.rename_bvars (ren ~~ [base (fst field), moreN] handle LIST _ => [])
  7.1420 -        (th OF [prod_type]))) (prod_types ~~ fields);
  7.1421 -
  7.1422 -    val dest_convs = make [] product_type_conv1 @ make [] product_type_conv2;
  7.1423 -    val field_injects = make [] product_type_inject;
  7.1424 -    val field_inducts = make ["x", "y"] product_type_induct;
  7.1425 -    val field_cases = make ["x", "y"] product_type_cases;
  7.1426 -    val field_splits = make ["a", "b"] product_type_split_paired_all @
  7.1427 -      make ["a", "b"] product_type_split_paired_All;
  7.1428 -
  7.1429 -    val (thms_thy, [field_defs', dest_defs', dest_convs', field_injects',
  7.1430 -        field_splits', field_inducts', field_cases']) = defs_thy
  7.1431 -      |> Codegen.assoc_consts_i (flat (map (fn (s, _) =>
  7.1432 -           [(suffix fieldN s, None, prod_code),
  7.1433 -            (suffix fstN s, None, fst_code),
  7.1434 -            (suffix sndN s, None, snd_code)]) fields))
  7.1435 -      |> Codegen.assoc_types (map (fn (s, _) =>
  7.1436 -           (suffix field_typeN s, prodT_code)) fields)
  7.1437 -      |> (PureThy.add_thmss o map Thm.no_attributes)
  7.1438 -       [("field_defs", field_defs),
  7.1439 -        ("dest_defs", dest_defs1 @ dest_defs2),
  7.1440 -        ("dest_convs", dest_convs),
  7.1441 -        ("field_injects", field_injects),
  7.1442 -        ("field_splits", field_splits),
  7.1443 -        ("field_inducts", field_inducts),
  7.1444 -        ("field_cases", field_cases)];
  7.1445 -
  7.1446 -  in (thms_thy, dest_convs', field_injects', field_splits', field_inducts', field_cases') end;
  7.1447 -
  7.1448 -
  7.1449 -(* record_definition *)
  7.1450 -
  7.1451 -fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
  7.1452 -  let
  7.1453 -    val sign = Theory.sign_of thy;
  7.1454 -
  7.1455 -    val alphas = map fst args;
  7.1456 -    val name = Sign.full_name sign bname;
  7.1457 -    val full = Sign.full_name_path sign bname;
  7.1458 -    val base = Sign.base_name;
  7.1459 -
  7.1460 -    val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
  7.1461 -
  7.1462 -
  7.1463 -    (* basic components *)
  7.1464 -
  7.1465 -    val ancestry = map (length o flat o map #fields) (Library.prefixes1 parents);
  7.1466 -
  7.1467 -    val parent_fields = flat (map #fields parents);
  7.1468 -    val parent_names = map fst parent_fields;
  7.1469 -    val parent_types = map snd parent_fields;
  7.1470 -    val parent_len = length parent_fields;
  7.1471 -    val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, rN]);
  7.1472 -    val parent_vars = ListPair.map Free (parent_xs, parent_types);
  7.1473 -    val parent_named_vars = parent_names ~~ parent_vars;
  7.1474 -
  7.1475 -    val fields = map (apfst full) bfields;
  7.1476 -    val names = map fst fields;
  7.1477 -    val types = map snd fields;
  7.1478 -    val len = length fields;
  7.1479 -    val xs = variantlist (map fst bfields, moreN :: rN :: parent_xs);
  7.1480 -    val vars = ListPair.map Free (xs, types);
  7.1481 -    val named_vars = names ~~ vars;
  7.1482 -
  7.1483 -    val all_fields = parent_fields @ fields;
  7.1484 -    val all_names = parent_names @ names;
  7.1485 -    val all_types = parent_types @ types;
  7.1486 -    val all_len = parent_len + len;
  7.1487 -    val all_xs = parent_xs @ xs;
  7.1488 -    val all_vars = parent_vars @ vars;
  7.1489 -    val all_named_vars = parent_named_vars @ named_vars;
  7.1490 -
  7.1491 -    val zeta = variant alphas "'z";
  7.1492 -    val moreT = TFree (zeta, HOLogic.typeS);
  7.1493 -    val more = Free (moreN, moreT);
  7.1494 -    val full_moreN = full moreN;
  7.1495 -    fun more_part t = mk_more t full_moreN;
  7.1496 -    fun more_part_update t x = mk_more_update t (full_moreN, x);
  7.1497 -    val all_types_more = all_types @ [moreT];
  7.1498 -    val all_xs_more = all_xs @ [moreN];
  7.1499 -
  7.1500 -    val parent_more = funpow parent_len mk_snd;
  7.1501 -    val idxs = 0 upto (len - 1);
  7.1502 -
  7.1503 -    val fieldsT = mk_recordT (fields, HOLogic.unitT);
  7.1504 -    fun rec_schemeT n = mk_recordT (prune n all_fields, moreT);
  7.1505 -    fun rec_scheme n = mk_record (prune n all_named_vars, more);
  7.1506 -    fun recT n = mk_recordT (prune n all_fields, HOLogic.unitT);
  7.1507 -    fun rec_ n = mk_record (prune n all_named_vars, HOLogic.unit);
  7.1508 -    fun r_scheme n = Free (rN, rec_schemeT n);
  7.1509 -    fun r n = Free (rN, recT n);
  7.1510 -
  7.1511 -    
  7.1512 -
  7.1513 -    (* prepare print translation functions *)
  7.1514 -    val field_tr's =
  7.1515 -      print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
  7.1516 -
  7.1517 -    val field_type_tr's = 
  7.1518 -	let val fldnames = if parent_len = 0 then (tl names) else names;
  7.1519 -        in print_translation_field_types (distinct (flat (map NameSpace.accesses' fldnames))) 
  7.1520 -        end;
  7.1521 -
  7.1522 -    fun record_type_abbr_tr's thy =
  7.1523 -	let val trnames = NameSpace.accesses' (hd all_names)
  7.1524 -            val sg = Theory.sign_of thy
  7.1525 -	in map (gen_record_type_abbr_tr' 
  7.1526 -                 sg bname alphas zeta (hd (rev names)) (rec_schemeT 0)) trnames end;   
  7.1527 -
  7.1528 -    (* prepare declarations *)
  7.1529 -
  7.1530 -    val sel_decls = map (mk_selC (rec_schemeT 0)) bfields @
  7.1531 -      [mk_moreC (rec_schemeT 0) (moreN, moreT)];
  7.1532 -    val update_decls = map (mk_updateC (rec_schemeT 0)) bfields @
  7.1533 -      [mk_more_updateC (rec_schemeT 0) (moreN, moreT)];
  7.1534 -    val make_decl = (makeN, all_types ---> recT 0);
  7.1535 -    val fields_decl = (fieldsN, types ---> fieldsT);
  7.1536 -    val extend_decl = (extendN, recT 0 --> moreT --> rec_schemeT 0);
  7.1537 -    val truncate_decl = (truncateN, rec_schemeT 0 --> recT 0);
  7.1538 -
  7.1539 -
  7.1540 -    (* prepare definitions *)
  7.1541 -
  7.1542 -    (*record (scheme) type abbreviation*)
  7.1543 -    val recordT_specs =
  7.1544 -      [(suffix schemeN bname, alphas @ [zeta], rec_schemeT 0, Syntax.NoSyn),
  7.1545 -        (bname, alphas, recT 0, Syntax.NoSyn)];
  7.1546 -
  7.1547 -    (*selectors*)
  7.1548 -    fun mk_sel_spec (i, c) =
  7.1549 -      mk_sel (r_scheme 0) c :== mk_fst (funpow i mk_snd (parent_more (r_scheme 0)));
  7.1550 -    val sel_specs =
  7.1551 -      ListPair.map mk_sel_spec (idxs, names) @
  7.1552 -        [more_part (r_scheme 0) :== funpow len mk_snd (parent_more (r_scheme 0))];
  7.1553 -
  7.1554 -    (*updates*)
  7.1555 -    val all_sels = mk_named_sels all_names (r_scheme 0);
  7.1556 -    fun mk_upd_spec (i, (c, x)) =
  7.1557 -      mk_update (r_scheme 0) (c, x) :==
  7.1558 -        mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part (r_scheme 0))
  7.1559 -    val update_specs =
  7.1560 -      ListPair.map mk_upd_spec (idxs, named_vars) @
  7.1561 -        [more_part_update (r_scheme 0) more :== mk_record (all_sels, more)];
  7.1562 -
  7.1563 -    (*derived operations*)
  7.1564 -    val make_spec = Const (full makeN, all_types ---> recT 0) $$ all_vars :==
  7.1565 -      mk_record (all_named_vars, HOLogic.unit);
  7.1566 -    val fields_spec = Const (full fieldsN, types ---> fieldsT) $$ vars :==
  7.1567 -      mk_record (named_vars, HOLogic.unit);
  7.1568 -    val extend_spec = Const (full extendN, recT 0 --> moreT --> rec_schemeT 0) $ r 0 $ more :==
  7.1569 -      mk_record (mk_named_sels all_names (r 0), more);
  7.1570 -    val truncate_spec = Const (full truncateN, rec_schemeT 0 --> recT 0) $ r_scheme 0 :==
  7.1571 -      mk_record (all_sels, HOLogic.unit);
  7.1572 -
  7.1573 -
  7.1574 -    (* prepare propositions *)
  7.1575 -
  7.1576 -    (*selectors*)
  7.1577 -    val sel_props =
  7.1578 -      map (fn (c, x) => mk_sel (rec_scheme 0) c === x) named_vars @
  7.1579 -        [more_part (rec_scheme 0) === more];
  7.1580 -
  7.1581 -    (*updates*)
  7.1582 -    fun mk_upd_prop (i, (c, T)) =
  7.1583 -      let val x' = Free (variant all_xs (base c ^ "'"), T) in
  7.1584 -        mk_update (rec_scheme 0) (c, x') ===
  7.1585 -          mk_record (nth_update (c, x') (parent_len + i, all_named_vars), more)
  7.1586 -      end;
  7.1587 -    val update_props =
  7.1588 -      ListPair.map mk_upd_prop (idxs, fields) @
  7.1589 -        let val more' = Free (variant all_xs (moreN ^ "'"), moreT)
  7.1590 -        in [more_part_update (rec_scheme 0) more' === mk_record (all_named_vars, more')] end;
  7.1591 -
  7.1592 -    (*equality*)
  7.1593 -    fun mk_sel_eq (t, T) =
  7.1594 -      let val t' = Term.abstract_over (r_scheme 0, t)
  7.1595 -      in Trueprop (HOLogic.eq_const T $ Term.incr_boundvars 1 t' $ t') end;
  7.1596 -    val sel_eqs = map2 mk_sel_eq
  7.1597 -      (map (mk_sel (r_scheme 0)) all_names @ [more_part (r_scheme 0)], all_types @ [moreT]);
  7.1598 -    val equality_prop =
  7.1599 -      Term.all (rec_schemeT 0) $ (Abs ("r", rec_schemeT 0,
  7.1600 -        Term.all (rec_schemeT 0) $ (Abs ("r'", rec_schemeT 0,
  7.1601 -          Logic.list_implies (sel_eqs,
  7.1602 -            Trueprop (HOLogic.eq_const (rec_schemeT 0) $ Bound 1 $ Bound 0))))));
  7.1603 -
  7.1604 -    (*induct*)
  7.1605 -    fun induct_scheme_prop n =
  7.1606 -      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) in
  7.1607 -        (All (prune n all_xs_more ~~ prune n all_types_more)
  7.1608 -          (Trueprop (P $ rec_scheme n)), Trueprop (P $ r_scheme n))
  7.1609 -      end;
  7.1610 -    fun induct_prop n =
  7.1611 -      let val P = Free ("P", recT n --> HOLogic.boolT) in
  7.1612 -        (All (prune n all_xs ~~ prune n all_types) (Trueprop (P $ rec_ n)), Trueprop (P $ r n))
  7.1613 -      end;
  7.1614 -
  7.1615 -    (*cases*)
  7.1616 -    val C = Trueprop (Free (variant all_xs_more "C", HOLogic.boolT));
  7.1617 -    fun cases_scheme_prop n =
  7.1618 -      All (prune n all_xs_more ~~ prune n all_types_more)
  7.1619 -        ((r_scheme n === rec_scheme n) ==> C) ==> C;
  7.1620 -    fun cases_prop n = All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C;
  7.1621 -
  7.1622 -    (*split*)
  7.1623 -    fun split_scheme_meta_prop n =
  7.1624 -      let val P = Free ("P", rec_schemeT n --> Term.propT) in
  7.1625 -       equals (Term.propT) $
  7.1626 -        (Term.list_all_free ([(rN,rec_schemeT n)],(P $ r_scheme n)))$
  7.1627 -        (All (prune n all_xs_more ~~ prune n all_types_more) (P $ rec_scheme n))
  7.1628 -      end;
  7.1629 -
  7.1630 -    fun split_scheme_object_prop n =
  7.1631 -      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
  7.1632 -          val ALL = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) 
  7.1633 -      in
  7.1634 -	Trueprop (
  7.1635 -           HOLogic.eq_const (HOLogic.boolT) $
  7.1636 -            (HOLogic.mk_all ((rN,rec_schemeT n,P $ r_scheme n)))$
  7.1637 -            (ALL (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
  7.1638 -      end;
  7.1639 -
  7.1640 -      fun split_scheme_object_ex_prop n =
  7.1641 -      let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
  7.1642 -          val EX = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) 
  7.1643 -      in
  7.1644 -	Trueprop (
  7.1645 -           HOLogic.eq_const (HOLogic.boolT) $
  7.1646 -            (HOLogic.mk_exists ((rN,rec_schemeT n,P $ r_scheme n)))$
  7.1647 -            (EX (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
  7.1648 -      end;
  7.1649 -    (* 1st stage: fields_thy *)
  7.1650 -
  7.1651 -    val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) =
  7.1652 -      thy
  7.1653 -      |> Theory.add_path bname
  7.1654 -      |> field_definitions fields names alphas zeta moreT more vars;
  7.1655 -
  7.1656 -    val all_field_inducts = flat (map #field_inducts parents) @ field_inducts;
  7.1657 -    val all_field_cases = flat (map #field_cases parents) @ field_cases;
  7.1658 -    val all_field_splits = flat (map #field_splits parents) @ field_splits
  7.1659 -
  7.1660 -    
  7.1661 -    (* 2nd stage: defs_thy *)
  7.1662 -
  7.1663 -        
  7.1664 -   
  7.1665 -
  7.1666 -    val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
  7.1667 -      fields_thy
  7.1668 -      |> Theory.add_trfuns 
  7.1669 -           ([],[],record_type_abbr_tr's fields_thy @ field_type_tr's @ field_tr's, [])
  7.1670 -      |> add_field_splits (map (suffix field_typeN) names) field_splits
  7.1671 -      |> Theory.parent_path
  7.1672 -      |> Theory.add_tyabbrs_i recordT_specs
  7.1673 -      |> Theory.add_path bname
  7.1674 -      |> Theory.add_consts_i
  7.1675 -        (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
  7.1676 -      |> (Theory.add_consts_i o map Syntax.no_syn)
  7.1677 -        (update_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
  7.1678 -      |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
  7.1679 -      |>>> (PureThy.add_defs_i false o map Thm.no_attributes) update_specs
  7.1680 -      |>>> (PureThy.add_defs_i false o map Thm.no_attributes)
  7.1681 -        [make_spec, fields_spec, extend_spec, truncate_spec]
  7.1682 -      |>> Theory.hide_consts false [full makeN, full fieldsN, full extendN, full truncateN,
  7.1683 -        full moreN, full (suffix updateN moreN)];
  7.1684 -
  7.1685 -
  7.1686 -    (* 3rd stage: thms_thy *)
  7.1687 -
  7.1688 -    val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
  7.1689 -    fun prove_simp simps =
  7.1690 -      let val tac = simp_all_tac HOL_basic_ss simps
  7.1691 -      in fn prop => prove_standard [] [] prop (K tac) end;
  7.1692 -
  7.1693 -    val parent_simps = flat (map #simps parents);
  7.1694 -    val sel_convs = map (prove_simp (parent_simps @ sel_defs @ field_simps)) sel_props;
  7.1695 -    val update_convs = map (prove_simp (parent_simps @ update_defs @ sel_convs)) update_props;
  7.1696 -
  7.1697 -    fun induct_scheme n =
  7.1698 -      let val (assm, concl) = induct_scheme_prop n in
  7.1699 -        prove_standard [] [assm] concl (fn prems =>
  7.1700 -          EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_inducts))
  7.1701 -          THEN resolve_tac prems 1)
  7.1702 -      end;
  7.1703 -
  7.1704 -    fun cases_scheme n =
  7.1705 -      prove_standard [] [] (cases_scheme_prop n) (fn _ =>
  7.1706 -        EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_cases))
  7.1707 -        THEN simp_all_tac HOL_basic_ss []);
  7.1708 -
  7.1709 -    fun split_scheme_meta n =
  7.1710 -      prove_standard [] [] (split_scheme_meta_prop n) (fn _ =>
  7.1711 -        Simplifier.full_simp_tac (HOL_basic_ss addsimps all_field_splits) 1);
  7.1712 -
  7.1713 -    fun split_scheme_object induct_scheme n =
  7.1714 -      prove_standard [] [] (split_scheme_object_prop n) (fn _ =>
  7.1715 -         EVERY [rtac iffI 1, 
  7.1716 -                REPEAT (rtac allI 1), etac allE 1, atac 1,
  7.1717 -                rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
  7.1718 -
  7.1719 -    fun split_scheme_object_ex split_scheme_meta n =
  7.1720 -      prove_standard [] [] (split_scheme_object_ex_prop n) (fn _ =>
  7.1721 -        fast_simp_tac (claset_of HOL.thy,
  7.1722 -                       HOL_basic_ss addsimps [split_scheme_meta]) 1);
  7.1723 -       
  7.1724 -    val induct_scheme0 = induct_scheme 0;
  7.1725 -    val cases_scheme0 = cases_scheme 0;
  7.1726 -    val split_scheme_meta0 = split_scheme_meta 0;
  7.1727 -    val split_scheme_object0 = split_scheme_object induct_scheme0 0;
  7.1728 -    val split_scheme_object_ex0 = split_scheme_object_ex split_scheme_meta0 0;
  7.1729 -    val more_induct_scheme = map induct_scheme ancestry;
  7.1730 -    val more_cases_scheme = map cases_scheme ancestry;
  7.1731 -
  7.1732 -    val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _, 
  7.1733 -                      [split_scheme_meta',split_scheme_object',
  7.1734 -                       split_scheme_object_ex',split_scheme_free']],
  7.1735 -        [induct_scheme', cases_scheme']), [more_induct_scheme', more_cases_scheme'])) =
  7.1736 -      defs_thy
  7.1737 -      |> (PureThy.add_thmss o map Thm.no_attributes)
  7.1738 -       [("select_convs", sel_convs),
  7.1739 -        ("update_convs", update_convs),
  7.1740 -        ("select_defs", sel_defs),
  7.1741 -        ("update_defs", update_defs),
  7.1742 -        ("defs", derived_defs),
  7.1743 -        ("splits",[split_scheme_meta0,split_scheme_object0,
  7.1744 -                   split_scheme_object_ex0,induct_scheme0])]
  7.1745 -      |>>> PureThy.add_thms
  7.1746 -       [(("induct_scheme", induct_scheme0), induct_type_global (suffix schemeN name)),
  7.1747 -        (("cases_scheme", cases_scheme0), cases_type_global (suffix schemeN name))]
  7.1748 -      |>>> PureThy.add_thmss
  7.1749 -        [(("more_induct_scheme", more_induct_scheme), induct_type_global ""),
  7.1750 -         (("more_cases_scheme", more_cases_scheme), cases_type_global "")];
  7.1751 -
  7.1752 -
  7.1753 -    (* 4th stage: more_thms_thy *)
  7.1754 -
  7.1755 -    val prove_standard = Tactic.prove_standard (Theory.sign_of thms_thy);
  7.1756 -
  7.1757 -    fun induct (n, scheme) =
  7.1758 -      let val (assm, concl) = induct_prop n in
  7.1759 -        prove_standard [] [assm] concl (fn prems =>
  7.1760 -          res_inst_tac [(rN, rN)] scheme 1
  7.1761 -          THEN try_param_tac "more" unit_induct 1
  7.1762 -          THEN resolve_tac prems 1)
  7.1763 -      end;
  7.1764 -
  7.1765 -    fun cases (n, scheme) =
  7.1766 -      prove_standard [] [] (cases_prop n) (fn _ =>
  7.1767 -        res_inst_tac [(rN, rN)] scheme 1
  7.1768 -        THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
  7.1769 -
  7.1770 -    val induct0 = induct (0, induct_scheme');
  7.1771 -    val cases0 = cases (0, cases_scheme');
  7.1772 -    val more_induct = map induct (ancestry ~~ more_induct_scheme');
  7.1773 -    val more_cases = map cases (ancestry ~~ more_cases_scheme');
  7.1774 -
  7.1775 -    val equality = prove_standard [] [] equality_prop (fn _ =>
  7.1776 -      fn st => let val [r, r'] = map #1 (rev (Tactic.innermost_params 1 st)) in
  7.1777 -        st |> (res_inst_tac [(rN, r)] cases_scheme' 1
  7.1778 -        THEN res_inst_tac [(rN, r')] cases_scheme' 1
  7.1779 -        THEN simp_all_tac HOL_basic_ss (parent_simps @ sel_convs))
  7.1780 -      end);
  7.1781 -
  7.1782 -    val (more_thms_thy, [_, _, equality']) =
  7.1783 -      thms_thy |> PureThy.add_thms
  7.1784 -       [(("induct", induct0), induct_type_global name),
  7.1785 -        (("cases", cases0), cases_type_global name),
  7.1786 -        (("equality", equality), [ContextRules.intro_bang_global None])]
  7.1787 -      |>> (#1 oo PureThy.add_thmss)
  7.1788 -        [(("more_induct", more_induct), induct_type_global ""),
  7.1789 -         (("more_cases", more_cases), cases_type_global "")];
  7.1790 -
  7.1791 -    val simps = sel_convs' @ update_convs';
  7.1792 -    val iffs = field_injects;
  7.1793 -
  7.1794 -    val more_thms_thy' =
  7.1795 -      more_thms_thy |> (#1 oo PureThy.add_thmss)
  7.1796 -        [(("simps", simps), [Simplifier.simp_add_global]),
  7.1797 -         (("iffs", iffs), [iff_add_global])];
  7.1798 -
  7.1799 -
  7.1800 -    (* 5th stage: final_thy *)
  7.1801 -
  7.1802 -    val final_thy =
  7.1803 -      more_thms_thy'
  7.1804 -      |> put_record name (make_record_info args parent fields field_inducts field_cases
  7.1805 -          field_splits (field_simps @ simps))
  7.1806 -      |> put_sel_upd (names @ [full_moreN]) simps
  7.1807 -      |> add_record_equalities (snd (split_last names)) equality'
  7.1808 -      |> add_record_splits (snd (split_last names)) 
  7.1809 -                           (split_scheme_meta',split_scheme_object',
  7.1810 -                            split_scheme_object_ex',split_scheme_free')
  7.1811 -      |> Theory.parent_path;
  7.1812 -
  7.1813 -  in (final_thy, {simps = simps, iffs = iffs}) end;
  7.1814 -
  7.1815 -
  7.1816 -
  7.1817  (** theory extender interface **)
  7.1818  
  7.1819  (* prepare arguments *)
  7.1820 @@ -1432,15 +1035,581 @@
  7.1821    let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg
  7.1822    in (Term.add_typ_tfrees (T, env), T) end;
  7.1823  
  7.1824 +(* attributes *)
  7.1825 +
  7.1826 +fun case_names_fields x = RuleCases.case_names ["fields"] x;
  7.1827 +fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
  7.1828 +fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
  7.1829 +
  7.1830 +(* tactics *)
  7.1831 +
  7.1832 +fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
  7.1833 +
  7.1834 +(* do case analysis / induction according to rule on last parameter of ith subgoal 
  7.1835 + * (or on s if there are no parameters); 
  7.1836 + * Instatiation of record variable (and predicate) in rule is calculated to
  7.1837 + * avoid problems with higher order unification. 
  7.1838 + *)
  7.1839 +
  7.1840 +fun try_param_tac s rule i st =
  7.1841 +  let
  7.1842 +    val cert = cterm_of (Thm.sign_of_thm st);
  7.1843 +    val g = nth_elem (i - 1, prems_of st);
  7.1844 +    val params = Logic.strip_params g;
  7.1845 +    val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
  7.1846 +    val rule' = Thm.lift_rule (st, i) rule;
  7.1847 +    val (P, ys) = strip_comb (HOLogic.dest_Trueprop
  7.1848 +      (Logic.strip_assums_concl (prop_of rule')));
  7.1849 +    (* ca indicates if rule is a case analysis or induction rule *)
  7.1850 +    val (x, ca) = (case rev (drop (length params, ys)) of
  7.1851 +        [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
  7.1852 +          (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
  7.1853 +      | [x] => (head_of x, false));
  7.1854 +    val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
  7.1855 +        [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of
  7.1856 +          None => sys_error "try_param_tac: no such variable"
  7.1857 +        | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl),
  7.1858 +            (x, Free (s, T))])
  7.1859 +      | (_, T) :: _ => [(P, list_abs (params, if ca then concl
  7.1860 +          else incr_boundvars 1 (Abs (s, T, concl)))),
  7.1861 +        (x, list_abs (params, Bound 0))])) rule'
  7.1862 +  in compose_tac (false, rule'', nprems_of rule) i st end;
  7.1863 +
  7.1864 +fun extension_typedef name repT alphas thy =
  7.1865 +  let
  7.1866 +    val UNIV = HOLogic.mk_UNIV repT;
  7.1867 +
  7.1868 +    val (thy',{set_def=Some def, Abs_induct = abs_induct, 
  7.1869 +               Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}) =
  7.1870 +        thy |> setmp TypedefPackage.quiet_mode true
  7.1871 +           (TypedefPackage.add_typedef_i true None
  7.1872 +             (suffix ext_typeN (Sign.base_name name), alphas, Syntax.NoSyn) UNIV None
  7.1873 +             (Tactic.rtac UNIV_witness 1))
  7.1874 +    val rewrite_rule = Tactic.rewrite_rule [def, rec_UNIV_I, rec_True_simp];
  7.1875 +  in (thy',map rewrite_rule [abs_inject, abs_inverse, abs_induct])
  7.1876 +  end;
  7.1877 +
  7.1878 +fun extension_definition full name fields names alphas zeta moreT more vars thy = 
  7.1879 +  let  
  7.1880 +    val base = Sign.base_name;
  7.1881 +
  7.1882 +    val fieldTs = (map snd fields);
  7.1883 +    val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) (alphas@[zeta]);
  7.1884 +    val extT_name = suffix ext_typeN name
  7.1885 +    val extT = Type (extT_name, alphas_zetaTs);
  7.1886 +    val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]);
  7.1887 +    val fields_more = fields@[(full moreN,moreT)];
  7.1888 +    val bfields_more = map (apfst base) fields_more;
  7.1889 +    val r = Free (rN,extT)
  7.1890 +    val len = length fields;
  7.1891 +    val idxms = 0 upto len;
  7.1892 +
  7.1893 +    (* prepare declarations and definitions *)
  7.1894 +    
  7.1895 +    (*fields constructor*)
  7.1896 +    val ext_decl = (mk_extC (name,extT) (fieldTs@[moreT]));     
  7.1897 +    val ext_spec = Const ext_decl :== 
  7.1898 +         (foldr (uncurry lambda) 
  7.1899 +            (vars@[more],(mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))))) 
  7.1900 +    
  7.1901 +    (*destructors*) 
  7.1902 +    val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more;
  7.1903 +
  7.1904 +    fun mk_dest_spec (i, (c,T)) =
  7.1905 +      let val snds = (funpow i HOLogic.mk_snd (mk_Rep name repT extT $ r))
  7.1906 +      in Const (mk_selC extT (suffix ext_dest c,T))
  7.1907 +         :== (lambda r (if i=len then snds else HOLogic.mk_fst snds))
  7.1908 +      end;
  7.1909 +    val dest_specs =
  7.1910 +      ListPair.map mk_dest_spec (idxms, fields_more);
  7.1911 +
  7.1912 +    (* code generator data *)
  7.1913 +        (* Representation as nested pairs is revealed for codegeneration *)
  7.1914 +    val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["I","I"];
  7.1915 +    val ext_type_code = Codegen.parse_mixfix (K dummyT) "_";
  7.1916 +    
  7.1917 +    (* 1st stage: defs_thy *)
  7.1918 +    val (defs_thy, ([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs)) =
  7.1919 +        thy 
  7.1920 +        |> extension_typedef name repT (alphas@[zeta])
  7.1921 +        |>> Codegen.assoc_consts_i 
  7.1922 +               [(mk_AbsN name,None,abs_code),
  7.1923 +                (mk_RepN name,None,rep_code)]
  7.1924 +        |>> Codegen.assoc_types [(extT_name,ext_type_code)]
  7.1925 +        |>> Theory.add_consts_i (map Syntax.no_syn ((apfst base ext_decl)::dest_decls))
  7.1926 +        |>>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
  7.1927 +
  7.1928 +    
  7.1929 +    (* prepare propositions *)
  7.1930 +
  7.1931 +    val vars_more = vars@[more];
  7.1932 +    val named_vars_more = (names@[full moreN])~~vars_more;
  7.1933 +    val ext = list_comb (Const ext_decl,vars_more);
  7.1934 +    val s     = Free (rN, extT);
  7.1935 +    val P = Free (variant (map (fn (Free (x,_))=>x) vars_more) "P", extT-->HOLogic.boolT);
  7.1936 +    val C = Free (variant (map (fn (Free (x,_))=>x) vars_more) "C", HOLogic.boolT);
  7.1937 +
  7.1938 +    val inject_prop =
  7.1939 +      let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
  7.1940 +      in All (map dest_Free (vars_more@vars_more')) 
  7.1941 +          ((HOLogic.eq_const extT $ 
  7.1942 +            list_comb (Const ext_decl,vars_more)$list_comb (Const ext_decl,vars_more')) 
  7.1943 +           ===
  7.1944 +           foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more')))
  7.1945 +      end;
  7.1946 +
  7.1947 +    val induct_prop =
  7.1948 +      All (map dest_Free vars_more) (Trueprop (P $ ext)) ==> Trueprop (P $ s);
  7.1949 +     
  7.1950 +    val cases_prop =
  7.1951 +      (All (map dest_Free vars_more) 
  7.1952 +        (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) 
  7.1953 +      ==> Trueprop C;
  7.1954 +
  7.1955 +    (*destructors*) 
  7.1956 +    val dest_conv_props =
  7.1957 +       map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
  7.1958 +
  7.1959 +    val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
  7.1960 +    fun prove_simp simps =
  7.1961 +      let val tac = simp_all_tac HOL_ss simps
  7.1962 +      in fn prop => prove_standard [] [] prop (K tac) end;
  7.1963 +    
  7.1964 +    (* prove propositions *)
  7.1965 +
  7.1966 +    val inject = (prove_simp [ext_def,abs_inject,Pair_eq] inject_prop);
  7.1967 +
  7.1968 +    val induct =
  7.1969 +        prove_standard [] [] induct_prop (fn prems =>
  7.1970 +         EVERY [try_param_tac rN abs_induct 1, 
  7.1971 +                asm_full_simp_tac (HOL_ss addsimps [ext_def,split_paired_all]) 1]);
  7.1972 +
  7.1973 +    val cases =
  7.1974 +        prove_standard [] [] cases_prop (fn prems =>
  7.1975 +         EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
  7.1976 +                try_param_tac rN induct 1,
  7.1977 +                rtac impI 1,
  7.1978 +                REPEAT (etac allE 1),
  7.1979 +                etac mp 1,
  7.1980 +                rtac refl 1])
  7.1981 +	
  7.1982 +    val dest_convs = map (prove_simp 
  7.1983 +                           ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
  7.1984 +    
  7.1985 +    val (thm_thy,([inject',induct',cases'],[dest_convs'])) =
  7.1986 +      defs_thy 
  7.1987 +      |> (PureThy.add_thms o map Thm.no_attributes) 
  7.1988 +           [("ext_inject", inject),
  7.1989 +            ("ext_induct", induct),
  7.1990 +            ("ext_cases", cases)]
  7.1991 +      |>>> (PureThy.add_thmss o map Thm.no_attributes)
  7.1992 +              [("dest_convs",dest_convs)] 
  7.1993 +
  7.1994 +  in (thm_thy,extT,induct',inject',dest_convs')
  7.1995 +  end;
  7.1996 +   
  7.1997 +fun chunks []      []   = []
  7.1998 +  | chunks []      xs   = [xs]
  7.1999 +  | chunks (l::ls) xs  = take (l,xs)::chunks ls (drop (l,xs));
  7.2000 + 
  7.2001 +fun chop_last [] = error "last: list should not be empty"
  7.2002 +  | chop_last [x] = ([],x)
  7.2003 +  | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end;
  7.2004 +     	
  7.2005 +fun subst_last s []      = error "subst_last: list should not be empty"
  7.2006 +  | subst_last s ([x])   = [s]
  7.2007 +  | subst_last s (x::xs) = (x::subst_last s xs);
  7.2008 +
  7.2009 +(* mk_recordT builds up the record type from the current extension tpye extT and a list
  7.2010 + * of parent extensions, starting with the root of the record hierarchy 
  7.2011 +*) 
  7.2012 +fun mk_recordT extT parent_exts = 
  7.2013 +    foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) (parent_exts,extT);
  7.2014 +
  7.2015 +(* record_definition *)
  7.2016 +
  7.2017 +fun record_definition (args, bname) parent parents raw_fields thy = 
  7.2018 +  let
  7.2019 +    val sign = Theory.sign_of thy;
  7.2020 +
  7.2021 +    val alphas = map fst args;
  7.2022 +    val name = Sign.full_name sign bname;
  7.2023 +    val full = Sign.full_name_path sign bname;
  7.2024 +    val base = Sign.base_name;
  7.2025 +
  7.2026 +    val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
  7.2027 +
  7.2028 +    val parent_fields = flat (map #fields parents);
  7.2029 +    val parent_chunks = map (length o #fields) parents;
  7.2030 +    val parent_names = map fst parent_fields;
  7.2031 +    val parent_types = map snd parent_fields;
  7.2032 +    val parent_fields_len = length parent_fields;
  7.2033 +    val parent_variants = variantlist (map base parent_names, [moreN, rN, rN ^ "'"]);
  7.2034 +    val parent_vars = ListPair.map Free (parent_variants, parent_types);
  7.2035 +    val parent_len = length parents;
  7.2036 +    val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
  7.2037 +
  7.2038 +    val fields = map (apfst full) bfields;
  7.2039 +    val names = map fst fields;
  7.2040 +    val extN = full bname;
  7.2041 +    val types = map snd fields;
  7.2042 +    val alphas_fields = foldr add_typ_tfree_names (types,[]);
  7.2043 +    val alphas_ext = alphas inter alphas_fields; 
  7.2044 +    val len = length fields;
  7.2045 +    val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::parent_variants);
  7.2046 +    val vars = ListPair.map Free (variants, types);
  7.2047 +    val named_vars = names ~~ vars;
  7.2048 +    val idxs = 0 upto (len - 1);
  7.2049 +    val idxms = 0 upto len;
  7.2050 +
  7.2051 +    val all_fields = parent_fields @ fields;
  7.2052 +    val all_names = parent_names @ names;
  7.2053 +    val all_types = parent_types @ types;
  7.2054 +    val all_len = parent_fields_len + len;
  7.2055 +    val all_variants = parent_variants @ variants;
  7.2056 +    val all_vars = parent_vars @ vars;
  7.2057 +    val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
  7.2058 +
  7.2059 +
  7.2060 +    val zeta = variant alphas "'z";
  7.2061 +    val moreT = TFree (zeta, HOLogic.typeS);
  7.2062 +    val more = Free (moreN, moreT);
  7.2063 +    val full_moreN = full moreN;
  7.2064 +    val bfields_more = bfields @ [(moreN,moreT)];
  7.2065 +    val fields_more = fields @ [(full_moreN,moreT)];
  7.2066 +    val vars_more = vars @ [more];
  7.2067 +    val named_vars_more = named_vars @[(full_moreN,more)];
  7.2068 +    val all_vars_more = all_vars @ [more];
  7.2069 +    val all_named_vars_more = all_named_vars @ [(full_moreN,more)];
  7.2070 +   
  7.2071 +    (* 1st stage: extension_thy *)
  7.2072 +	
  7.2073 +    val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs) =
  7.2074 +      thy
  7.2075 +      |> Theory.add_path bname
  7.2076 +      |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
  7.2077 +
  7.2078 +   
  7.2079 +    val Type extension_scheme = extT;
  7.2080 +    val extension_name = unsuffix ext_typeN (fst extension_scheme);
  7.2081 +    val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end; 
  7.2082 +    val extension_names = 
  7.2083 +         (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN];
  7.2084 +    val extension_id = foldl (op ^) ("",extension_names);
  7.2085 +
  7.2086 + 
  7.2087 +    fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents));
  7.2088 +    val rec_schemeT0 = rec_schemeT 0;
  7.2089 +
  7.2090 +    fun recT n = 
  7.2091 +      let val (c,Ts) = extension
  7.2092 +      in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents))
  7.2093 +      end;
  7.2094 +    val recT0 = recT 0;
  7.2095 +    
  7.2096 +    fun mk_rec args n =
  7.2097 +      let val (args',more) = chop_last args;
  7.2098 +	  fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
  7.2099 +          fun build Ts = 
  7.2100 +           foldr mk_ext' (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')),more) 
  7.2101 +      in 
  7.2102 +        if more = HOLogic.unit 
  7.2103 +        then build (map recT (0 upto parent_len)) 
  7.2104 +        else build (map rec_schemeT (0 upto parent_len))
  7.2105 +      end;
  7.2106 +   
  7.2107 +    val r_rec0 = mk_rec all_vars_more 0;
  7.2108 +    val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
  7.2109 +
  7.2110 +    fun r n = Free (rN, rec_schemeT n)
  7.2111 +    val r0 = r 0;
  7.2112 +    fun r_unit n = Free (rN, recT n)
  7.2113 +    val r_unit0 = r_unit 0;
  7.2114 +
  7.2115 +    (* prepare print translation functions *)
  7.2116 +    val field_tr's =
  7.2117 +      print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
  7.2118 +
  7.2119 +    val adv_ext_tr's =
  7.2120 +    let
  7.2121 +      val trnames = NameSpace.accesses' extN;
  7.2122 +    in map (gen_record_tr') trnames end;
  7.2123 +
  7.2124 +    val adv_record_type_abbr_tr's =
  7.2125 +      let val trnames = NameSpace.accesses' (hd extension_names);
  7.2126 +          val lastExt = (unsuffix ext_typeN (fst extension));
  7.2127 +      in map (gen_record_type_abbr_tr' bname alphas zeta lastExt rec_schemeT0) trnames
  7.2128 +      end;
  7.2129 +
  7.2130 +    val adv_record_type_tr's =
  7.2131 +      let val trnames = if parent_len > 0 then NameSpace.accesses' extN else [];
  7.2132 +                        (* avoid conflict with adv_record_type_abbr_tr's *)
  7.2133 +      in map (gen_record_type_tr') trnames
  7.2134 +      end;
  7.2135 +
  7.2136 +    
  7.2137 +    (* prepare declarations *)
  7.2138 +
  7.2139 +    val sel_decls = map (mk_selC rec_schemeT0) bfields_more;
  7.2140 +    val upd_decls = map (mk_updC rec_schemeT0) bfields_more;
  7.2141 +    val make_decl = (makeN, all_types ---> recT0);
  7.2142 +    val fields_decl = (fields_selN, types ---> Type extension); 
  7.2143 +    val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
  7.2144 +    val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
  7.2145 +
  7.2146 +    (* prepare definitions *)
  7.2147 +    
  7.2148 +    fun parent_more s = 
  7.2149 +         if null parents then s 
  7.2150 +         else mk_sel s (NameSpace.append (#name (hd (rev parents))) moreN, extT);
  7.2151 +
  7.2152 +    fun parent_more_upd v s =
  7.2153 +      if null parents then v 
  7.2154 +      else let val mp = (NameSpace.append (#name (hd (rev parents))) moreN);
  7.2155 +           in mk_upd mp v s end;
  7.2156 +   
  7.2157 +    (*record (scheme) type abbreviation*)
  7.2158 +    val recordT_specs =
  7.2159 +      [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
  7.2160 +        (bname, alphas, recT0, Syntax.NoSyn)];	
  7.2161 +
  7.2162 +    (*selectors*) 
  7.2163 +    fun mk_sel_spec (c,T) = 
  7.2164 +	 Const (mk_selC rec_schemeT0 (c,T)) 
  7.2165 +          :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0));
  7.2166 +    val sel_specs = map mk_sel_spec fields_more;
  7.2167 +
  7.2168 +    (*updates*)
  7.2169 +    fun mk_upd_spec (c,T) =
  7.2170 +      let 
  7.2171 +        val args = map (fn (n,nT) => if n=c then Free (base c,T) else (mk_sel r0 (n,nT))) 
  7.2172 +                       fields_more;
  7.2173 +        val new = mk_ext (extN,extT) args; 
  7.2174 +      in Const (mk_updC rec_schemeT0 (c,T))
  7.2175 +          :== (lambda (Free (base c,T)) (lambda r0 (parent_more_upd new r0)))
  7.2176 +      end;
  7.2177 +    val upd_specs = map mk_upd_spec fields_more;
  7.2178 +
  7.2179 +    (*derived operations*)
  7.2180 +    val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
  7.2181 +      mk_rec (all_vars @ [HOLogic.unit]) 0;
  7.2182 +    val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :==
  7.2183 +      mk_rec (all_vars @ [HOLogic.unit]) parent_len;
  7.2184 +    val extend_spec = 
  7.2185 +      Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :==
  7.2186 +      mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
  7.2187 +    val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :==
  7.2188 +      mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
  7.2189 +
  7.2190 +    (* 2st stage: defs_thy *)
  7.2191 + 
  7.2192 +    val (defs_thy,((sel_defs,upd_defs),derived_defs)) = 
  7.2193 +        extension_thy
  7.2194 +        |> Theory.add_trfuns 
  7.2195 +            ([],[],field_tr's, [])
  7.2196 +        |> Theory.add_advanced_trfuns 
  7.2197 +            ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
  7.2198 +
  7.2199 +        |> Theory.parent_path
  7.2200 +        |> Theory.add_tyabbrs_i recordT_specs
  7.2201 +        |> Theory.add_path bname
  7.2202 +        |> Theory.add_consts_i
  7.2203 +            (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
  7.2204 +        |> (Theory.add_consts_i o map Syntax.no_syn) 
  7.2205 +            (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
  7.2206 +        |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
  7.2207 +        |>>> (PureThy.add_defs_i false o map Thm.no_attributes) upd_specs
  7.2208 +	|>>> (PureThy.add_defs_i false o map Thm.no_attributes)
  7.2209 +               [make_spec, fields_spec, extend_spec, truncate_spec];
  7.2210 +        
  7.2211 +
  7.2212 +    (* prepare propositions *)
  7.2213 +    val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
  7.2214 +    val C = Free (variant all_variants "C", HOLogic.boolT);    
  7.2215 +    val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT);
  7.2216 +
  7.2217 +    (*selectors*) 
  7.2218 +    val sel_conv_props =
  7.2219 +       map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more;
  7.2220 +
  7.2221 +    (*updates*) 
  7.2222 +    fun mk_upd_prop (i,(c,T)) =
  7.2223 +      let val x' = Free (variant all_variants (base c ^ "'"),T) 
  7.2224 +          val args' = nth_update x' (parent_fields_len + i, all_vars_more)
  7.2225 +      in mk_upd c x' r_rec0 === mk_rec args' 0  end;
  7.2226 +    val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
  7.2227 +
  7.2228 +    (*induct*)
  7.2229 +    val induct_scheme_prop =
  7.2230 +      All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
  7.2231 +    val induct_prop =  
  7.2232 +      (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
  7.2233 +       Trueprop (P_unit $ r_unit0));
  7.2234 +
  7.2235 +    (*surjective*)
  7.2236 +    val surjective_prop =
  7.2237 +      let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more
  7.2238 +      in r0 === mk_rec args 0 end;
  7.2239 +
  7.2240 +    (*cases*)
  7.2241 +    val cases_scheme_prop =
  7.2242 +      (All (map dest_Free all_vars_more) 
  7.2243 +        (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C)) 
  7.2244 +      ==> Trueprop C;
  7.2245 +
  7.2246 +    val cases_prop =
  7.2247 +      (All (map dest_Free all_vars) 
  7.2248 +        (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C)) 
  7.2249 +       ==> Trueprop C;
  7.2250 +
  7.2251 +    (*split*)
  7.2252 +    val split_meta_prop =
  7.2253 +      let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in
  7.2254 +        Logic.mk_equals 
  7.2255 +         (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
  7.2256 +      end; 
  7.2257 +
  7.2258 +    val split_object_prop =
  7.2259 +      let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) (vs,t)
  7.2260 +      in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0))
  7.2261 +      end;
  7.2262 +
  7.2263 +
  7.2264 +    val split_ex_prop =
  7.2265 +      let fun EX vs t = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) (vs,t)
  7.2266 +      in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0))
  7.2267 +      end;
  7.2268 +
  7.2269 +    (*equality*)
  7.2270 +    val equality_prop =
  7.2271 +      let 
  7.2272 +	val s' = Free (rN ^ "'", rec_schemeT0)
  7.2273 +        fun mk_sel_eq (c,Free (_,T)) =  mk_sel r0 (c,T) === mk_sel s' (c,T) 
  7.2274 +        val seleqs = map mk_sel_eq all_named_vars_more
  7.2275 +      in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end;
  7.2276 +
  7.2277 +    (* 3rd stage: thms_thy *)
  7.2278 +
  7.2279 +    val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
  7.2280 +    fun prove_simp ss simps =
  7.2281 +      let val tac = simp_all_tac ss simps
  7.2282 +      in fn prop => prove_standard [] [] prop (K tac) end;
  7.2283 +
  7.2284 +    val ss = get_simpset (sign_of defs_thy);
  7.2285 +    val sel_convs = map (prove_simp ss 
  7.2286 +                           (sel_defs@ext_dest_convs)) sel_conv_props;
  7.2287 +
  7.2288 +    val upd_convs = map (prove_simp ss (sel_convs@upd_defs)) 
  7.2289 +                         upd_conv_props;
  7.2290 +      
  7.2291 +    val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
  7.2292 +
  7.2293 +    val induct_scheme = prove_standard [] [] induct_scheme_prop (fn prems =>
  7.2294 +          (EVERY [if null parent_induct 
  7.2295 +                  then all_tac else try_param_tac rN (hd parent_induct) 1,
  7.2296 +                  try_param_tac rN ext_induct 1,
  7.2297 +                  asm_simp_tac HOL_basic_ss 1]));
  7.2298 +
  7.2299 +    val induct =
  7.2300 +      let val (assm, concl) = induct_prop;
  7.2301 +      in
  7.2302 +        prove_standard [] [assm] concl (fn prems =>
  7.2303 +          try_param_tac rN induct_scheme 1
  7.2304 +          THEN try_param_tac "more" unit_induct 1
  7.2305 +          THEN resolve_tac prems 1)
  7.2306 +      end;
  7.2307 +
  7.2308 +    val surjective = 
  7.2309 +      prove_standard [] [] surjective_prop (fn prems =>
  7.2310 +          (EVERY [try_param_tac rN induct_scheme 1,
  7.2311 +                  simp_tac (ss addsimps sel_convs) 1]))
  7.2312 +    
  7.2313 +    val cases_scheme =
  7.2314 +        prove_standard [] [] cases_scheme_prop (fn prems =>
  7.2315 +         EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
  7.2316 +               try_param_tac rN induct_scheme 1,
  7.2317 +               rtac impI 1,
  7.2318 +               REPEAT (etac allE 1),
  7.2319 +               etac mp 1,
  7.2320 +               rtac refl 1])
  7.2321 +
  7.2322 +    val cases =
  7.2323 +      prove_standard [] [] cases_prop  (fn _ =>
  7.2324 +        try_param_tac rN cases_scheme 1
  7.2325 +        THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
  7.2326 +
  7.2327 +    val split_meta =
  7.2328 +        prove_standard [] [] split_meta_prop (fn prems =>
  7.2329 +         EVERY [rtac equal_intr_rule 1,
  7.2330 +                  rtac meta_allE 1, etac triv_goal 1, atac 1,
  7.2331 +                rtac (prop_subst OF [surjective]) 1,
  7.2332 +                REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]),
  7.2333 +                atac 1]);
  7.2334 +
  7.2335 +    val split_object =
  7.2336 +        prove_standard [] [] split_object_prop (fn prems =>
  7.2337 +         EVERY [rtac iffI 1, 
  7.2338 +                REPEAT (rtac allI 1), etac allE 1, atac 1,
  7.2339 +                rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
  7.2340 +
  7.2341 +    val split_ex = 
  7.2342 +        prove_standard [] [] split_ex_prop (fn prems =>
  7.2343 +         fast_simp_tac (claset_of HOL.thy,
  7.2344 +                       HOL_basic_ss addsimps [split_meta]) 1);
  7.2345 +
  7.2346 +    val equality = prove_standard [] [] equality_prop (fn _ =>
  7.2347 +      fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
  7.2348 +        st |> (res_inst_tac [(rN, s)] cases_scheme 1
  7.2349 +        THEN res_inst_tac [(rN, s')] cases_scheme 1
  7.2350 +        THEN simp_all_tac ss (sel_convs))
  7.2351 +      end);
  7.2352 +
  7.2353 +    val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
  7.2354 +                    derived_defs'],
  7.2355 +                   [surjective',equality']),[induct_scheme',induct',cases_scheme',cases'])) =
  7.2356 +      defs_thy
  7.2357 +      |> (PureThy.add_thmss o map Thm.no_attributes)
  7.2358 +         [("select_convs", sel_convs),
  7.2359 +          ("update_convs", upd_convs),
  7.2360 +          ("select_defs", sel_defs),
  7.2361 +          ("update_defs", upd_defs),
  7.2362 +          ("splits", [split_meta,split_object,split_ex]),
  7.2363 +          ("defs", derived_defs)]
  7.2364 +      |>>> (PureThy.add_thms o map Thm.no_attributes)
  7.2365 +          [("surjective", surjective),
  7.2366 +           ("equality", equality)]
  7.2367 +      |>>> PureThy.add_thms 
  7.2368 +        [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
  7.2369 +         (("induct", induct), induct_type_global name),
  7.2370 +         (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
  7.2371 +         (("cases", cases), cases_type_global name)];
  7.2372 +
  7.2373 +
  7.2374 +    val sel_upd_simps = sel_convs' @ upd_convs';
  7.2375 +    val iffs = [ext_inject]
  7.2376 +    val final_thy =
  7.2377 +      thms_thy
  7.2378 +      |> (#1 oo PureThy.add_thmss)
  7.2379 +          [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
  7.2380 +           (("iffs",iffs), [iff_add_global])]
  7.2381 +      |> put_record name (make_record_info args parent fields extension induct_scheme') 
  7.2382 +      |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
  7.2383 +      |> add_record_equalities extension_id equality'
  7.2384 +      |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
  7.2385 +      |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) 
  7.2386 +      |> add_fieldext (extension_name,snd extension) (names @ [full_moreN]) 
  7.2387 +      |> Theory.parent_path;
  7.2388 +
  7.2389 +  in final_thy
  7.2390 +  end;
  7.2391  
  7.2392  (* add_record *)
  7.2393  
  7.2394  (*we do all preparations and error checks here, deferring the real
  7.2395    work to record_definition*)
  7.2396 -
  7.2397  fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
  7.2398    let
  7.2399 -    val _ = Theory.requires thy "Record" "record definitions";
  7.2400 +    val _ = Theory.requires thy "Record" "record definitions"; 
  7.2401      val sign = Theory.sign_of thy;
  7.2402      val _ = message ("Defining record " ^ quote bname ^ " ...");
  7.2403  
  7.2404 @@ -1479,7 +1648,7 @@
  7.2405      (* errors *)
  7.2406  
  7.2407      val name = Sign.full_name sign bname;
  7.2408 -    val err_dup_record =
  7.2409 +    val err_dup_record =  
  7.2410        if is_none (get_record thy name) then []
  7.2411        else ["Duplicate definition of record " ^ quote name];
  7.2412  
  7.2413 @@ -1513,7 +1682,7 @@
  7.2414        err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
  7.2415        err_dup_fields @ err_bad_fields @ err_dup_sorts;
  7.2416    in
  7.2417 -    if null errs then () else error (cat_lines errs);
  7.2418 +    if null errs then () else error (cat_lines errs)  ;
  7.2419      thy |> record_definition (args, bname) parent parents bfields
  7.2420    end
  7.2421    handle ERROR => error ("Failed to define record " ^ quote bname);
  7.2422 @@ -1521,19 +1690,15 @@
  7.2423  val add_record = gen_add_record read_typ read_raw_parent;
  7.2424  val add_record_i = gen_add_record cert_typ (K I);
  7.2425  
  7.2426 -
  7.2427 -(** package setup **)
  7.2428 -
  7.2429  (* setup theory *)
  7.2430  
  7.2431  val setup =
  7.2432   [RecordsData.init,
  7.2433    Theory.add_trfuns ([], parse_translation, [], []),
  7.2434 -  Method.add_methods [record_split_method],
  7.2435 +  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),  
  7.2436    Simplifier.change_simpset_of Simplifier.addsimprocs
  7.2437      [record_simproc, record_eq_simproc]];
  7.2438  
  7.2439 -
  7.2440  (* outer syntax *)
  7.2441  
  7.2442  local structure P = OuterParse and K = OuterSyntax.Keyword in
  7.2443 @@ -1543,8 +1708,8 @@
  7.2444      (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
  7.2445  
  7.2446  val recordP =
  7.2447 -  OuterSyntax.command "record" "define extensible record" K.thy_decl
  7.2448 -    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (#1 o add_record x y z)));
  7.2449 +  OuterSyntax.command "record" "define extensible record" K.thy_decl   
  7.2450 +    (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));  
  7.2451  
  7.2452  val _ = OuterSyntax.add_parsers [recordP];
  7.2453  
     8.1 --- a/src/HOL/ex/Records.thy	Sat May 01 22:28:51 2004 +0200
     8.2 +++ b/src/HOL/ex/Records.thy	Mon May 03 23:22:17 2004 +0200
     8.3 @@ -1,6 +1,7 @@
     8.4  (*  Title:      HOL/ex/Records.thy
     8.5      ID:         $Id$
     8.6 -    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     8.7 +    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
     8.8 +                TU Muenchen
     8.9      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    8.10  *)
    8.11  
    8.12 @@ -19,6 +20,7 @@
    8.13    following theorems:
    8.14  *}
    8.15  
    8.16 +
    8.17  thm "point.simps"
    8.18  thm "point.iffs"
    8.19  thm "point.defs"
    8.20 @@ -28,10 +30,10 @@
    8.21    automatically to the standard simpset, @{thm [source] point.iffs} is
    8.22    added to the Classical Reasoner and Simplifier context.
    8.23  
    8.24 -  \medskip Record declarations define new type abbreviations:
    8.25 +  \medskip Record declarations define new types and type abbreviations:
    8.26    @{text [display]
    8.27 -"    point = (| xpos :: nat, ypos :: nat |)
    8.28 -    'a point_scheme = (| xpos :: nat, ypos :: nat, ... :: 'a |)"}
    8.29 +"  point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
    8.30 +  'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
    8.31  *}
    8.32  
    8.33  consts foo1 :: point
    8.34 @@ -107,7 +109,7 @@
    8.35    induction.
    8.36  *}
    8.37  
    8.38 -lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
    8.39 +lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
    8.40  proof (cases r)
    8.41    fix xpos ypos more
    8.42    assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
    8.43 @@ -174,10 +176,12 @@
    8.44  
    8.45  
    8.46  text {*
    8.47 -  The record declaration defines new type constructors:
    8.48 +  The record declaration defines a new type constructure and abbreviations:
    8.49    @{text [display]
    8.50 -"    cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |)
    8.51 -    'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"}
    8.52 +"  cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = 
    8.53 +     () cpoint_ext_type point_ext_type
    8.54 +   'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = 
    8.55 +     'a cpoint_ext_type point_ext_type"}
    8.56  *}
    8.57  
    8.58  consts foo6 :: cpoint
     9.1 --- a/src/HOL/thy_syntax.ML	Sat May 01 22:28:51 2004 +0200
     9.2 +++ b/src/HOL/thy_syntax.ML	Mon May 03 23:22:17 2004 +0200
     9.3 @@ -277,7 +277,7 @@
     9.4  val _ = ThySyn.add_syntax
     9.5   ["intrs", "monos", "congs", "simpset", "|", "and", "distinct", "inject", "induct"]
     9.6   [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl,
     9.7 -  section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
     9.8 +  section "record" "|> RecordPackage.add_record" record_decl,
     9.9    section "inductive" 	"" (inductive_decl false),
    9.10    section "coinductive"	"" (inductive_decl true),
    9.11    section "datatype" 	"" datatype_decl,
    10.1 --- a/src/Pure/sign.ML	Sat May 01 22:28:51 2004 +0200
    10.2 +++ b/src/Pure/sign.ML	Mon May 03 23:22:17 2004 +0200
    10.3 @@ -61,6 +61,7 @@
    10.4    val extern: sg -> string -> string -> xstring
    10.5    val cond_extern: sg -> string -> string -> xstring
    10.6    val cond_extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list
    10.7 +  val extern_typ: sg -> typ -> typ
    10.8    val intern_class: sg -> xclass -> class
    10.9    val intern_tycon: sg -> xstring -> string
   10.10    val intern_const: sg -> xstring -> string
   10.11 @@ -551,6 +552,9 @@
   10.12    val cond_extern = cond_extrn o spaces_of;
   10.13    fun cond_extern_table sg = cond_extrn_table (spaces_of sg);
   10.14  
   10.15 +  fun extern_typ (sg as Sg (_, {spaces, ...})) T =
   10.16 +       if ! NameSpace.long_names then T else extrn_typ spaces T;
   10.17 +
   10.18    val intern_class = intrn_class o spaces_of;
   10.19    val intern_sort = intrn_sort o spaces_of;
   10.20    val intern_typ = intrn_typ o spaces_of;
   10.21 @@ -596,9 +600,8 @@
   10.22  
   10.23  fun pretty_term sg = pretty_term' (syn_of sg) sg;
   10.24  
   10.25 -fun pretty_typ (sg as Sg (_, {spaces, ...})) T =
   10.26 -  Syntax.pretty_typ (syn_of sg)
   10.27 -    (if ! NameSpace.long_names then T else extrn_typ spaces T);
   10.28 +fun pretty_typ sg T =
   10.29 +  Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
   10.30  
   10.31  fun pretty_sort (sg as Sg (_, {spaces, ...})) S =
   10.32    Syntax.pretty_sort (syn_of sg)