Initial attempt at porting record update to repository Isabelle.
authortsewell@rubicon.NSW.bigpond.net.au
Thu Aug 27 00:40:53 2009 +1000 (2009-08-27)
changeset 32743c4e9a48bc50e
parent 32379 a97e9caebd60
child 32744 50406c4951d9
Initial attempt at porting record update to repository Isabelle.
src/HOL/IsTuple.thy
src/HOL/Record.thy
src/HOL/Tools/istuple_support.ML
src/HOL/Tools/record.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IsTuple.thy	Thu Aug 27 00:40:53 2009 +1000
     1.3 @@ -0,0 +1,289 @@
     1.4 +theory IsTuple imports Product_Type
     1.5 +
     1.6 +uses ("Tools/istuple_support.ML")
     1.7 +
     1.8 +begin
     1.9 +
    1.10 +constdefs
    1.11 +  istuple_fst :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.12 + "istuple_fst isom \<equiv> (fst \<circ> isom)"
    1.13 +  istuple_snd :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.14 + "istuple_snd isom \<equiv> (snd \<circ> isom)"
    1.15 +  istuple_fst_update :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> (('b \<times> 'c) \<Rightarrow> 'a)
    1.16 +                           \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.17 + "istuple_fst_update isom inv \<equiv> \<lambda>f v. inv (f (fst (isom v)), snd (isom v))"
    1.18 +  istuple_snd_update :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> (('b \<times> 'c) \<Rightarrow> 'a)
    1.19 +                           \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.20 + "istuple_snd_update isom inv \<equiv> \<lambda>f v. inv (fst (isom v), f (snd (isom v)))"
    1.21 +
    1.22 +constdefs
    1.23 +  istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.24 + "istuple_surjective_proof_assist x y f \<equiv> f x = y"
    1.25 +  istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a))
    1.26 +                              \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.27 + "istuple_update_accessor_cong_assist upd acc
    1.28 +    \<equiv> (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v)
    1.29 +       \<and> (\<forall>v. upd id v = v)"
    1.30 +  istuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b)
    1.31 +                              \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    1.32 + "istuple_update_accessor_eq_assist upd acc v f v' x
    1.33 +    \<equiv> upd f v = v' \<and> acc v = x
    1.34 +      \<and> istuple_update_accessor_cong_assist upd acc"
    1.35 +
    1.36 +lemma update_accessor_congruence_foldE:
    1.37 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
    1.38 +  and       r: "r = r'" and v: "acc r' = v'"
    1.39 +  and       f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
    1.40 +  shows        "upd f r = upd f' r'"
    1.41 +  using uac r v[symmetric]
    1.42 +  apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
    1.43 +   apply (simp add: istuple_update_accessor_cong_assist_def)
    1.44 +  apply (simp add: f)
    1.45 +  done
    1.46 +
    1.47 +lemma update_accessor_congruence_unfoldE:
    1.48 +  "\<lbrakk> istuple_update_accessor_cong_assist upd acc;
    1.49 +     r = r'; acc r' = v'; \<And>v. v = v' \<Longrightarrow> f v = f' v \<rbrakk>
    1.50 +     \<Longrightarrow> upd f r = upd f' r'"
    1.51 +  apply (erule(2) update_accessor_congruence_foldE)
    1.52 +  apply simp
    1.53 +  done
    1.54 +
    1.55 +lemma istuple_update_accessor_cong_assist_id:
    1.56 +  "istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id"
    1.57 +  by (rule ext, simp add: istuple_update_accessor_cong_assist_def)
    1.58 +
    1.59 +lemma update_accessor_noopE:
    1.60 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
    1.61 +      and acc: "f (acc x) = acc x"
    1.62 +  shows        "upd f x = x"
    1.63 +  using uac
    1.64 +  by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def]
    1.65 +          cong: update_accessor_congruence_unfoldE[OF uac])
    1.66 +
    1.67 +lemma update_accessor_noop_compE:
    1.68 +  assumes uac: "istuple_update_accessor_cong_assist upd acc"
    1.69 +  assumes acc: "f (acc x) = acc x"
    1.70 +  shows      "upd (g \<circ> f) x = upd g x"
    1.71 +  by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac])
    1.72 +
    1.73 +lemma update_accessor_cong_assist_idI:
    1.74 +  "istuple_update_accessor_cong_assist id id"
    1.75 +  by (simp add: istuple_update_accessor_cong_assist_def)
    1.76 +
    1.77 +lemma update_accessor_cong_assist_triv:
    1.78 +  "istuple_update_accessor_cong_assist upd acc
    1.79 +       \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
    1.80 +  by assumption
    1.81 +
    1.82 +lemma update_accessor_accessor_eqE:
    1.83 +  "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> acc v = x"
    1.84 +  by (simp add: istuple_update_accessor_eq_assist_def)
    1.85 +
    1.86 +lemma update_accessor_updator_eqE:
    1.87 +  "\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> upd f v = v'"
    1.88 +  by (simp add: istuple_update_accessor_eq_assist_def)
    1.89 +
    1.90 +lemma istuple_update_accessor_eq_assist_idI:
    1.91 +  "v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v"
    1.92 +  by (simp add: istuple_update_accessor_eq_assist_def
    1.93 +                update_accessor_cong_assist_idI)
    1.94 +
    1.95 +lemma istuple_update_accessor_eq_assist_triv:
    1.96 +  "istuple_update_accessor_eq_assist upd acc v f v' x
    1.97 +     \<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x"
    1.98 +  by assumption
    1.99 +
   1.100 +lemma istuple_update_accessor_cong_from_eq:
   1.101 +  "istuple_update_accessor_eq_assist upd acc v f v' x
   1.102 +     \<Longrightarrow> istuple_update_accessor_cong_assist upd acc"
   1.103 +  by (simp add: istuple_update_accessor_eq_assist_def)
   1.104 +
   1.105 +lemma o_eq_dest:
   1.106 +  "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
   1.107 +  apply (clarsimp simp: o_def)
   1.108 +  apply (erule fun_cong)
   1.109 +  done
   1.110 +
   1.111 +lemma o_eq_elim:
   1.112 +  "\<lbrakk> a o b = c o d; \<lbrakk> \<And>v. a (b v) = c (d v) \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
   1.113 +  apply (erule meta_mp)
   1.114 +  apply (erule o_eq_dest)
   1.115 +  done
   1.116 +
   1.117 +lemma istuple_surjective_proof_assistI:
   1.118 +  "f x = y \<Longrightarrow>
   1.119 +     istuple_surjective_proof_assist x y f"
   1.120 +  by (simp add: istuple_surjective_proof_assist_def)
   1.121 +
   1.122 +lemma istuple_surjective_proof_assist_idE:
   1.123 +  "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
   1.124 +  by (simp add: istuple_surjective_proof_assist_def)
   1.125 +
   1.126 +locale isomorphic_tuple =
   1.127 +  fixes isom :: "'a \<Rightarrow> ('b \<times> 'c)" and inv :: "('b \<times> 'c) \<Rightarrow> 'a"
   1.128 +    and cons :: "'b \<Rightarrow> 'c \<Rightarrow> 'a"
   1.129 +  assumes isom_eq: "(isom x = isom y) = (x = y)"
   1.130 +  and inverse_inv: "isom (inv v) = v"
   1.131 +  and cons_def: "cons \<equiv> curry inv"
   1.132 +
   1.133 +begin
   1.134 +
   1.135 +lemma inverse_isom:
   1.136 +  "(inv (isom v)) = v"
   1.137 +  by (rule iffD1 [OF isom_eq], simp add: inverse_inv)
   1.138 +
   1.139 +lemma inv_eq:
   1.140 +  "(inv x = inv y) = (x = y)"
   1.141 +  apply (rule iffI)
   1.142 +   apply (drule arg_cong[where f=isom])
   1.143 +   apply (simp add: inverse_inv)
   1.144 +  apply simp
   1.145 +  done
   1.146 +
   1.147 +lemmas simps = isom_eq inv_eq inverse_inv inverse_isom cons_def
   1.148 +
   1.149 +lemma istuple_access_update_fst_fst:
   1.150 +  "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   1.151 +    (f o istuple_fst isom) o (istuple_fst_update isom inv o h) g
   1.152 +          = j o (f o istuple_fst isom)"
   1.153 +  by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps
   1.154 +             intro!: ext elim!: o_eq_elim)
   1.155 +
   1.156 +lemma istuple_access_update_snd_snd:
   1.157 +  "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow>
   1.158 +    (f o istuple_snd isom) o (istuple_snd_update isom inv o h) g
   1.159 +          = j o (f o istuple_snd isom)"
   1.160 +  by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps
   1.161 +             intro!: ext elim!: o_eq_elim)
   1.162 +
   1.163 +lemma istuple_access_update_fst_snd:
   1.164 +  "(f o istuple_fst isom) o (istuple_snd_update isom inv o h) g
   1.165 +          = id o (f o istuple_fst isom)"
   1.166 +  by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps
   1.167 +             intro!: ext elim!: o_eq_elim)
   1.168 +
   1.169 +lemma istuple_access_update_snd_fst:
   1.170 +  "(f o istuple_snd isom) o (istuple_fst_update isom inv o h) g
   1.171 +          = id o (f o istuple_snd isom)"
   1.172 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps
   1.173 +             intro!: ext elim!: o_eq_elim)
   1.174 +
   1.175 +lemma istuple_update_swap_fst_fst:
   1.176 +  "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   1.177 +    (istuple_fst_update isom inv o h) f o (istuple_fst_update isom inv o j) g
   1.178 +          = (istuple_fst_update isom inv o j) g o (istuple_fst_update isom inv o h) f"
   1.179 +  by (clarsimp simp: istuple_fst_update_def simps
   1.180 +             intro!: ext elim!: o_eq_elim)
   1.181 +
   1.182 +lemma istuple_update_swap_snd_snd:
   1.183 +  "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow>
   1.184 +    (istuple_snd_update isom inv o h) f o (istuple_snd_update isom inv o j) g
   1.185 +          = (istuple_snd_update isom inv o j) g o (istuple_snd_update isom inv o h) f"
   1.186 +  by (clarsimp simp: istuple_snd_update_def simps
   1.187 +             intro!: ext elim!: o_eq_elim)
   1.188 +
   1.189 +lemma istuple_update_swap_fst_snd:
   1.190 +  "(istuple_snd_update isom inv o h) f o (istuple_fst_update isom inv o j) g
   1.191 +          = (istuple_fst_update isom inv o j) g o (istuple_snd_update isom inv o h) f"
   1.192 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   1.193 +             intro!: ext elim!: o_eq_elim)
   1.194 +
   1.195 +lemma istuple_update_swap_snd_fst:
   1.196 +  "(istuple_fst_update isom inv o h) f o (istuple_snd_update isom inv o j) g
   1.197 +          = (istuple_snd_update isom inv o j) g o (istuple_fst_update isom inv o h) f"
   1.198 +  by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps
   1.199 +             intro!: ext elim!: o_eq_elim)
   1.200 +
   1.201 +lemma istuple_update_compose_fst_fst:
   1.202 +  "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   1.203 +    (istuple_fst_update isom inv o h) f o (istuple_fst_update isom inv o j) g
   1.204 +          = (istuple_fst_update isom inv o k) (f o g)"
   1.205 +  by (fastsimp simp: istuple_fst_update_def simps
   1.206 +             intro!: ext elim!: o_eq_elim dest: fun_cong)
   1.207 +
   1.208 +lemma istuple_update_compose_snd_snd:
   1.209 +  "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow>
   1.210 +    (istuple_snd_update isom inv o h) f o (istuple_snd_update isom inv o j) g
   1.211 +          = (istuple_snd_update isom inv o k) (f o g)"
   1.212 +  by (fastsimp simp: istuple_snd_update_def simps
   1.213 +             intro!: ext elim!: o_eq_elim dest: fun_cong)
   1.214 +
   1.215 +lemma istuple_surjective_proof_assist_step:
   1.216 +  "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f);
   1.217 +     istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk>
   1.218 +      \<Longrightarrow> istuple_surjective_proof_assist v (cons a b) f"
   1.219 +  by (clarsimp simp: istuple_surjective_proof_assist_def simps
   1.220 +                     istuple_fst_def istuple_snd_def)
   1.221 +
   1.222 +lemma istuple_fst_update_accessor_cong_assist:
   1.223 +  "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   1.224 +      istuple_update_accessor_cong_assist (istuple_fst_update isom inv o f) (g o istuple_fst isom)"
   1.225 +  by (simp add: istuple_update_accessor_cong_assist_def istuple_fst_update_def istuple_fst_def simps)
   1.226 +
   1.227 +lemma istuple_snd_update_accessor_cong_assist:
   1.228 +  "istuple_update_accessor_cong_assist f g \<Longrightarrow>
   1.229 +      istuple_update_accessor_cong_assist (istuple_snd_update isom inv o f) (g o istuple_snd isom)"
   1.230 +  by (simp add: istuple_update_accessor_cong_assist_def istuple_snd_update_def istuple_snd_def simps)
   1.231 +
   1.232 +lemma istuple_fst_update_accessor_eq_assist:
   1.233 +  "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow>
   1.234 +      istuple_update_accessor_eq_assist (istuple_fst_update isom inv o f) (g o istuple_fst isom)
   1.235 +              (cons a b) u (cons a' b) v"
   1.236 +  by (simp add: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def simps
   1.237 +                istuple_update_accessor_cong_assist_def)
   1.238 +
   1.239 +lemma istuple_snd_update_accessor_eq_assist:
   1.240 +  "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow>
   1.241 +      istuple_update_accessor_eq_assist (istuple_snd_update isom inv o f) (g o istuple_snd isom)
   1.242 +              (cons a b) u (cons a b') v"
   1.243 +  by (simp add: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def simps
   1.244 +                istuple_update_accessor_cong_assist_def)
   1.245 +
   1.246 +lemma cons_conj_eqI:
   1.247 +  "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow>
   1.248 +    (cons a b = cons c d \<and> P) = Q"
   1.249 +  by (simp add: simps)
   1.250 +
   1.251 +lemmas intros =
   1.252 +    istuple_access_update_fst_fst
   1.253 +    istuple_access_update_snd_snd
   1.254 +    istuple_access_update_fst_snd
   1.255 +    istuple_access_update_snd_fst
   1.256 +    istuple_update_swap_fst_fst
   1.257 +    istuple_update_swap_snd_snd
   1.258 +    istuple_update_swap_fst_snd
   1.259 +    istuple_update_swap_snd_fst
   1.260 +    istuple_update_compose_fst_fst
   1.261 +    istuple_update_compose_snd_snd
   1.262 +    istuple_surjective_proof_assist_step
   1.263 +    istuple_fst_update_accessor_eq_assist
   1.264 +    istuple_snd_update_accessor_eq_assist
   1.265 +    istuple_fst_update_accessor_cong_assist
   1.266 +    istuple_snd_update_accessor_cong_assist
   1.267 +    cons_conj_eqI
   1.268 +
   1.269 +end
   1.270 +
   1.271 +interpretation tuple_automorphic: isomorphic_tuple [id id Pair]
   1.272 +  by (unfold_locales, simp_all add: curry_def)
   1.273 +
   1.274 +lemma refl_conj_eq:
   1.275 +  "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
   1.276 +  by simp
   1.277 +
   1.278 +lemma meta_all_sameI:
   1.279 +  "(\<And>x. PROP P x \<equiv> PROP Q x) \<Longrightarrow> (\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)"
   1.280 +  by simp
   1.281 +
   1.282 +lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
   1.283 +  by simp
   1.284 +
   1.285 +lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
   1.286 +  by simp
   1.287 +
   1.288 +ML {* val traceref = ref [TrueI]; *}
   1.289 +
   1.290 +use "Tools/istuple_support.ML";
   1.291 +
   1.292 +end
     2.1 --- a/src/HOL/Record.thy	Sat Aug 15 15:29:54 2009 +0200
     2.2 +++ b/src/HOL/Record.thy	Thu Aug 27 00:40:53 2009 +1000
     2.3 @@ -1,26 +1,36 @@
     2.4  (*  Title:      HOL/Record.thy
     2.5 +    ID:         $Id: Record.thy,v 1.33 2007/12/19 15:32:12 schirmer Exp $
     2.6      Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     2.7  *)
     2.8  
     2.9  header {* Extensible records with structural subtyping *}
    2.10  
    2.11  theory Record
    2.12 -imports Product_Type
    2.13 -uses ("Tools/record.ML")
    2.14 +imports Product_Type IsTuple
    2.15 +uses ("Tools/record_package.ML")
    2.16  begin
    2.17  
    2.18  lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
    2.19    by simp
    2.20  
    2.21 -lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
    2.22 -  by simp
    2.23 -
    2.24 -lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    2.25 -  by simp
    2.26 -
    2.27  lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 
    2.28    by (simp add: comp_def)
    2.29  
    2.30 +lemma meta_iffD2:
    2.31 +  "\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P"
    2.32 +  by simp
    2.33 +
    2.34 +lemma o_eq_dest_lhs:
    2.35 +  "a o b = c \<Longrightarrow> a (b v) = c v"
    2.36 +  by clarsimp
    2.37 +
    2.38 +lemma id_o_refl:
    2.39 +  "id o f = f o id"
    2.40 +  by simp
    2.41 +
    2.42 +lemma o_eq_id_dest:
    2.43 +  "a o b = id o c \<Longrightarrow> a (b v) = c v"
    2.44 +  by clarsimp
    2.45  
    2.46  subsection {* Concrete record syntax *}
    2.47  
    2.48 @@ -55,7 +65,7 @@
    2.49    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    2.50    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
    2.51  
    2.52 -use "Tools/record.ML"
    2.53 -setup Record.setup
    2.54 +use "Tools/record_package.ML"
    2.55 +setup RecordPackage.setup
    2.56  
    2.57  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/istuple_support.ML	Thu Aug 27 00:40:53 2009 +1000
     3.3 @@ -0,0 +1,145 @@
     3.4 +(*  Title:	HOL/Tools/ntuple_support.ML
     3.5 +    Author:	Thomas Sewell, NICTA
     3.6 +
     3.7 +Support for defining instances of tuple-like types and extracting
     3.8 +introduction rules needed by the record package.
     3.9 +*)
    3.10 +
    3.11 +
    3.12 +signature ISTUPLE_SUPPORT =
    3.13 +sig
    3.14 +  val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
    3.15 +            (term * theory);
    3.16 +  type tagged_net = ((string * int) * thm) Net.net;
    3.17 +
    3.18 +  val get_istuple_intros: theory -> tagged_net;
    3.19 +
    3.20 +  val build_tagged_net: string -> thm list -> tagged_net;
    3.21 +  val resolve_from_tagged_net: tagged_net -> int -> tactic;
    3.22 +  val tag_thm_trace: thm list ref;
    3.23 +  val merge_tagged_nets: (tagged_net * tagged_net) -> tagged_net;
    3.24 +end;
    3.25 +
    3.26 +structure IsTupleSupport : ISTUPLE_SUPPORT =
    3.27 +struct
    3.28 +
    3.29 +val consN = "_NTupleCons";
    3.30 +val defN = "_def";
    3.31 +
    3.32 +val istuple_UNIV_I = thm "istuple_UNIV_I";
    3.33 +val istuple_True_simp = thm "istuple_True_simp";
    3.34 +
    3.35 +val istuple_intro = thm "isomorphic_tuple.intro";
    3.36 +val istuple_intros = thms "isomorphic_tuple.intros";
    3.37 +
    3.38 +val init_intros = thms "tuple_automorphic.intros";
    3.39 +
    3.40 +type tagged_net = ((string * int) * thm) Net.net;
    3.41 +
    3.42 +(* broadly similar to the use of nets in Tactic.resolve_from_net_tac.
    3.43 +   the tag strings identify which group of theorems a theorem in the
    3.44 +   net belongs to. *)
    3.45 +fun build_tagged_net tag thms = let
    3.46 +    fun add_to_net thm (i, net) =
    3.47 +        (i + 1, Net.insert_term (K false) (concl_of thm, ((tag, i), thm)) net);
    3.48 +    val (n, net) = fold add_to_net thms (0, Net.empty);
    3.49 +  in net end;
    3.50 +
    3.51 +val tag_thm_trace = ref ([] : thm list);
    3.52 +
    3.53 +(* we check here that only theorems from a single group are being
    3.54 +   selected for unification, and that there are no duplicates. this
    3.55 +   is a good test that the net is doing its job, picking exactly the
    3.56 +   appropriate rules rather than overapproximating. *)
    3.57 +fun tagged_thms_check t xs = let
    3.58 +    val tags = sort_distinct string_ord (map (fst o fst) xs);
    3.59 +    val ids  = sort_distinct int_ord (map (snd o fst) xs);
    3.60 +    val thms = map snd xs;
    3.61 +in
    3.62 +   if length tags > 1
    3.63 +   then (tag_thm_trace := t :: thms;
    3.64 +     raise THM ("tag mismatch " ^ hd tags ^ ", " ^ nth tags 1, 1, t :: thms))
    3.65 +   else if length ids < length xs
    3.66 +   then (tag_thm_trace := t :: thms;
    3.67 +     raise THM ("tag match duplicate id ", 1, t :: thms))
    3.68 +   else ()
    3.69 +end;
    3.70 +
    3.71 +fun resolve_from_tagged_net net i t =
    3.72 +  SUBGOAL (fn (prem, i) => let
    3.73 +      val options = Net.unify_term net (Logic.strip_assums_concl prem);
    3.74 +      val sorted  = sort (int_ord o pairself (snd o fst)) options;
    3.75 +      val check   = tagged_thms_check t sorted;
    3.76 +    in resolve_tac (map snd sorted) i end) i t;
    3.77 +
    3.78 +val merge_tagged_nets = Net.merge (Thm.eq_thm_prop o pairself snd);
    3.79 +
    3.80 +structure IsTupleIntros = TheoryDataFun
    3.81 +(
    3.82 +  type T = tagged_net;
    3.83 +  val empty = build_tagged_net "initial introduction rules" init_intros;
    3.84 +  val copy = I;
    3.85 +  val extend = I;
    3.86 +  val merge = K merge_tagged_nets;
    3.87 +);
    3.88 +
    3.89 +val get_istuple_intros = IsTupleIntros.get;
    3.90 +
    3.91 +fun do_typedef name repT alphas thy =
    3.92 +  let
    3.93 +    fun get_thms thy name =
    3.94 +      let
    3.95 +        val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
    3.96 +          Abs_inverse=abs_inverse, ...} = TypedefPackage.get_info thy name;
    3.97 +        val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
    3.98 +      in (map rewrite_rule [rep_inject, abs_inverse],
    3.99 +            Const (absN, repT --> absT)) end;
   3.100 +  in
   3.101 +    thy
   3.102 +    |> TypecopyPackage.add_typecopy (name, alphas) repT NONE
   3.103 +    |-> (fn (name, _) => `(fn thy => get_thms thy name))
   3.104 +  end;
   3.105 +
   3.106 +fun add_istuple_type (name, alphas) (left, right) thy =
   3.107 +let
   3.108 +  val repT = HOLogic.mk_prodT (left, right);
   3.109 +
   3.110 +  val (([rep_inject, abs_inverse], abs), typ_thy) =
   3.111 +    thy
   3.112 +    |> do_typedef name repT alphas
   3.113 +    ||> Sign.add_path name;
   3.114 +
   3.115 +  val abs_curry = HOLogic.mk_curry abs;
   3.116 +  val consT     = fastype_of abs_curry;
   3.117 +  val cons      = Const (Sign.full_name typ_thy (name ^ consN), consT);
   3.118 +  val cons_spec = (name ^ consN ^ defN, Logic.mk_equals (cons, abs_curry));
   3.119 +
   3.120 +  val ([cons_def], cdef_thy) =
   3.121 +    typ_thy
   3.122 +    |> Sign.add_consts_i [Syntax.no_syn (name ^ consN, consT)]
   3.123 +    |> PureThy.add_defs_i false [Thm.no_attributes cons_spec];
   3.124 +
   3.125 +  val istuple = [abs_inverse, cons_def] MRS (rep_inject RS istuple_intro);
   3.126 +  val intros = [istuple] RL istuple_intros;
   3.127 +  val intro_net = build_tagged_net name intros;
   3.128 +
   3.129 +  val thm_thy =
   3.130 +    cdef_thy
   3.131 +    |> IsTupleIntros.map (curry merge_tagged_nets intro_net)
   3.132 +    |> Sign.parent_path;
   3.133 +in
   3.134 +  (cons, thm_thy)
   3.135 +end;
   3.136 +
   3.137 +end;
   3.138 +
   3.139 +structure IsTupleIntros2 = TheoryDataFun
   3.140 +(
   3.141 +  type T = IsTupleSupport.tagged_net;
   3.142 +  val empty = IsTupleSupport.build_tagged_net "" [];
   3.143 +  val copy = I;
   3.144 +  val extend = I;
   3.145 +  val merge = K IsTupleSupport.merge_tagged_nets;
   3.146 +);
   3.147 +
   3.148 +
     4.1 --- a/src/HOL/Tools/record.ML	Sat Aug 15 15:29:54 2009 +0200
     4.2 +++ b/src/HOL/Tools/record.ML	Thu Aug 27 00:40:53 2009 +1000
     4.3 @@ -55,8 +55,6 @@
     4.4  struct
     4.5  
     4.6  val eq_reflection = thm "eq_reflection";
     4.7 -val rec_UNIV_I = thm "rec_UNIV_I";
     4.8 -val rec_True_simp = thm "rec_True_simp";
     4.9  val Pair_eq = thm "Product_Type.prod.inject";
    4.10  val atomize_all = thm "HOL.atomize_all";
    4.11  val atomize_imp = thm "HOL.atomize_imp";
    4.12 @@ -65,6 +63,34 @@
    4.13  val Pair_sel_convs = [fst_conv,snd_conv];
    4.14  val K_record_comp = @{thm "K_record_comp"};
    4.15  val K_comp_convs = [@{thm o_apply}, K_record_comp]
    4.16 +val transitive_thm = thm "transitive";
    4.17 +val o_assoc = @{thm "o_assoc"};
    4.18 +val id_apply = @{thm id_apply};
    4.19 +val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
    4.20 +
    4.21 +val refl_conj_eq = thm "refl_conj_eq";
    4.22 +val meta_all_sameI = thm "meta_all_sameI";
    4.23 +val meta_iffD2 = thm "meta_iffD2";
    4.24 +
    4.25 +val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
    4.26 +val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
    4.27 +
    4.28 +val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"};
    4.29 +val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"};
    4.30 +val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"};
    4.31 +val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"};
    4.32 +
    4.33 +val updacc_foldE = @{thm "update_accessor_congruence_foldE"};
    4.34 +val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"};
    4.35 +val updacc_noopE = @{thm "update_accessor_noopE"};
    4.36 +val updacc_noop_compE = @{thm "update_accessor_noop_compE"};
    4.37 +val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"};
    4.38 +val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
    4.39 +val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
    4.40 +
    4.41 +val o_eq_dest = thm "o_eq_dest";
    4.42 +val o_eq_id_dest = thm "o_eq_id_dest";
    4.43 +val o_eq_dest_lhs = thm "o_eq_dest_lhs";
    4.44  
    4.45  (** name components **)
    4.46  
    4.47 @@ -73,6 +99,7 @@
    4.48  val moreN = "more";
    4.49  val schemeN = "_scheme";
    4.50  val ext_typeN = "_ext_type";
    4.51 +val inner_typeN = "_inner_type";
    4.52  val extN ="_ext";
    4.53  val casesN = "_cases";
    4.54  val ext_dest = "_sel";
    4.55 @@ -232,23 +259,26 @@
    4.56    parent: (typ list * string) option,
    4.57    fields: (string * typ) list,
    4.58    extension: (string * typ list),
    4.59 -  induct: thm
    4.60 +  induct: thm,
    4.61 +  extdef: thm
    4.62   };
    4.63  
    4.64 -fun make_record_info args parent fields extension induct =
    4.65 +fun make_record_info args parent fields extension induct extdef =
    4.66   {args = args, parent = parent, fields = fields, extension = extension,
    4.67 -  induct = induct}: record_info;
    4.68 +  induct = induct, extdef = extdef}: record_info;
    4.69  
    4.70  
    4.71  type parent_info =
    4.72   {name: string,
    4.73    fields: (string * typ) list,
    4.74    extension: (string * typ list),
    4.75 -  induct: thm
    4.76 +  induct: thm,
    4.77 +  extdef: thm
    4.78  };
    4.79  
    4.80 -fun make_parent_info name fields extension induct =
    4.81 - {name = name, fields = fields, extension = extension, induct = induct}: parent_info;
    4.82 +fun make_parent_info name fields extension induct extdef =
    4.83 + {name = name, fields = fields, extension = extension,
    4.84 +  induct = induct, extdef = extdef}: parent_info;
    4.85  
    4.86  
    4.87  (* theory data *)
    4.88 @@ -278,14 +308,18 @@
    4.89    type T = record_data;
    4.90    val empty =
    4.91      make_record_data Symtab.empty
    4.92 -      {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
    4.93 +      {selectors = Symtab.empty, updates = Symtab.empty,
    4.94 +          simpset = HOL_basic_ss, defset = HOL_basic_ss,
    4.95 +          foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
    4.96         Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
    4.97  
    4.98    val copy = I;
    4.99    val extend = I;
   4.100    fun merge _
   4.101     ({records = recs1,
   4.102 -     sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
   4.103 +     sel_upd = {selectors = sels1, updates = upds1,
   4.104 +                simpset = ss1, defset = ds1,
   4.105 +                foldcong = fc1, unfoldcong = uc1},
   4.106       equalities = equalities1,
   4.107       extinjects = extinjects1,
   4.108       extsplit = extsplit1,
   4.109 @@ -293,7 +327,9 @@
   4.110       extfields = extfields1,
   4.111       fieldext = fieldext1},
   4.112      {records = recs2,
   4.113 -     sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
   4.114 +     sel_upd = {selectors = sels2, updates = upds2,
   4.115 +                simpset = ss2, defset = ds2,
   4.116 +                foldcong = fc2, unfoldcong = uc2},
   4.117       equalities = equalities2,
   4.118       extinjects = extinjects2,
   4.119       extsplit = extsplit2,
   4.120 @@ -304,7 +340,10 @@
   4.121        (Symtab.merge (K true) (recs1, recs2))
   4.122        {selectors = Symtab.merge (K true) (sels1, sels2),
   4.123          updates = Symtab.merge (K true) (upds1, upds2),
   4.124 -        simpset = Simplifier.merge_ss (ss1, ss2)}
   4.125 +        simpset = Simplifier.merge_ss (ss1, ss2),
   4.126 +        defset = Simplifier.merge_ss (ds1, ds2),
   4.127 +        foldcong = Simplifier.merge_ss (fc1, fc2),
   4.128 +        unfoldcong = Simplifier.merge_ss (uc1, uc2)}
   4.129        (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
   4.130        (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
   4.131        (Symtab.merge Thm.eq_thm_prop (extsplit1,extsplit2))
   4.132 @@ -355,7 +394,21 @@
   4.133  
   4.134  val is_selector = Symtab.defined o #selectors o get_sel_upd;
   4.135  val get_updates = Symtab.lookup o #updates o get_sel_upd;
   4.136 -fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
   4.137 +fun get_ss_with_context getss thy =
   4.138 +    Simplifier.theory_context thy (getss (get_sel_upd thy));
   4.139 +
   4.140 +val get_simpset = get_ss_with_context (#simpset);
   4.141 +val get_sel_upd_defs = get_ss_with_context (#defset);
   4.142 +val get_foldcong_ss = get_ss_with_context (#foldcong);
   4.143 +val get_unfoldcong_ss = get_ss_with_context (#unfoldcong);
   4.144 +
   4.145 +fun get_update_details u thy = let
   4.146 +    val sel_upd = get_sel_upd thy;
   4.147 +  in case (Symtab.lookup (#updates sel_upd) u) of
   4.148 +    SOME s => let
   4.149 +        val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s;
   4.150 +      in SOME (s, dep, ismore) end
   4.151 +  | NONE => NONE end;
   4.152  
   4.153  fun put_sel_upd names simps = RecordsData.map (fn {records,
   4.154    sel_upd = {selectors, updates, simpset},
   4.155 @@ -489,7 +542,7 @@
   4.156        let
   4.157          fun err msg = error (msg ^ " parent record " ^ quote name);
   4.158  
   4.159 -        val {args, parent, fields, extension, induct} =
   4.160 +        val {args, parent, fields, extension, induct, extdef} =
   4.161            (case get_record thy name of SOME info => info | NONE => err "Unknown");
   4.162          val _ = if length types <> length args then err "Bad number of arguments for" else ();
   4.163  
   4.164 @@ -505,7 +558,7 @@
   4.165          val extension' = apsnd (map subst) extension;
   4.166        in
   4.167          add_parents thy parent'
   4.168 -          (make_parent_info name fields' extension' induct :: parents)
   4.169 +          (make_parent_info name fields' extension' induct extdef :: parents)
   4.170        end;
   4.171  
   4.172  
   4.173 @@ -882,95 +935,113 @@
   4.174        then noopt ()
   4.175        else opt ();
   4.176  
   4.177 -local
   4.178 -fun abstract_over_fun_app (Abs (f,fT,t)) =
   4.179 -  let
   4.180 -     val (f',t') = Term.dest_abs (f,fT,t);
   4.181 -     val T = domain_type fT;
   4.182 -     val (x,T') = hd (Term.variant_frees t' [("x",T)]);
   4.183 -     val f_x = Free (f',fT)$(Free (x,T'));
   4.184 -     fun is_constr (Const (c,_)$_) = can (unsuffix extN) c
   4.185 -       | is_constr _ = false;
   4.186 -     fun subst (t as u$w) = if Free (f',fT)=u
   4.187 -                            then if is_constr w then f_x
   4.188 -                                 else raise TERM ("abstract_over_fun_app",[t])
   4.189 -                            else subst u$subst w
   4.190 -       | subst (Abs (x,T,t)) = (Abs (x,T,subst t))
   4.191 -       | subst t = t
   4.192 -     val t'' = abstract_over (f_x,subst t');
   4.193 -     val vars = strip_qnt_vars "all" t'';
   4.194 -     val bdy = strip_qnt_body "all" t'';
   4.195 -
   4.196 -  in list_abs ((x,T')::vars,bdy) end
   4.197 -  | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]);
   4.198 -(* Generates a theorem of the kind:
   4.199 - * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x*
   4.200 - *)
   4.201 -fun mk_fun_apply_eq (Abs (f, fT, t)) thy =
   4.202 +fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t'))
   4.203 +  = case (get_updates thy u)
   4.204 +    of SOME u_name => u_name = s
   4.205 +     | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]);
   4.206 +
   4.207 +fun mk_comp f g = let
   4.208 +    val x = fastype_of g;
   4.209 +    val a = domain_type x;
   4.210 +    val b = range_type x;
   4.211 +    val c = range_type (fastype_of f);
   4.212 +    val T = (b --> c) --> ((a --> b) --> (a --> c))
   4.213 +  in Const ("Fun.comp", T) $ f $ g end;
   4.214 +
   4.215 +fun mk_comp_id f = let
   4.216 +    val T = range_type (fastype_of f);
   4.217 +  in mk_comp (Const ("Fun.id", T --> T)) f end;
   4.218 +
   4.219 +fun get_updfuns (upd $ _ $ t) = upd :: get_updfuns t
   4.220 +  | get_updfuns _             = [];
   4.221 +
   4.222 +fun get_accupd_simps thy term defset intros_tac = let
   4.223 +    val (acc, [body]) = strip_comb term;
   4.224 +    val recT          = domain_type (fastype_of acc);
   4.225 +    val updfuns       = sort_distinct Term.fast_term_ord
   4.226 +                           (get_updfuns body);
   4.227 +    fun get_simp upd  = let
   4.228 +        val T    = domain_type (fastype_of upd);
   4.229 +        val lhs  = mk_comp acc (upd $ Free ("f", T));
   4.230 +        val rhs  = if is_sel_upd_pair thy acc upd
   4.231 +                   then mk_comp (Free ("f", T)) acc else mk_comp_id acc;
   4.232 +        val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   4.233 +        val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
   4.234 +            EVERY [simp_tac defset 1,
   4.235 +                   REPEAT_DETERM (intros_tac 1),
   4.236 +                   TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]);
   4.237 +        val dest = if is_sel_upd_pair thy acc upd
   4.238 +                   then o_eq_dest else o_eq_id_dest;
   4.239 +      in standard (othm RS dest) end;
   4.240 +  in map get_simp updfuns end;
   4.241 +
   4.242 +structure SymSymTab = TableFun(type key = string * string
   4.243 +                                val ord = prod_ord fast_string_ord fast_string_ord);
   4.244 +
   4.245 +fun get_updupd_simp thy defset intros_tac u u' comp = let
   4.246 +    val f    = Free ("f", domain_type (fastype_of u));
   4.247 +    val f'   = Free ("f'", domain_type (fastype_of u'));
   4.248 +    val lhs  = mk_comp (u $ f) (u' $ f');
   4.249 +    val rhs  = if comp
   4.250 +               then u $ mk_comp f f'
   4.251 +               else mk_comp (u' $ f') (u $ f);
   4.252 +    val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   4.253 +    val othm = Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
   4.254 +        EVERY [simp_tac defset 1,
   4.255 +               REPEAT_DETERM (intros_tac 1),
   4.256 +               TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
   4.257 +    val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   4.258 +  in standard (othm RS dest) end;
   4.259 +
   4.260 +fun get_updupd_simps thy term defset intros_tac = let
   4.261 +    val recT          = fastype_of term;
   4.262 +    val updfuns       = get_updfuns term;
   4.263 +    val cname         = fst o dest_Const;
   4.264 +    fun getswap u u'  = get_updupd_simp thy defset intros_tac u u'
   4.265 +                              (cname u = cname u');
   4.266 +    fun buildswapstoeq upd [] swaps = swaps
   4.267 +      | buildswapstoeq upd (u::us) swaps = let
   4.268 +             val key      = (cname u, cname upd);
   4.269 +             val newswaps = if SymSymTab.defined swaps key then swaps
   4.270 +                            else SymSymTab.insert (K true)
   4.271 +                                     (key, getswap u upd) swaps;
   4.272 +          in if cname u = cname upd then newswaps
   4.273 +             else buildswapstoeq upd us newswaps end;
   4.274 +    fun swapsneeded []      prev seen swaps = map snd (SymSymTab.dest swaps)
   4.275 +      | swapsneeded (u::us) prev seen swaps =
   4.276 +           if Symtab.defined seen (cname u)
   4.277 +           then swapsneeded us prev seen
   4.278 +                   (buildswapstoeq u prev swaps)
   4.279 +           else swapsneeded us (u::prev)
   4.280 +                   (Symtab.insert (K true) (cname u, ()) seen) swaps;
   4.281 +  in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end;
   4.282 +
   4.283 +fun named_cterm_instantiate values thm = let
   4.284 +    fun match name (Var ((name', _), _)) = name = name'
   4.285 +      | match name _ = false;
   4.286 +    fun getvar name = case (find_first (match name) (term_vars (prop_of thm)))
   4.287 +      of SOME var => cterm_of (theory_of_thm thm) var
   4.288 +       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
   4.289 +  in
   4.290 +    cterm_instantiate (map (apfst getvar) values) thm
   4.291 +  end;
   4.292 +
   4.293 +fun prove_unfold_defs thy ss T ex_simps ex_simprs prop =
   4.294    let
   4.295 -    val rT = domain_type fT;
   4.296 -    val vars = Term.strip_qnt_vars "all" t;
   4.297 -    val Ts = map snd vars;
   4.298 -    val n = length vars;
   4.299 -    fun app_bounds 0 t = t$Bound 0
   4.300 -      | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t
   4.301 -
   4.302 -
   4.303 -    val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)];
   4.304 -    val prop = Logic.mk_equals
   4.305 -                (list_all ((f,fT)::vars,
   4.306 -                           app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))),
   4.307 -                 list_all ((fst r,rT)::vars,
   4.308 -                           app_bounds (n - 1) ((Free P)$Bound n)));
   4.309 -    val prove_standard = quick_and_dirty_prove true thy;
   4.310 -    val thm = prove_standard [] prop (fn _ =>
   4.311 -	 EVERY [rtac equal_intr_rule 1,
   4.312 -                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1,
   4.313 -                Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]);
   4.314 -  in thm end
   4.315 -  | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]);
   4.316 -
   4.317 -in
   4.318 -(* During proof of theorems produced by record_simproc you can end up in
   4.319 - * situations like "!!f ... . ... f r ..." where f is an extension update function.
   4.320 - * In order to split "f r" we transform this to "!!r ... . ... r ..." so that the
   4.321 - * usual split rules for extensions can apply.
   4.322 - *)
   4.323 -val record_split_f_more_simproc =
   4.324 -  Simplifier.simproc @{theory HOL} "record_split_f_more_simp" ["x"]
   4.325 -    (fn thy => fn _ => fn t =>
   4.326 -      (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$
   4.327 -                  (trm as Abs _) =>
   4.328 -         (case rec_id (~1) T of
   4.329 -            "" => NONE
   4.330 -          | n => if T=T'
   4.331 -                 then (let
   4.332 -                        val P=cterm_of thy (abstract_over_fun_app trm);
   4.333 -                        val thm = mk_fun_apply_eq trm thy;
   4.334 -                        val PV = cterm_of thy (hd (OldTerm.term_vars (prop_of thm)));
   4.335 -                        val thm' = cterm_instantiate [(PV,P)] thm;
   4.336 -                       in SOME  thm' end handle TERM _ => NONE)
   4.337 -                else NONE)
   4.338 -       | _ => NONE))
   4.339 -end
   4.340 -
   4.341 -fun prove_split_simp thy ss T prop =
   4.342 -  let
   4.343 -    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get thy;
   4.344 -    val extsplits =
   4.345 -            Library.foldl (fn (thms,(n,_)) => the_list (Symtab.lookup extsplit n) @ thms)
   4.346 -                    ([],dest_recTs T);
   4.347 -    val thms = (case get_splits thy (rec_id (~1) T) of
   4.348 -                   SOME (all_thm,_,_,_) =>
   4.349 -                     all_thm::(case extsplits of [thm] => [] | _ => extsplits)
   4.350 -                              (* [thm] is the same as all_thm *)
   4.351 -                 | NONE => extsplits)
   4.352 -    val thms'=K_comp_convs@thms;
   4.353 -    val ss' = (Simplifier.inherit_context ss simpset
   4.354 -                addsimps thms'
   4.355 -                addsimprocs [record_split_f_more_simproc]);
   4.356 +    val defset = get_sel_upd_defs thy;
   4.357 +    val intros = IsTupleSupport.get_istuple_intros thy;
   4.358 +    val in_tac = IsTupleSupport.resolve_from_tagged_net intros;
   4.359 +    val prop'  = Envir.beta_eta_contract prop;
   4.360 +    val (lhs, rhs)   = Logic.dest_equals (Logic.strip_assums_concl prop');
   4.361 +    val (head, args) = strip_comb lhs;
   4.362 +    val simps        = if length args = 1
   4.363 +                       then get_accupd_simps thy lhs defset in_tac
   4.364 +                       else get_updupd_simps thy lhs defset in_tac;
   4.365    in
   4.366 -    quick_and_dirty_prove true thy [] prop (fn _ => simp_tac ss' 1)
   4.367 +    Goal.prove (ProofContext.init thy) [] [] prop' (fn prems =>
   4.368 +              simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1
   4.369 +         THEN TRY (simp_tac (HOL_basic_ss addsimps ex_simps
   4.370 +                                          addsimprocs ex_simprs) 1))
   4.371    end;
   4.372  
   4.373  
   4.374 @@ -984,21 +1055,6 @@
   4.375       if null (loose_bnos t) then ((n,kT),(Abs (x,xT,Bound (i+1)))) else ((n,T),b)
   4.376    | K_skeleton n T b _ = ((n,T),b);
   4.377  
   4.378 -(*
   4.379 -fun K_skeleton n _ b ((K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_) = 
   4.380 -      ((n,kT),K_rec$b)
   4.381 -  | K_skeleton n _ (Bound i) 
   4.382 -      (Abs (x,T,(K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_$Bound 0)) =
   4.383 -        ((n,kT),Abs (x,T,(K_rec$Bound (i+1)$Bound 0)))
   4.384 -  | K_skeleton n T b  _ = ((n,T),b);
   4.385 - *)
   4.386 -
   4.387 -fun normalize_rhs thm =
   4.388 -  let
   4.389 -     val ss = HOL_basic_ss addsimps K_comp_convs; 
   4.390 -     val rhs = thm |> Thm.cprop_of |> Thm.dest_comb |> snd;
   4.391 -     val rhs' = (Simplifier.rewrite ss rhs);
   4.392 -  in Thm.transitive thm rhs' end;
   4.393  in
   4.394  (* record_simproc *)
   4.395  (* Simplifies selections of an record update:
   4.396 @@ -1044,7 +1100,7 @@
   4.397                               else (case mk_eq_terms r of
   4.398                                       SOME (trm,trm',vars)
   4.399                                       => let
   4.400 -                                          val (kv,kb) = 
   4.401 +                                          val (kv,kb) =
   4.402                                                   K_skeleton "k" kT (Bound (length vars)) k;
   4.403                                          in SOME (upd$kb$trm,trm',kv::vars) end
   4.404                                     | NONE
   4.405 @@ -1057,150 +1113,140 @@
   4.406              in
   4.407                (case mk_eq_terms (upd$k$r) of
   4.408                   SOME (trm,trm',vars)
   4.409 -                 => SOME (prove_split_simp thy ss domS
   4.410 -                                 (list_all(vars, Logic.mk_equals (sel $ trm, trm'))))
   4.411 +                 => SOME (prove_unfold_defs thy ss domS [] []
   4.412 +                             (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
   4.413                 | NONE => NONE)
   4.414              end
   4.415            | NONE => NONE)
   4.416          else NONE
   4.417        | _ => NONE));
   4.418  
   4.419 +fun get_upd_acc_cong_thm upd acc thy simpset = let
   4.420 +    val intros = IsTupleSupport.get_istuple_intros thy;
   4.421 +    val in_tac = IsTupleSupport.resolve_from_tagged_net intros;
   4.422 +
   4.423 +    val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]
   4.424 +    val prop  = concl_of (named_cterm_instantiate insts updacc_cong_triv);
   4.425 +  in Goal.prove (ProofContext.init thy) [] [] prop (fn prems =>
   4.426 +        EVERY [simp_tac simpset 1,
   4.427 +               REPEAT_DETERM (in_tac 1),
   4.428 +               TRY (resolve_tac [updacc_cong_idI] 1)])
   4.429 +  end;
   4.430 +
   4.431  (* record_upd_simproc *)
   4.432  (* simplify multiple updates:
   4.433   *  (1)  "N_update y (M_update g (N_update x (M_update f r))) =
   4.434            (N_update (y o x) (M_update (g o f) r))"
   4.435   *  (2)  "r(|M:= M r|) = r"
   4.436 - * For (2) special care of "more" updates has to be taken:
   4.437 - *    r(|more := m; A := A r|)
   4.438 - * If A is contained in the fields of m we cannot remove the update A := A r!
   4.439 - * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|)
   4.440 + * In both cases "more" updates complicate matters: for this reason
   4.441 + * we omit considering further updates if doing so would introduce
   4.442 + * both a more update and an update to a field within it.
   4.443  *)
   4.444  val record_upd_simproc =
   4.445    Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
   4.446      (fn thy => fn ss => fn t =>
   4.447 -      (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
   4.448 -         let datatype ('a,'b) calc = Init of 'b | Inter of 'a
   4.449 -             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy;
   4.450 -
   4.451 -             (*fun mk_abs_var x t = (x, fastype_of t);*)
   4.452 -             fun sel_name u = Long_Name.base_name (unsuffix updateN u);
   4.453 -
   4.454 -             fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
   4.455 -                  if has_field extfields s (domain_type' mT) then upd else seed s r
   4.456 -               | seed _ r = r;
   4.457 -
   4.458 -             fun grow u uT k kT vars (sprout,skeleton) =
   4.459 -                   if sel_name u = moreN
   4.460 -                   then let val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k;
   4.461 -                        in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end
   4.462 -                   else ((sprout,skeleton),vars);
   4.463 -
   4.464 -
   4.465 -             fun dest_k (Abs (x,T,((sel as Const (s,_))$r))) =
   4.466 -                  if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE
   4.467 -               | dest_k (Abs (_,_,(Abs (x,T,((sel as Const (s,_))$r)))$Bound 0)) =
   4.468 -                  (* eta expanded variant *)
   4.469 -                  if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE
   4.470 -               | dest_k _ = NONE;
   4.471 -
   4.472 -             fun is_upd_same (sprout,skeleton) u k =
   4.473 -               (case dest_k k of SOME (x,T,sel,s,r) =>
   4.474 -                   if (unsuffix updateN u) = s andalso (seed s sprout) = r
   4.475 -                   then SOME (fn t => Abs (x,T,incr_boundvars 1 t),sel,seed s skeleton)
   4.476 -                   else NONE
   4.477 -                | NONE => NONE);
   4.478 -
   4.479 -             fun init_seed r = ((r,Bound 0), [("r", rT)]);
   4.480 -
   4.481 -             fun add (n:string) f fmaps =
   4.482 -               (case AList.lookup (op =) fmaps n of
   4.483 -                  NONE => AList.update (op =) (n,[f]) fmaps
   4.484 -                | SOME fs => AList.update (op =) (n,f::fs) fmaps)
   4.485 -
   4.486 -             fun comps (n:string) T fmaps =
   4.487 -               (case AList.lookup (op =) fmaps n of
   4.488 -                 SOME fs =>
   4.489 -                   foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs
   4.490 -                | NONE => error ("record_upd_simproc.comps"))
   4.491 -
   4.492 -             (* mk_updterm returns either
   4.493 -              *  - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made,
   4.494 -              *     where vars are the bound variables in the skeleton
   4.495 -              *  - Inter (orig-term-skeleton,simplified-term-skeleton,
   4.496 -              *           vars, (term-sprout, skeleton-sprout))
   4.497 -              *     where "All vars. orig-term-skeleton = simplified-term-skeleton" is
   4.498 -              *     the desired simplification rule,
   4.499 -              *     the sprouts accumulate the "more-updates" on the way from the seed
   4.500 -              *     to the outermost update. It is only relevant to calculate the
   4.501 -              *     possible simplification for (2)
   4.502 -              * The algorithm first walks down the updates to the seed-record while
   4.503 -              * memorising the updates in the already-table. While walking up the
   4.504 -              * updates again, the optimised term is constructed.
   4.505 -              *)
   4.506 -             fun mk_updterm upds already
   4.507 -                 (t as ((upd as Const (u,uT as (Type (_,[kT,_])))) $ k $ r)) =
   4.508 -                 if Symtab.defined upds u
   4.509 -                 then let
   4.510 -                         fun rest already = mk_updterm upds already
   4.511 -                      in if u mem_string already
   4.512 -                         then (case (rest already r) of
   4.513 -                                 Init ((sprout,skel),vars) =>
   4.514 -                                 let
   4.515 -                                   val n = sel_name u;
   4.516 -                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   4.517 -                                   val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel);
   4.518 -                                 in Inter (upd$kb$skel,skel,vars',add n kb [],sprout') end
   4.519 -                               | Inter (trm,trm',vars,fmaps,sprout) =>
   4.520 -                                 let
   4.521 -                                   val n = sel_name u;
   4.522 -                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   4.523 -                                   val (sprout',vars') = grow u uT k kT (kv::vars) sprout;
   4.524 -                                 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout')
   4.525 -                                 end)
   4.526 -                         else
   4.527 -                          (case rest (u::already) r of
   4.528 -                             Init ((sprout,skel),vars) =>
   4.529 -                              (case is_upd_same (sprout,skel) u k of
   4.530 -                                 SOME (K_rec,sel,skel') =>
   4.531 -                                 let
   4.532 -                                   val (sprout',vars') = grow u uT k kT vars (sprout,skel);
   4.533 -                                  in Inter(upd$(K_rec (sel$skel'))$skel,skel,vars',[],sprout')
   4.534 -                                  end
   4.535 -                               | NONE =>
   4.536 -                                 let
   4.537 -                                   val n = sel_name u;
   4.538 -                                   val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   4.539 -                                 in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end)
   4.540 -                           | Inter (trm,trm',vars,fmaps,sprout) =>
   4.541 -                               (case is_upd_same sprout u k of
   4.542 -                                  SOME (K_rec,sel,skel) =>
   4.543 -                                  let
   4.544 -                                    val (sprout',vars') = grow u uT k kT vars sprout
   4.545 -                                  in Inter(upd$(K_rec (sel$skel))$trm,trm',vars',fmaps,sprout')
   4.546 -                                  end
   4.547 -                                | NONE =>
   4.548 -                                  let
   4.549 -                                    val n = sel_name u
   4.550 -                                    val T = domain_type kT
   4.551 -                                    val (kv,kb) = K_skeleton n kT (Bound (length vars)) k;
   4.552 -                                    val (sprout',vars') = grow u uT k kT (kv::vars) sprout
   4.553 -                                    val fmaps' = add n kb fmaps
   4.554 -                                  in Inter (upd$kb$trm,upd$comps n T fmaps'$trm'
   4.555 -                                           ,vars',fmaps',sprout') end))
   4.556 -                     end
   4.557 -                 else Init (init_seed t)
   4.558 -               | mk_updterm _ _ t = Init (init_seed t);
   4.559 -
   4.560 -         in (case mk_updterm updates [] t of
   4.561 -               Inter (trm,trm',vars,_,_)
   4.562 -                => SOME (normalize_rhs 
   4.563 -                          (prove_split_simp thy ss rT
   4.564 -                            (list_all(vars, Logic.mk_equals (trm, trm')))))
   4.565 -             | _ => NONE)
   4.566 -         end
   4.567 -       | _ => NONE))
   4.568 +      let
   4.569 +        (* we can use more-updators with other updators as long
   4.570 +           as none of the other updators go deeper than any more
   4.571 +           updator. min here is the depth of the deepest other
   4.572 +           updator, max the depth of the shallowest more updator *)
   4.573 +        fun include_depth (dep, true) (min, max) =
   4.574 +          if (min <= dep)
   4.575 +          then SOME (min, if dep <= max orelse max = ~1 then dep else max)
   4.576 +          else NONE
   4.577 +          | include_depth (dep, false) (min, max) =
   4.578 +          if (dep <= max orelse max = ~1)
   4.579 +          then SOME (if min <= dep then dep else min, max)
   4.580 +          else NONE;
   4.581 +
   4.582 +        fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max =
   4.583 +            (case get_update_details u thy of
   4.584 +              SOME (s, dep, ismore) =>
   4.585 +                (case include_depth (dep, ismore) (min, max) of
   4.586 +                  SOME (min', max') => let
   4.587 +                        val (us, bs, _) = getupdseq tm min' max';
   4.588 +                      in ((upd, s, f) :: us, bs, fastype_of term) end
   4.589 +                | NONE => ([], term, HOLogic.unitT))
   4.590 +            | NONE => ([], term, HOLogic.unitT))
   4.591 +          | getupdseq term _ _ = ([], term, HOLogic.unitT);
   4.592 +
   4.593 +        val (upds, base, baseT) = getupdseq t 0 ~1;
   4.594 +
   4.595 +        fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm =
   4.596 +            if s = s' andalso null (loose_bnos tm')
   4.597 +              andalso subst_bound (HOLogic.unit, tm') = tm
   4.598 +            then (true, Abs (n, T, Const (s', T') $ Bound 1))
   4.599 +            else (false, HOLogic.unit)
   4.600 +          | is_upd_noop s f tm = (false, HOLogic.unit);
   4.601 +
   4.602 +        fun get_noop_simps (upd as Const (u, T))
   4.603 +                      (f as Abs (n, T', (acc as Const (s, T'')) $ _)) = let
   4.604 +
   4.605 +            val ss    = get_sel_upd_defs thy;
   4.606 +            val uathm = get_upd_acc_cong_thm upd acc thy ss;
   4.607 +          in [standard (uathm RS updacc_noopE),
   4.608 +              standard (uathm RS updacc_noop_compE)] end;
   4.609 +
   4.610 +        (* if f is constant then (f o g) = f. we know that K_skeleton
   4.611 +           only returns constant abstractions thus when we see an
   4.612 +           abstraction we can discard inner updates. *)
   4.613 +        fun add_upd (f as Abs _) fs = [f]
   4.614 +          | add_upd f fs = (f :: fs);
   4.615 +
   4.616 +        (* mk_updterm returns
   4.617 +         * (orig-term-skeleton, simplified-skeleton,
   4.618 +         *  variables, duplicate-updates, simp-flag, noop-simps)
   4.619 +         *
   4.620 +         *  where duplicate-updates is a table used to pass upward
   4.621 +         *  the list of update functions which can be composed
   4.622 +         *  into an update above them, simp-flag indicates whether
   4.623 +         *  any simplification was achieved, and noop-simps are
   4.624 +         *  used for eliminating case (2) defined above
   4.625 +         *)
   4.626 +        fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = let
   4.627 +            val (lhs, rhs, vars, dups, simp, noops) =
   4.628 +                  mk_updterm upds (Symtab.update (u, ()) above) term;
   4.629 +            val (fvar, skelf) = K_skeleton (Sign.base_name s) (domain_type T)
   4.630 +                                      (Bound (length vars)) f;
   4.631 +            val (isnoop, skelf') = is_upd_noop s f term;
   4.632 +            val funT  = domain_type T;
   4.633 +            fun mk_comp_local (f, f') =
   4.634 +              Const ("Fun.comp", funT --> funT --> funT) $ f $ f';
   4.635 +          in if isnoop
   4.636 +              then (upd $ skelf' $ lhs, rhs, vars,
   4.637 +                    Symtab.update (u, []) dups, true,
   4.638 +                    if Symtab.defined noops u then noops
   4.639 +                    else Symtab.update (u, get_noop_simps upd skelf') noops)
   4.640 +            else if Symtab.defined above u
   4.641 +              then (upd $ skelf $ lhs, rhs, fvar :: vars,
   4.642 +                    Symtab.map_default (u, []) (add_upd skelf) dups,
   4.643 +                    true, noops)
   4.644 +            else case Symtab.lookup dups u of
   4.645 +              SOME fs =>
   4.646 +                   (upd $ skelf $ lhs,
   4.647 +                    upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
   4.648 +                    fvar :: vars, dups, true, noops)
   4.649 +            | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs,
   4.650 +                       fvar :: vars, dups, simp, noops)
   4.651 +          end
   4.652 +          | mk_updterm [] above term = (Bound 0, Bound 0, [("r", baseT)],
   4.653 +                                          Symtab.empty, false, Symtab.empty)
   4.654 +          | mk_updterm us above term = raise TERM ("mk_updterm match",
   4.655 +                                              map (fn (x, y, z) => x) us);
   4.656 +
   4.657 +        val (lhs, rhs, vars, dups, simp, noops)
   4.658 +                  = mk_updterm upds Symtab.empty base;
   4.659 +        val noops' = flat (map snd (Symtab.dest noops));
   4.660 +      in
   4.661 +        if simp then
   4.662 +           SOME (prove_unfold_defs thy ss baseT noops' [record_simproc]
   4.663 +                             (list_all(vars,(equals baseT$lhs$rhs))))
   4.664 +        else NONE
   4.665 +      end)
   4.666 +
   4.667  end
   4.668  
   4.669 +
   4.670  (* record_eq_simproc *)
   4.671  (* looks up the most specific record-equality.
   4.672   * Note on efficiency:
   4.673 @@ -1467,28 +1513,6 @@
   4.674                  i st)) (st,((length params) - 1) downto 0))
   4.675    end;
   4.676  
   4.677 -fun extension_typedef name repT alphas thy =
   4.678 -  let
   4.679 -    fun get_thms thy name =
   4.680 -      let
   4.681 -        val SOME { Abs_induct = abs_induct,
   4.682 -          Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name;
   4.683 -        val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
   4.684 -      in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
   4.685 -    val tname = Binding.name (Long_Name.base_name name);
   4.686 -  in
   4.687 -    thy
   4.688 -    |> Typecopy.typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
   4.689 -    |-> (fn (name, _) => `(fn thy => get_thms thy name))
   4.690 -  end;
   4.691 -
   4.692 -fun mixit convs refls =
   4.693 -  let
   4.694 -    fun f ((res,lhs,rhs),refl) =
   4.695 -      ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs);
   4.696 -  in #1 (Library.foldl f (([],[],convs),refls)) end;
   4.697 -
   4.698 -
   4.699  fun extension_definition full name fields names alphas zeta moreT more vars thy =
   4.700    let
   4.701      val base = Long_Name.base_name;
   4.702 @@ -1498,7 +1522,6 @@
   4.703      val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
   4.704      val extT_name = suffix ext_typeN name
   4.705      val extT = Type (extT_name, alphas_zetaTs);
   4.706 -    val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]);
   4.707      val fields_more = fields@[(full moreN,moreT)];
   4.708      val fields_moreTs = fieldTs@[moreT];
   4.709      val bfields_more = map (apfst base) fields_more;
   4.710 @@ -1506,61 +1529,97 @@
   4.711      val len = length fields;
   4.712      val idxms = 0 upto len;
   4.713  
   4.714 +    (* before doing anything else, create the tree of new types
   4.715 +       that will back the record extension *)
   4.716 +    
   4.717 +    fun mktreeT [] = raise (TYPE ("mktreeT: empty list", [], []))
   4.718 +      | mktreeT [T] = T
   4.719 +      | mktreeT xs =
   4.720 +    let
   4.721 +      val len   = length xs;
   4.722 +      val half  = len div 2;
   4.723 +      val left  = List.take (xs, half);
   4.724 +      val right = List.drop (xs, half);
   4.725 +    in
   4.726 +      HOLogic.mk_prodT (mktreeT left, mktreeT right)
   4.727 +    end;
   4.728 +
   4.729 +    fun mktreeV [] = raise (TYPE ("mktreeV: empty list", [], []))
   4.730 +      | mktreeV [T] = T
   4.731 +      | mktreeV xs =
   4.732 +    let
   4.733 +      val len   = length xs;
   4.734 +      val half  = len div 2;
   4.735 +      val left  = List.take (xs, half);
   4.736 +      val right = List.drop (xs, half);
   4.737 +    in
   4.738 +      HOLogic.mk_prod (mktreeV left, mktreeV right)
   4.739 +    end;
   4.740 +
   4.741 +    fun mk_istuple ((thy, i), (left, rght)) =
   4.742 +    let
   4.743 +      val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i);
   4.744 +      val nm   = suffix suff (Sign.base_name name);
   4.745 +      val (cons, thy') = IsTupleSupport.add_istuple_type
   4.746 +               (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
   4.747 +    in
   4.748 +      ((thy', i + 1), cons $ left $ rght)
   4.749 +    end;
   4.750 +
   4.751 +    (* trying to create a 1-element istuple will fail, and
   4.752 +       is pointless anyway *)
   4.753 +    fun mk_even_istuple ((thy, i), [arg]) =
   4.754 +        ((thy, i), arg)
   4.755 +      | mk_even_istuple ((thy, i), args) =
   4.756 +        mk_istuple ((thy, i), HOLogic.dest_prod (mktreeV args));
   4.757 +
   4.758 +    fun build_meta_tree_type i thy vars more =
   4.759 +    let
   4.760 +      val len   = length vars;
   4.761 +    in
   4.762 +      if len < 1
   4.763 +      then raise (TYPE ("meta_tree_type args too short", [], vars))
   4.764 +      else if len > 16
   4.765 +      then let
   4.766 +          fun group16 [] = []
   4.767 +            | group16 xs = Library.take (16, xs)
   4.768 +                             :: group16 (Library.drop (16, xs));
   4.769 +          val vars' = group16 vars;
   4.770 +          val ((thy', i'), composites) =
   4.771 +                   foldl_map mk_even_istuple ((thy, i), vars');
   4.772 +        in
   4.773 +          build_meta_tree_type i' thy' composites more
   4.774 +        end
   4.775 +      else let
   4.776 +          val ((thy', i'), term)
   4.777 +             = mk_istuple ((thy, 0), (mktreeV vars, more));
   4.778 +        in
   4.779 +          (term, thy')
   4.780 +        end
   4.781 +    end;
   4.782 +
   4.783 +    val _ = timing_msg "record extension preparing definitions";
   4.784 +
   4.785 +    (* 1st stage part 1: introduce the tree of new types *)
   4.786 +    fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
   4.787 +    val (ext_body, typ_thy) =
   4.788 +      timeit_msg "record extension nested type def:" get_meta_tree;
   4.789 +
   4.790      (* prepare declarations and definitions *)
   4.791  
   4.792      (*fields constructor*)
   4.793      val ext_decl = (mk_extC (name,extT) fields_moreTs);
   4.794 -    (*
   4.795 -    val ext_spec = Const ext_decl :==
   4.796 -         (foldr (uncurry lambda)
   4.797 -            (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more]))
   4.798 -    *)
   4.799 -    val ext_spec = list_comb (Const ext_decl,vars@[more]) :==
   4.800 -         (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more])));
   4.801 +    val ext_spec = list_comb (Const ext_decl,vars@[more]) :== ext_body;
   4.802  
   4.803      fun mk_ext args = list_comb (Const ext_decl, args);
   4.804  
   4.805 -    (*destructors*)
   4.806 -    val _ = timing_msg "record extension preparing definitions";
   4.807 -    val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more;
   4.808 -
   4.809 -    fun mk_dest_spec (i, (c,T)) =
   4.810 -      let val snds = (funpow i HOLogic.mk_snd (mk_Rep name repT extT $ r))
   4.811 -      in Const (mk_selC extT (suffix ext_dest c,T))
   4.812 -         :== (lambda r (if i=len then snds else HOLogic.mk_fst snds))
   4.813 -      end;
   4.814 -    val dest_specs =
   4.815 -      ListPair.map mk_dest_spec (idxms, fields_more);
   4.816 -
   4.817 -    (*updates*)
   4.818 -    val upd_decls = map (mk_updC updN extT) bfields_more;
   4.819 -    fun mk_upd_spec (c,T) =
   4.820 -      let
   4.821 -        val args = map (fn (n,nT) => if n=c then Free (base c,T --> T)$
   4.822 -                                                  (mk_sel r (suffix ext_dest n,nT))
   4.823 -                                     else (mk_sel r (suffix ext_dest n,nT)))
   4.824 -                       fields_more;
   4.825 -      in Const (mk_updC updN extT (c,T))$(Free (base c,T --> T))$r
   4.826 -          :== mk_ext args
   4.827 -      end;
   4.828 -    val upd_specs = map mk_upd_spec fields_more;
   4.829 -
   4.830 -    (* 1st stage: defs_thy *)
   4.831 +    (* 1st stage part 2: define the ext constant *)
   4.832      fun mk_defs () =
   4.833 -      thy
   4.834 -      |> extension_typedef name repT (alphas @ [zeta])
   4.835 -      ||> Sign.add_consts_i
   4.836 -            (map (Syntax.no_syn o apfst Binding.name) (apfst base ext_decl :: dest_decls @ upd_decls))
   4.837 -      ||>> PureThy.add_defs false
   4.838 -            (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
   4.839 -      ||>> PureThy.add_defs false
   4.840 -            (map (Thm.no_attributes o apfst Binding.name) upd_specs)
   4.841 -      |-> (fn args as ((_, dest_defs), upd_defs) =>
   4.842 -          fold Code.add_default_eqn dest_defs
   4.843 -          #> fold Code.add_default_eqn upd_defs
   4.844 -          #> pair args);
   4.845 -    val ((([abs_inject, abs_inverse, abs_induct], ext_def :: dest_defs), upd_defs), defs_thy) =
   4.846 -      timeit_msg "record extension type/selector/update defs:" mk_defs;
   4.847 +      typ_thy
   4.848 +      |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)]
   4.849 +      |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name ext_spec)]
   4.850 +    val ([ext_def], defs_thy) =
   4.851 +      timeit_msg "record extension constructor def:" mk_defs;
   4.852  
   4.853      (* prepare propositions *)
   4.854      val _ = timing_msg "record extension preparing propositions";
   4.855 @@ -1572,14 +1631,17 @@
   4.856      val w     = Free (wN, extT);
   4.857      val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
   4.858      val C = Free (Name.variant variants "C", HOLogic.boolT);
   4.859 +    val intros = IsTupleSupport.get_istuple_intros defs_thy;
   4.860 +    val intros_tac = IsTupleSupport.resolve_from_tagged_net intros;
   4.861  
   4.862      val inject_prop =
   4.863        let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
   4.864 -      in All (map dest_Free (vars_more@vars_more'))
   4.865 -          ((HOLogic.eq_const extT $
   4.866 -            mk_ext vars_more$mk_ext vars_more')
   4.867 -           ===
   4.868 -           foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more')))
   4.869 +      in
   4.870 +        ((HOLogic.mk_conj (HOLogic.eq_const extT $
   4.871 +          mk_ext vars_more$mk_ext vars_more', HOLogic.true_const))
   4.872 +         ===
   4.873 +         foldr1 HOLogic.mk_conj
   4.874 +           (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const]))
   4.875        end;
   4.876  
   4.877      val induct_prop =
   4.878 @@ -1590,22 +1652,6 @@
   4.879          (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C))
   4.880        ==> Trueprop C;
   4.881  
   4.882 -    (*destructors*)
   4.883 -    val dest_conv_props =
   4.884 -       map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
   4.885 -
   4.886 -    (*updates*)
   4.887 -    fun mk_upd_prop (i,(c,T)) =
   4.888 -      let val x' = Free (Name.variant variants (base c ^ "'"),T --> T)
   4.889 -          val args' = nth_map i  (K (x'$nth vars_more i)) vars_more
   4.890 -      in mk_upd updN c x' ext === mk_ext args'  end;
   4.891 -    val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
   4.892 -
   4.893 -    val surjective_prop =
   4.894 -      let val args =
   4.895 -           map (fn (c, Free (_,T)) => mk_sel s (suffix ext_dest c,T)) named_vars_more;
   4.896 -      in s === mk_ext args end;
   4.897 -
   4.898      val split_meta_prop =
   4.899        let val P = Free (Name.variant variants "P", extT-->Term.propT) in
   4.900          Logic.mk_equals
   4.901 @@ -1618,110 +1664,65 @@
   4.902        let val tac = simp_all_tac HOL_ss simps
   4.903        in fn prop => prove stndrd [] prop (K tac) end;
   4.904  
   4.905 -    fun inject_prf () = (prove_simp true [ext_def,abs_inject,Pair_eq] inject_prop);
   4.906 +    fun inject_prf () =
   4.907 +      simplify HOL_ss (
   4.908 +        prove_standard [] inject_prop (fn prems =>
   4.909 +           EVERY [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
   4.910 +                  REPEAT_DETERM (resolve_tac [refl_conj_eq] 1
   4.911 +                                  ORELSE intros_tac 1
   4.912 +                                  ORELSE resolve_tac [refl] 1)]));
   4.913 +
   4.914      val inject = timeit_msg "record extension inject proof:" inject_prf;
   4.915  
   4.916 +    (* We need a surjection property r = (| f = f r, g = g r ... |)
   4.917 +       to prove other theorems. We haven't given names to the accessors
   4.918 +       f, g etc yet however, so we generate an ext structure with
   4.919 +       free variables as all arguments and allow the introduction tactic to
   4.920 +       operate on it as far as it can. We then use standard to convert
   4.921 +       the free variables into unifiable variables and unify them with
   4.922 +       (roughly) the definition of the accessor. *)
   4.923 +    fun surject_prf () = let
   4.924 +        val cterm_ext = cterm_of defs_thy ext;
   4.925 +        val start     = named_cterm_instantiate [("y", cterm_ext)]
   4.926 +                              surject_assist_idE;
   4.927 +        val tactic1   = simp_tac (HOL_basic_ss addsimps [ext_def]) 1
   4.928 +                        THEN REPEAT_ALL_NEW intros_tac 1
   4.929 +        val tactic2   = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   4.930 +        val [halfway] = Seq.list_of (tactic1 start);
   4.931 +        val [surject] = Seq.list_of (tactic2 (standard halfway));
   4.932 +      in
   4.933 +        surject
   4.934 +      end;
   4.935 +    val surject = timeit_msg "record extension surjective proof:" surject_prf;
   4.936 +
   4.937 +    fun split_meta_prf () =
   4.938 +        prove_standard [] split_meta_prop (fn prems =>
   4.939 +         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
   4.940 +                etac meta_allE 1, atac 1,
   4.941 +                rtac (prop_subst OF [surject]) 1,
   4.942 +                REPEAT (etac meta_allE 1), atac 1]);
   4.943 +    val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
   4.944 +
   4.945      fun induct_prf () =
   4.946        let val (assm, concl) = induct_prop
   4.947        in prove_standard [assm] concl (fn {prems, ...} =>
   4.948 -           EVERY [try_param_tac rN abs_induct 1,
   4.949 -                  simp_tac (HOL_ss addsimps [split_paired_all]) 1,
   4.950 -                  resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
   4.951 -      end;
   4.952 +           EVERY [cut_rules_tac [split_meta RS meta_iffD2] 1,
   4.953 +                  resolve_tac prems 2,
   4.954 +                  asm_simp_tac HOL_ss 1]) end;
   4.955      val induct = timeit_msg "record extension induct proof:" induct_prf;
   4.956  
   4.957 -    fun cases_prf_opt () =
   4.958 -      let
   4.959 -        val (_$(Pvar$_)) = concl_of induct;
   4.960 -        val ind = cterm_instantiate
   4.961 -                    [(cterm_of defs_thy Pvar, cterm_of defs_thy
   4.962 -                            (lambda w (HOLogic.imp$HOLogic.mk_eq(r,w)$C)))]
   4.963 -                    induct;
   4.964 -        in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
   4.965 -
   4.966 -    fun cases_prf_noopt () =
   4.967 -        prove_standard [] cases_prop (fn _ =>
   4.968 -         EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
   4.969 -                try_param_tac rN induct 1,
   4.970 -                rtac impI 1,
   4.971 -                REPEAT (etac allE 1),
   4.972 -                etac mp 1,
   4.973 -                rtac refl 1])
   4.974 -
   4.975 -    val cases_prf = quick_and_dirty_prf cases_prf_noopt cases_prf_opt;
   4.976 -    val cases = timeit_msg "record extension cases proof:" cases_prf;
   4.977 -
   4.978 -    fun dest_convs_prf () = map (prove_simp false
   4.979 -                      ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
   4.980 -    val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf;
   4.981 -    fun dest_convs_standard_prf () = map standard dest_convs;
   4.982 -
   4.983 -    val dest_convs_standard =
   4.984 -        timeit_msg "record extension dest_convs_standard proof:" dest_convs_standard_prf;
   4.985 -
   4.986 -    fun upd_convs_prf_noopt () = map (prove_simp true (dest_convs_standard@upd_defs))
   4.987 -                                       upd_conv_props;
   4.988 -    fun upd_convs_prf_opt () =
   4.989 -      let
   4.990 -
   4.991 -        fun mkrefl (c,T) = Thm.reflexive
   4.992 -                    (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T-->T)));
   4.993 -        val refls = map mkrefl fields_more;
   4.994 -        val dest_convs' = map mk_meta_eq dest_convs;
   4.995 -        val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs');
   4.996 -
   4.997 -        val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
   4.998 -
   4.999 -        fun mkthm (udef,(fld_refl,thms)) =
  4.1000 -          let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms);
  4.1001 -               (* (|N=N (|N=N,M=M,K=K,more=more|)
  4.1002 -                    M=M (|N=N,M=M,K=K,more=more|)
  4.1003 -                    K=K'
  4.1004 -                    more = more (|N=N,M=M,K=K,more=more|) =
  4.1005 -                  (|N=N,M=M,K=K',more=more|)
  4.1006 -                *)
  4.1007 -              val (_$(_$v$r)$_) = prop_of udef;
  4.1008 -              val (_$(v'$_)$_) = prop_of fld_refl;
  4.1009 -              val udef' = cterm_instantiate
  4.1010 -                            [(cterm_of defs_thy v,cterm_of defs_thy v'),
  4.1011 -                             (cterm_of defs_thy r,cterm_of defs_thy ext)] udef;
  4.1012 -          in  standard (Thm.transitive udef' bdyeq) end;
  4.1013 -      in map mkthm (rev upd_defs  ~~ (mixit dest_convs' map_eqs)) end;
  4.1014 -
  4.1015 -    val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt;
  4.1016 -
  4.1017 -    val upd_convs =
  4.1018 -         timeit_msg "record extension upd_convs proof:" upd_convs_prf;
  4.1019 -
  4.1020 -    fun surjective_prf () =
  4.1021 -      prove_standard [] surjective_prop (fn _ =>
  4.1022 -          (EVERY [try_param_tac rN induct 1,
  4.1023 -                  simp_tac (HOL_basic_ss addsimps dest_convs_standard) 1]));
  4.1024 -    val surjective = timeit_msg "record extension surjective proof:" surjective_prf;
  4.1025 -
  4.1026 -    fun split_meta_prf () =
  4.1027 -        prove_standard [] split_meta_prop (fn _ =>
  4.1028 -         EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  4.1029 -                etac meta_allE 1, atac 1,
  4.1030 -                rtac (prop_subst OF [surjective]) 1,
  4.1031 -                REPEAT (etac meta_allE 1), atac 1]);
  4.1032 -    val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
  4.1033 -
  4.1034 -
  4.1035 -    val (([inject',induct',cases',surjective',split_meta'],
  4.1036 +    val (([inject',induct',surjective',split_meta',ext_def'],
  4.1037            [dest_convs',upd_convs']),
  4.1038        thm_thy) =
  4.1039        defs_thy
  4.1040        |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
  4.1041             [("ext_inject", inject),
  4.1042              ("ext_induct", induct),
  4.1043 -            ("ext_cases", cases),
  4.1044              ("ext_surjective", surjective),
  4.1045 -            ("ext_split", split_meta)]
  4.1046 -      ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
  4.1047 -            [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)]
  4.1048 -
  4.1049 -  in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
  4.1050 +            ("ext_split", split_meta),
  4.1051 +            ("ext_def", ext_def)]
  4.1052 +
  4.1053 +  in (thm_thy,extT,induct',inject',split_meta',ext_def')
  4.1054    end;
  4.1055  
  4.1056  fun chunks []      []   = []
  4.1057 @@ -1826,7 +1827,7 @@
  4.1058      val all_named_vars_more = all_named_vars @ [(full_moreN,more)];
  4.1059  
  4.1060      (* 1st stage: extension_thy *)
  4.1061 -    val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split,u_convs) =
  4.1062 +    val (extension_thy,extT,ext_induct,ext_inject,ext_split,ext_def) =
  4.1063        thy
  4.1064        |> Sign.add_path bname
  4.1065        |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
  4.1066 @@ -1862,6 +1863,9 @@
  4.1067  
  4.1068      val r_rec0 = mk_rec all_vars_more 0;
  4.1069      val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
  4.1070 +    val r_rec0_Vars = let
  4.1071 +        fun to_Var (Free (c, T)) = Var ((c, 0), T);
  4.1072 +      in mk_rec (map to_Var all_vars_more) 0 end;
  4.1073  
  4.1074      fun r n = Free (rN, rec_schemeT n)
  4.1075      val r0 = r 0;
  4.1076 @@ -1916,21 +1920,63 @@
  4.1077        [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
  4.1078          (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
  4.1079  
  4.1080 +    val ext_defs = ext_def :: map #extdef parents;
  4.1081 +    val intros = IsTupleSupport.get_istuple_intros extension_thy;
  4.1082 +    val intros_tac = IsTupleSupport.resolve_from_tagged_net intros;
  4.1083 +
  4.1084 +    (* Theorems from the istuple intros.
  4.1085 +       This is complex enough to deserve a full comment.
  4.1086 +       By unfolding ext_defs from r_rec0 we create a tree of constructor
  4.1087 +       calls (many of them Pair, but others as well). The introduction
  4.1088 +       rules for update_accessor_eq_assist can unify two different ways
  4.1089 +       on these constructors. If we take the complete result sequence of
  4.1090 +       running a the introduction tactic, we get one theorem for each upd/acc
  4.1091 +       pair, from which we can derive the bodies of our selector and
  4.1092 +       updator and their convs. *)
  4.1093 +    fun get_access_update_thms () = let
  4.1094 +        val cterm_rec = cterm_of extension_thy r_rec0;
  4.1095 +        val cterm_vrs = cterm_of extension_thy r_rec0_Vars;
  4.1096 +        val insts     = [("v", cterm_rec), ("v'", cterm_vrs)];
  4.1097 +        val init_thm  = named_cterm_instantiate insts updacc_eq_triv;
  4.1098 +        val terminal  = rtac updacc_eq_idI 1 THEN rtac refl 1;
  4.1099 +        val tactic    = simp_tac (HOL_basic_ss addsimps ext_defs) 1
  4.1100 +                        THEN REPEAT (intros_tac 1 ORELSE terminal);
  4.1101 +        val updaccs   = Seq.list_of (tactic init_thm);
  4.1102 +      in
  4.1103 +        (updaccs RL [updacc_accessor_eqE],
  4.1104 +         updaccs RL [updacc_updator_eqE],
  4.1105 +         updaccs RL [updacc_cong_from_eq])
  4.1106 +      end;
  4.1107 +    val (accessor_thms, updator_thms, upd_acc_cong_assists) =
  4.1108 +       timeit_msg "record getting tree access/updates:" get_access_update_thms;
  4.1109 +
  4.1110 +    fun lastN xs = List.drop (xs, parent_fields_len);
  4.1111 +
  4.1112      (*selectors*)
  4.1113 -    fun mk_sel_spec (c,T) =
  4.1114 -         Const (mk_selC rec_schemeT0 (c,T))
  4.1115 -          :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0));
  4.1116 -    val sel_specs = map mk_sel_spec fields_more;
  4.1117 +    fun mk_sel_spec ((c,T), thm) =
  4.1118 +      let
  4.1119 +        val (acc $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
  4.1120 +                               o Envir.beta_eta_contract o concl_of) thm;
  4.1121 +        val _ = if (arg aconv r_rec0) then ()
  4.1122 +                else raise TERM ("mk_sel_spec: different arg", [arg]);
  4.1123 +      in
  4.1124 +        Const (mk_selC rec_schemeT0 (c,T))
  4.1125 +          :== acc
  4.1126 +      end;
  4.1127 +    val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
  4.1128  
  4.1129      (*updates*)
  4.1130  
  4.1131 -    fun mk_upd_spec (c,T) =
  4.1132 +    fun mk_upd_spec ((c,T), thm) =
  4.1133        let
  4.1134 -        val new = mk_upd' updN c (Free (base c,T-->T)) extT(*(parent_more r0)*);
  4.1135 -      in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T-->T))$r0
  4.1136 -          :== (parent_more_upd new r0)
  4.1137 +        val (upd $ _ $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
  4.1138 +                                   o Envir.beta_eta_contract o concl_of) thm;
  4.1139 +        val _ = if (arg aconv r_rec0) then ()
  4.1140 +                else raise TERM ("mk_sel_spec: different arg", [arg]);
  4.1141 +      in Const (mk_updC updateN rec_schemeT0 (c,T))
  4.1142 +          :== upd
  4.1143        end;
  4.1144 -    val upd_specs = map mk_upd_spec fields_more;
  4.1145 +    val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
  4.1146  
  4.1147      (*derived operations*)
  4.1148      val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
  4.1149 @@ -2052,16 +2098,26 @@
  4.1150      val ss = get_simpset defs_thy;
  4.1151  
  4.1152      fun sel_convs_prf () = map (prove_simp false ss
  4.1153 -                           (sel_defs@ext_dest_convs)) sel_conv_props;
  4.1154 +                           (sel_defs@accessor_thms)) sel_conv_props;
  4.1155      val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
  4.1156      fun sel_convs_standard_prf () = map standard sel_convs
  4.1157      val sel_convs_standard =
  4.1158            timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
  4.1159  
  4.1160 -    fun upd_convs_prf () =
  4.1161 -          map (prove_simp true ss (upd_defs@u_convs)) upd_conv_props;
  4.1162 -
  4.1163 +    fun upd_convs_prf () = map (prove_simp false ss
  4.1164 +                           (upd_defs@updator_thms)) upd_conv_props;
  4.1165      val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
  4.1166 +    fun upd_convs_standard_prf () = map standard upd_convs
  4.1167 +    val upd_convs_standard =
  4.1168 +          timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
  4.1169 +
  4.1170 +    fun get_upd_acc_congs () = let
  4.1171 +        val symdefs  = map symmetric (sel_defs @ upd_defs);
  4.1172 +        val fold_ss  = HOL_basic_ss addsimps symdefs;
  4.1173 +        val ua_congs = map (simplify fold_ss) upd_acc_cong_assists;
  4.1174 +      in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
  4.1175 +    val (fold_congs, unfold_congs) =
  4.1176 +          timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
  4.1177  
  4.1178      val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
  4.1179  
  4.1180 @@ -2114,14 +2170,31 @@
  4.1181          THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
  4.1182      val cases = timeit_msg "record cases proof:" cases_prf;
  4.1183  
  4.1184 +    fun surjective_prf () = let
  4.1185 +        val o_ass_thm = symmetric (mk_meta_eq o_assoc);
  4.1186 +        val o_reassoc = simplify (HOL_basic_ss addsimps [o_ass_thm]);
  4.1187 +        val sel_defs' = map o_reassoc sel_defs;
  4.1188 +        val ss        = HOL_basic_ss addsimps (ext_defs @ sel_defs');
  4.1189 +      in
  4.1190 +        prove_standard [] surjective_prop (fn prems =>
  4.1191 +            (EVERY [rtac surject_assist_idE 1,
  4.1192 +                    simp_tac ss 1,
  4.1193 +                    REPEAT (intros_tac 1 ORELSE
  4.1194 +                            (rtac surject_assistI 1 THEN
  4.1195 +                             simp_tac (HOL_basic_ss addsimps id_o_apps) 1))]))
  4.1196 +      end;
  4.1197 +    val surjective = timeit_msg "record surjective proof:" surjective_prf;
  4.1198 +
  4.1199      fun split_meta_prf () =
  4.1200 -        prove false [] split_meta_prop (fn _ =>
  4.1201 +        prove false [] split_meta_prop (fn prems =>
  4.1202           EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  4.1203                  etac meta_allE 1, atac 1,
  4.1204                  rtac (prop_subst OF [surjective]) 1,
  4.1205                  REPEAT (etac meta_allE 1), atac 1]);
  4.1206      val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
  4.1207 -    val split_meta_standard = standard split_meta;
  4.1208 +    fun split_meta_standardise () = standard split_meta;
  4.1209 +    val split_meta_standard = timeit_msg "record split_meta standard:"
  4.1210 +        split_meta_standardise;
  4.1211  
  4.1212      fun split_object_prf_opt () =
  4.1213        let
  4.1214 @@ -2155,16 +2228,16 @@
  4.1215  
  4.1216  
  4.1217      fun split_ex_prf () =
  4.1218 -        prove_standard [] split_ex_prop (fn _ =>
  4.1219 -          EVERY [rtac iffI 1,
  4.1220 -                   etac exE 1,
  4.1221 -                   simp_tac (HOL_basic_ss addsimps [split_meta_standard]) 1,
  4.1222 -                   ex_inst_tac 1,
  4.1223 -                   (*REPEAT (rtac exI 1),*)
  4.1224 -                   atac 1,
  4.1225 -                 REPEAT (etac exE 1),
  4.1226 -                 rtac exI 1,
  4.1227 -                 atac 1]);
  4.1228 +      let
  4.1229 +        val ss   = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
  4.1230 +        val [Pv] = term_vars (prop_of split_object);
  4.1231 +        val cPv  = cterm_of defs_thy Pv;
  4.1232 +        val cP   = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
  4.1233 +        val so3  = cterm_instantiate ([(cPv, cP)]) split_object;
  4.1234 +        val so4  = simplify ss so3;
  4.1235 +      in
  4.1236 +        prove_standard [] split_ex_prop (fn prems => resolve_tac [so4] 1)
  4.1237 +      end;
  4.1238      val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
  4.1239  
  4.1240      fun equality_tac thms =
  4.1241 @@ -2183,6 +2256,7 @@
  4.1242       val equality = timeit_msg "record equality proof:" equality_prf;
  4.1243  
  4.1244      val ((([sel_convs', upd_convs', sel_defs', upd_defs',
  4.1245 +            fold_congs', unfold_congs', surjective',
  4.1246            [split_meta', split_object', split_ex'], derived_defs'],
  4.1247            [surjective', equality']),
  4.1248            [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
  4.1249 @@ -2205,15 +2279,18 @@
  4.1250  
  4.1251  
  4.1252      val sel_upd_simps = sel_convs' @ upd_convs';
  4.1253 +    val sel_upd_defs = sel_defs' @ upd_defs';
  4.1254      val iffs = [ext_inject]
  4.1255 +    val depth = parent_len + 1;
  4.1256      val final_thy =
  4.1257        thms_thy
  4.1258        |> (snd oo PureThy.add_thmss)
  4.1259            [((Binding.name "simps", sel_upd_simps),
  4.1260              [Simplifier.simp_add, Nitpick_Const_Simps.add]),
  4.1261             ((Binding.name "iffs", iffs), [iff_add])]
  4.1262 -      |> put_record name (make_record_info args parent fields extension induct_scheme')
  4.1263 -      |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
  4.1264 +      |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
  4.1265 +      |> put_sel_upd_names full_moreN depth sel_upd_simps
  4.1266 +                           sel_upd_defs (fold_congs', unfold_congs')
  4.1267        |> add_record_equalities extension_id equality'
  4.1268        |> add_extinjects ext_inject
  4.1269        |> add_extsplit extension_name ext_split